[examples/lambda] Move closure-related material to chap2; start chap4

examples/lambda/barendregt/chap2Script.sml

@@ -153,15 +153,17 @@ val lameq_weaken_cong = store_thm(
   ``(M1:term) == M2 ==> N1 == N2 ==> (M1 == N1 <=> M2 == N2)``,
   METIS_TAC [lameq_rules]);
 
-val fixed_point_thm = store_thm(  (* p. 14 *)
-  "fixed_point_thm",
-  ``!f. ?x. f @@ x == x``,
+Theorem fixed_point_thm:
+  !f. ?x. f @@ x == x ∧ FV x = FV f
+Proof
   GEN_TAC THEN Q_TAC (NEW_TAC "x") `FV f` THEN
   Q.ABBREV_TAC `w = (LAM x (f @@ (VAR x @@ VAR x)))` THEN
   Q.EXISTS_TAC `w @@ w` THEN
   `w @@ w == [w/x] (f @@ (VAR x @@ VAR x))` by PROVE_TAC [lameq_rules] THEN
   POP_ASSUM MP_TAC THEN
-  ASM_SIMP_TAC (srw_ss())[SUB_THM, lemma14b, lameq_rules]);
+  ASM_SIMP_TAC (srw_ss())[SUB_THM, lemma14b, lameq_rules] >>
+  rw[] >> ASM_SET_TAC[]
+QED
 
 (* properties of substitution - p19 *)
 
@@ -304,6 +306,7 @@ QED
    cf. Definition 4.1.1 [1, p.76]. If ‘eqns’ is a set of closed equations,
    then ‘{(M,N) | asmlam eqns M N}’ is the set of closed equations provable
    in lambda + eqns, denoted by ‘eqns^+’ in [1], or ‘asmlam eqns’ here.
+
  *)
 Inductive asmlam :
 [~eqn:]
@@ -1146,6 +1149,97 @@ QED
 
 val _ = remove_ovl_mapping "Y" {Thy = "chap2", Name = "Y"}
 
+(* ----------------------------------------------------------------------
+    closed terms and closures of (open or closed) terms, leading into
+    B's Chapter 2's section “Solvable and unsolvable terms” p41.
+
+    These definitions are stated again in Chapter 8 as per references
+    below.
+   ---------------------------------------------------------------------- *)
+
+(* By prefixing a list of abstractions of FVs, any term can be "closed". The
+   set ‘closures M’ represent such closures with different order of FVs.
+ *)
+Definition closures_def :
+    closures M = {LAMl vs M | vs | ALL_DISTINCT vs /\ set vs = FV M}
+End
+
+Theorem closures_not_empty :
+    !M. closures M <> {}
+Proof
+    Q.X_GEN_TAC ‘M’
+ >> rw [GSYM MEMBER_NOT_EMPTY]
+ >> Q.EXISTS_TAC ‘LAMl (SET_TO_LIST (FV M)) M’
+ >> rw [closures_def]
+ >> Q.EXISTS_TAC ‘SET_TO_LIST (FV M)’
+ >> rw [SET_TO_LIST_INV]
+QED
+
+Theorem closures_of_closed[simp] :
+    !M. closed M ==> closures M = {M}
+Proof
+    rw [closures_def, closed_def]
+ >> rw [Once EXTENSION]
+QED
+
+Theorem closures_of_open_sing :
+    !M v. FV M = {v} ==> closures M = {LAM v M}
+Proof
+    rw [closures_def, LIST_TO_SET_SING]
+ >> rw [Once EXTENSION]
+QED
+
+(* ‘closure M’ is just one arbitrary element in ‘closures M’. *)
+Overload closure = “\M. CHOICE (closures M)”
+
+Theorem closure_in_closures :
+    !M. closure M IN closures M
+Proof
+    rw [CHOICE_DEF, closures_not_empty]
+QED
+
+Theorem closure_idem[simp] :
+    !M. closed M ==> closure M = M
+Proof
+    rw [closures_of_closed]
+QED
+
+Theorem closure_open_sing :
+    !M v. FV M = {v} ==> closure M = LAM v M
+Proof
+    rpt STRIP_TAC
+ >> ‘closures M = {LAM v M}’ by PROVE_TAC [closures_of_open_sing]
+ >> rw []
+QED
+
+Theorem closed_closure[simp]:
+  closed (closure M)
+Proof
+  qspec_then ‘M’ assume_tac closure_in_closures >> gvs[closures_def] >>
+  simp[closed_def, appFOLDLTheory.FV_LAMl]
+QED
+
+(*---------------------------------------------------------------------------*
+ * solvable terms and some equivalent definitions
+ *---------------------------------------------------------------------------*)
+
+(* 8.3.1 (ii) [1, p.171] *)
+Definition solvable_def :
+    solvable (M :term) = ?M' Ns. M' IN closures M /\ M' @* Ns == I
+End
+
+(* 8.3.1 (i) [1, p.171] *)
+Theorem solvable_alt_closed :
+    !M. closed M ==> (solvable M <=> ?Ns. M @* Ns == I)
+Proof
+    rw [solvable_def, closed_def]
+QED
+
+(* 8.3.1 (iii) [1, p.171] *)
+Overload unsolvable = “\M. ~solvable M”
+
+
+
 val _ = export_theory()
 val _ = html_theory "chap2";
 

examples/lambda/barendregt/chap4Script.sml

@@ -0,0 +1,204 @@
+open HolKernel Parse boolLib bossLib;
+open binderLib
+
+open pred_setTheory
+open termTheory chap2Theory chap3Theory
+val _ = new_theory "chap4";
+
+val _ = hide "B"
+
+(* definition 4.1.1(i) is already in chap2, given name asmlam *)
+
+Definition lambdathy_def:
+  lambdathy A ⇔ consistent (asmlam A) ∧ UNCURRY (asmlam A) = A
+End
+
+Definition church1_def:
+  church1 = LAM "x" (LAM "y" (VAR "x" @@ VAR "y"))
+End
+
+Overload "𝟙" = “church1”
+
+
+Overload "TC" = “asmlam”
+
+Overload "eta_extend" = “λA. asmlam (UNCURRY eta ∪ A)”
+val _ = set_mapped_fixity {tok = UTF8.chr 0x1D73C, fixity = Suffix 2100,
+                           term_name = "eta_extend"}
+
+
+Theorem lameta_subset_eta_extend:
+  ∀M N. lameta M N ⇒ 𝒯 𝜼 M N
+Proof
+  Induct_on ‘lameta’ >>
+  rw[asmlam_refl, asmlam_beta, asmlam_lcong, asmlam_rcong, asmlam_abscong] >~
+  [‘_ 𝜼 M N’, ‘_ 𝜼 N M’] >- metis_tac[asmlam_sym] >~
+  [‘_ 𝜼 (LAM v (M @@ VAR v)) M’]
+  >- (irule asmlam_eqn >> simp[eta_def] >> metis_tac[]) >>
+  metis_tac[asmlam_trans]
+QED
+
+Theorem asmlam_equality:
+  asmlam A = asmlam B ⇔
+    (∀a1 a2. (a1,a2) ∈ A ⇒ asmlam B a1 a2) ∧
+    (∀b1 b2. (b1,b2) ∈ B ⇒ asmlam A b1 b2)
+Proof
+  iff_tac
+  >- (simp[] >> rw[] >~
+      [‘A⁺ = B⁺’, ‘(a1,a2) ∈ A’]
+      >- (‘A⁺ a1 a2’ suffices_by simp[] >> simp[asmlam_eqn]) >>
+      simp[asmlam_eqn]) >>
+  strip_tac >> simp[FUN_EQ_THM, EQ_IMP_THM, FORALL_AND_THM] >> conj_tac >>
+  Induct_on ‘asmlam’ >>
+  rw[asmlam_beta, asmlam_refl, asmlam_lcong, asmlam_rcong, asmlam_abscong] >>
+  metis_tac[asmlam_sym, asmlam_trans]
+QED
+
+Theorem eta_alt:
+  FINITE X ⇒ (η M N ⇔ ∃v. v ∉ X ∧ v # N ∧ M = LAM v (N @@ VAR v))
+Proof
+  simp[EQ_IMP_THM, eta_def] >> rw[]
+  >- (simp[LAM_eq_thm, SF DNF_ss, SF CONJ_ss, tpm_fresh] >>
+      Q_TAC (NEW_TAC "z") ‘{v} ∪ FV N ∪ X’ >> metis_tac[]) >>
+  simp[LAM_eq_thm, SF CONJ_ss, tpm_fresh, SF SFY_ss]
+QED
+
+Theorem lemma4_1_5:
+  ((I,𝟙) INSERT 𝒯)⁺ = 𝒯 𝜼
+Proof
+  simp[asmlam_equality] >> rw[]
+  >- (irule lameta_subset_eta_extend >>
+      simp[church1_def, I_def] >> irule lameta_SYM >>
+      irule lameta_ABS >> irule lameta_ETA >> simp[]) >>
+  simp[asmlam_eqn] >>
+  ‘FINITE {"x"; "y"}’ by simp[] >>
+  dxrule_then assume_tac eta_alt >> gvs[] >>
+  rename [‘_⁺ (LAM v (M @@ VAR v)) M’] >>
+  qmatch_abbrev_tac ‘A⁺ _ _’ >>
+  ‘A⁺ (LAM v (M @@ VAR v)) (𝟙 @@ M)’
+    by (‘A⁺ (𝟙 @@ M) ([M/"x"] (LAM "y" (VAR "x" @@ VAR "y")))’
+          by simp[asmlam_beta, church1_def] >>
+        Q_TAC (NEW_TAC "z") ‘FV M ∪ {"x"; "y"}’ >>
+        ‘LAM "y" (VAR "x" @@ VAR "y") = LAM z ([VAR z/"y"](VAR "x" @@ VAR "y"))’
+          by simp[SIMPLE_ALPHA] >>
+        gs[SUB_THM] >>
+        ‘LAM z (M @@ VAR z) = LAM v (M @@ VAR v)’
+          suffices_by metis_tac[asmlam_sym] >>
+        simp[LAM_eq_thm, SF CONJ_ss, tpm_fresh]) >>
+  ‘A⁺ (𝟙 @@ M) (I @@ M)’
+    by (irule asmlam_lcong  >> simp[Abbr‘A’] >>
+        metis_tac[asmlam_sym, asmlam_eqn, IN_INSERT]) >>
+  dxrule_all_then assume_tac asmlam_trans >>
+  ‘A⁺ (I @@ M) M’ suffices_by metis_tac[asmlam_trans] >>
+  simp[lameq_asmlam, lameq_I]
+QED
+
+(* Barendregt def'n 4.1.6(i) *)
+Definition K0_def:
+  K0 = { (M,N) | unsolvable M ∧ unsolvable N ∧ closed M ∧ closed N }
+End
+
+Overload "𝒦₀" = “K0”
+
+Definition Kthy_def:
+  Kthy = { (M,N) | asmlam K0 M N }
+End
+Overload "𝒦" = “Kthy”
+
+(* Barendregt def'n 4.1.7(ii) *)
+Definition sensible_def:
+  sensible 𝒯 ⇔ lambdathy 𝒯 ∧ 𝒦 ⊆ 𝒯
+End
+
+(* Barendregt def'n 4.1.7(iii) *)
+Definition semisensible_def:
+  semisensible 𝒯 ⇔ ∀M N. 𝒯⁺ M N ⇒ ¬(unsolvable M ∧ solvable N)
+End
+
+val Kfp_def =
+  new_specification ("Kfp_def", ["Kfp"], SPEC “K:term” fixed_point_thm);
+
+Overload "K∞" = “Kfp”
+
+Theorem FV_Kfp[simp]:
+  FV Kfp = {}
+Proof
+  simp[Kfp_def]
+QED
+
+Theorem Kfp_thm:
+  Kfp @@ x == Kfp
+Proof
+  strip_assume_tac Kfp_def >>
+  dxrule_then (qspec_then ‘x’ assume_tac) lameq_APPL >>
+  dxrule_then assume_tac lameq_SYM >> irule lameq_TRANS >>
+  first_x_assum $ irule_at Any >> simp[lameq_K]
+QED
+
+Theorem KfpI:
+  𝒯⁺ I Kfp ⇒ inconsistent 𝒯⁺
+Proof
+  strip_tac >> simp[inconsistent_def] >>
+  qx_genl_tac [‘M’, ‘N’] >>
+  qmatch_abbrev_tac ‘A M N’ >>
+  ‘∀P. A P Kfp’
+    suffices_by (strip_tac >> simp[Abbr‘A’] >>
+                 metis_tac[asmlam_trans, asmlam_sym]) >>
+  qx_gen_tac ‘P’ >>
+  ‘A P (I @@ P)’
+    by (simp[Abbr‘A’] >> metis_tac[asmlam_sym, lameq_asmlam, lameq_I]) >>
+  ‘A (I @@ P) (Kfp @@ P)’
+    by (simp[Abbr‘A’] >> metis_tac[asmlam_lcong, IN_INSERT, asmlam_eqn]) >>
+  ‘∀x y z. A x y ∧ A y z ⇒ A x z’ by metis_tac[asmlam_trans] >>
+  first_assum $ dxrule_all_then assume_tac >>
+  first_x_assum irule >> pop_assum $ irule_at Any >>
+  simp[Abbr‘A’, lameq_asmlam, Kfp_thm]
+QED
+
+Theorem asmlam_EMPTY:
+  asmlam {} = $==
+Proof
+  simp[FUN_EQ_THM, EQ_IMP_THM, lameq_asmlam] >>
+  Induct_on ‘asmlam’ >> metis_tac[lameq_rules, NOT_IN_EMPTY]
+QED
+
+Theorem Kfp_unsolvable[simp]:
+  unsolvable Kfp
+Proof
+  simp[solvable_alt_closed, closed_def] >>
+  Induct >> simp[]
+  >- (strip_tac >> gvs[GSYM asmlam_EMPTY] >>
+      dxrule_then assume_tac asmlam_sym >> drule KfpI >>
+      simp[asmlam_EMPTY, lameq_consistent]) >>
+  rpt strip_tac >>
+  resolve_then Any assume_tac Kfp_thm lameq_appstar_cong >>
+  metis_tac[lameq_SYM, lameq_TRANS]
+QED
+
+Theorem lemma4_1_8i:
+  I # Kfp
+Proof
+  simp[incompatible_def, KfpI, asmlam_eqn]
+QED
+
+(* argument seems to rely on solvable (LAM v t) ⇔ solvable t, which is proved
+   in chapter 8, suggesting all of this stuff should move to a mechanisation of
+   chapter 16
+Theorem corollary4_1_19:
+  sensible 𝒯 ⇒ semisensible 𝒯
+Proof
+  simp[sensible_def, semisensible_def] >> CCONTR_TAC >> gvs[] >>
+  rename [‘solvable M’, ‘unsolvable N’, ‘𝒯⁺ N M’] >>
+  wlog_tac ‘closed M ∧ closed N’ [‘M’,‘N’]
+  >- (gvs[]
+      >- (first_x_assum $ qspecl_then [‘closure M’, ‘closure N’] mp_tac >>
+          simp[]
+  qpat_x_assum ‘solvable M’ mp_tac >> simp[solvable_def] >>
+  qx_genl_tac [‘M'’, ‘Ps’] >> Cases_on ‘M' ·· Ps == I’ >> simp[] >>
+  simp[closures_def] >> qx_gen_tac ‘vs’ >> rpt strip_tac >>
+QED
+*)
+
+
+
+val _ = export_theory();