From 5316e1e42f8f9196124a6b880fe61fe91bbff46a Mon Sep 17 00:00:00 2001 From: Chun Tian Date: Tue, 3 Oct 2023 22:41:51 +1100 Subject: [PATCH] Done has_hnf_LAM --- examples/lambda/barendregt/chap2Script.sml | 1 + examples/lambda/barendregt/chap3Script.sml | 20 ++++++++ examples/lambda/barendregt/solvableScript.sml | 27 +++++----- .../barendregt/standardisationScript.sml | 51 ++++++------------- 4 files changed, 48 insertions(+), 51 deletions(-) diff --git a/examples/lambda/barendregt/chap2Script.sml b/examples/lambda/barendregt/chap2Script.sml index 762021c2a0..5ac9dff6fa 100644 --- a/examples/lambda/barendregt/chap2Script.sml +++ b/examples/lambda/barendregt/chap2Script.sml @@ -106,6 +106,7 @@ val lameq_weaken_cong = store_thm( METIS_TAC [lameq_rules]); Theorem lameq_SYM = List.nth(CONJUNCTS lameq_rules, 2) +Theorem lameq_TRANS = List.nth(CONJUNCTS lameq_rules, 3) val fixed_point_thm = store_thm( (* p. 14 *) "fixed_point_thm", diff --git a/examples/lambda/barendregt/chap3Script.sml b/examples/lambda/barendregt/chap3Script.sml index f27acd8caf..9618d09aef 100644 --- a/examples/lambda/barendregt/chap3Script.sml +++ b/examples/lambda/barendregt/chap3Script.sml @@ -925,6 +925,26 @@ Proof >> MATCH_MP_TAC grandbeta_imp_betastar >> art [] QED +(* cf. abs_grandbeta, added by Chun Tian *) +Theorem abs_betastar : + !x M Z. LAM x M -b->* Z ==> ?N'. (Z = LAM x N') /\ M == N' +Proof + rpt GEN_TAC + >> REWRITE_TAC [SYM theorem3_17] + >> Q.ID_SPEC_TAC ‘Z’ + >> HO_MATCH_MP_TAC (Q.ISPEC ‘grandbeta’ TC_INDUCT_ALT_RIGHT) + >> rpt STRIP_TAC + >- (FULL_SIMP_TAC std_ss [abs_grandbeta] \\ + Q.EXISTS_TAC ‘N0’ >> art [] \\ + MATCH_MP_TAC grandbeta_imp_lameq >> art []) + >> Q.PAT_X_ASSUM ‘Z = LAM x N'’ (FULL_SIMP_TAC std_ss o wrap) + >> FULL_SIMP_TAC std_ss [abs_grandbeta] + >> Q.EXISTS_TAC ‘N0’ >> art [] + >> MATCH_MP_TAC lameq_TRANS + >> Q.EXISTS_TAC ‘N'’ >> art [] + >> MATCH_MP_TAC grandbeta_imp_lameq >> art [] +QED + val lameq_consistent = store_thm( "lameq_consistent", ``consistent $==``, diff --git a/examples/lambda/barendregt/solvableScript.sml b/examples/lambda/barendregt/solvableScript.sml index fda754d89b..22d4300260 100644 --- a/examples/lambda/barendregt/solvableScript.sml +++ b/examples/lambda/barendregt/solvableScript.sml @@ -105,9 +105,6 @@ Proof >> rw [lameq_K] QED -Theorem lameq_symm[local] = List.nth(CONJUNCTS lameq_rules, 2) -Theorem lameq_trans[local] = List.nth(CONJUNCTS lameq_rules, 3) - Theorem solvable_xIO : solvable (VAR x @@ I @@ Omega) Proof @@ -187,7 +184,7 @@ Proof MATCH_MP_TAC FV_ssub \\ rw [Abbr ‘fm’, FUN_FMAP_DEF, FAPPLY_FUPDATE_THM]) (* stage work *) - >> MATCH_MP_TAC lameq_trans + >> MATCH_MP_TAC lameq_TRANS >> Q.EXISTS_TAC ‘fm ' (M @* Ns)’ >> reverse CONJ_TAC >- (ONCE_REWRITE_TAC [SYM ssub_I] \\ @@ -244,7 +241,7 @@ Proof MATCH_MP_TAC LAMl_appstar >> rw []) >> DISCH_TAC >> ‘LAMl vs M @* Ns0 @* Ns1 == fm ' M @* Ns1’ by PROVE_TAC [lameq_appstar_cong] - >> ‘fm ' M @* Ns1 == I’ by PROVE_TAC [lameq_trans, lameq_symm] + >> ‘fm ' M @* Ns1 == I’ by PROVE_TAC [lameq_TRANS, lameq_SYM] >> qexistsl_tac [‘fm ' M’, ‘Ns1’] >> rw [closed_substitution_instances_def] >> Q.EXISTS_TAC ‘fm’ >> rw [Abbr ‘fm’] @@ -282,7 +279,7 @@ Proof FULL_SIMP_TAC std_ss [GSYM appstar_APPEND] \\ Q.ABBREV_TAC ‘Ns' = Ns ++ Is’ \\ ‘LENGTH Ns' = n’ by (rw [Abbr ‘Ns'’, Abbr ‘Is’]) \\ - ‘LAMl vs M @* Ns' == I’ by PROVE_TAC [lameq_trans] \\ + ‘LAMl vs M @* Ns' == I’ by PROVE_TAC [lameq_TRANS] \\ Know ‘EVERY closed Ns'’ >- (rw [EVERY_APPEND, Abbr ‘Ns'’] \\ rw [EVERY_MEM, Abbr ‘Is’, closed_def, MEM_GENLIST] \\ @@ -328,7 +325,7 @@ Proof >> Know ‘LAMl vs M @* Ps @* Ns == (FEMPTY |++ ZIP (vs,Ps)) ' M @* Ns’ >- (MATCH_MP_TAC lameq_appstar_cong >> art []) >> DISCH_TAC - >> ‘LAMl vs M @* Ps @* Ns == I’ by PROVE_TAC [lameq_trans] + >> ‘LAMl vs M @* Ps @* Ns == I’ by PROVE_TAC [lameq_TRANS] >> qexistsl_tac [‘LAMl vs M’, ‘Ps ++ Ns’] >> rw [appstar_APPEND, closures_def] >> Q.EXISTS_TAC ‘vs’ >> art [] @@ -370,7 +367,7 @@ Proof MATCH_MP_TAC LAMl_appstar >> rw []) >> DISCH_TAC >> ‘LAMl vs M @* Ns0 @* Ns1 == fm ' M @* Ns1’ by PROVE_TAC [lameq_appstar_cong] - >> ‘fm ' M @* Ns1 == I’ by PROVE_TAC [lameq_trans, lameq_symm] + >> ‘fm ' M @* Ns1 == I’ by PROVE_TAC [lameq_TRANS, lameq_SYM] (* Ns0' is the permuted version of Ns0 *) >> Q.ABBREV_TAC ‘Ns0' = GENLIST (\i. EL (f i) Ns0) n’ >> ‘LENGTH Ns0' = n’ by rw [Abbr ‘Ns0'’, LENGTH_GENLIST] @@ -393,9 +390,9 @@ Proof MATCH_MP_TAC LAMl_appstar >> rw []) >> DISCH_TAC >> ‘LAMl vs' M @* Ns0' @* Ns1 == fm' ' M @* Ns1’ by PROVE_TAC [lameq_appstar_cong] - >> MATCH_MP_TAC lameq_trans + >> MATCH_MP_TAC lameq_TRANS >> Q.EXISTS_TAC ‘fm' ' M @* Ns1’ >> art [] - >> MATCH_MP_TAC lameq_trans + >> MATCH_MP_TAC lameq_TRANS >> Q.EXISTS_TAC ‘fm ' M @* Ns1’ >> art [] >> Suff ‘fm = fm'’ >- rw [] (* cleanup uncessary assumptions *) @@ -477,7 +474,7 @@ Proof >> ‘LAMl vs M @* (Ns ++ Is) == I @* Is’ by rw [appstar_APPEND] >> Q.ABBREV_TAC ‘Ns' = Ns ++ Is’ >> ‘LENGTH Ns' = n’ by (rw [Abbr ‘Ns'’, Abbr ‘Is’]) - >> ‘LAMl vs M @* Ns' == I’ by PROVE_TAC [lameq_trans] + >> ‘LAMl vs M @* Ns' == I’ by PROVE_TAC [lameq_TRANS] >> Know ‘EVERY closed Ns'’ >- (rw [EVERY_APPEND, Abbr ‘Ns'’] \\ rw [EVERY_MEM, Abbr ‘Is’, closed_def, MEM_GENLIST] \\ @@ -510,7 +507,7 @@ Proof rw [Abbr ‘fm0’, Abbr ‘N’, DOMSUB_FAPPLY_THM, closed_def]) >> Rewr' \\ DISCH_TAC \\ Know ‘fm0 ' (LAM x M @@ N) @* Ns == I’ - >- (MATCH_MP_TAC lameq_trans \\ + >- (MATCH_MP_TAC lameq_TRANS \\ Q.EXISTS_TAC ‘fm0 ' ([N/x] M) @* Ns’ \\ POP_ASSUM (REWRITE_TAC o wrap) \\ MATCH_MP_TAC lameq_appstar_cong \\ @@ -526,7 +523,7 @@ Proof Q.EXISTS_TAC ‘fm0’ >> rw [Abbr ‘fm0’, DOMSUB_FAPPLY_THM], (* goal 1.2 (of 2) *) Know ‘fm ' (LAM x M @@ I) @* Ns == I’ - >- (MATCH_MP_TAC lameq_trans \\ + >- (MATCH_MP_TAC lameq_TRANS \\ Q.EXISTS_TAC ‘fm ' M @* Ns’ >> art [] \\ MATCH_MP_TAC lameq_appstar_cong \\ MATCH_MP_TAC lameq_ssub_cong >> art [] \\ @@ -562,7 +559,7 @@ Proof simp [appstar_APPEND] \\ DISCH_TAC \\ Know ‘[h/x] (fm ' M) @* t == I’ - >- (MATCH_MP_TAC lameq_trans \\ + >- (MATCH_MP_TAC lameq_TRANS \\ Q.EXISTS_TAC ‘LAM x (fm ' M) @@ h @* t’ >> art [] \\ MATCH_MP_TAC lameq_appstar_cong \\ rw [lameq_rules]) \\ @@ -597,7 +594,7 @@ Proof simp [appstar_APPEND] \\ DISCH_TAC \\ Know ‘[h/x] (fm ' M) @* t == I’ - >- (MATCH_MP_TAC lameq_trans \\ + >- (MATCH_MP_TAC lameq_TRANS \\ Q.EXISTS_TAC ‘LAM x (fm ' M) @@ h @* t’ >> art [] \\ MATCH_MP_TAC lameq_appstar_cong \\ rw [lameq_rules]) \\ diff --git a/examples/lambda/barendregt/standardisationScript.sml b/examples/lambda/barendregt/standardisationScript.sml index f76427b26e..908bd22238 100644 --- a/examples/lambda/barendregt/standardisationScript.sml +++ b/examples/lambda/barendregt/standardisationScript.sml @@ -2432,8 +2432,6 @@ Proof >> ASM_SIMP_TAC (betafy (srw_ss())) [] QED -Theorem lameq_trans[local] = List.nth(CONJUNCTS lameq_rules, 3) - Theorem LAMl_appstar : !vs M Ns. ALL_DISTINCT vs /\ (LENGTH vs = LENGTH Ns) /\ EVERY closed Ns ==> LAMl vs M @* Ns == (FEMPTY |++ ZIP (vs,Ns)) ' M @@ -2490,7 +2488,7 @@ Proof MATCH_MP_TAC LAMl_SUB \\ Q.PAT_X_ASSUM ‘closed N’ MP_TAC >> rw [closed_def]) >> DISCH_TAC - >> MATCH_MP_TAC lameq_trans + >> MATCH_MP_TAC lameq_TRANS >> Q.EXISTS_TAC ‘LAMl vs ([N/v] M) @* Ns’ >> art [] >> MATCH_MP_TAC lameq_appstar_cong >> art [] QED @@ -2525,42 +2523,23 @@ Proof >> qexistsl_tac [‘vs’, ‘args’, ‘y’] >> art [] QED -Theorem has_hnf_LAM_lemma1 : - !M x. has_hnf M ==> has_hnf (LAM x M) -Proof - RW_TAC std_ss [has_hnf_def] - >> Q.EXISTS_TAC ‘LAM x N’ - >> CONJ_TAC >- PROVE_TAC [lameq_rules] - >> ‘?vs args y. N = LAMl vs (VAR y @* args)’ by METIS_TAC [hnf_cases] - >> rw [hnf_cases] -QED - -(* cf. hnf_thm *) -Theorem has_hnf_LAM_lemma2 : - !M x. has_hnf (LAM x M) ==> has_hnf M -Proof - RW_TAC std_ss [has_hnf_def] - >> ‘?Z. LAM x M -b->* Z /\ N -b->* Z’ by METIS_TAC [lameq_CR] - >> Q.PAT_X_ASSUM ‘LAM x M -b->* Z’ - (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [RTC_CASES1])) - >- (POP_ASSUM (fs o wrap o SYM) \\ - ‘hnf (LAM x M)’ by PROVE_TAC [hnf_preserved] \\ - ‘hnf M’ by PROVE_TAC [hnf_thm] \\ - Q.EXISTS_TAC ‘M’ >> rw []) - >> ‘LAM x M =b=> u’ by PROVE_TAC [exercise3_3_1] - >> POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [abs_grandbeta])) - >> Q.PAT_X_ASSUM ‘u = LAM x N0’ (fs o wrap) - >> ‘hnf Z’ by PROVE_TAC [hnf_preserved] - >> cheat -QED - (* Proposition 8.3.13 (i) *) -Theorem has_hnf_LAM : +Theorem has_hnf_LAM[simp] : !M x. has_hnf M <=> has_hnf (LAM x M) Proof - rpt GEN_TAC - >> EQ_TAC - >> REWRITE_TAC [has_hnf_LAM_lemma1, has_hnf_LAM_lemma2] + RW_TAC std_ss [has_hnf_def] + >> EQ_TAC >> rpt STRIP_TAC + >- (Q.EXISTS_TAC ‘LAM x N’ \\ + CONJ_TAC >- PROVE_TAC [lameq_rules] \\ + ‘?vs args y. N = LAMl vs (VAR y @* args)’ by METIS_TAC [hnf_cases] \\ + rw [hnf_cases]) + (* stage work *) + >> ‘?Z. LAM x M -b->* Z /\ N -b->* Z’ by METIS_TAC [lameq_CR] + >> Suff ‘?N'. (Z = LAM x N') /\ M == N'’ + >- (STRIP_TAC \\ + ‘hnf Z’ by PROVE_TAC [hnf_preserved] \\ + Q.EXISTS_TAC ‘N'’ >> gs [hnf_thm]) + >> MATCH_MP_TAC abs_betastar >> art [] QED val _ = export_theory()