Principle head normal forms (principle_hnf)

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/head_reductionScript.sml

@@ -101,6 +101,14 @@ val hreduce1_unique = store_thm(
   HO_MATCH_MP_TAC hreduce1_ind THEN
   SIMP_TAC (srw_ss() ++ DNF_ss) [hreduce1_rwts]);
 
+Theorem hreduce1_rules_appstar :
+    !Ns. M1 -h-> M2 /\ ~is_abs M1 ==> M1 @* Ns -h-> M2 @* Ns
+Proof
+    Induct_on ‘Ns’ using SNOC_INDUCT
+ >> rw [appstar_SNOC]
+ >> fs [hreduce1_rules]
+QED
+
 Theorem hreduce1_gen_bvc_ind :
   !P f. (!x. FINITE (f x)) /\
         (!v M N x. v NOTIN f x ==> P (LAM v M @@ N) ([N/v] M) x) /\
@@ -182,20 +190,23 @@ QED
    ---------------------------------------------------------------------- *)
 
 val hnf_def = Define`hnf M = ∀N. ¬(M -h-> N)`;
-val hnf_thm = Store_thm(
-  "hnf_thm",
-  ``(hnf (VAR s) ⇔ T) ∧
+
+Theorem hnf_thm[simp] :
+    (hnf (VAR s) ⇔ T) ∧
     (hnf (M @@ N) ⇔ hnf M ∧ ¬is_abs M) ∧
-    (hnf (LAM v M) ⇔ hnf M)``,
+    (hnf (LAM v M) ⇔ hnf M)
+Proof
   SRW_TAC [][hnf_def, hreduce1_rwts] THEN
   Cases_on `is_abs M` THEN SRW_TAC [][hreduce1_rwts] THEN
   Q.SPEC_THEN `M` FULL_STRUCT_CASES_TAC term_CASES THEN
-  FULL_SIMP_TAC (srw_ss()) [hreduce1_rwts]);
+  FULL_SIMP_TAC (srw_ss()) [hreduce1_rwts]
+QED
 
-val hnf_tpm = Store_thm(
-  "hnf_tpm",
-  ``∀M π. hnf (π·M) = hnf M``,
-  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]);
+Theorem hnf_tpm[simp] :
+    ∀M π. hnf (π·M) = hnf M
+Proof
+  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]
+QED
 
 val strong_cc_ind = IndDefLib.derive_strong_induction (compat_closure_rules,
                                                        compat_closure_ind)
@@ -251,6 +262,35 @@ Proof
   simp[PULL_EXISTS, hnf_appstar]
 QED
 
+(* A more general version of ‘hnf_cases’ directly based on term_laml_cases *)
+Theorem hnf_cases_genX :
+    !X. FINITE X ==>
+        !M. hnf M <=> ?vs args y. ALL_DISTINCT vs /\ (M = LAMl vs (VAR y @* args)) /\
+                                  DISJOINT (set vs) X
+Proof
+    reverse (rw [FORALL_AND_THM, EQ_IMP_THM])
+ >- rw [hnf_appstar]
+ >> MP_TAC (Q.SPEC ‘M’ (MATCH_MP term_laml_cases (ASSUME “FINITE (X :string -> bool)”)))
+ >> RW_TAC std_ss []
+ >| [ (* goal 1 (of 3) *)
+      qexistsl_tac [‘[]’, ‘[]’, ‘s’] >> rw [],
+      (* goal 2 (of 3) *)
+      Know ‘is_comb (M1 @@ M2)’ >- rw [] \\
+      ONCE_REWRITE_TAC [is_comb_appstar_exists] >> rw [] \\
+      Q.PAT_X_ASSUM ‘M1 @@ M2 = t @* args’ (FULL_SIMP_TAC std_ss o wrap) \\
+      fs [hnf_appstar] \\
+     ‘is_var t’ by METIS_TAC [term_cases] >> fs [is_var_cases],
+      (* goal 3 (of 3) *)
+      fs [hnf_LAMl] >> rename1 ‘hnf M’ \\
+     ‘is_var M \/ is_comb M’ by METIS_TAC [term_cases]
+      >- (fs [is_var_cases] \\
+          qexistsl_tac [‘v::vs’, ‘[]’, ‘y’] >> rw []) \\
+      FULL_SIMP_TAC std_ss [Once is_comb_appstar_exists] \\
+      gs [hnf_appstar] \\
+     ‘is_var t’ by METIS_TAC [term_cases] >> fs [is_var_cases] \\
+      qexistsl_tac [‘v::vs’, ‘args’, ‘y’] >> rw [] ]
+QED
+
 (* ----------------------------------------------------------------------
     Weak head reductions (weak_head or -w->)
    ---------------------------------------------------------------------- *)
@@ -698,6 +738,13 @@ val has_hnf_def = Define`
   has_hnf M = ?N. M == N /\ hnf N
 `;
 
+Theorem hnf_has_hnf :
+    !M. hnf M ==> has_hnf M
+Proof
+    rw [has_hnf_def]
+ >> Q.EXISTS_TAC ‘M’ >> rw []
+QED
+
 val has_bnf_hnf = store_thm(
   "has_bnf_hnf",
   ``has_bnf M ⇒ has_hnf M``,
@@ -1116,3 +1163,9 @@ QED
 
 val _ = export_theory()
 val _ = html_theory "head_reduction";
+
+(* References:
+
+   [1] Barendregt, H.P.: The Lambda Calculus, Its Syntax and Semantics.
+       College Publications, London (1984).
+ *)