--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Sep 28 22:08:51 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Sep 28 22:10:21 2021 +0200
@@ -36,15 +36,12 @@
val may_use_binary_ints =
let
- fun aux def (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2) =
- aux def t1 andalso aux false t2
- | aux def (\<^const>\<open>Pure.imp\<close> $ t1 $ t2) = aux false t1 andalso aux def t2
- | aux def (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) =
- aux def t1 andalso aux false t2
- | aux def (\<^const>\<open>HOL.implies\<close> $ t1 $ t2) = aux false t1 andalso aux def t2
+ fun aux def \<^Const_>\<open>Pure.eq _ for t1 t2\<close> = aux def t1 andalso aux false t2
+ | aux def \<^Const_>\<open>Pure.imp for t1 t2\<close> = aux false t1 andalso aux def t2
+ | aux def \<^Const_>\<open>HOL.eq _ for t1 t2\<close> = aux def t1 andalso aux false t2
+ | aux def \<^Const_>\<open>implies for t1 t2\<close> = aux false t1 andalso aux def t2
| aux def (t1 $ t2) = aux def t1 andalso aux def t2
- | aux def (t as Const (s, _)) =
- (not def orelse t <> \<^const>\<open>Suc\<close>) andalso
+ | aux def (t as Const (s, _)) = (not def orelse t <> \<^Const>\<open>Suc\<close>) andalso
not (member (op =)
[\<^const_name>\<open>Abs_Frac\<close>, \<^const_name>\<open>Rep_Frac\<close>,
\<^const_name>\<open>nat_gcd\<close>, \<^const_name>\<open>nat_lcm\<close>,
@@ -143,7 +140,7 @@
| _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
case t of
- \<^const>\<open>Trueprop\<close> $ t1 => box_var_in_def new_Ts old_Ts t1 z
+ \<^Const_>\<open>Trueprop for t1\<close> => box_var_in_def new_Ts old_Ts t1 z
| Const (s0, _) $ t1 $ _ =>
if s0 = \<^const_name>\<open>Pure.eq\<close> orelse s0 = \<^const_name>\<open>HOL.eq\<close> then
let
@@ -190,31 +187,29 @@
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
| Const (s0 as \<^const_name>\<open>Pure.eq\<close>, T0) $ t1 $ t2 =>
do_equals new_Ts old_Ts s0 T0 t1 t2
- | \<^const>\<open>Pure.imp\<close> $ t1 $ t2 =>
- \<^const>\<open>Pure.imp\<close> $ do_term new_Ts old_Ts (flip_polarity polar) t1
- $ do_term new_Ts old_Ts polar t2
- | \<^const>\<open>Pure.conjunction\<close> $ t1 $ t2 =>
- \<^const>\<open>Pure.conjunction\<close> $ do_term new_Ts old_Ts polar t1
- $ do_term new_Ts old_Ts polar t2
- | \<^const>\<open>Trueprop\<close> $ t1 =>
- \<^const>\<open>Trueprop\<close> $ do_term new_Ts old_Ts polar t1
- | \<^const>\<open>Not\<close> $ t1 =>
- \<^const>\<open>Not\<close> $ do_term new_Ts old_Ts (flip_polarity polar) t1
+ | \<^Const_>\<open>Pure.imp for t1 t2\<close> =>
+ \<^Const>\<open>Pure.imp for \<open>do_term new_Ts old_Ts (flip_polarity polar) t1\<close>
+ \<open>do_term new_Ts old_Ts polar t2\<close>\<close>
+ | \<^Const_>\<open>Pure.conjunction for t1 t2\<close> =>
+ \<^Const>\<open>Pure.conjunction for \<open>do_term new_Ts old_Ts polar t1\<close>
+ \<open>do_term new_Ts old_Ts polar t2\<close>\<close>
+ | \<^Const_>\<open>Trueprop for t1\<close> => \<^Const>\<open>Trueprop for \<open>do_term new_Ts old_Ts polar t1\<close>\<close>
+ | \<^Const_>\<open>Not for t1\<close> => \<^Const>\<open>Not for \<open>do_term new_Ts old_Ts (flip_polarity polar) t1\<close>\<close>
| Const (s0 as \<^const_name>\<open>All\<close>, T0) $ Abs (s1, T1, t1) =>
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
| Const (s0 as \<^const_name>\<open>Ex\<close>, T0) $ Abs (s1, T1, t1) =>
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
| Const (s0 as \<^const_name>\<open>HOL.eq\<close>, T0) $ t1 $ t2 =>
do_equals new_Ts old_Ts s0 T0 t1 t2
- | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 =>
- \<^const>\<open>HOL.conj\<close> $ do_term new_Ts old_Ts polar t1
- $ do_term new_Ts old_Ts polar t2
- | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 =>
- \<^const>\<open>HOL.disj\<close> $ do_term new_Ts old_Ts polar t1
- $ do_term new_Ts old_Ts polar t2
- | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 =>
- \<^const>\<open>HOL.implies\<close> $ do_term new_Ts old_Ts (flip_polarity polar) t1
- $ do_term new_Ts old_Ts polar t2
+ | \<^Const_>\<open>conj for t1 t2\<close> =>
+ \<^Const>\<open>conj for \<open>do_term new_Ts old_Ts polar t1\<close>
+ \<open>do_term new_Ts old_Ts polar t2\<close>\<close>
+ | \<^Const_>\<open>disj for t1 t2\<close> =>
+ \<^Const>\<open>disj for \<open>do_term new_Ts old_Ts polar t1\<close>
+ \<open>do_term new_Ts old_Ts polar t2\<close>\<close>
+ | \<^Const_>\<open>implies for t1 t2\<close> =>
+ \<^Const>\<open>implies for \<open>do_term new_Ts old_Ts (flip_polarity polar) t1\<close>
+ \<open>do_term new_Ts old_Ts polar t2\<close>\<close>
| Const (x as (s, T)) =>
if is_descr s then
do_descr s T
@@ -335,11 +330,11 @@
case t of
(t0 as Const (\<^const_name>\<open>Pure.eq\<close>, _)) $ t1 $ t2 =>
do_eq_or_imp Ts true def t0 t1 t2 seen
- | (t0 as \<^const>\<open>Pure.imp\<close>) $ t1 $ t2 =>
+ | (t0 as \<^Const_>\<open>Pure.imp\<close>) $ t1 $ t2 =>
if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
| (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ t1 $ t2 =>
do_eq_or_imp Ts true def t0 t1 t2 seen
- | (t0 as \<^const>\<open>HOL.implies\<close>) $ t1 $ t2 =>
+ | (t0 as \<^Const_>\<open>implies\<close>) $ t1 $ t2 =>
do_eq_or_imp Ts false def t0 t1 t2 seen
| Abs (s, T, t') =>
let val (t', seen) = do_term (T :: Ts) def t' [] seen in
@@ -402,11 +397,11 @@
| _ => I) t (K 0)
fun aux Ts careful ((t0 as Const (\<^const_name>\<open>Pure.eq\<close>, _)) $ t1 $ t2) =
aux_eq Ts careful true t0 t1 t2
- | aux Ts careful ((t0 as \<^const>\<open>Pure.imp\<close>) $ t1 $ t2) =
+ | aux Ts careful ((t0 as \<^Const_>\<open>Pure.imp\<close>) $ t1 $ t2) =
t0 $ aux Ts false t1 $ aux Ts careful t2
| aux Ts careful ((t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ t1 $ t2) =
aux_eq Ts careful true t0 t1 t2
- | aux Ts careful ((t0 as \<^const>\<open>HOL.implies\<close>) $ t1 $ t2) =
+ | aux Ts careful ((t0 as \<^Const_>\<open>implies\<close>) $ t1 $ t2) =
t0 $ aux Ts false t1 $ aux Ts careful t2
| aux Ts careful (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) careful t')
| aux Ts careful (t1 $ t2) = aux Ts careful t1 $ aux Ts careful t2
@@ -417,13 +412,13 @@
raise SAME ()
else if axiom andalso is_Var t2 andalso
num_occs_of_var (dest_Var t2) = 1 then
- \<^const>\<open>True\<close>
+ \<^Const>\<open>True\<close>
else case strip_comb t2 of
(* The first case is not as general as it could be. *)
(Const (\<^const_name>\<open>PairBox\<close>, _),
[Const (\<^const_name>\<open>fst\<close>, _) $ Var z1,
Const (\<^const_name>\<open>snd\<close>, _) $ Var z2]) =>
- if z1 = z2 andalso num_occs_of_var z1 = 2 then \<^const>\<open>True\<close>
+ if z1 = z2 andalso num_occs_of_var z1 = 2 then \<^Const>\<open>True\<close>
else raise SAME ()
| (Const (x as (s, T)), args) =>
let
@@ -454,26 +449,22 @@
(** Destruction of universal and existential equalities **)
-fun curry_assms (\<^const>\<open>Pure.imp\<close> $ (\<^const>\<open>Trueprop\<close>
- $ (\<^const>\<open>HOL.conj\<close> $ t1 $ t2)) $ t3) =
+fun curry_assms \<^Const_>\<open>Pure.imp for \<^Const>\<open>Trueprop for \<^Const_>\<open>conj for t1 t2\<close>\<close> t3\<close> =
curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
- | curry_assms (\<^const>\<open>Pure.imp\<close> $ t1 $ t2) =
- \<^const>\<open>Pure.imp\<close> $ curry_assms t1 $ curry_assms t2
+ | curry_assms \<^Const_>\<open>Pure.imp for t1 t2\<close> = \<^Const>\<open>Pure.imp for \<open>curry_assms t1\<close> \<open>curry_assms t2\<close>\<close>
| curry_assms t = t
val destroy_universal_equalities =
let
fun aux prems zs t =
case t of
- \<^const>\<open>Pure.imp\<close> $ t1 $ t2 => aux_implies prems zs t1 t2
+ \<^Const_>\<open>Pure.imp for t1 t2\<close> => aux_implies prems zs t1 t2
| _ => Logic.list_implies (rev prems, t)
and aux_implies prems zs t1 t2 =
case t1 of
- Const (\<^const_name>\<open>Pure.eq\<close>, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
- | \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Var z $ t') =>
- aux_eq prems zs z t' t1 t2
- | \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t' $ Var z) =>
- aux_eq prems zs z t' t1 t2
+ \<^Const_>\<open>Pure.eq _ for \<open>Var z\<close> t'\<close> => aux_eq prems zs z t' t1 t2
+ | \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for \<open>Var z\<close> t'\<close>\<close> => aux_eq prems zs z t' t1 t2
+ | \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for t' \<open>Var z\<close>\<close>\<close> => aux_eq prems zs z t' t1 t2
| _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
and aux_eq prems zs z t' t1 t2 =
if not (member (op =) zs z) andalso
@@ -528,7 +519,7 @@
fun kill [] [] ts = foldr1 s_conj ts
| kill (s :: ss) (T :: Ts) ts =
(case find_bound_assign ctxt (length ss) [] ts of
- SOME (_, []) => \<^const>\<open>True\<close>
+ SOME (_, []) => \<^Const>\<open>True\<close>
| SOME (arg_t, ts) =>
kill ss Ts (map (subst_one_bound (length ss)
(incr_bv (~1, length ss + 1, arg_t))) ts)
@@ -592,27 +583,27 @@
case t of
Const (s0 as \<^const_name>\<open>Pure.all\<close>, T0) $ Abs (s1, T1, t1) =>
do_quantifier s0 T0 s1 T1 t1
- | \<^const>\<open>Pure.imp\<close> $ t1 $ t2 =>
- \<^const>\<open>Pure.imp\<close> $ aux ss Ts js skolemizable (flip_polarity polar) t1
- $ aux ss Ts js skolemizable polar t2
- | \<^const>\<open>Pure.conjunction\<close> $ t1 $ t2 =>
- \<^const>\<open>Pure.conjunction\<close> $ aux ss Ts js skolemizable polar t1
- $ aux ss Ts js skolemizable polar t2
- | \<^const>\<open>Trueprop\<close> $ t1 =>
- \<^const>\<open>Trueprop\<close> $ aux ss Ts js skolemizable polar t1
- | \<^const>\<open>Not\<close> $ t1 =>
- \<^const>\<open>Not\<close> $ aux ss Ts js skolemizable (flip_polarity polar) t1
+ | \<^Const_>\<open>Pure.imp for t1 t2\<close> =>
+ \<^Const>\<open>Pure.imp for \<open>aux ss Ts js skolemizable (flip_polarity polar) t1\<close>
+ \<open>aux ss Ts js skolemizable polar t2\<close>\<close>
+ | \<^Const_>\<open>Pure.conjunction for t1 t2\<close> =>
+ \<^Const>\<open>Pure.conjunction for \<open>aux ss Ts js skolemizable polar t1\<close>
+ \<open>aux ss Ts js skolemizable polar t2\<close>\<close>
+ | \<^Const_>\<open>Trueprop for t1\<close> =>
+ \<^Const>\<open>Trueprop for \<open>aux ss Ts js skolemizable polar t1\<close>\<close>
+ | \<^Const_>\<open>Not for t1\<close> =>
+ \<^Const>\<open>Not for \<open>aux ss Ts js skolemizable (flip_polarity polar) t1\<close>\<close>
| Const (s0 as \<^const_name>\<open>All\<close>, T0) $ Abs (s1, T1, t1) =>
do_quantifier s0 T0 s1 T1 t1
| Const (s0 as \<^const_name>\<open>Ex\<close>, T0) $ Abs (s1, T1, t1) =>
do_quantifier s0 T0 s1 T1 t1
- | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 =>
+ | \<^Const_>\<open>conj for t1 t2\<close> =>
s_conj (apply2 (aux ss Ts js skolemizable polar) (t1, t2))
- | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 =>
+ | \<^Const_>\<open>disj for t1 t2\<close> =>
s_disj (apply2 (aux ss Ts js skolemizable polar) (t1, t2))
- | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 =>
- \<^const>\<open>HOL.implies\<close> $ aux ss Ts js skolemizable (flip_polarity polar) t1
- $ aux ss Ts js skolemizable polar t2
+ | \<^Const_>\<open>implies for t1 t2\<close> =>
+ \<^Const>\<open>implies for \<open>aux ss Ts js skolemizable (flip_polarity polar) t1\<close>
+ \<open>aux ss Ts js skolemizable polar t2\<close>\<close>
| (t0 as Const (\<^const_name>\<open>Let\<close>, _)) $ t1 $ t2 =>
t0 $ t1 $ aux ss Ts js skolemizable polar t2
| Const (x as (s, T)) =>
@@ -622,8 +613,8 @@
let
val gfp = (fixpoint_kind_of_const thy def_tables x = Gfp)
val (pref, connective) =
- if gfp then (lbfp_prefix, \<^const>\<open>HOL.disj\<close>)
- else (ubfp_prefix, \<^const>\<open>HOL.conj\<close>)
+ if gfp then (lbfp_prefix, \<^Const>\<open>disj\<close>)
+ else (ubfp_prefix, \<^Const>\<open>conj\<close>)
fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
|> aux ss Ts js skolemizable polar
fun neg () = Const (pref ^ s, T)
@@ -653,10 +644,9 @@
(** Function specialization **)
-fun params_in_equation (\<^const>\<open>Pure.imp\<close> $ _ $ t2) = params_in_equation t2
- | params_in_equation (\<^const>\<open>Trueprop\<close> $ t1) = params_in_equation t1
- | params_in_equation (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _) =
- snd (strip_comb t1)
+fun params_in_equation \<^Const_>\<open>Pure.imp for _ t2\<close> = params_in_equation t2
+ | params_in_equation \<^Const_>\<open>Trueprop for t1\<close> = params_in_equation t1
+ | params_in_equation \<^Const_>\<open>HOL.eq _ for t1 _\<close> = snd (strip_comb t1)
| params_in_equation _ = []
fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
@@ -865,10 +855,8 @@
if exists_subterm (curry (op aconv) u) def then NONE else SOME u
in
case t of
- Const (\<^const_name>\<open>Pure.eq\<close>, _) $ (u as Free _) $ def => do_equals u def
- | \<^const>\<open>Trueprop\<close>
- $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (u as Free _) $ def) =>
- do_equals u def
+ \<^Const_>\<open>Pure.eq _ for \<open>u as Free _\<close> def\<close> => do_equals u def
+ | \<^Const_>\<open>Trueprop\<close> $ \<^Const_>\<open>HOL.eq _ for \<open>u as Free _\<close> def\<close> => do_equals u def
| _ => NONE
end
@@ -917,7 +905,7 @@
and add_def_axiom depth = add_axiom fst apfst true depth
and add_nondef_axiom depth = add_axiom snd apsnd false depth
and add_maybe_def_axiom depth t =
- (if head_of t <> \<^const>\<open>Pure.imp\<close> then add_def_axiom
+ (if head_of t <> \<^Const>\<open>Pure.imp\<close> then add_def_axiom
else add_nondef_axiom) depth t
and add_eq_axiom depth t =
(if is_constr_pattern_formula ctxt t then add_def_axiom
@@ -1104,10 +1092,10 @@
case t of
(t0 as Const (\<^const_name>\<open>All\<close>, T0)) $ Abs (s, T1, t1) =>
(case t1 of
- (t10 as \<^const>\<open>HOL.conj\<close>) $ t11 $ t12 =>
+ (t10 as \<^Const_>\<open>conj\<close>) $ t11 $ t12 =>
t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
$ distribute_quantifiers (t0 $ Abs (s, T1, t12))
- | (t10 as \<^const>\<open>Not\<close>) $ t11 =>
+ | (t10 as \<^Const_>\<open>Not\<close>) $ t11 =>
t10 $ distribute_quantifiers (Const (\<^const_name>\<open>Ex\<close>, T0)
$ Abs (s, T1, t11))
| t1 =>
@@ -1117,14 +1105,14 @@
t0 $ Abs (s, T1, distribute_quantifiers t1))
| (t0 as Const (\<^const_name>\<open>Ex\<close>, T0)) $ Abs (s, T1, t1) =>
(case distribute_quantifiers t1 of
- (t10 as \<^const>\<open>HOL.disj\<close>) $ t11 $ t12 =>
+ (t10 as \<^Const_>\<open>disj\<close>) $ t11 $ t12 =>
t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
$ distribute_quantifiers (t0 $ Abs (s, T1, t12))
- | (t10 as \<^const>\<open>HOL.implies\<close>) $ t11 $ t12 =>
+ | (t10 as \<^Const_>\<open>implies\<close>) $ t11 $ t12 =>
t10 $ distribute_quantifiers (Const (\<^const_name>\<open>All\<close>, T0)
$ Abs (s, T1, t11))
$ distribute_quantifiers (t0 $ Abs (s, T1, t12))
- | (t10 as \<^const>\<open>Not\<close>) $ t11 =>
+ | (t10 as \<^Const_>\<open>Not\<close>) $ t11 =>
t10 $ distribute_quantifiers (Const (\<^const_name>\<open>All\<close>, T0)
$ Abs (s, T1, t11))
| t1 =>