summaryrefslogtreecommitdiff
path: root/tests/hol4/paper/paperTheory.sig
diff options
context:
space:
mode:
authorGuillaume Boisseau2024-05-24 17:10:02 +0200
committerGitHub2024-05-24 17:10:02 +0200
commit4971b7edf4538144df735f9fa5327fe4d0e2e003 (patch)
tree979ed531f66c3b0040fa5714fa70db606ca786c0 /tests/hol4/paper/paperTheory.sig
parentfbfa0e13ab56ee847e891fa7d798d2eb226b6794 (diff)
parent3adbe18d36df3767e98f30b760ccd9c6ace640ad (diff)
Merge pull request #206 from AeneasVerif/subdir
Diffstat (limited to 'tests/hol4/paper/paperTheory.sig')
-rw-r--r--tests/hol4/paper/paperTheory.sig210
1 files changed, 210 insertions, 0 deletions
diff --git a/tests/hol4/paper/paperTheory.sig b/tests/hol4/paper/paperTheory.sig
new file mode 100644
index 00000000..2da80da1
--- /dev/null
+++ b/tests/hol4/paper/paperTheory.sig
@@ -0,0 +1,210 @@
+signature paperTheory =
+sig
+ type thm = Thm.thm
+
+ (* Definitions *)
+ val call_choose_fwd_def : thm
+ val choose_back_def : thm
+ val choose_fwd_def : thm
+ val list_nth_mut_back_def : thm
+ val list_nth_mut_fwd_def : thm
+ val list_t_TY_DEF : thm
+ val list_t_case_def : thm
+ val list_t_size_def : thm
+ val ref_incr_fwd_back_def : thm
+ val sum_fwd_def : thm
+ val test_choose_fwd_def : thm
+ val test_incr_fwd_def : thm
+ val test_nth_fwd_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 paper_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+ [divDef] Parent theory of "paper"
+
+ [call_choose_fwd_def] Definition
+
+ ⊢ ∀p. call_choose_fwd p =
+ (let
+ (px,py) = p
+ in
+ do
+ pz <- choose_fwd T px py;
+ pz0 <- u32_add pz (int_to_u32 1);
+ (px0,_) <- choose_back T px py pz0;
+ Return px0
+ od)
+
+ [choose_back_def] Definition
+
+ ⊢ ∀b x y ret.
+ choose_back b x y ret =
+ if b then Return (ret,y) else Return (x,ret)
+
+ [choose_fwd_def] Definition
+
+ ⊢ ∀b x y. choose_fwd b x y = if b then Return x else Return y
+
+ [list_nth_mut_back_def] Definition
+
+ ⊢ ∀l i ret.
+ list_nth_mut_back l i ret =
+ case l of
+ ListCons x tl =>
+ if i = int_to_u32 0 then Return (ListCons ret tl)
+ else
+ do
+ i0 <- u32_sub i (int_to_u32 1);
+ tl0 <- list_nth_mut_back tl i0 ret;
+ Return (ListCons x tl0)
+ od
+ | ListNil => Fail Failure
+
+ [list_nth_mut_fwd_def] Definition
+
+ ⊢ ∀l i.
+ list_nth_mut_fwd l i =
+ case l of
+ ListCons x tl =>
+ if i = int_to_u32 0 then Return x
+ else
+ do
+ i0 <- u32_sub i (int_to_u32 1);
+ list_nth_mut_fwd tl i0
+ od
+ | ListNil => Fail Failure
+
+ [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
+
+ [ref_incr_fwd_back_def] Definition
+
+ ⊢ ∀x. ref_incr_fwd_back x = i32_add x (int_to_i32 1)
+
+ [sum_fwd_def] Definition
+
+ ⊢ ∀l. sum_fwd l =
+ case l of
+ ListCons x tl => do i <- sum_fwd tl; i32_add x i od
+ | ListNil => Return (int_to_i32 0)
+
+ [test_choose_fwd_def] Definition
+
+ ⊢ test_choose_fwd =
+ do
+ z <- choose_fwd T (int_to_i32 0) (int_to_i32 0);
+ z0 <- i32_add z (int_to_i32 1);
+ if z0 ≠ int_to_i32 1 then Fail Failure
+ else
+ do
+ (x,y) <- choose_back T (int_to_i32 0) (int_to_i32 0) z0;
+ if x ≠ int_to_i32 1 then Fail Failure
+ else if y ≠ int_to_i32 0 then Fail Failure
+ else Return ()
+ od
+ od
+
+ [test_incr_fwd_def] Definition
+
+ ⊢ test_incr_fwd =
+ do
+ x <- ref_incr_fwd_back (int_to_i32 0);
+ if x ≠ int_to_i32 1 then Fail Failure else Return ()
+ od
+
+ [test_nth_fwd_def] Definition
+
+ ⊢ test_nth_fwd =
+ (let
+ l = ListNil;
+ l0 = ListCons (int_to_i32 3) l;
+ l1 = ListCons (int_to_i32 2) l0
+ in
+ do
+ x <-
+ list_nth_mut_fwd (ListCons (int_to_i32 1) l1) (int_to_u32 2);
+ x0 <- i32_add x (int_to_i32 1);
+ l2 <-
+ list_nth_mut_back (ListCons (int_to_i32 1) l1)
+ (int_to_u32 2) x0;
+ i <- sum_fwd l2;
+ if i ≠ int_to_i32 7 then Fail Failure else Return ()
+ od)
+
+ [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