# HG changeset patch # User wenzelm # Date 1632222858 -7200 # Node ID 5d411d85da8cd87af6e922611e6787e97ae62db0 # Parent edf8b141a8c4ec45561950c551f3e6c1d0658837 clarified antiquotations; diff -r edf8b141a8c4 -r 5d411d85da8c src/FOL/IFOL.thy --- 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} diff -r edf8b141a8c4 -r 5d411d85da8c src/FOL/fologic.ML --- 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>\Trueprop for P\; - -val dest_Trueprop = \<^Const_fn>\Trueprop for P => P\; - fun mk_conj (t1, t2) = \<^Const>\conj for t1 t2\ and mk_disj (t1, t2) = \<^Const>\disj for t1 t2\ and mk_imp (t1, t2) = \<^Const>\imp for t1 t2\ diff -r edf8b141a8c4 -r 5d411d85da8c src/ZF/Tools/datatype_package.ML --- 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), diff -r edf8b141a8c4 -r 5d411d85da8c src/ZF/Tools/ind_cases.ML --- 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 diff -r edf8b141a8c4 -r 5d411d85da8c src/ZF/Tools/induct_tacs.ML --- 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_>\mem for \Free (v,_)\ A\ = (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_>\mem for \Var(ixn,_)\ _\ = (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_>\mem for _ data\ = FOLogic.dest_Trueprop (hd (Thm.prems_of elim)); + val \<^Const_>\mem for _ data\ = \<^dest_judgment> (hd (Thm.prems_of elim)); val Const(big_rec_name, _) = head_of data; diff -r edf8b141a8c4 -r 5d411d85da8c src/ZF/Tools/inductive_package.ML --- 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_>\Trueprop for \\<^Const_>\mem for t X\\\, 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>\Collect\ $ 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>\i\, 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 = " ^ diff -r edf8b141a8c4 -r 5d411d85da8c src/ZF/Tools/primrec_package.ML --- 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); diff -r edf8b141a8c4 -r 5d411d85da8c src/ZF/arith_data.ML --- 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) diff -r edf8b141a8c4 -r 5d411d85da8c src/ZF/ind_syntax.ML --- 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>\mem\ $ list_comb (Const (Sign.full_bname sg name, T), args) $ rec_tm)) + (map \<^make_judgment> prems, + \<^make_judgment> (\<^Const>\mem\ $ 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);