diff options
Diffstat (limited to 'backends/hol4/divDefProto2Theory.sig')
-rw-r--r-- | backends/hol4/divDefProto2Theory.sig | 107 |
1 files changed, 53 insertions, 54 deletions
diff --git a/backends/hol4/divDefProto2Theory.sig b/backends/hol4/divDefProto2Theory.sig index 7ce4b194..77d5631e 100644 --- a/backends/hol4/divDefProto2Theory.sig +++ b/backends/hol4/divDefProto2Theory.sig @@ -3,6 +3,7 @@ sig type thm = Thm.thm (* Definitions *) + val even_odd_body_def : thm val fix_def : thm val fix_fuel_P_def : thm val fix_fuel_def : thm @@ -10,12 +11,13 @@ sig val list_t_TY_DEF : thm val list_t_case_def : thm val list_t_size_def : thm - val nth_body1_def : thm - val nth_body_valid_def : thm - val simp_types_def : thm + val nth_body_def : thm (* Theorems *) val datatype_list_t : thm + val even_def : thm + val even_odd_body_is_valid : thm + val even_odd_body_is_valid_aux : thm val fix_fixed_diverges : thm val fix_fixed_eq : thm val fix_fixed_terminates : thm @@ -30,7 +32,6 @@ sig val fix_not_diverge_implies_fix_fuel : thm val fix_not_diverge_implies_fix_fuel_aux : thm val is_valid_fp_body_compute : thm - val is_valid_suffice : thm val list_t_11 : thm val list_t_Axiom : thm val list_t_case_cong : thm @@ -38,14 +39,38 @@ sig val list_t_distinct : thm val list_t_induction : thm val list_t_nchotomy : thm - val nth_body_valid_eq : thm - val nth_body_valid_is_valid : thm + val nth_body_is_valid : thm + val nth_body_is_valid_aux : thm val nth_def : thm + val odd_def : thm val divDefProto2_grammars : type_grammar.grammar * term_grammar.grammar (* [primitives] Parent theory of "divDefProto2" + [even_odd_body_def] Definition + + ⊢ ∀f x. + even_odd_body f x = + case x of + INL 0 => Return (INR (INR T)) + | INL i => + (case f (INR (INL (i − 1))) of + Return (INL v) => Fail Failure + | Return (INR (INL v2)) => Fail Failure + | Return (INR (INR b)) => Return (INR (INR b)) + | Fail e => Fail e + | Diverge => Diverge) + | INR (INL 0) => Return (INR (INR F)) + | INR (INL i) => + (case f (INL (i − 1)) of + Return (INL v) => Fail Failure + | Return (INR (INL v2)) => Fail Failure + | Return (INR (INR b)) => Return (INR (INR b)) + | Fail e => Fail e + | Diverge => Diverge) + | INR (INR v5) => Fail Failure + [fix_def] Definition ⊢ ∀f x. @@ -101,36 +126,10 @@ sig list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧ ∀f. list_t_size f ListNil = 0 - [nth_body1_def] Definition - - ⊢ ∀f x. - nth_body1 f x = - case x of - INL x => - (let - (ls,i) = x - in - case ls of - ListCons x tl => - if u32_to_int i = 0 then Return (INR x) - else - do - i0 <- u32_sub i (int_to_u32 1); - r <- - case f (INL (tl,i0)) of - Return (INL v) => Fail Failure - | Return (INR i1) => Return i1 - | Fail e => Fail e - | Diverge => Diverge; - Return (INR r) - od - | ListNil => Fail Failure) - | INR v3 => Fail Failure - - [nth_body_valid_def] Definition + [nth_body_def] Definition ⊢ ∀f x. - nth_body_valid f x = + nth_body f x = case x of INL x => (let @@ -150,22 +149,22 @@ sig | ListNil => Fail Failure) | INR v2 => Fail Failure - [simp_types_def] Definition - - ⊢ ∀f. simp_types f = - (λx'. - case x' of - INL x => - (case f x of - Return y => Return (INR y) - | Fail e => Fail e - | Diverge => Diverge) - | INR v1 => Fail Failure) - [datatype_list_t] Theorem ⊢ DATATYPE (list_t ListCons ListNil) + [even_def] Theorem + + ⊢ ∀i. even i = if i = 0 then Return T else odd (i − 1) + + [even_odd_body_is_valid] Theorem + + ⊢ is_valid_fp_body (SUC (SUC 0)) even_odd_body + + [even_odd_body_is_valid_aux] Theorem + + ⊢ is_valid_fp_body (SUC (SUC n)) even_odd_body + [fix_fixed_diverges] Theorem ⊢ ∀N f. @@ -273,10 +272,6 @@ sig is_valid_fp_body (NUMERAL (BIT1 n)) h ∧ ∀g. f g x = do z <- g y; h g z od - [is_valid_suffice] Theorem - - ⊢ ∃y. ∀g. g x = g y - [list_t_11] Theorem ⊢ ∀a0 a1 a0' a1'. @@ -312,13 +307,13 @@ sig ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil - [nth_body_valid_eq] Theorem + [nth_body_is_valid] Theorem - ⊢ nth_body_valid = nth_body1 + ⊢ is_valid_fp_body (SUC (SUC 0)) nth_body - [nth_body_valid_is_valid] Theorem + [nth_body_is_valid_aux] Theorem - ⊢ is_valid_fp_body (SUC (SUC 0)) nth_body_valid + ⊢ is_valid_fp_body (SUC (SUC n)) nth_body [nth_def] Theorem @@ -330,6 +325,10 @@ sig else do i0 <- u32_sub i (int_to_u32 1); nth tl i0 od | ListNil => Fail Failure + [odd_def] Theorem + + ⊢ ∀i. odd i = if i = 0 then Return F else even (i − 1) + *) end |