--- a/src/ZF/Inductive.thy Sat Sep 11 22:07:43 2021 +0200
+++ b/src/ZF/Inductive.thy Sat Sep 11 22:28:01 2021 +0200
@@ -37,8 +37,8 @@
ML \<open>
structure Lfp =
struct
- val oper = \<^const>\<open>lfp\<close>
- val bnd_mono = \<^const>\<open>bnd_mono\<close>
+ val oper = \<^Const>\<open>lfp\<close>
+ val bnd_mono = \<^Const>\<open>bnd_mono\<close>
val bnd_monoI = @{thm bnd_monoI}
val subs = @{thm def_lfp_subset}
val Tarski = @{thm def_lfp_unfold}
@@ -47,8 +47,8 @@
structure Standard_Prod =
struct
- val sigma = \<^const>\<open>Sigma\<close>
- val pair = \<^const>\<open>Pair\<close>
+ val sigma = \<^Const>\<open>Sigma\<close>
+ val pair = \<^Const>\<open>Pair\<close>
val split_name = \<^const_name>\<open>split\<close>
val pair_iff = @{thm Pair_iff}
val split_eq = @{thm split}
@@ -61,10 +61,10 @@
structure Standard_Sum =
struct
- val sum = \<^const>\<open>sum\<close>
- val inl = \<^const>\<open>Inl\<close>
- val inr = \<^const>\<open>Inr\<close>
- val elim = \<^const>\<open>case\<close>
+ val sum = \<^Const>\<open>sum\<close>
+ val inl = \<^Const>\<open>Inl\<close>
+ val inr = \<^Const>\<open>Inr\<close>
+ val elim = \<^Const>\<open>case\<close>
val case_inl = @{thm case_Inl}
val case_inr = @{thm case_Inr}
val inl_iff = @{thm Inl_iff}
@@ -84,8 +84,8 @@
structure Gfp =
struct
- val oper = \<^const>\<open>gfp\<close>
- val bnd_mono = \<^const>\<open>bnd_mono\<close>
+ val oper = \<^Const>\<open>gfp\<close>
+ val bnd_mono = \<^Const>\<open>bnd_mono\<close>
val bnd_monoI = @{thm bnd_monoI}
val subs = @{thm def_gfp_subset}
val Tarski = @{thm def_gfp_unfold}
@@ -94,8 +94,8 @@
structure Quine_Prod =
struct
- val sigma = \<^const>\<open>QSigma\<close>
- val pair = \<^const>\<open>QPair\<close>
+ val sigma = \<^Const>\<open>QSigma\<close>
+ val pair = \<^Const>\<open>QPair\<close>
val split_name = \<^const_name>\<open>qsplit\<close>
val pair_iff = @{thm QPair_iff}
val split_eq = @{thm qsplit}
@@ -108,10 +108,10 @@
structure Quine_Sum =
struct
- val sum = \<^const>\<open>qsum\<close>
- val inl = \<^const>\<open>QInl\<close>
- val inr = \<^const>\<open>QInr\<close>
- val elim = \<^const>\<open>qcase\<close>
+ val sum = \<^Const>\<open>qsum\<close>
+ val inl = \<^Const>\<open>QInl\<close>
+ val inr = \<^Const>\<open>QInr\<close>
+ val elim = \<^Const>\<open>qcase\<close>
val case_inl = @{thm qcase_QInl}
val case_inr = @{thm qcase_QInr}
val inl_iff = @{thm QInl_iff}
--- a/src/ZF/Tools/datatype_package.ML Sat Sep 11 22:07:43 2021 +0200
+++ b/src/ZF/Tools/datatype_package.ML Sat Sep 11 22:28:01 2021 +0200
@@ -56,7 +56,7 @@
Syntax.string_of_term_global \<^theory>\<open>IFOL\<close> t));
val rec_names = (*nat doesn't have to be added*)
\<^const_name>\<open>nat\<close> :: map (#1 o dest_Const) rec_hds
- val u = if co then \<^const>\<open>QUniv.quniv\<close> else \<^const>\<open>Univ.univ\<close>
+ val u = if co then \<^Const>\<open>QUniv.quniv\<close> else \<^Const>\<open>Univ.univ\<close>
val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms)
(fn t as Const (a, _) => if member (op =) rec_names a then I else insert (op =) t
| _ => I)) con_ty_lists [];
@@ -88,7 +88,7 @@
(** Define the constructors **)
(*The empty tuple is 0*)
- fun mk_tuple [] = \<^const>\<open>zero\<close>
+ fun mk_tuple [] = \<^Const>\<open>zero\<close>
| mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args;
fun mk_inject n k u = Balanced_Tree.access
@@ -162,7 +162,7 @@
Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
(*a recursive call for x is the application rec`x *)
- val rec_call = \<^const>\<open>apply\<close> $ Free ("rec", \<^typ>\<open>i\<close>);
+ val rec_call = \<^Const>\<open>apply\<close> $ Free ("rec", \<^typ>\<open>i\<close>);
(*look back down the "case args" (which have been reversed) to
determine the de Bruijn index*)
@@ -231,7 +231,7 @@
val recursor_def =
Misc_Legacy.mk_defpair
(recursor_tm,
- \<^const>\<open>Univ.Vrecursor\<close> $
+ \<^Const>\<open>Univ.Vrecursor\<close> $
absfree ("rec", \<^typ>\<open>i\<close>) (list_comb (case_const, recursor_cases)));
(* Build the new theory *)
--- a/src/ZF/Tools/inductive_package.ML Sat Sep 11 22:07:43 2021 +0200
+++ b/src/ZF/Tools/inductive_package.ML Sat Sep 11 22:28:01 2021 +0200
@@ -115,7 +115,7 @@
(*The Part(A,h) terms -- compose injections to make h*)
fun mk_Part (Bound 0) = Free(X', Ind_Syntax.iT) (*no mutual rec, no Part needed*)
- | mk_Part h = \<^const>\<open>Part\<close> $ Free(X', Ind_Syntax.iT) $ Abs (w', Ind_Syntax.iT, h);
+ | mk_Part h = \<^Const>\<open>Part\<close> $ Free(X', Ind_Syntax.iT) $ Abs (w', Ind_Syntax.iT, h);
(*Access to balanced disjoint sums via injections*)
val parts = map mk_Part
@@ -302,7 +302,7 @@
SOME pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
| NONE => (*possibly membership in M(rec_tm), for M monotone*)
let fun mk_sb (rec_tm,pred) =
- (rec_tm, \<^const>\<open>Collect\<close> $ rec_tm $ pred)
+ (rec_tm, \<^Const>\<open>Collect\<close> $ rec_tm $ pred)
in subst_free (map mk_sb ind_alist) prem :: iprems end)
| add_induct_prem ind_alist (prem,iprems) = prem :: iprems;
@@ -390,8 +390,7 @@
elem_factors ---> FOLogic.oT)
val qconcl =
List.foldr FOLogic.mk_all
- (FOLogic.imp $
- (\<^const>\<open>mem\<close> $ elem_tuple $ rec_tm)
+ (FOLogic.imp $ \<^Const>\<open>mem for elem_tuple rec_tm\<close>
$ (list_comb (pfree, elem_frees))) elem_frees
in (CP.ap_split elem_type FOLogic.oT pfree,
qconcl)
@@ -401,8 +400,7 @@
(*Used to form simultaneous induction lemma*)
fun mk_rec_imp (rec_tm,pred) =
- FOLogic.imp $ (\<^const>\<open>mem\<close> $ Bound 0 $ rec_tm) $
- (pred $ Bound 0);
+ FOLogic.imp $ \<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close> $ (pred $ Bound 0);
(*To instantiate the main induction rule*)
val induct_concl =
--- a/src/ZF/ind_syntax.ML Sat Sep 11 22:07:43 2021 +0200
+++ b/src/ZF/ind_syntax.ML Sat Sep 11 22:28:01 2021 +0200
@@ -23,10 +23,9 @@
(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
fun mk_all_imp (A,P) =
FOLogic.all_const iT $
- Abs("v", iT, FOLogic.imp $ (\<^const>\<open>mem\<close> $ Bound 0 $ A) $
- Term.betapply(P, Bound 0));
+ Abs("v", iT, FOLogic.imp $ \<^Const>\<open>mem for \<open>Bound 0\<close> A\<close> $ Term.betapply(P, Bound 0));
-fun mk_Collect (a, D, t) = \<^const>\<open>Collect\<close> $ D $ absfree (a, iT) t;
+fun mk_Collect (a, D, t) = \<^Const>\<open>Collect for D\<close> $ absfree (a, iT) t;
(*simple error-checking in the premises of an inductive definition*)
fun chk_prem rec_hd \<^Const_>\<open>conj for _ _\<close> =
@@ -82,20 +81,19 @@
Logic.list_implies
(map FOLogic.mk_Trueprop prems,
FOLogic.mk_Trueprop
- (\<^const>\<open>mem\<close> $ list_comb (Const (Sign.full_bname sg name, T), args)
- $ rec_tm))
+ (\<^Const>\<open>mem\<close> $ list_comb (Const (Sign.full_bname sg name, T), args) $ rec_tm))
in map mk_intr constructs end;
fun mk_all_intr_tms sg arg = flat (ListPair.map (mk_intr_tms sg) arg);
-fun mk_Un (t1, t2) = \<^const>\<open>Un\<close> $ t1 $ t2;
+fun mk_Un (t1, t2) = \<^Const>\<open>Un for t1 t2\<close>;
(*Make a datatype's domain: form the union of its set parameters*)
fun union_params (rec_tm, cs) =
let val (_,args) = strip_comb rec_tm
fun is_ind arg = (type_of arg = iT)
in case filter is_ind (args @ cs) of
- [] => \<^const>\<open>zero\<close>
+ [] => \<^Const>\<open>zero\<close>
| u_args => Balanced_Tree.make mk_Un u_args
end;
--- a/src/ZF/int_arith.ML Sat Sep 11 22:07:43 2021 +0200
+++ b/src/ZF/int_arith.ML Sat Sep 11 22:28:01 2021 +0200
@@ -42,7 +42,7 @@
(*Utilities*)
-fun mk_numeral i = \<^const>\<open>integ_of\<close> $ mk_bin i;
+fun mk_numeral i = \<^Const>\<open>integ_of\<close> $ mk_bin i;
fun dest_numeral \<^Const_>\<open>integ_of for w\<close> = dest_bin w
| dest_numeral t = raise TERM ("dest_numeral", [t]);
@@ -70,7 +70,7 @@
| dest_summing (pos, \<^Const_>\<open>zdiff for t u\<close>, ts) =
dest_summing (pos, t, dest_summing (not pos, u, ts))
| dest_summing (pos, t, ts) =
- if pos then t::ts else \<^const>\<open>zminus\<close> $ t :: ts;
+ if pos then t::ts else \<^Const>\<open>zminus for t\<close> :: ts;
fun dest_sum t = dest_summing (true, t, []);