Added hnf_cases, etc.

examples/lambda/barendregt/chap2Script.sml

@@ -561,6 +561,21 @@ val is_var_vsubst_invariant = Store_thm(
   HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN
   SRW_TAC [][SUB_THM, SUB_VAR]);
 
+Theorem is_var_cases :
+    is_var t <=> ?y. t = VAR y
+Proof
+    Q.SPEC_THEN ‘t’ STRUCT_CASES_TAC term_CASES
+ >> SRW_TAC [][]
+QED
+
+Theorem term_cases :
+    !t. is_var t \/ is_comb t \/ is_abs t
+Proof
+    Q.X_GEN_TAC ‘t’
+ >> Q.SPEC_THEN ‘t’ STRUCT_CASES_TAC term_CASES
+ >> SRW_TAC [][]
+QED
+
 val (bnf_thm, _) = define_recursive_term_function
   `(bnf (VAR s) <=> T) /\
    (bnf (t1 @@ t2) <=> bnf t1 /\ bnf t2 /\ ~is_abs t1) /\

examples/lambda/barendregt/standardisationScript.sml

@@ -1395,36 +1395,6 @@ val strange_cases = prove(
               ]
   ]);
 
-Theorem hnf_LAMl[simp] :
-    hnf (LAMl vs M) <=> hnf M
-Proof
-    Induct_on ‘vs’ >> rw []
-QED
-
-Theorem hnf_appstar :
-    hnf (M @* Ns) /\ Ns <> [] ==> hnf M /\ ~is_abs M
-Proof
-    Q.ID_SPEC_TAC ‘Ns’
- >> HO_MATCH_MP_TAC SNOC_INDUCT
- >> rw [SNOC_APPEND, SYM appstar_SNOC]
- >> Cases_on ‘Ns = []’ >> fs []
-QED
-
-Theorem hnf_decompose :
-    !M : term. hnf M ==> ?vs args y. M = LAMl vs ((VAR y) @* args)
-Proof
-    rpt STRIP_TAC
- >> MP_TAC (Q.SPEC ‘M’ strange_cases)
- >> RW_TAC std_ss []
- >- (FULL_SIMP_TAC std_ss [size_1] \\
-     qexistsl_tac [‘vs’ , ‘[]’, ‘y’] >> rw [])
- >> FULL_SIMP_TAC std_ss [hnf_LAMl]
- >> ‘hnf t /\ ~is_abs t’ by PROVE_TAC [hnf_appstar]
- >> MP_TAC (Q.SPEC ‘t’ term_CASES)
- >> STRIP_TAC >> fs []
- >> qexistsl_tac [‘vs’, ‘args’, ‘s’] >> rw []
-QED
-
 val head_reduction_standard = store_thm(
   "head_reduction_standard",
   ``!s. is_head_reduction s ==> standard_reduction s``,
@@ -2527,5 +2497,35 @@ Proof
  >> MATCH_MP_TAC lameq_appstar_cong >> art []
 QED
 
+Theorem hnf_LAMl[simp] :
+    hnf (LAMl vs M) <=> hnf M
+Proof
+    Induct_on ‘vs’ >> rw []
+QED
+
+Theorem hnf_appstar :
+    hnf (M @* Ns) /\ Ns <> [] ==> hnf M /\ ~is_abs M
+Proof
+    Q.ID_SPEC_TAC ‘Ns’
+ >> HO_MATCH_MP_TAC SNOC_INDUCT
+ >> rw [SNOC_APPEND, SYM appstar_SNOC]
+ >> Cases_on ‘Ns = []’ >> fs []
+QED
+
+Theorem hnf_cases :
+    !M : term. hnf M ==> ?vs args y. M = LAMl vs ((VAR y) @* args)
+Proof
+    rpt STRIP_TAC
+ >> MP_TAC (Q.SPEC ‘M’ strange_cases)
+ >> RW_TAC std_ss []
+ >- (FULL_SIMP_TAC std_ss [size_1] \\
+     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 []
+QED
+
 val _ = export_theory()
 val _ = html_theory "standardisation";