[examples/lambda] Tweak some simultaneous substitution results

Modernise syntax in places, and with a BVC-compatible induction principle for ==, prove that M == N ==> !fm. fm ' M == fm ' N where fm is a finite map from variable names (strings) to terms.
HOL-Theorem-Prover · Oct 30, 2023 · b0fd7e4 · b0fd7e4 · binghe · Oct 31, 2023
1 parent 0ed59af
commit b0fd7e4
Show file tree

Hide file tree

Showing 2 changed files with 129 additions and 72 deletions.
diff --git a/examples/lambda/barendregt/chap2Script.sml b/examples/lambda/barendregt/chap2Script.sml
@@ -78,7 +78,9 @@ val one_hole_is_normal = store_thm(
   SIMP_TAC std_ss []);
 
 Inductive lameq :
+[~BETA:]
      (!x M N. (LAM x M) @@ N == [N/x]M) /\
+[~REFL:]
      (!M. M == M) /\
 [~SYM:]
      (!M N. M == N ==> N == M) /\
@@ -88,14 +90,59 @@ Inductive lameq :
      (!M N Z. M == N ==> M @@ Z == N @@ Z) /\
 [~APPR:]
      (!M N Z. M == N ==> Z @@ M == Z @@ N) /\
+[~ABS:]
      (!M N x. M == N ==> LAM x M == LAM x N)
 End
 
-Theorem lameq_refl[simp]: M:term == M
+Theorem lameq_refl[simp] = lameq_REFL
+
+Theorem lameq_tpm:
+  ∀M N. M == N ⇒ ∀π. tpm π M == tpm π N
 Proof
-  SRW_TAC [][lameq_rules]
+  Induct_on ‘M == N’ >> simp[tpm_thm, tpm_subst, lameq_BETA] >>
+  metis_tac[lameq_rules]
 QED
 
+Theorem lameq_ind_genX:
+  ∀P f.
+    (∀x:α. FINITE (f x)) ∧
+    (∀v M N x. v ∉ f x ⇒ P (LAM v M @@ N) ([N/v]M) x) ∧
+    (∀M x. P M M x) ∧
+    (∀M N x. N == M ∧ (∀y. P N M y) ⇒ P M N x) ∧
+    (∀L M N x. L == M ∧ M == N ∧ (∀w. P L M w) ∧ (∀y. P M N y) ⇒ P L N x) ∧
+    (∀M N Z x. M == N ∧ (∀y. P M N y) ⇒ P (M @@ Z) (N @@ Z) x) ∧
+    (∀M N Z x. M == N ∧ (∀y. P M N y) ⇒ P (Z @@ M) (Z @@ N) x) ∧
+    (∀v M N x. M == N ∧ v ∉ f x ∧ (∀y. P M N y) ⇒ P (LAM v M) (LAM v N) x) ⇒
+    ∀M N. M == N ⇒ ∀x. P M N x
+Proof
+  rpt gen_tac >> strip_tac >>
+  ‘∀M N. M == N ⇒ ∀π x. P (tpm π M) (tpm π N) x’
+    suffices_by metis_tac[pmact_nil] >>
+  Induct_on ‘M == N’ >> rw[tpm_subst] >~
+  [‘P (LAM (lswapstr π v) _) (LAM _ _) x’]
+  >- (Q_TAC (NEW_TAC "z") ‘FV (tpm π M) ∪ FV (tpm π N) ∪ f x’ >>
+      ‘LAM (lswapstr π v) (tpm π M) = LAM z (tpm [(z,lswapstr π v)] (tpm π M)) ∧
+       LAM (lswapstr π v) (tpm π N) = LAM z (tpm [(z,lswapstr π v)] (tpm π N))’
+        by simp[tpm_ALPHA] >>
+      simp[] >> first_x_assum irule >> simp[GSYM tpm_CONS, lameq_tpm]) >~
+  [‘P (LAM (lswapstr π v) (tpm π M) @@ tpm π N) _ x’]
+  >- (Q_TAC (NEW_TAC "z") ‘FV (tpm π M) ∪ FV (tpm π N) ∪ f x’ >>
+      ‘LAM (lswapstr π v) (tpm π M) = LAM z (tpm [(z,lswapstr π v)] (tpm π M))’
+        by simp[tpm_ALPHA] >>
+      simp[] >>
+      ‘[tpm π N/z] (tpm [(z,lswapstr π v)] (tpm π M)) =
+       [tpm π N/lswapstr π v] (tpm π M)’ suffices_by metis_tac[] >>
+      simp[fresh_tpm_subst, lemma15a]) >>
+  metis_tac[lameq_tpm]
+QED
+
+Theorem lameq_ind_X =
+        lameq_ind_genX |> INST_TYPE [alpha |-> “:unit”]
+                       |> Q.SPECL [‘λM N u. Q M N’, ‘K X’]
+                       |> SRULE[]
+                       |> Q.INST[‘Q’ |-> ‘P’]
+                       |> Q.GENL [‘P’, ‘X’]
+
 val lameq_app_cong = store_thm(
   "lameq_app_cong",
   ``M1 == M2 ==> N1 == N2 ==> M1 @@ N1 == M2 @@ N2``,
@@ -846,34 +893,42 @@ Proof
   SRW_TAC [][GSYM rator_subst_commutes, FV_SUB]
 QED
 
-val benf_def = Define`benf t <=> bnf t /\ enf t`;
-
+Definition benf_def:  benf t <=> bnf t /\ enf t
+End
 
-val has_bnf_def = Define`has_bnf t = ?t'. t == t' /\ bnf t'`;
+Definition has_bnf_def: has_bnf t = ?t'. t == t' /\ bnf t'
+End
 
+(* wrong? shouldn't this be ==_eta rather than == ? *)
 val has_benf_def = Define`has_benf t = ?t'. t == t' /\ benf t'`;
 
-(* FIXME: can ‘(!y. y IN FDOM fm ==> closed (fm ' y))’ be removed? *)
+Theorem fresh_ssub:
+  ∀N. y ∉ FV N ∧ (∀k:string. k ∈ FDOM fm ⇒ y # fm ' k) ⇒ y # fm ' N
+Proof
+  ho_match_mp_tac nc_INDUCTION2 >>
+  qexists ‘fmFV fm’ >>
+  rw[] >> metis_tac[]
+QED
+
+Theorem ssub_SUBST:
+  ∀M.
+    (∀k. k ∈ FDOM fm ⇒ v # fm ' k) ∧ v ∉ FDOM fm ⇒
+    fm ' ([N/v]M) = [fm ' N / v] (fm ' M)
+Proof
+  ho_match_mp_tac nc_INDUCTION2 >>
+  qexists ‘fmFV fm ∪ {v} ∪ FV N’ >>
+  rw[] >> rw[lemma14b, SUB_VAR] >>
+  gvs[DECIDE “~p ∨ q ⇔ p ⇒ q”, PULL_FORALL] >>
+  ‘y # fm ' N’ suffices_by simp[SUB_THM] >>
+  irule fresh_ssub >> simp[]
+QED
+
 Theorem lameq_ssub_cong :
-    !fm. (!y. y IN FDOM fm ==> closed (fm ' y)) /\
-          M == N ==> fm ' M == fm ' N
-Proof
-    HO_MATCH_MP_TAC fmap_INDUCT
- >> rw [FAPPLY_FUPDATE_THM]
- >> Know ‘!y. y IN FDOM fm ==> closed (fm ' y)’
- >- (Q.X_GEN_TAC ‘z’ >> DISCH_TAC \\
-    ‘z <> x’ by PROVE_TAC [] \\
-     Q.PAT_X_ASSUM ‘!y. y = x \/ y IN FDOM fm ==> P’ (MP_TAC o (Q.SPEC ‘z’)) \\
-     RW_TAC std_ss [])
- >> DISCH_TAC
- >> ‘fm ' M == fm ' N’ by PROVE_TAC []
- >> Know ‘(fm |+ (x,y)) ' M = [y/x] (fm ' M)’
- >- (MATCH_MP_TAC ssub_update_apply >> art [])
- >> Rewr'
- >> Know ‘(fm |+ (x,y)) ' N = [y/x] (fm ' N)’
- >- (MATCH_MP_TAC ssub_update_apply >> art [])
- >> Rewr'
- >> ASM_SIMP_TAC (betafy (srw_ss())) []
+  !M N. M == N ==> ∀fm. fm ' M == fm ' N
+Proof
+  HO_MATCH_MP_TAC lameq_ind_genX >> qexists ‘fmFV’ >>
+  simp[PULL_EXISTS] >> rw[] >>
+  simp[ssub_SUBST, lameq_BETA] >> metis_tac[lameq_rules]
 QED
 
 Theorem lameq_appstar_cong :

diff --git a/examples/lambda/basics/termScript.sml b/examples/lambda/basics/termScript.sml
@@ -97,13 +97,11 @@ val supp_tpm = prove(
   match_mp_tac (GEN_ALL supp_unique_apart) >>
   srw_tac [][supptpm_support, supptpm_apart, FINITE_GFV])
 
-val _ = overload_on ("FV", ``supp ^t_pmact_t``)
+Overload FV = “supp ^t_pmact_t”
 
-val FINITE_FV = store_thm(
-  "FINITE_FV",
-  ``FINITE (FV t)``,
-  srw_tac [][supp_tpm, FINITE_GFV]);
-val _ = export_rewrites ["FINITE_FV"]
+Theorem FINITE_FV[simp]: FINITE (FV t)
+Proof srw_tac [][supp_tpm, FINITE_GFV]
+QED
 
 fun supp_clause {con_termP, con_def} = let
   val t = mk_comb(``supp ^t_pmact_t``, lhand (concl (SPEC_ALL con_def)))
@@ -777,18 +775,20 @@ QED
     Simultaneous substitution (using a finite map) - much more interesting
    ---------------------------------------------------------------------- *)
 
-val strterm_fmap_supp = store_thm(
-  "strterm_fmap_supp",
-  ``supp (fm_pmact string_pmact ^t_pmact_t) fmap =
-      FDOM fmap ∪
-      supp (set_pmact ^t_pmact_t) (FRANGE fmap)``,
-  SRW_TAC [][fmap_supp]);
+Overload fmFV = “supp (fm_pmact string_pmact ^t_pmact_t)”
+Overload tmsFV = “supp (set_pmact ^t_pmact_t)”
+Overload fmtpm = “fmpm string_pmact term_pmact”
+
+Theorem strterm_fmap_supp:
+  fmFV fmap = FDOM fmap ∪ tmsFV (FRANGE fmap)
+Proof SRW_TAC [][fmap_supp]
+QED
 
-val FINITE_strterm_fmap_supp = store_thm(
-  "FINITE_strterm_fmap_supp",
-  ``FINITE (supp (fm_pmact string_pmact ^t_pmact_t) fmap)``,
-  SRW_TAC [][strterm_fmap_supp, supp_setpm] THEN SRW_TAC [][]);
-val _ = export_rewrites ["FINITE_strterm_fmap_supp"]
+Theorem FINITE_strterm_fmap_supp[simp]:
+  FINITE (fmFV fmap)
+Proof
+  SRW_TAC [][strterm_fmap_supp, supp_setpm] THEN SRW_TAC [][]
+QED
 
 val lem1 = prove(
   ``∃a. ~(a ∈ supp (fm_pmact string_pmact ^t_pmact_t) fm)``,
@@ -814,20 +814,23 @@ val supp_EMPTY = prove(
   qexists_tac `{}` >> srw_tac [][support_def]);
 
 
-val lem2 = prove(
-  ``∀fm. FINITE (supp (set_pmact ^t_pmact_t) (FRANGE fm))``,
-  srw_tac [][supp_setpm] >> srw_tac [][]);
+Theorem lem2[local]: ∀fm. FINITE (tmsFV (FRANGE fm))
+Proof
+  srw_tac [][supp_setpm] >> srw_tac [][]
+QED
 
 val ordering = prove(
   ``(∃f. P f) <=> (∃f. P (combin$C f))``,
   srw_tac [][EQ_IMP_THM] >-
     (qexists_tac `λx y. f y x` >> srw_tac [ETA_ss][combinTheory.C_DEF]) >>
   metis_tac [])
 
-val notin_frange = prove(
-  ``v ∉ supp (set_pmact ^t_pmact_t) (FRANGE p) <=> ∀y. y ∈ FDOM p ==> v ∉ FV (p ' y)``,
+Theorem notin_frange:
+  v ∉ tmsFV (FRANGE p) <=> ∀y. y ∈ FDOM p ==> v ∉ FV (p ' y)
+Proof
   srw_tac [][supp_setpm, EQ_IMP_THM, finite_mapTheory.FRANGE_DEF] >>
-  metis_tac []);
+  metis_tac []
+QED
 
 val ssub_exists =
     parameter_tm_recursion
@@ -867,38 +870,37 @@ val single_ssub = store_thm(
   HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `s INSERT FV M` THEN
   SRW_TAC [][SUB_VAR, SUB_THM]);
 
-val in_fmap_supp = store_thm(
-  "in_fmap_supp",
-  ``x ∈ supp (fm_pmact string_pmact ^t_pmact_t) fm <=>
-      x ∈ FDOM fm ∨
-      ∃y. y ∈ FDOM fm ∧ x ∈ FV (fm ' y)``,
+Theorem in_fmap_supp:
+  x ∈ fmFV fm ⇔ x ∈ FDOM fm ∨ ∃y. y ∈ FDOM fm ∧ x ∈ FV (fm ' y)
+Proof
   SRW_TAC [][strterm_fmap_supp, nomsetTheory.supp_setpm] THEN
-  SRW_TAC [boolSimps.DNF_ss][finite_mapTheory.FRANGE_DEF] THEN METIS_TAC []);
-
-val not_in_fmap_supp = store_thm(
-  "not_in_fmap_supp",
-  ``x ∉ supp (fm_pmact string_pmact ^t_pmact_t) fm <=>
-      x ∉ FDOM fm ∧ ∀y. y ∈ FDOM fm ==> x ∉ FV (fm ' y)``,
-  METIS_TAC [in_fmap_supp]);
-val _ = export_rewrites ["not_in_fmap_supp"]
-
-val ssub_14b = store_thm(
-  "ssub_14b",
-  ``∀t. (FV t ∩ FDOM phi = EMPTY) ==> ((phi : string |-> term) ' t = t)``,
+  SRW_TAC [boolSimps.DNF_ss][finite_mapTheory.FRANGE_DEF] THEN METIS_TAC []
+QED
+
+Theorem not_in_fmap_supp[simp]:
+  x ∉ fmFV fm <=> x ∉ FDOM fm ∧ ∀y. y ∈ FDOM fm ==> x ∉ FV (fm ' y)
+Proof
+  METIS_TAC [in_fmap_supp]
+QED
+
+Theorem ssub_14b:
+  ∀t. (FV t ∩ FDOM phi = EMPTY) ==> ((phi : string |-> term) ' t = t)
+Proof
   HO_MATCH_MP_TAC nc_INDUCTION2 THEN
-  Q.EXISTS_TAC `supp (fm_pmact string_pmact ^t_pmact_t) phi` THEN
-  SRW_TAC [][SUB_THM, SUB_VAR, pred_setTheory.EXTENSION] THEN METIS_TAC []);
+  Q.EXISTS_TAC `fmFV phi` THEN
+  SRW_TAC [][SUB_THM, SUB_VAR, pred_setTheory.EXTENSION] THEN METIS_TAC []
+QED
 
 val ssub_value = store_thm(
   "ssub_value",
   ``(FV t = EMPTY) ==> ((phi : string |-> term) ' t = t)``,
   SRW_TAC [][ssub_14b]);
 
-val ssub_FEMPTY = store_thm(
-  "ssub_FEMPTY",
-  ``∀t. (FEMPTY:string|->term) ' t = t``,
-  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]);
-val _ = export_rewrites ["ssub_FEMPTY"]
+Theorem ssub_FEMPTY[simp]:
+  ∀t. (FEMPTY:string|->term) ' t = t
+Proof
+  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]
+QED
 
 Theorem FV_ssub :
     !fm N. (!y. y IN FDOM fm ==> FV (fm ' y) = {}) ==>