clarified signature -- prefer antiquotations (with subtle change of exception content);
--- a/src/FOL/fologic.ML Sun Sep 19 21:35:51 2021 +0200
+++ b/src/FOL/fologic.ML Sun Sep 19 21:37:14 2021 +0200
@@ -6,14 +6,8 @@
signature FOLOGIC =
sig
- val oT: typ
val mk_Trueprop: term -> term
val dest_Trueprop: term -> term
- val not: term
- val conj: term
- val disj: term
- val imp: term
- val iff: term
val mk_conj: term * term -> term
val mk_disj: term * term -> term
val mk_imp: term * term -> term
@@ -28,52 +22,32 @@
val eq_const: typ -> term
val mk_eq: term * term -> term
val dest_eq: term -> term * term
- val mk_binop: string -> term * term -> term
- val mk_binrel: string -> term * term -> term
- val dest_bin: string -> typ -> term -> term * term
end;
structure FOLogic: FOLOGIC =
struct
-val oT = \<^Type>\<open>o\<close>;
-
-val Trueprop = \<^Const>\<open>Trueprop\<close>;
-
-fun mk_Trueprop P = Trueprop $ P;
+fun mk_Trueprop P = \<^Const>\<open>Trueprop for P\<close>;
-fun dest_Trueprop \<^Const_>\<open>Trueprop for P\<close> = P
- | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
-
-
-(* Logical constants *)
+val dest_Trueprop = \<^Const_fn>\<open>Trueprop for P => P\<close>;
-val not = \<^Const>\<open>Not\<close>;
-val conj = \<^Const>\<open>conj\<close>;
-val disj = \<^Const>\<open>disj\<close>;
-val imp = \<^Const>\<open>imp\<close>;
-val iff = \<^Const>\<open>iff\<close>;
+fun mk_conj (t1, t2) = \<^Const>\<open>conj for t1 t2\<close>
+and mk_disj (t1, t2) = \<^Const>\<open>disj for t1 t2\<close>
+and mk_imp (t1, t2) = \<^Const>\<open>imp for t1 t2\<close>
+and mk_iff (t1, t2) = \<^Const>\<open>iff for t1 t2\<close>;
-fun mk_conj (t1, t2) = conj $ t1 $ t2
-and mk_disj (t1, t2) = disj $ t1 $ t2
-and mk_imp (t1, t2) = imp $ t1 $ t2
-and mk_iff (t1, t2) = iff $ t1 $ t2;
-
-fun dest_imp \<^Const_>\<open>imp for A B\<close> = (A, B)
- | dest_imp t = raise TERM ("dest_imp", [t]);
+val dest_imp = \<^Const_fn>\<open>imp for A B => \<open>(A, B)\<close>\<close>;
fun dest_conj \<^Const_>\<open>conj for t t'\<close> = t :: dest_conj t'
| dest_conj t = [t];
-fun dest_iff \<^Const_>\<open>iff for A B\<close> = (A, B)
- | dest_iff t = raise TERM ("dest_iff", [t]);
+val dest_iff = \<^Const_fn>\<open>iff for A B => \<open>(A, B)\<close>\<close>;
fun eq_const T = \<^Const>\<open>eq T\<close>;
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
-fun dest_eq \<^Const_>\<open>eq _ for lhs rhs\<close> = (lhs, rhs)
- | dest_eq t = raise TERM ("dest_eq", [t])
+val dest_eq = \<^Const_fn>\<open>eq _ for lhs rhs => \<open>(lhs, rhs)\<close>\<close>;
fun all_const T = \<^Const>\<open>All T\<close>;
fun mk_all (Free (x, T), P) = all_const T $ absfree (x, T) P;
@@ -81,22 +55,4 @@
fun exists_const T = \<^Const>\<open>Ex T\<close>;
fun mk_exists (Free (x, T), P) = exists_const T $ absfree (x, T) P;
-
-(* binary operations and relations *)
-
-fun mk_binop c (t, u) =
- let val T = fastype_of t in
- Const (c, [T, T] ---> T) $ t $ u
- end;
-
-fun mk_binrel c (t, u) =
- let val T = fastype_of t in
- Const (c, [T, T] ---> oT) $ t $ u
- end;
-
-fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) =
- if c = c' andalso T = T' then (t, u)
- else raise TERM ("dest_bin " ^ c, [tm])
- | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]);
-
end;
--- a/src/FOL/simpdata.ML Sun Sep 19 21:35:51 2021 +0200
+++ b/src/FOL/simpdata.ML Sun Sep 19 21:37:14 2021 +0200
@@ -63,8 +63,8 @@
| dest_conj _ = NONE
fun dest_imp \<^Const_>\<open>imp for s t\<close> = SOME (s, t)
| dest_imp _ = NONE
- val conj = FOLogic.conj
- val imp = FOLogic.imp
+ val conj = \<^Const>\<open>conj\<close>
+ val imp = \<^Const>\<open>imp\<close>
(*rules*)
val iff_reflection = @{thm iff_reflection}
val iffI = @{thm iffI}
--- a/src/ZF/Tools/cartprod.ML Sun Sep 19 21:35:51 2021 +0200
+++ b/src/ZF/Tools/cartprod.ML Sun Sep 19 21:37:14 2021 +0200
@@ -70,24 +70,22 @@
fun pseudo_type (t $ A $ Abs(_,_,B)) =
if t = Pr.sigma
then mk_prod(pseudo_type A, pseudo_type B)
- else \<^typ>\<open>i\<close>
- | pseudo_type _ = \<^typ>\<open>i\<close>;
+ else \<^Type>\<open>i\<close>
+ | pseudo_type _ = \<^Type>\<open>i\<close>;
(*Maps the type T1*...*Tn to [T1,...,Tn], however nested*)
fun factors (Type("*", [T1, T2])) = factors T1 @ factors T2
| factors T = [T];
(*Make a well-typed instance of "split"*)
-fun split_const T = Const(Pr.split_name,
- [[Ind_Syntax.iT, Ind_Syntax.iT]--->T,
- Ind_Syntax.iT] ---> T);
+fun split_const T = Const(Pr.split_name, [[\<^Type>\<open>i\<close>, \<^Type>\<open>i\<close>]--->T, \<^Type>\<open>i\<close>] ---> T);
(*In ap_split S T u, term u expects separate arguments for the factors of S,
with result type T. The call creates a new term expecting one argument
of type S.*)
fun ap_split (Type("*", [T1,T2])) T3 u =
split_const T3 $
- Abs("v", Ind_Syntax.iT, (*Not T1, as it involves pseudo-product types*)
+ Abs("v", \<^Type>\<open>i\<close>, (*Not T1, as it involves pseudo-product types*)
ap_split T2 T3
((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $
Bound 0))
@@ -109,7 +107,7 @@
in
remove_split ctxt
(Drule.instantiate_normalize (TVars.empty,
- Vars.make [((v, Ind_Syntax.iT-->T2), Thm.cterm_of ctxt newt)]) rl)
+ Vars.make [((v, \<^Type>\<open>i\<close> --> T2), Thm.cterm_of ctxt newt)]) rl)
end
| split_rule_var _ (t,T,rl) = rl;
--- a/src/ZF/Tools/datatype_package.ML Sun Sep 19 21:35:51 2021 +0200
+++ b/src/ZF/Tools/datatype_package.ML Sun Sep 19 21:37:14 2021 +0200
@@ -115,10 +115,10 @@
(*Combine split terms using case; yields the case operator for one part*)
fun call_case case_list =
- let fun call_f (free,[]) = Abs("null", \<^typ>\<open>i\<close>, free)
+ let fun call_f (free,[]) = Abs("null", \<^Type>\<open>i\<close>, free)
| call_f (free,args) =
CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
- \<^typ>\<open>i\<close>
+ \<^Type>\<open>i\<close>
free
in Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list) end;
@@ -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", \<^Type>\<open>i\<close>);
(*look back down the "case args" (which have been reversed) to
determine the de Bruijn index*)
@@ -199,7 +199,7 @@
(*Add an argument position for each occurrence of a recursive set.
Strictly speaking, the recursive arguments are the LAST of the function
variable, but they all have type "i" anyway*)
- fun add_rec_args args' T = (map (fn _ => \<^typ>\<open>i\<close>) args') ---> T
+ fun add_rec_args args' T = (map (fn _ => \<^Type>\<open>i\<close>) args') ---> T
(*Plug in the function variable type needed for the recursor
as well as the new arguments (recursive calls)*)
@@ -232,7 +232,7 @@
Misc_Legacy.mk_defpair
(recursor_tm,
\<^Const>\<open>Univ.Vrecursor\<close> $
- absfree ("rec", \<^typ>\<open>i\<close>) (list_comb (case_const, recursor_cases)));
+ absfree ("rec", \<^Type>\<open>i\<close>) (list_comb (case_const, recursor_cases)));
(* Build the new theory *)
@@ -412,7 +412,7 @@
let
val ctxt = Proof_Context.init_global thy;
fun read_is strs =
- map (Syntax.parse_term ctxt #> Type.constraint \<^typ>\<open>i\<close>) strs
+ map (Syntax.parse_term ctxt #> Type.constraint \<^Type>\<open>i\<close>) strs
|> Syntax.check_terms ctxt;
val rec_tms = read_is srec_tms;
--- a/src/ZF/Tools/inductive_package.ML Sun Sep 19 21:35:51 2021 +0200
+++ b/src/ZF/Tools/inductive_package.ML Sun Sep 19 21:37:14 2021 +0200
@@ -108,14 +108,14 @@
let val prems = map dest_tprop (Logic.strip_imp_prems intr)
val dummy = List.app (fn rec_hd => List.app (Ind_Syntax.chk_prem rec_hd) prems) rec_hds
val exfrees = subtract (op =) rec_params (Misc_Legacy.term_frees intr)
- val zeq = FOLogic.mk_eq (Free(z', Ind_Syntax.iT), #1 (Ind_Syntax.rule_concl intr))
+ val zeq = FOLogic.mk_eq (Free(z', \<^Type>\<open>i\<close>), #1 (Ind_Syntax.rule_concl intr))
in List.foldr FOLogic.mk_exists
(Balanced_Tree.make FOLogic.mk_conj (zeq::prems)) exfrees
end;
(*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);
+ fun mk_Part (Bound 0) = Free(X', \<^Type>\<open>i\<close>) (*no mutual rec, no Part needed*)
+ | mk_Part h = \<^Const>\<open>Part\<close> $ Free(X', \<^Type>\<open>i\<close>) $ Abs (w', \<^Type>\<open>i\<close>, h);
(*Access to balanced disjoint sums via injections*)
val parts = map mk_Part
@@ -126,7 +126,7 @@
val part_intrs = map (subst_free (rec_tms ~~ parts) o fp_part) intr_tms;
val fp_abs =
- absfree (X', Ind_Syntax.iT)
+ absfree (X', \<^Type>\<open>i\<close>)
(Ind_Syntax.mk_Collect (z', dom_sum,
Balanced_Tree.make FOLogic.mk_disj part_intrs));
@@ -159,7 +159,7 @@
(case parts of
[_] => [] (*no mutual recursion*)
| _ => rec_tms ~~ (*define the sets as Parts*)
- map (subst_atomic [(Free (X', Ind_Syntax.iT), big_rec_tm)]) parts));
+ map (subst_atomic [(Free (X', \<^Type>\<open>i\<close>), big_rec_tm)]) parts));
(*tracing: print the fixedpoint definition*)
val dummy = if !Ind_Syntax.trace then
@@ -323,7 +323,7 @@
| ind_tac ctxt (prem::prems) i =
DEPTH_SOLVE_1 (ares_tac ctxt [prem, @{thm refl}] i) THEN ind_tac ctxt prems (i-1);
- val pred = Free(pred_name, Ind_Syntax.iT --> FOLogic.oT);
+ val pred = Free(pred_name, \<^Type>\<open>i\<close> --> \<^Type>\<open>o\<close>);
val ind_prems = map (induct_prem (map (rpair pred) rec_tms))
intr_tms;
@@ -387,12 +387,12 @@
fun mk_predpair rec_tm =
let val rec_name = (#1 o dest_Const o head_of) rec_tm
val pfree = Free(pred_name ^ "_" ^ Long_Name.base_name rec_name,
- elem_factors ---> FOLogic.oT)
+ elem_factors ---> \<^Type>\<open>o\<close>)
val qconcl =
List.foldr FOLogic.mk_all
- (FOLogic.imp $ \<^Const>\<open>mem for elem_tuple rec_tm\<close>
+ (\<^Const>\<open>imp\<close> $ \<^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,
+ in (CP.ap_split elem_type \<^Type>\<open>o\<close> pfree,
qconcl)
end;
@@ -400,14 +400,14 @@
(*Used to form simultaneous induction lemma*)
fun mk_rec_imp (rec_tm,pred) =
- FOLogic.imp $ \<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close> $ (pred $ Bound 0);
+ \<^Const>\<open>imp\<close> $ \<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close> $ (pred $ Bound 0);
(*To instantiate the main induction rule*)
val induct_concl =
FOLogic.mk_Trueprop
(Ind_Syntax.mk_all_imp
(big_rec_tm,
- Abs("z", Ind_Syntax.iT,
+ Abs("z", \<^Type>\<open>i\<close>,
Balanced_Tree.make FOLogic.mk_conj
(ListPair.map mk_rec_imp (rec_tms, preds)))))
and mutual_induct_concl =
@@ -515,7 +515,7 @@
val induct0 =
CP.split_rule_var ctxt4
- (pred_var, elem_type-->FOLogic.oT, induct0)
+ (pred_var, elem_type --> \<^Type>\<open>o\<close>, induct0)
|> Drule.export_without_context
and mutual_induct = CP.remove_split ctxt4 mutual_induct_fsplit
@@ -564,7 +564,7 @@
(raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
let
val ctxt = Proof_Context.init_global thy;
- val read_terms = map (Syntax.parse_term ctxt #> Type.constraint Ind_Syntax.iT)
+ val read_terms = map (Syntax.parse_term ctxt #> Type.constraint \<^Type>\<open>i\<close>)
#> Syntax.check_terms ctxt;
val intr_atts = map (map (Attrib.attribute_cmd ctxt) o snd) intr_srcs;
--- a/src/ZF/Tools/primrec_package.ML Sun Sep 19 21:35:51 2021 +0200
+++ b/src/ZF/Tools/primrec_package.ML Sun Sep 19 21:37:14 2021 +0200
@@ -106,7 +106,7 @@
and recursor_pairs = map (dest_eqn o Thm.concl_of) rec_rewrites
fun absterm (Free x, body) = absfree x body
- | absterm (t, body) = Abs("rec", Ind_Syntax.iT, abstract_over (t, body))
+ | absterm (t, body) = Abs("rec", \<^Type>\<open>i\<close>, abstract_over (t, body))
(*Translate rec equations into function arguments suitable for recursor.
Missing cases are replaced by 0 and all cases are put into order.*)
@@ -140,7 +140,7 @@
(*the recursive argument*)
val rec_arg =
Free (singleton (Name.variant_list (map #1 (ls@rs))) (Long_Name.base_name big_rec_name),
- Ind_Syntax.iT)
+ \<^Type>\<open>i\<close>)
val def_tm = Logic.mk_equals
(subst_bound (rec_arg, fabs),
--- a/src/ZF/arith_data.ML Sun Sep 19 21:35:51 2021 +0200
+++ b/src/ZF/arith_data.ML Sun Sep 19 21:37:14 2021 +0200
@@ -22,8 +22,6 @@
structure ArithData: ARITH_DATA =
struct
-val iT = Ind_Syntax.iT;
-
val zero = \<^Const>\<open>zero\<close>;
val succ = \<^Const>\<open>succ\<close>;
fun mk_succ t = succ $ t;
@@ -49,8 +47,9 @@
(*Use <-> or = depending on the type of t*)
fun mk_eq_iff(t,u) =
- if fastype_of t = iT then FOLogic.mk_eq(t,u)
- else FOLogic.mk_iff(t,u);
+ if fastype_of t = \<^Type>\<open>i\<close>
+ then \<^Const>\<open>IFOL.eq \<open>\<^Type>\<open>i\<close>\<close> for t u\<close>
+ else \<^Const>\<open>IFOL.iff for t u\<close>;
(*We remove equality assumptions because they confuse the simplifier and
because only type-checking assumptions are necessary.*)
@@ -79,12 +78,10 @@
| mk_prod (t :: ts) = if t = one then mk_prod ts
else mk_times (t, mk_prod ts);
-val dest_times = FOLogic.dest_bin \<^const_name>\<open>Arith.mult\<close> iT;
-
-fun dest_prod t =
- let val (t,u) = dest_times t
- in dest_prod t @ dest_prod u end
- handle TERM _ => [t];
+fun dest_prod tm =
+ let val (t,u) = \<^Const_fn>\<open>Arith.mult for t u => \<open>(t, u)\<close>\<close> tm
+ in dest_prod t @ dest_prod u end
+ handle TERM _ => [tm];
(*Dummy version: the only arguments are 0 and 1*)
fun mk_coeff (0, t) = zero
@@ -168,7 +165,7 @@
open CancelNumeralsCommon
val prove_conv = prove_conv "natless_cancel_numerals"
fun mk_bal (t, u) = \<^Const>\<open>Ordinal.lt for t u\<close>
- val dest_bal = FOLogic.dest_bin \<^const_name>\<open>Ordinal.lt\<close> iT
+ val dest_bal = \<^Const_fn>\<open>Ordinal.lt for t u => \<open>(t, u)\<close>\<close>
val bal_add1 = @{thm less_add_iff [THEN iff_trans]}
val bal_add2 = @{thm less_add_iff [THEN iff_trans]}
fun trans_tac ctxt = gen_trans_tac ctxt @{thm iff_trans}
@@ -181,7 +178,7 @@
open CancelNumeralsCommon
val prove_conv = prove_conv "natdiff_cancel_numerals"
fun mk_bal (t, u) = \<^Const>\<open>Arith.diff for t u\<close>
- val dest_bal = FOLogic.dest_bin \<^const_name>\<open>Arith.diff\<close> iT
+ val dest_bal = \<^Const_fn>\<open>Arith.diff for t u => \<open>(t, u)\<close>\<close>
val bal_add1 = @{thm diff_add_eq [THEN trans]}
val bal_add2 = @{thm diff_add_eq [THEN trans]}
fun trans_tac ctxt = gen_trans_tac ctxt @{thm trans}
--- a/src/ZF/ind_syntax.ML Sun Sep 19 21:35:51 2021 +0200
+++ b/src/ZF/ind_syntax.ML Sun Sep 19 21:37:14 2021 +0200
@@ -18,14 +18,12 @@
(** Abstract syntax definitions for ZF **)
-val iT = \<^Type>\<open>i\<close>;
-
(*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 for \<open>Bound 0\<close> A\<close> $ Term.betapply(P, Bound 0));
+ FOLogic.all_const \<^Type>\<open>i\<close> $
+ Abs("v", \<^Type>\<open>i\<close>, \<^Const>\<open>imp\<close> $ \<^Const>\<open>mem for \<open>Bound 0\<close> A\<close> $ Term.betapply(P, Bound 0));
-fun mk_Collect (a, D, t) = \<^Const>\<open>Collect for D\<close> $ absfree (a, iT) t;
+fun mk_Collect (a, D, t) = \<^Const>\<open>Collect for D\<close> $ absfree (a, \<^Type>\<open>i\<close>) t;
(*simple error-checking in the premises of an inductive definition*)
fun chk_prem rec_hd \<^Const_>\<open>conj for _ _\<close> =
@@ -64,10 +62,10 @@
(*read a constructor specification*)
fun read_construct ctxt (id: string, sprems, syn: mixfix) =
- let val prems = map (Syntax.parse_term ctxt #> Type.constraint FOLogic.oT) sprems
+ let val prems = map (Syntax.parse_term ctxt #> Type.constraint \<^Type>\<open>o\<close>) sprems
|> Syntax.check_terms ctxt
val args = map (#1 o dest_mem) prems
- val T = (map (#2 o dest_Free) args) ---> iT
+ val T = (map (#2 o dest_Free) args) ---> \<^Type>\<open>i\<close>
handle TERM _ => error
"Bad variable in constructor specification"
in ((id,T,syn), id, args, prems) end;
@@ -91,7 +89,7 @@
(*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)
+ fun is_ind arg = (type_of arg = \<^Type>\<open>i\<close>)
in case filter is_ind (args @ cs) of
[] => \<^Const>\<open>zero\<close>
| u_args => Balanced_Tree.make mk_Un u_args
--- a/src/ZF/int_arith.ML Sun Sep 19 21:35:51 2021 +0200
+++ b/src/ZF/int_arith.ML Sun Sep 19 21:37:14 2021 +0200
@@ -82,12 +82,10 @@
| mk_prod (t :: ts) = if t = one then mk_prod ts
else mk_times (t, mk_prod ts);
-val dest_times = FOLogic.dest_bin \<^const_name>\<open>zmult\<close> \<^typ>\<open>i\<close>;
-
-fun dest_prod t =
- let val (t,u) = dest_times t
- in dest_prod t @ dest_prod u end
- handle TERM _ => [t];
+fun dest_prod tm =
+ let val (t,u) = \<^Const_fn>\<open>zmult for t u => \<open>(t, u)\<close>\<close> tm
+ in dest_prod t @ dest_prod u end
+ handle TERM _ => [tm];
(*DON'T do the obvious simplifications; that would create special cases*)
fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
@@ -192,7 +190,7 @@
(open CancelNumeralsCommon
val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
fun mk_bal (t, u) = \<^Const>\<open>zless for t u\<close>
- val dest_bal = FOLogic.dest_bin \<^const_name>\<open>zless\<close> \<^typ>\<open>i\<close>
+ val dest_bal = \<^Const_fn>\<open>zless for t u => \<open>(t, u)\<close>\<close>
val bal_add1 = @{thm less_add_iff1} RS @{thm iff_trans}
val bal_add2 = @{thm less_add_iff2} RS @{thm iff_trans}
);
@@ -201,7 +199,7 @@
(open CancelNumeralsCommon
val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
fun mk_bal (t, u) = \<^Const>\<open>zle for t u\<close>
- val dest_bal = FOLogic.dest_bin \<^const_name>\<open>zle\<close> \<^typ>\<open>i\<close>
+ val dest_bal = \<^Const_fn>\<open>zle for t u => \<open>(t, u)\<close>\<close>
val bal_add1 = @{thm le_add_iff1} RS @{thm iff_trans}
val bal_add2 = @{thm le_add_iff2} RS @{thm iff_trans}
);