--- a/src/HOL/Tools/Quotient/quotient_def.ML Sun Apr 11 16:51:07 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Sun Apr 11 16:51:36 2010 +0200
@@ -64,7 +64,7 @@
val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
val (_, prop') = Local_Defs.cert_def lthy prop
- val (_, newrhs) = Primitive_Defs.abs_def prop'
+ val (_, newrhs) = Local_Defs.abs_def prop'
val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sun Apr 11 16:51:07 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sun Apr 11 16:51:36 2010 +0200
@@ -91,7 +91,7 @@
val (c, thy') =
Sign.declare_const ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
val cdef = cname ^ "_def"
- val (ax, thy'') =
+ val ((_, ax), thy'') =
Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy'
val ax' = Drule.export_without_context ax
in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy'') end
--- a/src/HOL/Tools/typedef.ML Sun Apr 11 16:51:07 2010 +0200
+++ b/src/HOL/Tools/typedef.ML Sun Apr 11 16:51:36 2010 +0200
@@ -8,7 +8,7 @@
signature TYPEDEF =
sig
type info =
- {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string} *
+ {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, axiom_name: string} *
{inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
Rep_induct: thm, Abs_induct: thm}
@@ -36,7 +36,7 @@
type info =
(*global part*)
- {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string} *
+ {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, axiom_name: string} *
(*local part*)
{inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
@@ -117,12 +117,12 @@
val typedef_deps = Term.add_consts A [];
- val (axiom, axiom_thy) = consts_thy
+ val ((axiom_name, axiom), axiom_thy) = consts_thy
|> Thm.add_axiom (typedef_name, mk_typedef newT oldT RepC AbsC A)
||> Theory.add_deps "" (dest_Const RepC) typedef_deps
||> Theory.add_deps "" (dest_Const AbsC) typedef_deps;
- in ((RepC, AbsC, axiom), axiom_thy) end;
+ in ((RepC, AbsC, axiom_name, axiom), axiom_thy) end;
(* prepare_typedef *)
@@ -177,20 +177,20 @@
val typedef_name = Binding.prefix_name "type_definition_" name;
- val ((RepC, AbsC, typedef), typedef_lthy) =
+ val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) =
let
val thy = ProofContext.theory_of set_lthy;
val cert = Thm.cterm_of thy;
val (defs, A) =
Local_Defs.export_cterm set_lthy (ProofContext.init thy) (cert set') ||> Thm.term_of;
- val ((RepC, AbsC, axiom), axiom_lthy) = set_lthy |>
+ val ((RepC, AbsC, axiom_name, axiom), axiom_lthy) = set_lthy |>
Local_Theory.theory_result (primitive_typedef typedef_name newT oldT Rep_name Abs_name A);
val cert = Thm.cterm_of (ProofContext.theory_of axiom_lthy);
val typedef =
Local_Defs.contract axiom_lthy defs (cert (mk_typedef newT oldT RepC AbsC set')) axiom;
- in ((RepC, AbsC, typedef), axiom_lthy) end;
+ in ((RepC, AbsC, axiom_name, typedef), axiom_lthy) end;
val alias_lthy = typedef_lthy
|> Local_Theory.const_alias Rep_name (#1 (Term.dest_Const RepC))
@@ -236,8 +236,8 @@
make @{thm type_definition.Abs_induct});
val info =
- ({rep_type = oldT, abs_type = newT,
- Rep_name = #1 (Term.dest_Const RepC), Abs_name = #1 (Term.dest_Const AbsC)},
+ ({rep_type = oldT, abs_type = newT, Rep_name = #1 (Term.dest_Const RepC),
+ Abs_name = #1 (Term.dest_Const AbsC), axiom_name = axiom_name},
{inhabited = inhabited, type_definition = type_definition, set_def = set_def,
Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
--- a/src/Pure/Isar/class_target.ML Sun Apr 11 16:51:07 2010 +0200
+++ b/src/Pure/Isar/class_target.ML Sun Apr 11 16:51:36 2010 +0200
@@ -333,8 +333,8 @@
|> Sign.declare_const ((b, Type.strip_sorts ty'), mx)
|> snd
|> Thm.add_def false false (b_def, def_eq)
- |>> Thm.varifyT_global
- |-> (fn def_thm => PureThy.store_thm (b_def, def_thm)
+ |>> apsnd Thm.varifyT_global
+ |-> (fn (_, def_thm) => PureThy.store_thm (b_def, def_thm)
#> snd
#> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
|> Sign.add_const_constraint (c', SOME ty')
--- a/src/Pure/Isar/overloading.ML Sun Apr 11 16:51:07 2010 +0200
+++ b/src/Pure/Isar/overloading.ML Sun Apr 11 16:51:36 2010 +0200
@@ -165,8 +165,9 @@
fun declare c_ty = pair (Const c_ty);
-fun define checked b (c, t) = Thm.add_def (not checked) true
- (b, Logic.mk_equals (Const (c, Term.fastype_of t), t));
+fun define checked b (c, t) =
+ Thm.add_def (not checked) true (b, Logic.mk_equals (Const (c, Term.fastype_of t), t))
+ #>> snd;
fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
#> Local_Theory.target synchronize_syntax
--- a/src/Pure/Isar/specification.ML Sun Apr 11 16:51:07 2010 +0200
+++ b/src/Pure/Isar/specification.ML Sun Apr 11 16:51:36 2010 +0200
@@ -173,7 +173,7 @@
fold_map Thm.add_axiom
(map (apfst (fn a => Binding.map_name (K a) b))
(PureThy.name_multi (Name.of_binding b) (map subst props)))
- #>> (fn ths => ((b, atts), [(ths, [])])));
+ #>> (fn ths => ((b, atts), [(map #2 ths, [])])));
(*facts*)
val (facts, facts_lthy) = axioms_thy
--- a/src/Pure/Isar/theory_target.ML Sun Apr 11 16:51:07 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML Sun Apr 11 16:51:36 2010 +0200
@@ -315,7 +315,7 @@
| NONE =>
if is_some (Class_Target.instantiation_param lthy b)
then AxClass.define_overloaded name' (head, rhs')
- else Thm.add_def false false (name', Logic.mk_equals (lhs', rhs')));
+ else Thm.add_def false false (name', Logic.mk_equals (lhs', rhs')) #>> snd);
val def = Local_Defs.trans_terms lthy3
[(*c == global.c xs*) local_def,
(*global.c xs == rhs'*) global_def,
--- a/src/Pure/axclass.ML Sun Apr 11 16:51:07 2010 +0200
+++ b/src/Pure/axclass.ML Sun Apr 11 16:51:36 2010 +0200
@@ -306,11 +306,11 @@
|-> (fn const' as Const (c'', _) =>
Thm.add_def false true
(Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
- #>> Thm.varifyT_global
- #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
- #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
- #> snd
- #> pair (Const (c, T))))
+ #>> apsnd Thm.varifyT_global
+ #-> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm)
+ #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
+ #> snd
+ #> pair (Const (c, T))))
||> Sign.restore_naming thy
end;
@@ -325,7 +325,7 @@
in
thy
|> Thm.add_def false false (b', prop)
- |>> (fn thm => Drule.transitive_thm OF [eq, thm])
+ |>> (fn (_, thm) => Drule.transitive_thm OF [eq, thm])
end;
@@ -515,7 +515,7 @@
fun add_axiom (b, prop) =
Thm.add_axiom (b, prop) #->
- (fn thm => PureThy.add_thm ((b, Drule.export_without_context thm), []));
+ (fn (_, thm) => PureThy.add_thm ((b, Drule.export_without_context thm), []));
fun axiomatize prep mk name add raw_args thy =
let
--- a/src/Pure/more_thm.ML Sun Apr 11 16:51:07 2010 +0200
+++ b/src/Pure/more_thm.ML Sun Apr 11 16:51:36 2010 +0200
@@ -62,8 +62,8 @@
val forall_intr_frees: thm -> thm
val unvarify_global: thm -> thm
val close_derivation: thm -> thm
- val add_axiom: binding * term -> theory -> thm * theory
- val add_def: bool -> bool -> binding * term -> theory -> thm * theory
+ val add_axiom: binding * term -> theory -> (string * thm) * theory
+ val add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory
type binding = binding * attribute list
val empty_binding: binding
val rule_attribute: (Context.generic -> thm -> thm) -> attribute
@@ -347,31 +347,36 @@
fun add_axiom (b, prop) thy =
let
val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
+
val _ = Sign.no_vars (Syntax.pp_global thy) prop;
val (strip, recover, prop') = stripped_sorts thy prop;
val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
+
val thy' =
Theory.add_axiom (b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop')) thy;
- val axm' = Thm.axiom thy' (Sign.full_name thy' b');
+ val axm_name = Sign.full_name thy' b';
+ val axm' = Thm.axiom thy' axm_name;
val thm =
Thm.instantiate (recover, []) axm'
|> unvarify_global
|> fold elim_implies of_sorts;
- in (thm, thy') end;
+ in ((axm_name, thm), thy') end;
fun add_def unchecked overloaded (b, prop) thy =
let
val _ = Sign.no_vars (Syntax.pp_global thy) prop;
val prems = map (Thm.cterm_of thy) (Logic.strip_imp_prems prop);
val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
+
val thy' = Theory.add_def unchecked overloaded (b, concl') thy;
- val axm' = Thm.axiom thy' (Sign.full_name thy' b);
+ val axm_name = Sign.full_name thy' b;
+ val axm' = Thm.axiom thy' axm_name;
val thm =
Thm.instantiate (recover, []) axm'
|> unvarify_global
|> fold_rev Thm.implies_intr prems;
- in (thm, thy') end;
+ in ((axm_name, thm), thy') end;
--- a/src/Pure/pure_thy.ML Sun Apr 11 16:51:07 2010 +0200
+++ b/src/Pure/pure_thy.ML Sun Apr 11 16:51:36 2010 +0200
@@ -210,7 +210,7 @@
fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
let
val prop = prep thy (b, raw_prop);
- val (def, thy') = Thm.add_def unchecked overloaded (b, prop) thy;
+ val ((_, def), thy') = Thm.add_def unchecked overloaded (b, prop) thy;
val thm = def
|> Thm.forall_intr_frees
|> Thm.forall_elim_vars 0
--- a/src/Pure/sorts.ML Sun Apr 11 16:51:07 2010 +0200
+++ b/src/Pure/sorts.ML Sun Apr 11 16:51:36 2010 +0200
@@ -57,8 +57,8 @@
val meet_sort_typ: algebra -> typ * sort -> typ -> typ (*exception CLASS_ERROR*)
val of_sort: algebra -> typ * sort -> bool
val of_sort_derivation: algebra ->
- {class_relation: 'a * class -> class -> 'a,
- type_constructor: string -> ('a * class) list list -> class -> 'a,
+ {class_relation: typ -> 'a * class -> class -> 'a,
+ type_constructor: string * typ list -> ('a * class) list list -> class -> 'a,
type_variable: typ -> ('a * class) list} ->
typ * sort -> 'a list (*exception CLASS_ERROR*)
val classrel_derivation: algebra ->
@@ -335,15 +335,15 @@
(* errors -- performance tuning via delayed message composition *)
datatype class_error =
- NoClassrel of class * class |
- NoArity of string * class |
- NoSubsort of sort * sort;
+ No_Classrel of class * class |
+ No_Arity of string * class |
+ No_Subsort of sort * sort;
-fun class_error pp (NoClassrel (c1, c2)) =
+fun class_error pp (No_Classrel (c1, c2)) =
"No class relation " ^ Pretty.string_of_classrel pp [c1, c2]
- | class_error pp (NoArity (a, c)) =
+ | class_error pp (No_Arity (a, c)) =
"No type arity " ^ Pretty.string_of_arity pp (a, [], [c])
- | class_error pp (NoSubsort (S1, S2)) =
+ | class_error pp (No_Subsort (S1, S2)) =
"Cannot derive subsort relation " ^ Pretty.string_of_sort pp S1
^ " < " ^ Pretty.string_of_sort pp S2;
@@ -357,7 +357,7 @@
val arities = arities_of algebra;
fun dom c =
(case AList.lookup (op =) (Symtab.lookup_list arities a) c of
- NONE => raise CLASS_ERROR (NoArity (a, c))
+ NONE => raise CLASS_ERROR (No_Arity (a, c))
| SOME (_, Ss) => Ss);
fun dom_inter c Ss = ListPair.map (inter_sort algebra) (dom c, Ss);
in
@@ -375,7 +375,7 @@
fun meet _ [] = I
| meet (TFree (_, S)) S' =
if sort_le algebra (S, S') then I
- else raise CLASS_ERROR (NoSubsort (S, S'))
+ else raise CLASS_ERROR (No_Subsort (S, S'))
| meet (TVar (v, S)) S' =
if sort_le algebra (S, S') then I
else Vartab.map_default (v, S) (inters S')
@@ -410,25 +410,30 @@
let
val arities = arities_of algebra;
- fun weaken S1 S2 = S2 |> map (fn c2 =>
- (case S1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of
- SOME d1 => class_relation d1 c2
- | NONE => raise CLASS_ERROR (NoSubsort (map #2 S1, S2))));
+ fun weaken T D1 S2 =
+ let val S1 = map snd D1 in
+ if S1 = S2 then map fst D1
+ else
+ S2 |> map (fn c2 =>
+ (case D1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of
+ SOME d1 => class_relation T d1 c2
+ | NONE => raise CLASS_ERROR (No_Subsort (S1, S2))))
+ end;
- fun derive _ [] = []
- | derive (Type (a, Ts)) S =
+ fun derive (_, []) = []
+ | derive (T as Type (a, Us), S) =
let
val Ss = mg_domain algebra a S;
- val dom = map2 (fn T => fn S => derive T S ~~ S) Ts Ss;
+ val dom = map2 (fn U => fn S => derive (U, S) ~~ S) Us Ss;
in
S |> map (fn c =>
let
val (c0, Ss') = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
- val dom' = map2 (fn d => fn S' => weaken d S' ~~ S') dom Ss';
- in class_relation (type_constructor a dom' c0, c0) c end)
+ val dom' = map (fn ((U, d), S') => weaken U d S' ~~ S') ((Us ~~ dom) ~~ Ss');
+ in class_relation T (type_constructor (a, Us) dom' c0, c0) c end)
end
- | derive T S = weaken (type_variable T) S;
- in uncurry derive end;
+ | derive (T, S) = weaken T (type_variable T) S;
+ in derive end;
fun classrel_derivation algebra class_relation =
let
@@ -437,7 +442,7 @@
in
fn (x, c1) => fn c2 =>
(case Graph.irreducible_paths (classes_of algebra) (c1, c2) of
- [] => raise CLASS_ERROR (NoClassrel (c1, c2))
+ [] => raise CLASS_ERROR (No_Classrel (c1, c2))
| cs :: _ => path (x, cs))
end;
--- a/src/Tools/Code/code_preproc.ML Sun Apr 11 16:51:07 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML Sun Apr 11 16:51:36 2010 +0200
@@ -365,13 +365,13 @@
fun dicts_of thy (proj_sort, algebra) (T, sort) =
let
fun class_relation (x, _) _ = x;
- fun type_constructor tyco xs class =
+ fun type_constructor (tyco, _) xs class =
inst_params thy tyco (Sorts.complete_sort algebra [class])
@ (maps o maps) fst xs;
fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
in
flat (Sorts.of_sort_derivation algebra
- { class_relation = class_relation, type_constructor = type_constructor,
+ { class_relation = K class_relation, type_constructor = type_constructor,
type_variable = type_variable } (T, proj_sort sort)
handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
end;
--- a/src/Tools/Code/code_thingol.ML Sun Apr 11 16:51:07 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML Sun Apr 11 16:51:36 2010 +0200
@@ -767,14 +767,14 @@
Global ((class, tyco), yss)
| class_relation (Local (classrels, v), subclass) superclass =
Local ((subclass, superclass) :: classrels, v);
- fun type_constructor tyco yss class =
+ fun type_constructor (tyco, _) yss class =
Global ((class, tyco), (map o map) fst yss);
fun type_variable (TFree (v, sort)) =
let
val sort' = proj_sort sort;
in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
val typargs = Sorts.of_sort_derivation algebra
- {class_relation = Sorts.classrel_derivation algebra class_relation,
+ {class_relation = K (Sorts.classrel_derivation algebra class_relation),
type_constructor = type_constructor,
type_variable = type_variable} (ty, proj_sort sort)
handle Sorts.CLASS_ERROR e => not_wellsorted thy some_thm ty sort e;