--- a/src/HOL/Meson.thy Thu Oct 28 20:05:18 2021 +0200
+++ b/src/HOL/Meson.thy Thu Oct 28 20:06:29 2021 +0200
@@ -190,7 +190,6 @@
unfolding skolem_def COMBK_def by (rule refl)
lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff]
-lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff]
subsection \<open>Meson package\<close>
@@ -204,6 +203,5 @@
not_impD iff_to_disjD not_iffD not_refl_disj_D conj_exD1 conj_exD2 disj_exD
disj_exD1 disj_exD2 disj_assoc disj_comm disj_FalseD1 disj_FalseD2 TruepropI
ext_cong_neq COMBI_def COMBK_def COMBB_def COMBC_def COMBS_def abs_I abs_K
- abs_B abs_C abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I skolem_COMBK_D
-
+ abs_B abs_C abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I
end
--- a/src/HOL/Tools/Meson/meson_clausify.ML Thu Oct 28 20:05:18 2021 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu Oct 28 20:06:29 2021 +0200
@@ -366,9 +366,9 @@
th ctxt1
val (cnf_ths, ctxt2) = clausify nnf_th
fun intr_imp ct th =
- Thm.instantiate
- (TVars.empty, Vars.make [(\<^var>\<open>?i::nat\<close>, Thm.cterm_of ctxt2 (HOLogic.mk_nat ax_no))])
- (zero_var_indexes @{thm skolem_COMBK_D})
+ \<^instantiate>\<open>i = \<open>Thm.cterm_of ctxt2 (HOLogic.mk_nat ax_no)\<close> in
+ lemma (schematic) \<open>skolem (COMBK P i) \<Longrightarrow> P\<close> for i :: nat
+ by (rule iffD2 [OF skolem_COMBK_iff])\<close>
RS Thm.implies_intr ct th
in
(opt |> Option.map (I #>> singleton (Variable.export ctxt2 ctxt0)
--- a/src/HOL/Tools/hologic.ML Thu Oct 28 20:05:18 2021 +0200
+++ b/src/HOL/Tools/hologic.ML Thu Oct 28 20:06:29 2021 +0200
@@ -205,16 +205,17 @@
let
val (P, Q) = apply2 (Object_Logic.dest_judgment ctxt o Thm.cprop_of) (thP, thQ)
handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
- val inst = (TVars.empty, Vars.make [(\<^var>\<open>?P::bool\<close>, P), (\<^var>\<open>?Q::bool\<close>, Q)]);
- in Drule.implies_elim_list (Thm.instantiate inst @{thm conjI}) [thP, thQ] end;
+ val rule = \<^instantiate>\<open>P and Q in lemma (open) \<open>P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q\<close> by (rule conjI)\<close>
+ in Drule.implies_elim_list rule [thP, thQ] end;
fun conj_elim ctxt thPQ =
let
val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment ctxt (Thm.cprop_of thPQ))
handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
- val inst = (TVars.empty, Vars.make [(\<^var>\<open>?P::bool\<close>, P), (\<^var>\<open>?Q::bool\<close>, Q)]);
- val thP = Thm.implies_elim (Thm.instantiate inst @{thm conjunct1}) thPQ;
- val thQ = Thm.implies_elim (Thm.instantiate inst @{thm conjunct2}) thPQ;
+ val thP =
+ Thm.implies_elim \<^instantiate>\<open>P and Q in lemma (open) \<open>P \<and> Q \<Longrightarrow> P\<close> by (rule conjunct1)\<close> thPQ;
+ val thQ =
+ Thm.implies_elim \<^instantiate>\<open>P and Q in lemma (open) \<open>P \<and> Q \<Longrightarrow> Q\<close> by (rule conjunct2)\<close> thPQ;
in (thP, thQ) end;
fun conj_elims ctxt th =
--- a/src/HOL/Tools/record.ML Thu Oct 28 20:05:18 2021 +0200
+++ b/src/HOL/Tools/record.ML Thu Oct 28 20:06:29 2021 +0200
@@ -1752,9 +1752,8 @@
rewrite_rule ctxt
[Axclass.unoverload ctxt (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
fun mk_eq_refl ctxt =
- @{thm equal_refl}
- |> Thm.instantiate
- (TVars.make [(\<^tvar>\<open>?'a::equal\<close>, Thm.ctyp_of ctxt (Logic.varifyT_global extT))], Vars.empty)
+ \<^instantiate>\<open>'a = \<open>Thm.ctyp_of ctxt (Logic.varifyT_global extT)\<close> in
+ lemma (schematic) \<open>equal_class.equal x x \<longleftrightarrow> True\<close> by (rule equal_refl)\<close>
|> Axclass.unoverload ctxt;
val ensure_random_record = ensure_sort_record (\<^sort>\<open>random\<close>, mk_random_eq);
val ensure_exhaustive_record =
--- a/src/HOL/Tools/sat.ML Thu Oct 28 20:05:18 2021 +0200
+++ b/src/HOL/Tools/sat.ML Thu Oct 28 20:06:29 2021 +0200
@@ -70,9 +70,6 @@
val counter = Unsynchronized.ref 0;
-val resolution_thm =
- @{lemma "(P \<Longrightarrow> False) \<Longrightarrow> (\<not> P \<Longrightarrow> False) \<Longrightarrow> False" by (rule case_split)}
-
(* ------------------------------------------------------------------------- *)
(* lit_ord: an order on integers that considers their absolute values only, *)
(* thereby treating integers that represent the same atom (positively *)
@@ -166,12 +163,13 @@
val c1' = Thm.implies_intr hyp1 c1 (* Gamma1 |- hyp1 ==> False *)
val c2' = Thm.implies_intr hyp2 c2 (* Gamma2 |- hyp2 ==> False *)
- val res_thm = (* |- (lit ==> False) ==> (~lit ==> False) ==> False *)
+ val res_thm =
let
- val cLit =
+ val P =
snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1)) (* strip Trueprop *)
in
- Thm.instantiate (TVars.empty, Vars.make [(\<^var>\<open>?P::bool\<close>, cLit)]) resolution_thm
+ \<^instantiate>\<open>P in
+ lemma \<open>(P \<Longrightarrow> False) \<Longrightarrow> (\<not> P \<Longrightarrow> False) \<Longrightarrow> False\<close> by (rule case_split)\<close>
end
val _ =