--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Sep 28 22:10:21 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Sep 28 22:12:52 2021 +0200
@@ -2215,7 +2215,7 @@
let
fun mk_goal c cps gcorec n k disc =
mk_Trueprop_eq (disc $ (gcorec $ c),
- if n = 1 then \<^const>\<open>True\<close>
+ if n = 1 then \<^Const>\<open>True\<close>
else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps));
val goalss = @{map 6} (map2 oooo mk_goal) cs cpss gcorecs ns kss discss;
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Tue Sep 28 22:10:21 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Tue Sep 28 22:12:52 2021 +0200
@@ -42,7 +42,7 @@
let
fun instantiate_with_lambda thm =
let
- val prop as \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Var (_, fT) $ _) $ _) =
+ val prop as \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>HOL.eq _ for \<open>Var (_, fT) $ _\<close> _\<close>\<close>\<close> =
Thm.prop_of thm;
val T = range_type fT;
val j = Term.maxidx_of_term prop + 1;
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Tue Sep 28 22:10:21 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Tue Sep 28 22:12:52 2021 +0200
@@ -385,7 +385,7 @@
val ssig_map_thms = #map_thms ssig_fp_bnf_sugar;
val all_algLam_alg_pointfuls = map (mk_pointful ctxt) all_algLam_algs;
- val \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs) = code_goal;
+ val \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for lhs rhs\<close>\<close> = code_goal;
val (fun_t, args) = strip_comb lhs;
val closed_rhs = fold_rev lambda args rhs;
@@ -447,7 +447,7 @@
val fp_nesting_Ts = map T_of_bnf fp_nesting_bnfs;
- fun is_nullary_disc_def (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _
+ fun is_nullary_disc_def (\<^Const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _
$ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _))) = true
| is_nullary_disc_def (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _
$ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _)) = true
@@ -512,7 +512,7 @@
val goal = mk_Trueprop_eq (fun_t, abs_curried_balanced arg_Ts algrho);
fun const_of_transfer thm =
- (case Thm.prop_of thm of \<^const>\<open>Trueprop\<close> $ (_ $ cst $ _) => cst);
+ (case Thm.prop_of thm of \<^Const>\<open>Trueprop\<close> $ (_ $ cst $ _) => cst);
val eq_algrho =
Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
@@ -590,7 +590,7 @@
fun derive_cong_ctr_intros ctxt cong_ctor_intro =
let
- val \<^const>\<open>Pure.imp\<close> $ _ $ (\<^const>\<open>Trueprop\<close> $ ((Rcong as _ $ _) $ _ $ (ctor $ _))) =
+ val \<^Const_>\<open>Pure.imp\<close> $ _ $ (\<^Const_>\<open>Trueprop\<close> $ ((Rcong as _ $ _) $ _ $ (ctor $ _))) =
Thm.prop_of cong_ctor_intro;
val fpT as Type (fpT_name, fp_argTs) = range_type (fastype_of ctor);
@@ -615,19 +615,19 @@
fun derive_cong_friend_intro ctxt cong_algrho_intro =
let
- val \<^const>\<open>Pure.imp\<close> $ _ $ (\<^const>\<open>Trueprop\<close> $ ((Rcong as _ $ _) $ _
+ val \<^Const_>\<open>Pure.imp\<close> $ _ $ (\<^Const_>\<open>Trueprop\<close> $ ((Rcong as _ $ _) $ _
$ ((algrho as Const (algrho_name, _)) $ _))) =
Thm.prop_of cong_algrho_intro;
val fpT as Type (_, fp_argTs) = range_type (fastype_of algrho);
- fun has_algrho (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ rhs)) =
+ fun has_algrho (\<^Const_>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ rhs)) =
fst (dest_Const (head_of (strip_abs_body rhs))) = algrho_name;
val eq_algrho :: _ =
maps (filter (has_algrho o Thm.prop_of) o #eq_algrhos o snd) (all_friend_extras_of ctxt);
- val \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ friend0 $ _) = Thm.prop_of eq_algrho;
+ val \<^Const_>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ friend0 $ _) = Thm.prop_of eq_algrho;
val friend = mk_ctr fp_argTs friend0;
val goal = mk_cong_intro_ctr_or_friend_goal ctxt fpT Rcong friend;
@@ -654,8 +654,8 @@
let
val thy = Proof_Context.theory_of ctxt;
- val \<^const>\<open>Pure.imp\<close> $ (\<^const>\<open>Trueprop\<close> $ (_ $ Abs (_, _, _ $
- Abs (_, _, \<^const>\<open>implies\<close> $ _ $ (_ $ (cong0 $ _) $ _ $ _))))) $ _ =
+ val \<^Const_>\<open>Pure.imp\<close> $ (\<^Const_>\<open>Trueprop\<close> $ (_ $ Abs (_, _, _ $
+ Abs (_, _, \<^Const_>\<open>implies\<close> $ _ $ (_ $ (cong0 $ _) $ _ $ _))))) $ _ =
Thm.prop_of dtor_coinduct;
val SOME {X as TVar ((X_s, _), _), fp_res = {dtor_ctors, ...}, pre_bnf,
@@ -820,7 +820,7 @@
|> curry (op ~~) (map (fn disc => disc $ lhs) discs);
fun mk_disc_iff_props props [] = props
- | mk_disc_iff_props _ ((lhs, \<^const>\<open>HOL.True\<close>) :: _) = [lhs]
+ | mk_disc_iff_props _ ((lhs, \<^Const_>\<open>True\<close>) :: _) = [lhs]
| mk_disc_iff_props props ((lhs, rhs) :: views) =
mk_disc_iff_props ((HOLogic.mk_eq (lhs, rhs)) :: props) views;
in
@@ -2242,7 +2242,7 @@
val fun_T =
(case code_goal of
- \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _) => fastype_of (head_of t)
+ \<^Const_>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _) => fastype_of (head_of t)
| _ => ill_formed_equation_lhs_rhs lthy [code_goal]);
val fun_t = Const (fun_name, fun_T);
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML Tue Sep 28 22:10:21 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML Tue Sep 28 22:12:52 2021 +0200
@@ -367,7 +367,7 @@
ctrXs_Tss
|> map_index (fn (i, Ts) =>
Abs (Name.uu, mk_tupleT_balanced Ts,
- if i + 1 = k then \<^const>\<open>HOL.True\<close> else \<^const>\<open>HOL.False\<close>))
+ if i + 1 = k then \<^Const>\<open>True\<close> else \<^Const>\<open>False\<close>))
|> mk_case_sumN_balanced
|> map_types substXYT
|> (fn tm => Library.foldl1 HOLogic.mk_comp [tm, rep, snd_const YpreT])
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Sep 28 22:10:21 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Sep 28 22:12:52 2021 +0200
@@ -189,22 +189,22 @@
fun sort_list_duplicates xs = map snd (sort (int_ord o apply2 fst) xs);
-val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default \<^const>\<open>True\<close>;
-val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default \<^const>\<open>False\<close>;
+val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default \<^Const>\<open>True\<close>;
+val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default \<^Const>\<open>False\<close>;
val mk_dnf = mk_disjs o map mk_conjs;
-val conjuncts_s = filter_out (curry (op aconv) \<^const>\<open>True\<close>) o HOLogic.conjuncts;
+val conjuncts_s = filter_out (curry (op aconv) \<^Const>\<open>True\<close>) o HOLogic.conjuncts;
-fun s_not \<^const>\<open>True\<close> = \<^const>\<open>False\<close>
- | s_not \<^const>\<open>False\<close> = \<^const>\<open>True\<close>
- | s_not (\<^const>\<open>Not\<close> $ t) = t
- | s_not (\<^const>\<open>conj\<close> $ t $ u) = \<^const>\<open>disj\<close> $ s_not t $ s_not u
- | s_not (\<^const>\<open>disj\<close> $ t $ u) = \<^const>\<open>conj\<close> $ s_not t $ s_not u
- | s_not t = \<^const>\<open>Not\<close> $ t;
+fun s_not \<^Const_>\<open>True\<close> = \<^Const>\<open>False\<close>
+ | s_not \<^Const_>\<open>False\<close> = \<^Const>\<open>True\<close>
+ | s_not \<^Const_>\<open>Not for t\<close> = t
+ | s_not \<^Const_>\<open>conj for t u\<close> = \<^Const>\<open>disj for \<open>s_not t\<close> \<open>s_not u\<close>\<close>
+ | s_not \<^Const_>\<open>disj for t u\<close> = \<^Const>\<open>conj for \<open>s_not t\<close> \<open>s_not u\<close>\<close>
+ | s_not t = \<^Const>\<open>Not for t\<close>;
val s_not_conj = conjuncts_s o s_not o mk_conjs;
-fun propagate_unit_pos u cs = if member (op aconv) cs u then [\<^const>\<open>False\<close>] else cs;
+fun propagate_unit_pos u cs = if member (op aconv) cs u then [\<^Const>\<open>False\<close>] else cs;
fun propagate_unit_neg not_u cs = remove (op aconv) not_u cs;
fun propagate_units css =
@@ -215,17 +215,17 @@
(map (propagate_unit_pos u) (uss @ css'))));
fun s_conjs cs =
- if member (op aconv) cs \<^const>\<open>False\<close> then \<^const>\<open>False\<close>
- else mk_conjs (remove (op aconv) \<^const>\<open>True\<close> cs);
+ if member (op aconv) cs \<^Const>\<open>False\<close> then \<^Const>\<open>False\<close>
+ else mk_conjs (remove (op aconv) \<^Const>\<open>True\<close> cs);
fun s_disjs ds =
- if member (op aconv) ds \<^const>\<open>True\<close> then \<^const>\<open>True\<close>
- else mk_disjs (remove (op aconv) \<^const>\<open>False\<close> ds);
+ if member (op aconv) ds \<^Const>\<open>True\<close> then \<^Const>\<open>True\<close>
+ else mk_disjs (remove (op aconv) \<^Const>\<open>False\<close> ds);
fun s_dnf css0 =
let val css = propagate_units css0 in
if null css then
- [\<^const>\<open>False\<close>]
+ [\<^Const>\<open>False\<close>]
else if exists null css then
[]
else
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Tue Sep 28 22:10:21 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Tue Sep 28 22:12:52 2021 +0200
@@ -154,7 +154,7 @@
fun inst_split_eq ctxt split =
(case Thm.prop_of split of
- \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Var (_, Type (_, [T, _])) $ _) $ _) =>
+ \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for \<open>Var (_, Type (_, [T, _])) $ _\<close> _\<close>\<close> =>
let
val s = Name.uu;
val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
--- a/src/HOL/Tools/BNF/bnf_lfp_countable.ML Tue Sep 28 22:10:21 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_countable.ML Tue Sep 28 22:12:52 2021 +0200
@@ -70,13 +70,13 @@
fun encode_sumN n k t =
Balanced_Tree.access {init = t,
- left = fn t => \<^const>\<open>sum_encode\<close> $ (@{const Inl (nat, nat)} $ t),
- right = fn t => \<^const>\<open>sum_encode\<close> $ (@{const Inr (nat, nat)} $ t)}
+ left = fn t => \<^Const>\<open>sum_encode for \<^Const>\<open>Inl \<^Type>\<open>nat\<close> \<^Type>\<open>nat\<close> for t\<close>\<close>,
+ right = fn t => \<^Const>\<open>sum_encode for \<^Const>\<open>Inr \<^Type>\<open>nat\<close> \<^Type>\<open>nat\<close> for t\<close>\<close>}
n k;
-fun encode_tuple [] = \<^term>\<open>0 :: nat\<close>
+fun encode_tuple [] = \<^Const>\<open>zero_class.zero \<^Type>\<open>nat\<close>\<close>
| encode_tuple ts =
- Balanced_Tree.make (fn (t, u) => \<^const>\<open>prod_encode\<close> $ (@{const Pair (nat, nat)} $ u $ t)) ts;
+ Balanced_Tree.make (fn (t, u) => \<^Const>\<open>prod_encode for \<^Const>\<open>Pair \<^Type>\<open>nat\<close> \<^Type>\<open>nat\<close> for u t\<close>\<close>) ts;
fun mk_encode_funs ctxt fpTs ns ctrss0 recs0 =
let
@@ -181,7 +181,7 @@
|> map (Thm.close_derivation \<^here>)
end;
-fun get_countable_goal_type_name (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>Ex\<close>, _)
+fun get_countable_goal_type_name (\<^Const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>Ex\<close>, _)
$ Abs (_, Type (_, [Type (s, _), _]), Const (\<^const_name>\<open>inj_on\<close>, _) $ Bound 0
$ Const (\<^const_name>\<open>top\<close>, _)))) = s
| get_countable_goal_type_name _ = error "Wrong goal format for datatype countability tactic";