Reworked "strange_cases" by the newly added "term_laml_cases"

examples/lambda/barendregt/chap2Script.sml

@@ -830,6 +830,16 @@ val is_comb_APP_EXISTS = store_thm(
   ``!t. is_comb t = (?u v. t = u @@ v)``,
   PROVE_TAC [term_CASES, is_comb_thm]);
 
+Theorem is_comb_appstar_exists :
+    !M. is_comb M ==> ?t args. (M = t @* args) /\ args <> [] /\ ~is_comb t
+Proof
+    HO_MATCH_MP_TAC simple_induction >> rw []
+ >> reverse (Cases_on ‘is_comb M’)
+ >- (qexistsl_tac [‘M’, ‘[M']’] >> rw [])
+ >> FULL_SIMP_TAC std_ss [GSYM appstar_SNOC]
+ >> qexistsl_tac [‘t’, ‘SNOC M' args’] >> rw []
+QED
+
 val is_comb_rator_rand = store_thm(
   "is_comb_rator_rand",
   ``!t. is_comb t ==> (rator t @@ rand t = t)``,
@@ -999,44 +1009,33 @@ Proof
  >> MATCH_MP_TAC lameq_appstar_cong >> art []
 QED
 
+(* NOTE: added ‘DISTINCT vs’ in all cases.
+
+   This proof is now based on the newly added "term_laml_cases".
+ *)
 Theorem strange_cases :
-    !M : term. (?vs M'. (M = LAMl vs M') /\ (size M' = 1)) \/
+    !M : term. (?vs M'. (M = LAMl vs M') /\ (size M' = 1) /\ ALL_DISTINCT vs) \/
                (?vs args t.
-                         (M = LAMl vs (FOLDL APP t args)) /\
-                         ~(args = []) /\ ~is_comb t)
+                         (M = LAMl vs (t @* args)) /\
+                         ~(args = []) /\ ~is_comb t /\ ALL_DISTINCT vs)
 Proof
-  HO_MATCH_MP_TAC simple_induction THEN REPEAT CONJ_TAC THENL [
-    (* VAR *) GEN_TAC THEN DISJ1_TAC THEN
-              MAP_EVERY Q.EXISTS_TAC [`[]`, `VAR s`] THEN SRW_TAC [][size_thm],
-    (* app *) MAP_EVERY Q.X_GEN_TAC [`M`,`N`] THEN
-              DISCH_THEN (CONJUNCTS_THEN ASSUME_TAC) THEN
-              DISJ2_TAC THEN Q.EXISTS_TAC `[]` THEN
-              SIMP_TAC (srw_ss()) [] THEN
-              `(?vs M'. (M = LAMl vs M') /\ (size M' = 1)) \/
-               (?vs args t.
-                        (M = LAMl vs (FOLDL APP t args)) /\ ~(args = []) /\
-                        ~is_comb t)` by PROVE_TAC []
-              THENL [
-                MAP_EVERY Q.EXISTS_TAC [`[N]`, `M`] THEN
-                ASM_SIMP_TAC (srw_ss()) [] THEN
-                fs [size_1_cases],
-                ASM_SIMP_TAC (srw_ss()) [] THEN
-                Cases_on `vs` THENL [
-                  MAP_EVERY Q.EXISTS_TAC [`SNOC N args`, `t`] THEN
-                  ASM_SIMP_TAC (srw_ss()) [FOLDL_SNOC],
-                  MAP_EVERY Q.EXISTS_TAC [`[N]`, `M`] THEN
-                  ASM_SIMP_TAC (srw_ss()) []
-                ]
-              ],
-    (* LAM *) MAP_EVERY Q.X_GEN_TAC [`x`,`M`] THEN STRIP_TAC THENL [
-                DISJ1_TAC THEN
-                MAP_EVERY Q.EXISTS_TAC [`x::vs`, `M'`] THEN
-                ASM_SIMP_TAC (srw_ss()) [],
-                DISJ2_TAC THEN
-                MAP_EVERY Q.EXISTS_TAC [`x::vs`, `args`, `t`] THEN
-                ASM_SIMP_TAC (srw_ss()) []
-              ]
-  ]
+    rpt STRIP_TAC
+ >> MP_TAC (Q.SPEC ‘M’ (MATCH_MP term_laml_cases
+                                (INST_TYPE [“:α” |-> “:string”] FINITE_EMPTY)))
+ >> RW_TAC std_ss [DISJOINT_EMPTY]
+ >| [ (* goal 1 (of 3) *)
+      DISJ1_TAC >> qexistsl_tac [‘[]’, ‘VAR s’] >> rw [],
+      (* goal 2 (of 3) *)
+      DISJ2_TAC >> reverse (Cases_on ‘is_comb M1’)
+      >- (qexistsl_tac [‘[]’, ‘[M2]’, ‘M1’] >> rw []) \\
+      IMP_RES_TAC is_comb_appstar_exists \\
+      qexistsl_tac [‘[]’, ‘SNOC M2 args’, ‘t’] >> rw [],
+      (* goal 3 (of 3) *)
+     ‘is_var Body \/ is_comb Body’ by METIS_TAC [term_cases]
+      >- (DISJ1_TAC >> qexistsl_tac [‘v::vs’, ‘Body’] >> rw [] \\
+          fs [is_var_cases]) \\
+      IMP_RES_TAC is_comb_appstar_exists \\
+      DISJ2_TAC >> qexistsl_tac [‘v::vs’, ‘args’, ‘t’] >> rw [] ]
 QED
 
 val _ = remove_ovl_mapping "Y" {Thy = "chap2", Name = "Y"}

examples/lambda/barendregt/head_reductionScript.sml

@@ -238,24 +238,17 @@ QED
 Theorem hnf_cases :
     !M : term. hnf M <=> ?vs args y. ALL_DISTINCT vs /\ (M = LAMl vs (VAR y @* args))
 Proof
-    simp [FORALL_AND_THM, EQ_IMP_THM]
- (* this direction is proved by Michael Norrish *)
- >> reverse conj_tac
- >- simp [PULL_EXISTS, hnf_appstar]
- (* below is learnt from bnf_characterisation *)
- >> ho_match_mp_tac nc_INDUCTION2
- >> qexists_tac ‘{}’ >> rw [] >~ [‘VAR _ @* _ = M1 @@ M2’]
- >- (gs [app_eq_appstar] \\
-     qexists_tac ‘args ++ [M2]’ >> rw [GSYM SNOC_APPEND])
- >> gs [app_eq_appstar] >~ [‘VAR z @* Ms’]
- >> reverse (Cases_on ‘MEM y vs’)
- >- (qexistsl_tac [‘y::vs’, ‘Ms’, ‘z’] >> simp [])
- >> ‘y # LAMl vs (VAR z @* Ms)’ by simp [FV_LAMl]
- >> Q_TAC (NEW_TAC "x") ‘y INSERT (set vs) UNION (FV (VAR z @* Ms))’
- >> ‘x # LAMl vs (VAR z @* Ms)’ by simp [FV_LAMl]
- >> dxrule_then (qspec_then ‘y’ mp_tac) tpm_ALPHA
- >> simp [tpm_fresh, FV_LAMl]
- >> strip_tac >> qexists ‘x::vs’ >> simp []
+  simp[FORALL_AND_THM, EQ_IMP_THM] >> conj_tac
+  >- (gen_tac >> MP_TAC (Q.SPEC ‘M’ strange_cases)
+      >> RW_TAC std_ss []
+      >- (FULL_SIMP_TAC std_ss [size_1_cases] \\
+          qexistsl_tac [‘vs’, ‘[]’, ‘y’] >> rw [])
+      >> FULL_SIMP_TAC std_ss [hnf_LAMl]
+      >> ‘hnf t /\ ~is_abs t’ by PROVE_TAC [hnf_appstar]
+      >> ‘is_var t’ by METIS_TAC [term_cases]
+      >> FULL_SIMP_TAC std_ss [is_var_cases]
+      >> qexistsl_tac [‘vs’, ‘args’, ‘y’] >> art []) >>
+  simp[PULL_EXISTS, hnf_appstar]
 QED
 
 (* ----------------------------------------------------------------------