summaryrefslogtreecommitdiff
path: root/backends/hol4/divDefProto2Theory.sig
diff options
context:
space:
mode:
Diffstat (limited to 'backends/hol4/divDefProto2Theory.sig')
-rw-r--r--backends/hol4/divDefProto2Theory.sig400
1 files changed, 255 insertions, 145 deletions
diff --git a/backends/hol4/divDefProto2Theory.sig b/backends/hol4/divDefProto2Theory.sig
index 349aabf7..7ce4b194 100644
--- a/backends/hol4/divDefProto2Theory.sig
+++ b/backends/hol4/divDefProto2Theory.sig
@@ -6,25 +6,41 @@ sig
val fix_def : thm
val fix_fuel_P_def : thm
val fix_fuel_def : thm
- val ftree_TY_DEF : thm
- val ftree_case_def : thm
- val ftree_size_def : thm
val is_valid_fp_body_def : thm
+ 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
(* Theorems *)
- val datatype_ftree : thm
- val eval_ftree_compute : thm
- val eval_ftree_def : thm
- val eval_ftree_ind : thm
+ val datatype_list_t : thm
+ val fix_fixed_diverges : thm
+ val fix_fixed_eq : thm
+ val fix_fixed_terminates : thm
+ val fix_fuel_P_least : thm
val fix_fuel_compute : thm
- val ftree_11 : thm
- val ftree_Axiom : thm
- val ftree_case_cong : thm
- val ftree_case_eq : thm
- val ftree_distinct : thm
- val ftree_induction : thm
- val ftree_nchotomy : thm
- val ftree_size_eq : thm
+ val fix_fuel_eq_fix : thm
+ val fix_fuel_mono : thm
+ val fix_fuel_mono_aux : thm
+ val fix_fuel_mono_least : thm
+ val fix_fuel_not_diverge_eq_fix : thm
+ val fix_fuel_not_diverge_eq_fix_aux : thm
+ 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
+ val list_t_case_eq : thm
+ 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_def : thm
val divDefProto2_grammars : type_grammar.grammar * term_grammar.grammar
(*
@@ -47,124 +63,130 @@ sig
⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧
∀n f x. fix_fuel (SUC n) f x = f (fix_fuel n f) x
- [ftree_TY_DEF] Definition
+ [is_valid_fp_body_def] Definition
+
+ ⊢ (∀f. is_valid_fp_body 0 f ⇔ F) ∧
+ ∀n f.
+ is_valid_fp_body (SUC n) f ⇔
+ ∀x. (∀g h. f g x = f h x) ∨
+ ∃h y.
+ is_valid_fp_body n h ∧ ∀g. f g x = do z <- g y; h g z od
+
+ [list_t_TY_DEF] Definition
⊢ ∃rep.
TYPE_DEFINITION
(λa0'.
- ∀ $var$('ftree') $var$('@temp @ind_typedivDefProto20prod')
- $var$('@temp @ind_typedivDefProto21list').
+ ∀ $var$('list_t').
(∀a0'.
- (∃a. a0' =
- (λa.
- ind_type$CONSTR 0 (ARB,ARB)
- (ind_type$FCONS a (λn. ind_type$BOTTOM)))
- a ∧
- $var$('@temp @ind_typedivDefProto20prod') a) ∨
- (∃a. a0' =
- (λa.
- ind_type$CONSTR (SUC 0) (a,ARB)
- (λn. ind_type$BOTTOM)) a) ⇒
- $var$('ftree') a0') ∧
- (∀a1'.
(∃a0 a1.
- a1' =
+ a0' =
(λa0 a1.
- ind_type$CONSTR (SUC (SUC 0)) (ARB,a0)
+ ind_type$CONSTR 0 a0
(ind_type$FCONS a1 (λn. ind_type$BOTTOM)))
- a0 a1 ∧
- $var$('@temp @ind_typedivDefProto21list') a1) ⇒
- $var$('@temp @ind_typedivDefProto20prod') a1') ∧
- (∀a2.
- a2 =
- ind_type$CONSTR (SUC (SUC (SUC 0))) (ARB,ARB)
- (λn. ind_type$BOTTOM) ∨
- (∃a0 a1.
- a2 =
- (λa0 a1.
- ind_type$CONSTR (SUC (SUC (SUC (SUC 0))))
- (ARB,ARB)
- (ind_type$FCONS a0
- (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
- a0 a1 ∧ $var$('ftree') a0 ∧
- $var$('@temp @ind_typedivDefProto21list') a1) ⇒
- $var$('@temp @ind_typedivDefProto21list') a2) ⇒
- $var$('ftree') a0') rep
+ 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
- [ftree_case_def] Definition
+ [list_t_case_def] Definition
- ⊢ (∀a f f1. ftree_CASE (Rec a) f f1 = f a) ∧
- ∀a f f1. ftree_CASE (NRec a) f f1 = f1 a
+ ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧
+ ∀f v. list_t_CASE ListNil f v = v
- [ftree_size_def] Definition
+ [list_t_size_def] Definition
- ⊢ (∀f a. ftree_size f (Rec a) = 1 + ftree1_size f a) ∧
- (∀f a. ftree_size f (NRec a) = 1) ∧
- (∀f a0 a1. ftree1_size f (a0,a1) = 1 + ftree2_size f a1) ∧
- (∀f. ftree2_size f [] = 0) ∧
- ∀f a0 a1.
- ftree2_size f (a0::a1) = 1 + (ftree_size f a0 + ftree2_size f a1)
+ ⊢ (∀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
- [is_valid_fp_body_def] Definition
+ [nth_body1_def] Definition
- ⊢ ∀f. is_valid_fp_body f ⇔ ∀x. ∃n ft. ∀g. f g x = eval_ftree n g ft
-
- [datatype_ftree] Theorem
-
- ⊢ DATATYPE (ftree Rec NRec)
-
- [eval_ftree_compute] Theorem
-
- ⊢ (∀x g fs. eval_ftree 0 g (fs,x) = Diverge) ∧
- (∀x n g fs.
- eval_ftree (NUMERAL (BIT1 n)) g (fs,x) =
- case x of
- INL r => r
- | INR (y,i) =>
- case g y of
- Return z =>
- (let
- f = EL i fs
- in
- eval_ftree (NUMERAL (BIT1 n) − 1) g (fs,f z))
- | Fail e => Fail e
- | Diverge => Diverge) ∧
- ∀x n g fs.
- eval_ftree (NUMERAL (BIT2 n)) g (fs,x) =
+ ⊢ ∀f x.
+ nth_body1 f x =
case x of
- INL r => r
- | INR (y,i) =>
- case g y of
- Return z =>
- (let
- f = EL i fs
- in
- eval_ftree (NUMERAL (BIT1 n)) g (fs,f z))
- | Fail e => Fail e
- | Diverge => Diverge
-
- [eval_ftree_def] Theorem
-
- ⊢ (∀x g fs. eval_ftree 0 g (fs,x) = Diverge) ∧
- ∀x n g fs.
- eval_ftree (SUC n) g (fs,x) =
+ 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
+
+ ⊢ ∀f x.
+ nth_body_valid f x =
case x of
- INL r => r
- | INR (y,i) =>
- case g y of
- Return z => (let f = EL i fs in eval_ftree n g (fs,f z))
- | Fail e => Fail e
- | Diverge => Diverge
-
- [eval_ftree_ind] Theorem
-
- ⊢ ∀P. (∀g fs x. P 0 g (fs,x)) ∧
- (∀n g fs x.
- (∀v1 y i z f.
- x = INR v1 ∧ v1 = (y,i) ∧ g y = Return z ∧ f = EL i fs ⇒
- P n g (fs,f z)) ⇒
- P (SUC n) g (fs,x)) ⇒
- ∀v v1 v2 v3. P v v1 (v2,v3)
+ 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 <- f (INL (tl,i0));
+ case r of
+ INL v => Fail Failure
+ | INR i1 => Return (INR i1)
+ od
+ | 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)
+
+ [fix_fixed_diverges] Theorem
+
+ ⊢ ∀N f.
+ is_valid_fp_body N f ⇒
+ ∀x. ¬(∃n. fix_fuel_P f x n) ⇒ fix f x = f (fix f) x
+
+ [fix_fixed_eq] Theorem
+
+ ⊢ ∀N f. is_valid_fp_body N f ⇒ ∀x. fix f x = f (fix f) x
+
+ [fix_fixed_terminates] Theorem
+
+ ⊢ ∀N f.
+ is_valid_fp_body N f ⇒
+ ∀x n. fix_fuel_P f x n ⇒ fix f x = f (fix f) x
+
+ [fix_fuel_P_least] Theorem
+
+ ⊢ ∀f n x.
+ fix_fuel n f x ≠ Diverge ⇒
+ fix_fuel_P f x ($LEAST (fix_fuel_P f x))
[fix_fuel_compute] Theorem
@@ -176,49 +198,137 @@ sig
fix_fuel (NUMERAL (BIT2 n)) f x =
f (fix_fuel (NUMERAL (BIT1 n)) f) x
- [ftree_11] Theorem
+ [fix_fuel_eq_fix] Theorem
+
+ ⊢ ∀N f.
+ is_valid_fp_body N f ⇒
+ ∀n x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix f x
+
+ [fix_fuel_mono] Theorem
+
+ ⊢ ∀N f.
+ is_valid_fp_body N f ⇒
+ ∀n x.
+ fix_fuel_P f x n ⇒ ∀m. n ≤ m ⇒ fix_fuel n f x = fix_fuel m f x
+
+ [fix_fuel_mono_aux] Theorem
+
+ ⊢ ∀n N M g f.
+ is_valid_fp_body M f ⇒
+ is_valid_fp_body N g ⇒
+ ∀x. ¬is_diverge (g (fix_fuel n f) x) ⇒
+ ∀m. n ≤ m ⇒ g (fix_fuel n f) x = g (fix_fuel m f) x
+
+ [fix_fuel_mono_least] Theorem
+
+ ⊢ ∀N f.
+ is_valid_fp_body N f ⇒
+ ∀n x.
+ fix_fuel_P f x n ⇒
+ fix_fuel n f x = fix_fuel ($LEAST (fix_fuel_P f x)) f x
+
+ [fix_fuel_not_diverge_eq_fix] Theorem
+
+ ⊢ ∀N f.
+ is_valid_fp_body N f ⇒
+ ∀n x.
+ f (fix_fuel n f) x ≠ Diverge ⇒ f (fix f) x = f (fix_fuel n f) x
+
+ [fix_fuel_not_diverge_eq_fix_aux] Theorem
+
+ ⊢ ∀N M g f.
+ is_valid_fp_body M f ⇒
+ is_valid_fp_body N g ⇒
+ ∀n x.
+ g (fix_fuel n f) x ≠ Diverge ⇒ g (fix f) x = g (fix_fuel n f) x
+
+ [fix_not_diverge_implies_fix_fuel] Theorem
+
+ ⊢ ∀N f.
+ is_valid_fp_body N f ⇒
+ ∀x. f (fix f) x ≠ Diverge ⇒ ∃n. f (fix f) x = f (fix_fuel n f) x
+
+ [fix_not_diverge_implies_fix_fuel_aux] Theorem
+
+ ⊢ ∀N M g f.
+ is_valid_fp_body M f ⇒
+ is_valid_fp_body N g ⇒
+ ∀x. g (fix f) x ≠ Diverge ⇒
+ ∃n. g (fix f) x = g (fix_fuel n f) x ∧
+ ∀m. n ≤ m ⇒ g (fix_fuel m f) x = g (fix_fuel n f) x
+
+ [is_valid_fp_body_compute] Theorem
+
+ ⊢ (∀f. is_valid_fp_body 0 f ⇔ F) ∧
+ (∀n f.
+ is_valid_fp_body (NUMERAL (BIT1 n)) f ⇔
+ ∀x. (∀g h. f g x = f h x) ∨
+ ∃h y.
+ is_valid_fp_body (NUMERAL (BIT1 n) − 1) h ∧
+ ∀g. f g x = do z <- g y; h g z od) ∧
+ ∀n f.
+ is_valid_fp_body (NUMERAL (BIT2 n)) f ⇔
+ ∀x. (∀g h. f g x = f h x) ∨
+ ∃h y.
+ 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'.
+ 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
- ⊢ (∀a a'. Rec a = Rec a' ⇔ a = a') ∧ ∀a a'. NRec a = NRec a' ⇔ a = a'
+ ⊢ ∀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'
- [ftree_Axiom] Theorem
+ [list_t_case_eq] Theorem
- ⊢ ∀f0 f1 f2 f3 f4. ∃fn0 fn1 fn2.
- (∀a. fn0 (Rec a) = f0 a (fn1 a)) ∧ (∀a. fn0 (NRec a) = f1 a) ∧
- (∀a0 a1. fn1 (a0,a1) = f2 a0 a1 (fn2 a1)) ∧ fn2 [] = f3 ∧
- ∀a0 a1. fn2 (a0::a1) = f4 a0 a1 (fn0 a0) (fn2 a1)
+ ⊢ list_t_CASE x f v = v' ⇔
+ (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v'
- [ftree_case_cong] Theorem
+ [list_t_distinct] Theorem
- ⊢ ∀M M' f f1.
- M = M' ∧ (∀a. M' = Rec a ⇒ f a = f' a) ∧
- (∀a. M' = NRec a ⇒ f1 a = f1' a) ⇒
- ftree_CASE M f f1 = ftree_CASE M' f' f1'
+ ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil
- [ftree_case_eq] Theorem
+ [list_t_induction] Theorem
- ⊢ ftree_CASE x f f1 = v ⇔
- (∃p. x = Rec p ∧ f p = v) ∨ ∃f'. x = NRec f' ∧ f1 f' = v
+ ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l
- [ftree_distinct] Theorem
+ [list_t_nchotomy] Theorem
- ⊢ ∀a' a. Rec a ≠ NRec a'
+ ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil
- [ftree_induction] Theorem
+ [nth_body_valid_eq] Theorem
- ⊢ ∀P0 P1 P2.
- (∀p. P1 p ⇒ P0 (Rec p)) ∧ (∀f. P0 (NRec f)) ∧
- (∀l. P2 l ⇒ ∀f. P1 (f,l)) ∧ P2 [] ∧
- (∀f l. P0 f ∧ P2 l ⇒ P2 (f::l)) ⇒
- (∀f. P0 f) ∧ (∀p. P1 p) ∧ ∀l. P2 l
+ ⊢ nth_body_valid = nth_body1
- [ftree_nchotomy] Theorem
+ [nth_body_valid_is_valid] Theorem
- ⊢ ∀ff. (∃p. ff = Rec p) ∨ ∃f. ff = NRec f
+ ⊢ is_valid_fp_body (SUC (SUC 0)) nth_body_valid
- [ftree_size_eq] Theorem
+ [nth_def] Theorem
- ⊢ ftree1_size f = pair_size (λv. 0) (list_size (ftree_size f)) ∧
- ftree2_size f = list_size (ftree_size f)
+ ⊢ ∀ls i.
+ nth ls i =
+ case ls of
+ ListCons x tl =>
+ if u32_to_int i = 0 then Return x
+ else do i0 <- u32_sub i (int_to_u32 1); nth tl i0 od
+ | ListNil => Fail Failure
*)
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-12 10:38:14 +0000