Fix proofs broken by HOL-Theorem-Prover/HOL@b25502a02ed

Author: mn200

compiler/backend/proofs/bvi_tailrecProofScript.sml

@@ -1682,15 +1682,17 @@ Proof
         \\ conj_asm1_tac
         >- (
           match_mp_tac code_rel_union
-          \\ fs[domain_fromAList,DISJOINT_SYM] )
+          \\ fs[domain_fromAList,DISJOINT_SYM]
+          \\ gvs[Abbr‘prog1’])
         \\ `namespace_rel (fromAList prog1) (fromAList prog2)`
         by (
           match_mp_tac (GEN_ALL compile_prog_namespace_rel)
           \\ asm_exists_tac \\ fs[input_condition_def])
         \\ conj_asm1_tac
         >- (
           match_mp_tac namespace_rel_union
-          \\ fs[domain_fromAList,DISJOINT_SYM])
+          \\ fs[domain_fromAList,DISJOINT_SYM]
+          \\ gs[Abbr‘prog1’])
         \\ simp[domain_union]
         \\ imp_res_tac compile_prog_next_mono
         \\ rveq \\ rw[]

compiler/backend/proofs/bvi_to_dataProofScript.sml

@@ -12,7 +12,9 @@ open preamble
 
 val _ = new_theory"bvi_to_dataProof";
 
-val _ = set_grammar_ancestry["bvi_to_data", "bviSem", "bviProps", "dataSem", "dataProps"];
+val _ = set_grammar_ancestry["bvi_to_data", "bviSem", "bviProps", "dataSem",
+                             "dataProps"];
+val _ = temp_delsimps ["fromAList_def"]
 val _ = hide"tail";
 
 (* value relation *)
@@ -935,7 +937,8 @@ Proof
        \\ full_simp_tac(srw_ss())[var_corr_def,get_var_def,lookup_map]
        \\ IMP_RES_TAC LIST_REL_MEM_IMP \\ full_simp_tac(srw_ss())[]
        \\ `lookup x t1.locals <> NONE` by METIS_TAC []
-       \\ Cases_on `lookup x t1.locals` \\ full_simp_tac(srw_ss())[] \\ METIS_TAC [])
+       \\ Cases_on `lookup x t1.locals` \\ full_simp_tac(srw_ss())[]
+       \\ METIS_TAC [])
     \\ full_simp_tac(srw_ss())[]
     \\ Q.ABBREV_TAC `env1 = mk_wf (inter t2.locals (list_to_num_set (REVERSE vs++live++corr)))`
     \\ `var_corr (REVERSE a) (REVERSE vs) (map data_to_bvi_v env1)` by

compiler/backend/proofs/bvl_inlineProofScript.sml

@@ -7,7 +7,7 @@ open preamble backendPropsTheory
      bvl_inlineTheory
 local open bvl_handleProofTheory in end
 
-val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj", "fromAList_def"]
 
 val _ = new_theory"bvl_inlineProof";
 
@@ -31,27 +31,27 @@ val state_rel_alt = state_rel_def
 val state_rel_def =
   state_rel_def |> SIMP_RULE (srw_ss()) [state_component_equality,GSYM CONJ_ASSOC];
 
-val do_app_lemma = prove(
-  ``state_rel t' r ==>
+Theorem do_app_lemma[local]:
+  state_rel t' r ==>
     case do_app op (REVERSE a) r of
     | Rerr err => do_app op (REVERSE a) t' = Rerr err
-    | Rval (v,r2) => ?t2. state_rel t2 r2 /\ do_app op (REVERSE a) t' = Rval (v,t2)``,
+    | Rval (v,r2) => ?t2. state_rel t2 r2 /\
+                          do_app op (REVERSE a) t' = Rval (v,t2)
+Proof
   Cases_on `op = Install` THEN1
    (rw [] \\ fs [do_app_def]
     \\ every_case_tac \\ fs []
     \\ fs [case_eq_thms,UNCURRY,do_install_def]
     \\ rveq \\ fs [PULL_EXISTS]
     \\ fs [SWAP_REVERSE_SYM] \\ rveq \\ fs []
     \\ fs [state_rel_def] \\ rveq \\ fs []
-    \\ fs [domain_map]
     \\ fs [state_component_equality]
     THEN1
      (fs [shift_seq_def,o_DEF] \\ rfs []
       \\ Cases_on `t'.compile_oracle 0` \\ fs []
       \\ Cases_on `r'` \\ fs [] \\ Cases_on `h` \\ fs [] \\ rveq \\ fs []
-      \\ fs [domain_map]
       \\ fs [map_union] \\ AP_TERM_TAC
-      \\ fs [map_fromAList] \\ AP_TERM_TAC \\ fs []
+      \\ simp [map_fromAList, map_insert] \\ AP_TERM_TAC \\ fs []
       \\ rpt (AP_THM_TAC ORELSE AP_TERM_TAC)
       \\ fs [FUN_EQ_THM,FORALL_PROD])
     \\ CCONTR_TAC \\ fs []
@@ -67,7 +67,6 @@ val do_app_lemma = prove(
         `r.compile`,`(I ## MAP (I ## I ## (λx. HD (remove_ticks [x])))) ∘
           t'.compile_oracle`] mp_tac)
     \\ qpat_x_assum `r = _` (assume_tac o GSYM) \\ fs []
-    \\ impl_tac THEN1 fs [domain_map]
     \\ strip_tac \\ fs []
     \\ qpat_x_assum `_ = r` (assume_tac o GSYM) \\ fs []
     \\ rw [] \\ fs [state_component_equality]
@@ -78,7 +77,7 @@ val do_app_lemma = prove(
       `r.compile`,`(I ## MAP (I ## I ## (λx. HD (remove_ticks [x])))) ∘
         t'.compile_oracle`] mp_tac)
   \\ qpat_x_assum `r = _` (assume_tac o GSYM) \\ fs []
-  \\ impl_tac THEN1 fs [domain_map] \\ fs []);
+QED
 
 Theorem evaluate_remove_ticks:
    !k xs env s (t:('c,'ffi) bvlSem$state) res s'.
@@ -767,8 +766,8 @@ Proof
   \\ qexists_tac `aa1` \\ fs []
 QED
 
-val tick_compile_prog_IMP_exp_rel = prove(
-  ``!limit cs0 in1 cs1 in2 k arity exp src_code.
+Theorem tick_compile_prog_IMP_exp_rel[local]:
+  !limit cs0 in1 cs1 in2 k arity exp src_code.
       tick_compile_prog limit cs0 in1 = (cs1,in2) /\
       ALOOKUP in1 k = SOME (arity,exp) /\
       ALL_DISTINCT (MAP FST in1) /\
@@ -780,7 +779,8 @@ val tick_compile_prog_IMP_exp_rel = prove(
       DISJOINT (domain cs0) (set (MAP FST in1)) ==>
       ∃exp2.
         ALOOKUP in2 k = SOME (arity,exp2) /\
-        exp_rel (union src_code (fromAList in1)) [exp] [exp2]``,
+        exp_rel (union src_code (fromAList in1)) [exp] [exp2]
+Proof
   Induct_on `in1`
   \\ fs [FORALL_PROD,tick_compile_prog_def,tick_inline_all_def]
   \\ once_rewrite_tac [tick_inline_all_acc]
@@ -794,7 +794,7 @@ val tick_compile_prog_IMP_exp_rel = prove(
     \\ match_mp_tac exp_rel_tick_inline \\ metis_tac [])
   \\ first_x_assum drule
   \\ disch_then (qspec_then `k` mp_tac) \\ fs []
-  \\ qmatch_goalsub_rename_tac `(p1,p2,p3)::in1`
+  \\ qmatch_goalsub_rename_tac `(p1,p2,p3) :: in1`
   \\ disch_then (qspec_then `union src_code (insert p1 (p2,p3) LN)` mp_tac)
   \\ fs [exp_rel_rw] \\ disch_then match_mp_tac
   \\ reverse (IF_CASES_TAC \\ fs [])
@@ -808,7 +808,6 @@ val tick_compile_prog_IMP_exp_rel = prove(
       \\ fs [subspt_lookup,lookup_union])
     \\ CCONTR_TAC \\ fs [] \\ metis_tac [])
   \\ reverse (rw [])
-  THEN1 (fs [DISJOINT_DEF,domain_union,EXTENSION] \\ metis_tac [])
   \\ fs [lookup_insert,case_eq_thms] \\ rveq
   THEN1
    (rename1 `must_inline k2 _ _`
@@ -817,19 +816,22 @@ val tick_compile_prog_IMP_exp_rel = prove(
     \\ qexists_tac `src_code`
     \\ conj_tac THEN1 fs [subspt_lookup,lookup_union]
     \\ match_mp_tac exp_rel_tick_inline \\ metis_tac [])
-  \\ fs [lookup_union,case_eq_thms,GSYM lookup_NONE_domain,lookup_insert,lookup_def]
+  \\ fs [lookup_union,case_eq_thms,GSYM lookup_NONE_domain,lookup_insert,
+         lookup_def]
   \\ pop_assum (assume_tac o GSYM)
   \\ first_x_assum drule \\ strip_tac \\ fs []
   \\ match_mp_tac (subspt_exp_rel |> ONCE_REWRITE_RULE [CONJ_COMM])
   \\ asm_exists_tac \\ fs []
-  \\ fs [subspt_lookup,lookup_union]);
+  \\ fs [subspt_lookup,lookup_union]
+QED
 
-val in_do_app_lemma = prove(
-  ``in_state_rel limit s1 t1 ==>
+Theorem in_do_app_lemma[local]:
+  in_state_rel limit s1 t1 ==>
     case do_app op a s1 of
     | Rerr err => (err <> Rabort Rtype_error ==> do_app op a t1 = Rerr err)
     | Rval (v,s2) => ?t2. in_state_rel limit s2 t2 /\
-                          do_app op a t1 = Rval (v,t2)``,
+                          do_app op a t1 = Rval (v,t2)
+Proof
   Cases_on `op = Install`
   THEN1
    (rw [] \\ fs [do_app_def]
@@ -898,7 +900,8 @@ val in_do_app_lemma = prove(
   \\ impl_tac THEN1 fs [in_state_rel_def]
   \\ fs [] \\ disch_then kall_tac
   \\ fs [in_state_rel_def]
-  \\ imp_res_tac do_app_const \\ fs []);
+  \\ imp_res_tac do_app_const \\ fs []
+QED
 
 Theorem evaluate_inline:
    !es env s1 res t1 s2 es2.
@@ -1447,11 +1450,13 @@ Proof
   \\ CASE_TAC \\ fs []
 QED
 
-val do_app_lemma = prove(
-  ``let_state_rel q4 l4 s1 t1 ==>
+Theorem do_app_lemma[local]:
+  let_state_rel q4 l4 s1 t1 ==>
     case do_app op a s1 of
     | Rerr err => do_app op a t1 = Rerr err
-    | Rval (v,s2) => ?t2. let_state_rel q4 l4 s2 t2 /\ do_app op a t1 = Rval (v,t2)``,
+    | Rval (v,s2) => ?t2. let_state_rel q4 l4 s2 t2 /\
+                          do_app op a t1 = Rval (v,t2)
+Proof
   Cases_on `op = Install` THEN1
    (rw [] \\ fs [do_app_def]
     \\ every_case_tac \\ fs []
@@ -1479,7 +1484,6 @@ val do_app_lemma = prove(
         `t1.compile`,`(I ## MAP (I ## let_opt q4 l4)) ∘
           s1.compile_oracle`] mp_tac)
     \\ qpat_x_assum `t1 = _` (assume_tac o GSYM) \\ fs []
-    \\ impl_tac THEN1 fs [domain_map]
     \\ strip_tac \\ fs []
     \\ qpat_x_assum `_ = t1` (assume_tac o GSYM) \\ fs []
     \\ rw [] \\ fs [state_component_equality]
@@ -1490,7 +1494,7 @@ val do_app_lemma = prove(
       `t1.compile`,`(I ## MAP (I ##  let_opt q4 l4)) ∘
         s1.compile_oracle`] mp_tac)
   \\ qpat_x_assum `t1 = _` (assume_tac o GSYM) \\ fs []
-  \\ impl_tac THEN1 fs [domain_map] \\ fs []);
+QED
 
 Theorem evaluate_let_op:
    !es env s1 res t1 s2.

compiler/backend/proofs/bvl_to_bviProofScript.sml

@@ -13,7 +13,9 @@ local open
   bvi_tailrecProofTheory
 in end;
 
-val _ = temp_delsimps ["NORMEQ_CONV", "lift_disj_eq", "lift_imp_disj"]
+val _ = temp_delsimps ["NORMEQ_CONV", "lift_disj_eq", "lift_imp_disj",
+                       "fromAList_def", "domain_union", "domain_insert",
+                       "domain_inter"]
 
 val _ = new_theory"bvl_to_bviProof";
 
@@ -1642,7 +1644,7 @@ Proof
   Induct >> simp[aux_code_installed_def] >>
   qx_gen_tac`p`>>PairCases_on`p`>>
   Cases >> simp[IS_SUBLIST] >> strip_tac >- (
-    simp[aux_code_installed_def,lookup_fromAList] >>
+    simp[aux_code_installed_def,lookup_fromAList, Excl "fromAList_def"] >>
     first_x_assum match_mp_tac >>
     var_eq_tac >> full_simp_tac(srw_ss())[] >>
     full_simp_tac(srw_ss())[IS_SUBLIST_APPEND,IS_PREFIX_APPEND] >>
@@ -2437,7 +2439,7 @@ Proof
         \\ fs [domain_fromAList]
         \\ drule (GEN_ALL compile_inc_next_range) \\ fs []
         \\ disch_then drule \\ fs []
-        \\ rw [] \\ fs [])
+        \\ rw [] \\ fs [] \\ gvs[Abbr‘prog1’])
       \\ reverse (rpt strip_tac) \\ rveq \\ fs []
       THEN1
        (first_x_assum drule \\ strip_tac

compiler/backend/proofs/clos_to_bvlProofScript.sml

@@ -23,7 +23,8 @@ val _ = new_theory"clos_to_bvlProof";
 
 val _ = temp_delsimps ["NORMEQ_CONV"]
 val _ = diminish_srw_ss ["ABBREV"]
-val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj", "fromAList_def",
+                       "domain_union", "domain_insert"]
 val _ = set_trace "BasicProvers.var_eq_old" 1
 
 val _ = set_grammar_ancestry

compiler/backend/proofs/data_to_word_assignProofScript.sml

@@ -15,6 +15,10 @@ val _ = new_theory "data_to_word_assignProof";
 val _ = temp_delsimps ["NORMEQ_CONV"]
 val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
 val _ = temp_delsimps ["DIV_NUMERAL_THM"]
+val _ = temp_delsimps ["fromAList_def", "domain_union",
+                       "domain_inter", "domain_difference",
+                       "domain_map", "sptree.map_def", "sptree.lookup_rwts",
+                       "sptree.insert_notEmpty", "sptree.isEmpty_union"]
 val _ = diminish_srw_ss ["ABBREV"]
 val _ = set_trace "BasicProvers.var_eq_old" 1
 

compiler/backend/proofs/data_to_word_bignumProofScript.sml

@@ -13,7 +13,10 @@ local open gen_gcTheory in end
 
 val _ = new_theory "data_to_word_bignumProof";
 
-val _ = temp_delsimps ["NORMEQ_CONV"]
+val _ = temp_delsimps ["NORMEQ_CONV", "fromAList_def", "domain_union",
+                       "domain_inter", "domain_difference",
+                       "domain_map", "sptree.map_def", "sptree.lookup_rwts",
+                       "sptree.insert_notEmpty", "sptree.isEmpty_union"]
 val _ = diminish_srw_ss ["ABBREV"]
 val _ = set_trace "BasicProvers.var_eq_old" 1