# HG changeset patch # User haftmann # Date 1270997496 -7200 # Node ID 853c777f29074c62ca7a7a5d4def25e6c48fff0b # Parent 03aa51cf85a2e659b29459baff231e324f3f45d0# Parent 7fa17a225852db0672ddf20474dc12bc38588fae merged diff -r 7fa17a225852 -r 853c777f2907 src/HOL/Tools/Quotient/quotient_def.ML --- 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 diff -r 7fa17a225852 -r 853c777f2907 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- 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 diff -r 7fa17a225852 -r 853c777f2907 src/HOL/Tools/typedef.ML --- 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, diff -r 7fa17a225852 -r 853c777f2907 src/Pure/Isar/class_target.ML --- 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') diff -r 7fa17a225852 -r 853c777f2907 src/Pure/Isar/overloading.ML --- 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 diff -r 7fa17a225852 -r 853c777f2907 src/Pure/Isar/specification.ML --- 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 diff -r 7fa17a225852 -r 853c777f2907 src/Pure/Isar/theory_target.ML --- 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, diff -r 7fa17a225852 -r 853c777f2907 src/Pure/axclass.ML --- 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 diff -r 7fa17a225852 -r 853c777f2907 src/Pure/more_thm.ML --- 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; diff -r 7fa17a225852 -r 853c777f2907 src/Pure/pure_thy.ML --- 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 diff -r 7fa17a225852 -r 853c777f2907 src/Pure/sorts.ML --- 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; diff -r 7fa17a225852 -r 853c777f2907 src/Tools/Code/code_preproc.ML --- 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; diff -r 7fa17a225852 -r 853c777f2907 src/Tools/Code/code_thingol.ML --- 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;