--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 28 22:08:51 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 28 22:10:21 2021 +0200
@@ -182,8 +182,7 @@
fun none_true assigns = forall (not_equal (SOME true) o snd) assigns
-fun has_lonely_bool_var (\<^const>\<open>Pure.conjunction\<close>
- $ (\<^const>\<open>Trueprop\<close> $ Free _) $ _) = true
+fun has_lonely_bool_var \<^Const_>\<open>Pure.conjunction for \<^Const_>\<open>Trueprop for \<open>Free _\<close>\<close> _\<close> = true
| has_lonely_bool_var _ = false
val syntactic_sorts =
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Sep 28 22:08:51 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Sep 28 22:10:21 2021 +0200
@@ -331,16 +331,16 @@
else
s
-fun s_conj (t1, \<^const>\<open>True\<close>) = t1
- | s_conj (\<^const>\<open>True\<close>, t2) = t2
+fun s_conj (t1, \<^Const_>\<open>True\<close>) = t1
+ | s_conj (\<^Const_>\<open>True\<close>, t2) = t2
| s_conj (t1, t2) =
- if t1 = \<^const>\<open>False\<close> orelse t2 = \<^const>\<open>False\<close> then \<^const>\<open>False\<close>
+ if t1 = \<^Const>\<open>False\<close> orelse t2 = \<^Const>\<open>False\<close> then \<^Const>\<open>False\<close>
else HOLogic.mk_conj (t1, t2)
-fun s_disj (t1, \<^const>\<open>False\<close>) = t1
- | s_disj (\<^const>\<open>False\<close>, t2) = t2
+fun s_disj (t1, \<^Const_>\<open>False\<close>) = t1
+ | s_disj (\<^Const_>\<open>False\<close>, t2) = t2
| s_disj (t1, t2) =
- if t1 = \<^const>\<open>True\<close> orelse t2 = \<^const>\<open>True\<close> then \<^const>\<open>True\<close>
+ if t1 = \<^Const>\<open>True\<close> orelse t2 = \<^Const>\<open>True\<close> then \<^Const>\<open>True\<close>
else HOLogic.mk_disj (t1, t2)
fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
@@ -348,13 +348,13 @@
| strip_connective _ t = [t]
fun strip_any_connective (t as (t0 $ _ $ _)) =
- if t0 = \<^const>\<open>HOL.conj\<close> orelse t0 = \<^const>\<open>HOL.disj\<close> then
+ if t0 = \<^Const>\<open>conj\<close> orelse t0 = \<^Const>\<open>disj\<close> then
(strip_connective t0 t, t0)
else
- ([t], \<^const>\<open>Not\<close>)
- | strip_any_connective t = ([t], \<^const>\<open>Not\<close>)
-val conjuncts_of = strip_connective \<^const>\<open>HOL.conj\<close>
-val disjuncts_of = strip_connective \<^const>\<open>HOL.disj\<close>
+ ([t], \<^Const>\<open>Not\<close>)
+ | strip_any_connective t = ([t], \<^Const>\<open>Not\<close>)
+val conjuncts_of = strip_connective \<^Const>\<open>conj\<close>
+val disjuncts_of = strip_connective \<^Const>\<open>disj\<close>
(* When you add constants to these lists, make sure to handle them in
"Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
@@ -797,8 +797,8 @@
the (Quotient_Info.lookup_quotients thy s)
val partial =
case Thm.prop_of equiv_thm of
- \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>equivp\<close>, _) $ _) => false
- | \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>part_equivp\<close>, _) $ _) => true
+ \<^Const_>\<open>Trueprop for \<^Const_>\<open>equivp _ for _\<close>\<close> => false
+ | \<^Const_>\<open>Trueprop for \<^Const_>\<open>part_equivp _ for _\<close>\<close> => true
| _ => raise NOT_SUPPORTED "Ill-formed quotient type equivalence \
\relation theorem"
val Ts' = qtyp |> dest_Type |> snd
@@ -948,7 +948,7 @@
fold (fn (z as ((s, _), T)) => fn t' =>
Logic.all_const T $ Abs (s, T, abstract_over (Var z, t')))
(take (length zs' - length zs) zs')
- fun aux zs (\<^const>\<open>Pure.imp\<close> $ t1 $ t2) =
+ fun aux zs \<^Const>\<open>Pure.imp for t1 t2\<close> =
let val zs' = Term.add_vars t1 zs in
close_up zs zs' (Logic.mk_implies (t1, aux zs' t2))
end
@@ -957,8 +957,8 @@
fun distinctness_formula T =
all_distinct_unordered_pairs_of
- #> map (fn (t1, t2) => \<^const>\<open>Not\<close> $ (HOLogic.eq_const T $ t1 $ t2))
- #> List.foldr (s_conj o swap) \<^const>\<open>True\<close>
+ #> map (fn (t1, t2) => \<^Const>\<open>Not\<close> $ (HOLogic.eq_const T $ t1 $ t2))
+ #> List.foldr (s_conj o swap) \<^Const>\<open>True\<close>
fun zero_const T = Const (\<^const_name>\<open>zero_class.zero\<close>, T)
fun suc_const T = Const (\<^const_name>\<open>Suc\<close>, T --> T)
@@ -986,7 +986,7 @@
SOME {abs_type, rep_type, Abs_name, ...} =>
[(Abs_name, varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
| NONE =>
- if T = \<^typ>\<open>ind\<close> then [dest_Const \<^const>\<open>Zero_Rep\<close>, dest_Const \<^const>\<open>Suc_Rep\<close>]
+ if T = \<^typ>\<open>ind\<close> then [dest_Const \<^Const>\<open>Zero_Rep\<close>, dest_Const \<^Const>\<open>Suc_Rep\<close>]
else [])
| uncached_data_type_constrs _ _ = []
@@ -1145,8 +1145,8 @@
if t1' aconv t2 then \<^prop>\<open>True\<close> else t1 $ t2
| s_betapply _ (t1 as Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1', t2) =
if t1' aconv t2 then \<^term>\<open>True\<close> else t1 $ t2
- | s_betapply _ (Const (\<^const_name>\<open>If\<close>, _) $ \<^const>\<open>True\<close> $ t1', _) = t1'
- | s_betapply _ (Const (\<^const_name>\<open>If\<close>, _) $ \<^const>\<open>False\<close> $ _, t2) = t2
+ | s_betapply _ (Const (\<^const_name>\<open>If\<close>, _) $ \<^Const_>\<open>True\<close> $ t1', _) = t1'
+ | s_betapply _ (Const (\<^const_name>\<open>If\<close>, _) $ \<^Const_>\<open>False\<close> $ _, t2) = t2
| s_betapply Ts (Const (\<^const_name>\<open>Let\<close>,
Type (_, [bound_T, Type (_, [_, body_T])]))
$ t12 $ Abs (s, T, t13'), t2) =
@@ -1181,18 +1181,18 @@
fun discr_term_for_constr hol_ctxt (x as (s, T)) =
let val dataT = body_type T in
if s = \<^const_name>\<open>Suc\<close> then
- Abs (Name.uu, dataT, \<^const>\<open>Not\<close> $ HOLogic.mk_eq (zero_const dataT, Bound 0))
+ Abs (Name.uu, dataT, \<^Const>\<open>Not\<close> $ HOLogic.mk_eq (zero_const dataT, Bound 0))
else if length (data_type_constrs hol_ctxt dataT) >= 2 then
Const (discr_for_constr x)
else
- Abs (Name.uu, dataT, \<^const>\<open>True\<close>)
+ Abs (Name.uu, dataT, \<^Const>\<open>True\<close>)
end
fun discriminate_value (hol_ctxt as {ctxt, ...}) x t =
case head_of t of
Const x' =>
- if x = x' then \<^const>\<open>True\<close>
- else if is_nonfree_constr ctxt x' then \<^const>\<open>False\<close>
+ if x = x' then \<^Const>\<open>True\<close>
+ else if is_nonfree_constr ctxt x' then \<^Const>\<open>False\<close>
else s_betapply [] (discr_term_for_constr hol_ctxt x, t)
| _ => s_betapply [] (discr_term_for_constr hol_ctxt x, t)
@@ -1379,10 +1379,10 @@
simplification rules (equational specifications). *)
fun term_under_def t =
case t of
- \<^const>\<open>Pure.imp\<close> $ _ $ t2 => term_under_def t2
- | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ _ => term_under_def t1
- | \<^const>\<open>Trueprop\<close> $ t1 => term_under_def t1
- | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _ => term_under_def t1
+ \<^Const_>\<open>Pure.imp for _ t2\<close> => term_under_def t2
+ | \<^Const_>\<open>Pure.eq _ for t1 _\<close> => term_under_def t1
+ | \<^Const_>\<open>Trueprop for t1\<close> => term_under_def t1
+ | \<^Const_>\<open>HOL.eq _ for t1 _\<close> => term_under_def t1
| Abs (_, _, t') => term_under_def t'
| t1 $ _ => term_under_def t1
| _ => t
@@ -1405,9 +1405,8 @@
| aux _ _ = NONE
val (lhs, rhs) =
case t of
- Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2 => (t1, t2)
- | \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) =>
- (t1, t2)
+ \<^Const_>\<open>Pure.eq _ for t1 t2\<close> => (t1, t2)
+ | \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for t1 t2\<close>\<close> => (t1, t2)
| _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
val args = strip_comb lhs |> snd
in fold_rev aux args (SOME rhs) end
@@ -1482,13 +1481,13 @@
fun lhs_of_equation t =
case t of
- Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, _, t1) => lhs_of_equation t1
- | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ _ => SOME t1
- | \<^const>\<open>Pure.imp\<close> $ _ $ t2 => lhs_of_equation t2
- | \<^const>\<open>Trueprop\<close> $ t1 => lhs_of_equation t1
- | Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t1) => lhs_of_equation t1
- | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _ => SOME t1
- | \<^const>\<open>HOL.implies\<close> $ _ $ t2 => lhs_of_equation t2
+ \<^Const_>\<open>Pure.all _ for \<open>Abs (_, _, t1)\<close>\<close> => lhs_of_equation t1
+ | \<^Const_>\<open>Pure.eq _ for t1 _\<close> => SOME t1
+ | \<^Const_>\<open>Pure.imp for _ t2\<close> => lhs_of_equation t2
+ | \<^Const_>\<open>Trueprop for t1\<close> => lhs_of_equation t1
+ | \<^Const_>\<open>All _ for \<open>Abs (_, _, t1)\<close>\<close> => lhs_of_equation t1
+ | \<^Const_>\<open>HOL.eq _ for t1 _\<close> => SOME t1
+ | \<^Const_>\<open>implies for _ t2\<close> => lhs_of_equation t2
| _ => NONE
fun is_constr_pattern _ (Bound _) = true
@@ -1598,19 +1597,19 @@
(incr_boundvars 1 func_t, x),
discriminate_value hol_ctxt x (Bound 0)))
|> AList.group (op aconv)
- |> map (apsnd (List.foldl s_disj \<^const>\<open>False\<close>))
+ |> map (apsnd (List.foldl s_disj \<^Const>\<open>False\<close>))
|> sort (int_ord o apply2 (size_of_term o snd))
|> rev
in
if res_T = bool_T then
- if forall (member (op =) [\<^const>\<open>False\<close>, \<^const>\<open>True\<close>] o fst) cases then
+ if forall (member (op =) [\<^Const>\<open>False\<close>, \<^Const>\<open>True\<close>] o fst) cases then
case cases of
[(body_t, _)] => body_t
- | [_, (\<^const>\<open>True\<close>, head_t2)] => head_t2
- | [_, (\<^const>\<open>False\<close>, head_t2)] => \<^const>\<open>Not\<close> $ head_t2
+ | [_, (\<^Const>\<open>True\<close>, head_t2)] => head_t2
+ | [_, (\<^Const>\<open>False\<close>, head_t2)] => \<^Const>\<open>Not for head_t2\<close>
| _ => raise BAD ("Nitpick_HOL.optimized_case_def", "impossible cases")
else
- \<^const>\<open>True\<close> |> fold_rev (add_constr_case res_T) cases
+ \<^Const>\<open>True\<close> |> fold_rev (add_constr_case res_T) cases
else
fst (hd cases) |> fold_rev (add_constr_case res_T) (tl cases)
end
@@ -1895,13 +1894,12 @@
in
Logic.list_implies (prems,
case concl of
- \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _]))
- $ t1 $ t2) =>
- \<^const>\<open>Trueprop\<close> $ extensional_equal j T t1 t2
- | \<^const>\<open>Trueprop\<close> $ t' =>
- \<^const>\<open>Trueprop\<close> $ HOLogic.mk_eq (t', \<^const>\<open>True\<close>)
- | Const (\<^const_name>\<open>Pure.eq\<close>, Type (_, [T, _])) $ t1 $ t2 =>
- \<^const>\<open>Trueprop\<close> $ extensional_equal j T t1 t2
+ \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq T for t1 t2\<close>\<close> =>
+ \<^Const>\<open>Trueprop for \<open>extensional_equal j T t1 t2\<close>\<close>
+ | \<^Const_>\<open>Trueprop for t'\<close> =>
+ \<^Const>\<open>Trueprop for \<open>HOLogic.mk_eq (t', \<^Const>\<open>True\<close>)\<close>\<close>
+ | \<^Const_>\<open>Pure.eq T for t1 t2\<close> =>
+ \<^Const>\<open>Trueprop for \<open>extensional_equal j T t1 t2\<close>\<close>
| _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation " ^
quote (Syntax.string_of_term ctxt t));
raise SAME ()))
@@ -1951,7 +1949,7 @@
end
fun ground_theorem_table thy =
- fold ((fn \<^const>\<open>Trueprop\<close> $ t1 =>
+ fold ((fn \<^Const_>\<open>Trueprop for t1\<close> =>
is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
| _ => I) o Thm.prop_of o snd) (Global_Theory.all_thms_of thy true) Inttab.empty
@@ -2016,13 +2014,13 @@
in
[Logic.mk_equals (normal_fun $ sel_a_t, sel_a_t),
Logic.list_implies
- ([\<^const>\<open>Not\<close> $ (is_unknown_t $ normal_x),
- \<^const>\<open>Not\<close> $ (is_unknown_t $ normal_y),
+ ([\<^Const>\<open>Not\<close> $ (is_unknown_t $ normal_x),
+ \<^Const>\<open>Not\<close> $ (is_unknown_t $ normal_y),
equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop,
Logic.mk_equals (normal_x, normal_y)),
Logic.list_implies
- ([HOLogic.mk_Trueprop (\<^const>\<open>Not\<close> $ (is_unknown_t $ normal_x)),
- HOLogic.mk_Trueprop (\<^const>\<open>Not\<close> $ HOLogic.mk_eq (normal_x, x_var))],
+ ([HOLogic.mk_Trueprop (\<^Const>\<open>Not\<close> $ (is_unknown_t $ normal_x)),
+ HOLogic.mk_Trueprop (\<^Const>\<open>Not\<close> $ HOLogic.mk_eq (normal_x, x_var))],
HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
|> partial ? cons (HOLogic.mk_Trueprop (equiv_rel $ sel_a_t $ sel_a_t))
end
@@ -2031,8 +2029,8 @@
let
val xs = data_type_constrs hol_ctxt T
val pred_T = T --> bool_T
- val iter_T = \<^typ>\<open>bisim_iterator\<close>
- val bisim_max = \<^const>\<open>bisim_iterator_max\<close>
+ val iter_T = \<^Type>\<open>bisim_iterator\<close>
+ val bisim_max = \<^Const>\<open>bisim_iterator_max\<close>
val n_var = Var (("n", 0), iter_T)
val n_var_minus_1 =
Const (\<^const_name>\<open>safe_The\<close>, (iter_T --> bool_T) --> iter_T)
@@ -2214,8 +2212,8 @@
fun repair_rec j (Const (\<^const_name>\<open>Ex\<close>, T1) $ Abs (s2, T2, t2')) =
Const (\<^const_name>\<open>Ex\<close>, T1)
$ Abs (s2, T2, repair_rec (j + 1) t2')
- | repair_rec j (\<^const>\<open>HOL.conj\<close> $ t1 $ t2) =
- \<^const>\<open>HOL.conj\<close> $ repair_rec j t1 $ repair_rec j t2
+ | repair_rec j \<^Const_>\<open>conj for t1 t2\<close> =
+ \<^Const>\<open>conj for \<open>repair_rec j t1\<close> \<open>repair_rec j t2\<close>\<close>
| repair_rec j t =
let val (head, args) = strip_comb t in
if head = Bound j then
@@ -2227,9 +2225,9 @@
val (nonrecs, recs) =
List.partition (curry (op =) 0 o num_occs_of_bound_in_term j)
(disjuncts_of body)
- val base_body = nonrecs |> List.foldl s_disj \<^const>\<open>False\<close>
+ val base_body = nonrecs |> List.foldl s_disj \<^Const>\<open>False\<close>
val step_body = recs |> map (repair_rec j)
- |> List.foldl s_disj \<^const>\<open>False\<close>
+ |> List.foldl s_disj \<^Const>\<open>False\<close>
in
(fold_rev Term.abs (tl xs) (incr_bv (~1, j, base_body))
|> ap_n_split (length arg_Ts) tuple_T bool_T,
@@ -2241,11 +2239,7 @@
in aux end
fun predicatify T t =
- let val set_T = HOLogic.mk_setT T in
- Abs (Name.uu, T,
- Const (\<^const_name>\<open>Set.member\<close>, T --> set_T --> bool_T)
- $ Bound 0 $ incr_boundvars 1 t)
- end
+ Abs (Name.uu, T, \<^Const>\<open>Set.member T for \<open>Bound 0\<close> \<open>incr_boundvars 1 t\<close>\<close>)
fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (s, T) def =
let
@@ -2365,7 +2359,7 @@
[inductive_pred_axiom hol_ctxt x]
else case def_of_const thy def_tables x of
SOME def =>
- \<^const>\<open>Trueprop\<close> $ HOLogic.mk_eq (Const x, def)
+ \<^Const>\<open>Trueprop\<close> $ HOLogic.mk_eq (Const x, def)
|> equationalize_term ctxt "" |> the |> single
| NONE => [])
| psimps => psimps)
@@ -2373,7 +2367,7 @@
fun is_equational_fun_surely_complete hol_ctxt x =
case equational_fun_axioms hol_ctxt x of
- [\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _)] =>
+ [\<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for t1 _\<close>\<close>] =>
strip_comb t1 |> snd |> forall is_Var
| _ => false
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Sep 28 22:08:51 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Sep 28 22:10:21 2021 +0200
@@ -333,8 +333,8 @@
else raise TYPE ("Nitpick_Model.format_fun.do_term", [T, T'], [])
in if T1' = T1 andalso T2' = T2 then t else do_fun T1' T2' T1 T2 t end
-fun truth_const_sort_key \<^const>\<open>True\<close> = "0"
- | truth_const_sort_key \<^const>\<open>False\<close> = "2"
+fun truth_const_sort_key \<^Const_>\<open>True\<close> = "0"
+ | truth_const_sort_key \<^Const_>\<open>False\<close> = "2"
| truth_const_sort_key _ = "1"
fun mk_tuple (Type (\<^type_name>\<open>prod\<close>, [T1, T2])) ts =
@@ -411,14 +411,14 @@
empty_const
| aux ((t1, t2) :: zs) =
aux zs
- |> t2 <> \<^const>\<open>False\<close>
+ |> t2 <> \<^Const>\<open>False\<close>
? curry (op $)
(insert_const
- $ (t1 |> t2 <> \<^const>\<open>True\<close>
+ $ (t1 |> t2 <> \<^Const>\<open>True\<close>
? curry (op $)
(Const (maybe_name, T --> T))))
in
- if forall (fn (_, t) => t <> \<^const>\<open>True\<close> andalso t <> \<^const>\<open>False\<close>)
+ if forall (fn (_, t) => t <> \<^Const>\<open>True\<close> andalso t <> \<^Const>\<open>False\<close>)
tps then
Const (unknown, set_T)
else
@@ -516,7 +516,7 @@
| term_for_atom seen \<^typ>\<open>prop\<close> _ j k =
HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j k)
| term_for_atom _ \<^typ>\<open>bool\<close> _ j _ =
- if j = 0 then \<^const>\<open>False\<close> else \<^const>\<open>True\<close>
+ if j = 0 then \<^Const>\<open>False\<close> else \<^Const>\<open>True\<close>
| term_for_atom seen T _ j k =
if T = nat_T then
HOLogic.mk_number nat_T j
@@ -524,7 +524,7 @@
HOLogic.mk_number int_T (int_for_atom (k, 0) j)
else if is_fp_iterator_type T then
HOLogic.mk_number nat_T (k - j - 1)
- else if T = \<^typ>\<open>bisim_iterator\<close> then
+ else if T = \<^Type>\<open>bisim_iterator\<close> then
HOLogic.mk_number nat_T j
else case data_type_spec data_types T of
NONE => nth_atom thy atomss pool T j
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Sep 28 22:08:51 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Sep 28 22:10:21 2021 +0200
@@ -829,10 +829,10 @@
" \<turnstile> " ^ Syntax.string_of_term ctxt t ^
" : _?");
case t of
- \<^const>\<open>False\<close> => (bool_M, accum ||> add_comp_frame (A Fls) Leq frame)
+ \<^Const_>\<open>False\<close> => (bool_M, accum ||> add_comp_frame (A Fls) Leq frame)
| Const (\<^const_name>\<open>None\<close>, T) =>
(mtype_for T, accum ||> add_comp_frame (A Fls) Leq frame)
- | \<^const>\<open>True\<close> => (bool_M, accum ||> add_comp_frame (A Tru) Leq frame)
+ | \<^Const_>\<open>True\<close> => (bool_M, accum ||> add_comp_frame (A Tru) Leq frame)
| (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ Bound 0 $ t2 =>
(* hack to exploit symmetry of equality when typing "insert" *)
(if t2 = Bound 0 then do_term \<^term>\<open>True\<close>
@@ -850,9 +850,9 @@
| \<^const_name>\<open>Ex\<close> =>
let val set_T = domain_type T in
do_term (Abs (Name.uu, set_T,
- \<^const>\<open>Not\<close> $ (HOLogic.mk_eq
+ \<^Const>\<open>Not\<close> $ (HOLogic.mk_eq
(Abs (Name.uu, domain_type set_T,
- \<^const>\<open>False\<close>),
+ \<^Const>\<open>False\<close>),
Bound 0)))) accum
end
| \<^const_name>\<open>HOL.eq\<close> => do_equals T accum
@@ -971,12 +971,11 @@
val (M', accum) =
do_term t' (accum |>> push_bound (V x) T M)
in (MFun (M, V x, M'), accum |>> pop_bound) end))
- | \<^const>\<open>Not\<close> $ t1 => do_connect imp_spec t1 \<^const>\<open>False\<close> accum
- | \<^const>\<open>conj\<close> $ t1 $ t2 => do_connect conj_spec t1 t2 accum
- | \<^const>\<open>disj\<close> $ t1 $ t2 => do_connect disj_spec t1 t2 accum
- | \<^const>\<open>implies\<close> $ t1 $ t2 => do_connect imp_spec t1 t2 accum
- | Const (\<^const_name>\<open>Let\<close>, _) $ t1 $ t2 =>
- do_term (betapply (t2, t1)) accum
+ | \<^Const_>\<open>Not for t1\<close> => do_connect imp_spec t1 \<^Const>\<open>False\<close> accum
+ | \<^Const_>\<open>conj for t1 t2\<close> => do_connect conj_spec t1 t2 accum
+ | \<^Const_>\<open>disj for t1 t2\<close> => do_connect disj_spec t1 t2 accum
+ | \<^Const_>\<open>implies for t1 t2\<close> => do_connect imp_spec t1 t2 accum
+ | \<^Const_>\<open>Let _ _ for t1 t2\<close> => do_term (betapply (t2, t1)) accum
| t1 $ t2 =>
let
fun is_in t (j, _) = loose_bvar1 (t, length bound_Ts - j - 1)
@@ -1060,7 +1059,7 @@
Const (s as \<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, T1, t1) =>
do_quantifier s T1 t1
| Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2 => do_equals t1 t2
- | \<^const>\<open>Trueprop\<close> $ t1 => do_formula sn t1 accum
+ | \<^Const_>\<open>Trueprop for t1\<close> => do_formula sn t1 accum
| Const (s as \<^const_name>\<open>All\<close>, _) $ Abs (_, T1, t1) =>
do_quantifier s T1 t1
| Const (s as \<^const_name>\<open>Ex\<close>, T0) $ (t1 as Abs (_, T1, t1')) =>
@@ -1068,19 +1067,17 @@
Plus => do_quantifier s T1 t1'
| Minus =>
(* FIXME: Needed? *)
- do_term (\<^const>\<open>Not\<close>
+ do_term (\<^Const>\<open>Not\<close>
$ (HOLogic.eq_const (domain_type T0) $ t1
- $ Abs (Name.uu, T1, \<^const>\<open>False\<close>))) accum)
- | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2 => do_equals t1 t2
- | Const (\<^const_name>\<open>Let\<close>, _) $ t1 $ t2 =>
- do_formula sn (betapply (t2, t1)) accum
- | \<^const>\<open>Pure.conjunction\<close> $ t1 $ t2 =>
- do_connect meta_conj_spec false t1 t2 accum
- | \<^const>\<open>Pure.imp\<close> $ t1 $ t2 => do_connect meta_imp_spec true t1 t2 accum
- | \<^const>\<open>Not\<close> $ t1 => do_connect imp_spec true t1 \<^const>\<open>False\<close> accum
- | \<^const>\<open>conj\<close> $ t1 $ t2 => do_connect conj_spec false t1 t2 accum
- | \<^const>\<open>disj\<close> $ t1 $ t2 => do_connect disj_spec false t1 t2 accum
- | \<^const>\<open>implies\<close> $ t1 $ t2 => do_connect imp_spec true t1 t2 accum
+ $ Abs (Name.uu, T1, \<^Const>\<open>False\<close>))) accum)
+ | \<^Const_>\<open>HOL.eq _ for t1 t2\<close> => do_equals t1 t2
+ | \<^Const_>\<open>Let _ _ for t1 t2\<close> => do_formula sn (betapply (t2, t1)) accum
+ | \<^Const_>\<open>Pure.conjunction for t1 t2\<close> => do_connect meta_conj_spec false t1 t2 accum
+ | \<^Const_>\<open>Pure.imp for t1 t2\<close> => do_connect meta_imp_spec true t1 t2 accum
+ | \<^Const_>\<open>Not for t1\<close> => do_connect imp_spec true t1 \<^Const>\<open>False\<close> accum
+ | \<^Const_>\<open>conj for t1 t2\<close> => do_connect conj_spec false t1 t2 accum
+ | \<^Const_>\<open>disj for t1 t2\<close> => do_connect disj_spec false t1 t2 accum
+ | \<^Const_>\<open>implies for t1 t2\<close> => do_connect imp_spec true t1 t2 accum
| _ => do_term t accum
end
|> tap (fn (gamma, _) =>
@@ -1122,18 +1119,15 @@
and do_implies t1 t2 = do_term t1 #> do_formula t2
and do_formula t accum =
case t of
- Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
- | \<^const>\<open>Trueprop\<close> $ t1 => do_formula t1 accum
- | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2 =>
- consider_general_equals mdata true t1 t2 accum
- | \<^const>\<open>Pure.imp\<close> $ t1 $ t2 => do_implies t1 t2 accum
- | \<^const>\<open>Pure.conjunction\<close> $ t1 $ t2 =>
- fold (do_formula) [t1, t2] accum
- | Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
- | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2 =>
- consider_general_equals mdata true t1 t2 accum
- | \<^const>\<open>conj\<close> $ t1 $ t2 => fold (do_formula) [t1, t2] accum
- | \<^const>\<open>implies\<close> $ t1 $ t2 => do_implies t1 t2 accum
+ \<^Const_>\<open>Pure.all _ for \<open>Abs (_, T1, t1)\<close>\<close> => do_all T1 t1 accum
+ | \<^Const_>\<open>Trueprop for t1\<close> => do_formula t1 accum
+ | \<^Const_>\<open>Pure.eq _ for t1 t2\<close> => consider_general_equals mdata true t1 t2 accum
+ | \<^Const_>\<open>Pure.imp for t1 t2\<close> => do_implies t1 t2 accum
+ | \<^Const_>\<open>Pure.conjunction for t1 t2\<close> => fold (do_formula) [t1, t2] accum
+ | \<^Const_>\<open>All _ for \<open>Abs (_, T1, t1)\<close>\<close> => do_all T1 t1 accum
+ | \<^Const_>\<open>HOL.eq _ for t1 t2\<close> => consider_general_equals mdata true t1 t2 accum
+ | \<^Const_>\<open>conj for t1 t2\<close> => fold (do_formula) [t1, t2] accum
+ | \<^Const_>\<open>implies for t1 t2\<close> => do_implies t1 t2 accum
| _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
\do_formula", [t])
in do_formula t end
--- 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 =>