--- a/src/CTT/CTT.thy Sat Mar 22 08:37:43 2014 +0100
+++ b/src/CTT/CTT.thy Sat Mar 22 22:00:26 2014 +0100
@@ -328,9 +328,9 @@
local
-fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not(is_Var (head_of a))
- | is_rigid_elem (Const("CTT.Eqelem",_) $ a $ _ $ _) = not(is_Var (head_of a))
- | is_rigid_elem (Const("CTT.Type",_) $ a) = not(is_Var (head_of a))
+fun is_rigid_elem (Const(@{const_name Elem},_) $ a $ _) = not(is_Var (head_of a))
+ | is_rigid_elem (Const(@{const_name Eqelem},_) $ a $ _ $ _) = not(is_Var (head_of a))
+ | is_rigid_elem (Const(@{const_name Type},_) $ a) = not(is_Var (head_of a))
| is_rigid_elem _ = false
in
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Mar 22 22:00:26 2014 +0100
@@ -404,7 +404,7 @@
: (Domain_Take_Proofs.iso_info list
* Domain_Take_Proofs.take_induct_info) * theory =
let
- val _ = Theory.requires thy "Domain" "domain isomorphisms"
+ val _ = Theory.requires thy (Context.theory_name @{theory}) "domain isomorphisms"
(* this theory is used just for parsing *)
val tmp_thy = thy |>
--- a/src/HOL/HOLCF/Tools/cpodef.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Sat Mar 22 22:00:26 2014 +0100
@@ -140,7 +140,7 @@
fun prepare prep_term name (tname, raw_args, _) raw_set opt_morphs thy =
let
- val _ = Theory.requires thy "Cpodef" "cpodefs"
+ val _ = Theory.requires thy (Context.theory_name @{theory}) "cpodefs"
(*rhs*)
val tmp_ctxt =
--- a/src/HOL/HOLCF/Tools/domaindef.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/HOLCF/Tools/domaindef.ML Sat Mar 22 22:00:26 2014 +0100
@@ -84,7 +84,7 @@
(thy: theory)
: (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory =
let
- val _ = Theory.requires thy "Domain" "domaindefs"
+ val _ = Theory.requires thy (Context.theory_name @{theory}) "domaindefs"
(*rhs*)
val tmp_ctxt =
--- a/src/HOL/Import/import_rule.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Import/import_rule.ML Sat Mar 22 22:00:26 2014 +0100
@@ -409,7 +409,7 @@
end
| process (thy, state) (#"Y", [name, _, _]) = setth (mtydef name thy) (thy, state)
| process (thy, state) (#"t", [n]) =
- setty (ctyp_of thy (TFree ("'" ^ (transl_qm n), ["HOL.type"]))) (thy, state)
+ setty (ctyp_of thy (TFree ("'" ^ (transl_qm n), @{sort type}))) (thy, state)
| process (thy, state) (#"a", n :: l) =
fold_map getty l (thy, state) |>>
(fn tys => ctyp_of thy (Type (gettyname n thy, map typ_of tys))) |-> setty
--- a/src/HOL/Library/bnf_decl.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Library/bnf_decl.ML Sat Mar 22 22:00:26 2014 +0100
@@ -94,7 +94,7 @@
val bnf_decl = prepare_decl (K I) (K I);
-fun read_constraint _ NONE = HOLogic.typeS
+fun read_constraint _ NONE = @{sort type}
| read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
val bnf_decl_cmd = prepare_decl read_constraint Syntax.read_typ;
--- a/src/HOL/Library/refute.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Library/refute.ML Sat Mar 22 22:00:26 2014 +0100
@@ -4,11 +4,6 @@
Finite model generation for HOL formulas, using a SAT solver.
*)
-(* ------------------------------------------------------------------------- *)
-(* Declares the 'REFUTE' signature as well as a structure 'Refute'. *)
-(* Documentation is available in the Isabelle/Isar theory 'HOL/Refute.thy'. *)
-(* ------------------------------------------------------------------------- *)
-
signature REFUTE =
sig
@@ -579,7 +574,7 @@
Type ("fun", [@{typ nat}, @{typ nat}])])) => t
| Const (@{const_name Groups.times}, Type ("fun", [@{typ nat},
Type ("fun", [@{typ nat}, @{typ nat}])])) => t
- | Const (@{const_name List.append}, _) => t
+ | Const (@{const_name append}, _) => t
(* UNSOUND
| Const (@{const_name lfp}, _) => t
| Const (@{const_name gfp}, _) => t
@@ -638,6 +633,16 @@
(* To avoid collecting the same axiom multiple times, we use an *)
(* accumulator 'axs' which contains all axioms collected so far. *)
+local
+
+fun get_axiom thy xname =
+ Name_Space.check (Context.Theory thy) (Theory.axiom_table thy) (xname, Position.none);
+
+val the_eq_trivial = get_axiom @{theory HOL} "the_eq_trivial";
+val someI = get_axiom @{theory Hilbert_Choice} "someI";
+
+in
+
fun collect_axioms ctxt t =
let
val thy = Proof_Context.theory_of ctxt
@@ -684,11 +689,11 @@
and collect_type_axioms T axs =
case T of
(* simple types *)
- Type ("prop", []) => axs
- | Type ("fun", [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs)
+ Type (@{type_name prop}, []) => axs
+ | Type (@{type_name fun}, [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs)
| Type (@{type_name set}, [T1]) => collect_type_axioms T1 axs
(* axiomatic type classes *)
- | Type ("itself", [T1]) => collect_type_axioms T1 axs
+ | Type (@{type_name itself}, [T1]) => collect_type_axioms T1 axs
| Type (s, Ts) =>
(case Datatype.get_info thy s of
SOME _ => (* inductive datatype *)
@@ -724,17 +729,15 @@
| Const (@{const_name undefined}, T) => collect_type_axioms T axs
| Const (@{const_name The}, T) =>
let
- val ax = specialize_type thy (@{const_name The}, T)
- (the (AList.lookup (op =) axioms "HOL.the_eq_trivial"))
+ val ax = specialize_type thy (@{const_name The}, T) (#2 the_eq_trivial)
in
- collect_this_axiom ("HOL.the_eq_trivial", ax) axs
+ collect_this_axiom (#1 the_eq_trivial, ax) axs
end
| Const (@{const_name Hilbert_Choice.Eps}, T) =>
let
- val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T)
- (the (AList.lookup (op =) axioms "Hilbert_Choice.someI"))
+ val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T) (#2 someI)
in
- collect_this_axiom ("Hilbert_Choice.someI", ax) axs
+ collect_this_axiom (#1 someI, ax) axs
end
| Const (@{const_name All}, T) => collect_type_axioms T axs
| Const (@{const_name Ex}, T) => collect_type_axioms T axs
@@ -761,7 +764,7 @@
| Const (@{const_name Groups.times}, T as Type ("fun", [@{typ nat},
Type ("fun", [@{typ nat}, @{typ nat}])])) =>
collect_type_axioms T axs
- | Const (@{const_name List.append}, T) => collect_type_axioms T axs
+ | Const (@{const_name append}, T) => collect_type_axioms T axs
(* UNSOUND
| Const (@{const_name lfp}, T) => collect_type_axioms T axs
| Const (@{const_name gfp}, T) => collect_type_axioms T axs
@@ -806,6 +809,8 @@
result
end;
+end;
+
(* ------------------------------------------------------------------------- *)
(* ground_types: collects all ground types in a term (including argument *)
(* types of other types), suppressing duplicates. Does not *)
@@ -819,8 +824,8 @@
val thy = Proof_Context.theory_of ctxt
fun collect_types T acc =
(case T of
- Type ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc)
- | Type ("prop", []) => acc
+ Type (@{type_name fun}, [T1, T2]) => collect_types T1 (collect_types T2 acc)
+ | Type (@{type_name prop}, []) => acc
| Type (@{type_name set}, [T1]) => collect_types T1 acc
| Type (s, Ts) =>
(case Datatype.get_info thy s of
@@ -2620,11 +2625,12 @@
fun List_append_interpreter ctxt model args t =
case t of
- Const (@{const_name List.append}, Type ("fun", [Type ("List.list", [T]), Type ("fun",
- [Type ("List.list", [_]), Type ("List.list", [_])])])) =>
+ Const (@{const_name append},
+ Type (@{type_name fun}, [Type (@{type_name list}, [T]),
+ Type (@{type_name fun}, [Type (@{type_name list}, [_]), Type (@{type_name list}, [_])])])) =>
let
val size_elem = size_of_type ctxt model T
- val size_list = size_of_type ctxt model (Type ("List.list", [T]))
+ val size_list = size_of_type ctxt model (Type (@{type_name list}, [T]))
(* maximal length of lists; 0 if we only consider the empty list *)
val list_length =
let
@@ -2866,7 +2872,7 @@
in
SOME (fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) pairs HOLogic_empty_set)
end
- | Type ("prop", []) =>
+ | Type (@{type_name prop}, []) =>
(case index_from_interpretation intr of
~1 => SOME (HOLogic.mk_Trueprop (Const (@{const_name undefined}, HOLogic.boolT)))
| 0 => SOME (HOLogic.mk_Trueprop @{term True})
@@ -3031,7 +3037,7 @@
(* applied before the 'stlc_interpreter' breaks the term apart into *)
(* subterms that are then passed to other interpreters! *)
(* ------------------------------------------------------------------------- *)
-
+(* FIXME formal @{const_name} for some entries (!??) *)
val setup =
add_interpreter "stlc" stlc_interpreter #>
add_interpreter "Pure" Pure_interpreter #>
--- a/src/HOL/Library/simps_case_conv.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Library/simps_case_conv.ML Sat Mar 22 22:00:26 2014 +0100
@@ -152,13 +152,12 @@
fun was_split t =
let
- val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq
- o fst o HOLogic.dest_imp
+ val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq o fst o HOLogic.dest_imp
val get_conjs = HOLogic.dest_conj o HOLogic.dest_Trueprop
- fun dest_alls (Const ("HOL.All", _) $ Abs (_, _, t)) = dest_alls t
+ fun dest_alls (Const (@{const_name All}, _) $ Abs (_, _, t)) = dest_alls t
| dest_alls t = t
in forall (is_free_eq_imp o dest_alls) (get_conjs t) end
- handle TERM _ => false
+ handle TERM _ => false
fun apply_split ctxt split thm = Seq.of_list
let val ((_,thm'), ctxt') = Variable.import false [thm] ctxt in
--- a/src/HOL/Matrix_LP/ComputeFloat.thy Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy Sat Mar 22 22:00:26 2014 +0100
@@ -239,6 +239,6 @@
lemmas arith = arith_simps rel_simps diff_nat_numeral nat_0
nat_neg_numeral powerarith floatarith not_false_eq_true not_true_eq_false
-ML_file "~~/src/HOL/Tools/float_arith.ML"
+ML_file "float_arith.ML"
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix_LP/float_arith.ML Sat Mar 22 22:00:26 2014 +0100
@@ -0,0 +1,221 @@
+(* Title: HOL/Matrix_LP/float_arith.ML
+ Author: Steven Obua
+*)
+
+signature FLOAT_ARITH =
+sig
+ exception Destruct_floatstr of string
+ val destruct_floatstr: (char -> bool) -> (char -> bool) -> string -> bool * string * string * bool * string
+
+ exception Floating_point of string
+ val approx_dec_by_bin: int -> Float.float -> Float.float * Float.float
+ val approx_decstr_by_bin: int -> string -> Float.float * Float.float
+
+ val mk_float: Float.float -> term
+ val dest_float: term -> Float.float
+
+ val approx_float: int -> (Float.float * Float.float -> Float.float * Float.float)
+ -> string -> term * term
+end;
+
+structure FloatArith : FLOAT_ARITH =
+struct
+
+exception Destruct_floatstr of string;
+
+fun destruct_floatstr isDigit isExp number =
+ let
+ val numlist = filter (not o Char.isSpace) (String.explode number)
+
+ fun countsigns ((#"+")::cs) = countsigns cs
+ | countsigns ((#"-")::cs) =
+ let
+ val (positive, rest) = countsigns cs
+ in
+ (not positive, rest)
+ end
+ | countsigns cs = (true, cs)
+
+ fun readdigits [] = ([], [])
+ | readdigits (q as c::cs) =
+ if (isDigit c) then
+ let
+ val (digits, rest) = readdigits cs
+ in
+ (c::digits, rest)
+ end
+ else
+ ([], q)
+
+ fun readfromexp_helper cs =
+ let
+ val (positive, rest) = countsigns cs
+ val (digits, rest') = readdigits rest
+ in
+ case rest' of
+ [] => (positive, digits)
+ | _ => raise (Destruct_floatstr number)
+ end
+
+ fun readfromexp [] = (true, [])
+ | readfromexp (c::cs) =
+ if isExp c then
+ readfromexp_helper cs
+ else
+ raise (Destruct_floatstr number)
+
+ fun readfromdot [] = ([], readfromexp [])
+ | readfromdot ((#".")::cs) =
+ let
+ val (digits, rest) = readdigits cs
+ val exp = readfromexp rest
+ in
+ (digits, exp)
+ end
+ | readfromdot cs = readfromdot ((#".")::cs)
+
+ val (positive, numlist) = countsigns numlist
+ val (digits1, numlist) = readdigits numlist
+ val (digits2, exp) = readfromdot numlist
+ in
+ (positive, String.implode digits1, String.implode digits2, fst exp, String.implode (snd exp))
+ end
+
+exception Floating_point of string;
+
+val ln2_10 = Math.ln 10.0 / Math.ln 2.0;
+fun exp5 x = Integer.pow x 5;
+fun exp10 x = Integer.pow x 10;
+fun exp2 x = Integer.pow x 2;
+
+fun find_most_significant q r =
+ let
+ fun int2real i =
+ case (Real.fromString o string_of_int) i of
+ SOME r => r
+ | NONE => raise (Floating_point "int2real")
+ fun subtract (q, r) (q', r') =
+ if r <= r' then
+ (q - q' * exp10 (r' - r), r)
+ else
+ (q * exp10 (r - r') - q', r')
+ fun bin2dec d =
+ if 0 <= d then
+ (exp2 d, 0)
+ else
+ (exp5 (~ d), d)
+
+ val L = Real.floor (int2real (IntInf.log2 q) + int2real r * ln2_10)
+ val L1 = L + 1
+
+ val (q1, r1) = subtract (q, r) (bin2dec L1)
+ in
+ if 0 <= q1 then
+ let
+ val (q2, r2) = subtract (q, r) (bin2dec (L1 + 1))
+ in
+ if 0 <= q2 then
+ raise (Floating_point "find_most_significant")
+ else
+ (L1, (q1, r1))
+ end
+ else
+ let
+ val (q0, r0) = subtract (q, r) (bin2dec L)
+ in
+ if 0 <= q0 then
+ (L, (q0, r0))
+ else
+ raise (Floating_point "find_most_significant")
+ end
+ end
+
+fun approx_dec_by_bin n (q,r) =
+ let
+ fun addseq acc d' [] = acc
+ | addseq acc d' (d::ds) = addseq (acc + exp2 (d - d')) d' ds
+
+ fun seq2bin [] = (0, 0)
+ | seq2bin (d::ds) = (addseq 0 d ds + 1, d)
+
+ fun approx d_seq d0 precision (q,r) =
+ if q = 0 then
+ let val x = seq2bin d_seq in
+ (x, x)
+ end
+ else
+ let
+ val (d, (q', r')) = find_most_significant q r
+ in
+ if precision < d0 - d then
+ let
+ val d' = d0 - precision
+ val x1 = seq2bin (d_seq)
+ val x2 = (fst x1 * exp2 (snd x1 - d') + 1, d') (* = seq2bin (d'::d_seq) *)
+ in
+ (x1, x2)
+ end
+ else
+ approx (d::d_seq) d0 precision (q', r')
+ end
+
+ fun approx_start precision (q, r) =
+ if q = 0 then
+ ((0, 0), (0, 0))
+ else
+ let
+ val (d, (q', r')) = find_most_significant q r
+ in
+ if precision <= 0 then
+ let
+ val x1 = seq2bin [d]
+ in
+ if q' = 0 then
+ (x1, x1)
+ else
+ (x1, seq2bin [d + 1])
+ end
+ else
+ approx [d] d precision (q', r')
+ end
+ in
+ if 0 <= q then
+ approx_start n (q,r)
+ else
+ let
+ val ((a1,b1), (a2, b2)) = approx_start n (~ q, r)
+ in
+ ((~ a2, b2), (~ a1, b1))
+ end
+ end
+
+fun approx_decstr_by_bin n decstr =
+ let
+ fun str2int s = the_default 0 (Int.fromString s)
+ fun signint p x = if p then x else ~ x
+
+ val (p, d1, d2, ep, e) = destruct_floatstr Char.isDigit (fn e => e = #"e" orelse e = #"E") decstr
+ val s = size d2
+
+ val q = signint p (str2int d1 * exp10 s + str2int d2)
+ val r = signint ep (str2int e) - s
+ in
+ approx_dec_by_bin n (q,r)
+ end
+
+fun mk_float (a, b) = @{term "float"} $
+ HOLogic.mk_prod (pairself (HOLogic.mk_number HOLogic.intT) (a, b));
+
+fun dest_float (Const (@{const_name float}, _) $ (Const (@{const_name Pair}, _) $ a $ b)) =
+ pairself (snd o HOLogic.dest_number) (a, b)
+ | dest_float t = ((snd o HOLogic.dest_number) t, 0);
+
+fun approx_float prec f value =
+ let
+ val interval = approx_decstr_by_bin prec value
+ val (flower, fupper) = f interval
+ in
+ (mk_float flower, mk_float fupper)
+ end;
+
+end;
--- a/src/HOL/NSA/StarDef.thy Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/NSA/StarDef.thy Sat Mar 22 22:00:26 2014 +0100
@@ -172,7 +172,7 @@
"Standard = range star_of"
text {* Transfer tactic should remove occurrences of @{term star_of} *}
-setup {* Transfer_Principle.add_const "StarDef.star_of" *}
+setup {* Transfer_Principle.add_const @{const_name star_of} *}
declare star_of_def [transfer_intro]
@@ -199,7 +199,7 @@
UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2])
text {* Transfer tactic should remove occurrences of @{term Ifun} *}
-setup {* Transfer_Principle.add_const "StarDef.Ifun" *}
+setup {* Transfer_Principle.add_const @{const_name Ifun} *}
lemma transfer_Ifun [transfer_intro]:
"\<lbrakk>f \<equiv> star_n F; x \<equiv> star_n X\<rbrakk> \<Longrightarrow> f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))"
@@ -306,7 +306,7 @@
by (simp add: unstar_def star_of_inject)
text {* Transfer tactic should remove occurrences of @{term unstar} *}
-setup {* Transfer_Principle.add_const "StarDef.unstar" *}
+setup {* Transfer_Principle.add_const @{const_name unstar} *}
lemma transfer_unstar [transfer_intro]:
"p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
@@ -348,7 +348,7 @@
by (simp add: Iset_def starP2_star_n)
text {* Transfer tactic should remove occurrences of @{term Iset} *}
-setup {* Transfer_Principle.add_const "StarDef.Iset" *}
+setup {* Transfer_Principle.add_const @{const_name Iset} *}
lemma transfer_mem [transfer_intro]:
"\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
--- a/src/HOL/NSA/transfer.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/NSA/transfer.ML Sat Mar 22 22:00:26 2014 +0100
@@ -35,7 +35,7 @@
consts = Library.merge (op =) (consts1, consts2)};
);
-fun unstar_typ (Type ("StarDef.star",[t])) = unstar_typ t
+fun unstar_typ (Type (@{type_name star}, [t])) = unstar_typ t
| unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts)
| unstar_typ T = T
--- a/src/HOL/Nominal/nominal_atoms.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Sat Mar 22 22:00:26 2014 +0100
@@ -86,7 +86,7 @@
fun mk_Cons x xs =
let val T = fastype_of x
- in Const ("List.list.Cons", T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end;
+ in Const (@{const_name Cons}, T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end;
fun add_thms_string args = Global_Theory.add_thms ((map o apfst o apfst) Binding.name args);
fun add_thmss_string args = Global_Theory.add_thmss ((map o apfst o apfst) Binding.name args);
@@ -142,7 +142,7 @@
val stmnt3 = HOLogic.mk_Trueprop
(HOLogic.mk_not
- (Const ("Finite_Set.finite", HOLogic.mk_setT ak_type --> HOLogic.boolT) $
+ (Const (@{const_name finite}, HOLogic.mk_setT ak_type --> HOLogic.boolT) $
HOLogic.mk_UNIV ak_type))
val simp2 = [@{thm image_def},@{thm bex_UNIV}]@inject_thm
@@ -179,9 +179,9 @@
val b = Free ("b", T);
val c = Free ("c", T);
val ab = Free ("ab", HOLogic.mk_prodT (T, T))
- val cif = Const ("HOL.If", HOLogic.boolT --> T --> T --> T);
+ val cif = Const (@{const_name If}, HOLogic.boolT --> T --> T --> T);
val cswap_akname = Const (full_swap_name, swapT);
- val cswap = Const ("Nominal.swap", swapT)
+ val cswap = Const (@{const_name Nominal.swap}, swapT)
val name = swap_name ^ "_def";
val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -215,7 +215,7 @@
val xs = Free ("xs", mk_permT T);
val a = Free ("a", T) ;
- val cnil = Const ("List.list.Nil", mk_permT T);
+ val cnil = Const (@{const_name Nil}, mk_permT T);
val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq (prm $ cnil $ a, a));
@@ -245,7 +245,7 @@
val perm_def_name = ak_name ^ "_prm_" ^ ak_name';
val pi = Free ("pi", mk_permT T);
val a = Free ("a", T');
- val cperm = Const ("Nominal.perm", mk_permT T --> T' --> T');
+ val cperm = Const (@{const_name Nominal.perm}, mk_permT T --> T' --> T');
val thy'' = Sign.add_path "rec" thy'
val cperm_def = Const (Sign.full_bname thy'' perm_def_name, mk_permT T --> T' --> T');
val thy''' = Sign.parent_path thy'';
@@ -265,7 +265,7 @@
let
val ak_name_qu = Sign.full_bname thy5 (ak_name);
val i_type = Type(ak_name_qu,[]);
- val cat = Const ("Nominal.at",(Term.itselfT i_type) --> HOLogic.boolT);
+ val cat = Const (@{const_name Nominal.at}, Term.itselfT i_type --> HOLogic.boolT);
val at_type = Logic.mk_type i_type;
fun proof ctxt =
simp_tac (put_simpset HOL_ss ctxt
@@ -290,14 +290,14 @@
val (pt_ax_classes,thy7) = fold_map (fn (ak_name, T) => fn thy =>
let
val cl_name = "pt_"^ak_name;
- val ty = TFree("'a",["HOL.type"]);
+ val ty = TFree("'a", @{sort type});
val x = Free ("x", ty);
val pi1 = Free ("pi1", mk_permT T);
val pi2 = Free ("pi2", mk_permT T);
- val cperm = Const ("Nominal.perm", mk_permT T --> ty --> ty);
- val cnil = Const ("List.list.Nil", mk_permT T);
- val cappend = Const ("List.append",mk_permT T --> mk_permT T --> mk_permT T);
- val cprm_eq = Const ("Nominal.prm_eq",mk_permT T --> mk_permT T --> HOLogic.boolT);
+ val cperm = Const (@{const_name Nominal.perm}, mk_permT T --> ty --> ty);
+ val cnil = Const (@{const_name Nil}, mk_permT T);
+ val cappend = Const (@{const_name append}, mk_permT T --> mk_permT T --> mk_permT T);
+ val cprm_eq = Const (@{const_name Nominal.prm_eq}, mk_permT T --> mk_permT T --> HOLogic.boolT);
(* nil axiom *)
val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_eq
(cperm $ cnil $ x, x));
@@ -309,7 +309,7 @@
(HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
in
- Axclass.define_class (Binding.name cl_name, ["HOL.type"]) []
+ Axclass.define_class (Binding.name cl_name, @{sort type}) []
[((Binding.name (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
((Binding.name (cl_name ^ "2"), []), [axiom2]),
((Binding.name (cl_name ^ "3"), []), [axiom3])] thy
@@ -326,7 +326,8 @@
val pt_name_qu = Sign.full_bname thy7 ("pt_"^ak_name);
val i_type1 = TFree("'x",[pt_name_qu]);
val i_type2 = Type(ak_name_qu,[]);
- val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
+ val cpt =
+ Const (@{const_name Nominal.pt}, (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
val pt_type = Logic.mk_type i_type1;
val at_type = Logic.mk_type i_type2;
fun proof ctxt =
@@ -349,10 +350,10 @@
let
val cl_name = "fs_"^ak_name;
val pt_name = Sign.full_bname thy ("pt_"^ak_name);
- val ty = TFree("'a",["HOL.type"]);
+ val ty = TFree("'a",@{sort type});
val x = Free ("x", ty);
- val csupp = Const ("Nominal.supp", ty --> HOLogic.mk_setT T);
- val cfinite = Const ("Finite_Set.finite", HOLogic.mk_setT T --> HOLogic.boolT)
+ val csupp = Const (@{const_name Nominal.supp}, ty --> HOLogic.mk_setT T);
+ val cfinite = Const (@{const_name finite}, HOLogic.mk_setT T --> HOLogic.boolT)
val axiom1 = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
@@ -372,7 +373,7 @@
val fs_name_qu = Sign.full_bname thy11 ("fs_"^ak_name);
val i_type1 = TFree("'x",[fs_name_qu]);
val i_type2 = Type(ak_name_qu,[]);
- val cfs = Const ("Nominal.fs",
+ val cfs = Const (@{const_name Nominal.fs},
(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
val fs_type = Logic.mk_type i_type1;
val at_type = Logic.mk_type i_type2;
@@ -394,19 +395,19 @@
fold_map (fn (ak_name', T') => fn thy' =>
let
val cl_name = "cp_"^ak_name^"_"^ak_name';
- val ty = TFree("'a",["HOL.type"]);
+ val ty = TFree("'a",@{sort type});
val x = Free ("x", ty);
val pi1 = Free ("pi1", mk_permT T);
val pi2 = Free ("pi2", mk_permT T');
- val cperm1 = Const ("Nominal.perm", mk_permT T --> ty --> ty);
- val cperm2 = Const ("Nominal.perm", mk_permT T' --> ty --> ty);
- val cperm3 = Const ("Nominal.perm", mk_permT T --> mk_permT T' --> mk_permT T');
+ val cperm1 = Const (@{const_name Nominal.perm}, mk_permT T --> ty --> ty);
+ val cperm2 = Const (@{const_name Nominal.perm}, mk_permT T' --> ty --> ty);
+ val cperm3 = Const (@{const_name Nominal.perm}, mk_permT T --> mk_permT T' --> mk_permT T');
val ax1 = HOLogic.mk_Trueprop
(HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x),
cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
in
- Axclass.define_class (Binding.name cl_name, ["HOL.type"]) []
+ Axclass.define_class (Binding.name cl_name, @{sort type}) []
[((Binding.name (cl_name ^ "1"), []), [ax1])] thy'
end) ak_names_types thy) ak_names_types thy12;
@@ -422,7 +423,7 @@
val i_type0 = TFree("'a",[cp_name_qu]);
val i_type1 = Type(ak_name_qu,[]);
val i_type2 = Type(ak_name_qu',[]);
- val ccp = Const ("Nominal.cp",
+ val ccp = Const (@{const_name Nominal.cp},
(Term.itselfT i_type0)-->(Term.itselfT i_type1)-->
(Term.itselfT i_type2)-->HOLogic.boolT);
val at_type = Logic.mk_type i_type1;
@@ -456,7 +457,7 @@
val ak_name_qu' = Sign.full_bname thy' ak_name';
val i_type1 = Type(ak_name_qu,[]);
val i_type2 = Type(ak_name_qu',[]);
- val cdj = Const ("Nominal.disjoint",
+ val cdj = Const (@{const_name Nominal.disjoint},
(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
val at_type = Logic.mk_type i_type1;
val at_type' = Logic.mk_type i_type2;
@@ -548,15 +549,14 @@
val pt_thm_unit = pt_unit_inst;
in
thy
- |> Axclass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
- |> Axclass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
- |> Axclass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn)
- |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
- |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
- |> Axclass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
- |> Axclass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name])
- (pt_proof pt_thm_nprod)
- |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
+ |> Axclass.prove_arity (@{type_name fun},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
+ |> Axclass.prove_arity (@{type_name set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
+ |> Axclass.prove_arity (@{type_name noption},[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn)
+ |> Axclass.prove_arity (@{type_name option},[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
+ |> Axclass.prove_arity (@{type_name list},[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
+ |> Axclass.prove_arity (@{type_name prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
+ |> Axclass.prove_arity (@{type_name nprod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_nprod)
+ |> Axclass.prove_arity (@{type_name unit},[],[cls_name]) (pt_proof pt_thm_unit)
end) ak_names thy13;
(******** fs_<ak> class instances ********)
@@ -614,12 +614,11 @@
val fs_thm_optn = fs_inst RS fs_option_inst;
in
thy
- |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit)
- |> Axclass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod)
- |> Axclass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name])
- (fs_proof fs_thm_nprod)
- |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
- |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
+ |> Axclass.prove_arity (@{type_name unit},[],[cls_name]) (fs_proof fs_thm_unit)
+ |> Axclass.prove_arity (@{type_name prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod)
+ |> Axclass.prove_arity (@{type_name nprod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_nprod)
+ |> Axclass.prove_arity (@{type_name list},[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
+ |> Axclass.prove_arity (@{type_name option},[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
end) ak_names thy20;
(******** cp_<ak>_<ai> class instances ********)
@@ -698,13 +697,13 @@
val cp_thm_set = cp_inst RS cp_set_inst;
in
thy'
- |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
+ |> Axclass.prove_arity (@{type_name unit},[],[cls_name]) (cp_proof cp_thm_unit)
|> Axclass.prove_arity (@{type_name Product_Type.prod}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
- |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
- |> Axclass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
- |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
- |> Axclass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
- |> Axclass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
+ |> Axclass.prove_arity (@{type_name list},[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
+ |> Axclass.prove_arity (@{type_name fun},[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
+ |> Axclass.prove_arity (@{type_name option},[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
+ |> Axclass.prove_arity (@{type_name noption},[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
+ |> Axclass.prove_arity (@{type_name set},[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
end) ak_names thy) ak_names thy25;
(* show that discrete nominal types are permutation types, finitely *)
--- a/src/HOL/Nominal/nominal_datatype.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Sat Mar 22 22:00:26 2014 +0100
@@ -90,13 +90,14 @@
val dj_cp = @{thm dj_cp};
-fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [T, _])]),
- Type ("fun", [_, U])])) = (T, U);
+fun dest_permT (Type (@{type_name fun},
+ [Type (@{type_name list}, [Type (@{type_name Product_Type.prod}, [T, _])]),
+ Type (@{type_name fun}, [_, U])])) = (T, U);
-fun permTs_of (Const ("Nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
+fun permTs_of (Const (@{const_name Nominal.perm}, T) $ t $ u) = fst (dest_permT T) :: permTs_of u
| permTs_of _ = [];
-fun perm_simproc' ctxt (Const ("Nominal.perm", T) $ t $ (u as Const ("Nominal.perm", U) $ r $ s)) =
+fun perm_simproc' ctxt (Const (@{const_name Nominal.perm}, T) $ t $ (u as Const (@{const_name Nominal.perm}, U) $ r $ s)) =
let
val thy = Proof_Context.theory_of ctxt;
val (aT as Type (a, []), S) = dest_permT T;
@@ -140,23 +141,23 @@
let
val T = fastype_of1 (Ts, t);
val U = fastype_of1 (Ts, u)
- in Const ("Nominal.perm", T --> U --> U) $ t $ u end;
+ in Const (@{const_name Nominal.perm}, T --> U --> U) $ t $ u end;
fun perm_of_pair (x, y) =
let
val T = fastype_of x;
val pT = mk_permT T
- in Const ("List.list.Cons", HOLogic.mk_prodT (T, T) --> pT --> pT) $
- HOLogic.mk_prod (x, y) $ Const ("List.list.Nil", pT)
+ in Const (@{const_name Cons}, HOLogic.mk_prodT (T, T) --> pT --> pT) $
+ HOLogic.mk_prod (x, y) $ Const (@{const_name Nil}, pT)
end;
fun mk_not_sym ths = maps (fn th => case prop_of th of
_ $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) => [th, th RS not_sym]
| _ => [th]) ths;
-fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
+fun fresh_const T U = Const (@{const_name Nominal.fresh}, T --> U --> HOLogic.boolT);
fun fresh_star_const T U =
- Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT);
+ Const (@{const_name Nominal.fresh_star}, HOLogic.mk_setT T --> U --> HOLogic.boolT);
fun gen_nominal_datatype prep_specs config dts thy =
let
@@ -185,8 +186,8 @@
(Sign.full_name thy n, Sign.full_name thy (Binding.suffix_name "_Rep" n))) dts;
val rps = map Library.swap ps;
- fun replace_types (Type ("Nominal.ABS", [T, U])) =
- Type ("fun", [T, Type ("Nominal.noption", [replace_types U])])
+ fun replace_types (Type (@{type_name ABS}, [T, U])) =
+ Type (@{type_name fun}, [T, Type (@{type_name noption}, [replace_types U])])
| replace_types (Type (s, Ts)) =
Type (the_default s (AList.lookup op = ps s), map replace_types Ts)
| replace_types T = T;
@@ -208,14 +209,14 @@
(**** define permutation functions ****)
- val permT = mk_permT (TFree ("'x", HOLogic.typeS));
+ val permT = mk_permT (TFree ("'x", @{sort type}));
val pi = Free ("pi", permT);
val perm_types = map (fn (i, _) =>
let val T = nth_dtyp i
in permT --> T --> T end) descr;
val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) =>
"perm_" ^ Datatype_Aux.name_of_typ (nth_dtyp i)) descr);
- val perm_names = replicate (length new_type_names) "Nominal.perm" @
+ val perm_names = replicate (length new_type_names) @{const_name Nominal.perm} @
map (Sign.full_bname thy1) (List.drop (perm_names', length new_type_names));
val perm_names_types = perm_names ~~ perm_types;
val perm_names_types' = perm_names' ~~ perm_types;
@@ -236,16 +237,16 @@
fold_rev (Term.abs o pair "x") Us
(Free (nth perm_names_types' (Datatype_Aux.body_index dt)) $ pi $
list_comb (x, map (fn (i, U) =>
- Const ("Nominal.perm", permT --> U --> U) $
- (Const ("List.rev", permT --> permT) $ pi) $
+ Const (@{const_name Nominal.perm}, permT --> U --> U) $
+ (Const (@{const_name rev}, permT --> permT) $ pi) $
Bound i) ((length Us - 1 downto 0) ~~ Us)))
end
- else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
+ else Const (@{const_name Nominal.perm}, permT --> T --> T) $ pi $ x
end;
in
(Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
(Free (nth perm_names_types' i) $
- Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
+ Free ("pi", mk_permT (TFree ("'x", @{sort type}))) $
list_comb (c, args),
list_comb (c, map perm_arg (dts ~~ args)))))
end) constrs
@@ -274,7 +275,7 @@
(map (fn (c as (s, T), x) =>
let val [T1, T2] = binder_types T
in HOLogic.mk_eq (Const c $ pi $ Free (x, T2),
- Const ("Nominal.perm", T) $ pi $ Free (x, T2))
+ Const (@{const_name Nominal.perm}, T) $ pi $ Free (x, T2))
end)
(perm_names_types ~~ perm_indnames))))
(fn {context = ctxt, ...} => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1,
@@ -293,7 +294,7 @@
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
(map (fn ((s, T), x) => HOLogic.mk_eq
(Const (s, permT --> T --> T) $
- Const ("List.list.Nil", permT) $ Free (x, T),
+ Const (@{const_name Nil}, permT) $ Free (x, T),
Free (x, T)))
(perm_names ~~
map body_type perm_types ~~ perm_indnames)))))
@@ -326,7 +327,7 @@
(map (fn ((s, T), x) =>
let val perm = Const (s, permT --> T --> T)
in HOLogic.mk_eq
- (perm $ (Const ("List.append", permT --> permT --> permT) $
+ (perm $ (Const (@{const_name append}, permT --> permT --> permT) $
pi1 $ pi2) $ Free (x, T),
perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
end)
@@ -357,7 +358,7 @@
in List.take (map Drule.export_without_context (Datatype_Aux.split_conj_thm
(Goal.prove_global_future thy2 [] []
(augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
- (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
+ (HOLogic.mk_Trueprop (Const (@{const_name Nominal.prm_eq},
permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
(map (fn ((s, T), x) =>
@@ -414,7 +415,7 @@
val pi2 = Free ("pi2", permT2);
val perm1 = Const (s, permT1 --> T --> T);
val perm2 = Const (s, permT2 --> T --> T);
- val perm3 = Const ("Nominal.perm", permT1 --> permT2 --> permT2)
+ val perm3 = Const (@{const_name Nominal.perm}, permT1 --> permT2 --> permT2)
in HOLogic.mk_eq
(perm1 $ pi1 $ (perm2 $ pi2 $ Free (x, T)),
perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T)))
@@ -462,17 +463,17 @@
(map (fn (i, _) => Datatype_Aux.name_of_typ (nth_dtyp i) ^ "_set") descr);
val big_rep_name =
space_implode "_" (Datatype_Prop.indexify_names (map_filter
- (fn (i, ("Nominal.noption", _, _)) => NONE
+ (fn (i, (@{type_name noption}, _, _)) => NONE
| (i, _) => SOME (Datatype_Aux.name_of_typ (nth_dtyp i))) descr)) ^ "_set";
val _ = warning ("big_rep_name: " ^ big_rep_name);
fun strip_option (dtf as Datatype.DtType ("fun", [dt, Datatype.DtRec i])) =
(case AList.lookup op = descr i of
- SOME ("Nominal.noption", _, [(_, [dt']), _]) =>
+ SOME (@{type_name noption}, _, [(_, [dt']), _]) =>
apfst (cons dt) (strip_option dt')
| _ => ([], dtf))
| strip_option (Datatype.DtType ("fun",
- [dt, Datatype.DtType ("Nominal.noption", [dt'])])) =
+ [dt, Datatype.DtType (@{type_name noption}, [dt'])])) =
apfst (cons dt) (strip_option dt')
| strip_option dt = ([], dt);
@@ -493,8 +494,8 @@
val free' = Datatype_Aux.app_bnds free (length Us);
fun mk_abs_fun T (i, t) =
let val U = fastype_of t
- in (i + 1, Const ("Nominal.abs_fun", [T, U, T] --->
- Type ("Nominal.noption", [U])) $ Datatype_Aux.mk_Free "y" T i $ t)
+ in (i + 1, Const (@{const_name Nominal.abs_fun}, [T, U, T] --->
+ Type (@{type_name noption}, [U])) $ Datatype_Aux.mk_Free "y" T i $ t)
end
in (j + 1, j' + length Ts,
case dt'' of
@@ -513,7 +514,7 @@
val (intr_ts, (rep_set_names', recTs')) =
apfst flat (apsnd ListPair.unzip (ListPair.unzip (map_filter
- (fn ((_, ("Nominal.noption", _, _)), _) => NONE
+ (fn ((_, (@{type_name noption}, _, _)), _) => NONE
| ((i, (_, _, constrs)), rep_set_name) =>
let val T = nth_dtyp i
in SOME (map (make_intr rep_set_name T) constrs,
@@ -540,7 +541,7 @@
val abs_perm = Global_Theory.get_thms thy4 "abs_perm";
val perm_indnames' = map_filter
- (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
+ (fn (x, (_, (@{type_name noption}, _, _))) => NONE | (x, _) => SOME x)
(perm_indnames ~~ descr);
fun mk_perm_closed name = map (fn th => Drule.export_without_context (th RS mp))
@@ -553,7 +554,7 @@
val S = Const (s, T --> HOLogic.boolT);
val permT = mk_permT (Type (name, []))
in HOLogic.mk_imp (S $ Free (x, T),
- S $ (Const ("Nominal.perm", permT --> T --> T) $
+ S $ (Const (@{const_name Nominal.perm}, permT --> T --> T) $
Free ("pi", permT) $ Free (x, T)))
end) (rep_set_names'' ~~ recTs' ~~ perm_indnames')))))
(fn {context = ctxt, ...} => EVERY
@@ -581,15 +582,15 @@
(resolve_tac rep_intrs 1)) thy |> (fn ((_, r), thy) =>
let
val permT = mk_permT
- (TFree (singleton (Name.variant_list (map fst tvs)) "'a", HOLogic.typeS));
+ (TFree (singleton (Name.variant_list (map fst tvs)) "'a", @{sort type}));
val pi = Free ("pi", permT);
val T = Type (Sign.full_name thy name, map TFree tvs);
in apfst (pair r o hd)
(Global_Theory.add_defs_unchecked true
[((Binding.map_name (fn n => "prm_" ^ n ^ "_def") name, Logic.mk_equals
- (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
+ (Const (@{const_name Nominal.perm}, permT --> T --> T) $ pi $ Free ("x", T),
Const (Sign.intern_const thy ("Abs_" ^ Binding.name_of name), U --> T) $
- (Const ("Nominal.perm", permT --> U --> U) $ pi $
+ (Const (@{const_name Nominal.perm}, permT --> U --> U) $ pi $
(Const (Sign.intern_const thy ("Rep_" ^ Binding.name_of name), T --> U) $
Free ("x", T))))), [])] thy)
end))
@@ -671,12 +672,12 @@
val T = fastype_of x;
val U = fastype_of t
in
- Const ("Nominal.abs_fun", T --> U --> T -->
- Type ("Nominal.noption", [U])) $ x $ t
+ Const (@{const_name Nominal.abs_fun}, T --> U --> T -->
+ Type (@{type_name noption}, [U])) $ x $ t
end;
val (ty_idxs, _) = List.foldl
- (fn ((i, ("Nominal.noption", _, _)), p) => p
+ (fn ((i, (@{type_name noption}, _, _)), p) => p
| ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
fun reindex (Datatype.DtType (s, dts)) = Datatype.DtType (s, map reindex dts)
@@ -691,7 +692,7 @@
in Long_Name.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
val (descr'', ndescr) = ListPair.unzip (map_filter
- (fn (i, ("Nominal.noption", _, _)) => NONE
+ (fn (i, (@{type_name noption}, _, _)) => NONE
| (i, (s, dts, constrs)) =>
let
val SOME index = AList.lookup op = ty_idxs i;
@@ -817,8 +818,8 @@
(augment_sort thy8
(pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (remove (op =) atom dt_atoms))
(HOLogic.mk_Trueprop (HOLogic.mk_eq
- (Const ("Nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
- Rep $ (Const ("Nominal.perm", permT --> T --> T) $ pi $ x)))))
+ (Const (@{const_name Nominal.perm}, permT --> U --> U) $ pi $ (Rep $ x),
+ Rep $ (Const (@{const_name Nominal.perm}, permT --> T --> T) $ pi $ x)))))
(fn {context = ctxt, ...} =>
simp_tac (put_simpset HOL_basic_ss ctxt addsimps (perm_defs @ Abs_inverse_thms @
perm_closed_thms @ Rep_thms)) 1)
@@ -860,7 +861,7 @@
fun perm t =
let val T = fastype_of t
- in Const ("Nominal.perm", permT --> T --> T) $ pi $ t end;
+ in Const (@{const_name Nominal.perm}, permT --> T --> T) $ pi $ t end;
fun constr_arg (dts, dt) (j, l_args, r_args) =
let
@@ -977,7 +978,7 @@
val Ts = map fastype_of args1;
val c = list_comb (Const (cname, Ts ---> T), args1);
fun supp t =
- Const ("Nominal.supp", fastype_of t --> HOLogic.mk_setT atomT) $ t;
+ Const (@{const_name Nominal.supp}, fastype_of t --> HOLogic.mk_setT atomT) $ t;
fun fresh t = fresh_const atomT (fastype_of t) $ Free ("a", atomT) $ t;
val supp_thm = Goal.prove_global_future thy8 [] []
(augment_sort thy8 pt_cp_sort
@@ -1070,8 +1071,8 @@
(augment_sort thy8 (fs_class_of thy8 atom :: pt_cp_sort)
(HOLogic.mk_Trueprop
(foldr1 HOLogic.mk_conj (map (fn (s, T) =>
- Const ("Finite_Set.finite", HOLogic.mk_setT atomT --> HOLogic.boolT) $
- (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T)))
+ Const (@{const_name finite}, HOLogic.mk_setT atomT --> HOLogic.boolT) $
+ (Const (@{const_name Nominal.supp}, T --> HOLogic.mk_setT atomT) $ Free (s, T)))
(indnames ~~ recTs)))))
(fn {context = ctxt, ...} => Datatype_Aux.ind_tac dt_induct indnames 1 THEN
ALLGOALS (asm_full_simp_tac (ctxt addsimps
@@ -1112,10 +1113,10 @@
val pnames = if length descr'' = 1 then ["P"]
else map (fn i => "P" ^ string_of_int i) (1 upto length descr'');
- val ind_sort = if null dt_atomTs then HOLogic.typeS
+ val ind_sort = if null dt_atomTs then @{sort type}
else Sign.minimize_sort thy9 (Sign.certify_sort thy9 (map (fs_class_of thy9) dt_atoms));
val fsT = TFree ("'n", ind_sort);
- val fsT' = TFree ("'n", HOLogic.typeS);
+ val fsT' = TFree ("'n", @{sort type});
val fresh_fs = map (fn (s, T) => (T, Free (s, fsT' --> HOLogic.mk_setT T)))
(Datatype_Prop.indexify_names (replicate (length dt_atomTs) "f") ~~ dt_atomTs);
@@ -1183,7 +1184,7 @@
val ind_prems' =
map (fn (_, f as Free (_, T)) => Logic.all (Free ("x", fsT'))
- (HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
+ (HOLogic.mk_Trueprop (Const (@{const_name finite},
Term.range_type T -->
HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
maps (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
@@ -1345,7 +1346,7 @@
cut_facts_tac iprems 1,
(resolve_tac prems THEN_ALL_NEW
SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of
- _ $ (Const ("Nominal.fresh", _) $ _ $ _) =>
+ _ $ (Const (@{const_name Nominal.fresh}, _) $ _ $ _) =>
simp_tac ind_ss1' i
| _ $ (Const (@{const_name Not}, _) $ _) =>
resolve_tac freshs2' i
@@ -1371,7 +1372,7 @@
map (fn (_, f) =>
let val f' = Logic.varify_global f
in (cterm_of thy9 f',
- cterm_of thy9 (Const ("Nominal.supp", fastype_of f')))
+ cterm_of thy9 (Const (@{const_name Nominal.supp}, fastype_of f')))
end) fresh_fs) induct_aux;
val induct = Goal.prove_global_future thy9 []
@@ -1398,7 +1399,7 @@
val (rec_result_Ts', rec_fn_Ts') = Datatype_Prop.make_primrec_Ts descr' used;
- val rec_sort = if null dt_atomTs then HOLogic.typeS else
+ val rec_sort = if null dt_atomTs then @{sort type} else
Sign.minimize_sort thy10 (Sign.certify_sort thy10 pt_cp_sort);
val rec_result_Ts = map (fn TFree (s, _) => TFree (s, rec_sort)) rec_result_Ts';
@@ -1459,8 +1460,8 @@
HOLogic.mk_Trueprop (nth rec_preds i $ Free y)) (recs ~~ frees'');
val prems5 = mk_fresh3 (recs ~~ frees'') frees';
val prems6 = maps (fn aT => map (fn y as (_, T) => HOLogic.mk_Trueprop
- (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
- (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ Free y)))
+ (Const (@{const_name finite}, HOLogic.mk_setT aT --> HOLogic.boolT) $
+ (Const (@{const_name Nominal.supp}, T --> HOLogic.mk_setT aT) $ Free y)))
frees'') atomTs;
val prems7 = map (fn x as (_, T) => HOLogic.mk_Trueprop
(fresh_const T fsT' $ Free x $ rec_ctxt)) binders;
@@ -1534,7 +1535,7 @@
(Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P)))
(fn {context = ctxt, ...} => dtac (Thm.instantiate ([],
[(cterm_of thy11 (Var (("pi", 0), permT)),
- cterm_of thy11 (Const ("List.rev", permT --> permT) $ pi))]) th) 1 THEN
+ cterm_of thy11 (Const (@{const_name rev}, permT --> permT) $ pi))]) th) 1 THEN
NominalPermeq.perm_simp_tac (put_simpset HOL_ss ctxt) 1)) (ps ~~ ths)
in (ths, ths') end) dt_atomTs);
@@ -1545,9 +1546,9 @@
val name = Long_Name.base_name (fst (dest_Type aT));
val fs_name = Global_Theory.get_thm thy11 ("fs_" ^ name ^ "1");
val aset = HOLogic.mk_setT aT;
- val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
+ val finite = Const (@{const_name finite}, aset --> HOLogic.boolT);
val fins = map (fn (f, T) => HOLogic.mk_Trueprop
- (finite $ (Const ("Nominal.supp", T --> aset) $ f)))
+ (finite $ (Const (@{const_name Nominal.supp}, T --> aset) $ f)))
(rec_fns ~~ rec_fn_Ts)
in
map (fn th => Drule.export_without_context (th RS mp)) (Datatype_Aux.split_conj_thm
@@ -1561,7 +1562,7 @@
val y = Free ("y" ^ string_of_int i, U)
in
HOLogic.mk_imp (R $ x $ y,
- finite $ (Const ("Nominal.supp", U --> aset) $ y))
+ finite $ (Const (@{const_name Nominal.supp}, U --> aset) $ y))
end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~
(1 upto length recTs))))))
(fn {prems = fins, context = ctxt} =>
@@ -1573,8 +1574,8 @@
val finite_premss = map (fn aT =>
map (fn (f, T) => HOLogic.mk_Trueprop
- (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
- (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ f)))
+ (Const (@{const_name finite}, HOLogic.mk_setT aT --> HOLogic.boolT) $
+ (Const (@{const_name Nominal.supp}, T --> HOLogic.mk_setT aT) $ f)))
(rec_fns ~~ rec_fn_Ts)) dt_atomTs;
val rec_fns' = map (augment_sort thy11 fs_cp_sort) rec_fns;
@@ -1613,7 +1614,7 @@
in EVERY
[rtac (Drule.cterm_instantiate
[(cterm_of thy11 S,
- cterm_of thy11 (Const ("Nominal.supp",
+ cterm_of thy11 (Const (@{const_name Nominal.supp},
fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))]
supports_fresh) 1,
simp_tac (put_simpset HOL_basic_ss context addsimps
@@ -1654,7 +1655,7 @@
val induct_aux_rec = Drule.cterm_instantiate
(map (pairself (cterm_of thy11) o apsnd (augment_sort thy11 fs_cp_sort))
(map (fn (aT, f) => (Logic.varify_global f, Abs ("z", HOLogic.unitT,
- Const ("Nominal.supp", fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple)))
+ Const (@{const_name Nominal.supp}, fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple)))
fresh_fs @
map (fn (((P, T), (x, U)), Q) =>
(Var ((P, 0), Logic.varifyT_global (fsT' --> T --> HOLogic.boolT)),
@@ -1684,8 +1685,8 @@
val finite_ctxt_prems = map (fn aT =>
HOLogic.mk_Trueprop
- (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
- (Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs;
+ (Const (@{const_name finite}, HOLogic.mk_setT aT --> HOLogic.boolT) $
+ (Const (@{const_name Nominal.supp}, fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs;
val rec_unique_thms = Datatype_Aux.split_conj_thm (Goal.prove
(Proof_Context.init_global thy11) (map fst rec_unique_frees)
@@ -1752,7 +1753,7 @@
| _ => false)
| _ => false) prems';
val fresh_prems = filter (fn th => case prop_of th of
- _ $ (Const ("Nominal.fresh", _) $ _ $ _) => true
+ _ $ (Const (@{const_name Nominal.fresh}, _) $ _ $ _) => true
| _ $ (Const (@{const_name Not}, _) $ _) => true
| _ => false) prems';
val Ts = map fastype_of boundsl;
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Sat Mar 22 22:00:26 2014 +0100
@@ -87,8 +87,8 @@
| get_inner_fresh_fun (v as Var _) = NONE
| get_inner_fresh_fun (Const _) = NONE
| get_inner_fresh_fun (Abs (_, _, t)) = get_inner_fresh_fun t
- | get_inner_fresh_fun (Const ("Nominal.fresh_fun",Type("fun",[Type ("fun",[Type (T,_),_]),_])) $ u)
- = SOME T
+ | get_inner_fresh_fun (Const (@{const_name Nominal.fresh_fun},
+ Type(@{type_name fun},[Type (@{type_name fun},[Type (T,_),_]),_])) $ u) = SOME T
| get_inner_fresh_fun (t $ u) =
let val a = get_inner_fresh_fun u in
if a = NONE then get_inner_fresh_fun t else a
--- a/src/HOL/Nominal/nominal_inductive.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Sat Mar 22 22:00:26 2014 +0100
@@ -196,7 +196,7 @@
end) (Logic.strip_imp_prems raw_induct' ~~ avoids');
val atomTs = distinct op = (maps (map snd o #2) prems);
- val ind_sort = if null atomTs then HOLogic.typeS
+ val ind_sort = if null atomTs then @{sort type}
else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn T => Sign.intern_class thy
("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs));
val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
@@ -332,7 +332,7 @@
fun concat_perm pi1 pi2 =
let val T = fastype_of pi1
in if T = fastype_of pi2 then
- Const (@{const_name List.append}, T --> T --> T) $ pi1 $ pi2
+ Const (@{const_name append}, T --> T --> T) $ pi1 $ pi2
else pi2
end;
val pis'' = fold (concat_perm #> map) pis' pis;
--- a/src/HOL/Nominal/nominal_inductive2.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Sat Mar 22 22:00:26 2014 +0100
@@ -45,7 +45,7 @@
fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
(theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
- fn Const ("Nominal.perm", _) $ _ $ t =>
+ fn Const (@{const_name Nominal.perm}, _) $ _ $ t =>
if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
then SOME perm_bool else NONE
| _ => NONE);
@@ -97,13 +97,13 @@
(case head_of p of
Const (name, _) =>
if member (op =) names name then SOME (HOLogic.mk_conj (p,
- Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $
+ Const (@{const_name Fun.id}, HOLogic.boolT --> HOLogic.boolT) $
(subst_bounds (pis, strip_all pis q))))
else NONE
| _ => NONE)
| inst_conj_all names ps pis t u =
if member (op aconv) ps (head_of u) then
- SOME (Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $
+ SOME (Const (@{const_name Fun.id}, HOLogic.boolT --> HOLogic.boolT) $
(subst_bounds (pis, strip_all pis t)))
else NONE
| inst_conj_all _ _ _ _ _ = NONE;
@@ -222,7 +222,7 @@
val atomTs = distinct op = (maps (map snd o #2) prems);
val atoms = map (fst o dest_Type) atomTs;
- val ind_sort = if null atomTs then HOLogic.typeS
+ val ind_sort = if null atomTs then @{sort type}
else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn a => Sign.intern_class thy
("fs_" ^ Long_Name.base_name a)) atoms));
val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
@@ -292,7 +292,7 @@
("pt_" ^ Long_Name.base_name a ^ "2")) atoms;
val eqvt_ss = simpset_of (put_simpset HOL_basic_ss (Proof_Context.init_global thy)
addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
- addsimprocs [mk_perm_bool_simproc ["Fun.id"],
+ addsimprocs [mk_perm_bool_simproc [@{const_name Fun.id}],
NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]);
val fresh_star_bij = Global_Theory.get_thms thy "fresh_star_bij";
val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms;
@@ -312,7 +312,7 @@
(** protect terms to avoid that fresh_star_prod_set interferes with **)
(** pairs used in introduction rules of inductive predicate **)
fun protect t =
- let val T = fastype_of t in Const ("Fun.id", T --> T) $ t end;
+ let val T = fastype_of t in Const (@{const_name Fun.id}, T --> T) $ t end;
val p = foldr1 HOLogic.mk_prod (map protect ts);
val atom = fst (dest_Type T);
val {at_inst, ...} = NominalAtoms.the_atom_info thy atom;
@@ -393,7 +393,7 @@
fun concat_perm pi1 pi2 =
let val T = fastype_of pi1
in if T = fastype_of pi2 then
- Const ("List.append", T --> T --> T) $ pi1 $ pi2
+ Const (@{const_name append}, T --> T --> T) $ pi1 $ pi2
else pi2
end;
val pis'' = fold_rev (concat_perm #> map) pis' pis;
--- a/src/HOL/Nominal/nominal_permeq.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML Sat Mar 22 22:00:26 2014 +0100
@@ -97,14 +97,15 @@
(* constant or when (f x) is a permuation with two or more arguments *)
fun applicable_app t =
(case (strip_comb t) of
- (Const ("Nominal.perm",_),ts) => (length ts) >= 2
+ (Const (@{const_name Nominal.perm},_),ts) => (length ts) >= 2
| (Const _,_) => false
| _ => true)
in
case redex of
(* case pi o (f x) == (pi o f) (pi o x) *)
- (Const("Nominal.perm",
- Type("fun",[Type("List.list",[Type(@{type_name Product_Type.prod},[Type(n,_),_])]),_])) $ pi $ (f $ x)) =>
+ (Const(@{const_name Nominal.perm},
+ Type(@{type_name fun},
+ [Type(@{type_name list}, [Type(@{type_name prod},[Type(n,_),_])]),_])) $ pi $ (f $ x)) =>
(if (applicable_app f) then
let
val name = Long_Name.base_name n
@@ -124,13 +125,13 @@
fun applicable_fun t =
(case (strip_comb t) of
(Abs _ ,[]) => true
- | (Const ("Nominal.perm",_),_) => false
+ | (Const (@{const_name Nominal.perm},_),_) => false
| (Const _, _) => true
| _ => false)
in
case redex of
(* case pi o f == (%x. pi o (f ((rev pi)o x))) *)
- (Const("Nominal.perm",_) $ pi $ f) =>
+ (Const(@{const_name Nominal.perm},_) $ pi $ f) =>
(if applicable_fun f then SOME perm_fun_def else NONE)
| _ => NONE
end
@@ -190,9 +191,9 @@
fun perm_compose_simproc' ctxt redex =
(case redex of
- (Const ("Nominal.perm", Type ("fun", [Type ("List.list",
- [Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm",
- Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $
+ (Const (@{const_name Nominal.perm}, Type (@{type_name fun}, [Type (@{type_name list},
+ [Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const (@{const_name Nominal.perm},
+ Type (@{type_name fun}, [Type (@{type_name list}, [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $
pi2 $ t)) =>
let
val thy = Proof_Context.theory_of ctxt
@@ -293,7 +294,7 @@
let val goal = nth (cprems_of st) (i - 1)
in
case Envir.eta_contract (Logic.strip_assums_concl (term_of goal)) of
- _ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) =>
+ _ $ (Const (@{const_name finite}, _) $ (Const (@{const_name Nominal.supp}, T) $ x)) =>
let
val cert = Thm.cterm_of (Thm.theory_of_thm st);
val ps = Logic.strip_params (term_of goal);
@@ -303,7 +304,7 @@
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
vs HOLogic.unit;
val s' = fold_rev Term.abs ps
- (Const ("Nominal.supp", fastype_of1 (Ts, s) -->
+ (Const (@{const_name Nominal.supp}, fastype_of1 (Ts, s) -->
Term.range_type T) $ s);
val supports_rule' = Thm.lift_rule goal supports_rule;
val _ $ (_ $ S $ _) =
@@ -337,7 +338,7 @@
val ctxt2 = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
in
case Logic.strip_assums_concl (term_of goal) of
- _ $ (Const ("Nominal.fresh", Type ("fun", [T, _])) $ _ $ t) =>
+ _ $ (Const (@{const_name Nominal.fresh}, Type ("fun", [T, _])) $ _ $ t) =>
let
val cert = Thm.cterm_of (Thm.theory_of_thm st);
val ps = Logic.strip_params (term_of goal);
@@ -348,7 +349,7 @@
vs HOLogic.unit;
val s' =
fold_rev Term.abs ps
- (Const ("Nominal.supp", fastype_of1 (Ts, s) --> HOLogic.mk_setT T) $ s);
+ (Const (@{const_name Nominal.supp}, fastype_of1 (Ts, s) --> HOLogic.mk_setT T) $ s);
val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;
val _ $ (_ $ S $ _) =
Logic.strip_assums_concl (hd (prems_of supports_fresh_rule'));
--- a/src/HOL/TLA/Action.thy Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/TLA/Action.thy Sat Mar 22 22:00:26 2014 +0100
@@ -117,7 +117,7 @@
fun action_use ctxt th =
case (concl_of th) of
- Const _ $ (Const ("Intensional.Valid", _) $ _) =>
+ Const _ $ (Const (@{const_name Valid}, _) $ _) =>
(flatten (action_unlift ctxt th) handle THM _ => th)
| _ => th;
*}
--- a/src/HOL/TLA/Intensional.thy Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/TLA/Intensional.thy Sat Mar 22 22:00:26 2014 +0100
@@ -283,7 +283,7 @@
fun int_use ctxt th =
case (concl_of th) of
- Const _ $ (Const ("Intensional.Valid", _) $ _) =>
+ Const _ $ (Const (@{const_name Valid}, _) $ _) =>
(flatten (int_unlift ctxt th) handle THM _ => th)
| _ => th
*}
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Sat Mar 22 22:00:26 2014 +0100
@@ -256,11 +256,11 @@
in
case thf_ty of
Prod_type (thf_ty1, thf_ty2) =>
- Type ("Product_Type.prod",
+ Type (@{type_name prod},
[interpret_type config thy type_map thf_ty1,
interpret_type config thy type_map thf_ty2])
| Fn_type (thf_ty1, thf_ty2) =>
- Type ("fun",
+ Type (@{type_name fun},
[interpret_type config thy type_map thf_ty1,
interpret_type config thy type_map thf_ty2])
| Atom_type _ =>
@@ -398,8 +398,7 @@
(*As above, but for products*)
fun mtimes thy =
fold (fn x => fn y =>
- Sign.mk_const thy
- ("Product_Type.Pair", [dummyT, dummyT]) $ y $ x)
+ Sign.mk_const thy (@{const_name Pair}, [dummyT, dummyT]) $ y $ x)
fun mtimes' (args, thy) f =
let
@@ -456,11 +455,11 @@
end
(*Next batch of functions give info about Isabelle/HOL types*)
-fun is_fun (Type ("fun", _)) = true
+fun is_fun (Type (@{type_name fun}, _)) = true
| is_fun _ = false
-fun is_prod (Type ("Product_Type.prod", _)) = true
+fun is_prod (Type (@{type_name prod}, _)) = true
| is_prod _ = false
-fun dom_type (Type ("fun", [ty1, _])) = ty1
+fun dom_type (Type (@{type_name fun}, [ty1, _])) = ty1
fun is_prod_typed thy config symb =
let
fun symb_type const_name =
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sat Mar 22 22:00:26 2014 +0100
@@ -999,15 +999,15 @@
val is =
upto (1, arity)
|> map Int.toString
- val arg_tys = map (fn i => TFree ("arg" ^ i ^ "_ty", HOLogic.typeS)) is
- val res_ty = TFree ("res" ^ "_ty", HOLogic.typeS)
+ val arg_tys = map (fn i => TFree ("arg" ^ i ^ "_ty", @{sort type})) is
+ val res_ty = TFree ("res" ^ "_ty", @{sort type})
val f_ty = arg_tys ---> res_ty
val f = Free ("f", f_ty)
val xs = map (fn i =>
- Free ("x" ^ i, TFree ("arg" ^ i ^ "_ty", HOLogic.typeS))) is
+ Free ("x" ^ i, TFree ("arg" ^ i ^ "_ty", @{sort type}))) is
(*FIXME DRY principle*)
val ys = map (fn i =>
- Free ("y" ^ i, TFree ("arg" ^ i ^ "_ty", HOLogic.typeS))) is
+ Free ("y" ^ i, TFree ("arg" ^ i ^ "_ty", @{sort type}))) is
val hyp_lhs = list_comb (f, xs)
val hyp_rhs = list_comb (f, ys)
@@ -1018,7 +1018,7 @@
|> HOLogic.mk_Trueprop
fun conc_eq i =
let
- val ty = TFree ("arg" ^ i ^ "_ty", HOLogic.typeS)
+ val ty = TFree ("arg" ^ i ^ "_ty", @{sort type})
val x = Free ("x" ^ i, ty)
val y = Free ("y" ^ i, ty)
val eq = HOLogic.eq_const ty $ x $ y
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sat Mar 22 22:00:26 2014 +0100
@@ -434,7 +434,7 @@
fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
val tvar_a_str = "'a"
-val tvar_a_z = ((tvar_a_str, 0), HOLogic.typeS)
+val tvar_a_z = ((tvar_a_str, 0), @{sort type})
val tvar_a = TVar tvar_a_z
val tvar_a_name = tvar_name tvar_a_z
val itself_name = `make_fixed_type_const @{type_name itself}
@@ -2404,7 +2404,7 @@
fun rationalize_decls thy (decls as decl :: (decls' as _ :: _)) =
let
- val T = result_type_of_decl decl |> map_type_tvar (fn (z, _) => TVar (z, HOLogic.typeS))
+ val T = result_type_of_decl decl |> map_type_tvar (fn (z, _) => TVar (z, @{sort type}))
in
if forall (type_generalization thy T o result_type_of_decl) decls' then [decl]
else decls
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sat Mar 22 22:00:26 2014 +0100
@@ -94,7 +94,7 @@
fun make_tfree ctxt w =
let val ww = "'" ^ w in
- TFree (ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))
+ TFree (ww, the_default @{sort type} (Variable.def_sort ctxt (ww, ~1)))
end
exception ATP_CLASS of string list
@@ -126,7 +126,7 @@
Sometimes variables from the ATP are indistinguishable from Isabelle variables, which
forces us to use a type parameter in all cases. *)
Type_Infer.param 0 ("'" ^ perhaps (unprefix_and_unascii tvar_prefix) a,
- (if null clss then HOLogic.typeS else map class_of_atp_class clss))))
+ (if null clss then @{sort type} else map class_of_atp_class clss))))
end
fun atp_type_of_atp_term (ATerm ((s, _), us)) = AType ((s, []), map atp_type_of_atp_term us)
@@ -175,7 +175,7 @@
else
(s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
-fun slack_fastype_of t = fastype_of t handle TERM _ => HOLogic.typeT
+fun slack_fastype_of t = fastype_of t handle TERM _ => Type_Infer.anyT @{sort type}
(* Cope with "tt(X) = X" atoms, where "X" is existentially quantified. *)
fun loose_aconv (Free (s, _), Free (s', _)) = s = s'
@@ -184,8 +184,8 @@
val spass_skolem_prefix = "sk" (* "skc" or "skf" *)
val vampire_skolem_prefix = "sK"
-(* First-order translation. No types are known for variables. "HOLogic.typeT" should allow them to
- be inferred. *)
+(* First-order translation. No types are known for variables. "Type_Infer.anyT @{sort type}"
+ should allow them to be inferred. *)
fun term_of_atp ctxt textual sym_tab =
let
val thy = Proof_Context.theory_of ctxt
@@ -206,7 +206,7 @@
if textual andalso length ts = 2 andalso loose_aconv (hd ts, List.last ts) then
@{const True}
else
- list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
+ list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), ts)
end
else
(case unprefix_and_unascii const_prefix s of
@@ -248,7 +248,8 @@
NONE)
|> (fn SOME T => T
| NONE =>
- map slack_fastype_of term_ts ---> the_default HOLogic.typeT opt_T)
+ map slack_fastype_of term_ts --->
+ the_default (Type_Infer.anyT @{sort type}) opt_T)
val t =
if new_skolem then Var ((new_skolem_var_name_of_const s'', var_index), T)
else Const (unproxify_const s', T)
@@ -274,7 +275,7 @@
SOME T => map slack_fastype_of term_ts ---> T
| NONE =>
map slack_fastype_of ts --->
- (case tys of [ty] => typ_of_atp_type ctxt ty | _ => HOLogic.typeT))
+ (case tys of [ty] => typ_of_atp_type ctxt ty | _ => Type_Infer.anyT @{sort type}))
val t =
(case unprefix_and_unascii fixed_var_prefix s of
SOME s => Free (s, T)
--- a/src/HOL/Tools/BNF/bnf_comp.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Sat Mar 22 22:00:26 2014 +0100
@@ -138,15 +138,15 @@
forall inner from inners. idead = dead *)
val (oDs, lthy1) = apfst (map TFree)
- (Variable.invent_types (replicate odead HOLogic.typeS) lthy);
+ (Variable.invent_types (replicate odead @{sort type}) lthy);
val (Dss, lthy2) = apfst (map (map TFree))
- (fold_map Variable.invent_types (map (fn n => replicate n HOLogic.typeS) ideads) lthy1);
+ (fold_map Variable.invent_types (map (fn n => replicate n @{sort type}) ideads) lthy1);
val (Ass, lthy3) = apfst (replicate ilive o map TFree)
- (Variable.invent_types (replicate ilive HOLogic.typeS) lthy2);
+ (Variable.invent_types (replicate ilive @{sort type}) lthy2);
val As = if ilive > 0 then hd Ass else [];
val Ass_repl = replicate olive As;
val (Bs, names_lthy) = apfst (map TFree)
- (Variable.invent_types (replicate ilive HOLogic.typeS) lthy3);
+ (Variable.invent_types (replicate ilive @{sort type}) lthy3);
val Bss_repl = replicate olive Bs;
val ((((fs', Qs'), Asets), xs), _) = names_lthy
@@ -363,11 +363,11 @@
(* TODO: check 0 < n <= live *)
val (Ds, lthy1) = apfst (map TFree)
- (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
+ (Variable.invent_types (replicate dead @{sort type}) lthy);
val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree)
- (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
+ (Variable.invent_types (replicate live @{sort type}) lthy1);
val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree)
- (Variable.invent_types (replicate (live - n) HOLogic.typeS) lthy2);
+ (Variable.invent_types (replicate (live - n) @{sort type}) lthy2);
val ((Asets, lives), _(*names_lthy*)) = lthy
|> mk_Frees "A" (map HOLogic.mk_setT (drop n As))
@@ -462,11 +462,11 @@
(* TODO: check 0 < n *)
val (Ds, lthy1) = apfst (map TFree)
- (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
+ (Variable.invent_types (replicate dead @{sort type}) lthy);
val ((newAs, As), lthy2) = apfst (chop n o map TFree)
- (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy1);
+ (Variable.invent_types (replicate (n + live) @{sort type}) lthy1);
val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree)
- (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy2);
+ (Variable.invent_types (replicate (n + live) @{sort type}) lthy2);
val (Asets, _(*names_lthy*)) = lthy
|> mk_Frees "A" (map HOLogic.mk_setT (newAs @ As));
@@ -553,11 +553,11 @@
fun unpermute xs = permute_like_unique (op =) dest src xs;
val (Ds, lthy1) = apfst (map TFree)
- (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
+ (Variable.invent_types (replicate dead @{sort type}) lthy);
val (As, lthy2) = apfst (map TFree)
- (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
+ (Variable.invent_types (replicate live @{sort type}) lthy1);
val (Bs, _(*lthy3*)) = apfst (map TFree)
- (Variable.invent_types (replicate live HOLogic.typeS) lthy2);
+ (Variable.invent_types (replicate live @{sort type}) lthy2);
val (Asets, _(*names_lthy*)) = lthy
|> mk_Frees "A" (map HOLogic.mk_setT (permute As));
@@ -757,9 +757,9 @@
val nwits = nwits_of_bnf bnf;
val (As, lthy1) = apfst (map TFree)
- (Variable.invent_types (replicate live HOLogic.typeS) (fold Variable.declare_typ Ds lthy));
+ (Variable.invent_types (replicate live @{sort type}) (fold Variable.declare_typ Ds lthy));
val (Bs, _) = apfst (map TFree)
- (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
+ (Variable.invent_types (replicate live @{sort type}) lthy1);
val (((fs, fs'), (Rs, Rs')), _(*names_lthy*)) = lthy
|> mk_Frees' "f" (map2 (curry op -->) As Bs)
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sat Mar 22 22:00:26 2014 +0100
@@ -901,7 +901,7 @@
end;
val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of_spec) specs;
- val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
+ val unsorted_Ass0 = map (map (resort_tfree @{sort type})) Ass0;
val unsorted_As = Library.foldr1 (merge_type_args fp) unsorted_Ass0;
val num_As = length unsorted_As;
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sat Mar 22 22:00:26 2014 +0100
@@ -963,7 +963,7 @@
val (bs, mxs) = map_split (apfst fst) fixes;
val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> mk_tupleT_balanced) fixes |> split_list;
- val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ arg_Ts) of
+ val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, @{sort type})) (bs ~~ arg_Ts) of
[] => ()
| (b, _) :: _ => primcorec_error ("type of " ^ Binding.print b ^ " contains top sort"));
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Sat Mar 22 22:00:26 2014 +0100
@@ -447,7 +447,7 @@
| is_only_old_datatype _ = false;
val _ = if exists is_only_old_datatype arg_Ts then raise OLD_PRIMREC () else ();
- val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ res_Ts) of
+ val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, @{sort type})) (bs ~~ res_Ts) of
[] => ()
| (b, _) :: _ => raise PRIMREC ("type of " ^ Binding.print b ^ " contains top sort", []));
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Sat Mar 22 22:00:26 2014 +0100
@@ -148,7 +148,7 @@
val mk_TFrees' = apfst (map TFree) oo Variable.invent_types;
-fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS);
+fun mk_TFrees n = mk_TFrees' (replicate n @{sort type});
fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts));
fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
@@ -169,7 +169,7 @@
fun variant_tfrees ss =
apfst (map TFree) o
- variant_types (map (ensure_prefix "'") ss) (replicate (length ss) HOLogic.typeS);
+ variant_types (map (ensure_prefix "'") ss) (replicate (length ss) @{sort type});
(*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*)
fun typ_subst_nonatomic [] = I
--- a/src/HOL/Tools/Datatype/datatype.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Sat Mar 22 22:00:26 2014 +0100
@@ -373,7 +373,7 @@
fun mk_thm i =
let
- val Ts = map (TFree o rpair HOLogic.typeS) (Name.variant_list used (replicate i "'t"));
+ val Ts = map (TFree o rpair @{sort type}) (Name.variant_list used (replicate i "'t"));
val f = Free ("f", Ts ---> U);
in
Goal.prove_sorry_global thy [] []
@@ -707,7 +707,7 @@
fun gen_add_datatype prep_specs config raw_specs thy =
let
- val _ = Theory.requires thy "Datatype" "datatype definitions";
+ val _ = Theory.requires thy (Context.theory_name @{theory}) "datatype definitions";
val (dts, spec_ctxt) = prep_specs raw_specs thy;
val ((_, tyvars, _), _) :: _ = dts;
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Sat Mar 22 22:00:26 2014 +0100
@@ -182,7 +182,7 @@
val rec_result_Ts =
map TFree
(Name.variant_list used (replicate (length descr') "'t") ~~
- replicate (length descr') HOLogic.typeS);
+ replicate (length descr') @{sort type});
val reccomb_fn_Ts = maps (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
@@ -251,7 +251,7 @@
val recTs = Datatype_Aux.get_rec_types descr';
val used = fold Term.add_tfree_namesT recTs [];
val newTs = take (length (hd descr)) recTs;
- val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
+ val T' = TFree (singleton (Name.variant_list used) "'t", @{sort type});
val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
@@ -296,7 +296,7 @@
val recTs = Datatype_Aux.get_rec_types descr';
val used' = fold Term.add_tfree_namesT recTs [];
val newTs = take (length (hd descr)) recTs;
- val T' = TFree (singleton (Name.variant_list used') "'t", HOLogic.typeS);
+ val T' = TFree (singleton (Name.variant_list used') "'t", @{sort type});
val P = Free ("P", T' --> HOLogic.boolT);
fun make_split (((_, (_, _, constrs)), T), comb_t) =
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Sat Mar 22 22:00:26 2014 +0100
@@ -36,7 +36,7 @@
else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
val rec_result_Ts = map (fn ((i, _), P) =>
- if member (op =) is i then TFree ("'" ^ P, HOLogic.typeS) else HOLogic.unitT)
+ if member (op =) is i then TFree ("'" ^ P, @{sort type}) else HOLogic.unitT)
(descr ~~ pnames);
fun make_pred i T U r x =
@@ -163,8 +163,8 @@
let
val ctxt = Proof_Context.init_global thy;
val cert = cterm_of thy;
- val rT = TFree ("'P", HOLogic.typeS);
- val rT' = TVar (("'P", 0), HOLogic.typeS);
+ val rT = TFree ("'P", @{sort type});
+ val rT' = TVar (("'P", 0), @{sort type});
fun make_casedist_prem T (cname, cargs) =
let
--- a/src/HOL/Tools/Datatype/rep_datatype.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Sat Mar 22 22:00:26 2014 +0100
@@ -278,7 +278,7 @@
val recTs = Datatype_Aux.get_rec_types descr';
val used = fold Term.add_tfree_namesT recTs [];
val newTs = take (length (hd descr)) recTs;
- val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
+ val T' = TFree (singleton (Name.variant_list used) "'t", @{sort type});
fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' dt) ---> T';
--- a/src/HOL/Tools/Function/fun.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Function/fun.ML Sat Mar 22 22:00:26 2014 +0100
@@ -73,7 +73,7 @@
val qs = map Free (Name.invent Name.context "a" n ~~ argTs)
in
HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
- Const ("HOL.undefined", rT))
+ Const (@{const_name undefined}, rT))
|> HOLogic.mk_Trueprop
|> fold_rev Logic.all qs
end
--- a/src/HOL/Tools/Function/function.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Function/function.ML Sat Mar 22 22:00:26 2014 +0100
@@ -156,7 +156,7 @@
end
val add_function =
- gen_add_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
+ gen_add_function false Specification.check_spec (Type_Infer.anyT @{sort type})
fun add_function_cmd a b c d int = gen_add_function int Specification.read_spec "_::type" a b c d
fun gen_function do_print prep default_constraint fixspec eqns config lthy =
@@ -170,7 +170,7 @@
end
val function =
- gen_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
+ gen_function false Specification.check_spec (Type_Infer.anyT @{sort type})
fun function_cmd a b c int = gen_function int Specification.read_spec "_::type" a b c
fun prepare_termination_proof prep_term raw_term_opt lthy =
--- a/src/HOL/Tools/Function/function_common.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Function/function_common.ML Sat Mar 22 22:00:26 2014 +0100
@@ -347,7 +347,7 @@
plural " " "s " not_defined ^ commas_quote not_defined)
fun check_sorts ((fname, fT), _) =
- Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, HOLogic.typeS)
+ Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, @{sort type})
orelse error (cat_lines
["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
--- a/src/HOL/Tools/Lifting/lifting_info.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Sat Mar 22 22:00:26 2014 +0100
@@ -446,30 +446,35 @@
let
val assms = map (perhaps (try HOLogic.dest_Trueprop)) (prems_of rule)
val concl = (perhaps (try HOLogic.dest_Trueprop)) (concl_of rule);
- val (lhs, rhs) = case concl of
- Const ("Orderings.ord_class.less_eq", _) $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) $ rhs =>
- (lhs, rhs)
- | Const ("Orderings.ord_class.less_eq", _) $ rhs $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) =>
- (lhs, rhs)
- | Const ("HOL.eq", _) $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) $ rhs => (lhs, rhs)
- | _ => error "The rule has a wrong format."
+ val (lhs, rhs) =
+ (case concl of
+ Const (@{const_name less_eq}, _) $ (lhs as Const (@{const_name relcompp},_) $ _ $ _) $ rhs =>
+ (lhs, rhs)
+ | Const (@{const_name less_eq}, _) $ rhs $ (lhs as Const (@{const_name relcompp},_) $ _ $ _) =>
+ (lhs, rhs)
+ | Const (@{const_name HOL.eq}, _) $ (lhs as Const (@{const_name relcompp},_) $ _ $ _) $ rhs =>
+ (lhs, rhs)
+ | _ => error "The rule has a wrong format.")
val lhs_vars = Term.add_vars lhs []
val rhs_vars = Term.add_vars rhs []
val assms_vars = fold Term.add_vars assms [];
- val _ = if has_duplicates op= lhs_vars then error "Left-hand side has variable duplicates" else ()
- val _ = if subset op= (rhs_vars, lhs_vars) then ()
+ val _ =
+ if has_duplicates op= lhs_vars
+ then error "Left-hand side has variable duplicates" else ()
+ val _ =
+ if subset op= (rhs_vars, lhs_vars) then ()
else error "Extra variables in the right-hand side of the rule"
- val _ = if subset op= (assms_vars, lhs_vars) then ()
+ val _ =
+ if subset op= (assms_vars, lhs_vars) then ()
else error "Extra variables in the assumptions of the rule"
val rhs_args = (snd o strip_comb) rhs;
- fun check_comp t = case t of
- Const ("Relation.relcompp", _) $ Var (_, _) $ Var (_,_) => ()
- | _ => error "There is an argument on the rhs that is not a composition."
+ fun check_comp t =
+ (case t of
+ Const (@{const_name relcompp}, _) $ Var _ $ Var _ => ()
+ | _ => error "There is an argument on the rhs that is not a composition.")
val _ = map check_comp rhs_args
- in
- ()
- end
+ in () end
in
fun add_distr_rule distr_rule ctxt =
@@ -477,13 +482,13 @@
val _ = sanity_check distr_rule
val concl = (perhaps (try HOLogic.dest_Trueprop)) (concl_of distr_rule)
in
- case concl of
- Const ("Orderings.ord_class.less_eq", _) $ (Const ("Relation.relcompp",_) $ _ $ _) $ _ =>
+ (case concl of
+ Const (@{const_name less_eq}, _) $ (Const (@{const_name relcompp},_) $ _ $ _) $ _ =>
add_pos_distr_rule distr_rule ctxt
- | Const ("Orderings.ord_class.less_eq", _) $ _ $ (Const ("Relation.relcompp",_) $ _ $ _) =>
+ | Const (@{const_name less_eq}, _) $ _ $ (Const (@{const_name relcompp},_) $ _ $ _) =>
add_neg_distr_rule distr_rule ctxt
- | Const ("HOL.eq", _) $ (Const ("Relation.relcompp",_) $ _ $ _) $ _ =>
- add_eq_distr_rule distr_rule ctxt
+ | Const (@{const_name HOL.eq}, _) $ (Const (@{const_name relcompp},_) $ _ $ _) $ _ =>
+ add_eq_distr_rule distr_rule ctxt)
end
end
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Sat Mar 22 22:00:26 2014 +0100
@@ -85,16 +85,16 @@
val eq_OO_meta = mk_meta_eq @{thm eq_OO}
fun print_generate_pcr_cr_eq_error ctxt term =
- let
- val goal = (Const ("HOL.eq", dummyT)) $ term $ Const ("HOL.eq", dummyT)
- val error_msg = cat_lines
- ["Generation of a pcr_cr_eq failed.",
- (Pretty.string_of (Pretty.block
- [Pretty.str "Reason: Cannot prove this: ", Pretty.brk 2, Syntax.pretty_term ctxt goal])),
- "Most probably a relator_eq rule for one of the involved types is missing."]
- in
- error error_msg
- end
+ let
+ val goal = Const (@{const_name HOL.eq}, dummyT) $ term $ Const (@{const_name HOL.eq}, dummyT)
+ val error_msg = cat_lines
+ ["Generation of a pcr_cr_eq failed.",
+ (Pretty.string_of (Pretty.block
+ [Pretty.str "Reason: Cannot prove this: ", Pretty.brk 2, Syntax.pretty_term ctxt goal])),
+ "Most probably a relator_eq rule for one of the involved types is missing."]
+ in
+ error error_msg
+ end
in
fun define_pcr_cr_eq lthy pcr_rel_def =
let
@@ -121,15 +121,15 @@
(Transfer.bottom_rewr_conv (Transfer.get_relator_eq lthy))))
in
case (term_of o Thm.rhs_of) pcr_cr_eq of
- Const (@{const_name "relcompp"}, _) $ Const ("HOL.eq", _) $ _ =>
+ Const (@{const_name "relcompp"}, _) $ Const (@{const_name HOL.eq}, _) $ _ =>
let
val thm =
pcr_cr_eq
|> Conv.fconv_rule (Conv.arg_conv (Conv.rewr_conv eq_OO_meta))
|> mk_HOL_eq
|> singleton (Variable.export lthy orig_lthy)
- val ((_, [thm]), lthy) = Local_Theory.note ((Binding.qualified true "pcr_cr_eq" qty_name, []),
- [thm]) lthy
+ val ((_, [thm]), lthy) =
+ Local_Theory.note ((Binding.qualified true "pcr_cr_eq" qty_name, []), [thm]) lthy
in
(thm, lthy)
end
@@ -626,7 +626,7 @@
val T_def = Morphism.thm (Local_Theory.target_morphism lthy) T_def
(**)
val quot_thm = case typedef_set of
- Const ("Orderings.top_class.top", _) =>
+ Const (@{const_name top}, _) =>
[typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
| Const (@{const_name "Collect"}, _) $ Abs (_, _, _) =>
[typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
@@ -638,7 +638,7 @@
fun qualify suffix = Binding.qualified true suffix qty_name
val opt_reflp_thm =
case typedef_set of
- Const ("Orderings.top_class.top", _) =>
+ Const (@{const_name top}, _) =>
SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2})
| _ => NONE
val dom_thm = get_Domainp_thm quot_thm
@@ -819,7 +819,7 @@
Pretty.brk 1,
Display.pretty_thm ctxt pcr_cr_eq]]
val (pcr_const_eq, eqs) = strip_comb eq_lhs
- fun is_eq (Const ("HOL.eq", _)) = true
+ fun is_eq (Const (@{const_name HOL.eq}, _)) = true
| is_eq _ = false
fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2)
| eq_Const _ _ = false
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Mar 22 22:00:26 2014 +0100
@@ -1053,7 +1053,7 @@
(Object_Logic.atomize_term thy prop)
val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl))
|> map_types (map_type_tfree
- (fn (s, []) => TFree (s, HOLogic.typeS)
+ (fn (s, []) => TFree (s, @{sort type})
| x => TFree x))
val _ =
if debug then
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Mar 22 22:00:26 2014 +0100
@@ -920,7 +920,7 @@
val Type ("fun", [T, T']) = fastype_of comb;
val (Const (case_name, _), fs) = strip_comb comb
val used = Term.add_tfree_names comb []
- val U = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS)
+ val U = TFree (singleton (Name.variant_list used) "'t", @{sort type})
val x = Free ("x", T)
val f = Free ("f", T' --> U)
fun apply_f f' =
@@ -947,8 +947,8 @@
val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
val ([_, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
- val T' = TFree (tname', HOLogic.typeS)
- val U = TFree (uname, HOLogic.typeS)
+ val T' = TFree (tname', @{sort type})
+ val U = TFree (uname, @{sort type})
val y = Free (yname, U)
val f' = absdummy (U --> T') (Bound 0 $ y)
val th' = Thm.certify_instantiate
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Sat Mar 22 22:00:26 2014 +0100
@@ -176,8 +176,10 @@
val (Ts, fns) = split_list xs
val constr = Const (c, Ts ---> simpleT)
val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0)
- val Eval_App = Const ("Code_Evaluation.App", HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
- val Eval_Const = Const ("Code_Evaluation.Const", HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
+ val Eval_App =
+ Const (@{const_name Code_Evaluation.App}, HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
+ val Eval_Const =
+ Const (@{const_name Code_Evaluation.Const}, HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
val start_term = test_function simpleT $
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Mar 22 22:00:26 2014 +0100
@@ -577,7 +577,7 @@
val pat_var_prefix = "_"
(* try "Long_Name.base_name" for shorter names *)
-fun massage_long_name s = if s = hd HOLogic.typeS then "T" else s
+fun massage_long_name s = if s = @{class type} then "T" else s
val crude_str_of_sort =
space_implode ":" o map massage_long_name o subtract (op =) @{sort type}
--- a/src/HOL/Tools/TFL/usyntax.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/TFL/usyntax.ML Sat Mar 22 22:00:26 2014 +0100
@@ -104,7 +104,7 @@
*
*---------------------------------------------------------------------------*)
val mk_prim_vartype = TVar;
-fun mk_vartype s = mk_prim_vartype ((s, 0), HOLogic.typeS);
+fun mk_vartype s = mk_prim_vartype ((s, 0), @{sort type});
(* But internally, it's useful *)
fun dest_vtype (TVar x) = x
--- a/src/HOL/Tools/choice_specification.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/choice_specification.ML Sat Mar 22 22:00:26 2014 +0100
@@ -131,7 +131,7 @@
fun proc_single prop =
let
val frees = Misc_Legacy.term_frees prop
- val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
+ val _ = forall (fn v => Sign.of_sort thy (type_of v,@{sort type})) frees
orelse error "Specificaton: Only free variables of sort 'type' allowed"
val prop_closed = close_form prop
in
--- a/src/HOL/Tools/float_arith.ML Sat Mar 22 08:37:43 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,221 +0,0 @@
-(* Title: HOL/Tools/float_arith.ML
- Author: Steven Obua
-*)
-
-signature FLOAT_ARITH =
-sig
- exception Destruct_floatstr of string
- val destruct_floatstr: (char -> bool) -> (char -> bool) -> string -> bool * string * string * bool * string
-
- exception Floating_point of string
- val approx_dec_by_bin: int -> Float.float -> Float.float * Float.float
- val approx_decstr_by_bin: int -> string -> Float.float * Float.float
-
- val mk_float: Float.float -> term
- val dest_float: term -> Float.float
-
- val approx_float: int -> (Float.float * Float.float -> Float.float * Float.float)
- -> string -> term * term
-end;
-
-structure FloatArith : FLOAT_ARITH =
-struct
-
-exception Destruct_floatstr of string;
-
-fun destruct_floatstr isDigit isExp number =
- let
- val numlist = filter (not o Char.isSpace) (String.explode number)
-
- fun countsigns ((#"+")::cs) = countsigns cs
- | countsigns ((#"-")::cs) =
- let
- val (positive, rest) = countsigns cs
- in
- (not positive, rest)
- end
- | countsigns cs = (true, cs)
-
- fun readdigits [] = ([], [])
- | readdigits (q as c::cs) =
- if (isDigit c) then
- let
- val (digits, rest) = readdigits cs
- in
- (c::digits, rest)
- end
- else
- ([], q)
-
- fun readfromexp_helper cs =
- let
- val (positive, rest) = countsigns cs
- val (digits, rest') = readdigits rest
- in
- case rest' of
- [] => (positive, digits)
- | _ => raise (Destruct_floatstr number)
- end
-
- fun readfromexp [] = (true, [])
- | readfromexp (c::cs) =
- if isExp c then
- readfromexp_helper cs
- else
- raise (Destruct_floatstr number)
-
- fun readfromdot [] = ([], readfromexp [])
- | readfromdot ((#".")::cs) =
- let
- val (digits, rest) = readdigits cs
- val exp = readfromexp rest
- in
- (digits, exp)
- end
- | readfromdot cs = readfromdot ((#".")::cs)
-
- val (positive, numlist) = countsigns numlist
- val (digits1, numlist) = readdigits numlist
- val (digits2, exp) = readfromdot numlist
- in
- (positive, String.implode digits1, String.implode digits2, fst exp, String.implode (snd exp))
- end
-
-exception Floating_point of string;
-
-val ln2_10 = Math.ln 10.0 / Math.ln 2.0;
-fun exp5 x = Integer.pow x 5;
-fun exp10 x = Integer.pow x 10;
-fun exp2 x = Integer.pow x 2;
-
-fun find_most_significant q r =
- let
- fun int2real i =
- case (Real.fromString o string_of_int) i of
- SOME r => r
- | NONE => raise (Floating_point "int2real")
- fun subtract (q, r) (q', r') =
- if r <= r' then
- (q - q' * exp10 (r' - r), r)
- else
- (q * exp10 (r - r') - q', r')
- fun bin2dec d =
- if 0 <= d then
- (exp2 d, 0)
- else
- (exp5 (~ d), d)
-
- val L = Real.floor (int2real (IntInf.log2 q) + int2real r * ln2_10)
- val L1 = L + 1
-
- val (q1, r1) = subtract (q, r) (bin2dec L1)
- in
- if 0 <= q1 then
- let
- val (q2, r2) = subtract (q, r) (bin2dec (L1 + 1))
- in
- if 0 <= q2 then
- raise (Floating_point "find_most_significant")
- else
- (L1, (q1, r1))
- end
- else
- let
- val (q0, r0) = subtract (q, r) (bin2dec L)
- in
- if 0 <= q0 then
- (L, (q0, r0))
- else
- raise (Floating_point "find_most_significant")
- end
- end
-
-fun approx_dec_by_bin n (q,r) =
- let
- fun addseq acc d' [] = acc
- | addseq acc d' (d::ds) = addseq (acc + exp2 (d - d')) d' ds
-
- fun seq2bin [] = (0, 0)
- | seq2bin (d::ds) = (addseq 0 d ds + 1, d)
-
- fun approx d_seq d0 precision (q,r) =
- if q = 0 then
- let val x = seq2bin d_seq in
- (x, x)
- end
- else
- let
- val (d, (q', r')) = find_most_significant q r
- in
- if precision < d0 - d then
- let
- val d' = d0 - precision
- val x1 = seq2bin (d_seq)
- val x2 = (fst x1 * exp2 (snd x1 - d') + 1, d') (* = seq2bin (d'::d_seq) *)
- in
- (x1, x2)
- end
- else
- approx (d::d_seq) d0 precision (q', r')
- end
-
- fun approx_start precision (q, r) =
- if q = 0 then
- ((0, 0), (0, 0))
- else
- let
- val (d, (q', r')) = find_most_significant q r
- in
- if precision <= 0 then
- let
- val x1 = seq2bin [d]
- in
- if q' = 0 then
- (x1, x1)
- else
- (x1, seq2bin [d + 1])
- end
- else
- approx [d] d precision (q', r')
- end
- in
- if 0 <= q then
- approx_start n (q,r)
- else
- let
- val ((a1,b1), (a2, b2)) = approx_start n (~ q, r)
- in
- ((~ a2, b2), (~ a1, b1))
- end
- end
-
-fun approx_decstr_by_bin n decstr =
- let
- fun str2int s = the_default 0 (Int.fromString s)
- fun signint p x = if p then x else ~ x
-
- val (p, d1, d2, ep, e) = destruct_floatstr Char.isDigit (fn e => e = #"e" orelse e = #"E") decstr
- val s = size d2
-
- val q = signint p (str2int d1 * exp10 s + str2int d2)
- val r = signint ep (str2int e) - s
- in
- approx_dec_by_bin n (q,r)
- end
-
-fun mk_float (a, b) = @{term "float"} $
- HOLogic.mk_prod (pairself (HOLogic.mk_number HOLogic.intT) (a, b));
-
-fun dest_float (Const ("Float.float", _) $ (Const (@{const_name Pair}, _) $ a $ b)) =
- pairself (snd o HOLogic.dest_number) (a, b)
- | dest_float t = ((snd o HOLogic.dest_number) t, 0);
-
-fun approx_float prec f value =
- let
- val interval = approx_decstr_by_bin prec value
- val (flower, fupper) = f interval
- in
- (mk_float flower, mk_float fupper)
- end;
-
-end;
--- a/src/HOL/Tools/hologic.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/hologic.ML Sat Mar 22 22:00:26 2014 +0100
@@ -6,8 +6,6 @@
signature HOLOGIC =
sig
- val typeS: sort
- val typeT: typ
val id_const: typ -> term
val mk_comp: term * term -> term
val boolN: string
@@ -141,12 +139,6 @@
structure HOLogic: HOLOGIC =
struct
-(* HOL syntax *)
-
-val typeS: sort = ["HOL.type"];
-val typeT = Type_Infer.anyT typeS;
-
-
(* functions *)
fun id_const T = Const ("Fun.id", T --> T);
--- a/src/HOL/Tools/inductive.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/inductive.ML Sat Mar 22 22:00:26 2014 +0100
@@ -1000,7 +1000,9 @@
cnames_syn pnames spec monos lthy =
let
val thy = Proof_Context.theory_of lthy;
- val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
+ val _ =
+ Theory.requires thy (Context.theory_name @{theory})
+ (coind_prefix coind ^ "inductive definitions");
(* abbrevs *)
--- a/src/HOL/Tools/inductive_realizer.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Sat Mar 22 22:00:26 2014 +0100
@@ -53,8 +53,8 @@
| _ => vs)) (Term.add_vars prop []) [];
val attach_typeS = map_types (map_atyps
- (fn TFree (s, []) => TFree (s, HOLogic.typeS)
- | TVar (ixn, []) => TVar (ixn, HOLogic.typeS)
+ (fn TFree (s, []) => TFree (s, @{sort type})
+ | TVar (ixn, []) => TVar (ixn, @{sort type})
| T => T));
fun dt_of_intrs thy vs nparms intrs =
--- a/src/HOL/Tools/recdef.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/recdef.ML Sat Mar 22 22:00:26 2014 +0100
@@ -180,7 +180,7 @@
(** add_recdef(_i) **)
-fun requires_recdef thy = Theory.requires thy "Old_Recdef" "recursive functions";
+fun requires_recdef thy = Theory.requires thy (Context.theory_name @{theory}) "recursive functions";
fun gen_add_recdef tfl_fn prep_att prep_hints not_permissive raw_name R eq_srcs hints thy =
let
--- a/src/HOL/Tools/record.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/record.ML Sat Mar 22 22:00:26 2014 +0100
@@ -1819,7 +1819,7 @@
val all_vars = parent_vars @ vars;
val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
- val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", HOLogic.typeS);
+ val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", @{sort type});
val moreT = TFree zeta;
val more = Free (moreN, moreT);
val full_moreN = full (Binding.name moreN);
@@ -2245,7 +2245,7 @@
fun add_record (params, binding) raw_parent raw_fields thy =
let
- val _ = Theory.requires thy "Record" "record definitions";
+ val _ = Theory.requires thy (Context.theory_name @{theory}) "record definitions";
val ctxt = Proof_Context.init_global thy;
fun cert_typ T = Type.no_tvars (Proof_Context.cert_typ ctxt T)
--- a/src/HOL/Tools/transfer.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Tools/transfer.ML Sat Mar 22 22:00:26 2014 +0100
@@ -467,7 +467,7 @@
| go _ ctxt = dummy ctxt
in
go t ctxt |> fst |> Syntax.check_term ctxt |>
- map_types (map_type_tfree (fn (a, _) => TFree (a, HOLogic.typeS)))
+ map_types (map_type_tfree (fn (a, _) => TFree (a, @{sort type})))
end
(** Monotonicity analysis **)
@@ -544,7 +544,7 @@
val relT = @{typ "bool => bool => bool"}
val idx = Thm.maxidx_of thm + 1
val thy = Proof_Context.theory_of ctxt
- fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), HOLogic.typeS)), cbool)
+ fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
in
thm
@@ -569,7 +569,7 @@
val relT = @{typ "bool => bool => bool"}
val idx = Thm.maxidx_of thm + 1
val thy = Proof_Context.theory_of ctxt
- fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), HOLogic.typeS)), cbool)
+ fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
in
thm
--- a/src/HOL/Transitive_Closure.thy Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/Transitive_Closure.thy Sat Mar 22 22:00:26 2014 +0100
@@ -1239,8 +1239,8 @@
fun decomp (@{const Trueprop} $ t) =
let fun dec (Const (@{const_name Set.member}, _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel ) =
- let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
- | decr (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+")
+ let fun decr (Const (@{const_name rtrancl}, _ ) $ r) = (r,"r*")
+ | decr (Const (@{const_name trancl}, _ ) $ r) = (r,"r+")
| decr r = (r,"r");
val (rel,r) = decr (Envir.beta_eta_contract rel);
in SOME (a,b,rel,r) end
@@ -1262,8 +1262,8 @@
fun decomp (@{const Trueprop} $ t) =
let fun dec (rel $ a $ b) =
- let fun decr (Const ("Transitive_Closure.rtranclp", _ ) $ r) = (r,"r*")
- | decr (Const ("Transitive_Closure.tranclp", _ ) $ r) = (r,"r+")
+ let fun decr (Const (@{const_name rtranclp}, _ ) $ r) = (r,"r*")
+ | decr (Const (@{const_name tranclp}, _ ) $ r) = (r,"r+")
| decr r = (r,"r");
val (rel,r) = decr rel;
in SOME (a, b, rel, r) end
--- a/src/HOL/ex/SVC_Oracle.thy Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy Sat Mar 22 22:00:26 2014 +0100
@@ -11,12 +11,12 @@
imports Main
begin
-ML_file "svc_funcs.ML"
-
consts
iff_keep :: "[bool, bool] => bool"
iff_unfold :: "[bool, bool] => bool"
+ML_file "svc_funcs.ML"
+
hide_const iff_keep iff_unfold
oracle svc_oracle = Svc.oracle
--- a/src/HOL/ex/svc_funcs.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/HOL/ex/svc_funcs.ML Sat Mar 22 22:00:26 2014 +0100
@@ -199,10 +199,10 @@
Buildin("NOT", [fm (not pos) p])
| fm pos (Const(@{const_name True}, _)) = TrueExpr
| fm pos (Const(@{const_name False}, _)) = FalseExpr
- | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) =
+ | fm pos (Const(@{const_name iff_keep}, _) $ p $ q) =
(*polarity doesn't matter*)
Buildin("=", [fm pos p, fm pos q])
- | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) =
+ | fm pos (Const(@{const_name iff_unfold}, _) $ p $ q) =
Buildin("AND", (*unfolding uses both polarities*)
[Buildin("=>", [fm (not pos) p, fm pos q]),
Buildin("=>", [fm (not pos) q, fm pos p])])
--- a/src/Pure/ML/ml_antiquotations.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML Sat Mar 22 22:00:26 2014 +0100
@@ -121,9 +121,9 @@
else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
ML_Antiquotation.inline @{binding const}
- (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional
+ (Args.context -- Scan.lift (Parse.position Args.name_inner_syntax) -- Scan.optional
(Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
- >> (fn ((ctxt, raw_c), Ts) =>
+ >> (fn ((ctxt, (raw_c, pos)), Ts) =>
let
val Const (c, _) =
Proof_Context.read_const {proper = true, strict = true} ctxt raw_c;
@@ -131,7 +131,7 @@
val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
val _ = length Ts <> n andalso
error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
- quote c ^ enclose "(" ")" (commas (replicate n "_")));
+ quote c ^ enclose "(" ")" (commas (replicate n "_")) ^ Position.here pos);
val const = Const (c, Consts.instance consts (c, Ts));
in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
--- a/src/ZF/OrdQuant.thy Sat Mar 22 08:37:43 2014 +0100
+++ b/src/ZF/OrdQuant.thy Sat Mar 22 22:00:26 2014 +0100
@@ -357,9 +357,8 @@
ML
{*
val Ord_atomize =
- atomize ([("OrdQuant.oall", [@{thm ospec}]),("OrdQuant.rall", [@{thm rspec}])]@
- ZF_conn_pairs,
- ZF_mem_pairs);
+ atomize ([(@{const_name oall}, @{thms ospec}), (@{const_name rall}, @{thms rspec})] @
+ ZF_conn_pairs, ZF_mem_pairs);
*}
declaration {* fn _ =>
Simplifier.map_ss (Simplifier.set_mksimps (K (map mk_eq o Ord_atomize o gen_all)))
--- a/src/ZF/Tools/datatype_package.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/ZF/Tools/datatype_package.ML Sat Mar 22 22:00:26 2014 +0100
@@ -65,7 +65,7 @@
fun add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy =
let
val dummy = (*has essential ancestors?*)
- Theory.requires thy "Datatype_ZF" "(co)datatype definitions";
+ Theory.requires thy (Context.theory_name @{theory}) "(co)datatype definitions";
val rec_hds = map head_of rec_tms;
--- a/src/ZF/Tools/inductive_package.ML Sat Mar 22 08:37:43 2014 +0100
+++ b/src/ZF/Tools/inductive_package.ML Sat Mar 22 22:00:26 2014 +0100
@@ -59,7 +59,7 @@
fun add_inductive_i verbose (rec_tms, dom_sum)
raw_intr_specs (monos, con_defs, type_intrs, type_elims) thy =
let
- val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions";
+ val _ = Theory.requires thy (Context.theory_name @{theory}) "(co)inductive definitions";
val ctxt = Proof_Context.init_global thy;
val intr_specs = map (apfst (apfst Binding.name_of)) raw_intr_specs;