summaryrefslogtreecommitdiff
path: root/tests/hol4/polonius_list
diff options
context:
space:
mode:
Diffstat (limited to 'tests/hol4/polonius_list')
-rw-r--r--tests/hol4/polonius_list/Holmakefile5
-rw-r--r--tests/hol4/polonius_list/poloniusListScript.sml37
-rw-r--r--tests/hol4/polonius_list/poloniusListTheory.sig120
3 files changed, 162 insertions, 0 deletions
diff --git a/tests/hol4/polonius_list/Holmakefile b/tests/hol4/polonius_list/Holmakefile
new file mode 100644
index 00000000..3c4b8973
--- /dev/null
+++ b/tests/hol4/polonius_list/Holmakefile
@@ -0,0 +1,5 @@
+# This file was automatically generated - modify ../Holmakefile.template instead
+INCLUDES = ../../../backends/hol4
+
+all: $(DEFAULT_TARGETS)
+.PHONY: all
diff --git a/tests/hol4/polonius_list/poloniusListScript.sml b/tests/hol4/polonius_list/poloniusListScript.sml
new file mode 100644
index 00000000..06876ed4
--- /dev/null
+++ b/tests/hol4/polonius_list/poloniusListScript.sml
@@ -0,0 +1,37 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [polonius_list] *)
+open primitivesLib divDefLib
+
+val _ = new_theory "poloniusList"
+
+
+Datatype:
+ (** [polonius_list::List] *)
+ list_t = | ListCons 't list_t | ListNil
+End
+
+val [get_list_at_x_fwd_def] = DefineDiv ‘
+ (** [polonius_list::get_list_at_x]: forward function *)
+ get_list_at_x_fwd (ls : u32 list_t) (x : u32) : u32 list_t result =
+ (case ls of
+ | ListCons hd tl =>
+ if hd = x then Return (ListCons hd tl) else get_list_at_x_fwd tl x
+ | ListNil => Return ListNil)
+’
+
+val [get_list_at_x_back_def] = DefineDiv ‘
+ (** [polonius_list::get_list_at_x]: backward function 0 *)
+ get_list_at_x_back
+ (ls : u32 list_t) (x : u32) (ret : u32 list_t) : u32 list_t result =
+ (case ls of
+ | ListCons hd tl =>
+ if hd = x
+ then Return ret
+ else (do
+ tl0 <- get_list_at_x_back tl x ret;
+ Return (ListCons hd tl0)
+ od)
+ | ListNil => Return ret)
+’
+
+val _ = export_theory ()
diff --git a/tests/hol4/polonius_list/poloniusListTheory.sig b/tests/hol4/polonius_list/poloniusListTheory.sig
new file mode 100644
index 00000000..41f21df7
--- /dev/null
+++ b/tests/hol4/polonius_list/poloniusListTheory.sig
@@ -0,0 +1,120 @@
+signature poloniusListTheory =
+sig
+ type thm = Thm.thm
+
+ (* Definitions *)
+ val get_list_at_x_back_def : thm
+ val get_list_at_x_fwd_def : thm
+ val list_t_TY_DEF : thm
+ val list_t_case_def : thm
+ val list_t_size_def : thm
+
+ (* Theorems *)
+ val datatype_list_t : thm
+ val list_t_11 : thm
+ val list_t_Axiom : thm
+ val list_t_case_cong : thm
+ val list_t_case_eq : thm
+ val list_t_distinct : thm
+ val list_t_induction : thm
+ val list_t_nchotomy : thm
+
+ val poloniusList_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+ [divDef] Parent theory of "poloniusList"
+
+ [get_list_at_x_back_def] Definition
+
+ ⊢ ∀ls x ret.
+ get_list_at_x_back ls x ret =
+ case ls of
+ ListCons hd tl =>
+ if hd = x then Return ret
+ else
+ do
+ tl0 <- get_list_at_x_back tl x ret;
+ Return (ListCons hd tl0)
+ od
+ | ListNil => Return ret
+
+ [get_list_at_x_fwd_def] Definition
+
+ ⊢ ∀ls x.
+ get_list_at_x_fwd ls x =
+ case ls of
+ ListCons hd tl =>
+ if hd = x then Return (ListCons hd tl)
+ else get_list_at_x_fwd tl x
+ | ListNil => Return ListNil
+
+ [list_t_TY_DEF] Definition
+
+ ⊢ ∃rep.
+ TYPE_DEFINITION
+ (λa0'.
+ ∀ $var$('list_t').
+ (∀a0'.
+ (∃a0 a1.
+ a0' =
+ (λa0 a1.
+ ind_type$CONSTR 0 a0
+ (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))
+ a0 a1 ∧ $var$('list_t') a1) ∨
+ a0' =
+ ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
+ $var$('list_t') a0') ⇒
+ $var$('list_t') a0') rep
+
+ [list_t_case_def] Definition
+
+ ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧
+ ∀f v. list_t_CASE ListNil f v = v
+
+ [list_t_size_def] Definition
+
+ ⊢ (∀f a0 a1.
+ list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧
+ ∀f. list_t_size f ListNil = 0
+
+ [datatype_list_t] Theorem
+
+ ⊢ DATATYPE (list_t ListCons ListNil)
+
+ [list_t_11] Theorem
+
+ ⊢ ∀a0 a1 a0' a1'.
+ ListCons a0 a1 = ListCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
+
+ [list_t_Axiom] Theorem
+
+ ⊢ ∀f0 f1. ∃fn.
+ (∀a0 a1. fn (ListCons a0 a1) = f0 a0 a1 (fn a1)) ∧
+ fn ListNil = f1
+
+ [list_t_case_cong] Theorem
+
+ ⊢ ∀M M' f v.
+ M = M' ∧ (∀a0 a1. M' = ListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧
+ (M' = ListNil ⇒ v = v') ⇒
+ list_t_CASE M f v = list_t_CASE M' f' v'
+
+ [list_t_case_eq] Theorem
+
+ ⊢ list_t_CASE x f v = v' ⇔
+ (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v'
+
+ [list_t_distinct] Theorem
+
+ ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil
+
+ [list_t_induction] Theorem
+
+ ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l
+
+ [list_t_nchotomy] Theorem
+
+ ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil
+
+
+*)
+end