--- a/src/FOL/IFOL.thy Tue Sep 21 13:12:14 2021 +0200
+++ b/src/FOL/IFOL.thy Tue Sep 21 13:14:18 2021 +0200
@@ -527,7 +527,7 @@
structure Hypsubst = Hypsubst
(
val dest_eq = FOLogic.dest_eq
- val dest_Trueprop = FOLogic.dest_Trueprop
+ val dest_Trueprop = \<^dest_judgment>
val dest_imp = FOLogic.dest_imp
val eq_reflection = @{thm eq_reflection}
val rev_eq_reflection = @{thm meta_eq_to_obj_eq}
--- a/src/FOL/fologic.ML Tue Sep 21 13:12:14 2021 +0200
+++ b/src/FOL/fologic.ML Tue Sep 21 13:14:18 2021 +0200
@@ -6,8 +6,6 @@
signature FOLOGIC =
sig
- val mk_Trueprop: term -> term
- val dest_Trueprop: term -> term
val mk_conj: term * term -> term
val mk_disj: term * term -> term
val mk_imp: term * term -> term
@@ -24,10 +22,6 @@
structure FOLogic: FOLOGIC =
struct
-fun mk_Trueprop P = \<^Const>\<open>Trueprop for P\<close>;
-
-val dest_Trueprop = \<^Const_fn>\<open>Trueprop for P => P\<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>
--- a/src/ZF/Tools/datatype_package.ML Tue Sep 21 13:12:14 2021 +0200
+++ b/src/ZF/Tools/datatype_package.ML Tue Sep 21 13:14:18 2021 +0200
@@ -270,7 +270,7 @@
(*Each equation has the form
case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
fun mk_case_eqn (((_,T,_), name, args, _), case_free) =
- FOLogic.mk_Trueprop
+ \<^make_judgment>
(FOLogic.mk_eq
(case_tm $
(list_comb (Const (Sign.intern_const thy1 name,T),
@@ -320,7 +320,7 @@
where REC = recursor(f_con1,...,f_conn) and rec_arg is a recursive
constructor argument.*)
fun mk_recursor_eqn (((_,T,_), name, args, _), recursor_case) =
- FOLogic.mk_Trueprop
+ \<^make_judgment>
(FOLogic.mk_eq
(recursor_tm $
(list_comb (Const (Sign.intern_const thy2 name,T),
--- a/src/ZF/Tools/ind_cases.ML Tue Sep 21 13:12:14 2021 +0200
+++ b/src/ZF/Tools/ind_cases.ML Tue Sep 21 13:14:18 2021 +0200
@@ -33,7 +33,7 @@
fun err msg = cat_error msg ("Malformed set membership statement: " ^ s);
val A = Syntax.read_prop ctxt s handle ERROR msg => err msg;
- val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop
+ val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (\<^dest_judgment>
(Logic.strip_imp_concl A)))))) handle TERM _ => err "";
in
(case Symtab.lookup (IndCasesData.get thy) c of
--- a/src/ZF/Tools/induct_tacs.ML Tue Sep 21 13:12:14 2021 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Tue Sep 21 13:14:18 2021 +0200
@@ -72,7 +72,7 @@
fun find_tname ctxt var As =
let fun mk_pair \<^Const_>\<open>mem for \<open>Free (v,_)\<close> A\<close> = (v, #1 (dest_Const (head_of A)))
| mk_pair _ = raise Match
- val pairs = map_filter (try (mk_pair o FOLogic.dest_Trueprop)) As
+ val pairs = map_filter (try (mk_pair o \<^dest_judgment>)) As
val x =
(case try (dest_Free o Syntax.read_term ctxt) var of
SOME (x, _) => x
@@ -101,7 +101,7 @@
val \<^Const_>\<open>mem for \<open>Var(ixn,_)\<close> _\<close> =
(case Thm.prems_of rule of
[] => error "induction is not available for this datatype"
- | major::_ => FOLogic.dest_Trueprop major)
+ | major::_ => \<^dest_judgment> major)
in
Rule_Insts.eres_inst_tac ctxt [((ixn, Position.none), var)] fixes rule i
end
@@ -124,9 +124,9 @@
Syntax.string_of_term_global thy eqn);
val constructors =
- map (head_of o const_of o FOLogic.dest_Trueprop o Thm.prop_of) case_eqns;
+ map (head_of o const_of o \<^dest_judgment> o Thm.prop_of) case_eqns;
- val \<^Const_>\<open>mem for _ data\<close> = FOLogic.dest_Trueprop (hd (Thm.prems_of elim));
+ val \<^Const_>\<open>mem for _ data\<close> = \<^dest_judgment> (hd (Thm.prems_of elim));
val Const(big_rec_name, _) = head_of data;
--- a/src/ZF/Tools/inductive_package.ML Tue Sep 21 13:12:14 2021 +0200
+++ b/src/ZF/Tools/inductive_package.ML Tue Sep 21 13:14:18 2021 +0200
@@ -185,7 +185,7 @@
val dummy = writeln " Proving monotonicity...";
val bnd_mono0 =
- Goal.prove_global thy1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))
+ Goal.prove_global thy1 [] [] (\<^make_judgment> (Fp.bnd_mono $ dom_sum $ fp_abs))
(fn {context = ctxt, ...} => EVERY
[resolve_tac ctxt [@{thm Collect_subset} RS @{thm bnd_monoI}] 1,
REPEAT (ares_tac ctxt (@{thms basic_monos} @ monos) 1)]);
@@ -300,7 +300,7 @@
prem is a premise of an intr rule*)
fun add_induct_prem ind_alist (prem as \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for t X\<close>\<close>\<close>, iprems) =
(case AList.lookup (op aconv) ind_alist X of
- SOME pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
+ SOME pred => prem :: \<^make_judgment> (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)
@@ -314,7 +314,7 @@
(Logic.strip_imp_prems intr)
val (t,X) = Ind_Syntax.rule_concl intr
val (SOME pred) = AList.lookup (op aconv) ind_alist X
- val concl = FOLogic.mk_Trueprop (pred $ t)
+ val concl = \<^make_judgment> (pred $ t)
in fold_rev Logic.all xs (Logic.list_implies (iprems,concl)) end
handle Bind => error"Recursion term not found in conclusion";
@@ -349,7 +349,7 @@
val quant_induct =
Goal.prove_global thy4 [] ind_prems
- (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
+ (\<^make_judgment> (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
(fn {context = ctxt, prems} => EVERY
[rewrite_goals_tac ctxt part_rec_defs,
resolve_tac ctxt [@{thm impI} RS @{thm allI}] 1,
@@ -404,14 +404,14 @@
(*To instantiate the main induction rule*)
val induct_concl =
- FOLogic.mk_Trueprop
+ \<^make_judgment>
(Ind_Syntax.mk_all_imp
(big_rec_tm,
Abs("z", \<^Type>\<open>i\<close>,
Balanced_Tree.make FOLogic.mk_conj
(ListPair.map mk_rec_imp (rec_tms, preds)))))
and mutual_induct_concl =
- FOLogic.mk_Trueprop (Balanced_Tree.make FOLogic.mk_conj qconcls);
+ \<^make_judgment> (Balanced_Tree.make FOLogic.mk_conj qconcls);
val dummy = if !Ind_Syntax.trace then
(writeln ("induct_concl = " ^
--- a/src/ZF/Tools/primrec_package.ML Tue Sep 21 13:12:14 2021 +0200
+++ b/src/ZF/Tools/primrec_package.ML Tue Sep 21 13:14:18 2021 +0200
@@ -18,7 +18,7 @@
exception RecError of string;
(*Remove outer Trueprop and equality sign*)
-val dest_eqn = FOLogic.dest_eq o FOLogic.dest_Trueprop;
+val dest_eqn = FOLogic.dest_eq o \<^dest_judgment>;
fun primrec_err s = error ("Primrec definition error:\n" ^ s);
--- a/src/ZF/arith_data.ML Tue Sep 21 13:12:14 2021 +0200
+++ b/src/ZF/arith_data.ML Tue Sep 21 13:14:18 2021 +0200
@@ -53,15 +53,13 @@
(*We remove equality assumptions because they confuse the simplifier and
because only type-checking assumptions are necessary.*)
-fun is_eq_thm th =
- can FOLogic.dest_eq (FOLogic.dest_Trueprop (Thm.prop_of th));
+fun is_eq_thm th = can FOLogic.dest_eq (\<^dest_judgment> (Thm.prop_of th));
fun prove_conv name tacs ctxt prems (t,u) =
if t aconv u then NONE
else
let val prems' = filter_out is_eq_thm prems
- val goal = Logic.list_implies (map Thm.prop_of prems',
- FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
+ val goal = Logic.list_implies (map Thm.prop_of prems', \<^make_judgment> (mk_eq_iff (t, u)));
in SOME (prems' MRS Goal.prove ctxt [] [] goal (K (EVERY tacs)))
handle ERROR msg =>
(warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE)
--- a/src/ZF/ind_syntax.ML Tue Sep 21 13:12:14 2021 +0200
+++ b/src/ZF/ind_syntax.ML Tue Sep 21 13:14:18 2021 +0200
@@ -79,9 +79,8 @@
let
fun mk_intr ((id,T,syn), name, args, prems) =
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))
+ (map \<^make_judgment> prems,
+ \<^make_judgment> (\<^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);