--- a/src/HOL/Decision_Procs/Approximation.thy Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Sep 29 22:54:38 2021 +0200
@@ -1033,24 +1033,24 @@
form
} ctxt ct
- fun term_of_bool true = \<^term>\<open>True\<close>
- | term_of_bool false = \<^term>\<open>False\<close>;
+ fun term_of_bool true = \<^Const>\<open>True\<close>
+ | term_of_bool false = \<^Const>\<open>False\<close>;
- val mk_int = HOLogic.mk_number \<^typ>\<open>int\<close> o @{code integer_of_int};
+ val mk_int = HOLogic.mk_number \<^Type>\<open>int\<close> o @{code integer_of_int};
fun term_of_float (@{code Float} (k, l)) =
- \<^term>\<open>Float\<close> $ mk_int k $ mk_int l;
+ \<^Const>\<open>Float for \<open>mk_int k\<close> \<open>mk_int l\<close>\<close>;
fun term_of_float_interval x = @{term "Interval::_\<Rightarrow>float interval"} $
HOLogic.mk_prod
(apply2 term_of_float (@{code lowerF} x, @{code upperF} x))
- fun term_of_float_interval_option NONE = \<^term>\<open>None :: (float interval) option\<close>
- | term_of_float_interval_option (SOME ff) = \<^term>\<open>Some :: float interval \<Rightarrow> _\<close>
- $ (term_of_float_interval ff);
+ fun term_of_float_interval_option NONE = \<^Const>\<open>None \<^typ>\<open>float interval option\<close>\<close>
+ | term_of_float_interval_option (SOME ff) =
+ \<^Const>\<open>Some \<^typ>\<open>float interval\<close> for \<open>term_of_float_interval ff\<close>\<close>;
val term_of_float_interval_option_list =
- HOLogic.mk_list \<^typ>\<open>(float interval) option\<close> o map term_of_float_interval_option;
+ HOLogic.mk_list \<^typ>\<open>float interval option\<close> o map term_of_float_interval_option;
val approx_bool = @{computation bool}
(fn _ => fn x => case x of SOME b => term_of_bool b
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Wed Sep 29 22:54:38 2021 +0200
@@ -649,13 +649,13 @@
by (induct l) (simp_all add: cring_class.in_carrier_def carrier_class)
ML \<open>
-val term_of_nat = HOLogic.mk_number \<^typ>\<open>nat\<close> o @{code integer_of_nat};
+val term_of_nat = HOLogic.mk_number \<^Type>\<open>nat\<close> o @{code integer_of_nat};
-val term_of_int = HOLogic.mk_number \<^typ>\<open>int\<close> o @{code integer_of_int};
+val term_of_int = HOLogic.mk_number \<^Type>\<open>int\<close> o @{code integer_of_int};
-fun term_of_pol (@{code Pc} k) = \<^term>\<open>Pc\<close> $ term_of_int k
- | term_of_pol (@{code Pinj} (n, p)) = \<^term>\<open>Pinj\<close> $ term_of_nat n $ term_of_pol p
- | term_of_pol (@{code PX} (p, n, q)) = \<^term>\<open>PX\<close> $ term_of_pol p $ term_of_nat n $ term_of_pol q;
+fun term_of_pol (@{code Pc} k) = \<^Const>\<open>Pc\<close> $ term_of_int k
+ | term_of_pol (@{code Pinj} (n, p)) = \<^Const>\<open>Pinj\<close> $ term_of_nat n $ term_of_pol p
+ | term_of_pol (@{code PX} (p, n, q)) = \<^Const>\<open>PX\<close> $ term_of_pol p $ term_of_nat n $ term_of_pol q;
local
@@ -742,53 +742,43 @@
in (map tr ths1, map tr ths2, map tr ths3, map tr ths4, tr th5, tr th) end
| NONE => error "get_ring_simps: lookup failed");
-fun ring_struct (Const (\<^const_name>\<open>Ring.ring.add\<close>, _) $ R $ _ $ _) = SOME R
- | ring_struct (Const (\<^const_name>\<open>Ring.a_minus\<close>, _) $ R $ _ $ _) = SOME R
- | ring_struct (Const (\<^const_name>\<open>Group.monoid.mult\<close>, _) $ R $ _ $ _) = SOME R
- | ring_struct (Const (\<^const_name>\<open>Ring.a_inv\<close>, _) $ R $ _) = SOME R
- | ring_struct (Const (\<^const_name>\<open>Group.pow\<close>, _) $ R $ _ $ _) = SOME R
- | ring_struct (Const (\<^const_name>\<open>Ring.ring.zero\<close>, _) $ R) = SOME R
- | ring_struct (Const (\<^const_name>\<open>Group.monoid.one\<close>, _) $ R) = SOME R
- | ring_struct (Const (\<^const_name>\<open>Algebra_Aux.of_integer\<close>, _) $ R $ _) = SOME R
+fun ring_struct \<^Const_>\<open>Ring.ring.add _ _ for R _ _\<close> = SOME R
+ | ring_struct \<^Const_>\<open>Ring.a_minus _ _ for R _ _\<close> = SOME R
+ | ring_struct \<^Const_>\<open>Group.monoid.mult _ _ for R _ _\<close> = SOME R
+ | ring_struct \<^Const_>\<open>Ring.a_inv _ _ for R _\<close> = SOME R
+ | ring_struct \<^Const_>\<open>Group.pow _ _ _ for R _ _\<close> = SOME R
+ | ring_struct \<^Const_>\<open>Ring.ring.zero _ _ for R\<close> = SOME R
+ | ring_struct \<^Const_>\<open>Group.monoid.one _ _ for R\<close> = SOME R
+ | ring_struct \<^Const_>\<open>Algebra_Aux.of_integer _ _ for R _\<close> = SOME R
| ring_struct _ = NONE;
-fun reif_polex vs (Const (\<^const_name>\<open>Ring.ring.add\<close>, _) $ _ $ a $ b) =
- \<^const>\<open>Add\<close> $ reif_polex vs a $ reif_polex vs b
- | reif_polex vs (Const (\<^const_name>\<open>Ring.a_minus\<close>, _) $ _ $ a $ b) =
- \<^const>\<open>Sub\<close> $ reif_polex vs a $ reif_polex vs b
- | reif_polex vs (Const (\<^const_name>\<open>Group.monoid.mult\<close>, _) $ _ $ a $ b) =
- \<^const>\<open>Mul\<close> $ reif_polex vs a $ reif_polex vs b
- | reif_polex vs (Const (\<^const_name>\<open>Ring.a_inv\<close>, _) $ _ $ a) =
- \<^const>\<open>Neg\<close> $ reif_polex vs a
- | reif_polex vs (Const (\<^const_name>\<open>Group.pow\<close>, _) $ _ $ a $ n) =
- \<^const>\<open>Pow\<close> $ reif_polex vs a $ n
+fun reif_polex vs \<^Const_>\<open>Ring.ring.add _ _ for _ a b\<close> =
+ \<^Const>\<open>Add for \<open>reif_polex vs a\<close> \<open>reif_polex vs b\<close>\<close>
+ | reif_polex vs \<^Const_>\<open>Ring.a_minus _ _ for _ a b\<close> =
+ \<^Const>\<open>Sub for \<open>reif_polex vs a\<close> \<open>reif_polex vs b\<close>\<close>
+ | reif_polex vs \<^Const_>\<open>Group.monoid.mult _ _ for _ a b\<close> =
+ \<^Const>\<open>Mul for \<open>reif_polex vs a\<close> \<open>reif_polex vs b\<close>\<close>
+ | reif_polex vs \<^Const_>\<open>Ring.a_inv _ _ for _ a\<close> =
+ \<^Const>\<open>Neg for \<open>reif_polex vs a\<close>\<close>
+ | reif_polex vs \<^Const_>\<open>Group.pow _ _ _ for _ a n\<close> =
+ \<^Const>\<open>Pow for \<open>reif_polex vs a\<close> n\<close>
| reif_polex vs (Free x) =
- \<^const>\<open>Var\<close> $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)
- | reif_polex vs (Const (\<^const_name>\<open>Ring.ring.zero\<close>, _) $ _) =
- \<^term>\<open>Const 0\<close>
- | reif_polex vs (Const (\<^const_name>\<open>Group.monoid.one\<close>, _) $ _) =
- \<^term>\<open>Const 1\<close>
- | reif_polex vs (Const (\<^const_name>\<open>Algebra_Aux.of_integer\<close>, _) $ _ $ n) =
- \<^const>\<open>Const\<close> $ n
+ \<^Const>\<open>Var for \<open>HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)\<close>\<close>
+ | reif_polex _ \<^Const_>\<open>Ring.ring.zero _ _ for _\<close> = \<^term>\<open>Const 0\<close>
+ | reif_polex _ \<^Const_>\<open>Group.monoid.one _ _ for _\<close> = \<^term>\<open>Const 1\<close>
+ | reif_polex _ \<^Const_>\<open>Algebra_Aux.of_integer _ _ for _ n\<close> = \<^Const>\<open>Const for n\<close>
| reif_polex _ _ = error "reif_polex: bad expression";
-fun reif_polex' vs (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ a $ b) =
- \<^const>\<open>Add\<close> $ reif_polex' vs a $ reif_polex' vs b
- | reif_polex' vs (Const (\<^const_name>\<open>Groups.minus\<close>, _) $ a $ b) =
- \<^const>\<open>Sub\<close> $ reif_polex' vs a $ reif_polex' vs b
- | reif_polex' vs (Const (\<^const_name>\<open>Groups.times\<close>, _) $ a $ b) =
- \<^const>\<open>Mul\<close> $ reif_polex' vs a $ reif_polex' vs b
- | reif_polex' vs (Const (\<^const_name>\<open>Groups.uminus\<close>, _) $ a) =
- \<^const>\<open>Neg\<close> $ reif_polex' vs a
- | reif_polex' vs (Const (\<^const_name>\<open>Power.power\<close>, _) $ a $ n) =
- \<^const>\<open>Pow\<close> $ reif_polex' vs a $ n
- | reif_polex' vs (Free x) =
- \<^const>\<open>Var\<close> $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)
- | reif_polex' vs (Const (\<^const_name>\<open>numeral\<close>, _) $ b) =
- \<^const>\<open>Const\<close> $ (@{const numeral (int)} $ b)
- | reif_polex' vs (Const (\<^const_name>\<open>zero_class.zero\<close>, _)) = \<^term>\<open>Const 0\<close>
- | reif_polex' vs (Const (\<^const_name>\<open>one_class.one\<close>, _)) = \<^term>\<open>Const 1\<close>
- | reif_polex' vs t = error "reif_polex: bad expression";
+fun reif_polex' vs \<^Const_>\<open>plus _ for a b\<close> = \<^Const>\<open>Add for \<open>reif_polex' vs a\<close> \<open>reif_polex' vs b\<close>\<close>
+ | reif_polex' vs \<^Const_>\<open>minus _ for a b\<close> = \<^Const>\<open>Sub for \<open>reif_polex' vs a\<close> \<open>reif_polex' vs b\<close>\<close>
+ | reif_polex' vs \<^Const_>\<open>times _ for a b\<close> = \<^Const>\<open>Mul for \<open>reif_polex' vs a\<close> \<open>reif_polex' vs b\<close>\<close>
+ | reif_polex' vs \<^Const_>\<open>uminus _ for a\<close> = \<^Const>\<open>Neg for \<open>reif_polex' vs a\<close>\<close>
+ | reif_polex' vs \<^Const_>\<open>power _ for a n\<close> = \<^Const>\<open>Pow for \<open>reif_polex' vs a\<close> n\<close>
+ | reif_polex' vs (Free x) = \<^Const>\<open>Var for \<open>HOLogic.mk_number \<^Type>\<open>nat\<close> (find_index (equal x) vs)\<close>\<close>
+ | reif_polex' _ \<^Const_>\<open>numeral _ for b\<close> = \<^Const>\<open>Const for \<^Const>\<open>numeral \<^Type>\<open>int\<close> for b\<close>\<close>
+ | reif_polex' _ \<^Const_>\<open>zero_class.zero _\<close> = \<^term>\<open>Const 0\<close>
+ | reif_polex' _ \<^Const_>\<open>one_class.one _\<close> = \<^term>\<open>Const 1\<close>
+ | reif_polex' _ t = error "reif_polex: bad expression";
fun head_conv (_, _, _, _, head_simp, _) ys =
(case strip_app ys of
@@ -892,9 +882,8 @@
val props = map fst (Facts.props (Proof_Context.facts_of ctxt)) @ maps dest_conj prems;
val ths = map (fn p as (x, _) =>
(case find_first
- ((fn Const (\<^const_name>\<open>Trueprop\<close>, _) $
- (Const (\<^const_name>\<open>Set.member\<close>, _) $
- Free (y, _) $ (Const (\<^const_name>\<open>carrier\<close>, _) $ S)) =>
+ ((fn \<^Const_>\<open>Trueprop
+ for \<^Const_>\<open>Set.member _ for \<open>Free (y, _)\<close> \<^Const_>\<open>carrier _ _ for S\<close>\<close>\<close> =>
x = y andalso R aconv S
| _ => false) o Thm.prop_of) props of
SOME th => th
@@ -905,11 +894,7 @@
ths in_carrier_Nil
end;
-fun mk_ring T =
- Const (\<^const_name>\<open>cring_class_ops\<close>,
- Type (\<^type_name>\<open>partial_object_ext\<close>, [T,
- Type (\<^type_name>\<open>monoid_ext\<close>, [T,
- Type (\<^type_name>\<open>ring_ext\<close>, [T, \<^typ>\<open>unit\<close>])])]));
+fun mk_ring T = \<^Const>\<open>cring_class_ops T\<close>;
val iterations = \<^cterm>\<open>1000::nat\<close>;
val Trueprop_cong = Thm.combination (Thm.reflexive \<^cterm>\<open>Trueprop\<close>);
@@ -926,7 +911,7 @@
| NONE => (mk_ring T, SOME cT, @{thm in_carrier_trivial}, reif_polex' xs));
val rls as (_, _, _, _, _, norm_subst_correct) = get_ring_simps ctxt optcT R;
val cxs = Thm.cterm_of ctxt (HOLogic.mk_list T (map Free xs));
- val ceqs = Thm.cterm_of ctxt (HOLogic.mk_list \<^typ>\<open>polex * polex\<close>
+ val ceqs = Thm.cterm_of ctxt (HOLogic.mk_list \<^typ>\<open>polex \<times> polex\<close>
(map (HOLogic.mk_prod o apply2 reif) eqs'));
val cp = Thm.cterm_of ctxt (reif (Thm.term_of ct));
val prem = Thm.equal_elim
--- a/src/HOL/Decision_Procs/Conversions.thy Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/Conversions.thy Wed Sep 29 22:54:38 2021 +0200
@@ -257,13 +257,12 @@
in
fn n =>
case Thm.term_of n of
- Const (\<^const_name>\<open>one_class.one\<close>, _) => numeral_1_eq_1_a
- | Const (\<^const_name>\<open>uminus\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _) =>
+ \<^Const_>\<open>one_class.one _\<close> => numeral_1_eq_1_a
+ | \<^Const_>\<open>uminus _ for \<^Const_>\<open>one_class.one _\<close>\<close> =>
Thm.combination (Thm.reflexive (Thm.dest_fun n)) numeral_1_eq_1_a
- | Const (\<^const_name>\<open>zero_class.zero\<close>, _) => Thm.reflexive n
- | Const (\<^const_name>\<open>numeral\<close>, _) $ _ => Thm.reflexive n
- | Const (\<^const_name>\<open>uminus\<close>, _) $
- (Const (\<^const_name>\<open>numeral\<close>, _) $ _) => Thm.reflexive n
+ | \<^Const_>\<open>zero_class.zero _\<close> => Thm.reflexive n
+ | \<^Const_>\<open>numeral _ for _\<close> => Thm.reflexive n
+ | \<^Const_>\<open>uminus _ for \<^Const_>\<open>numeral _ for _\<close>\<close> => Thm.reflexive n
| _ => err "expand1" n
end;
@@ -272,10 +271,8 @@
in
fn eq =>
case Thm.term_of (Thm.rhs_of eq) of
- Const (\<^const_name>\<open>Num.numeral\<close>, _) $ Const (\<^const_name>\<open>Num.One\<close>, _) =>
- Thm.transitive eq numeral_1_eq_1_a
- | Const (\<^const_name>\<open>uminus\<close>, _) $
- (Const (\<^const_name>\<open>Num.numeral\<close>, _) $ Const (\<^const_name>\<open>Num.One\<close>, _)) =>
+ \<^Const_>\<open>Num.numeral _ for \<^Const_>\<open>Num.One\<close>\<close> => Thm.transitive eq numeral_1_eq_1_a
+ | \<^Const_>\<open>uminus _ for \<^Const_>\<open>Num.numeral _ for \<^Const_>\<open>Num.One\<close>\<close>\<close> =>
Thm.transitive eq
(Thm.combination (Thm.reflexive (Thm.dest_fun (Thm.rhs_of eq)))
numeral_1_eq_1_a)
@@ -777,7 +774,7 @@
val eq = Thm.combination (Thm.reflexive (Thm.dest_fun (Thm.dest_fun2 ct))) p_eq
in
case Thm.term_of (Thm.rhs_of p_eq) of
- Const (\<^const_name>\<open>True\<close>, _) =>
+ \<^Const_>\<open>True\<close> =>
let
val x_eq = x cx;
val cx = Thm.rhs_of x_eq;
@@ -788,7 +785,7 @@
(Thm.reflexive cy))
(inst [] [cx, cy] if_True)
end
- | Const (\<^const_name>\<open>False\<close>, _) =>
+ | \<^Const_>\<open>False\<close> =>
let
val y_eq = y cy;
val cy = Thm.rhs_of y_eq;
@@ -812,7 +809,7 @@
val If_conv_a = If_conv (type_of_eqn drop_0_a);
fun conv n ys = (case Thm.term_of n of
- Const (\<^const_name>\<open>zero_class.zero\<close>, _) => inst [] [ys] drop_0_a
+ \<^Const_>\<open>zero_class.zero _\<close> => inst [] [ys] drop_0_a
| _ => (case strip_app ys of
(\<^const_name>\<open>Cons\<close>, [x, xs]) =>
transitive'
--- a/src/HOL/Decision_Procs/Cooper.thy Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Wed Sep 29 22:54:38 2021 +0200
@@ -2386,17 +2386,17 @@
| num_of_term vs \<^term>\<open>0::int\<close> = @{code C} (@{code int_of_integer} 0)
| num_of_term vs \<^term>\<open>1::int\<close> = @{code C} (@{code int_of_integer} 1)
| num_of_term vs \<^term>\<open>- 1::int\<close> = @{code C} (@{code int_of_integer} (~ 1))
- | num_of_term vs (\<^term>\<open>numeral :: _ \<Rightarrow> int\<close> $ t) =
+ | num_of_term vs \<^Const_>\<open>numeral _ for t\<close> =
@{code C} (@{code int_of_integer} (HOLogic.dest_numeral t))
- | num_of_term vs (\<^term>\<open>- numeral :: _ \<Rightarrow> int\<close> $ t) =
+ | num_of_term vs (\<^term>\<open>- numeral :: _ \<Rightarrow> int\<close> $ t) = (* FIXME !? *)
@{code C} (@{code int_of_integer} (~(HOLogic.dest_numeral t)))
| num_of_term vs (Bound i) = @{code Bound} (@{code nat_of_integer} i)
- | num_of_term vs (\<^term>\<open>uminus :: int \<Rightarrow> int\<close> $ t') = @{code Neg} (num_of_term vs t')
- | num_of_term vs (\<^term>\<open>(+) :: int \<Rightarrow> int \<Rightarrow> int\<close> $ t1 $ t2) =
+ | num_of_term vs \<^Const_>\<open>uminus \<^Type>\<open>int\<close> for t'\<close> = @{code Neg} (num_of_term vs t')
+ | num_of_term vs \<^Const_>\<open>plus \<^Type>\<open>int\<close> for t1 t2\<close> =
@{code Add} (num_of_term vs t1, num_of_term vs t2)
- | num_of_term vs (\<^term>\<open>(-) :: int \<Rightarrow> int \<Rightarrow> int\<close> $ t1 $ t2) =
+ | num_of_term vs \<^Const_>\<open>minus \<^Type>\<open>int\<close> for t1 t2\<close> =
@{code Sub} (num_of_term vs t1, num_of_term vs t2)
- | num_of_term vs (\<^term>\<open>(*) :: int \<Rightarrow> int \<Rightarrow> int\<close> $ t1 $ t2) =
+ | num_of_term vs \<^Const_>\<open>times \<^Type>\<open>int\<close> for t1 t2\<close> =
(case try HOLogic.dest_number t1 of
SOME (_, i) => @{code Mul} (@{code int_of_integer} i, num_of_term vs t2)
| NONE =>
@@ -2405,34 +2405,34 @@
| NONE => error "num_of_term: unsupported multiplication"))
| num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term \<^context> t);
-fun fm_of_term ps vs \<^term>\<open>True\<close> = @{code T}
- | fm_of_term ps vs \<^term>\<open>False\<close> = @{code F}
- | fm_of_term ps vs (\<^term>\<open>(<) :: int \<Rightarrow> int \<Rightarrow> bool\<close> $ t1 $ t2) =
+fun fm_of_term ps vs \<^Const_>\<open>True\<close> = @{code T}
+ | fm_of_term ps vs \<^Const_>\<open>False\<close> = @{code F}
+ | fm_of_term ps vs \<^Const_>\<open>less \<^Type>\<open>int\<close> for t1 t2\<close> =
@{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
- | fm_of_term ps vs (\<^term>\<open>(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool\<close> $ t1 $ t2) =
+ | fm_of_term ps vs \<^Const_>\<open>less_eq \<^Type>\<open>int\<close> for t1 t2\<close> =
@{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
- | fm_of_term ps vs (\<^term>\<open>(=) :: int \<Rightarrow> int \<Rightarrow> bool\<close> $ t1 $ t2) =
+ | fm_of_term ps vs \<^Const_>\<open>HOL.eq \<^Type>\<open>int\<close> for t1 t2\<close> =
@{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
- | fm_of_term ps vs (\<^term>\<open>(dvd) :: int \<Rightarrow> int \<Rightarrow> bool\<close> $ t1 $ t2) =
+ | fm_of_term ps vs \<^Const_>\<open>dvd \<^Type>\<open>int\<close> for t1 t2\<close> =
(case try HOLogic.dest_number t1 of
SOME (_, i) => @{code Dvd} (@{code int_of_integer} i, num_of_term vs t2)
| NONE => error "num_of_term: unsupported dvd")
- | fm_of_term ps vs (\<^term>\<open>(=) :: bool \<Rightarrow> bool \<Rightarrow> bool\<close> $ t1 $ t2) =
+ | fm_of_term ps vs \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for t1 t2\<close> =
@{code Iff} (fm_of_term ps vs t1, fm_of_term ps vs t2)
- | fm_of_term ps vs (\<^term>\<open>HOL.conj\<close> $ t1 $ t2) =
+ | fm_of_term ps vs \<^Const_>\<open>HOL.conj for t1 t2\<close> =
@{code And} (fm_of_term ps vs t1, fm_of_term ps vs t2)
- | fm_of_term ps vs (\<^term>\<open>HOL.disj\<close> $ t1 $ t2) =
+ | fm_of_term ps vs \<^Const_>\<open>HOL.disj for t1 t2\<close> =
@{code Or} (fm_of_term ps vs t1, fm_of_term ps vs t2)
- | fm_of_term ps vs (\<^term>\<open>HOL.implies\<close> $ t1 $ t2) =
+ | fm_of_term ps vs \<^Const_>\<open>HOL.implies for t1 t2\<close> =
@{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
- | fm_of_term ps vs (\<^term>\<open>HOL.Not\<close> $ t') =
+ | fm_of_term ps vs \<^Const_>\<open>HOL.Not for t'\<close> =
@{code Not} (fm_of_term ps vs t')
- | fm_of_term ps vs (Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (xn, xT, p)) =
+ | fm_of_term ps vs \<^Const_>\<open>Ex _ for \<open>Abs (xn, xT, p)\<close>\<close> =
let
val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p); (* FIXME !? *)
val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
in @{code E} (fm_of_term ps vs' p) end
- | fm_of_term ps vs (Const (\<^const_name>\<open>All\<close>, _) $ Abs (xn, xT, p)) =
+ | fm_of_term ps vs \<^Const_>\<open>All _ for \<open>Abs (xn, xT, p)\<close>\<close> =
let
val (xn', p') = Syntax_Trans.variant_abs (xn, xT, p); (* FIXME !? *)
val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
@@ -2444,44 +2444,44 @@
let
val q = @{code integer_of_nat} n
in fst (the (find_first (fn (_, m) => q = m) vs)) end
- | term_of_num vs (@{code Neg} t') = \<^term>\<open>uminus :: int \<Rightarrow> int\<close> $ term_of_num vs t'
- | term_of_num vs (@{code Add} (t1, t2)) = \<^term>\<open>(+) :: int \<Rightarrow> int \<Rightarrow> int\<close> $
- term_of_num vs t1 $ term_of_num vs t2
- | term_of_num vs (@{code Sub} (t1, t2)) = \<^term>\<open>(-) :: int \<Rightarrow> int \<Rightarrow> int\<close> $
- term_of_num vs t1 $ term_of_num vs t2
- | term_of_num vs (@{code Mul} (i, t2)) = \<^term>\<open>(*) :: int \<Rightarrow> int \<Rightarrow> int\<close> $
- term_of_num vs (@{code C} i) $ term_of_num vs t2
+ | term_of_num vs (@{code Neg} t') = \<^Const>\<open>uminus \<^Type>\<open>int\<close> for \<open>term_of_num vs t'\<close>\<close>
+ | term_of_num vs (@{code Add} (t1, t2)) =
+ \<^Const>\<open>plus \<^Type>\<open>int\<close> for \<open>term_of_num vs t1\<close> \<open>term_of_num vs t2\<close>\<close>
+ | term_of_num vs (@{code Sub} (t1, t2)) =
+ \<^Const>\<open>minus \<^Type>\<open>int\<close> for \<open>term_of_num vs t1\<close> \<open>term_of_num vs t2\<close>\<close>
+ | term_of_num vs (@{code Mul} (i, t2)) =
+ \<^Const>\<open>times \<^Type>\<open>int\<close> for \<open>term_of_num vs (@{code C} i)\<close> \<open>term_of_num vs t2\<close>\<close>
| term_of_num vs (@{code CN} (n, i, t)) =
term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
-fun term_of_fm ps vs @{code T} = \<^term>\<open>True\<close>
- | term_of_fm ps vs @{code F} = \<^term>\<open>False\<close>
+fun term_of_fm ps vs @{code T} = \<^Const>\<open>True\<close>
+ | term_of_fm ps vs @{code F} = \<^Const>\<open>False\<close>
| term_of_fm ps vs (@{code Lt} t) =
- \<^term>\<open>(<) :: int \<Rightarrow> int \<Rightarrow> bool\<close> $ term_of_num vs t $ \<^term>\<open>0::int\<close>
+ \<^Const>\<open>less \<^Type>\<open>int\<close> for \<open>term_of_num vs t\<close> \<^term>\<open>0::int\<close>\<close>
| term_of_fm ps vs (@{code Le} t) =
- \<^term>\<open>(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool\<close> $ term_of_num vs t $ \<^term>\<open>0::int\<close>
+ \<^Const>\<open>less_eq \<^Type>\<open>int\<close> for \<open>term_of_num vs t\<close> \<^term>\<open>0::int\<close>\<close>
| term_of_fm ps vs (@{code Gt} t) =
- \<^term>\<open>(<) :: int \<Rightarrow> int \<Rightarrow> bool\<close> $ \<^term>\<open>0::int\<close> $ term_of_num vs t
+ \<^Const>\<open>less \<^Type>\<open>int\<close> for \<^term>\<open>0::int\<close> \<open>term_of_num vs t\<close>\<close>
| term_of_fm ps vs (@{code Ge} t) =
- \<^term>\<open>(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool\<close> $ \<^term>\<open>0::int\<close> $ term_of_num vs t
+ \<^Const>\<open>less_eq \<^Type>\<open>int\<close> for \<^term>\<open>0::int\<close> \<open>term_of_num vs t\<close>\<close>
| term_of_fm ps vs (@{code Eq} t) =
- \<^term>\<open>(=) :: int \<Rightarrow> int \<Rightarrow> bool\<close> $ term_of_num vs t $ \<^term>\<open>0::int\<close>
+ \<^Const>\<open>HOL.eq \<^Type>\<open>int\<close> for \<open>term_of_num vs t\<close> \<^term>\<open>0::int\<close>\<close>
| term_of_fm ps vs (@{code NEq} t) =
term_of_fm ps vs (@{code Not} (@{code Eq} t))
| term_of_fm ps vs (@{code Dvd} (i, t)) =
- \<^term>\<open>(dvd) :: int \<Rightarrow> int \<Rightarrow> bool\<close> $ term_of_num vs (@{code C} i) $ term_of_num vs t
+ \<^Const>\<open>dvd \<^Type>\<open>int\<close> for \<open>term_of_num vs (@{code C} i)\<close> \<open>term_of_num vs t\<close>\<close>
| term_of_fm ps vs (@{code NDvd} (i, t)) =
term_of_fm ps vs (@{code Not} (@{code Dvd} (i, t)))
| term_of_fm ps vs (@{code Not} t') =
- HOLogic.Not $ term_of_fm ps vs t'
+ \<^Const>\<open>HOL.Not for \<open>term_of_fm ps vs t'\<close>\<close>
| term_of_fm ps vs (@{code And} (t1, t2)) =
- HOLogic.conj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+ \<^Const>\<open>HOL.conj for \<open>term_of_fm ps vs t1\<close> \<open>term_of_fm ps vs t2\<close>\<close>
| term_of_fm ps vs (@{code Or} (t1, t2)) =
- HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+ \<^Const>\<open>HOL.disj for \<open>term_of_fm ps vs t1\<close> \<open>term_of_fm ps vs t2\<close>\<close>
| term_of_fm ps vs (@{code Imp} (t1, t2)) =
- HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+ \<^Const>\<open>HOL.implies for \<open>term_of_fm ps vs t1\<close> \<open>term_of_fm ps vs t2\<close>\<close>
| term_of_fm ps vs (@{code Iff} (t1, t2)) =
- \<^term>\<open>(=) :: bool \<Rightarrow> bool \<Rightarrow> bool\<close> $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+ \<^Const>\<open>HOL.eq \<^Type>\<open>bool\<close> for \<open>term_of_fm ps vs t1\<close> \<open>term_of_fm ps vs t2\<close>\<close>
| term_of_fm ps vs (@{code Closed} n) =
let
val q = @{code integer_of_nat} n
@@ -2491,12 +2491,12 @@
fun term_bools acc t =
let
val is_op =
- member (=) [\<^term>\<open>HOL.conj\<close>, \<^term>\<open>HOL.disj\<close>, \<^term>\<open>HOL.implies\<close>,
- \<^term>\<open>(=) :: bool \<Rightarrow> _\<close>,
- \<^term>\<open>(=) :: int \<Rightarrow> _\<close>, \<^term>\<open>(<) :: int \<Rightarrow> _\<close>,
- \<^term>\<open>(\<le>) :: int \<Rightarrow> _\<close>, \<^term>\<open>HOL.Not\<close>, \<^term>\<open>All :: (int \<Rightarrow> _) \<Rightarrow> _\<close>,
- \<^term>\<open>Ex :: (int \<Rightarrow> _) \<Rightarrow> _\<close>, \<^term>\<open>True\<close>, \<^term>\<open>False\<close>]
- fun is_ty t = not (fastype_of t = HOLogic.boolT)
+ member (=) [\<^Const>\<open>HOL.conj\<close>, \<^Const>\<open>HOL.disj\<close>, \<^Const>\<open>HOL.implies\<close>,
+ \<^Const>\<open>HOL.eq \<^Type>\<open>bool\<close>\<close>,
+ \<^Const>\<open>HOL.eq \<^Type>\<open>int\<close>\<close>, \<^Const>\<open>less \<^Type>\<open>int\<close>\<close>,
+ \<^Const>\<open>less_eq \<^Type>\<open>int\<close>\<close>, \<^Const>\<open>HOL.Not\<close>, \<^Const>\<open>All \<^Type>\<open>int\<close>\<close>,
+ \<^Const>\<open>Ex \<^Type>\<open>int\<close>\<close>, \<^Const>\<open>True\<close>, \<^Const>\<open>False\<close>]
+ fun is_ty t = not (fastype_of t = \<^Type>\<open>bool\<close>)
in
(case t of
(l as f $ a) $ b =>
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Sep 29 22:54:38 2021 +0200
@@ -719,10 +719,10 @@
val [lt, le] = map (Morphism.term phi) [\<^term>\<open>(\<sqsubset>)\<close>, \<^term>\<open>(\<sqsubseteq>)\<close>]
fun h x t =
case Thm.term_of t of
- Const(\<^const_name>\<open>HOL.eq\<close>, _)$y$z =>
+ \<^Const_>\<open>HOL.eq _ for y z\<close> =>
if Thm.term_of x aconv y then Ferrante_Rackoff_Data.Eq
else Ferrante_Rackoff_Data.Nox
- | \<^term>\<open>Not\<close>$(Const(\<^const_name>\<open>HOL.eq\<close>, _)$y$z) =>
+ | \<^Const_>\<open>Not for \<^Const>\<open>HOL.eq _ for y z\<close>\<close> =>
if Thm.term_of x aconv y then Ferrante_Rackoff_Data.NEq
else Ferrante_Rackoff_Data.Nox
| b$y$z => if Term.could_unify (b, lt) then
@@ -901,27 +901,27 @@
fun dest_frac ct =
case Thm.term_of ct of
- Const (\<^const_name>\<open>Rings.divide\<close>,_) $ a $ b=>
+ \<^Const_>\<open>Rings.divide _ for a b\<close> =>
Rat.make (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
- | Const(\<^const_name>\<open>inverse\<close>, _)$a => Rat.make(1, HOLogic.dest_number a |> snd)
+ | \<^Const_>\<open>inverse _ for a\<close> => Rat.make(1, HOLogic.dest_number a |> snd)
| t => Rat.of_int (snd (HOLogic.dest_number t))
fun whatis x ct = case Thm.term_of ct of
- Const(\<^const_name>\<open>Groups.plus\<close>, _)$(Const(\<^const_name>\<open>Groups.times\<close>,_)$_$y)$_ =>
+ \<^Const_>\<open>plus _ for \<^Const_>\<open>times _ for _ y\<close> _\<close> =>
if y aconv Thm.term_of x then ("c*x+t",[(funpow 2 Thm.dest_arg1) ct, Thm.dest_arg ct])
else ("Nox",[])
-| Const(\<^const_name>\<open>Groups.plus\<close>, _)$y$_ =>
+| \<^Const_>\<open>plus _ for y _\<close> =>
if y aconv Thm.term_of x then ("x+t",[Thm.dest_arg ct])
else ("Nox",[])
-| Const(\<^const_name>\<open>Groups.times\<close>, _)$_$y =>
+| \<^Const_>\<open>times _ for _ y\<close> =>
if y aconv Thm.term_of x then ("c*x",[Thm.dest_arg1 ct])
else ("Nox",[])
| t => if t aconv Thm.term_of x then ("x",[]) else ("Nox",[]);
fun xnormalize_conv ctxt [] ct = Thm.reflexive ct
-| xnormalize_conv ctxt (vs as (x::_)) ct =
+ | xnormalize_conv ctxt (vs as (x::_)) ct =
case Thm.term_of ct of
- Const(\<^const_name>\<open>Orderings.less\<close>,_)$_$Const(\<^const_name>\<open>Groups.zero\<close>,_) =>
+ \<^Const_>\<open>less _ for _ \<^Const_>\<open>zero_class.zero _\<close>\<close> =>
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
@@ -964,14 +964,14 @@
| _ => Thm.reflexive ct)
-| Const(\<^const_name>\<open>Orderings.less_eq\<close>,_)$_$Const(\<^const_name>\<open>Groups.zero\<close>,_) =>
+| \<^Const_>\<open>less_eq _ for _ \<^Const_>\<open>zero_class.zero _\<close>\<close> =>
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
val T = Thm.typ_of_cterm x
val cT = Thm.ctyp_of_cterm x
val cr = dest_frac c
- val clt = Thm.cterm_of ctxt (Const (\<^const_name>\<open>ord_class.less\<close>, T --> T --> \<^typ>\<open>bool\<close>))
+ val clt = Thm.cterm_of ctxt \<^Const>\<open>less T\<close>
val cz = Thm.dest_arg ct
val neg = cr < @0
val cthp = Simplifier.rewrite ctxt
@@ -996,7 +996,7 @@
val T = Thm.typ_of_cterm x
val cT = Thm.ctyp_of_cterm x
val cr = dest_frac c
- val clt = Thm.cterm_of ctxt (Const (\<^const_name>\<open>ord_class.less\<close>, T --> T --> \<^typ>\<open>bool\<close>))
+ val clt = Thm.cterm_of ctxt \<^Const>\<open>less T\<close>
val cz = Thm.dest_arg ct
val neg = cr < @0
val cthp = Simplifier.rewrite ctxt
@@ -1010,7 +1010,7 @@
in rth end
| _ => Thm.reflexive ct)
-| Const(\<^const_name>\<open>HOL.eq\<close>,_)$_$Const(\<^const_name>\<open>Groups.zero\<close>,_) =>
+| \<^Const_>\<open>HOL.eq _ for _ \<^Const_>\<open>zero_class.zero _\<close>\<close> =>
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
@@ -1056,7 +1056,7 @@
val ss = simpset_of \<^context>
in
fun field_isolate_conv phi ctxt vs ct = case Thm.term_of ct of
- Const(\<^const_name>\<open>Orderings.less\<close>,_)$a$b =>
+ \<^Const_>\<open>less _ for a b\<close> =>
let val (ca,cb) = Thm.dest_binop ct
val T = Thm.ctyp_of_cterm ca
val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
@@ -1065,7 +1065,7 @@
(Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier_ord vs)))) th
val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
-| Const(\<^const_name>\<open>Orderings.less_eq\<close>,_)$a$b =>
+| \<^Const_>\<open>less_eq _ for a b\<close> =>
let val (ca,cb) = Thm.dest_binop ct
val T = Thm.ctyp_of_cterm ca
val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
@@ -1075,7 +1075,7 @@
val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
-| Const(\<^const_name>\<open>HOL.eq\<close>,_)$a$b =>
+| \<^Const_>\<open>HOL.eq _ for a b\<close> =>
let val (ca,cb) = Thm.dest_binop ct
val T = Thm.ctyp_of_cterm ca
val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
@@ -1084,7 +1084,7 @@
(Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier_ord vs)))) th
val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
-| \<^term>\<open>Not\<close> $(Const(\<^const_name>\<open>HOL.eq\<close>,_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
+| \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq _ for a b\<close>\<close> => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
| _ => Thm.reflexive ct
end;
@@ -1092,17 +1092,17 @@
let
fun h x t =
case Thm.term_of t of
- Const(\<^const_name>\<open>HOL.eq\<close>, _)$y$z =>
+ \<^Const_>\<open>HOL.eq _ for y z\<close> =>
if Thm.term_of x aconv y then Ferrante_Rackoff_Data.Eq
else Ferrante_Rackoff_Data.Nox
- | \<^term>\<open>Not\<close>$(Const(\<^const_name>\<open>HOL.eq\<close>, _)$y$z) =>
+ | \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq _ for y z\<close>\<close> =>
if Thm.term_of x aconv y then Ferrante_Rackoff_Data.NEq
else Ferrante_Rackoff_Data.Nox
- | Const(\<^const_name>\<open>Orderings.less\<close>,_)$y$z =>
+ | \<^Const_>\<open>less _ for y z\<close> =>
if Thm.term_of x aconv y then Ferrante_Rackoff_Data.Lt
else if Thm.term_of x aconv z then Ferrante_Rackoff_Data.Gt
else Ferrante_Rackoff_Data.Nox
- | Const (\<^const_name>\<open>Orderings.less_eq\<close>,_)$y$z =>
+ | \<^Const_>\<open>less_eq _ for y z\<close> =>
if Thm.term_of x aconv y then Ferrante_Rackoff_Data.Le
else if Thm.term_of x aconv z then Ferrante_Rackoff_Data.Ge
else Ferrante_Rackoff_Data.Nox
--- a/src/HOL/Decision_Procs/Ferrack.thy Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Wed Sep 29 22:54:38 2021 +0200
@@ -2458,15 +2458,15 @@
fun num_of_term vs (Free vT) = mk_Bound (find_index (fn vT' => vT = vT') vs)
| num_of_term vs \<^term>\<open>real_of_int (0::int)\<close> = mk_C 0
| num_of_term vs \<^term>\<open>real_of_int (1::int)\<close> = mk_C 1
- | num_of_term vs \<^term>\<open>0::real\<close> = mk_C 0
- | num_of_term vs \<^term>\<open>1::real\<close> = mk_C 1
+ | num_of_term vs \<^Const_>\<open>zero_class.zero \<^Type>\<open>real\<close>\<close> = mk_C 0
+ | num_of_term vs \<^Const_>\<open>one_class.one \<^Type>\<open>real\<close>\<close> = mk_C 1
| num_of_term vs (Bound i) = mk_Bound i
- | num_of_term vs (\<^term>\<open>uminus :: real \<Rightarrow> real\<close> $ t') = @{code Neg} (num_of_term vs t')
- | num_of_term vs (\<^term>\<open>(+) :: real \<Rightarrow> real \<Rightarrow> real\<close> $ t1 $ t2) =
+ | num_of_term vs \<^Const_>\<open>uminus \<^Type>\<open>real\<close> for t'\<close> = @{code Neg} (num_of_term vs t')
+ | num_of_term vs \<^Const_>\<open>plus \<^Type>\<open>real\<close> for t1 t2\<close> =
@{code Add} (num_of_term vs t1, num_of_term vs t2)
- | num_of_term vs (\<^term>\<open>(-) :: real \<Rightarrow> real \<Rightarrow> real\<close> $ t1 $ t2) =
+ | num_of_term vs \<^Const_>\<open>minus \<^Type>\<open>real\<close> for t1 t2\<close> =
@{code Sub} (num_of_term vs t1, num_of_term vs t2)
- | num_of_term vs (\<^term>\<open>(*) :: real \<Rightarrow> real \<Rightarrow> real\<close> $ t1 $ t2) = (case num_of_term vs t1
+ | num_of_term vs \<^Const_>\<open>times \<^Type>\<open>real\<close> for t1 t2\<close> = (case num_of_term vs t1
of @{code C} i => @{code Mul} (i, num_of_term vs t2)
| _ => error "num_of_term: unsupported multiplication")
| num_of_term vs (\<^term>\<open>real_of_int :: int \<Rightarrow> real\<close> $ t') =
@@ -2476,57 +2476,49 @@
(mk_C (snd (HOLogic.dest_number t'))
handle TERM _ => error ("num_of_term: unknown term"));
-fun fm_of_term vs \<^term>\<open>True\<close> = @{code T}
- | fm_of_term vs \<^term>\<open>False\<close> = @{code F}
- | fm_of_term vs (\<^term>\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) =
+fun fm_of_term vs \<^Const_>\<open>True\<close> = @{code T}
+ | fm_of_term vs \<^Const_>\<open>False\<close> = @{code F}
+ | fm_of_term vs \<^Const_>\<open>less \<^Type>\<open>real\<close> for t1 t2\<close> =
@{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
- | fm_of_term vs (\<^term>\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) =
+ | fm_of_term vs \<^Const_>\<open>less_eq \<^Type>\<open>real\<close> for t1 t2\<close> =
@{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
- | fm_of_term vs (\<^term>\<open>(=) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) =
+ | fm_of_term vs \<^Const_>\<open>HOL.eq \<^Type>\<open>real\<close> for t1 t2\<close> =
@{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
- | fm_of_term vs (\<^term>\<open>(\<longleftrightarrow>) :: bool \<Rightarrow> bool \<Rightarrow> bool\<close> $ t1 $ t2) =
+ | fm_of_term vs \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for t1 t2\<close> =
@{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (\<^term>\<open>HOL.conj\<close> $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (\<^term>\<open>HOL.disj\<close> $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (\<^term>\<open>HOL.implies\<close> $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (\<^term>\<open>HOL.Not\<close> $ t') = @{code Not} (fm_of_term vs t')
- | fm_of_term vs (Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (xn, xT, p)) =
- @{code E} (fm_of_term (("", dummyT) :: vs) p)
- | fm_of_term vs (Const (\<^const_name>\<open>All\<close>, _) $ Abs (xn, xT, p)) =
- @{code A} (fm_of_term (("", dummyT) :: vs) p)
+ | fm_of_term vs \<^Const_>\<open>HOL.conj for t1 t2\<close> = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs \<^Const_>\<open>HOL.disj for t1 t2\<close> = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs \<^Const_>\<open>HOL.implies for t1 t2\<close> = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
+ | fm_of_term vs \<^Const_>\<open>HOL.Not for t'\<close> = @{code Not} (fm_of_term vs t')
+ | fm_of_term vs \<^Const_>\<open>Ex _ for \<open>Abs (xn, xT, p)\<close>\<close> = @{code E} (fm_of_term (("", dummyT) :: vs) p)
+ | fm_of_term vs \<^Const_>\<open>All _ for \<open>Abs (xn, xT, p)\<close>\<close> = @{code A} (fm_of_term (("", dummyT) :: vs) p)
| fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term \<^context> t);
fun term_of_num vs (@{code C} i) = \<^term>\<open>real_of_int :: int \<Rightarrow> real\<close> $
HOLogic.mk_number HOLogic.intT (@{code integer_of_int} i)
| term_of_num vs (@{code Bound} n) = Free (nth vs (@{code integer_of_nat} n))
- | term_of_num vs (@{code Neg} t') = \<^term>\<open>uminus :: real \<Rightarrow> real\<close> $ term_of_num vs t'
- | term_of_num vs (@{code Add} (t1, t2)) = \<^term>\<open>(+) :: real \<Rightarrow> real \<Rightarrow> real\<close> $
- term_of_num vs t1 $ term_of_num vs t2
- | term_of_num vs (@{code Sub} (t1, t2)) = \<^term>\<open>(-) :: real \<Rightarrow> real \<Rightarrow> real\<close> $
- term_of_num vs t1 $ term_of_num vs t2
- | term_of_num vs (@{code Mul} (i, t2)) = \<^term>\<open>(*) :: real \<Rightarrow> real \<Rightarrow> real\<close> $
- term_of_num vs (@{code C} i) $ term_of_num vs t2
+ | term_of_num vs (@{code Neg} t') = \<^Const>\<open>uminus \<^Type>\<open>real\<close> for \<open>term_of_num vs t'\<close>\<close>
+ | term_of_num vs (@{code Add} (t1, t2)) =
+ \<^Const>\<open>plus \<^Type>\<open>real\<close> for \<open>term_of_num vs t1\<close> \<open>term_of_num vs t2\<close>\<close>
+ | term_of_num vs (@{code Sub} (t1, t2)) =
+ \<^Const>\<open>minus \<^Type>\<open>real\<close> for \<open>term_of_num vs t1\<close> \<open>term_of_num vs t2\<close>\<close>
+ | term_of_num vs (@{code Mul} (i, t2)) =
+ \<^Const>\<open>times \<^Type>\<open>real\<close> for \<open>term_of_num vs (@{code C} i)\<close> \<open>term_of_num vs t2\<close>\<close>
| term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
-fun term_of_fm vs @{code T} = \<^term>\<open>True\<close>
- | term_of_fm vs @{code F} = \<^term>\<open>False\<close>
- | term_of_fm vs (@{code Lt} t) = \<^term>\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $
- term_of_num vs t $ \<^term>\<open>0::real\<close>
- | term_of_fm vs (@{code Le} t) = \<^term>\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $
- term_of_num vs t $ \<^term>\<open>0::real\<close>
- | term_of_fm vs (@{code Gt} t) = \<^term>\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $
- \<^term>\<open>0::real\<close> $ term_of_num vs t
- | term_of_fm vs (@{code Ge} t) = \<^term>\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $
- \<^term>\<open>0::real\<close> $ term_of_num vs t
- | term_of_fm vs (@{code Eq} t) = \<^term>\<open>(=) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $
- term_of_num vs t $ \<^term>\<open>0::real\<close>
+fun term_of_fm vs @{code T} = \<^Const>\<open>True\<close>
+ | term_of_fm vs @{code F} = \<^Const>\<open>False\<close>
+ | term_of_fm vs (@{code Lt} t) = \<^Const>\<open>less \<^Type>\<open>real\<close> for \<open>term_of_num vs t\<close> \<^term>\<open>0::real\<close>\<close>
+ | term_of_fm vs (@{code Le} t) = \<^Const>\<open>less_eq \<^Type>\<open>real\<close> for \<open>term_of_num vs t\<close> \<^term>\<open>0::real\<close>\<close>
+ | term_of_fm vs (@{code Gt} t) = \<^Const>\<open>less \<^Type>\<open>real\<close> for \<^term>\<open>0::real\<close> \<open>term_of_num vs t\<close>\<close>
+ | term_of_fm vs (@{code Ge} t) = \<^Const>\<open>less_eq \<^Type>\<open>real\<close> for \<^term>\<open>0::real\<close> \<open>term_of_num vs t\<close>\<close>
+ | term_of_fm vs (@{code Eq} t) = \<^Const>\<open>HOL.eq \<^Type>\<open>real\<close> for \<open>term_of_num vs t\<close> \<^term>\<open>0::real\<close>\<close>
| term_of_fm vs (@{code NEq} t) = term_of_fm vs (@{code Not} (@{code Eq} t))
- | term_of_fm vs (@{code Not} t') = HOLogic.Not $ term_of_fm vs t'
- | term_of_fm vs (@{code And} (t1, t2)) = HOLogic.conj $ term_of_fm vs t1 $ term_of_fm vs t2
- | term_of_fm vs (@{code Or} (t1, t2)) = HOLogic.disj $ term_of_fm vs t1 $ term_of_fm vs t2
- | term_of_fm vs (@{code Imp} (t1, t2)) = HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2
- | term_of_fm vs (@{code Iff} (t1, t2)) = \<^term>\<open>(\<longleftrightarrow>) :: bool \<Rightarrow> bool \<Rightarrow> bool\<close> $
- term_of_fm vs t1 $ term_of_fm vs t2;
+ | term_of_fm vs (@{code Not} t') = \<^Const>\<open>HOL.Not for \<open>term_of_fm vs t'\<close>\<close>
+ | term_of_fm vs (@{code And} (t1, t2)) = \<^Const>\<open>HOL.conj for \<open>term_of_fm vs t1\<close> \<open>term_of_fm vs t2\<close>\<close>
+ | term_of_fm vs (@{code Or} (t1, t2)) = \<^Const>\<open>HOL.disj for \<open>term_of_fm vs t1\<close> \<open>term_of_fm vs t2\<close>\<close>
+ | term_of_fm vs (@{code Imp} (t1, t2)) = \<^Const>\<open>HOL.implies for \<open>term_of_fm vs t1\<close> \<open>term_of_fm vs t2\<close>\<close>
+ | term_of_fm vs (@{code Iff} (t1, t2)) = \<^Const>\<open>HOL.eq \<^Type>\<open>bool\<close> for \<open>term_of_fm vs t1\<close> \<open>term_of_fm vs t2\<close>\<close>
in fn (ctxt, t) =>
let
--- a/src/HOL/Decision_Procs/MIR.thy Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Wed Sep 29 22:54:38 2021 +0200
@@ -5581,92 +5581,92 @@
| num_of_term vs \<^term>\<open>1::real\<close> = mk_C 1
| num_of_term vs \<^term>\<open>- 1::real\<close> = mk_C (~ 1)
| num_of_term vs (Bound i) = mk_Bound i
- | num_of_term vs (\<^term>\<open>uminus :: real \<Rightarrow> real\<close> $ t') = @{code Neg} (num_of_term vs t')
- | num_of_term vs (\<^term>\<open>(+) :: real \<Rightarrow> real \<Rightarrow> real\<close> $ t1 $ t2) =
+ | num_of_term vs \<^Const_>\<open>uminus \<^Type>\<open>real\<close> for t'\<close> = @{code Neg} (num_of_term vs t')
+ | num_of_term vs \<^Const_>\<open>plus \<^Type>\<open>real\<close> for t1 t2\<close> =
@{code Add} (num_of_term vs t1, num_of_term vs t2)
- | num_of_term vs (\<^term>\<open>(-) :: real \<Rightarrow> real \<Rightarrow> real\<close> $ t1 $ t2) =
+ | num_of_term vs \<^Const_>\<open>minus \<^Type>\<open>real\<close> for t1 t2\<close> =
@{code Sub} (num_of_term vs t1, num_of_term vs t2)
- | num_of_term vs (\<^term>\<open>(*) :: real \<Rightarrow> real \<Rightarrow> real\<close> $ t1 $ t2) =
- (case (num_of_term vs t1)
- of @{code C} i => @{code Mul} (i, num_of_term vs t2)
- | _ => error "num_of_term: unsupported Multiplication")
- | num_of_term vs (\<^term>\<open>of_int :: int \<Rightarrow> real\<close> $ (\<^term>\<open>numeral :: _ \<Rightarrow> int\<close> $ t')) =
+ | num_of_term vs \<^Const_>\<open>times \<^Type>\<open>real\<close> for t1 t2\<close> =
+ (case num_of_term vs t1 of
+ @{code C} i => @{code Mul} (i, num_of_term vs t2)
+ | _ => error "num_of_term: unsupported Multiplication")
+ | num_of_term vs \<^Const_>\<open>of_int \<^Type>\<open>real\<close> for \<^Const_>\<open>numeral \<^Type>\<open>int\<close> for t'\<close>\<close> =
mk_C (HOLogic.dest_numeral t')
- | num_of_term vs (\<^term>\<open>of_int :: int \<Rightarrow> real\<close> $ (\<^term>\<open>- numeral :: _ \<Rightarrow> int\<close> $ t')) =
+ | num_of_term vs (\<^Const_>\<open>of_int \<^Type>\<open>real\<close>\<close> $ (\<^term>\<open>- numeral :: _ \<Rightarrow> int\<close> $ t')) = (* FIXME !? *)
mk_C (~ (HOLogic.dest_numeral t'))
- | num_of_term vs (\<^term>\<open>of_int :: int \<Rightarrow> real\<close> $ (\<^term>\<open>floor :: real \<Rightarrow> int\<close> $ t')) =
+ | num_of_term vs \<^Const_>\<open>of_int \<^Type>\<open>real\<close> for \<^Const_>\<open>floor \<^Type>\<open>real\<close> for t'\<close>\<close> =
@{code Floor} (num_of_term vs t')
- | num_of_term vs (\<^term>\<open>of_int :: int \<Rightarrow> real\<close> $ (\<^term>\<open>ceiling :: real \<Rightarrow> int\<close> $ t')) =
+ | num_of_term vs \<^Const_>\<open>of_int \<^Type>\<open>real\<close> for \<^Const_>\<open>ceiling \<^Type>\<open>real\<close> for t'\<close>\<close> =
@{code Neg} (@{code Floor} (@{code Neg} (num_of_term vs t')))
- | num_of_term vs (\<^term>\<open>numeral :: _ \<Rightarrow> real\<close> $ t') =
+ | num_of_term vs \<^Const_>\<open>numeral \<^Type>\<open>real\<close> for t'\<close> =
mk_C (HOLogic.dest_numeral t')
- | num_of_term vs (\<^term>\<open>- numeral :: _ \<Rightarrow> real\<close> $ t') =
+ | num_of_term vs (\<^term>\<open>- numeral :: _ \<Rightarrow> real\<close> $ t') = (* FIXME !? *)
mk_C (~ (HOLogic.dest_numeral t'))
| num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term \<^context> t);
-fun fm_of_term vs \<^term>\<open>True\<close> = @{code T}
- | fm_of_term vs \<^term>\<open>False\<close> = @{code F}
- | fm_of_term vs (\<^term>\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) =
+fun fm_of_term vs \<^Const_>\<open>True\<close> = @{code T}
+ | fm_of_term vs \<^Const_>\<open>False\<close> = @{code F}
+ | fm_of_term vs \<^Const_>\<open>less \<^Type>\<open>real\<close> for t1 t2\<close> =
@{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
- | fm_of_term vs (\<^term>\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) =
+ | fm_of_term vs \<^Const_>\<open>less_eq \<^Type>\<open>real\<close> for t1 t2\<close> =
@{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
- | fm_of_term vs (\<^term>\<open>(=) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) =
+ | fm_of_term vs \<^Const_>\<open>HOL.eq \<^Type>\<open>real\<close> for t1 t2\<close> =
@{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
- | fm_of_term vs (\<^term>\<open>(rdvd)\<close> $ (\<^term>\<open>of_int :: int \<Rightarrow> real\<close> $ (\<^term>\<open>numeral :: _ \<Rightarrow> int\<close> $ t1)) $ t2) =
+ | fm_of_term vs \<^Const_>\<open>rdvd for \<^Const_>\<open>of_int \<^Type>\<open>real\<close> for \<^Const_>\<open>numeral \<^Type>\<open>int\<close> for t1\<close>\<close> t2\<close> =
mk_Dvd (HOLogic.dest_numeral t1, num_of_term vs t2)
- | fm_of_term vs (\<^term>\<open>(rdvd)\<close> $ (\<^term>\<open>of_int :: int \<Rightarrow> real\<close> $ (\<^term>\<open>- numeral :: _ \<Rightarrow> int\<close> $ t1)) $ t2) =
+ | fm_of_term vs \<^Const_>\<open>rdvd for \<^Const_>\<open>of_int \<^Type>\<open>real\<close> for \<open>(\<^term>\<open>- numeral :: _ \<Rightarrow> int\<close> $ t1)\<close>\<close> t2\<close> = (* FIXME !? *)
mk_Dvd (~ (HOLogic.dest_numeral t1), num_of_term vs t2)
- | fm_of_term vs (\<^term>\<open>(=) :: bool \<Rightarrow> bool \<Rightarrow> bool\<close> $ t1 $ t2) =
+ | fm_of_term vs \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for t1 t2\<close> =
@{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (\<^term>\<open>HOL.conj\<close> $ t1 $ t2) =
+ | fm_of_term vs \<^Const_>\<open>HOL.conj for t1 t2\<close> =
@{code And} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (\<^term>\<open>HOL.disj\<close> $ t1 $ t2) =
+ | fm_of_term vs \<^Const_>\<open>HOL.disj for t1 t2\<close> =
@{code Or} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (\<^term>\<open>HOL.implies\<close> $ t1 $ t2) =
+ | fm_of_term vs \<^Const_>\<open>HOL.implies for t1 t2\<close> =
@{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
- | fm_of_term vs (\<^term>\<open>HOL.Not\<close> $ t') =
+ | fm_of_term vs \<^Const_>\<open>HOL.Not for t'\<close> =
@{code Not} (fm_of_term vs t')
- | fm_of_term vs (Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (xn, xT, p)) =
+ | fm_of_term vs \<^Const_>\<open>Ex _ for \<open>Abs (xn, xT, p)\<close>\<close> =
@{code E} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
- | fm_of_term vs (Const (\<^const_name>\<open>All\<close>, _) $ Abs (xn, xT, p)) =
+ | fm_of_term vs \<^Const_>\<open>All _ for \<open>Abs (xn, xT, p)\<close>\<close> =
@{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
| fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term \<^context> t);
-fun term_of_num vs (@{code C} i) = \<^term>\<open>of_int :: int \<Rightarrow> real\<close> $
- HOLogic.mk_number HOLogic.intT (@{code integer_of_int} i)
+fun term_of_num vs (@{code C} i) =
+ \<^Const>\<open>of_int \<^Type>\<open>real\<close> for \<open>HOLogic.mk_number HOLogic.intT (@{code integer_of_int} i)\<close>\<close>
| term_of_num vs (@{code Bound} n) =
let
val m = @{code integer_of_nat} n;
in fst (the (find_first (fn (_, q) => m = q) vs)) end
| term_of_num vs (@{code Neg} (@{code Floor} (@{code Neg} t'))) =
- \<^term>\<open>of_int :: int \<Rightarrow> real\<close> $ (\<^term>\<open>ceiling :: real \<Rightarrow> int\<close> $ term_of_num vs t')
- | term_of_num vs (@{code Neg} t') = \<^term>\<open>uminus :: real \<Rightarrow> real\<close> $ term_of_num vs t'
- | term_of_num vs (@{code Add} (t1, t2)) = \<^term>\<open>(+) :: real \<Rightarrow> real \<Rightarrow> real\<close> $
- term_of_num vs t1 $ term_of_num vs t2
- | term_of_num vs (@{code Sub} (t1, t2)) = \<^term>\<open>(-) :: real \<Rightarrow> real \<Rightarrow> real\<close> $
- term_of_num vs t1 $ term_of_num vs t2
- | term_of_num vs (@{code Mul} (i, t2)) = \<^term>\<open>(*) :: real \<Rightarrow> real \<Rightarrow> real\<close> $
- term_of_num vs (@{code C} i) $ term_of_num vs t2
- | term_of_num vs (@{code Floor} t) = \<^term>\<open>of_int :: int \<Rightarrow> real\<close> $ (\<^term>\<open>floor :: real \<Rightarrow> int\<close> $ term_of_num vs t)
+ \<^Const>\<open>of_int \<^Type>\<open>real\<close> for \<^Const>\<open>ceiling \<^Type>\<open>real\<close> for \<open>term_of_num vs t'\<close>\<close>\<close>
+ | term_of_num vs (@{code Neg} t') = \<^Const>\<open>uminus \<^Type>\<open>real\<close> for \<open>term_of_num vs t'\<close>\<close>
+ | term_of_num vs (@{code Add} (t1, t2)) =
+ \<^Const>\<open>plus \<^Type>\<open>real\<close> for \<open>term_of_num vs t1\<close> \<open>term_of_num vs t2\<close>\<close>
+ | term_of_num vs (@{code Sub} (t1, t2)) =
+ \<^Const>\<open>minus \<^Type>\<open>real\<close> for \<open>term_of_num vs t1\<close> \<open>term_of_num vs t2\<close>\<close>
+ | term_of_num vs (@{code Mul} (i, t2)) =
+ \<^Const>\<open>times \<^Type>\<open>real\<close> for \<open>term_of_num vs (@{code C} i)\<close> \<open>term_of_num vs t2\<close>\<close>
+ | term_of_num vs (@{code Floor} t) = \<^Const>\<open>of_int \<^Type>\<open>real\<close> for \<^Const>\<open>floor \<^Type>\<open>real\<close> for \<open>term_of_num vs t\<close>\<close>\<close>
| term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t))
| term_of_num vs (@{code CF} (c, t, s)) = term_of_num vs (@{code Add} (@{code Mul} (c, @{code Floor} t), s));
-fun term_of_fm vs @{code T} = \<^term>\<open>True\<close>
- | term_of_fm vs @{code F} = \<^term>\<open>False\<close>
+fun term_of_fm vs @{code T} = \<^Const>\<open>True\<close>
+ | term_of_fm vs @{code F} = \<^Const>\<open>False\<close>
| term_of_fm vs (@{code Lt} t) =
- \<^term>\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ term_of_num vs t $ \<^term>\<open>0::real\<close>
+ \<^Const>\<open>less \<^Type>\<open>real\<close> for \<open>term_of_num vs t\<close> \<^term>\<open>0::real\<close>\<close>
| term_of_fm vs (@{code Le} t) =
- \<^term>\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ term_of_num vs t $ \<^term>\<open>0::real\<close>
+ \<^Const>\<open>less_eq \<^Type>\<open>real\<close> for \<open>term_of_num vs t\<close> \<^term>\<open>0::real\<close>\<close>
| term_of_fm vs (@{code Gt} t) =
- \<^term>\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ \<^term>\<open>0::real\<close> $ term_of_num vs t
+ \<^Const>\<open>less \<^Type>\<open>real\<close> for \<^term>\<open>0::real\<close> \<open>term_of_num vs t\<close>\<close>
| term_of_fm vs (@{code Ge} t) =
- \<^term>\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ \<^term>\<open>0::real\<close> $ term_of_num vs t
+ \<^Const>\<open>less_eq \<^Type>\<open>real\<close> for \<^term>\<open>0::real\<close> \<open>term_of_num vs t\<close>\<close>
| term_of_fm vs (@{code Eq} t) =
- \<^term>\<open>(=) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ term_of_num vs t $ \<^term>\<open>0::real\<close>
+ \<^Const>\<open>HOL.eq \<^Type>\<open>real\<close> for \<open>term_of_num vs t\<close> \<^term>\<open>0::real\<close>\<close>
| term_of_fm vs (@{code NEq} t) =
term_of_fm vs (@{code Not} (@{code Eq} t))
| term_of_fm vs (@{code Dvd} (i, t)) =
- \<^term>\<open>(rdvd)\<close> $ term_of_num vs (@{code C} i) $ term_of_num vs t
+ \<^Const>\<open>rdvd for \<open>term_of_num vs (@{code C} i)\<close> \<open>term_of_num vs t\<close>\<close>
| term_of_fm vs (@{code NDvd} (i, t)) =
term_of_fm vs (@{code Not} (@{code Dvd} (i, t)))
| term_of_fm vs (@{code Not} t') =
@@ -5678,7 +5678,7 @@
| term_of_fm vs (@{code Imp} (t1, t2)) =
HOLogic.imp $ term_of_fm vs t1 $ term_of_fm vs t2
| term_of_fm vs (@{code Iff} (t1, t2)) =
- \<^term>\<open>(=) :: bool \<Rightarrow> bool \<Rightarrow> bool\<close> $ term_of_fm vs t1 $ term_of_fm vs t2;
+ \<^Const>\<open>HOL.eq \<^Type>\<open>bool\<close> for \<open>term_of_fm vs t1\<close> \<open>term_of_fm vs t2\<close>\<close>;
in
fn (ctxt, t) =>
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Sep 29 22:54:38 2021 +0200
@@ -3922,9 +3922,6 @@
\<open>
let
-fun binopT T = T --> T --> T;
-fun relT T = T --> T --> \<^typ>\<open>bool\<close>;
-
val mk_C = @{code C} o apply2 @{code int_of_integer};
val mk_poly_Bound = @{code poly.Bound} o @{code nat_of_integer};
val mk_Bound = @{code Bound} o @{code nat_of_integer};
@@ -3934,7 +3931,7 @@
fun try_dest_num t = SOME ((snd o HOLogic.dest_number) t)
handle TERM _ => NONE;
-fun dest_nat (t as Const (\<^const_name>\<open>Suc\<close>, _)) = HOLogic.dest_nat t
+fun dest_nat (t as \<^Const_>\<open>Suc\<close>) = HOLogic.dest_nat t (* FIXME !? *)
| dest_nat t = dest_num t;
fun the_index ts t =
@@ -3942,58 +3939,46 @@
val k = find_index (fn t' => t aconv t') ts;
in if k < 0 then raise General.Subscript else k end;
-fun num_of_term ps (Const (\<^const_name>\<open>Groups.uminus\<close>, _) $ t) =
- @{code poly.Neg} (num_of_term ps t)
- | num_of_term ps (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ a $ b) =
- @{code poly.Add} (num_of_term ps a, num_of_term ps b)
- | num_of_term ps (Const (\<^const_name>\<open>Groups.minus\<close>, _) $ a $ b) =
- @{code poly.Sub} (num_of_term ps a, num_of_term ps b)
- | num_of_term ps (Const (\<^const_name>\<open>Groups.times\<close>, _) $ a $ b) =
- @{code poly.Mul} (num_of_term ps a, num_of_term ps b)
- | num_of_term ps (Const (\<^const_name>\<open>Power.power\<close>, _) $ a $ n) =
+fun num_of_term ps \<^Const_>\<open>uminus _ for t\<close> = @{code poly.Neg} (num_of_term ps t)
+ | num_of_term ps \<^Const_>\<open>plus _ for a b\<close> = @{code poly.Add} (num_of_term ps a, num_of_term ps b)
+ | num_of_term ps \<^Const_>\<open>minus _ for a b\<close> = @{code poly.Sub} (num_of_term ps a, num_of_term ps b)
+ | num_of_term ps \<^Const_>\<open>times _ for a b\<close> = @{code poly.Mul} (num_of_term ps a, num_of_term ps b)
+ | num_of_term ps \<^Const_>\<open>power _ for a n\<close> =
@{code poly.Pw} (num_of_term ps a, @{code nat_of_integer} (dest_nat n))
- | num_of_term ps (Const (\<^const_name>\<open>Rings.divide\<close>, _) $ a $ b) =
- mk_C (dest_num a, dest_num b)
+ | num_of_term ps \<^Const_>\<open>divide _ for a b\<close> = mk_C (dest_num a, dest_num b)
| num_of_term ps t =
(case try_dest_num t of
SOME k => mk_C (k, 1)
| NONE => mk_poly_Bound (the_index ps t));
-fun tm_of_term fs ps (Const(\<^const_name>\<open>Groups.uminus\<close>, _) $ t) =
- @{code Neg} (tm_of_term fs ps t)
- | tm_of_term fs ps (Const(\<^const_name>\<open>Groups.plus\<close>, _) $ a $ b) =
- @{code Add} (tm_of_term fs ps a, tm_of_term fs ps b)
- | tm_of_term fs ps (Const(\<^const_name>\<open>Groups.minus\<close>, _) $ a $ b) =
- @{code Sub} (tm_of_term fs ps a, tm_of_term fs ps b)
- | tm_of_term fs ps (Const(\<^const_name>\<open>Groups.times\<close>, _) $ a $ b) =
- @{code Mul} (num_of_term ps a, tm_of_term fs ps b)
+fun tm_of_term fs ps \<^Const_>\<open>uminus _ for t\<close> = @{code Neg} (tm_of_term fs ps t)
+ | tm_of_term fs ps \<^Const_>\<open>plus _ for a b\<close> = @{code Add} (tm_of_term fs ps a, tm_of_term fs ps b)
+ | tm_of_term fs ps \<^Const_>\<open>minus _ for a b\<close> = @{code Sub} (tm_of_term fs ps a, tm_of_term fs ps b)
+ | tm_of_term fs ps \<^Const_>\<open>times _ for a b\<close> = @{code Mul} (num_of_term ps a, tm_of_term fs ps b)
| tm_of_term fs ps t = (@{code CP} (num_of_term ps t)
handle TERM _ => mk_Bound (the_index fs t)
| General.Subscript => mk_Bound (the_index fs t));
-fun fm_of_term fs ps \<^term>\<open>True\<close> = @{code T}
- | fm_of_term fs ps \<^term>\<open>False\<close> = @{code F}
- | fm_of_term fs ps (Const (\<^const_name>\<open>HOL.Not\<close>, _) $ p) =
- @{code Not} (fm_of_term fs ps p)
- | fm_of_term fs ps (Const (\<^const_name>\<open>HOL.conj\<close>, _) $ p $ q) =
- @{code And} (fm_of_term fs ps p, fm_of_term fs ps q)
- | fm_of_term fs ps (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ p $ q) =
- @{code Or} (fm_of_term fs ps p, fm_of_term fs ps q)
- | fm_of_term fs ps (Const (\<^const_name>\<open>HOL.implies\<close>, _) $ p $ q) =
+fun fm_of_term fs ps \<^Const_>\<open>True\<close> = @{code T}
+ | fm_of_term fs ps \<^Const_>\<open>False\<close> = @{code F}
+ | fm_of_term fs ps \<^Const_>\<open>HOL.Not for p\<close> = @{code Not} (fm_of_term fs ps p)
+ | fm_of_term fs ps \<^Const_>\<open>HOL.conj for p q\<close> = @{code And} (fm_of_term fs ps p, fm_of_term fs ps q)
+ | fm_of_term fs ps \<^Const_>\<open>HOL.disj for p q\<close> = @{code Or} (fm_of_term fs ps p, fm_of_term fs ps q)
+ | fm_of_term fs ps \<^Const_>\<open>HOL.implies for p q\<close> =
@{code Imp} (fm_of_term fs ps p, fm_of_term fs ps q)
- | fm_of_term fs ps (\<^term>\<open>HOL.iff\<close> $ p $ q) =
+ | fm_of_term fs ps \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for p q\<close> =
@{code Iff} (fm_of_term fs ps p, fm_of_term fs ps q)
- | fm_of_term fs ps (Const (\<^const_name>\<open>HOL.eq\<close>, T) $ p $ q) =
+ | fm_of_term fs ps \<^Const_>\<open>HOL.eq _ for p q\<close> =
@{code Eq} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q))
- | fm_of_term fs ps (Const (\<^const_name>\<open>Orderings.less\<close>, _) $ p $ q) =
+ | fm_of_term fs ps \<^Const_>\<open>less _ for p q\<close> =
@{code Lt} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q))
- | fm_of_term fs ps (Const (\<^const_name>\<open>Orderings.less_eq\<close>, _) $ p $ q) =
+ | fm_of_term fs ps \<^Const_>\<open>less_eq _ for p q\<close> =
@{code Le} (@{code Sub} (tm_of_term fs ps p, tm_of_term fs ps q))
- | fm_of_term fs ps (Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (abs as (_, xT, _))) =
+ | fm_of_term fs ps (\<^Const_>\<open>Ex _\<close> $ Abs (abs as (_, xT, _))) =
let
val (xn', p') = Syntax_Trans.variant_abs abs; (* FIXME !? *)
in @{code E} (fm_of_term (Free (xn', xT) :: fs) ps p') end
- | fm_of_term fs ps (Const (\<^const_name>\<open>All\<close>,_) $ Abs (abs as (_, xT, _))) =
+ | fm_of_term fs ps (\<^Const_>\<open>All _\<close> $ Abs (abs as (_, xT, _))) =
let
val (xn', p') = Syntax_Trans.variant_abs abs; (* FIXME !? *)
in @{code A} (fm_of_term (Free (xn', xT) :: fs) ps p') end
@@ -4003,64 +3988,57 @@
let
val (c, d) = apply2 (@{code integer_of_int}) (a, b)
in
- (if d = 1 then HOLogic.mk_number T c
- else if d = 0 then Const (\<^const_name>\<open>Groups.zero\<close>, T)
- else
- Const (\<^const_name>\<open>Rings.divide\<close>, binopT T) $
- HOLogic.mk_number T c $ HOLogic.mk_number T d)
+ if d = 1 then HOLogic.mk_number T c
+ else if d = 0 then \<^Const>\<open>zero_class.zero T\<close>
+ else \<^Const>\<open>divide T for \<open>HOLogic.mk_number T c\<close> \<open>HOLogic.mk_number T d\<close>\<close>
end
| term_of_num T ps (@{code poly.Bound} i) = nth ps (@{code integer_of_nat} i)
| term_of_num T ps (@{code poly.Add} (a, b)) =
- Const (\<^const_name>\<open>Groups.plus\<close>, binopT T) $ term_of_num T ps a $ term_of_num T ps b
+ \<^Const>\<open>plus T for \<open>term_of_num T ps a\<close> \<open>term_of_num T ps b\<close>\<close>
| term_of_num T ps (@{code poly.Mul} (a, b)) =
- Const (\<^const_name>\<open>Groups.times\<close>, binopT T) $ term_of_num T ps a $ term_of_num T ps b
+ \<^Const>\<open>times T for \<open>term_of_num T ps a\<close> \<open>term_of_num T ps b\<close>\<close>
| term_of_num T ps (@{code poly.Sub} (a, b)) =
- Const (\<^const_name>\<open>Groups.minus\<close>, binopT T) $ term_of_num T ps a $ term_of_num T ps b
+ \<^Const>\<open>minus T for \<open>term_of_num T ps a\<close> \<open>term_of_num T ps b\<close>\<close>
| term_of_num T ps (@{code poly.Neg} a) =
- Const (\<^const_name>\<open>Groups.uminus\<close>, T --> T) $ term_of_num T ps a
+ \<^Const>\<open>uminus T for \<open>term_of_num T ps a\<close>\<close>
| term_of_num T ps (@{code poly.Pw} (a, n)) =
- Const (\<^const_name>\<open>Power.power\<close>, T --> \<^typ>\<open>nat\<close> --> T) $
- term_of_num T ps a $ HOLogic.mk_number HOLogic.natT (@{code integer_of_nat} n)
+ \<^Const>\<open>power T for \<open>term_of_num T ps a\<close> \<open>HOLogic.mk_number \<^Type>\<open>nat\<close> (@{code integer_of_nat} n)\<close>\<close>
| term_of_num T ps (@{code poly.CN} (c, n, p)) =
term_of_num T ps (@{code poly.Add} (c, @{code poly.Mul} (@{code poly.Bound} n, p)));
fun term_of_tm T fs ps (@{code CP} p) = term_of_num T ps p
| term_of_tm T fs ps (@{code Bound} i) = nth fs (@{code integer_of_nat} i)
| term_of_tm T fs ps (@{code Add} (a, b)) =
- Const (\<^const_name>\<open>Groups.plus\<close>, binopT T) $ term_of_tm T fs ps a $ term_of_tm T fs ps b
+ \<^Const>\<open>plus T for \<open>term_of_tm T fs ps a\<close> \<open>term_of_tm T fs ps b\<close>\<close>
| term_of_tm T fs ps (@{code Mul} (a, b)) =
- Const (\<^const_name>\<open>Groups.times\<close>, binopT T) $ term_of_num T ps a $ term_of_tm T fs ps b
+ \<^Const>\<open>times T for \<open>term_of_num T ps a\<close> \<open>term_of_tm T fs ps b\<close>\<close>
| term_of_tm T fs ps (@{code Sub} (a, b)) =
- Const (\<^const_name>\<open>Groups.minus\<close>, binopT T) $ term_of_tm T fs ps a $ term_of_tm T fs ps b
+ \<^Const>\<open>minus T for \<open>term_of_tm T fs ps a\<close> \<open>term_of_tm T fs ps b\<close>\<close>
| term_of_tm T fs ps (@{code Neg} a) =
- Const (\<^const_name>\<open>Groups.uminus\<close>, T --> T) $ term_of_tm T fs ps a
+ \<^Const>\<open>uminus T for \<open>term_of_tm T fs ps a\<close>\<close>
| term_of_tm T fs ps (@{code CNP} (n, c, p)) =
term_of_tm T fs ps (@{code Add} (@{code Mul} (c, @{code Bound} n), p));
-fun term_of_fm T fs ps @{code T} = \<^term>\<open>True\<close>
- | term_of_fm T fs ps @{code F} = \<^term>\<open>False\<close>
- | term_of_fm T fs ps (@{code Not} p) = \<^term>\<open>HOL.Not\<close> $ term_of_fm T fs ps p
+fun term_of_fm T fs ps @{code T} = \<^Const>\<open>True\<close>
+ | term_of_fm T fs ps @{code F} = \<^Const>\<open>False\<close>
+ | term_of_fm T fs ps (@{code Not} p) = \<^Const>\<open>HOL.Not for \<open>term_of_fm T fs ps p\<close>\<close>
| term_of_fm T fs ps (@{code And} (p, q)) =
- \<^term>\<open>HOL.conj\<close> $ term_of_fm T fs ps p $ term_of_fm T fs ps q
+ \<^Const>\<open>HOL.conj for \<open>term_of_fm T fs ps p\<close> \<open>term_of_fm T fs ps q\<close>\<close>
| term_of_fm T fs ps (@{code Or} (p, q)) =
- \<^term>\<open>HOL.disj\<close> $ term_of_fm T fs ps p $ term_of_fm T fs ps q
+ \<^Const>\<open>HOL.disj for \<open>term_of_fm T fs ps p\<close> \<open>term_of_fm T fs ps q\<close>\<close>
| term_of_fm T fs ps (@{code Imp} (p, q)) =
- \<^term>\<open>HOL.implies\<close> $ term_of_fm T fs ps p $ term_of_fm T fs ps q
+ \<^Const>\<open>HOL.implies for \<open>term_of_fm T fs ps p\<close> \<open>term_of_fm T fs ps q\<close>\<close>
| term_of_fm T fs ps (@{code Iff} (p, q)) =
- \<^term>\<open>HOL.iff\<close> $ term_of_fm T fs ps p $ term_of_fm T fs ps q
+ \<^Const>\<open>HOL.eq \<^Type>\<open>bool\<close> for \<open>term_of_fm T fs ps p\<close> \<open>term_of_fm T fs ps q\<close>\<close>
| term_of_fm T fs ps (@{code Lt} p) =
- Const (\<^const_name>\<open>Orderings.less\<close>, relT T) $
- term_of_tm T fs ps p $ Const (\<^const_name>\<open>Groups.zero\<close>, T)
+ \<^Const>\<open>less T for \<open>term_of_tm T fs ps p\<close> \<^Const>\<open>zero_class.zero T\<close>\<close>
| term_of_fm T fs ps (@{code Le} p) =
- Const (\<^const_name>\<open>Orderings.less_eq\<close>, relT T) $
- term_of_tm T fs ps p $ Const (\<^const_name>\<open>Groups.zero\<close>, T)
+ \<^Const>\<open>less_eq T for \<open>term_of_tm T fs ps p\<close> \<^Const>\<open>zero_class.zero T\<close>\<close>
| term_of_fm T fs ps (@{code Eq} p) =
- Const (\<^const_name>\<open>HOL.eq\<close>, relT T) $
- term_of_tm T fs ps p $ Const (\<^const_name>\<open>Groups.zero\<close>, T)
+ \<^Const>\<open>HOL.eq T for \<open>term_of_tm T fs ps p\<close> \<^Const>\<open>zero_class.zero T\<close>\<close>
| term_of_fm T fs ps (@{code NEq} p) =
- \<^term>\<open>Not\<close> $
- (Const (\<^const_name>\<open>HOL.eq\<close>, relT T) $
- term_of_tm T fs ps p $ Const (\<^const_name>\<open>Groups.zero\<close>, T))
+ \<^Const>\<open>Not for (* FIXME HOL.Not!? *)
+ \<^Const>\<open>HOL.eq T for \<open>term_of_tm T fs ps p\<close> \<^Const>\<open>zero_class.zero T\<close>\<close>\<close>
| term_of_fm T fs ps _ = error "term_of_fm: quantifiers";
fun frpar_procedure alternative T ps fm =
--- a/src/HOL/Decision_Procs/Reflective_Field.thy Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy Wed Sep 29 22:54:38 2021 +0200
@@ -619,23 +619,23 @@
qed
ML \<open>
-val term_of_nat = HOLogic.mk_number \<^typ>\<open>nat\<close> o @{code integer_of_nat};
+val term_of_nat = HOLogic.mk_number \<^Type>\<open>nat\<close> o @{code integer_of_nat};
-val term_of_int = HOLogic.mk_number \<^typ>\<open>int\<close> o @{code integer_of_int};
+val term_of_int = HOLogic.mk_number \<^Type>\<open>int\<close> o @{code integer_of_int};
-fun term_of_pexpr (@{code PExpr1} x) = \<^term>\<open>PExpr1\<close> $ term_of_pexpr1 x
- | term_of_pexpr (@{code PExpr2} x) = \<^term>\<open>PExpr2\<close> $ term_of_pexpr2 x
-and term_of_pexpr1 (@{code PCnst} k) = \<^term>\<open>PCnst\<close> $ term_of_int k
- | term_of_pexpr1 (@{code PVar} n) = \<^term>\<open>PVar\<close> $ term_of_nat n
- | term_of_pexpr1 (@{code PAdd} (x, y)) = \<^term>\<open>PAdd\<close> $ term_of_pexpr x $ term_of_pexpr y
- | term_of_pexpr1 (@{code PSub} (x, y)) = \<^term>\<open>PSub\<close> $ term_of_pexpr x $ term_of_pexpr y
- | term_of_pexpr1 (@{code PNeg} x) = \<^term>\<open>PNeg\<close> $ term_of_pexpr x
-and term_of_pexpr2 (@{code PMul} (x, y)) = \<^term>\<open>PMul\<close> $ term_of_pexpr x $ term_of_pexpr y
- | term_of_pexpr2 (@{code PPow} (x, n)) = \<^term>\<open>PPow\<close> $ term_of_pexpr x $ term_of_nat n
+fun term_of_pexpr (@{code PExpr1} x) = \<^Const>\<open>PExpr1\<close> $ term_of_pexpr1 x
+ | term_of_pexpr (@{code PExpr2} x) = \<^Const>\<open>PExpr2\<close> $ term_of_pexpr2 x
+and term_of_pexpr1 (@{code PCnst} k) = \<^Const>\<open>PCnst\<close> $ term_of_int k
+ | term_of_pexpr1 (@{code PVar} n) = \<^Const>\<open>PVar\<close> $ term_of_nat n
+ | term_of_pexpr1 (@{code PAdd} (x, y)) = \<^Const>\<open>PAdd\<close> $ term_of_pexpr x $ term_of_pexpr y
+ | term_of_pexpr1 (@{code PSub} (x, y)) = \<^Const>\<open>PSub\<close> $ term_of_pexpr x $ term_of_pexpr y
+ | term_of_pexpr1 (@{code PNeg} x) = \<^Const>\<open>PNeg\<close> $ term_of_pexpr x
+and term_of_pexpr2 (@{code PMul} (x, y)) = \<^Const>\<open>PMul\<close> $ term_of_pexpr x $ term_of_pexpr y
+ | term_of_pexpr2 (@{code PPow} (x, n)) = \<^Const>\<open>PPow\<close> $ term_of_pexpr x $ term_of_nat n
fun term_of_result (x, (y, zs)) =
HOLogic.mk_prod (term_of_pexpr x, HOLogic.mk_prod
- (term_of_pexpr y, HOLogic.mk_list \<^typ>\<open>pexpr\<close> (map term_of_pexpr zs)));
+ (term_of_pexpr y, HOLogic.mk_list \<^Type>\<open>pexpr\<close> (map term_of_pexpr zs)));
local
@@ -680,59 +680,47 @@
open Ring_Tac;
-fun field_struct (Const (\<^const_name>\<open>Ring.ring.add\<close>, _) $ R $ _ $ _) = SOME R
- | field_struct (Const (\<^const_name>\<open>Ring.a_minus\<close>, _) $ R $ _ $ _) = SOME R
- | field_struct (Const (\<^const_name>\<open>Group.monoid.mult\<close>, _) $ R $ _ $ _) = SOME R
- | field_struct (Const (\<^const_name>\<open>Ring.a_inv\<close>, _) $ R $ _) = SOME R
- | field_struct (Const (\<^const_name>\<open>Group.pow\<close>, _) $ R $ _ $ _) = SOME R
- | field_struct (Const (\<^const_name>\<open>Algebra_Aux.m_div\<close>, _) $ R $ _ $ _) = SOME R
- | field_struct (Const (\<^const_name>\<open>Ring.ring.zero\<close>, _) $ R) = SOME R
- | field_struct (Const (\<^const_name>\<open>Group.monoid.one\<close>, _) $ R) = SOME R
- | field_struct (Const (\<^const_name>\<open>Algebra_Aux.of_integer\<close>, _) $ R $ _) = SOME R
+fun field_struct \<^Const_>\<open>Ring.ring.add _ _ for R _ _\<close> = SOME R
+ | field_struct \<^Const_>\<open>Ring.a_minus _ _ for R _ _\<close> = SOME R
+ | field_struct \<^Const_>\<open>Group.monoid.mult _ _ for R _ _\<close> = SOME R
+ | field_struct \<^Const_>\<open>Ring.a_inv _ _ for R _\<close> = SOME R
+ | field_struct \<^Const_>\<open>Group.pow _ _ _ for R _ _\<close> = SOME R
+ | field_struct \<^Const_>\<open>Algebra_Aux.m_div _ _for R _ _\<close> = SOME R
+ | field_struct \<^Const_>\<open>Ring.ring.zero _ _ for R\<close> = SOME R
+ | field_struct \<^Const_>\<open>Group.monoid.one _ _ for R\<close> = SOME R
+ | field_struct \<^Const_>\<open>Algebra_Aux.of_integer _ _ for R _\<close> = SOME R
| field_struct _ = NONE;
-fun reif_fexpr vs (Const (\<^const_name>\<open>Ring.ring.add\<close>, _) $ _ $ a $ b) =
- \<^const>\<open>FAdd\<close> $ reif_fexpr vs a $ reif_fexpr vs b
- | reif_fexpr vs (Const (\<^const_name>\<open>Ring.a_minus\<close>, _) $ _ $ a $ b) =
- \<^const>\<open>FSub\<close> $ reif_fexpr vs a $ reif_fexpr vs b
- | reif_fexpr vs (Const (\<^const_name>\<open>Group.monoid.mult\<close>, _) $ _ $ a $ b) =
- \<^const>\<open>FMul\<close> $ reif_fexpr vs a $ reif_fexpr vs b
- | reif_fexpr vs (Const (\<^const_name>\<open>Ring.a_inv\<close>, _) $ _ $ a) =
- \<^const>\<open>FNeg\<close> $ reif_fexpr vs a
- | reif_fexpr vs (Const (\<^const_name>\<open>Group.pow\<close>, _) $ _ $ a $ n) =
- \<^const>\<open>FPow\<close> $ reif_fexpr vs a $ n
- | reif_fexpr vs (Const (\<^const_name>\<open>Algebra_Aux.m_div\<close>, _) $ _ $ a $ b) =
- \<^const>\<open>FDiv\<close> $ reif_fexpr vs a $ reif_fexpr vs b
+fun reif_fexpr vs \<^Const_>\<open>Ring.ring.add _ _ for _ a b\<close> =
+ \<^Const>\<open>FAdd for \<open>reif_fexpr vs a\<close> \<open>reif_fexpr vs b\<close>\<close>
+ | reif_fexpr vs \<^Const_>\<open>Ring.a_minus _ _ for _ a b\<close> =
+ \<^Const>\<open>FSub for \<open>reif_fexpr vs a\<close> \<open>reif_fexpr vs b\<close>\<close>
+ | reif_fexpr vs \<^Const_>\<open>Group.monoid.mult _ _ for _ a b\<close> =
+ \<^Const>\<open>FMul for \<open>reif_fexpr vs a\<close> \<open>reif_fexpr vs b\<close>\<close>
+ | reif_fexpr vs \<^Const_>\<open>Ring.a_inv _ _ for _ a\<close> =
+ \<^Const>\<open>FNeg for \<open>reif_fexpr vs a\<close>\<close>
+ | reif_fexpr vs \<^Const>\<open>Group.pow _ _ _ for _ a n\<close> =
+ \<^Const>\<open>FPow for \<open>reif_fexpr vs a\<close> n\<close>
+ | reif_fexpr vs \<^Const_>\<open>Algebra_Aux.m_div _ _ for _ a b\<close> =
+ \<^Const>\<open>FDiv for \<open>reif_fexpr vs a\<close> \<open>reif_fexpr vs b\<close>\<close>
| reif_fexpr vs (Free x) =
- \<^const>\<open>FVar\<close> $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)
- | reif_fexpr vs (Const (\<^const_name>\<open>Ring.ring.zero\<close>, _) $ _) =
- \<^term>\<open>FCnst 0\<close>
- | reif_fexpr vs (Const (\<^const_name>\<open>Group.monoid.one\<close>, _) $ _) =
- \<^term>\<open>FCnst 1\<close>
- | reif_fexpr vs (Const (\<^const_name>\<open>Algebra_Aux.of_integer\<close>, _) $ _ $ n) =
- \<^const>\<open>FCnst\<close> $ n
+ \<^Const>\<open>FVar for \<open>HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)\<close>\<close>
+ | reif_fexpr vs \<^Const_>\<open>Ring.ring.zero _ _ for _\<close> = \<^term>\<open>FCnst 0\<close>
+ | reif_fexpr vs \<^Const_>\<open>Group.monoid.one _ _ for _\<close> = \<^term>\<open>FCnst 1\<close>
+ | reif_fexpr vs \<^Const_>\<open>Algebra_Aux.of_integer _ _ for _ n\<close> = \<^Const>\<open>FCnst for n\<close>
| reif_fexpr _ _ = error "reif_fexpr: bad expression";
-fun reif_fexpr' vs (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ a $ b) =
- \<^const>\<open>FAdd\<close> $ reif_fexpr' vs a $ reif_fexpr' vs b
- | reif_fexpr' vs (Const (\<^const_name>\<open>Groups.minus\<close>, _) $ a $ b) =
- \<^const>\<open>FSub\<close> $ reif_fexpr' vs a $ reif_fexpr' vs b
- | reif_fexpr' vs (Const (\<^const_name>\<open>Groups.times\<close>, _) $ a $ b) =
- \<^const>\<open>FMul\<close> $ reif_fexpr' vs a $ reif_fexpr' vs b
- | reif_fexpr' vs (Const (\<^const_name>\<open>Groups.uminus\<close>, _) $ a) =
- \<^const>\<open>FNeg\<close> $ reif_fexpr' vs a
- | reif_fexpr' vs (Const (\<^const_name>\<open>Power.power\<close>, _) $ a $ n) =
- \<^const>\<open>FPow\<close> $ reif_fexpr' vs a $ n
- | reif_fexpr' vs (Const (\<^const_name>\<open>divide\<close>, _) $ a $ b) =
- \<^const>\<open>FDiv\<close> $ reif_fexpr' vs a $ reif_fexpr' vs b
+fun reif_fexpr' vs \<^Const_>\<open>plus _ for a b\<close> = \<^Const>\<open>FAdd for \<open>reif_fexpr' vs a\<close> \<open>reif_fexpr' vs b\<close>\<close>
+ | reif_fexpr' vs \<^Const_>\<open>minus _ for a b\<close> = \<^Const>\<open>FSub for \<open>reif_fexpr' vs a\<close> \<open>reif_fexpr' vs b\<close>\<close>
+ | reif_fexpr' vs \<^Const_>\<open>times _ for a b\<close> = \<^Const>\<open>FMul for \<open>reif_fexpr' vs a\<close> \<open>reif_fexpr' vs b\<close>\<close>
+ | reif_fexpr' vs \<^Const_>\<open>uminus _ for a\<close> = \<^Const>\<open>FNeg for \<open>reif_fexpr' vs a\<close>\<close>
+ | reif_fexpr' vs \<^Const_>\<open>power _ for a n\<close> = \<^Const>\<open>FPow for \<open>reif_fexpr' vs a\<close> n\<close>
+ | reif_fexpr' vs \<^Const_>\<open>divide _ for a b\<close> = \<^Const>\<open>FDiv for \<open>reif_fexpr' vs a\<close> \<open>reif_fexpr' vs b\<close>\<close>
| reif_fexpr' vs (Free x) =
- \<^const>\<open>FVar\<close> $ HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)
- | reif_fexpr' vs (Const (\<^const_name>\<open>zero_class.zero\<close>, _)) =
- \<^term>\<open>FCnst 0\<close>
- | reif_fexpr' vs (Const (\<^const_name>\<open>one_class.one\<close>, _)) =
- \<^term>\<open>FCnst 1\<close>
- | reif_fexpr' vs (Const (\<^const_name>\<open>numeral\<close>, _) $ b) =
- \<^const>\<open>FCnst\<close> $ (@{const numeral (int)} $ b)
+ \<^Const>\<open>FVar for \<open>HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)\<close>\<close>
+ | reif_fexpr' vs \<^Const_>\<open>zero_class.zero _\<close> = \<^term>\<open>FCnst 0\<close>
+ | reif_fexpr' vs \<^Const_>\<open>one_class.one _\<close> = \<^term>\<open>FCnst 1\<close>
+ | reif_fexpr' vs \<^Const_>\<open>numeral _ for b\<close> = \<^Const>\<open>FCnst for \<^Const>\<open>numeral \<^Type>\<open>int\<close> for b\<close>\<close>
| reif_fexpr' _ _ = error "reif_fexpr: bad expression";
fun eq_field_simps
@@ -861,7 +849,7 @@
fun conv xs qs = (case strip_app qs of
(\<^const_name>\<open>Nil\<close>, []) => inst [] [xs] nonzero_Nil
| (\<^const_name>\<open>Cons\<close>, [p, ps]) => (case Thm.term_of ps of
- Const (\<^const_name>\<open>Nil\<close>, _) =>
+ \<^Const_>\<open>Nil _\<close> =>
transitive' (inst [] [xs, p] nonzero_singleton)
(cong1 (cong2 (args2 peval_conv') Thm.reflexive))
| _ => transitive' (inst [] [xs, p, ps] nonzero_Cons)
@@ -873,7 +861,7 @@
let
val (prems, concl) = Logic.strip_horn g;
fun find_eq s = (case s of
- (_ $ (Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _])) $ t $ u)) =>
+ (_ $ \<^Const_>\<open>HOL.eq T for t u\<close>) =>
(case (field_struct t, field_struct u) of
(SOME R, _) => SOME ((t, u), R, T, NONE, mk_in_carrier ctxt R [], reif_fexpr)
| (_, SOME R) => SOME ((t, u), R, T, NONE, mk_in_carrier ctxt R [], reif_fexpr)
--- a/src/HOL/Decision_Procs/approximation.ML Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/approximation.ML Wed Sep 29 22:54:38 2021 +0200
@@ -15,12 +15,8 @@
fun reorder_bounds_tac ctxt prems i =
let
- fun variable_of_bound (Const (\<^const_name>\<open>Trueprop\<close>, _) $
- (Const (\<^const_name>\<open>Set.member\<close>, _) $
- Free (name, _) $ _)) = name
- | variable_of_bound (Const (\<^const_name>\<open>Trueprop\<close>, _) $
- (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
- Free (name, _) $ _)) = name
+ fun variable_of_bound \<^Const_>\<open>Trueprop for \<^Const_>\<open>Set.member _ for \<open>Free (name, _)\<close> _\<close>\<close> = name
+ | variable_of_bound \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for \<open>Free (name, _)\<close> _\<close>\<close> = name
| variable_of_bound t = raise TERM ("variable_of_bound", [t])
val variable_bounds
@@ -43,18 +39,18 @@
end
fun approximate ctxt t = case fastype_of t
- of \<^typ>\<open>bool\<close> =>
+ of \<^Type>\<open>bool\<close> =>
Approximation_Computation.approx_bool ctxt t
- | \<^typ>\<open>(float interval) option\<close> =>
+ | \<^typ>\<open>float interval option\<close> =>
Approximation_Computation.approx_arith ctxt t
- | \<^typ>\<open>(float interval) option list\<close> =>
+ | \<^typ>\<open>float interval option list\<close> =>
Approximation_Computation.approx_form_eval ctxt t
| _ => error ("Bad term: " ^ Syntax.string_of_term ctxt t);
fun rewrite_interpret_form_tac ctxt prec splitting taylor i st = let
fun lookup_splitting (Free (name, _)) =
(case AList.lookup (op =) splitting name
- of SOME s => HOLogic.mk_number \<^typ>\<open>nat\<close> s
+ of SOME s => HOLogic.mk_number \<^Type>\<open>nat\<close> s
| NONE => \<^term>\<open>0 :: nat\<close>)
| lookup_splitting t = raise TERM ("lookup_splitting", [t])
val vs = nth (Thm.prems_of st) (i - 1)
@@ -63,16 +59,16 @@
|> Term.strip_comb |> snd |> List.last
|> HOLogic.dest_list
val p = prec
- |> HOLogic.mk_number \<^typ>\<open>nat\<close>
+ |> HOLogic.mk_number \<^Type>\<open>nat\<close>
|> Thm.cterm_of ctxt
in case taylor
of NONE => let
val n = vs |> length
- |> HOLogic.mk_number \<^typ>\<open>nat\<close>
+ |> HOLogic.mk_number \<^Type>\<open>nat\<close>
|> Thm.cterm_of ctxt
val s = vs
|> map lookup_splitting
- |> HOLogic.mk_list \<^typ>\<open>nat\<close>
+ |> HOLogic.mk_list \<^Type>\<open>nat\<close>
|> Thm.cterm_of ctxt
in
(resolve_tac ctxt [Thm.instantiate (TVars.empty,
@@ -86,7 +82,7 @@
then raise (TERM ("More than one variable used for taylor series expansion", [Thm.prop_of st]))
else let
val t = t
- |> HOLogic.mk_number \<^typ>\<open>nat\<close>
+ |> HOLogic.mk_number \<^Type>\<open>nat\<close>
|> Thm.cterm_of ctxt
val s = vs |> map lookup_splitting |> hd
|> Thm.cterm_of ctxt
@@ -97,42 +93,38 @@
end
end
-fun calculated_subterms (\<^const>\<open>Trueprop\<close> $ t) = calculated_subterms t
- | calculated_subterms (\<^const>\<open>HOL.implies\<close> $ _ $ t) = calculated_subterms t
- | calculated_subterms (\<^term>\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) = [t1, t2]
- | calculated_subterms (\<^term>\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ t1 $ t2) = [t1, t2]
- | calculated_subterms (\<^term>\<open>(\<in>) :: real \<Rightarrow> real set \<Rightarrow> bool\<close> $ t1 $
- (\<^term>\<open>atLeastAtMost :: real \<Rightarrow> real \<Rightarrow> real set\<close> $ t2 $ t3)) = [t1, t2, t3]
+fun calculated_subterms \<^Const_>\<open>Trueprop for t\<close> = calculated_subterms t
+ | calculated_subterms \<^Const_>\<open>implies for _ t\<close> = calculated_subterms t
+ | calculated_subterms \<^Const_>\<open>less_eq \<^Type>\<open>real\<close> for t1 t2\<close> = [t1, t2]
+ | calculated_subterms \<^Const_>\<open>less \<^Type>\<open>real\<close> for t1 t2\<close> = [t1, t2]
+ | calculated_subterms \<^Const_>\<open>Set.member \<^Type>\<open>real\<close> for
+ t1 \<^Const_>\<open>atLeastAtMost \<^Type>\<open>real\<close> for t2 t3\<close>\<close> = [t1, t2, t3]
| calculated_subterms t = raise TERM ("calculated_subterms", [t])
-fun dest_interpret_form (\<^const>\<open>interpret_form\<close> $ b $ xs) = (b, xs)
+fun dest_interpret_form \<^Const_>\<open>interpret_form for b xs\<close> = (b, xs)
| dest_interpret_form t = raise TERM ("dest_interpret_form", [t])
-fun dest_interpret (\<^const>\<open>interpret_floatarith\<close> $ b $ xs) = (b, xs)
+fun dest_interpret \<^Const_>\<open>interpret_floatarith for b xs\<close> = (b, xs)
| dest_interpret t = raise TERM ("dest_interpret", [t])
-fun dest_interpret_env (\<^const>\<open>interpret_form\<close> $ _ $ xs) = xs
- | dest_interpret_env (\<^const>\<open>interpret_floatarith\<close> $ _ $ xs) = xs
+fun dest_interpret_env \<^Const_>\<open>interpret_form for _ xs\<close> = xs
+ | dest_interpret_env \<^Const_>\<open>interpret_floatarith for _ xs\<close> = xs
| dest_interpret_env t = raise TERM ("dest_interpret_env", [t])
-fun dest_float (\<^const>\<open>Float\<close> $ m $ e) = (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
+fun dest_float \<^Const_>\<open>Float for m e\<close> = (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
| dest_float t = raise TERM ("dest_float", [t])
-fun dest_ivl
- (Const (\<^const_name>\<open>Some\<close>, _) $
- (Const (\<^const_name>\<open>Interval\<close>, _) $ ((Const (\<^const_name>\<open>Pair\<close>, _) $ u $ l)))) =
+fun dest_ivl \<^Const_>\<open>Some _ for \<^Const_>\<open>Interval _ for \<^Const_>\<open>Pair _ _ for u l\<close>\<close>\<close> =
SOME (dest_float u, dest_float l)
- | dest_ivl (Const (\<^const_name>\<open>None\<close>, _)) = NONE
+ | dest_ivl \<^Const_>\<open>None _\<close> = NONE
| dest_ivl t = raise TERM ("dest_result", [t])
-fun mk_approx' prec t = (\<^const>\<open>approx'\<close>
- $ HOLogic.mk_number \<^typ>\<open>nat\<close> prec
- $ t $ \<^term>\<open>[] :: (float interval) option list\<close>)
+fun mk_approx' prec t =
+ \<^Const>\<open>approx' for \<open>HOLogic.mk_number \<^Type>\<open>nat\<close> prec\<close> t \<^Const>\<open>Nil \<^typ>\<open>float interval option\<close>\<close>\<close>
-fun mk_approx_form_eval prec t xs = (\<^const>\<open>approx_form_eval\<close>
- $ HOLogic.mk_number \<^typ>\<open>nat\<close> prec
- $ t $ xs)
+fun mk_approx_form_eval prec t xs =
+ \<^Const>\<open>approx_form_eval for \<open>HOLogic.mk_number \<^Type>\<open>nat\<close> prec\<close> t xs\<close>
fun float2_float10 prec round_down (m, e) = (
let
@@ -166,21 +158,21 @@
fun mk_result prec (SOME (l, u)) =
(let
fun mk_float10 rnd x = (let val (m, e) = float2_float10 prec rnd x
- in if e = 0 then HOLogic.mk_number \<^typ>\<open>real\<close> m
- else if e = 1 then \<^term>\<open>divide :: real \<Rightarrow> real \<Rightarrow> real\<close> $
- HOLogic.mk_number \<^typ>\<open>real\<close> m $
+ in if e = 0 then HOLogic.mk_number \<^Type>\<open>real\<close> m
+ else if e = 1 then \<^Const>\<open>divide \<^Type>\<open>real\<close>\<close> $
+ HOLogic.mk_number \<^Type>\<open>real\<close> m $
\<^term>\<open>10\<close>
- else \<^term>\<open>divide :: real \<Rightarrow> real \<Rightarrow> real\<close> $
- HOLogic.mk_number \<^typ>\<open>real\<close> m $
+ else \<^Const>\<open>divide \<^Type>\<open>real\<close>\<close> $
+ HOLogic.mk_number \<^Type>\<open>real\<close> m $
(\<^term>\<open>power 10 :: nat \<Rightarrow> real\<close> $
- HOLogic.mk_number \<^typ>\<open>nat\<close> (~e)) end)
- in \<^term>\<open>atLeastAtMost :: real \<Rightarrow> real \<Rightarrow> real set\<close> $ mk_float10 true l $ mk_float10 false u end)
+ HOLogic.mk_number \<^Type>\<open>nat\<close> (~e)) end)
+ in \<^Const>\<open>atLeastAtMost \<^Type>\<open>real\<close> for \<open>mk_float10 true l\<close> \<open>mk_float10 false u\<close>\<close> end)
| mk_result _ NONE = \<^term>\<open>UNIV :: real set\<close>
fun realify t =
let
val t = Logic.varify_global t
- val m = map (fn (name, _) => (name, \<^typ>\<open>real\<close>)) (Term.add_tvars t [])
+ val m = map (fn (name, _) => (name, \<^Type>\<open>real\<close>)) (Term.add_tvars t [])
val t = Term.subst_TVars m t
in t end
@@ -237,12 +229,12 @@
|> HOLogic.dest_Trueprop
|> dest_interpret_form
|> (fn (data, xs) =>
- mk_approx_form_eval prec data (HOLogic.mk_list \<^typ>\<open>(float interval) option\<close>
- (map (fn _ => \<^term>\<open>None :: (float interval) option\<close>) (HOLogic.dest_list xs)))
+ mk_approx_form_eval prec data (HOLogic.mk_list \<^typ>\<open>float interval option\<close>
+ (map (fn _ => \<^Const>\<open>None \<^typ>\<open>float interval option\<close>\<close>) (HOLogic.dest_list xs)))
|> approximate ctxt
|> HOLogic.dest_list
|> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term)
- |> map (fn (elem, s) => \<^term>\<open>(\<in>) :: real \<Rightarrow> real set \<Rightarrow> bool\<close> $ elem $ mk_result prec (dest_ivl s))
+ |> map (fn (elem, s) => \<^Const>\<open>Set.member \<^Type>\<open>real\<close> for elem \<open>mk_result prec (dest_ivl s)\<close>\<close>)
|> foldr1 HOLogic.mk_conj))
fun approx_arith prec ctxt t = realify t
@@ -257,8 +249,8 @@
|> mk_result prec
fun approx prec ctxt t =
- if type_of t = \<^typ>\<open>prop\<close> then approx_form prec ctxt t
- else if type_of t = \<^typ>\<open>bool\<close> then approx_form prec ctxt (\<^const>\<open>Trueprop\<close> $ t)
+ if type_of t = \<^Type>\<open>prop\<close> then approx_form prec ctxt t
+ else if type_of t = \<^Type>\<open>bool\<close> then approx_form prec ctxt \<^Const>\<open>Trueprop for t\<close>
else approx_arith prec ctxt t
fun approximate_cmd modes raw_t state =
--- a/src/HOL/Decision_Procs/approximation_generator.ML Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/approximation_generator.ML Wed Sep 29 22:54:38 2021 +0200
@@ -33,33 +33,33 @@
fun real_of_man_exp m e = Real.fromManExp {man = Real.fromInt m, exp = e}
-fun mapprox_float (\<^term>\<open>Float\<close> $ m $ e) = real_of_man_exp (int_of_term m) (int_of_term e)
+fun mapprox_float \<^Const_>\<open>Float for m e\<close> = real_of_man_exp (int_of_term m) (int_of_term e)
| mapprox_float t = Real.fromInt (snd (HOLogic.dest_number t))
handle TERM _ => raise TERM ("mapprox_float", [t]);
(* TODO: define using compiled terms? *)
-fun mapprox_floatarith (\<^term>\<open>Add\<close> $ a $ b) xs = mapprox_floatarith a xs + mapprox_floatarith b xs
- | mapprox_floatarith (\<^term>\<open>Minus\<close> $ a) xs = ~ (mapprox_floatarith a xs)
- | mapprox_floatarith (\<^term>\<open>Mult\<close> $ a $ b) xs = mapprox_floatarith a xs * mapprox_floatarith b xs
- | mapprox_floatarith (\<^term>\<open>Inverse\<close> $ a) xs = 1.0 / mapprox_floatarith a xs
- | mapprox_floatarith (\<^term>\<open>Cos\<close> $ a) xs = Math.cos (mapprox_floatarith a xs)
- | mapprox_floatarith (\<^term>\<open>Arctan\<close> $ a) xs = Math.atan (mapprox_floatarith a xs)
- | mapprox_floatarith (\<^term>\<open>Abs\<close> $ a) xs = abs (mapprox_floatarith a xs)
- | mapprox_floatarith (\<^term>\<open>Max\<close> $ a $ b) xs =
+fun mapprox_floatarith \<^Const_>\<open>Add for a b\<close> xs = mapprox_floatarith a xs + mapprox_floatarith b xs
+ | mapprox_floatarith \<^Const_>\<open>Minus for a\<close> xs = ~ (mapprox_floatarith a xs)
+ | mapprox_floatarith \<^Const_>\<open>Mult for a b\<close> xs = mapprox_floatarith a xs * mapprox_floatarith b xs
+ | mapprox_floatarith \<^Const_>\<open>Inverse for a\<close> xs = 1.0 / mapprox_floatarith a xs
+ | mapprox_floatarith \<^Const_>\<open>Cos for a\<close> xs = Math.cos (mapprox_floatarith a xs)
+ | mapprox_floatarith \<^Const_>\<open>Arctan for a\<close> xs = Math.atan (mapprox_floatarith a xs)
+ | mapprox_floatarith \<^Const_>\<open>Abs for a\<close> xs = abs (mapprox_floatarith a xs)
+ | mapprox_floatarith \<^Const_>\<open>Max for a b\<close> xs =
Real.max (mapprox_floatarith a xs, mapprox_floatarith b xs)
- | mapprox_floatarith (\<^term>\<open>Min\<close> $ a $ b) xs =
+ | mapprox_floatarith \<^Const_>\<open>Min for a b\<close> xs =
Real.min (mapprox_floatarith a xs, mapprox_floatarith b xs)
- | mapprox_floatarith \<^term>\<open>Pi\<close> _ = Math.pi
- | mapprox_floatarith (\<^term>\<open>Sqrt\<close> $ a) xs = Math.sqrt (mapprox_floatarith a xs)
- | mapprox_floatarith (\<^term>\<open>Exp\<close> $ a) xs = Math.exp (mapprox_floatarith a xs)
- | mapprox_floatarith (\<^term>\<open>Powr\<close> $ a $ b) xs =
+ | mapprox_floatarith \<^Const_>\<open>Pi\<close> _ = Math.pi
+ | mapprox_floatarith \<^Const_>\<open>Sqrt for a\<close> xs = Math.sqrt (mapprox_floatarith a xs)
+ | mapprox_floatarith \<^Const_>\<open>Exp for a\<close> xs = Math.exp (mapprox_floatarith a xs)
+ | mapprox_floatarith \<^Const_>\<open>Powr for a b\<close> xs =
Math.pow (mapprox_floatarith a xs, mapprox_floatarith b xs)
- | mapprox_floatarith (\<^term>\<open>Ln\<close> $ a) xs = Math.ln (mapprox_floatarith a xs)
- | mapprox_floatarith (\<^term>\<open>Power\<close> $ a $ n) xs =
+ | mapprox_floatarith \<^Const_>\<open>Ln for a\<close> xs = Math.ln (mapprox_floatarith a xs)
+ | mapprox_floatarith \<^Const_>\<open>Power for a n\<close> xs =
Math.pow (mapprox_floatarith a xs, Real.fromInt (nat_of_term n))
- | mapprox_floatarith (\<^term>\<open>Floor\<close> $ a) xs = Real.fromInt (floor (mapprox_floatarith a xs))
- | mapprox_floatarith (\<^term>\<open>Var\<close> $ n) xs = nth xs (nat_of_term n)
- | mapprox_floatarith (\<^term>\<open>Num\<close> $ m) _ = mapprox_float m
+ | mapprox_floatarith \<^Const_>\<open>Floor for a\<close> xs = Real.fromInt (floor (mapprox_floatarith a xs))
+ | mapprox_floatarith \<^Const_>\<open>Var for n\<close> xs = nth xs (nat_of_term n)
+ | mapprox_floatarith \<^Const_>\<open>Num for m\<close> _ = mapprox_float m
| mapprox_floatarith t _ = raise TERM ("mapprox_floatarith", [t])
fun mapprox_atLeastAtMost eps x a b xs =
@@ -69,23 +69,20 @@
mapprox_floatarith a xs + eps <= x' andalso x' + eps <= mapprox_floatarith b xs
end
-fun mapprox_form eps (\<^term>\<open>Bound\<close> $ x $ a $ b $ f) xs =
+fun mapprox_form eps \<^Const_>\<open>Bound for x a b f\<close> xs =
(not (mapprox_atLeastAtMost eps x a b xs)) orelse mapprox_form eps f xs
-| mapprox_form eps (\<^term>\<open>Assign\<close> $ x $ a $ f) xs =
+| mapprox_form eps \<^Const_>\<open>Assign for x a f\<close> xs =
(Real.!= (mapprox_floatarith x xs, mapprox_floatarith a xs)) orelse mapprox_form eps f xs
-| mapprox_form eps (\<^term>\<open>Less\<close> $ a $ b) xs = mapprox_floatarith a xs + eps < mapprox_floatarith b xs
-| mapprox_form eps (\<^term>\<open>LessEqual\<close> $ a $ b) xs = mapprox_floatarith a xs + eps <= mapprox_floatarith b xs
-| mapprox_form eps (\<^term>\<open>AtLeastAtMost\<close> $ x $ a $ b) xs = mapprox_atLeastAtMost eps x a b xs
-| mapprox_form eps (\<^term>\<open>Conj\<close> $ f $ g) xs = mapprox_form eps f xs andalso mapprox_form eps g xs
-| mapprox_form eps (\<^term>\<open>Disj\<close> $ f $ g) xs = mapprox_form eps f xs orelse mapprox_form eps g xs
+| mapprox_form eps \<^Const_>\<open>Less for a b\<close> xs = mapprox_floatarith a xs + eps < mapprox_floatarith b xs
+| mapprox_form eps \<^Const_>\<open>LessEqual for a b\<close> xs = mapprox_floatarith a xs + eps <= mapprox_floatarith b xs
+| mapprox_form eps \<^Const_>\<open>AtLeastAtMost for x a b\<close> xs = mapprox_atLeastAtMost eps x a b xs
+| mapprox_form eps \<^Const_>\<open>Conj for f g\<close> xs = mapprox_form eps f xs andalso mapprox_form eps g xs
+| mapprox_form eps \<^Const_>\<open>Disj for f g\<close> xs = mapprox_form eps f xs orelse mapprox_form eps g xs
| mapprox_form _ t _ = raise TERM ("mapprox_form", [t])
-fun dest_interpret_form (\<^const>\<open>interpret_form\<close> $ b $ xs) = (b, xs)
+fun dest_interpret_form \<^Const_>\<open>interpret_form for b xs\<close> = (b, xs)
| dest_interpret_form t = raise TERM ("dest_interpret_form", [t])
-fun optionT t = Type (\<^type_name>\<open>option\<close>, [t])
-fun mk_Some t = Const (\<^const_name>\<open>Some\<close>, t --> optionT t)
-
fun random_float_list size xs seed =
fold (K (apsnd (random_float size) #-> (fn c => apfst (fn b => b::c)))) xs ([],seed)
@@ -96,7 +93,7 @@
fun term_of_Float (@{code Float} (m, e)) = @{term Float} $ term_of_int m $ term_of_int e
-fun is_True \<^term>\<open>True\<close> = true
+fun is_True \<^Const_>\<open>True\<close> = true
| is_True _ = false
val postproc_form_eqs =
@@ -130,12 +127,12 @@
let
val (rs, seed') = random_float_list size xs seed
fun mk_approx_form e ts =
- \<^const>\<open>approx_form\<close> $
- HOLogic.mk_number \<^typ>\<open>nat\<close> prec $
+ \<^Const>\<open>approx_form\<close> $
+ HOLogic.mk_number \<^Type>\<open>nat\<close> prec $
e $
- (HOLogic.mk_list \<^typ>\<open>(float interval) option\<close>
- (map (fn t => mk_Some \<^typ>\<open>float interval\<close> $ (\<^term>\<open>interval_of::float\<Rightarrow>_\<close> $ t)) ts)) $
- \<^term>\<open>[] :: nat list\<close>
+ (HOLogic.mk_list \<^typ>\<open>float interval option\<close>
+ (map (fn t => \<^Const>\<open>Some \<^typ>\<open>float interval\<close>\<close> $ \<^Const>\<open>interval_of \<^Type>\<open>float\<close> for t\<close>) ts)) $
+ \<^Const>\<open>Nil \<^Type>\<open>nat\<close>\<close>
in
(if
mapprox_form eps e (map (real_of_Float o fst) rs)
@@ -150,7 +147,7 @@
val ts' = map
(AList.lookup op = (map dest_Free xs ~~ ts)
#> the_default Term.dummy
- #> curry op $ \<^term>\<open>real_of_float::float\<Rightarrow>_\<close>
+ #> curry op $ \<^Const>\<open>real_of_float\<close>
#> conv_term ctxt (rewrite_with ctxt postproc_form_eqs))
frees
in
--- a/src/HOL/Decision_Procs/cooper_tac.ML Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Wed Sep 29 22:54:38 2021 +0200
@@ -26,7 +26,7 @@
val np = length ps
val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
(List.foldr HOLogic.mk_imp c rhs, np) ps
- val (vs, _) = List.partition (fn t => q orelse (type_of t) = \<^typ>\<open>nat\<close>)
+ val (vs, _) = List.partition (fn t => q orelse (type_of t) = \<^Type>\<open>nat\<close>)
(Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm');
val fm2 = List.foldr mk_all2 fm' vs
in (fm2, np + length vs, length rhs) end;
@@ -84,7 +84,7 @@
(* The result of the quantifier elimination *)
val (th, tac) =
(case Thm.prop_of pre_thm of
- Const (\<^const_name>\<open>Pure.imp\<close>, _) $ (Const (\<^const_name>\<open>Trueprop\<close>, _) $ t1) $ _ =>
+ \<^Const_>\<open>Pure.imp for \<^Const_>\<open>Trueprop for t1\<close> _\<close> =>
let
val pth = linzqe_oracle (ctxt, Envir.eta_long [] t1)
in
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Wed Sep 29 22:54:38 2021 +0200
@@ -63,7 +63,7 @@
fun assm_tac i = REPEAT_DETERM_N nh (assume_tac ctxt i)
(* The result of the quantifier elimination *)
val (th, tac) = case Thm.prop_of pre_thm of
- Const (\<^const_name>\<open>Pure.imp\<close>, _) $ (Const (\<^const_name>\<open>Trueprop\<close>, _) $ t1) $ _ =>
+ \<^Const_>\<open>Pure.imp for \<^Const_>\<open>Trueprop for t1\<close> _\<close> =>
let val pth = linr_oracle (ctxt, Envir.eta_long [] t1)
in
((pth RS iffD2) RS pre_thm,
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Wed Sep 29 22:54:38 2021 +0200
@@ -33,12 +33,12 @@
{isolate_conv = icv, whatis = wi, simpset = simpset}):entry) =
let
fun uset (vars as (x::vs)) p = case Thm.term_of p of
- Const(\<^const_name>\<open>HOL.conj\<close>, _)$ _ $ _ =>
+ \<^Const_>\<open>HOL.conj for _ _\<close> =>
let
val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
val (lS,lth) = uset vars l val (rS, rth) = uset vars r
in (lS@rS, Drule.binop_cong_rule b lth rth) end
- | Const(\<^const_name>\<open>HOL.disj\<close>, _)$ _ $ _ =>
+ | \<^Const_>\<open>HOL.disj for _ _\<close> =>
let
val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
val (lS,lth) = uset vars l val (rS, rth) = uset vars r
@@ -78,7 +78,7 @@
fun main vs p =
let
val ((xn,ce),(x,fm)) = (case Thm.term_of p of
- Const(\<^const_name>\<open>Ex\<close>,_)$Abs(xn,xT,_) =>
+ \<^Const_>\<open>Ex _ for \<open>Abs(xn,xT,_)\<close>\<close> =>
Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn
| _ => raise CTERM ("main QE only treats existential quantifiers!", [p]))
val cT = Thm.ctyp_of_cterm x
@@ -99,8 +99,8 @@
in
fun provein x S =
case Thm.term_of S of
- Const(\<^const_name>\<open>Orderings.bot\<close>, _) => raise CTERM ("provein : not a member!", [S])
- | Const(\<^const_name>\<open>insert\<close>, _) $ y $_ =>
+ \<^Const_>\<open>Orderings.bot _\<close> => raise CTERM ("provein : not a member!", [S])
+ | \<^Const_>\<open>insert _ for y _\<close> =>
let val (cy,S') = Thm.dest_binop S
in if Thm.term_of x aconv y then Thm.instantiate' [] [SOME x, SOME S'] insI1
else Thm.implies_elim (Thm.instantiate' [] [SOME x, SOME S', SOME cy] insI2)
@@ -123,12 +123,12 @@
fun decomp_mpinf fm =
case Thm.term_of fm of
- Const(\<^const_name>\<open>HOL.conj\<close>,_)$_$_ =>
+ \<^Const_>\<open>HOL.conj for _ _\<close> =>
let val (p,q) = Thm.dest_binop fm
in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj)
(Thm.lambda x p) (Thm.lambda x q))
end
- | Const(\<^const_name>\<open>HOL.disj\<close>,_)$_$_ =>
+ | \<^Const_>\<open>HOL.disj for _ _\<close> =>
let val (p,q) = Thm.dest_binop fm
in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj)
(Thm.lambda x p) (Thm.lambda x q))
@@ -176,19 +176,17 @@
let
fun h bounds tm =
(case Thm.term_of tm of
- Const (\<^const_name>\<open>HOL.eq\<close>, T) $ _ $ _ =>
- if domain_type T = HOLogic.boolT then find_args bounds tm
- else Thm.dest_fun2 tm
- | Const (\<^const_name>\<open>Not\<close>, _) $ _ => h bounds (Thm.dest_arg tm)
- | Const (\<^const_name>\<open>All\<close>, _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const (\<^const_name>\<open>Ex\<close>, _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _ => find_args bounds tm
- | Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _ => find_args bounds tm
- | Const (\<^const_name>\<open>HOL.implies\<close>, _) $ _ $ _ => find_args bounds tm
- | Const (\<^const_name>\<open>Pure.imp\<close>, _) $ _ $ _ => find_args bounds tm
- | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _ => find_args bounds tm
- | Const (\<^const_name>\<open>Pure.all\<close>, _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const (\<^const_name>\<open>Trueprop\<close>, _) $ _ => h bounds (Thm.dest_arg tm)
+ \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for _ _\<close> => find_args bounds tm
+ | \<^Const_>\<open>Not for _\<close> => h bounds (Thm.dest_arg tm)
+ | \<^Const_>\<open>All _ for _\<close> => find_body bounds (Thm.dest_arg tm)
+ | \<^Const_>\<open>Ex _ for _\<close> => find_body bounds (Thm.dest_arg tm)
+ | \<^Const_>\<open>conj for _ _\<close> => find_args bounds tm
+ | \<^Const_>\<open>disj for _ _\<close> => find_args bounds tm
+ | \<^Const_>\<open>implies for _ _\<close> => find_args bounds tm
+ | \<^Const_>\<open>Pure.imp for _ _\<close> => find_args bounds tm
+ | \<^Const_>\<open>Pure.eq _ for _ _\<close> => find_args bounds tm
+ | \<^Const_>\<open>Pure.all _ for _\<close> => find_body bounds (Thm.dest_arg tm)
+ | \<^Const_>\<open>Trueprop for _\<close> => h bounds (Thm.dest_arg tm)
| _ => Thm.dest_fun2 tm)
and find_args bounds tm =
(h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm)
--- a/src/HOL/Decision_Procs/langford.ML Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Wed Sep 29 22:54:38 2021 +0200
@@ -15,8 +15,8 @@
let
fun h acc ct =
(case Thm.term_of ct of
- Const (\<^const_name>\<open>Orderings.bot\<close>, _) => acc
- | Const (\<^const_name>\<open>insert\<close>, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct));
+ \<^Const_>\<open>bot _\<close> => acc
+ | \<^Const_>\<open>insert _ for _ _\<close> => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct));
in h [] end;
fun prove_finite cT u =
@@ -34,7 +34,7 @@
fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep =
(case Thm.term_of ep of
- Const (\<^const_name>\<open>Ex\<close>, _) $ _ =>
+ \<^Const_>\<open>Ex _ for _\<close> =>
let
val p = Thm.dest_arg ep
val ths =
@@ -53,10 +53,10 @@
val qe =
(case (Thm.term_of L, Thm.term_of U) of
- (Const (\<^const_name>\<open>Orderings.bot\<close>, _),_) =>
+ (\<^Const_>\<open>bot _\<close>, _) =>
let val (neU, fU) = proveneF U
in simp_rule ctxt (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end
- | (_, Const (\<^const_name>\<open>Orderings.bot\<close>, _)) =>
+ | (_, \<^Const_>\<open>bot _\<close>) =>
let val (neL,fL) = proveneF L
in simp_rule ctxt (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end
| _ =>
@@ -71,13 +71,13 @@
let
fun h acc ct =
(case Thm.term_of ct of
- \<^term>\<open>HOL.conj\<close> $ _ $ _ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
+ \<^Const>\<open>HOL.conj for _ _\<close> => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
| _ => ct :: acc)
in h [] end;
fun conjuncts ct =
(case Thm.term_of ct of
- \<^term>\<open>HOL.conj\<close> $ _ $ _ => Thm.dest_arg1 ct :: conjuncts (Thm.dest_arg ct)
+ \<^Const>\<open>HOL.conj for _ _\<close> => Thm.dest_arg1 ct :: conjuncts (Thm.dest_arg ct)
| _ => [ct]);
fun fold1 f = foldr1 (uncurry f); (* FIXME !? *)
@@ -89,12 +89,12 @@
let
fun h acc th =
(case Thm.prop_of th of
- \<^term>\<open>Trueprop\<close> $ (\<^term>\<open>HOL.conj\<close> $ p $ q) =>
+ \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.conj for p q\<close>\<close> =>
h (h acc (th RS conjunct2)) (th RS conjunct1)
- | \<^term>\<open>Trueprop\<close> $ p => (p, th) :: acc)
+ | \<^Const_>\<open>Trueprop for p\<close> => (p, th) :: acc)
in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
-fun is_conj (\<^term>\<open>HOL.conj\<close>$_$_) = true
+fun is_conj \<^Const_>\<open>HOL.conj for _ _\<close> = true
| is_conj _ = false;
fun prove_conj tab cjs =
@@ -122,7 +122,7 @@
fun is_eqx x eq =
(case Thm.term_of eq of
- Const (\<^const_name>\<open>HOL.eq\<close>, _) $ l $ r =>
+ \<^Const_>\<open>HOL.eq _ for l r\<close> =>
l aconv Thm.term_of x orelse r aconv Thm.term_of x
| _ => false);
@@ -130,7 +130,7 @@
fun proc ctxt ct =
(case Thm.term_of ct of
- Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (xn, _, _) =>
+ \<^Const_>\<open>Ex _ for \<open>Abs (xn, _, _)\<close>\<close> =>
let
val e = Thm.dest_fun ct
val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
@@ -197,19 +197,17 @@
let
fun h bounds tm =
(case Thm.term_of tm of
- Const (\<^const_name>\<open>HOL.eq\<close>, T) $ _ $ _ =>
- if domain_type T = HOLogic.boolT then find_args bounds tm
- else Thm.dest_fun2 tm
- | Const (\<^const_name>\<open>Not\<close>, _) $ _ => h bounds (Thm.dest_arg tm)
- | Const (\<^const_name>\<open>All\<close>, _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const (\<^const_name>\<open>Pure.all\<close>, _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const (\<^const_name>\<open>Ex\<close>, _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _ => find_args bounds tm
- | Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _ => find_args bounds tm
- | Const (\<^const_name>\<open>HOL.implies\<close>, _) $ _ $ _ => find_args bounds tm
- | Const (\<^const_name>\<open>Pure.imp\<close>, _) $ _ $ _ => find_args bounds tm
- | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _ => find_args bounds tm
- | Const (\<^const_name>\<open>Trueprop\<close>, _) $ _ => h bounds (Thm.dest_arg tm)
+ \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for _ _\<close> => find_args bounds tm
+ | \<^Const_>\<open>Not for _\<close> => h bounds (Thm.dest_arg tm)
+ | \<^Const_>\<open>All _ for _\<close> => find_body bounds (Thm.dest_arg tm)
+ | \<^Const_>\<open>Pure.all _ for _\<close> => find_body bounds (Thm.dest_arg tm)
+ | \<^Const_>\<open>Ex _ for _\<close> => find_body bounds (Thm.dest_arg tm)
+ | \<^Const_>\<open>HOL.conj for _ _\<close> => find_args bounds tm
+ | \<^Const_>\<open>HOL.disj for _ _\<close> => find_args bounds tm
+ | \<^Const_>\<open>HOL.implies for _ _\<close> => find_args bounds tm
+ | \<^Const_>\<open>Pure.imp for _ _\<close> => find_args bounds tm
+ | \<^Const_>\<open>Pure.eq _ for _ _\<close> => find_args bounds tm
+ | \<^Const_>\<open>Trueprop for _\<close> => h bounds (Thm.dest_arg tm)
| _ => Thm.dest_fun2 tm)
and find_args bounds tm =
(h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
--- a/src/HOL/Decision_Procs/mir_tac.ML Wed Sep 29 18:22:32 2021 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Wed Sep 29 22:54:38 2021 +0200
@@ -105,7 +105,7 @@
(* The result of the quantifier elimination *)
val (th, tac) =
case Thm.prop_of pre_thm of
- Const (\<^const_name>\<open>Pure.imp\<close>, _) $ (Const (\<^const_name>\<open>Trueprop\<close>, _) $ t1) $ _ =>
+ \<^Const_>\<open>Pure.imp for \<^Const_>\<open>Trueprop for t1\<close> _\<close> =>
let
val pth = mirfr_oracle (ctxt, Envir.eta_long [] t1)
in