--- a/src/HOL/Tools/Argo/argo_tactic.ML Sun Oct 31 23:15:46 2021 +0100
+++ b/src/HOL/Tools/Argo/argo_tactic.ML Sun Oct 31 23:41:07 2021 +0100
@@ -302,9 +302,6 @@
let val cprop = as_prop ct
in Thm.implies_intr cprop (f (Thm.assume cprop)) end
-fun instantiate cv ct =
- Thm.instantiate (TVars.empty, Vars.make [(Term.dest_Var (Thm.term_of cv), ct)])
-
(* proof replay for tautologies *)
@@ -517,8 +514,6 @@
(* proof replay for unit resolution *)
-val unit_rule = @{lemma "(P \<Longrightarrow> False) \<Longrightarrow> (\<not>P \<Longrightarrow> False) \<Longrightarrow> False" by fast}
-val unit_rule_var = Thm.dest_arg (Thm.dest_arg1 (Thm.cprem_of unit_rule 1))
val bogus_ct = \<^cterm>\<open>True\<close>
fun replay_unit_res lit (pthm, plits) (nthm, nlits) =
@@ -527,8 +522,8 @@
val nlit = the (AList.lookup (op =) nlits (~lit))
val prune = Ord_List.remove lit_ord (lit, bogus_ct)
in
- unit_rule
- |> instantiate unit_rule_var (Thm.dest_arg plit)
+ \<^instantiate>\<open>P = \<open>Thm.dest_arg plit\<close> in
+ lemma "(P \<Longrightarrow> False) \<Longrightarrow> (\<not>P \<Longrightarrow> False) \<Longrightarrow> False" by fast\<close>
|> Thm.elim_implies (Thm.implies_intr plit pthm)
|> Thm.elim_implies (Thm.implies_intr nlit nthm)
|> rpair (Ord_List.union lit_ord (prune nlits) (prune plits))
@@ -553,10 +548,8 @@
(* proof replay for reflexivity *)
-val refl_rule = @{thm refl}
-val refl_rule_var = Thm.dest_arg1 (Thm.dest_arg (Thm.cprop_of refl_rule))
-
-fun replay_refl ct = Thm.instantiate (Thm.match (refl_rule_var, ct)) refl_rule
+fun replay_refl x =
+ \<^instantiate>\<open>'a = \<open>Thm.ctyp_of_cterm x\<close> and x in lemma \<open>x = x\<close> by (rule refl)\<close>
(* proof replay for symmetry *)
@@ -663,13 +656,15 @@
(* normalizing goals *)
+fun instantiate v ct = Thm.instantiate (TVars.empty, Vars.make [(v, ct)])
+
fun instantiate_elim_rule thm =
- let val ct = Drule.strip_imp_concl (Thm.cprop_of thm)
+ let
+ val ct = Drule.strip_imp_concl (Thm.cprop_of thm)
in
(case Thm.term_of ct of
- \<^Const_>\<open>Trueprop for \<open>Var (_, \<^Type>\<open>bool\<close>)\<close>\<close> =>
- instantiate (Thm.dest_arg ct) \<^cterm>\<open>False\<close> thm
- | Var _ => instantiate ct \<^cprop>\<open>False\<close> thm
+ \<^Const_>\<open>Trueprop for \<open>Var (v as (_, \<^Type>\<open>bool\<close>))\<close>\<close> => instantiate v \<^cterm>\<open>False\<close> thm
+ | Var v => instantiate v \<^cprop>\<open>False\<close> thm
| _ => thm)
end