Fixes of examples/lambda work due to one renamed theorem in rich_list…

…Theory
HOL-Theorem-Prover · Apr 21, 2024 · 4630435 · 4630435
1 parent d9c4303
commit 4630435
Show file tree

Hide file tree

Showing 5 changed files with 23 additions and 16 deletions.
diff --git a/examples/lambda/barendregt/boehmScript.sml b/examples/lambda/barendregt/boehmScript.sml
@@ -2762,7 +2762,7 @@ Proof
  >> ‘LENGTH as = d - m’ by rw [Abbr ‘as’, LENGTH_FRONT]
  >> qabbrev_tac ‘b = LAST l’
  >> Know ‘l = SNOC b as’
- >- (ASM_SIMP_TAC std_ss [Abbr ‘as’, Abbr ‘b’, SNOC_LAST_FRONT])
+ >- (ASM_SIMP_TAC std_ss [Abbr ‘as’, Abbr ‘b’, SNOC_OF_LAST_FRONT])
  >> DISCH_TAC
  >> qabbrev_tac ‘p3 = MAP rightctxt (REVERSE (MAP VAR l))’
  >> ‘Boehm_transform p3’ by rw [Abbr ‘p3’, MAP_MAP_o, GSYM MAP_REVERSE]
@@ -3342,7 +3342,7 @@ Proof
      Know ‘LAMl Z (VAR z) = LAMl (FRONT Z) (LAM z (VAR z))’
      >- (REWRITE_TAC [GSYM LAMl_SNOC] \\
          Suff ‘SNOC z (FRONT Z) = Z’ >- Rewr \\
-         qunabbrev_tac ‘z’ >> MATCH_MP_TAC SNOC_LAST_FRONT >> art []) >> Rewr' \\
+         qunabbrev_tac ‘z’ >> MATCH_MP_TAC SNOC_OF_LAST_FRONT >> art []) >> Rewr' \\
      REWRITE_TAC [appstar_APPEND] \\
      qabbrev_tac ‘t :term = LAM z (VAR z)’ \\
      MATCH_MP_TAC lameq_TRANS >> Q.EXISTS_TAC ‘t @* MAP VAR vs’ \\
@@ -3369,7 +3369,7 @@ Proof
      Know ‘LAMl Z (VAR z) = LAMl (FRONT Z) (LAM z (VAR z))’
      >- (REWRITE_TAC [GSYM LAMl_SNOC] \\
          Suff ‘SNOC z (FRONT Z) = Z’ >- Rewr \\
-         qunabbrev_tac ‘z’ >> MATCH_MP_TAC SNOC_LAST_FRONT >> art []) >> Rewr' \\
+         qunabbrev_tac ‘z’ >> MATCH_MP_TAC SNOC_OF_LAST_FRONT >> art []) >> Rewr' \\
      Know ‘args2' ++ MAP VAR vs = SNOC (VAR b0) (args2' ++ MAP VAR (FRONT vs))’
      >- (qunabbrev_tac ‘b0’ \\
          Know ‘VAR (LAST bs) :term = LAST (MAP VAR vs)’
@@ -3379,7 +3379,7 @@ Proof
              MATCH_MP_TAC (GSYM FRONT_APPEND_NOT_NIL) >> rw []) >> Rewr' \\
          Suff ‘LAST (MAP VAR vs) = LAST (args2' ++ MAP VAR vs)’
          >- (Rewr' >> qabbrev_tac ‘l = args2' ++ MAP VAR vs’ \\
-             MATCH_MP_TAC (GSYM SNOC_LAST_FRONT) >> rw [Abbr ‘l’]) \\
+             MATCH_MP_TAC SNOC_LAST_FRONT >> rw [Abbr ‘l’]) \\
          MATCH_MP_TAC (GSYM LAST_APPEND_NOT_NIL) >> rw []) >> Rewr' \\
      REWRITE_TAC [appstar_SNOC] \\
      qabbrev_tac ‘t :term = LAM z (VAR z)’ \\

diff --git a/examples/lambda/barendregt/chap2Script.sml b/examples/lambda/barendregt/chap2Script.sml
@@ -1225,7 +1225,7 @@ Proof
  >- (MATCH_MP_TAC LAMl_ALPHA_ssub >> rw [DISJOINT_SYM] \\
      Suff ‘FV M = set Z’ >- METIS_TAC [DISJOINT_SYM] \\
      rw [Abbr ‘M’, FV_appstar] \\
-    ‘Z = SNOC (LAST Z) (FRONT Z)’ by PROVE_TAC [SNOC_LAST_FRONT] \\
+    ‘Z = SNOC (LAST Z) (FRONT Z)’ by PROVE_TAC [SNOC_OF_LAST_FRONT] \\
      POP_ORW \\
      simp [LIST_TO_SET_SNOC] \\
      rw [Once EXTENSION, MEM_MAP] \\
@@ -1241,7 +1241,7 @@ Proof
  >> qabbrev_tac ‘y = LAST Y’
  (* postfix for LAMl_ALPHA_ssub *)
  >> ‘!t. LAMl Y t = LAMl (SNOC y (FRONT Y)) t’
-       by (ASM_SIMP_TAC std_ss [Abbr ‘y’, SNOC_LAST_FRONT]) >> POP_ORW
+       by (ASM_SIMP_TAC std_ss [Abbr ‘y’, SNOC_OF_LAST_FRONT]) >> POP_ORW
  >> REWRITE_TAC [LAMl_SNOC]
  >> Know ‘fm ' M = VAR y @* MAP VAR (FRONT Y)’
  >- (simp [Abbr ‘M’, ssub_appstar] \\

diff --git a/examples/lambda/barendregt/chap3Script.sml b/examples/lambda/barendregt/chap3Script.sml
@@ -1164,6 +1164,13 @@ val beta_eta_lameta = store_thm(
     ]
   ]);
 
+(* |- !M N.
+        lameta M N ==> ?Z. reduction (beta RUNION eta) M Z /\
+                           reduction (beta RUNION eta) N Z
+ *)
+Theorem lameta_CR = REWRITE_RULE [beta_eta_lameta, beta_eta_CR]
+                                 (Q.SPEC ‘beta RUNION eta’ theorem3_13)
+
 val beta_eta_normal_form_benf = store_thm(
   "beta_eta_normal_form_benf",
   ``normal_form (beta RUNION eta) = benf``,

diff --git a/examples/lambda/barendregt/head_reductionScript.sml b/examples/lambda/barendregt/head_reductionScript.sml
@@ -1654,7 +1654,7 @@ Theorem lameq_hnf_fresh_subst :
 Proof
     Induct_on ‘as’ using SNOC_INDUCT >> rw []
  >> Cases_on ‘args = []’ >- fs []
- >> ‘args = SNOC (LAST args) (FRONT args)’ by PROVE_TAC [SNOC_LAST_FRONT]
+ >> ‘args = SNOC (LAST args) (FRONT args)’ by PROVE_TAC [SNOC_OF_LAST_FRONT]
  >> POP_ORW
  >> REWRITE_TAC [appstar_SNOC, SUB_THM]
  >> MATCH_MP_TAC lameq_TRANS
@@ -1951,7 +1951,7 @@ Proof
  >- (MATCH_MP_TAC LAMl_ALPHA_ssub >> rw [DISJOINT_SYM] \\
      Suff ‘FV M = set Z’ >- METIS_TAC [DISJOINT_SYM] \\
      rw [Abbr ‘M’, FV_appstar] \\
-    ‘Z = SNOC (LAST Z) (FRONT Z)’ by PROVE_TAC [SNOC_LAST_FRONT] \\
+    ‘Z = SNOC (LAST Z) (FRONT Z)’ by PROVE_TAC [SNOC_OF_LAST_FRONT] \\
      POP_ORW \\
      simp [LIST_TO_SET_SNOC] \\
      rw [Once EXTENSION, MEM_MAP] \\
@@ -1966,7 +1966,7 @@ Proof
  >> ‘FDOM fm = set Z’ by rw [FDOM_fromPairs, Abbr ‘fm’]
  >> qabbrev_tac ‘y = LAST Y’
  >> ‘!t. LAMl Y t = LAMl (SNOC y (FRONT Y)) t’
-       by (ASM_SIMP_TAC std_ss [Abbr ‘y’, SNOC_LAST_FRONT]) >> POP_ORW
+       by (ASM_SIMP_TAC std_ss [Abbr ‘y’, SNOC_OF_LAST_FRONT]) >> POP_ORW
  >> REWRITE_TAC [LAMl_SNOC]
  >> Know ‘fm ' M = VAR y @* MAP VAR (FRONT Y)’
  >- (simp [Abbr ‘M’, ssub_appstar] \\
@@ -2066,7 +2066,7 @@ Proof
      Q.PAT_X_ASSUM ‘ALL_DISTINCT Y’ MP_TAC \\
      Know ‘SNOC y vs = Y’
      >- (qunabbrevl_tac [‘y’, ‘vs’] \\
-         MATCH_MP_TAC SNOC_LAST_FRONT >> art []) \\
+         MATCH_MP_TAC SNOC_OF_LAST_FRONT >> art []) \\
      DISCH_THEN (ONCE_REWRITE_TAC o wrap o SYM) \\
      rw [ALL_DISTINCT_SNOC]
      >- (qunabbrev_tac ‘vs1’ >> PROVE_TAC [MEM_TAKE]) \\
@@ -2094,7 +2094,7 @@ Proof
  >- (Q.PAT_X_ASSUM ‘ALL_DISTINCT Y’ MP_TAC \\
      Know ‘SNOC y vs = Y’
      >- (qunabbrevl_tac [‘y’, ‘vs’] \\
-         MATCH_MP_TAC SNOC_LAST_FRONT >> art []) \\
+         MATCH_MP_TAC SNOC_OF_LAST_FRONT >> art []) \\
      DISCH_THEN (ONCE_REWRITE_TAC o wrap o SYM) \\
      rw [ALL_DISTINCT_SNOC] \\
      qunabbrev_tac ‘vs1’ >> PROVE_TAC [MEM_TAKE])
@@ -2139,7 +2139,7 @@ Proof
      Q.PAT_X_ASSUM ‘ALL_DISTINCT Y’ MP_TAC \\
      Know ‘SNOC y vs = Y’
      >- (qunabbrevl_tac [‘y’, ‘vs’] \\
-         MATCH_MP_TAC SNOC_LAST_FRONT >> art []) \\
+         MATCH_MP_TAC SNOC_OF_LAST_FRONT >> art []) \\
      DISCH_THEN (ONCE_REWRITE_TAC o wrap o SYM) \\
      rw [ALL_DISTINCT_SNOC] \\
      CCONTR_TAC >> fs [Abbr ‘vs2’] \\

diff --git a/examples/lambda/barendregt/solvableScript.sml b/examples/lambda/barendregt/solvableScript.sml
@@ -1610,7 +1610,7 @@ Proof
  >- (MATCH_MP_TAC LAMl_ALPHA_ssub >> rw [DISJOINT_SYM] \\
      Suff ‘FV M = set Z’ >- METIS_TAC [DISJOINT_SYM] \\
      rw [Abbr ‘M’, FV_appstar] \\
-    ‘Z = SNOC (LAST Z) (FRONT Z)’ by PROVE_TAC [SNOC_LAST_FRONT] \\
+    ‘Z = SNOC (LAST Z) (FRONT Z)’ by PROVE_TAC [SNOC_OF_LAST_FRONT] \\
      POP_ORW \\
      simp [LIST_TO_SET_SNOC] \\
      rw [Once EXTENSION, MEM_MAP] \\
@@ -1626,7 +1626,7 @@ Proof
  >> qabbrev_tac ‘y = LAST Y’
  (* postfix for LAMl_ALPHA_ssub *)
  >> ‘!t. LAMl Y t = LAMl (SNOC y (FRONT Y)) t’
-       by (ASM_SIMP_TAC std_ss [Abbr ‘y’, SNOC_LAST_FRONT]) >> POP_ORW
+       by (ASM_SIMP_TAC std_ss [Abbr ‘y’, SNOC_OF_LAST_FRONT]) >> POP_ORW
  >> REWRITE_TAC [LAMl_SNOC]
  >> Know ‘fm ' M = VAR y @* MAP VAR (FRONT Y)’
  >- (simp [Abbr ‘M’, ssub_appstar] \\
@@ -1657,11 +1657,11 @@ Proof
  >> qabbrev_tac ‘vs = FRONT Y’
  >> Know ‘ALL_DISTINCT vs /\ ~MEM y vs’
  >- (Q.PAT_X_ASSUM ‘ALL_DISTINCT Y’ MP_TAC \\
-    ‘Y = SNOC y vs’ by METIS_TAC [SNOC_LAST_FRONT] >> POP_ORW \\
+    ‘Y = SNOC y vs’ by METIS_TAC [SNOC_OF_LAST_FRONT] >> POP_ORW \\
      rw [ALL_DISTINCT_SNOC])
  >> STRIP_TAC
  >> MATCH_MP_TAC principle_hnf_permutator_lemma
- >> ‘SNOC y vs = Y’ by METIS_TAC [SNOC_LAST_FRONT] >> POP_ORW
+ >> ‘SNOC y vs = Y’ by METIS_TAC [SNOC_OF_LAST_FRONT] >> POP_ORW
  >> rw [EVERY_MEM, Abbr ‘vs’, LENGTH_FRONT] >- art []
  >> FIRST_X_ASSUM MATCH_MP_TAC
  >> Q.EXISTS_TAC ‘e’ >> art []