--- a/src/HOL/Tools/Argo/argo_real.ML Sun Sep 19 21:55:11 2021 +0200
+++ b/src/HOL/Tools/Argo/argo_real.ML Mon Sep 20 11:35:27 2021 +0200
@@ -9,63 +9,62 @@
(* translating input terms *)
-fun trans_type _ \<^typ>\<open>Real.real\<close> tcx = SOME (Argo_Expr.Real, tcx)
+fun trans_type _ \<^Type>\<open>real\<close> tcx = SOME (Argo_Expr.Real, tcx)
| trans_type _ _ _ = NONE
-fun trans_term f (@{const Groups.uminus_class.uminus (real)} $ t) tcx =
+fun trans_term f \<^Const_>\<open>uminus \<open>\<^Type>\<open>real\<close>\<close> for t\<close> tcx =
tcx |> f t |>> Argo_Expr.mk_neg |> SOME
- | trans_term f (@{const Groups.plus_class.plus (real)} $ t1 $ t2) tcx =
+ | trans_term f \<^Const_>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_add2 |> SOME
- | trans_term f (@{const Groups.minus_class.minus (real)} $ t1 $ t2) tcx =
+ | trans_term f \<^Const_>\<open>minus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_sub |> SOME
- | trans_term f (@{const Groups.times_class.times (real)} $ t1 $ t2) tcx =
+ | trans_term f \<^Const_>\<open>times \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_mul |> SOME
- | trans_term f (@{const Rings.divide_class.divide (real)} $ t1 $ t2) tcx =
+ | trans_term f \<^Const_>\<open>divide \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_div |> SOME
- | trans_term f (@{const Orderings.ord_class.min (real)} $ t1 $ t2) tcx =
+ | trans_term f \<^Const_>\<open>min \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_min |> SOME
- | trans_term f (@{const Orderings.ord_class.max (real)} $ t1 $ t2) tcx =
+ | trans_term f \<^Const_>\<open>max \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_max |> SOME
- | trans_term f (@{const Groups.abs_class.abs (real)} $ t) tcx =
+ | trans_term f \<^Const_>\<open>abs \<open>\<^Type>\<open>real\<close>\<close> for t\<close> tcx =
tcx |> f t |>> Argo_Expr.mk_abs |> SOME
- | trans_term f (@{const Orderings.ord_class.less (real)} $ t1 $ t2) tcx =
+ | trans_term f \<^Const_>\<open>less \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_lt |> SOME
- | trans_term f (@{const Orderings.ord_class.less_eq (real)} $ t1 $ t2) tcx =
+ | trans_term f \<^Const_>\<open>less_eq \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_le |> SOME
| trans_term _ t tcx =
(case try HOLogic.dest_number t of
- SOME (\<^typ>\<open>Real.real\<close>, n) => SOME (Argo_Expr.mk_num (Rat.of_int n), tcx)
+ SOME (\<^Type>\<open>real\<close>, n) => SOME (Argo_Expr.mk_num (Rat.of_int n), tcx)
| _ => NONE)
(* reverse translation *)
-fun mk_plus t1 t2 = @{const Groups.plus_class.plus (real)} $ t1 $ t2
+fun mk_plus t1 t2 = \<^Const>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
fun mk_sum ts = uncurry (fold_rev mk_plus) (split_last ts)
-fun mk_times t1 t2 = @{const Groups.times_class.times (real)} $ t1 $ t2
-fun mk_divide t1 t2 = @{const Rings.divide_class.divide (real)} $ t1 $ t2
-fun mk_le t1 t2 = @{const Orderings.ord_class.less_eq (real)} $ t1 $ t2
-fun mk_lt t1 t2 = @{const Orderings.ord_class.less (real)} $ t1 $ t2
+fun mk_times t1 t2 = \<^Const>\<open>times \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
+fun mk_divide t1 t2 = \<^Const>\<open>divide \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
+fun mk_le t1 t2 = \<^Const>\<open>less_eq \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
+fun mk_lt t1 t2 = \<^Const>\<open>less \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
-fun mk_real_num i = HOLogic.mk_number \<^typ>\<open>Real.real\<close> i
+fun mk_real_num i = HOLogic.mk_number \<^Type>\<open>real\<close> i
fun mk_number n =
let val (p, q) = Rat.dest n
in if q = 1 then mk_real_num p else mk_divide (mk_real_num p) (mk_real_num q) end
fun term_of _ (Argo_Expr.E (Argo_Expr.Num n, _)) = SOME (mk_number n)
- | term_of f (Argo_Expr.E (Argo_Expr.Neg, [e])) =
- SOME (@{const Groups.uminus_class.uminus (real)} $ f e)
+ | term_of f (Argo_Expr.E (Argo_Expr.Neg, [e])) = SOME \<^Const>\<open>uminus \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e\<close>\<close>
| term_of f (Argo_Expr.E (Argo_Expr.Add, es)) = SOME (mk_sum (map f es))
| term_of f (Argo_Expr.E (Argo_Expr.Sub, [e1, e2])) =
- SOME (@{const Groups.minus_class.minus (real)} $ f e1 $ f e2)
+ SOME \<^Const>\<open>minus \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
| term_of f (Argo_Expr.E (Argo_Expr.Mul, [e1, e2])) = SOME (mk_times (f e1) (f e2))
| term_of f (Argo_Expr.E (Argo_Expr.Div, [e1, e2])) = SOME (mk_divide (f e1) (f e2))
| term_of f (Argo_Expr.E (Argo_Expr.Min, [e1, e2])) =
- SOME (@{const Orderings.ord_class.min (real)} $ f e1 $ f e2)
+ SOME \<^Const>\<open>min \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
| term_of f (Argo_Expr.E (Argo_Expr.Max, [e1, e2])) =
- SOME (@{const Orderings.ord_class.max (real)} $ f e1 $ f e2)
- | term_of f (Argo_Expr.E (Argo_Expr.Abs, [e])) = SOME (@{const Groups.abs_class.abs (real)} $ f e)
+ SOME \<^Const>\<open>max \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
+ | term_of f (Argo_Expr.E (Argo_Expr.Abs, [e])) = SOME \<^Const>\<open>abs \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e\<close>\<close>
| term_of f (Argo_Expr.E (Argo_Expr.Le, [e1, e2])) = SOME (mk_le (f e1) (f e2))
| term_of f (Argo_Expr.E (Argo_Expr.Lt, [e1, e2])) = SOME (mk_lt (f e1) (f e2))
| term_of _ _ = NONE
@@ -93,15 +92,15 @@
fun inv_num_conv ctxt = nums_conv mk_divide (fn (_, n) => Rat.inv n) ctxt @1
fun cmp_nums_conv ctxt b ct =
- let val t = if b then \<^const>\<open>HOL.True\<close> else \<^const>\<open>HOL.False\<close>
+ let val t = if b then \<^Const>\<open>True\<close> else \<^Const>\<open>False\<close>
in simp_conv ctxt (HOLogic.mk_eq (Thm.term_of ct, t)) ct end
local
-fun is_add2 (@{const Groups.plus_class.plus (real)} $ _ $ _) = true
+fun is_add2 \<^Const_>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for _ _\<close> = true
| is_add2 _ = false
-fun is_add3 (@{const Groups.plus_class.plus (real)} $ _ $ t) = is_add2 t
+fun is_add3 \<^Const_>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for _ t\<close> = is_add2 t
| is_add3 _ = false
val flatten_thm = mk_rewr @{lemma "(a::real) + b + c = a + (b + c)" by simp}
--- a/src/HOL/Tools/Argo/argo_tactic.ML Sun Sep 19 21:55:11 2021 +0200
+++ b/src/HOL/Tools/Argo/argo_tactic.ML Mon Sep 20 11:35:27 2021 +0200
@@ -144,8 +144,8 @@
SOME ty => (ty, tcx)
| NONE => add_new_type T tcx)
-fun trans_type _ \<^typ>\<open>HOL.bool\<close> = pair Argo_Expr.Bool
- | trans_type ctxt (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) =
+fun trans_type _ \<^Type>\<open>bool\<close> = pair Argo_Expr.Bool
+ | trans_type ctxt \<^Type>\<open>fun T1 T2\<close> =
trans_type ctxt T1 ##>> trans_type ctxt T2 #>> Argo_Expr.Func
| trans_type ctxt T = (fn tcx =>
(case ext_trans_type ctxt (trans_type ctxt) T tcx of
@@ -164,23 +164,23 @@
SOME c => (Argo_Expr.mk_con c, tcx)
| NONE => add_new_term ctxt t (Term.fastype_of t) tcx)
-fun mk_eq \<^typ>\<open>HOL.bool\<close> = Argo_Expr.mk_iff
+fun mk_eq \<^Type>\<open>bool\<close> = Argo_Expr.mk_iff
| mk_eq _ = Argo_Expr.mk_eq
-fun trans_term _ \<^const>\<open>HOL.True\<close> = pair Argo_Expr.true_expr
- | trans_term _ \<^const>\<open>HOL.False\<close> = pair Argo_Expr.false_expr
- | trans_term ctxt (\<^const>\<open>HOL.Not\<close> $ t) = trans_term ctxt t #>> Argo_Expr.mk_not
- | trans_term ctxt (\<^const>\<open>HOL.conj\<close> $ t1 $ t2) =
+fun trans_term _ \<^Const_>\<open>True\<close> = pair Argo_Expr.true_expr
+ | trans_term _ \<^Const_>\<open>False\<close> = pair Argo_Expr.false_expr
+ | trans_term ctxt \<^Const_>\<open>Not for t\<close> = trans_term ctxt t #>> Argo_Expr.mk_not
+ | trans_term ctxt \<^Const_>\<open>conj for t1 t2\<close> =
trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_and2
- | trans_term ctxt (\<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
+ | trans_term ctxt \<^Const_>\<open>disj for t1 t2\<close> =
trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_or2
- | trans_term ctxt (\<^const>\<open>HOL.implies\<close> $ t1 $ t2) =
+ | trans_term ctxt \<^Const_>\<open>implies for t1 t2\<close> =
trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_imp
- | trans_term ctxt (Const (\<^const_name>\<open>HOL.If\<close>, _) $ t1 $ t2 $ t3) =
+ | trans_term ctxt \<^Const_>\<open>If _ for t1 t2 t3\<close> =
trans_term ctxt t1 ##>> trans_term ctxt t2 ##>> trans_term ctxt t3 #>>
(fn ((u1, u2), u3) => Argo_Expr.mk_ite u1 u2 u3)
- | trans_term ctxt (Const (\<^const_name>\<open>HOL.eq\<close>, T) $ t1 $ t2) =
- trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry (mk_eq (Term.domain_type T))
+ | trans_term ctxt \<^Const_>\<open>HOL.eq T for t1 t2\<close> =
+ trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry (mk_eq T)
| trans_term ctxt (t as (t1 $ t2)) = (fn tcx =>
(case ext_trans_term ctxt (trans_term ctxt) t tcx of
SOME result => result
@@ -258,18 +258,16 @@
| mk_nary' _ f ts = mk_nary f ts
fun mk_ite t1 t2 t3 =
- let
- val T = Term.fastype_of t2
- val ite = Const (\<^const_name>\<open>HOL.If\<close>, [\<^typ>\<open>HOL.bool\<close>, T, T] ---> T)
- in ite $ t1 $ t2 $ t3 end
+ let val T = Term.fastype_of t2
+ in \<^Const>\<open>If T for t1 t2 t3\<close> end
-fun term_of _ (Argo_Expr.E (Argo_Expr.True, _)) = \<^const>\<open>HOL.True\<close>
- | term_of _ (Argo_Expr.E (Argo_Expr.False, _)) = \<^const>\<open>HOL.False\<close>
+fun term_of _ (Argo_Expr.E (Argo_Expr.True, _)) = \<^Const>\<open>True\<close>
+ | term_of _ (Argo_Expr.E (Argo_Expr.False, _)) = \<^Const>\<open>False\<close>
| term_of cx (Argo_Expr.E (Argo_Expr.Not, [e])) = HOLogic.mk_not (term_of cx e)
| term_of cx (Argo_Expr.E (Argo_Expr.And, es)) =
- mk_nary' \<^const>\<open>HOL.True\<close> HOLogic.mk_conj (map (term_of cx) es)
+ mk_nary' \<^Const>\<open>True\<close> HOLogic.mk_conj (map (term_of cx) es)
| term_of cx (Argo_Expr.E (Argo_Expr.Or, es)) =
- mk_nary' \<^const>\<open>HOL.False\<close> HOLogic.mk_disj (map (term_of cx) es)
+ mk_nary' \<^Const>\<open>False\<close> HOLogic.mk_disj (map (term_of cx) es)
| term_of cx (Argo_Expr.E (Argo_Expr.Imp, [e1, e2])) =
HOLogic.mk_imp (term_of cx e1, term_of cx e2)
| term_of cx (Argo_Expr.E (Argo_Expr.Iff, [e1, e2])) =
@@ -289,7 +287,7 @@
SOME t => t
| NONE => raise Fail "bad expression")
-fun as_prop ct = Thm.apply \<^cterm>\<open>HOL.Trueprop\<close> ct
+fun as_prop ct = Thm.apply \<^cterm>\<open>Trueprop\<close> ct
fun cterm_of ctxt cons e = Thm.cterm_of ctxt (term_of (ctxt, cons) e)
fun cprop_of ctxt cons e = as_prop (cterm_of ctxt cons e)
@@ -317,7 +315,7 @@
fun with_frees ctxt n mk =
let
val ns = map (fn i => "P" ^ string_of_int i) (0 upto (n - 1))
- val ts = map (Free o rpair \<^typ>\<open>bool\<close>) ns
+ val ts = map (Free o rpair \<^Type>\<open>bool\<close>) ns
val t = mk_nary HOLogic.mk_disj (mk ts)
in prove_taut ctxt ns t end
@@ -374,12 +372,12 @@
fun flat_conj_conv ct =
(case Thm.term_of ct of
- \<^const>\<open>HOL.conj\<close> $ _ $ _ => flatten_conv flat_conj_conv flatten_and_thm ct
+ \<^Const_>\<open>conj for _ _\<close> => flatten_conv flat_conj_conv flatten_and_thm ct
| _ => Conv.all_conv ct)
fun flat_disj_conv ct =
(case Thm.term_of ct of
- \<^const>\<open>HOL.disj\<close> $ _ $ _ => flatten_conv flat_disj_conv flatten_or_thm ct
+ \<^Const_>\<open>disj for _ _\<close> => flatten_conv flat_disj_conv flatten_or_thm ct
| _ => Conv.all_conv ct)
fun explode rule1 rule2 thm =
@@ -415,7 +413,7 @@
in mk_rewr (discharge2 lhs rhs rule) end
fun with_conj f g ct = iff_intro iff_conj_thm (f o explode_conj) g ct
-fun with_ndis f g ct = iff_intro iff_ndis_thm (f o explode_ndis) g (Thm.apply \<^cterm>\<open>HOL.Not\<close> ct)
+fun with_ndis f g ct = iff_intro iff_ndis_thm (f o explode_ndis) g (Thm.apply \<^cterm>\<open>Not\<close> ct)
fun swap_indices n iss = map (fn i => find_index (fn is => member (op =) is i) iss) (0 upto (n - 1))
fun sort_nary w f g (n, iss) = w (f (map hd iss)) (under_assumption (f (swap_indices n iss) o g))
@@ -485,7 +483,7 @@
| replay_args_conv ctxt [c1, c2] ct = binop_conv (replay_conv ctxt c1) (replay_conv ctxt c2) ct
| replay_args_conv ctxt (c :: cs) ct =
(case Term.head_of (Thm.term_of ct) of
- Const (\<^const_name>\<open>HOL.If\<close>, _) =>
+ \<^Const_>\<open>If _\<close> =>
let val (cs', c') = split_last cs
in Conv.combination_conv (replay_args_conv ctxt (c :: cs')) (replay_conv ctxt c') ct end
| _ => binop_conv (replay_conv ctxt c) (replay_args_conv ctxt cs) ct)
@@ -521,7 +519,7 @@
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>HOL.True\<close>
+val bogus_ct = \<^cterm>\<open>True\<close>
fun replay_unit_res lit (pthm, plits) (nthm, nlits) =
let
@@ -544,7 +542,7 @@
fun replay_hyp i ct =
if i < 0 then (Thm.assume ct, [(~i, ct)])
else
- let val cu = as_prop (Thm.apply \<^cterm>\<open>HOL.Not\<close> (Thm.apply \<^cterm>\<open>HOL.Not\<close> (Thm.dest_arg ct)))
+ let val cu = as_prop (Thm.apply \<^cterm>\<open>Not\<close> (Thm.apply \<^cterm>\<open>Not\<close> (Thm.dest_arg ct)))
in (discharge (Thm.assume cu) dneg_rule, [(~i, cu)]) end
@@ -602,7 +600,7 @@
fun unclausify (thm, lits) ls =
(case (Thm.prop_of thm, lits) of
- (\<^const>\<open>HOL.Trueprop\<close> $ \<^const>\<open>HOL.False\<close>, [(_, ct)]) =>
+ (\<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>False\<close>\<close>\<close>, [(_, ct)]) =>
let val thm = Thm.implies_intr ct thm
in (discharge thm unclausify_rule1 handle THM _ => discharge thm unclausify_rule2, ls) end
| _ => (thm, Ord_List.union lit_ord lits ls))
@@ -669,22 +667,22 @@
let val ct = Drule.strip_imp_concl (Thm.cprop_of thm)
in
(case Thm.term_of ct of
- \<^const>\<open>HOL.Trueprop\<close> $ Var (_, \<^typ>\<open>HOL.bool\<close>) =>
- instantiate (Thm.dest_arg ct) \<^cterm>\<open>HOL.False\<close> thm
- | Var _ => instantiate ct \<^cprop>\<open>HOL.False\<close> thm
+ \<^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
| _ => thm)
end
fun atomize_conv ctxt ct =
(case Thm.term_of ct of
- \<^const>\<open>HOL.Trueprop\<close> $ _ => Conv.all_conv
- | \<^const>\<open>Pure.imp\<close> $ _ $ _ =>
+ \<^Const_>\<open>Trueprop for _\<close> => Conv.all_conv
+ | \<^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