Done unsolvable_Omega

examples/lambda/barendregt/chap3Script.sml

@@ -1,10 +1,10 @@
 open HolKernel Parse boolLib bossLib;
 
-open boolSimps metisLib basic_swapTheory relationTheory hurdUtils;
+open boolSimps metisLib basic_swapTheory relationTheory listTheory hurdUtils;
 
 local open pred_setLib in end;
 
-open binderLib BasicProvers nomsetTheory termTheory chap2Theory;
+open binderLib BasicProvers nomsetTheory termTheory chap2Theory appFOLDLTheory;
 
 val _ = new_theory "chap3";
 
@@ -858,12 +858,65 @@ val bnf_triangle = store_thm(
   ``M -b->* N /\ M -b->* N' /\ bnf N ==> N' -b->* N``,
   METIS_TAC [betaCR_square, bnf_reduction_to_self]);
 
-Theorem Omega_starloops[simp]: Omega -b->* N <=> N = Omega
+Theorem Omega_betaloops[simp] :
+    Omega -b-> N <=> N = Omega
 Proof
-  Q_TAC SUFF_TAC `!M N. M -b->* N ==> (M = Omega) ==> (N = Omega)`
-     THEN1 METIS_TAC [RTC_RULES] THEN
-  HO_MATCH_MP_TAC RTC_INDUCT THEN SRW_TAC [][] THEN
-  FULL_SIMP_TAC (srw_ss()) [ccbeta_rwt, Omega_def]
+    FULL_SIMP_TAC (srw_ss()) [ccbeta_rwt, Omega_def]
+QED
+
+Theorem Omega_starloops[simp] :
+    Omega -b->* N <=> N = Omega
+Proof
+    Suff ‘!M N. M -b->* N ==> (M = Omega) ==> (N = Omega)’
+ >- METIS_TAC [RTC_RULES]
+ >> HO_MATCH_MP_TAC RTC_INDUCT >> SRW_TAC [][]
+ >> FULL_SIMP_TAC std_ss [Omega_betaloops]
+QED
+
+Theorem Omega_app_betaloops[local] :
+    Omega @@ A -b-> N ==> ?A'. N = Omega @@ A'
+Proof
+    ‘~is_abs Omega’ by rw [Omega_def]
+ >> rw [ccbeta_rwt]
+ >- (Q.EXISTS_TAC ‘A’ >> rw [])
+ >> Q.EXISTS_TAC ‘N'’ >> rw []
+QED
+
+Theorem Omega_app_starloops :
+    Omega @@ A -b->* N ==> ?A'. N = Omega @@ A'
+Proof
+    Suff ‘!M N. M -b->* N ==> !A. M = Omega @@ A ==> ?A'. N = Omega @@ A'’
+ >- METIS_TAC [RTC_RULES]
+ >> HO_MATCH_MP_TAC RTC_INDUCT >> SRW_TAC [][]
+ >> ‘?A'. M' = Omega @@ A'’ by METIS_TAC [Omega_app_betaloops]
+ >> Q.PAT_X_ASSUM ‘!A. M' = Omega @@ A ==> P’ (MP_TAC o (Q.SPEC ‘A'’))
+ >> RW_TAC std_ss []
+QED
+
+Theorem Omega_appstar_betaloops[local] :
+    !N. Omega @* Ms -b-> N ==> ?Ms'. N = Omega @* Ms'
+Proof
+    Induct_on ‘Ms’ using SNOC_INDUCT
+ >- (rw [] >> Q.EXISTS_TAC ‘[]’ >> rw [])
+ >> rw [appstar_SNOC]
+ >> ‘~is_abs (Omega @* Ms)’ by rw [Omega_def]
+ >> fs [ccbeta_rwt]
+ >- (Q.PAT_X_ASSUM ‘!N. P’ (MP_TAC o (Q.SPEC ‘M'’)) \\
+     RW_TAC std_ss [] \\
+     Q.EXISTS_TAC ‘SNOC x Ms'’ >> rw [])
+ >> Q.EXISTS_TAC ‘SNOC N' Ms’ >> rw []
+QED
+
+Theorem Omega_appstar_starloops :
+    Omega @* Ms -b->* N ==> ?Ms'. N = Omega @* Ms'
+Proof
+    Suff ‘!M N. M -b->* N ==> !Ms. M = Omega @* Ms ==> ?Ms'. N = Omega @* Ms'’
+ >- METIS_TAC [RTC_RULES]
+ >> HO_MATCH_MP_TAC RTC_INDUCT >> SRW_TAC [][]
+ >- (Q.EXISTS_TAC ‘Ms’ >> rw [])
+ >> ‘?Ms'. M' = Omega @* Ms'’ by METIS_TAC [Omega_appstar_betaloops]
+ >> Q.PAT_X_ASSUM ‘!Ms. M' = Omega @* Ms ==> P’ (MP_TAC o (Q.SPEC ‘Ms'’))
+ >> RW_TAC std_ss []
 QED
 
 val lameq_betaconversion = store_thm(

examples/lambda/barendregt/solvableScript.sml

@@ -895,20 +895,21 @@ Proof
  >> MATCH_MP_TAC principle_hnf_LAMl_appstar_lemma >> rw []
 QED
 
-(* FIXME: how to leverage Omega_starloops and prove this theorem?
+(* Example 8.3.2 [1, p.171] *)
 Theorem unsolvable_Omega :
     unsolvable Omega
 Proof
    ‘closed Omega’ by rw [closed_def]
  >> rw [solvable_alt_closed]
- >> CCONTR_TAC
+ >> CCONTR_TAC >> fs []
  >> ‘?Z. Omega @* Ns -b->* Z /\ I -b->* Z’ by METIS_TAC [lameq_CR]
  >> fs [bnf_reduction_to_self]
  >> Q.PAT_X_ASSUM ‘closed Omega’ K_TAC
  >> POP_ASSUM K_TAC (* Z = I *)
- >> cheat
+ >> ‘?Ms. I = Omega @* Ms’ by METIS_TAC [Omega_appstar_starloops]
+ >> POP_ASSUM MP_TAC
+ >> rw [Omega_def, I_def]
 QED
- *)
 
 val _ = export_theory ();
 val _ = html_theory "solvable";