Fix proofs after pat_assum rename in HOL

Author: xrchz

holConstrainedExtensionScript.sml

@@ -429,7 +429,7 @@ val constrain_tmass_is_term_assignment = store_thm("constrain_tmass_is_term_assi
     PairCases_on`p`>>
     first_assum(fn th => first_x_assum(strip_assume_tac o MATCH_MP th)) >>
     fs[LET_THM] >>
-    qpat_assum`FLOOKUP X Y = Z`mp_tac >>
+    qpat_x_assum`FLOOKUP X Y = Z`mp_tac >>
     simp[FLOOKUP_FUNION] >>
     BasicProvers.CASE_TAC >- (
       BasicProvers.CASE_TAC >- (
@@ -458,7 +458,7 @@ val constrain_tmass_is_term_assignment = store_thm("constrain_tmass_is_term_assi
         metis_tac[] ) >>
       strip_tac >>
       imp_res_tac ALOOKUP_MEM >>
-      qpat_assum`∀X. Y`mp_tac >>
+      qpat_x_assum`∀X. Y`mp_tac >>
       qpat_abbrev_tac`vars = mlstring_sort X` >>
       disch_then(qspec_then`K boolset =++ ZIP(tyvars_of_upd upd, MAP τ vars)`mp_tac) >>
       impl_tac >- (
@@ -527,13 +527,13 @@ val constrain_tmass_is_term_assignment = store_thm("constrain_tmass_is_term_assi
     imp_res_tac ALOOKUP_MEM >> rfs[MEM_MAP,EXISTS_PROD,ZIP_MAP]>>
     imp_res_tac MEM_ZIP_MEM_MAP >> rfs[] >>
     metis_tac[]) >>
-  qpat_assum`FLOOKUP X Y = Z`mp_tac >>
+  qpat_x_assum`FLOOKUP X Y = Z`mp_tac >>
   simp[FLOOKUP_FUNION] >>
   BasicProvers.CASE_TAC >- (
     strip_tac >>
     fs[theory_ok_def] >>
     qsuff_tac`F`>-rw[]>>
-    qpat_assum`¬x`mp_tac >>simp[]>>
+    qpat_x_assum`¬x`mp_tac >>simp[]>>
     first_x_assum match_mp_tac >>
     simp[IN_FRANGE_FLOOKUP] >>
     metis_tac[] ) >>
@@ -555,7 +555,7 @@ val constrain_tmass_is_term_assignment = store_thm("constrain_tmass_is_term_assi
    is_std_type_assignment δ` by (
      reverse conj_asm2_tac >- fs[is_std_interpretation_def] >>
      simp[Abbr`d1`,GSYM constrain_assignment_def] ) >>
-  qpat_assum`_ = SOME v` mp_tac >>
+  qpat_x_assum`_ = SOME v` mp_tac >>
   Q.PAT_ABBREV_TAC`t1 = domain (typeof pred)` >>
   Q.PAT_ABBREV_TAC`t2 = Tyapp name X` >>
   fs[GSYM mlstring_sort_def] >>
@@ -579,7 +579,7 @@ val constrain_tmass_is_term_assignment = store_thm("constrain_tmass_is_term_assi
     match_mp_tac typesem_sig >>
     qexists_tac`tysof (ctxt)` >>
     imp_res_tac proves_term_ok >>
-    qpat_assum`k ∈ X`kall_tac >>
+    qpat_x_assum`k ∈ X`kall_tac >>
     fs[term_ok_def] >>
     conj_tac >- (
       imp_res_tac term_ok_type_ok >>
@@ -598,7 +598,7 @@ val constrain_tmass_is_term_assignment = store_thm("constrain_tmass_is_term_assi
   BasicProvers.CASE_TAC >>
   BasicProvers.CASE_TAC >>
   qsuff_tac`set (tyvars v) = set (tvars pred)` >- (
-    qpat_assum`set (tyvars v) = X`kall_tac >>
+    qpat_x_assum`set (tyvars v) = X`kall_tac >>
     rw[] >>
     `mlstring_sort (tvars pred) = mlstring_sort (tyvars v)` by (
       `ALL_DISTINCT (tvars pred)` by simp[] >>
@@ -997,7 +997,7 @@ val constrain_interpretation_satisfies = store_thm("constrain_interpretation_sat
     `mlstring_sort (tyvars ty0) = tyvars_of_upd upd` by (
       fs[MEM_MAP,PULL_EXISTS,EXISTS_PROD] >>
       fs[tyvars_of_upd_def] >>
-      qpat_assum`X = mlstring_sort (tvars p)`(mp_tac o SYM) >>
+      qpat_x_assum`X = mlstring_sort (tvars p)`(mp_tac o SYM) >>
       simp[] >> strip_tac >>
       imp_res_tac ALOOKUP_MEM >>
       res_tac >>

reflectionScript.sml

@@ -205,7 +205,7 @@ val range_fun_to_inner = store_thm("range_fun_to_inner",
     rw[] ) >>
   qspecl_then[`a`,`range ina`,`range inb`]mp_tac (UNDISCH in_funspace_abstract) >>
   simp[] >> strip_tac >>
-  qpat_assum`a = X`(SUBST1_TAC) >>
+  qpat_x_assum`a = X`(SUBST1_TAC) >>
   qsuff_tac`∃x. Abstract (range ina) (range inb) f = fun_to_inner ina inb x` >- metis_tac[] >>
   rw[fun_to_inner_def] >>
   qexists_tac`finv inb o f o ina` >>
@@ -334,7 +334,7 @@ val tag_exists = prove(
     metis_tac[pair_not_empty] ) >>
   strip_tac >>
   imp_res_tac (UNDISCH in_funspace_abstract) >>
-  qpat_assum`X = Y`mp_tac >>
+  qpat_x_assum`X = Y`mp_tac >>
   imp_res_tac is_extensional >> fs[extensional_def] >> pop_assum kall_tac >>
   simp[EQ_IMP_THM,EXISTS_OR_THM] >> disj1_tac >>
   srw_tac[boolSimps.DNF_ss][mem_binary_union,mem_boolset,true_def] >> disj1_tac >>
@@ -461,7 +461,7 @@ val good_context_instance_equality = prove(
   impl_tac >- (
     simp[is_type_valuation_def,combinTheory.APPLY_UPDATE_THM] >>
     reverse(rw[mem_boolset]) >- metis_tac[] >>
-    qpat_assum`X = Y` (SUBST1_TAC o SYM) >>
+    qpat_x_assum`X = Y` (SUBST1_TAC o SYM) >>
     match_mp_tac (UNDISCH typesem_inhabited) >>
     fs[is_valuation_def,is_interpretation_def] >>
     metis_tac[] ) >>
@@ -1285,7 +1285,7 @@ val termsem_comb1_ax = store_thm("termsem_comb1_ax",
   Q.PAT_ABBREV_TAC`s = [(a0,Var x tyia)]` >>
   `term_ok (sigof ctxt) t` by (
     fs[theory_ok_def] >> res_tac >>
-    qpat_assum`is_std_sig X`assume_tac >>
+    qpat_x_assum`is_std_sig X`assume_tac >>
     fs[term_ok_equation,term_ok_def] ) >>
   `term_ok (sigof ctxt) (VSUBST s t)` by (
     match_mp_tac term_ok_VSUBST >>
@@ -1385,7 +1385,7 @@ val termsem_comb2_ax = store_thm("termsem_comb2_ax",
   Q.PAT_ABBREV_TAC`s = [(a0,Var x tyia);Y]` >>
   `term_ok (sigof ctxt) t` by (
     fs[theory_ok_def] >> res_tac >>
-    qpat_assum`is_std_sig X`assume_tac >>
+    qpat_x_assum`is_std_sig X`assume_tac >>
     fs[term_ok_equation,term_ok_def] ) >>
   `term_ok (sigof ctxt) (VSUBST s t)` by (
     match_mp_tac term_ok_VSUBST >>
@@ -1516,7 +1516,7 @@ val termsem_comb3_ax = store_thm("termsem_comb3_ax",
   Q.PAT_ABBREV_TAC`s = (a0,Var x tyia)::Y	` >>
   `term_ok (sigof ctxt) t` by (
     fs[theory_ok_def] >> res_tac >>
-    qpat_assum`is_std_sig X`assume_tac >>
+    qpat_x_assum`is_std_sig X`assume_tac >>
     fs[term_ok_equation,term_ok_def] ) >>
   `term_ok (sigof ctxt) (VSUBST s t)` by (
     match_mp_tac term_ok_VSUBST >>