--- a/src/HOL/Tools/SMT/conj_disj_perm.ML Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/conj_disj_perm.ML Tue Sep 28 22:14:02 2021 +0200
@@ -25,9 +25,9 @@
fun explode_thm thm =
(case HOLogic.dest_Trueprop (Thm.prop_of thm) of
- \<^const>\<open>HOL.conj\<close> $ _ $ _ => explode_conj_thm @{thm conjunct1} @{thm conjunct2} thm
- | \<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.disj\<close> $ _ $ _) => explode_conj_thm ndisj1_rule ndisj2_rule thm
- | \<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.Not\<close> $ _) => explode_thm (thm RS @{thm notnotD})
+ \<^Const_>\<open>conj for _ _\<close> => explode_conj_thm @{thm conjunct1} @{thm conjunct2} thm
+ | \<^Const_>\<open>Not for \<^Const_>\<open>disj for _ _\<close>\<close> => explode_conj_thm ndisj1_rule ndisj2_rule thm
+ | \<^Const_>\<open>Not for \<^Const_>\<open>Not for _\<close>\<close> => explode_thm (thm RS @{thm notnotD})
| _ => add_lit thm)
and explode_conj_thm rule1 rule2 thm lits =
@@ -36,7 +36,7 @@
val not_false_rule = @{lemma "\<not>False" by auto}
fun explode thm = explode_thm thm (add_lit not_false_rule (add_lit @{thm TrueI} Termtab.empty))
-fun find_dual_lit lits (\<^const>\<open>HOL.Not\<close> $ t, thm) = Termtab.lookup lits t |> Option.map (pair thm)
+fun find_dual_lit lits (\<^Const_>\<open>Not for t\<close>, thm) = Termtab.lookup lits t |> Option.map (pair thm)
| find_dual_lit _ _ = NONE
fun find_dual_lits lits = Termtab.get_first (find_dual_lit lits) lits
@@ -49,10 +49,10 @@
SOME thm => thm
| NONE => join_term lits t)
-and join_term lits (\<^const>\<open>HOL.conj\<close> $ t $ u) = @{thm conjI} OF (map (join lits) [t, u])
- | join_term lits (\<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.disj\<close> $ t $ u)) =
+and join_term lits \<^Const_>\<open>conj for t u\<close> = @{thm conjI} OF (map (join lits) [t, u])
+ | join_term lits \<^Const_>\<open>Not for \<^Const_>\<open>HOL.disj for t u\<close>\<close> =
ndisj_rule OF (map (join lits o HOLogic.mk_not) [t, u])
- | join_term lits (\<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.Not\<close> $ t)) = join lits t RS not_not_rule
+ | join_term lits \<^Const_>\<open>Not for \<^Const>\<open>Not for t\<close>\<close> = join lits t RS not_not_rule
| join_term _ t = raise TERM ("join_term", [t])
fun prove_conj_disj_imp ct cu = with_assumption ct (fn thm => join (explode thm) (Thm.term_of cu))
@@ -68,19 +68,19 @@
fun prove_any_imp ct =
(case Thm.term_of ct of
- \<^const>\<open>HOL.False\<close> => @{thm FalseE}
- | \<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.Not\<close> $ \<^const>\<open>HOL.False\<close>) => not_not_false_rule
- | \<^const>\<open>HOL.Not\<close> $ \<^const>\<open>HOL.True\<close> => not_true_rule
+ \<^Const_>\<open>False\<close> => @{thm FalseE}
+ | \<^Const_>\<open>Not for \<^Const>\<open>Not for \<^Const>\<open>False\<close>\<close>\<close> => not_not_false_rule
+ | \<^Const_>\<open>Not for \<^Const>\<open>True\<close>\<close> => not_true_rule
| _ => raise CTERM ("prove_any_imp", [ct]))
fun prove_contradiction_imp ct =
with_assumption ct (fn thm =>
let val lits = explode thm
in
- (case Termtab.lookup lits \<^const>\<open>HOL.False\<close> of
+ (case Termtab.lookup lits \<^Const>\<open>False\<close> of
SOME thm' => thm' RS @{thm FalseE}
| NONE =>
- (case Termtab.lookup lits (\<^const>\<open>HOL.Not\<close> $ \<^const>\<open>HOL.True\<close>) of
+ (case Termtab.lookup lits \<^Const>\<open>Not for \<^Const>\<open>True\<close>\<close> of
SOME thm' => thm' RS not_true_rule
| NONE =>
(case find_dual_lits lits of
@@ -99,13 +99,13 @@
datatype kind = True | False | Conj | Disj | Other
-fun choose t _ _ _ \<^const>\<open>HOL.True\<close> = t
- | choose _ f _ _ \<^const>\<open>HOL.False\<close> = f
- | choose _ _ c _ (\<^const>\<open>HOL.conj\<close> $ _ $ _) = c
- | choose _ _ _ d (\<^const>\<open>HOL.disj\<close> $ _ $ _) = d
+fun choose t _ _ _ \<^Const_>\<open>True\<close> = t
+ | choose _ f _ _ \<^Const_>\<open>False\<close> = f
+ | choose _ _ c _ \<^Const_>\<open>conj for _ _\<close> = c
+ | choose _ _ _ d \<^Const_>\<open>disj for _ _\<close> = d
| choose _ _ _ _ _ = Other
-fun kind_of (\<^const>\<open>HOL.Not\<close> $ t) = choose False True Disj Conj t
+fun kind_of \<^Const_>\<open>Not for t\<close> = choose False True Disj Conj t
| kind_of t = choose True False Conj Disj t
fun prove_conj_disj_perm ct cp =
@@ -120,7 +120,7 @@
fun conj_disj_perm_tac ctxt = CSUBGOAL (fn (ct, i) =>
(case Thm.term_of ct of
- \<^const>\<open>HOL.Trueprop\<close> $ (@{const HOL.eq(bool)} $ _ $ _) =>
+ \<^Const_>\<open>Trueprop for \<^Const>\<open>HOL.eq \<^Type>\<open>bool\<close> for _ _\<close>\<close> =>
resolve_tac ctxt [prove_conj_disj_perm ct (Thm.dest_binop (Thm.dest_arg ct))] i
| _ => no_tac))
--- a/src/HOL/Tools/SMT/smt_normalize.ML Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Tue Sep 28 22:14:02 2021 +0200
@@ -31,7 +31,7 @@
(** instantiate elimination rules **)
local
- val (cpfalse, cfalse) = `SMT_Util.mk_cprop (Thm.cterm_of \<^context> \<^const>\<open>False\<close>)
+ val (cpfalse, cfalse) = `SMT_Util.mk_cprop \<^cterm>\<open>False\<close>
fun inst f ct thm =
let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
@@ -40,7 +40,7 @@
fun instantiate_elim thm =
(case Thm.concl_of thm of
- \<^const>\<open>Trueprop\<close> $ Var (_, \<^typ>\<open>bool\<close>) => inst Thm.dest_arg cfalse thm
+ \<^Const_>\<open>Trueprop for \<open>Var (_, \<^Type>\<open>bool\<close>)\<close>\<close> => inst Thm.dest_arg cfalse thm
| Var _ => inst I cpfalse thm
| _ => thm)
@@ -51,9 +51,8 @@
fun norm_def thm =
(case Thm.prop_of thm of
- \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ Abs _) =>
- norm_def (thm RS @{thm fun_cong})
- | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ Abs _ => norm_def (HOLogic.mk_obj_eq thm)
+ \<^Const_>\<open>Trueprop for \<^Const>\<open>HOL.eq _ for _ \<open>Abs _\<close>\<close>\<close> => norm_def (thm RS @{thm fun_cong})
+ | \<^Const_>\<open>Pure.eq _ for _ \<open>Abs _\<close>\<close> => norm_def (HOLogic.mk_obj_eq thm)
| _ => thm)
@@ -61,11 +60,11 @@
fun atomize_conv ctxt ct =
(case Thm.term_of ct of
- \<^const>\<open>Pure.imp\<close> $ _ $ _ =>
+ \<^Const_>\<open>Pure.imp for _ _\<close> =>
Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_imp}
- | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _ =>
+ | \<^Const_>\<open>Pure.eq _ for _ _\<close> =>
Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_eq}
- | Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs _ =>
+ | \<^Const_>\<open>Pure.all _ for \<open>Abs _\<close>\<close> =>
Conv.binder_conv (atomize_conv o snd) ctxt then_conv Conv.rewr_conv @{thm atomize_all}
| _ => Conv.all_conv) ct
handle CTERM _ => Conv.all_conv ct
@@ -120,9 +119,9 @@
fun proper_quant inside f t =
(case t of
- Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, u) => proper_quant true f u
- | Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, u) => proper_quant true f u
- | \<^const>\<open>trigger\<close> $ p $ u =>
+ \<^Const_>\<open>All _ for \<open>Abs (_, _, u)\<close>\<close> => proper_quant true f u
+ | \<^Const_>\<open>Ex _ for \<open>Abs (_, _, u)\<close>\<close> => proper_quant true f u
+ | \<^Const_>\<open>trigger for p u\<close> =>
(if inside then f p else false) andalso proper_quant false f u
| Abs (_, _, u) => proper_quant false f u
| u1 $ u2 => proper_quant false f u1 andalso proper_quant false f u2
@@ -142,7 +141,7 @@
fun dest_cond_eq ct =
(case Thm.term_of ct of
Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _ => Thm.dest_binop ct
- | \<^const>\<open>HOL.implies\<close> $ _ $ _ => dest_cond_eq (Thm.dest_arg ct)
+ | \<^Const_>\<open>implies for _ _\<close> => dest_cond_eq (Thm.dest_arg ct)
| _ => raise CTERM ("no equation", [ct]))
fun get_constrs thy (Type (n, _)) = these (BNF_LFP_Compat.get_constrs thy n)
@@ -220,7 +219,7 @@
in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end
- fun has_trigger (\<^const>\<open>trigger\<close> $ _ $ _) = true
+ fun has_trigger \<^Const_>\<open>trigger for _ _\<close> = true
| has_trigger _ = false
fun try_trigger_conv cv ct =
@@ -331,12 +330,12 @@
local
val simple_nat_ops = [
- @{const HOL.eq (nat)}, @{const less (nat)}, @{const less_eq (nat)},
- \<^const>\<open>Suc\<close>, @{const plus (nat)}, @{const minus (nat)}]
+ \<^Const>\<open>HOL.eq \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>less \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>less_eq \<^Type>\<open>nat\<close>\<close>,
+ \<^Const>\<open>Suc\<close>, \<^Const>\<open>plus \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>minus \<^Type>\<open>nat\<close>\<close>]
val nat_consts = simple_nat_ops @
- [@{const numeral (nat)}, @{const zero_class.zero (nat)}, @{const one_class.one (nat)}] @
- [@{const times (nat)}, @{const divide (nat)}, @{const modulo (nat)}]
+ [\<^Const>\<open>numeral \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>zero_class.zero \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>one_class.one \<^Type>\<open>nat\<close>\<close>] @
+ [\<^Const>\<open>times \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>divide \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>modulo \<^Type>\<open>nat\<close>\<close>]
val is_nat_const = member (op aconv) nat_consts
@@ -349,10 +348,10 @@
fun int_ops_conv cv ctxt ct =
(case Thm.term_of ct of
- @{const of_nat (int)} $ (Const (\<^const_name>\<open>If\<close>, _) $ _ $ _ $ _) =>
+ \<^Const_>\<open>of_nat \<^Type>\<open>int\<close> for \<open>\<^Const_>\<open>If _ for _ _ _\<close>\<close>\<close> =>
Conv.rewr_conv int_if_thm then_conv
if_conv (cv ctxt) (int_ops_conv cv ctxt)
- | @{const of_nat (int)} $ _ =>
+ | \<^Const>\<open>of_nat \<^Type>\<open>int\<close> for _\<close> =>
(Conv.rewrs_conv int_ops_thms then_conv
Conv.top_sweep_conv (int_ops_conv cv) ctxt) else_conv
Conv.arg_conv (Conv.sub_conv cv ctxt)
@@ -372,7 +371,7 @@
fun add_int_of_nat vs ct cu (q, cts) =
(case Thm.term_of ct of
- @{const of_nat(int)} =>
+ \<^Const>\<open>of_nat \<^Type>\<open>int\<close>\<close> =>
if Term.exists_subterm (member (op aconv) vs) (Thm.term_of cu) then (true, cts)
else (q, insert (op aconvc) cu cts)
| _ => (q, cts))
@@ -490,7 +489,7 @@
val schematic_consts_of =
let
- fun collect (\<^const>\<open>trigger\<close> $ p $ t) = collect_trigger p #> collect t
+ fun collect \<^Const_>\<open>trigger for p t\<close> = collect_trigger p #> collect t
| collect (t $ u) = collect t #> collect u
| collect (Abs (_, _, t)) = collect t
| collect (t as Const (n, _)) =
--- a/src/HOL/Tools/SMT/smt_real.ML Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_real.ML Tue Sep 28 22:14:02 2021 +0200
@@ -25,7 +25,7 @@
| is_linear [t, u] = SMT_Util.is_number t orelse SMT_Util.is_number u
| is_linear _ = false
- fun mk_times ts = Term.list_comb (@{const times (real)}, ts)
+ fun mk_times ts = Term.list_comb (\<^Const>\<open>times \<^Type>\<open>real\<close>\<close>, ts)
fun times _ _ ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE
in
@@ -34,17 +34,17 @@
SMT_Builtin.add_builtin_typ SMTLIB_Interface.smtlibC
(\<^typ>\<open>real\<close>, K (SOME ("Real", [])), real_num) #>
fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [
- (@{const less (real)}, "<"),
- (@{const less_eq (real)}, "<="),
- (@{const uminus (real)}, "-"),
- (@{const plus (real)}, "+"),
- (@{const minus (real)}, "-") ] #>
+ (\<^Const>\<open>less \<^Type>\<open>real\<close>\<close>, "<"),
+ (\<^Const>\<open>less_eq \<^Type>\<open>real\<close>\<close>, "<="),
+ (\<^Const>\<open>uminus \<^Type>\<open>real\<close>\<close>, "-"),
+ (\<^Const>\<open>plus \<^Type>\<open>real\<close>\<close>, "+"),
+ (\<^Const>\<open>minus \<^Type>\<open>real\<close>\<close>, "-") ] #>
SMT_Builtin.add_builtin_fun SMTLIB_Interface.smtlibC
- (Term.dest_Const @{const times (real)}, times) #>
+ (Term.dest_Const \<^Const>\<open>times \<^Type>\<open>real\<close>\<close>, times) #>
SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C
- (@{const times (real)}, "*") #>
+ (\<^Const>\<open>times \<^Type>\<open>real\<close>\<close>, "*") #>
SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C
- (@{const divide (real)}, "/")
+ (\<^Const>\<open>divide \<^Type>\<open>real\<close>\<close>, "/")
end
@@ -64,14 +64,14 @@
fun mk_nary _ cu [] = cu
| mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
- val mk_uminus = Thm.apply (Thm.cterm_of \<^context> @{const uminus (real)})
- val add = Thm.cterm_of \<^context> @{const plus (real)}
+ val mk_uminus = Thm.apply \<^cterm>\<open>uminus :: real \<Rightarrow> _\<close>
+ val add = \<^cterm>\<open>(+) :: real \<Rightarrow> _\<close>
val real0 = Numeral.mk_cnumber \<^ctyp>\<open>real\<close> 0
- val mk_sub = Thm.mk_binop (Thm.cterm_of \<^context> @{const minus (real)})
- val mk_mul = Thm.mk_binop (Thm.cterm_of \<^context> @{const times (real)})
- val mk_div = Thm.mk_binop (Thm.cterm_of \<^context> @{const divide (real)})
- val mk_lt = Thm.mk_binop (Thm.cterm_of \<^context> @{const less (real)})
- val mk_le = Thm.mk_binop (Thm.cterm_of \<^context> @{const less_eq (real)})
+ val mk_sub = Thm.mk_binop \<^cterm>\<open>(-) :: real \<Rightarrow> _\<close>
+ val mk_mul = Thm.mk_binop \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close>
+ val mk_div = Thm.mk_binop \<^cterm>\<open>(/) :: real \<Rightarrow> _\<close>
+ val mk_lt = Thm.mk_binop \<^cterm>\<open>(<) :: real \<Rightarrow> _\<close>
+ val mk_le = Thm.mk_binop \<^cterm>\<open>(\<le>) :: real \<Rightarrow> _\<close>
fun z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
| z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) cts = SOME (mk_nary add real0 cts)
--- a/src/HOL/Tools/SMT/smt_replay_methods.ML Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_replay_methods.ML Tue Sep 28 22:14:02 2021 +0200
@@ -218,30 +218,30 @@
fun abstract_ter abs f t t1 t2 t3 =
abstract_sub t (abs t1 ##>> abs t2 ##>> abs t3 #>> (Scan.triple1 #> f))
-fun abstract_lit (\<^const>\<open>HOL.Not\<close> $ t) = abstract_term t #>> HOLogic.mk_not
+fun abstract_lit \<^Const>\<open>Not for t\<close> = abstract_term t #>> HOLogic.mk_not
| abstract_lit t = abstract_term t
-fun abstract_not abs (t as \<^const>\<open>HOL.Not\<close> $ t1) =
+fun abstract_not abs (t as \<^Const_>\<open>Not\<close> $ t1) =
abstract_sub t (abs t1 #>> HOLogic.mk_not)
| abstract_not _ t = abstract_lit t
-fun abstract_conj (t as \<^const>\<open>HOL.conj\<close> $ t1 $ t2) =
+fun abstract_conj (t as \<^Const_>\<open>conj\<close> $ t1 $ t2) =
abstract_bin abstract_conj HOLogic.mk_conj t t1 t2
| abstract_conj t = abstract_lit t
-fun abstract_disj (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
+fun abstract_disj (t as \<^Const_>\<open>disj\<close> $ t1 $ t2) =
abstract_bin abstract_disj HOLogic.mk_disj t t1 t2
| abstract_disj t = abstract_lit t
-fun abstract_prop (t as (c as @{const If (bool)}) $ t1 $ t2 $ t3) =
+fun abstract_prop (t as (c as \<^Const>\<open>If \<^Type>\<open>bool\<close>\<close>) $ t1 $ t2 $ t3) =
abstract_ter abstract_prop (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3
- | abstract_prop (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
+ | abstract_prop (t as \<^Const_>\<open>disj\<close> $ t1 $ t2) =
abstract_bin abstract_prop HOLogic.mk_disj t t1 t2
- | abstract_prop (t as \<^const>\<open>HOL.conj\<close> $ t1 $ t2) =
+ | abstract_prop (t as \<^Const_>\<open>conj\<close> $ t1 $ t2) =
abstract_bin abstract_prop HOLogic.mk_conj t t1 t2
- | abstract_prop (t as \<^const>\<open>HOL.implies\<close> $ t1 $ t2) =
+ | abstract_prop (t as \<^Const_>\<open>implies\<close> $ t1 $ t2) =
abstract_bin abstract_prop HOLogic.mk_imp t t1 t2
- | abstract_prop (t as \<^term>\<open>HOL.eq :: bool => _\<close> $ t1 $ t2) =
+ | abstract_prop (t as \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close>\<close> $ t1 $ t2) =
abstract_bin abstract_prop HOLogic.mk_eq t t1 t2
| abstract_prop t = abstract_not abstract_prop t
@@ -253,8 +253,8 @@
abstract_sub t (abs t' #>> (fn u' => c $ Abs (s, T, u')))
| abs (t as (c as Const (\<^const_name>\<open>If\<close>, _)) $ t1 $ t2 $ t3) =
abstract_ter abs (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3
- | abs (t as \<^const>\<open>HOL.Not\<close> $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
- | abs (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
+ | abs (t as \<^Const_>\<open>Not\<close> $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
+ | abs (t as \<^Const_>\<open>disj\<close> $ t1 $ t2) =
abstract_sub t (abs t1 ##>> abs t2 #>> HOLogic.mk_disj)
| abs (t as (c as Const (\<^const_name>\<open>uminus_class.uminus\<close>, _)) $ t1) =
abstract_sub t (abs t1 #>> (fn u => c $ u))
@@ -282,10 +282,10 @@
| (NONE, _) => abstract_term t cx))
in abs u end
-fun abstract_unit (t as (\<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.disj\<close> $ t1 $ t2))) =
+fun abstract_unit (t as \<^Const_>\<open>Not for \<^Const_>\<open>disj for t1 t2\<close>\<close>) =
abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
HOLogic.mk_not o HOLogic.mk_disj)
- | abstract_unit (t as (\<^const>\<open>HOL.disj\<close> $ t1 $ t2)) =
+ | abstract_unit (t as \<^Const_>\<open>disj for t1 t2\<close>) =
abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
HOLogic.mk_disj)
| abstract_unit (t as (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2)) =
@@ -293,49 +293,49 @@
abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
HOLogic.mk_eq)
else abstract_lit t
- | abstract_unit (t as (\<^const>\<open>HOL.Not\<close> $ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2))) =
+ | abstract_unit (t as \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq _ for t1 t2\<close>\<close>) =
if fastype_of t1 = \<^typ>\<open>bool\<close> then
abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
HOLogic.mk_eq #>> HOLogic.mk_not)
else abstract_lit t
- | abstract_unit (t as (\<^const>\<open>HOL.Not\<close> $ t1)) =
+ | abstract_unit (t as \<^Const>\<open>Not for t1\<close>) =
abstract_sub t (abstract_unit t1 #>> HOLogic.mk_not)
| abstract_unit t = abstract_lit t
-fun abstract_bool (t as (@{const HOL.disj} $ t1 $ t2)) =
+fun abstract_bool (t as \<^Const_>\<open>disj for t1 t2\<close>) =
abstract_sub t (abstract_bool t1 ##>> abstract_bool t2 #>>
HOLogic.mk_disj)
- | abstract_bool (t as (@{const HOL.conj} $ t1 $ t2)) =
+ | abstract_bool (t as \<^Const_>\<open>conj for t1 t2\<close>) =
abstract_sub t (abstract_bool t1 ##>> abstract_bool t2 #>>
HOLogic.mk_conj)
- | abstract_bool (t as (Const(@{const_name HOL.eq}, _) $ t1 $ t2)) =
+ | abstract_bool (t as \<^Const_>\<open>HOL.eq _ for t1 t2\<close>) =
if fastype_of t1 = @{typ bool} then
abstract_sub t (abstract_bool t1 ##>> abstract_bool t2 #>>
HOLogic.mk_eq)
else abstract_lit t
- | abstract_bool (t as (@{const HOL.Not} $ t1)) =
+ | abstract_bool (t as \<^Const_>\<open>Not for t1\<close>) =
abstract_sub t (abstract_bool t1 #>> HOLogic.mk_not)
- | abstract_bool (t as (@{const HOL.implies} $ t1 $ t2)) =
+ | abstract_bool (t as \<^Const>\<open>implies for t1 t2\<close>) =
abstract_sub t (abstract_bool t1 ##>> abstract_bool t2 #>>
HOLogic.mk_imp)
| abstract_bool t = abstract_lit t
-fun abstract_bool_shallow (t as (@{const HOL.disj} $ t1 $ t2)) =
+fun abstract_bool_shallow (t as \<^Const_>\<open>disj for t1 t2\<close>) =
abstract_sub t (abstract_bool_shallow t1 ##>> abstract_bool_shallow t2 #>>
HOLogic.mk_disj)
- | abstract_bool_shallow (t as (@{const HOL.Not} $ t1)) =
+ | abstract_bool_shallow (t as \<^Const_>\<open>Not for t1\<close>) =
abstract_sub t (abstract_bool_shallow t1 #>> HOLogic.mk_not)
| abstract_bool_shallow t = abstract_term t
-fun abstract_bool_shallow_equivalence (t as (@{const HOL.disj} $ t1 $ t2)) =
+fun abstract_bool_shallow_equivalence (t as \<^Const_>\<open>disj for t1 t2\<close>) =
abstract_sub t (abstract_bool_shallow_equivalence t1 ##>> abstract_bool_shallow_equivalence t2 #>>
HOLogic.mk_disj)
- | abstract_bool_shallow_equivalence (t as (Const(@{const_name HOL.eq}, _) $ t1 $ t2)) =
- if fastype_of t1 = @{typ bool} then
+ | abstract_bool_shallow_equivalence (t as \<^Const_>\<open>HOL.eq _ for t1 t2\<close>) =
+ if fastype_of t1 = \<^Type>\<open>bool\<close> then
abstract_sub t (abstract_lit t1 ##>> abstract_lit t2 #>>
HOLogic.mk_eq)
else abstract_lit t
- | abstract_bool_shallow_equivalence (t as (@{const HOL.Not} $ t1)) =
+ | abstract_bool_shallow_equivalence (t as \<^Const_>\<open>Not for t1\<close>) =
abstract_sub t (abstract_bool_shallow_equivalence t1 #>> HOLogic.mk_not)
| abstract_bool_shallow_equivalence t = abstract_lit t
@@ -347,8 +347,8 @@
abstract_sub t (abs t' #>> (fn u' => c $ Abs (s, T, u')))
| abs (t as (Const (\<^const_name>\<open>If\<close>, _)) $ _ $ _ $ _) =
abstract_sub t (abstract_term t)
- | abs (t as \<^const>\<open>HOL.Not\<close> $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
- | abs (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
+ | abs (t as \<^Const>\<open>Not\<close> $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
+ | abs (t as \<^Const>\<open>disj\<close> $ t1 $ t2) =
abstract_sub t (abs t1 ##>> abs t2 #>> HOLogic.mk_disj)
| abs (t as (c as Const (\<^const_name>\<open>uminus_class.uminus\<close>, _)) $ t1) =
abstract_sub t (abs t1 #>> (fn u => c $ u))
--- a/src/HOL/Tools/SMT/smt_translate.ML Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML Tue Sep 28 22:14:02 2021 +0200
@@ -306,12 +306,12 @@
| (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts)
| (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts
| (u, ts) => traverses Ts u ts)
- and in_trigger Ts ((c as \<^const>\<open>trigger\<close>) $ p $ t) = c $ in_pats Ts p $ traverse Ts t
+ and in_trigger Ts ((c as \<^Const_>\<open>trigger\<close>) $ p $ t) = c $ in_pats Ts p $ traverse Ts t
| in_trigger Ts t = traverse Ts t
and in_pats Ts ps =
in_list \<^typ>\<open>pattern symb_list\<close> (in_list \<^typ>\<open>pattern\<close> (in_pat Ts)) ps
- and in_pat Ts ((p as Const (\<^const_name>\<open>pat\<close>, _)) $ t) = p $ traverse Ts t
- | in_pat Ts ((p as Const (\<^const_name>\<open>nopat\<close>, _)) $ t) = p $ traverse Ts t
+ and in_pat Ts ((p as \<^Const_>\<open>pat _\<close>) $ t) = p $ traverse Ts t
+ | in_pat Ts ((p as \<^Const_>\<open>nopat _\<close>) $ t) = p $ traverse Ts t
| in_pat _ t = raise TERM ("bad pattern", [t])
and traverses Ts t ts = Term.list_comb (t, map (traverse Ts) ts)
in map (traverse []) ts end
@@ -343,9 +343,9 @@
fun in_term pat t =
(case Term.strip_comb t of
- (\<^const>\<open>True\<close>, []) => t
- | (\<^const>\<open>False\<close>, []) => t
- | (u as Const (\<^const_name>\<open>If\<close>, _), [t1, t2, t3]) =>
+ (\<^Const_>\<open>True\<close>, []) => t
+ | (\<^Const_>\<open>False\<close>, []) => t
+ | (u as \<^Const_>\<open>If _\<close>, [t1, t2, t3]) =>
if pat then raise BAD_PATTERN () else u $ in_form t1 $ in_term pat t2 $ in_term pat t3
| (Const (c as (n, _)), ts) =>
if is_builtin_conn_or_pred ctxt c ts orelse is_quant n then
@@ -364,7 +364,7 @@
and in_pats ps =
in_list \<^typ>\<open>pattern symb_list\<close> (SOME o in_list \<^typ>\<open>pattern\<close> (try in_pat)) ps
- and in_trigger ((c as \<^const>\<open>trigger\<close>) $ p $ t) = c $ in_pats p $ in_form t
+ and in_trigger ((c as \<^Const_>\<open>trigger\<close>) $ p $ t) = c $ in_pats p $ in_form t
| in_trigger t = in_form t
and in_form t =
@@ -412,7 +412,7 @@
| (ps, [false]) => cons (SNoPat ps)
| _ => raise TERM ("bad multi-pattern", ts))
-fun dest_trigger (\<^const>\<open>trigger\<close> $ tl $ t) =
+fun dest_trigger \<^Const_>\<open>trigger for tl t\<close> =
(rev (fold (dest_pats o SMT_Util.dest_symb_list) (SMT_Util.dest_symb_list tl) []), t)
| dest_trigger t = ([], t)
@@ -511,7 +511,7 @@
|> (fn T => Const (\<^const_name>\<open>pat\<close>, T) $ lhs)
|> SMT_Util.mk_symb_list \<^typ>\<open>pattern\<close> o single
|> SMT_Util.mk_symb_list \<^typ>\<open>pattern symb_list\<close> o single
- |> (fn t => \<^const>\<open>trigger\<close> $ t $ eq)
+ |> (fn t => \<^Const>\<open>trigger for t eq\<close>)
| mk_trigger t = t
val (ctxt2, (ts3, ll_defs)) =
--- a/src/HOL/Tools/SMT/smt_util.ML Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_util.ML Tue Sep 28 22:14:02 2021 +0200
@@ -131,16 +131,16 @@
(* terms *)
-fun dest_conj (\<^const>\<open>HOL.conj\<close> $ t $ u) = (t, u)
+fun dest_conj \<^Const_>\<open>conj for t u\<close> = (t, u)
| dest_conj t = raise TERM ("not a conjunction", [t])
-fun dest_disj (\<^const>\<open>HOL.disj\<close> $ t $ u) = (t, u)
+fun dest_disj \<^Const_>\<open>disj for t u\<close> = (t, u)
| dest_disj t = raise TERM ("not a disjunction", [t])
fun under_quant f t =
(case t of
- Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, u) => under_quant f u
- | Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, u) => under_quant f u
+ \<^Const_>\<open>All _ for \<open>Abs (_, _, u)\<close>\<close> => under_quant f u
+ | \<^Const_>\<open>Ex _ for \<open>Abs (_, _, u)\<close>\<close> => under_quant f u
| _ => f t)
val is_number =
@@ -197,17 +197,17 @@
val dest_all_cbinders = repeat_yield (try o dest_cbinder)
-val mk_cprop = Thm.apply (Thm.cterm_of \<^context> \<^const>\<open>Trueprop\<close>)
+val mk_cprop = Thm.apply \<^cterm>\<open>Trueprop\<close>
fun dest_cprop ct =
(case Thm.term_of ct of
- \<^const>\<open>Trueprop\<close> $ _ => Thm.dest_arg ct
+ \<^Const_>\<open>Trueprop for _\<close> => Thm.dest_arg ct
| _ => raise CTERM ("not a property", [ct]))
val equals = mk_const_pat \<^theory> \<^const_name>\<open>Pure.eq\<close> Thm.dest_ctyp0
fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
-val dest_prop = (fn \<^const>\<open>Trueprop\<close> $ t => t | t => t)
+val dest_prop = fn \<^Const_>\<open>Trueprop for t\<close> => t | t => t
fun term_of ct = dest_prop (Thm.term_of ct)
fun prop_of thm = dest_prop (Thm.prop_of thm)
@@ -237,7 +237,7 @@
fun prop_conv cv ct =
(case Thm.term_of ct of
- \<^const>\<open>Trueprop\<close> $ _ => Conv.arg_conv cv ct
+ \<^Const_>\<open>Trueprop for _\<close> => Conv.arg_conv cv ct
| _ => raise CTERM ("not a property", [ct]))
end;
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Tue Sep 28 22:14:02 2021 +0200
@@ -35,7 +35,7 @@
| is_linear _ = false
fun times _ _ ts =
- let val mk = Term.list_comb o pair @{const times (int)}
+ let val mk = Term.list_comb o pair \<^Const>\<open>times \<^Type>\<open>int\<close>\<close>
in if is_linear ts then SOME ("*", 2, ts, mk) else NONE end
in
@@ -46,21 +46,21 @@
(\<^typ>\<open>bool\<close>, K (SOME ("Bool", [])), K (K NONE)),
(\<^typ>\<open>int\<close>, K (SOME ("Int", [])), int_num)] #>
fold (SMT_Builtin.add_builtin_fun' smtlibC) [
- (\<^const>\<open>True\<close>, "true"),
- (\<^const>\<open>False\<close>, "false"),
- (\<^const>\<open>Not\<close>, "not"),
- (\<^const>\<open>HOL.conj\<close>, "and"),
- (\<^const>\<open>HOL.disj\<close>, "or"),
- (\<^const>\<open>HOL.implies\<close>, "=>"),
- (@{const HOL.eq ('a)}, "="),
- (@{const If ('a)}, "ite"),
- (@{const less (int)}, "<"),
- (@{const less_eq (int)}, "<="),
- (@{const uminus (int)}, "-"),
- (@{const plus (int)}, "+"),
- (@{const minus (int)}, "-")] #>
+ (\<^Const>\<open>True\<close>, "true"),
+ (\<^Const>\<open>False\<close>, "false"),
+ (\<^Const>\<open>Not\<close>, "not"),
+ (\<^Const>\<open>conj\<close>, "and"),
+ (\<^Const>\<open>disj\<close>, "or"),
+ (\<^Const>\<open>implies\<close>, "=>"),
+ (\<^Const>\<open>HOL.eq \<^typ>\<open>'a\<close>\<close>, "="),
+ (\<^Const>\<open>If \<^typ>\<open>'a\<close>\<close>, "ite"),
+ (\<^Const>\<open>less \<^Type>\<open>int\<close>\<close>, "<"),
+ (\<^Const>\<open>less_eq \<^Type>\<open>int\<close>\<close>, "<="),
+ (\<^Const>\<open>uminus \<^Type>\<open>int\<close>\<close>, "-"),
+ (\<^Const>\<open>plus \<^Type>\<open>int\<close>\<close>, "+"),
+ (\<^Const>\<open>minus \<^Type>\<open>int\<close>\<close>, "-")] #>
SMT_Builtin.add_builtin_fun smtlibC
- (Term.dest_Const @{const times (int)}, times)
+ (Term.dest_Const \<^Const>\<open>times \<^Type>\<open>int\<close>\<close>, times)
end
--- a/src/HOL/Tools/SMT/smtlib_proof.ML Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/smtlib_proof.ML Tue Sep 28 22:14:02 2021 +0200
@@ -150,8 +150,8 @@
fun mk_less t1 t2 = mk_binary_pred \<^const_name>\<open>ord_class.less\<close> \<^sort>\<open>linorder\<close> t1 t2
fun mk_less_eq t1 t2 = mk_binary_pred \<^const_name>\<open>ord_class.less_eq\<close> \<^sort>\<open>linorder\<close> t1 t2
-fun core_term_parser (SMTLIB.Sym "true", _) = SOME \<^const>\<open>HOL.True\<close>
- | core_term_parser (SMTLIB.Sym "false", _) = SOME \<^const>\<open>HOL.False\<close>
+fun core_term_parser (SMTLIB.Sym "true", _) = SOME \<^Const>\<open>True\<close>
+ | core_term_parser (SMTLIB.Sym "false", _) = SOME \<^Const>\<open>False\<close>
| core_term_parser (SMTLIB.Sym "not", [t]) = SOME (HOLogic.mk_not t)
| core_term_parser (SMTLIB.Sym "and", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_conj) t ts)
| core_term_parser (SMTLIB.Sym "or", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_disj) t ts)
--- a/src/HOL/Tools/SMT/verit_proof.ML Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/verit_proof.ML Tue Sep 28 22:14:02 2021 +0200
@@ -738,7 +738,7 @@
fun remove_assumption_id assumption_id prems =
filter_out (curry (op =) assumption_id) prems
fun add_assumption assumption concl =
- \<^const>\<open>Pure.imp\<close> $ mk_prop_of_term assumption $ mk_prop_of_term concl
+ \<^Const>\<open>Pure.imp for \<open>mk_prop_of_term assumption\<close> \<open>mk_prop_of_term concl\<close>\<close>
fun inline_assumption assumption assumption_id
(VeriT_Node {id, rule, prems, proof_ctxt, concl}) =
mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt
--- a/src/HOL/Tools/SMT/z3_interface.ML Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML Tue Sep 28 22:14:02 2021 +0200
@@ -38,8 +38,8 @@
fp_kinds = [BNF_Util.Least_FP],
serialize = #serialize (SMTLIB_Interface.translate_config SMT_Util.First_Order ctxt)}
- fun is_div_mod @{const divide (int)} = true
- | is_div_mod @{const modulo (int)} = true
+ fun is_div_mod \<^Const_>\<open>divide \<^Type>\<open>int\<close>\<close> = true
+ | is_div_mod \<^Const>\<open>modulo \<^Type>\<open>int\<close>\<close> = true
| is_div_mod _ = false
val have_int_div_mod = exists (Term.exists_subterm is_div_mod o Thm.prop_of)
@@ -50,9 +50,9 @@
else (thms, extra_thms)
val setup_builtins =
- SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const times (int)}, "*") #>
- SMT_Builtin.add_builtin_fun' smtlib_z3C (\<^const>\<open>z3div\<close>, "div") #>
- SMT_Builtin.add_builtin_fun' smtlib_z3C (\<^const>\<open>z3mod\<close>, "mod")
+ SMT_Builtin.add_builtin_fun' smtlib_z3C (\<^Const>\<open>times \<^Type>\<open>int\<close>\<close>, "*") #>
+ SMT_Builtin.add_builtin_fun' smtlib_z3C (\<^Const>\<open>z3div\<close>, "div") #>
+ SMT_Builtin.add_builtin_fun' smtlib_z3C (\<^Const>\<open>z3mod\<close>, "mod")
in
val _ = Theory.setup (Context.theory_map (
@@ -116,13 +116,13 @@
| mk_builtin_num ctxt i T =
chained_mk_builtin_num ctxt (get_mk_builtins ctxt) i T
-val mk_true = Thm.cterm_of \<^context> (\<^const>\<open>Not\<close> $ \<^const>\<open>False\<close>)
-val mk_false = Thm.cterm_of \<^context> \<^const>\<open>False\<close>
-val mk_not = Thm.apply (Thm.cterm_of \<^context> \<^const>\<open>Not\<close>)
-val mk_implies = Thm.mk_binop (Thm.cterm_of \<^context> \<^const>\<open>HOL.implies\<close>)
-val mk_iff = Thm.mk_binop (Thm.cterm_of \<^context> @{const HOL.eq (bool)})
-val conj = Thm.cterm_of \<^context> \<^const>\<open>HOL.conj\<close>
-val disj = Thm.cterm_of \<^context> \<^const>\<open>HOL.disj\<close>
+val mk_true = \<^cterm>\<open>\<not> False\<close>
+val mk_false = \<^cterm>\<open>False\<close>
+val mk_not = Thm.apply \<^cterm>\<open>HOL.Not\<close>
+val mk_implies = Thm.mk_binop \<^cterm>\<open>HOL.implies\<close>
+val mk_iff = Thm.mk_binop \<^cterm>\<open>(=) :: bool \<Rightarrow> _\<close>
+val conj = \<^cterm>\<open>HOL.conj\<close>
+val disj = \<^cterm>\<open>HOL.disj\<close>
fun mk_nary _ cu [] = cu
| mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
@@ -143,15 +143,15 @@
let val cTs = Thm.dest_ctyp (Thm.ctyp_of_cterm array)
in Thm.apply (Thm.mk_binop (SMT_Util.instTs cTs update) array index) value end
-val mk_uminus = Thm.apply (Thm.cterm_of \<^context> @{const uminus (int)})
-val add = Thm.cterm_of \<^context> @{const plus (int)}
+val mk_uminus = Thm.apply \<^cterm>\<open>uminus :: int \<Rightarrow> _\<close>
+val add = \<^cterm>\<open>(+) :: int \<Rightarrow> _\<close>
val int0 = Numeral.mk_cnumber \<^ctyp>\<open>int\<close> 0
-val mk_sub = Thm.mk_binop (Thm.cterm_of \<^context> @{const minus (int)})
-val mk_mul = Thm.mk_binop (Thm.cterm_of \<^context> @{const times (int)})
-val mk_div = Thm.mk_binop (Thm.cterm_of \<^context> \<^const>\<open>z3div\<close>)
-val mk_mod = Thm.mk_binop (Thm.cterm_of \<^context> \<^const>\<open>z3mod\<close>)
-val mk_lt = Thm.mk_binop (Thm.cterm_of \<^context> @{const less (int)})
-val mk_le = Thm.mk_binop (Thm.cterm_of \<^context> @{const less_eq (int)})
+val mk_sub = Thm.mk_binop \<^cterm>\<open>(-) :: int \<Rightarrow> _\<close>
+val mk_mul = Thm.mk_binop \<^cterm>\<open>(*) :: int \<Rightarrow> _\<close>
+val mk_div = Thm.mk_binop \<^cterm>\<open>z3div\<close>
+val mk_mod = Thm.mk_binop \<^cterm>\<open>z3mod\<close>
+val mk_lt = Thm.mk_binop \<^cterm>\<open>(<) :: int \<Rightarrow> _\<close>
+val mk_le = Thm.mk_binop \<^cterm>\<open>(\<le>) :: int \<Rightarrow> _\<close>
fun mk_builtin_fun ctxt sym cts =
(case (sym, cts) of
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Tue Sep 28 22:14:02 2021 +0200
@@ -315,10 +315,10 @@
(thm COMP_INCR intro_hyp_rule1)
handle THM _ => thm COMP_INCR intro_hyp_rule2
-fun negated_prop (\<^const>\<open>HOL.Not\<close> $ t) = HOLogic.mk_Trueprop t
+fun negated_prop \<^Const_>\<open>Not for t\<close> = HOLogic.mk_Trueprop t
| negated_prop t = HOLogic.mk_Trueprop (HOLogic.mk_not t)
-fun intro_hyps tab (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) cx =
+fun intro_hyps tab (t as \<^Const_>\<open>HOL.disj\<close> $ t1 $ t2) cx =
lookup_intro_hyps tab t (fold (intro_hyps tab) [t1, t2]) cx
| intro_hyps tab t cx =
lookup_intro_hyps tab t (fn _ => raise LEMMA ()) cx
@@ -376,7 +376,7 @@
fun def_axiom_disj ctxt t =
(case dest_prop t of
- \<^const>\<open>HOL.disj\<close> $ u1 $ u2 =>
+ \<^Const_>\<open>disj for u1 u2\<close> =>
SMT_Replay_Methods.prove_abstract' ctxt t prop_tac (
SMT_Replay_Methods.abstract_prop u2 ##>> SMT_Replay_Methods.abstract_prop u1 #>>
HOLogic.mk_disj o swap)