diff options
| -rw-r--r-- | backends/hol4/divDefProto2Script.sml | 678 | ||||
| -rw-r--r-- | backends/hol4/divDefProto2Theory.sig | 225 | ||||
| -rw-r--r-- | backends/hol4/primitivesArithScript.sml | 1 |
3 files changed, 904 insertions, 0 deletions
diff --git a/backends/hol4/divDefProto2Script.sml b/backends/hol4/divDefProto2Script.sml new file mode 100644 index 00000000..985b930f --- /dev/null +++ b/backends/hol4/divDefProto2Script.sml @@ -0,0 +1,678 @@ +(* Prototype: divDefLib but with general combinators *) + +open HolKernel boolLib bossLib Parse +open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory + +open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory +open primitivesLib + +val _ = new_theory "divDefProto2" + + +(* + * Test with a general validity predicate. + * + * TODO: this works! Cleanup. + *) +val fix_fuel_def = Define ‘ + (fix_fuel (0 : num) (f : ('a -> 'a result) -> 'a -> 'a result) (x : 'a) : 'a result = Diverge) ∧ + (fix_fuel (SUC n) (f : ('a -> 'a result) -> 'a -> 'a result) (x : 'a) : 'a result = f (fix_fuel n f) x) +’ + +val fix_fuel_P_def = Define ‘ + fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x)) +’ + +val fix_def = Define ‘ + fix (f : ('a -> 'a result) -> 'a -> 'a result) (x : 'a) : 'a result = + if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge +’ + +val is_valid_fp_body_def = Define ‘ + (is_valid_fp_body (0 : num) (f : ('a -> 'a result) -> 'a -> 'a result) = F) ∧ + + (is_valid_fp_body (SUC n) (f : ('a -> 'a result) -> 'a -> 'a result) = + ∀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)) +’ + +(* Auxiliary lemma. + We generalize the goal of fix_fuel_mono in the case the fuel is non-empty + (this allows us to unfold definitions like ‘fix_fuel’ once, and reveal + a first intermediate function). + + Important: the structure of the proof is induction over ‘n’ then ‘N’. + *) +Theorem fix_fuel_mono_aux: + ∀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 +Proof + Induct_on ‘n’ >> + Induct_on ‘N’ >- fs [is_valid_fp_body_def] + >-( + rw [] >> + fs [is_valid_fp_body_def, is_diverge_def] >> + first_x_assum (qspec_assume ‘x’) >> + rw [] + >-((* Case 1: the continuation doesn't matter *) fs []) >> + (* Case 2: the continuation *does* matter (i.e., there is a recursive call *) + (* Instantiate the validity property with the different continuations *) + first_assum (qspec_assume ‘fix_fuel n f’) >> + first_assum (qspec_assume ‘fix_fuel n' f’) >> + fs [] >> + ntac 3 (pop_assum ignore_tac) >> + fs [bind_def] >> + fs [fix_fuel_def]) + >-(fs [is_valid_fp_body_def]) >> + rw [] >> + qpat_assum ‘is_valid_fp_body (SUC N) g’ mp_tac >> + pure_rewrite_tac [is_valid_fp_body_def] >> + fs [is_diverge_def] >> + rw [] >> + first_x_assum (qspec_assume ‘x’) >> + rw [] + >-((* Case 1: the continuation doesn't matter *) fs []) >> + (* Case 2: the continuation *does* matter (i.e., there is a recursive call *) + (* Use the validity property with the different continuations *) + fs [] >> pop_assum ignore_tac >> + fs [bind_def, fix_fuel_def] >> + Cases_on ‘m’ >- int_tac >> + fs [fix_fuel_def] >> + (* *) + last_x_assum (qspecl_assume [‘M’, ‘M’, ‘f’, ‘f’]) >> + gvs [] >> + first_x_assum (qspec_assume ‘y’) >> + Cases_on ‘f (fix_fuel n f) y’ >> fs [] >> + first_x_assum (qspec_assume ‘n'’) >> gvs [] >> Cases_on ‘f (fix_fuel n' f) y’ >> fs [] >> + (* *) + first_assum (qspecl_assume [‘M’, ‘h’, ‘f’]) >> + gvs [] +QED + +Theorem fix_fuel_mono: + ∀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 +Proof + rw [] >> + Cases_on ‘n’ + >-(fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >> + fs [fix_fuel_P_def, fix_fuel_def] >> rw [] >> + qspecl_assume [‘n'’, ‘N’, ‘N’, ‘f’, ‘f’] fix_fuel_mono_aux >> + Cases_on ‘m’ >- fs [] >> + gvs [fix_fuel_def] +QED + +(* TODO: remove? *) +Theorem fix_fuel_mono_least: + ∀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 +Proof + rw [] >> + pure_once_rewrite_tac [EQ_SYM_EQ] >> + irule fix_fuel_mono >> fs [] >> + (* Use the "fundamental" property about $LEAST *) + qspec_assume ‘fix_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >> + (* Prove the premise *) + pop_assum sg_premise_tac >- metis_tac [] >> fs [] >> + conj_tac + >- (spose_not_then assume_tac >> fs [not_le_eq_gt]) >> + metis_tac [] +QED + +Theorem fix_fuel_eq_fix: + ∀N f. is_valid_fp_body N f ⇒ + ∀n x. fix_fuel_P f x n ⇒ + fix_fuel n f x = fix f x +Proof + fs [fix_def] >> + rw [] >> + imp_res_tac fix_fuel_mono_least >> + fs [fix_fuel_P_def, is_diverge_def] >> + case_tac >> fs [] +QED + +Theorem fix_fuel_P_least: + ∀f n x. fix_fuel n f x ≠ Diverge ⇒ fix_fuel_P f x ($LEAST (fix_fuel_P f x)) +Proof + rw [] >> + qspec_assume ‘fix_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >> + (* Prove the premise *) + pop_assum sg_premise_tac + >-(fs [fix_fuel_P_def, is_diverge_def] >> qexists ‘n’ >> fs [] >> case_tac >> fs []) >> + rw [] +QED + +(* If ‘g (fix f) x’ doesn't diverge, we can exhibit some fuel *) +Theorem fix_not_diverge_implies_fix_fuel_aux: + ∀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 +Proof + Induct_on ‘N’ + >-(fs [is_valid_fp_body_def]) >> + rw [is_valid_fp_body_def] >> + first_x_assum (qspec_assume ‘x’) >> rw [] + >-(first_assum (qspecl_assume [‘fix f’, ‘fix_fuel 0 f’]) >> fs []) >> + (* Use the validity hypothesis *) + fs [] >> pop_assum ignore_tac >> + (* Use the induction hypothesis *) + last_x_assum (qspecl_assume [‘M’, ‘h’, ‘f’]) >> gvs [] >> + (* Case disjunction on ‘fix f ÿ’*) + Cases_on ‘fix f y’ >> fs [bind_def] >~ [‘fix f y = Fail _’] + >-( + (* Fail case: easy, the call to ‘h’ is ignored *) + fs [fix_def] >> pop_assum mp_tac >> rw [] >> + qexists ‘$LEAST (fix_fuel_P f y)’ >> + fs [] >> + (* Use the monotonicity property for ‘f’ *) + rw [] >> + qspecl_assume [‘M’, ‘f’] fix_fuel_mono >> gvs [] >> + first_x_assum (qspecl_assume [‘$LEAST (fix_fuel_P f y)’, ‘y’]) >> gvs [] >> + fs [fix_fuel_P_def, is_diverge_def] >> gvs [] >> + first_x_assum (qspecl_assume [‘m’]) >> gvs [] >> + first_x_assum (fn th => assume_tac (GSYM th)) >> fs [] + ) >> + (* Return case: we must take the maximum of the fuel for ‘f’ and ‘h’, and use + the monotonicity property *) + fs [fix_def] >> pop_assum mp_tac >> rw [] >> + first_x_assum (qspec_assume ‘a’) >> gvs [] >> + qexists ‘MAX ($LEAST (fix_fuel_P f y)) n'’ >> fs [] >> + (* Use the monotonicity properties *) + (* Instantiate the Monotonicity property for ‘f’ (the induction hypothesis gives + the one for ‘h’) *) + qspecl_assume [‘M’, ‘f’] fix_fuel_mono >> gvs [] >> + first_x_assum (qspecl_assume [‘$LEAST (fix_fuel_P f y)’, ‘y’]) >> gvs [] >> + fs [fix_fuel_P_def, is_diverge_def] >> gvs [] >> + first_x_assum (qspecl_assume [‘MAX ($LEAST (fix_fuel_P f y)) n'’]) >> gvs [] >> + first_x_assum (fn th => assume_tac (GSYM th)) >> fs [] >> + (* Prove the monotonicity property for ‘do z <- fix f y; h (fix f) z’ *) + rw [] >> + (* First, one of the ‘fix_fuel ... f y’ doesn't use the proper fuel *) + sg ‘fix_fuel ($LEAST (fix_fuel_P f y)) f y = Return a’ + >-( + qspecl_assume [‘f’, ‘MAX ($LEAST (fix_fuel_P f y)) n'’, ‘y’] fix_fuel_P_least >> + gvs [fix_fuel_P_def, is_diverge_def] >> + Cases_on ‘fix_fuel ($LEAST (fix_fuel_P f y)) f y’ >> fs [] >> + (* Use the monotonicity property - there are two goals here *) + qspecl_assume [‘M’, ‘f’] fix_fuel_mono >> gvs [] >> + first_x_assum (qspecl_assume [‘$LEAST (fix_fuel_P f y)’, ‘y’]) >> gvs [] >> + fs [fix_fuel_P_def, is_diverge_def] >> gvs [] >> + first_x_assum (qspecl_assume [‘MAX ($LEAST (fix_fuel_P f y)) n'’]) >> gvs []) >> + (* Instantiate the monotonicity property for ‘f’ *) + qspecl_assume [‘M’, ‘f’] fix_fuel_mono >> gvs [] >> + first_x_assum (qspecl_assume [‘$LEAST (fix_fuel_P f y)’, ‘y’]) >> gvs [] >> + gvs [fix_fuel_P_def, is_diverge_def] >> gvs [] >> + first_x_assum (qspecl_assume [‘m’]) >> gvs [] >> + first_x_assum (fn th => assume_tac (GSYM th)) >> fs [] +QED + +(* If ‘g (fix f) x’ doesn't diverge, we can exhibit some fuel *) +Theorem fix_not_diverge_implies_fix_fuel: + ∀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 +Proof + metis_tac [fix_not_diverge_implies_fix_fuel_aux] +QED + +Theorem fix_fixed_diverges: + ∀N f. is_valid_fp_body N f ⇒ ∀x. ~(∃ n. fix_fuel_P f x n) ⇒ fix f x = f (fix f) x +Proof + (* We do the proof by contraposition: if ‘f (fix f) x’ doesn't diverge, we + can exhibit some fuel (lemma [fix_not_diverge_implies_fix_fuel]) *) + rw [fix_def] >> + imp_res_tac fix_not_diverge_implies_fix_fuel >> + pop_assum (qspec_assume ‘x’) >> + fs [fix_fuel_P_def, is_diverge_def] >> + (* Case analysis: we have to prove that the ‘Return’ and ‘Fail’ cases lead + to a contradiction *) + Cases_on ‘f (fix f) x’ >> gvs [] >> + first_x_assum (qspec_assume ‘SUC n’) >> fs [fix_fuel_def] >> + pop_assum mp_tac >> case_tac >> fs [] +QED + +(* If ‘g (fix_fuel n f) x’ doesn't diverge, then it is equal to ‘g (fix f) x’ *) +Theorem fix_fuel_not_diverge_eq_fix_aux: + ∀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 +Proof + Induct_on ‘N’ + >-(fs [is_valid_fp_body_def]) >> + rw [is_valid_fp_body_def] >> + first_x_assum (qspec_assume ‘x’) >> rw [] + >-(first_assum (qspecl_assume [‘fix f’, ‘fix_fuel 0 f’]) >> fs []) >> + (* Use the validity hypothesis *) + fs [] >> pop_assum ignore_tac >> + (* For ‘fix f y = fix_fuel n f y’: use the monotonicity property *) + sg ‘fix_fuel_P f y n’ + >-(Cases_on ‘fix_fuel n f y’ >> fs [fix_fuel_P_def, is_diverge_def, bind_def]) >> + sg ‘fix f y = fix_fuel n f y’ >-(metis_tac [fix_fuel_eq_fix])>> + (* Case disjunction on the call to ‘f’ *) + Cases_on ‘fix_fuel n f y’ >> gvs [bind_def] >> + (* We have to prove that: ‘h (fix f) a = h (fix_fuel n f) a’: use the induction hypothesis *) + metis_tac [] +QED + +Theorem fix_fuel_not_diverge_eq_fix: + ∀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 +Proof + metis_tac [fix_fuel_not_diverge_eq_fix_aux] +QED + +Theorem fix_fixed_terminates: + ∀N f. is_valid_fp_body N f ⇒ ∀x n. fix_fuel_P f x n ⇒ fix f x = f (fix f) x +Proof + (* The proof simply uses the lemma [fix_fuel_not_diverge_eq_fix] *) + rw [fix_fuel_P_def, is_diverge_def, fix_def] >> case_tac >> fs [] >> + (* We can prove that ‘fix_fuel ($LEAST ...) f x ≠ Diverge’ *) + qspecl_assume [‘f’, ‘n’, ‘x’] fix_fuel_P_least >> + pop_assum sg_premise_tac >-(Cases_on ‘fix_fuel n f x’ >> fs []) >> + fs [fix_fuel_P_def, is_diverge_def] >> + (* *) + Cases_on ‘($LEAST (fix_fuel_P f x))’ >> fs [fix_fuel_def] >> + irule (GSYM fix_fuel_not_diverge_eq_fix) >> + Cases_on ‘f (fix_fuel n'' f) x’ >> fs [] >> metis_tac [] +QED + +(* +Type ft = ``: 'a -> ('a result + (num # num # 'a))`` + +val fix_fuel_def = Define ‘ + (fix_fuel (0 : num) (fs : ('a ft) list) + (i : num) (x : 'a) : 'a result = Diverge) ∧ + + (fix_fuel (SUC n) fs i x = + case EL i fs x of + | INL r => r + | INR (j, k, y) => + case fix_fuel n fs j y of + | Fail e => Fail e + | Diverge => Diverge + | Return z => + fix_fuel n fs k z) +’ + +val fix_fuel_P_def = Define ‘ + fix_fuel_P fs i x n = ~(is_diverge (fix_fuel n fs i x)) +’ + +val fix_def = Define ‘ + fix (fs : ('a ft) list) (i : num) (x : 'a) : 'a result = + if (∃ n. fix_fuel_P fs i x n) + then fix_fuel ($LEAST (fix_fuel_P fs i x)) fs i x + else Diverge +’ + +Theorem fix_fuel_mono: + ∀f. is_valid_fp_body f ⇒ + ∀n x. fix_fuel_P f x n ⇒ + ∀ m. n ≤ m ⇒ + fix_fuel n f x = fix_fuel m f x +Proof + ntac 2 strip_tac >> + Induct_on ‘n’ >> rpt strip_tac + >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >> + Cases_on ‘m’ >- int_tac >> fs [] >> + fs [is_valid_fp_body_def] >> + fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >> + + (*(* Use the validity property *) + last_assum (qspec_assume ‘x’) >> (* TODO: consume? *) *) + + (*pop_assum ignore_tac >> (* TODO: not sure *) *) + Induct_on ‘N’ >- fs [eval_ftree_def] >> + rw [] >> + rw [eval_ftree_def] >> + Cases_on ‘h x’ >> fs [] >> + Cases_on ‘y’ >> fs [] >> + Cases_on ‘y'’ >> fs [] >> + + last_assum (qspec_assume ‘q’) >> + Cases_on ‘fix_fuel n f q’ >> fs [] >> + + Cases_on ‘N’ >> fs [eval_ftree_def] >> + + Cases_on ‘y’ >> fs [] >> + Cases_on ‘y'’ >> fs [] >> + rw [] >> + (* This makes a case disjunction on the validity property *) + rw [] + >-((* Case 1: the continuation doesn't matter *) fs []) >> + (* Case 2: the continuation *does* matter (i.e., there is a recursive call *) + (* Instantiate the validity property with the different continuations *) + first_assum (qspec_assume ‘fix_fuel n f’) >> + first_assum (qspec_assume ‘fix_fuel n' f’) >> + last_assum (qspec_assume ‘y’) >> + fs [] +QED + + + +Type ft = ``: ('a -> 'a result) -> 'a -> ('a result + (num # 'a))`` + +val fix_fuel_def = Define ‘ + (fix_fuel (0 : num) (fs : ('a ft) list) (g : 'a -> 'a result) + (i : num) (x : 'a) : 'a result = Diverge) ∧ + + (fix_fuel (SUC n) fs g i x = + case EL i fs g x of + | INL r => r + | INR (j, y) => + case g y of + | Fail e => Fail e + | Diverge => Diverge + | Return z => fix_fuel n fs g j z) +’ + +val fix_fuel_def = Define ‘ + (fix_fuel (0 : num) (fs : ('a ft) list) g (i : num) (x : 'a) : 'a result = Diverge) ∧ + + (fix_fuel (SUC n) fs g i x = + case EL i fs x of + | INL r => r + | INR (j, y) => + case g y of + | Fail e => Fail e + | Diverge => Diverge + | Return z => fix_fuel n fs g j z) +’ + +val fix_fuel_def = Define ‘ + (fix_fuel (0 : num) (f : ('a -> 'a result) -> 'a -> 'a result) (x : 'a) : 'a result = Diverge) ∧ + (fix_fuel (SUC n) (f : ('a -> 'a result) -> 'a -> 'a result) (x : 'a) : 'a result = f (fix_fuel n f) x) +’ + +val fix_fuel_P_def = Define ‘ + fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x)) +’ + +val fix_def = Define ‘ + fix (f : ('a -> 'a result) -> 'a -> 'a result) (x : 'a) : 'a result = + if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge +’ + +(*Datatype: + ftree = Rec (('a -> ('a result + ('a # num))) # ftree list) | NRec ('a -> 'a result) +End + +Type frtree = ``: ('b -> ('b result + ('a # num))) list`` +Type ftree = “: ('a, 'b) frtree # ('b result + ('a # num))” +*) + +val eval_ftree_def = Define ‘ + (eval_ftree 0 (g : 'a -> 'a result) + (fs : ('a -> ('a result + ('a # num))) list) x = Diverge) ∧ + + (eval_ftree (SUC n) g fs x = + case x of + | INL r => r + | INR (y, i) => + case g y of + | Fail e => Fail e + | Diverge => Diverge + | Return z => + let f = EL i fs in + eval_ftree n g fs (f z)) +’ + +Theorem fix_fuel_mono: + ∀N fs i. + let f = (\g x. eval_ftree N g fs (INR (x, i))) in + ∀n x. fix_fuel_P f x n ⇒ + ∀ m. n ≤ m ⇒ fix_fuel n f x = fix_fuel m f x +Proof + Induct_on ‘N’ + >-( + fs [eval_ftree_def] >> + + ntac 2 strip_tac >> + Induct_on ‘n’ >> rpt strip_tac + >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >> + Cases_on ‘m’ >- int_tac >> fs [] >> + fs [is_valid_fp_body_def] >> + fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >> + + +val is_valid_fp_body_def = Define ‘ + is_valid_fp_body (f : ('a -> 'b result) -> 'a -> 'b result) = + (∃N ft. ∀x g. f g x = eval_ftree N g ft (x, i)) +’ + +val eval_ftree_def = Define ‘ + (eval_ftree 0 (g : 'a -> 'b result) + (fs : ('b -> ('b result + ('a # num))) list, x : 'b result + ('a # num)) = Diverge) ∧ + + (eval_ftree (SUC n) g (fs, x) = + case x of + | INL r => r + | INR (y, i) => + case g y of + | Fail e => Fail e + | Diverge => Diverge + | Return z => + let f = EL i fs in + eval_ftree n g (fs, f z)) +’ + +val is_valid_fp_body_def = Define ‘ + is_valid_fp_body (f : ('a -> 'b result) -> 'a -> 'b result) = + (∃N ft h. ∀x g. f g x = eval_ftree N g (ft, h x)) +’ + +Theorem fix_fuel_mono: + let f = (\x. eval_ftree N g (ft, h x)) in + ∀n x. fix_fuel_P f x n ⇒ + ∀ m. n ≤ m ⇒ fix_fuel n f x = fix_fuel m f x +Proof + + +Theorem fix_fuel_mono: + ∀f. is_valid_fp_body f ⇒ + ∀n x. fix_fuel_P f x n ⇒ + ∀ m. n ≤ m ⇒ + fix_fuel n f x = fix_fuel m f x +Proof + ntac 2 strip_tac >> + Induct_on ‘n’ >> rpt strip_tac + >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >> + Cases_on ‘m’ >- int_tac >> fs [] >> + fs [is_valid_fp_body_def] >> + fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >> + + (*(* Use the validity property *) + last_assum (qspec_assume ‘x’) >> (* TODO: consume? *) *) + + (*pop_assum ignore_tac >> (* TODO: not sure *) *) + Induct_on ‘N’ >- fs [eval_ftree_def] >> + rw [] >> + rw [eval_ftree_def] >> + Cases_on ‘h x’ >> fs [] >> + Cases_on ‘y’ >> fs [] >> + Cases_on ‘y'’ >> fs [] >> + + last_assum (qspec_assume ‘q’) >> + Cases_on ‘fix_fuel n f q’ >> fs [] >> + + Cases_on ‘N’ >> fs [eval_ftree_def] >> + + Cases_on ‘y’ >> fs [] >> + Cases_on ‘y'’ >> fs [] >> + rw [] >> + (* This makes a case disjunction on the validity property *) + rw [] + >-((* Case 1: the continuation doesn't matter *) fs []) >> + (* Case 2: the continuation *does* matter (i.e., there is a recursive call *) + (* Instantiate the validity property with the different continuations *) + first_assum (qspec_assume ‘fix_fuel n f’) >> + first_assum (qspec_assume ‘fix_fuel n' f’) >> + last_assum (qspec_assume ‘y’) >> + fs [] +QED + + +val length_ftree = “ +( + [ + (\n. INL (return (1 + n))) + ], + (case ls of + | ListCons x tl => + INR (tl, 0) + | ListNil => INL (return 0)) +) : ('a list_t, int) ftree +” + +val eval_length_ftree = mk_icomb (“eval_ftree 1 g”, length_ftree) + +Theorem length_body_eq: + eval_ftree (SUC (SUC 0)) g + ( + [ + (\n. INL (Return (1 + n))) + ], + (case ls of + | ListCons x tl => + INR (tl, 0) + | ListNil => INL (Return 0)) + ) = + case ls of + | ListCons x tl => + do + n <- g tl; + Return (1 + n) + od + | ListNil => Return 0 +Proof + fs [eval_ftree_def, bind_def] >> + Cases_on ‘ls’ >> fs [] +QED + +val eval_ftree_def = Define ‘ + eval_ftree 0 (fs : ('a, 'b) ftree) (g : 'a -> 'b result) (x : 'b result + ('a # num)) = Diverge ∧ + + eval_ftree (SUC n) fs g x = + case x of + | INL r => r + | INR (y, i) => + case g y of + | Fail e => Fail e + | Diverge => Diverge + | Return z => + let f = EL i fs in + eval_ftree n fs g (f z) +’ + +val length_body_funs_def = Define + +“ +[ + (\ls. case ls of + | ListCons x tl => + INR (tl, 1) + | ListNil => INL (return 0)), + (\n. INL (return (1 + n))) +] +” + + + +“:('a, 'b) FT” + +Define + +val nth_body = Define ‘ + + +’ + +“INL” +“INR” + +“ + Rec ( + case ls of + | ListCons x tl => + do + INR (tl, 0) + od + | ListNil => INL (return 0), + [NRec (\n. return (1 + n))]) +” + +“ + case ls of + | ListCons x tl => + if u32_to_int i = (0:int) + then (Return x) + else + do + i0 <- u32_sub i (int_to_u32 1); + y <- nth tl i0; + return y + od + | ListNil => Fail Failure +” + + +“:'a + 'b” +“:'a # 'b” + +(*** Encoding of a function *) +Datatype: + ('a, 'b) test = Return ('a -> 'b) +End + +val tyax = + new_type_definition ("three", + Q.prove(`?p. (\(x,y). ~(x /\ y)) p`, cheat)) + +val three_bij = define_new_type_bijections + {name="three_tybij", ABS="abs3", REP="rep3", tyax=tyax} +type_of “rep3” +type_of “abs3” + +m “” + + Q.EXISTS_TAC `(F,F)` THEN GEN_BETA_TAC THEN REWRITE_TAC [])); + +“Return (\x. x)” + +Datatype: + ftree = Rec ('a -> ('a result + ('a # ftree))) | NRec ('a -> 'a result) +End + +Datatype: + 'a ftree = Rec ('a -> ('a result + ('a # ftree))) | NRec ('a -> 'a result) +End + +Datatype: + ftree = Rec ('a -> ('a result + ('a # ftree))) | NRec ('a -> 'a result) +End + +Datatype: + result = Return 'a | Fail error | Diverge +End + +Type M = ``: 'a result`` + + +val fix_def = Define ‘ + fix (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = + if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge +’ + +val _ = export_theory () diff --git a/backends/hol4/divDefProto2Theory.sig b/backends/hol4/divDefProto2Theory.sig new file mode 100644 index 00000000..349aabf7 --- /dev/null +++ b/backends/hol4/divDefProto2Theory.sig @@ -0,0 +1,225 @@ +signature divDefProto2Theory = +sig + type thm = Thm.thm + + (* Definitions *) + 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 + + (* Theorems *) + val datatype_ftree : thm + val eval_ftree_compute : thm + val eval_ftree_def : thm + val eval_ftree_ind : 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 divDefProto2_grammars : type_grammar.grammar * term_grammar.grammar +(* + [primitives] Parent theory of "divDefProto2" + + [fix_def] Definition + + ⊢ ∀f x. + fix f x = + if ∃n. fix_fuel_P f x n then + fix_fuel ($LEAST (fix_fuel_P f x)) f x + else Diverge + + [fix_fuel_P_def] Definition + + ⊢ ∀f x n. fix_fuel_P f x n ⇔ ¬is_diverge (fix_fuel n f x) + + [fix_fuel_def] Definition + + ⊢ (∀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 + + ⊢ ∃rep. + TYPE_DEFINITION + (λa0'. + ∀ $var$('ftree') $var$('@temp @ind_typedivDefProto20prod') + $var$('@temp @ind_typedivDefProto21list'). + (∀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 a1. + ind_type$CONSTR (SUC (SUC 0)) (ARB,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 + + [ftree_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 + + [ftree_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) + + [is_valid_fp_body_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) = + 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) = + 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) + + [fix_fuel_compute] Theorem + + ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧ + (∀n f x. + fix_fuel (NUMERAL (BIT1 n)) f x = + f (fix_fuel (NUMERAL (BIT1 n) − 1) f) x) ∧ + ∀n f x. + fix_fuel (NUMERAL (BIT2 n)) f x = + f (fix_fuel (NUMERAL (BIT1 n)) f) x + + [ftree_11] Theorem + + ⊢ (∀a a'. Rec a = Rec a' ⇔ a = a') ∧ ∀a a'. NRec a = NRec a' ⇔ a = a' + + [ftree_Axiom] 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) + + [ftree_case_cong] 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' + + [ftree_case_eq] Theorem + + ⊢ ftree_CASE x f f1 = v ⇔ + (∃p. x = Rec p ∧ f p = v) ∨ ∃f'. x = NRec f' ∧ f1 f' = v + + [ftree_distinct] Theorem + + ⊢ ∀a' a. Rec a ≠ NRec a' + + [ftree_induction] 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 + + [ftree_nchotomy] Theorem + + ⊢ ∀ff. (∃p. ff = Rec p) ∨ ∃f. ff = NRec f + + [ftree_size_eq] Theorem + + ⊢ ftree1_size f = pair_size (λv. 0) (list_size (ftree_size f)) ∧ + ftree2_size f = list_size (ftree_size f) + + +*) +end diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml index 2682e507..b7b44b25 100644 --- a/backends/hol4/primitivesArithScript.sml +++ b/backends/hol4/primitivesArithScript.sml @@ -18,6 +18,7 @@ val le_eq_ge = store_thm("le_eq_ge", “!(x y : int). x <= y <=> y >= x”, coop val gt_eq_lt = store_thm("gt_eq_lt", “!(x y : int). x > y <=> y < x”, cooper_tac) val lt_eq_gt = store_thm("lt_eq_gt", “!(x y : int). x < y <=> y > x”, cooper_tac) +(* Miscelleanous *) Theorem int_add_minus_same_eq: ∀ (i j : int). i + j - j = i Proof |