More fixes for changes in HOL

Author: hrutvik

compiler/backend/passes/proofs/state_to_cakeProofScript.sml

@@ -1908,7 +1908,7 @@ Proof
       qexists0 >> reverse $ rw[step_rel_cases]
       >- (gvs[store_lookup_def] >> Cases_on `cst` >> gvs[]) >>
       gvs[state_rel, ADD1] >> rpt $ goal_assum $ drule_at Any >>
-      imp_res_tac LIST_REL_LENGTH >> simp[]
+      imp_res_tac LIST_REL_LENGTH >> simp[SNOC_APPEND]
       ) >>
     (* AtomOp *)
     gvs[application_def, sstep] >>

compiler/backend/passes/proofs/thunk_combine_Forcing_LambdasScript.sml

@@ -1179,7 +1179,7 @@ Proof
   qspecl_then [‘eL’] assume_tac SNOC_CASES >> gs [ADD1] >>
   rename1 ‘SNOC v vL’ >> Cases_on ‘vL’ >> gs []
   >- gs [eval_to_def, dest_anyClosure_def] >>
-  gvs [FOLDR_SNOC, FOLDL_APPEND, eval_to_def] >>
+  gvs [FOLDR_SNOC, FOLDL_APPEND, eval_to_def, SNOC_APPEND] >>
   rename1 ‘SUC (LENGTH vL) = LENGTH eL’ >>
   first_x_assum $ qspecl_then [‘eL’, ‘Lam v e’, ‘k’] assume_tac >>
   gvs [subst_def, eval_to_def, dest_anyClosure_def] >>
@@ -1209,7 +1209,7 @@ Proof
   qspecl_then [‘eL’] assume_tac SNOC_CASES >> gs [ADD1] >>
   rename1 ‘SNOC v vL’ >> Cases_on ‘vL’ >> gs []
   >- gs [eval_to_def, dest_anyClosure_def] >>
-  gvs [FOLDR_SNOC, FOLDL_APPEND, eval_to_def] >>
+  gvs [FOLDR_SNOC, FOLDL_APPEND, eval_to_def, SNOC_APPEND] >>
   rename1 ‘SUC (LENGTH vL) = LENGTH eL’ >>
   gs [subst_def, eval_to_def, dest_anyClosure_def] >>
   AP_TERM_TAC >>
@@ -1252,7 +1252,7 @@ Proof
   qspecl_then [‘eL’] assume_tac SNOC_CASES >> gs [ADD1] >>
   rename1 ‘SNOC v vL’ >> Cases_on ‘vL’ >> gs []
   >- (gs [eval_to_def, dest_anyClosure_def]) >>
-  gs [FOLDR_SNOC, FOLDL_APPEND, eval_to_def]
+  gs [FOLDR_SNOC, FOLDL_APPEND, eval_to_def, SNOC_APPEND]
 QED
 
 Theorem eval_to_Apps_Rec_0:
@@ -1315,14 +1315,16 @@ Proof
   Induct using SNOC_INDUCT \\ gs []
   \\ rw [] \\ gs [GSYM LESS_EQ_IFF_LESS_SUC, FOLDL_SNOC]
   \\ rename1 ‘SNOC x eL’
+  \\ gvs[SNOC_APPEND]
   \\ qspec_then ‘eL2’ assume_tac SNOC_CASES \\ gvs [FOLDL_APPEND]
-  \\ rename1 ‘eL2 ++ [x2]’ \\ gs [SNOC_APPEND]
-  \\ dxrule_then assume_tac LESS_EQ_CASES \\ gs [EL_SNOC, EL_LENGTH_SNOC, eval_to_def, EL_APPEND_EQN]
+  \\ rename1 ‘SNOC x2 eL2’ \\ gvs[SNOC_APPEND, FOLDL_APPEND]
+  \\ dxrule_then assume_tac LESS_EQ_CASES
+  \\ gs [EL_SNOC, EL_LENGTH_SNOC, eval_to_def, EL_APPEND_EQN]
   \\ Cases_on ‘eval_to k x2 = INL Diverge’ \\ gs []
   \\ dxrule_then assume_tac eval_to_mono \\ gs [GSYM ADD1]
   >- (‘∃j. ($= +++ v_rel) (eval_to k x) (eval_to (k + j) x2)’
         by (last_x_assum $ qspec_then ‘LENGTH eL2’ assume_tac
-            \\ Cases_on ‘eval_to k x = INL Type_error’ \\ gs [])
+            \\ Cases_on ‘eval_to k x = INL Type_error’ \\ gs [SF SFY_ss])
       \\ Cases_on ‘eval_to k x’
       >~[‘eval_to k x = INL err’]
       >- (Cases_on ‘err’ \\ gs []
@@ -1333,7 +1335,8 @@ Proof
       \\ impl_tac \\ gs []
       \\ rw []
       \\ last_x_assum $ drule_then assume_tac \\ gs []
-      \\ first_x_assum $ irule_at Any)
+      \\ first_x_assum $ irule_at Any
+      )
   \\ last_x_assum $ qspec_then ‘LENGTH eL2’ assume_tac \\ gs []
   \\ Cases_on ‘eval_to k x2’ \\ gs []
 QED
@@ -1349,9 +1352,9 @@ Theorem eval_to_Apps_arg_Div_combine_rel2:
 Proof
   Induct using SNOC_INDUCT \\ gs []
   \\ rw [] \\ gs [GSYM LESS_EQ_IFF_LESS_SUC, FOLDL_SNOC]
-  \\ rename1 ‘SNOC x eL’
+  \\ rename1 ‘SNOC x eL’ \\ gvs[SNOC_APPEND]
   \\ qspec_then ‘eL2’ assume_tac SNOC_CASES \\ gvs [FOLDL_APPEND]
-  \\ rename1 ‘eL2 ++ [x2]’ \\ gs [SNOC_APPEND]
+  \\ rename1 ‘SNOC x2 eL2’ \\ gs [SNOC_APPEND, FOLDL_APPEND]
   \\ dxrule_then assume_tac LESS_EQ_CASES \\ gs [EL_SNOC, EL_LENGTH_SNOC, eval_to_def, EL_APPEND_EQN]
   \\ Cases_on ‘eval_to k x2 = INL Diverge’ \\ gs []
   \\ dxrule_then assume_tac eval_to_mono \\ gs [GSYM ADD1]
@@ -1417,11 +1420,11 @@ Theorem eval_to_Apps_Div_or_INR:
 Proof
   Induct using SNOC_INDUCT \\ gs [FOLDL_SNOC]
   \\ gen_tac \\ gen_tac \\ qspec_then ‘vL1’ assume_tac SNOC_CASES
-  \\ gs [GSYM ADD1, FOLDL_APPEND]
+  \\ gs [GSYM ADD1, FOLDL_APPEND, SNOC_APPEND]
   \\ rw []
   \\ once_rewrite_tac [eval_to_def] \\ gs []
   \\ first_assum $ qspec_then ‘LENGTH eL’ assume_tac \\ gs [EL_LENGTH_SNOC, EL_APPEND_EQN]
-  \\ Cases_on ‘eval_to k x’ \\ gs []
+  \\ Cases_on ‘eval_to k x’
   \\ rename1 ‘LIST_REL _ (vL1 ++ [v1])’
   \\ last_x_assum $ qspecl_then [‘vL1’, ‘e’, ‘k’] mp_tac \\ gs []
   \\ impl_tac
@@ -1455,7 +1458,7 @@ Theorem eval_to_Apps_LIST_INR:
   ∀eL vL e k. LIST_REL (λe v. ∀j. eval_to (j + k) e = INR v) eL vL
               ⇒ ∀j. k ≤ j ⇒ eval_to j (Apps e eL) = eval_to j (Apps e (MAP Value vL))
 Proof
-  Induct using SNOC_INDUCT \\ gs [LIST_REL_SNOC, PULL_EXISTS, FOLDL_APPEND, FOLDL_SNOC]
+  Induct using SNOC_INDUCT \\ gs [LIST_REL_SNOC, PULL_EXISTS, FOLDL_APPEND, FOLDL_SNOC, SNOC_APPEND]
   \\ rw [] \\ last_x_assum $ drule_all_then assume_tac
   \\ gs [eval_to_def]
   \\ first_x_assum $ qspec_then ‘j - k’ assume_tac

compiler/backend/passes/proofs/thunk_remove_unuseful_bindingsScript.sml

@@ -554,7 +554,7 @@ Proof
           \\ ‘OPTREL clean_rel (ALOOKUP (REVERSE xs) s) (ALOOKUP (REVERSE ys) s)’
             by (irule LIST_REL_OPTREL
                 \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, LIST_EQ_REWRITE, EL_MAP])
-          \\ gvs [REVERSE_APPEND]
+          \\ gvs [REVERSE_APPEND, SNOC_APPEND]
           \\ IF_CASES_TAC \\ gvs []
           \\ gvs [OPTREL_def]
           \\ rpt $ dxrule_then assume_tac ALOOKUP_MEM \\ gvs [EVERY_MEM, MEM_MAP, PULL_EXISTS, FORALL_PROD]
@@ -577,7 +577,7 @@ Proof
               \\ ‘OPTREL clean_rel (ALOOKUP (REVERSE xs) s) (ALOOKUP (REVERSE ys) s)’
                 by (irule LIST_REL_OPTREL
                     \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, LIST_EQ_REWRITE, EL_MAP])
-              \\ gvs [REVERSE_APPEND] \\ IF_CASES_TAC
+              \\ gvs [REVERSE_APPEND, SNOC_APPEND] \\ IF_CASES_TAC
               \\ gvs [OPTREL_def]
               \\ rpt $ dxrule_then assume_tac ALOOKUP_MEM \\ gvs [EVERY_MEM, MEM_MAP, PULL_EXISTS]
               \\ last_x_assum $ dxrule_then assume_tac
@@ -611,7 +611,7 @@ Proof
               \\ ‘OPTREL clean_rel (ALOOKUP (REVERSE xs) s) (ALOOKUP (REVERSE ys) s)’
                 by (irule LIST_REL_OPTREL
                     \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, LIST_EQ_REWRITE, EL_MAP])
-              \\ gvs [REVERSE_APPEND]
+              \\ gvs [REVERSE_APPEND, SNOC_APPEND]
               \\ rename1 ‘¬MEM v _’ \\ rename1 ‘v = s’ \\ Cases_on ‘v = s’ \\ gvs []
               \\ gvs [OPTREL_def]
               \\ rpt $ dxrule_then assume_tac ALOOKUP_MEM \\ gvs [EVERY_MEM, MEM_MAP, PULL_EXISTS]
@@ -751,7 +751,7 @@ Proof
         \\ qspecl_then [‘MAP (λ(v,e). (v, Recclosure f v)) f’, ‘x’] assume_tac subst_notin_frees
         \\ gvs [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD, GSYM FST_THM,
                 EVERY_MEM, DISJOINT_ALT, subst_funs_def])
-    >- (gvs [eval_to_def, subst_funs_def, MAP_APPEND, subst_APPEND]
+    >- (gvs [eval_to_def, subst_funs_def, MAP_APPEND, subst_APPEND, SNOC_APPEND]
         \\ IF_CASES_TAC >- (qexists_tac ‘0’ \\ gs []) \\ gs [subst1_notin_frees]
         \\ last_x_assum $ qspec_then ‘k - 1’ assume_tac \\ gvs [] \\ pop_assum irule
         \\ irule clean_rel_subst
@@ -890,7 +890,7 @@ Proof
             by (irule LIST_REL_OPTREL
                 \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, EL_MAP, LIST_EQ_REWRITE])
           \\ gs [OPTREL_def]
-          >- (qexists_tac ‘j’ \\ gvs [REVERSE_APPEND]
+          >- (qexists_tac ‘j’ \\ gvs [REVERSE_APPEND, SNOC_APPEND]
               \\ IF_CASES_TAC \\ gvs [])
           \\ rename1 ‘clean_rel x0 y0’
           \\ ‘MEM (s, x0) xs’ by (rpt $ dxrule_then assume_tac ALOOKUP_MEM \\ gvs [])
@@ -899,6 +899,7 @@ Proof
           \\ Cases_on ‘x0’ \\ gvs [ok_bind_def, clean_rel_def]
           >~[‘subst_funs ys e2’]
           >- (rename1 ‘clean_rel e1 e2’
+              \\ gvs[SNOC_APPEND]
               \\ rename1 ‘xs ++ [(v,w)]’
               \\ last_x_assum $ qspecl_then [‘subst_funs (xs++[(v,w)]) e1’, ‘subst_funs ys e2’] mp_tac
               \\ impl_tac
@@ -919,21 +920,21 @@ Proof
               \\ Cases_on ‘eval_to (k - 1) (subst_funs ys e2) = INL Diverge’ \\ gs []
               >- (qexists_tac ‘0’
                   \\ Cases_on ‘eval_to k x = INL Diverge’ \\ gs []
-                  \\ dxrule_then (qspecl_then [‘j + k’] assume_tac) eval_to_mono \\ gs [REVERSE_APPEND]
+                  \\ dxrule_then (qspecl_then [‘j + k’] assume_tac) eval_to_mono \\ gs [REVERSE_APPEND, SNOC_APPEND]
                   \\ IF_CASES_TAC \\ gvs []
                   \\ Cases_on ‘eval_to (k - 1) (subst_funs (xs ++ [(v,w)]) e1) = INL Diverge’ \\ gs []
                   \\ dxrule_then (qspecl_then [‘j2 + k - 1’] assume_tac) eval_to_mono \\ gs [])
               \\ qexists_tac ‘j + j2’
               \\ ‘eval_to (j + j2 + k) x = eval_to (j + k) x’ by (irule eval_to_mono \\ gvs [])
-              \\ gvs [REVERSE_APPEND]
+              \\ gvs [REVERSE_APPEND, SNOC_APPEND]
               \\ IF_CASES_TAC \\ gvs []
               \\ ‘eval_to (j + (j2 + k) - 1) (subst_funs (xs++[(v,w)]) e1)
                   = eval_to (j2 + k - 1) (subst_funs (xs++[(v,w)]) e1)’
                 by (irule eval_to_mono
                     \\ Cases_on ‘eval_to (j2 + k - 1) (subst_funs (xs++[(v,w)]) e1)’
                     \\ Cases_on ‘eval_to (k - 1) (subst_funs ys e2)’ \\ gvs [])
               \\ gvs [])
-          \\ qexists_tac ‘j’ \\ gvs [REVERSE_APPEND]
+          \\ qexists_tac ‘j’ \\ gvs [REVERSE_APPEND, SNOC_APPEND]
           \\ IF_CASES_TAC \\ gvs []
           \\ rpt $ dxrule_then assume_tac ALOOKUP_MEM \\ gs []
           \\ last_x_assum $ kall_tac \\ last_x_assum $ kall_tac
@@ -1347,7 +1348,7 @@ Proof
       \\ ‘OPTREL clean_rel (ALOOKUP (REVERSE xs) s) (ALOOKUP (REVERSE ys) s)’
         by (irule LIST_REL_OPTREL
             \\ gvs [LIST_REL_EL_EQN, ELIM_UNCURRY, EL_MAP, LIST_EQ_REWRITE])
-      \\ gvs [REVERSE_APPEND] \\ IF_CASES_TAC \\ gs []
+      \\ gvs [REVERSE_APPEND, SNOC_APPEND] \\ IF_CASES_TAC \\ gs []
       \\ gs [OPTREL_def]
       \\ qpat_x_assum ‘clean_rel x0 _’ mp_tac
       \\ ‘ok_bind x0’ by (rpt $ dxrule_then assume_tac ALOOKUP_MEM \\ gvs [EVERY_MEM, MEM_MAP, PULL_EXISTS]

compiler/backend/passes/proofs/thunk_split_Forcing_LamProofScript.sml

@@ -1110,7 +1110,7 @@ Proof
                   qpat_x_assum ‘LENGTH l3 = LENGTH (FILTER FST (ZIP (bL, REVERSE l)))’ mp_tac >>
                   rpt $ pop_assum kall_tac >>
                   qid_spec_tac ‘l3’ >> qid_spec_tac ‘bL’ >>
-                  Induct_on ‘l’ using SNOC_INDUCT >> simp [merge_inside_def, REVERSE_SNOC] >>
+                  Induct_on ‘l’ using SNOC_INDUCT >> simp [merge_inside_def, REVERSE_SNOC, SNOC_APPEND] >>
                   gen_tac >> Cases >> simp [] >>
                   IF_CASES_TAC >> simp [merge_inside_def] >>
                   Cases >> simp [merge_inside_def]) >>
@@ -1362,7 +1362,7 @@ Proof
                   by (Cases_on ‘row’ >> gs [] >>
                       rename1 ‘my_function_row _ (h::_)’ >> PairCases_on ‘h’ >>
                       gs [rows_of_def, freevars_def] >>
-                      gs [SUBSET_DEF]) >>
+                      metis_tac[SUBSET_DEF]) >>
                 pop_assum mp_tac >>
                 dxrule_then (drule_then mp_tac) SUBSET_TRANS >>
                 qpat_x_assum ‘set_of s2 ⊆ set_of s3’ mp_tac >>

typeclass/typing/pure_tcexp_typingPropsScript.sml

@@ -1428,8 +1428,7 @@ Proof
   >- (
     first_x_assum $ irule_at (Pos last) >>
     gvs[MAP_MAP_o,combinTheory.o_DEF,LAMBDA_PROD] >>
-    first_x_assum $ resolve_then (Pos hd)
-      mp_tac APPEND_ASSOC_four >>
+    first_x_assum $ resolve_then (Pos hd) mp_tac EQ_REFL >>
     disch_then $ qspec_then `MAP (tshift (LENGTH new)) ts` mp_tac >>
     impl_tac
     >- (
@@ -1460,7 +1459,7 @@ Proof
       last_x_assum drule >>
       ntac 2 (pairarg_tac >> gvs[]) >>
       strip_tac >>
-      first_x_assum $ resolve_then (Pos hd) mp_tac APPEND_ASSOC_four >>
+      first_x_assum $ resolve_then (Pos hd) mp_tac EQ_REFL >>
       disch_then $ qspec_then `MAP (tshift (LENGTH vars)) ts` mp_tac >>
       impl_tac
       >- (
@@ -1476,7 +1475,7 @@ Proof
     first_x_assum drule >>
     rw[type_ok_def] >>
     dxrule_then irule kind_ok_subst_db_APPEND >>
-    irule_at (Pos $ el 2) APPEND_ASSOC_four >>
+    irule_at (Pos $ el 2) EQ_REFL >>
     rw[LIST_REL_EL_EQN,EL_MAP] >>
     first_x_assum $ drule_then strip_assume_tac >>
     dxrule_then irule kind_ok_shift_db_APPEND >>
@@ -1934,7 +1933,7 @@ Proof
     first_x_assum drule >>
     rw[type_ok_def] >>
     dxrule_then irule kind_ok_shift_db_APPEND >>
-    irule_at (Pos hd) APPEND_ASSOC_four >>
+    irule_at (Pos hd) EQ_REFL >>
     simp[]
   )
   >- (

typeclass/typing/typeclass_kindCheckScript.sml

@@ -235,7 +235,7 @@ Theorem kind_wf_cons_types:
 Proof
   Induct_on `ts` using SNOC_INDUCT >>
   rw[cons_types_def,kind_arrows_def,kind_arrows_APPEND,
-    cons_types_SNOC,LIST_REL_SNOC,PULL_EXISTS] >>
+    cons_types_SNOC,LIST_REL_SNOC,PULL_EXISTS, SNOC_APPEND] >>
   metis_tac[]
 QED
 

typeclass/typing/typeclass_typesPropsScript.sml

@@ -386,7 +386,7 @@ QED
 Theorem ty_args_SNOC:
   ty_args (Cons t1 t2) = SNOC t2 (ty_args t1)
 Proof
-  simp[ty_args_def,ty_args_aux_SNOC]
+  simp[ty_args_def,ty_args_aux_SNOC,SNOC_APPEND]
 QED
 
 Theorem ty_args_alt:
@@ -573,7 +573,7 @@ Theorem subst_db_ty_args:
   | a => MAP (subst_db skip ts) (ty_args t)
 Proof
   ho_match_mp_tac subst_db_ind >>
-  rw[subst_db_def,ty_args_alt,head_ty_def] >>
+  rw[subst_db_def,ty_args_alt,head_ty_def,SNOC_APPEND] >>
   TOP_CASE_TAC >>
   IF_CASES_TAC >>
   rw[]
@@ -599,7 +599,7 @@ Theorem shift_db_ty_args:
     MAP (shift_db skip n) (ty_args t)
 Proof
   ho_match_mp_tac shift_db_ind >>
-  rw[shift_db_def,ty_args_alt]
+  rw[shift_db_def,ty_args_alt,SNOC_APPEND]
 QED
 
 (******************** Properties of types ********************)

typeclass/typing/typeclass_typingProofScript.sml

@@ -3094,7 +3094,7 @@ Proof
   irule_at (Pat `Functions (_::_) _ = _`) Functions_CONS_alt >>
   simp[cons_types_def] >>
   irule_at (Pat `Functions _ _ = Functions _ _`) EQ_REFL >>
-  simp[kind_ok,LLOOKUP_THM,EL_APPEND_EQN,specialises_def] >>
+  simp[kind_ok,LLOOKUP_THM,EL_APPEND_EQN,specialises_def,SNOC_APPEND] >>
   qrefine `GENLIST TypeVar (LENGTH meth_pred_type0)` >>
   rw[LIST_REL_EL_EQN,kind_ok,oEL_THM,EL_APPEND_EQN] >>
   DEP_REWRITE_TAC[subst_db_sub_tshift_TypeVar] >>
@@ -4103,6 +4103,7 @@ Proof
     first_x_assum drule >>
     simp[Abbr`pred_ty_scheme`,PULL_EXISTS,
       translate_pred_type_scheme_get_method_type] >>
+    gvs[SNOC_APPEND] >>
     rw[translate_predicate_def] >>
     simp[ELIM_UNCURRY,SRULE[ELIM_UNCURRY] ALOOKUP_MAP_2] >>
     simp[tcons_to_type_def,cons_types_def] >>