Done has_hnf_LAM

binghe · Oct 3, 2023 · 5316e1e · 5316e1e
1 parent 0934436
commit 5316e1e
Show file tree

Hide file tree

Showing 4 changed files with 48 additions and 51 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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()