some theorems named explicitly
authorhaftmann
Mon Mar 10 21:51:45 2008 +0100 (2008-03-10)
changeset 26247b6608fbeaae1
parent 26246 e212c22f35c2
child 26248 f2cd4bf1e404
some theorems named explicitly
src/Pure/Isar/class.ML
     1.1 --- a/src/Pure/Isar/class.ML	Mon Mar 10 21:51:44 2008 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Mon Mar 10 21:51:45 2008 +0100
     1.3 @@ -8,9 +8,9 @@
     1.4  signature CLASS =
     1.5  sig
     1.6    (*classes*)
     1.7 -  val class: bstring -> class list -> Element.context_i Locale.element list
     1.8 +  val class: bstring -> class list -> Element.context_i list
     1.9      -> string list -> theory -> string * Proof.context
    1.10 -  val class_cmd: bstring -> xstring list -> Element.context Locale.element list
    1.11 +  val class_cmd: bstring -> xstring list -> Element.context list
    1.12      -> xstring list -> theory -> string * Proof.context
    1.13  
    1.14    val init: class -> theory -> Proof.context
    1.15 @@ -30,9 +30,12 @@
    1.16    val print_classes: theory -> unit
    1.17  
    1.18    (*instances*)
    1.19 -  val init_instantiation: string list * (string * sort) list * sort -> theory -> local_theory
    1.20 -  val instantiation_instance: (local_theory -> local_theory) -> local_theory -> Proof.state
    1.21 -  val prove_instantiation_instance: (Proof.context -> tactic) -> local_theory -> local_theory
    1.22 +  val init_instantiation: string list * (string * sort) list * sort
    1.23 +    -> theory -> local_theory
    1.24 +  val instantiation_instance: (local_theory -> local_theory)
    1.25 +    -> local_theory -> Proof.state
    1.26 +  val prove_instantiation_instance: (Proof.context -> tactic)
    1.27 +    -> local_theory -> local_theory
    1.28    val conclude_instantiation: local_theory -> local_theory
    1.29    val instantiation_param: local_theory -> string -> string option
    1.30    val confirm_declaration: string -> local_theory -> local_theory
    1.31 @@ -266,7 +269,7 @@
    1.32  
    1.33  val class_prefix = Logic.const_of_class o Sign.base_name;
    1.34  
    1.35 -fun calculate thy sups base_sort assm_axiom param_map class =
    1.36 +fun calculate sups base_sort assm_axiom param_map class thy =
    1.37    let
    1.38      (*static parts of morphism*)
    1.39      val subst_typ = map_atyps (fn TFree (v, sort) =>
    1.40 @@ -311,10 +314,10 @@
    1.41        |> Option.map instantiate_base_sort
    1.42        |> Option.map (MetaSimplifier.rewrite_rule defs)
    1.43        |> Option.map Goal.close_result;
    1.44 +    val class_intro = (#intro o AxClass.get_info thy) class;
    1.45      val fixate = Thm.instantiate
    1.46        (map (pairself (Thm.ctyp_of thy)) [(TVar ((Name.aT, 0), []), TFree (Name.aT, base_sort)),
    1.47          (TVar ((Name.aT, 0), base_sort), TFree (Name.aT, base_sort))], [])
    1.48 -    val class_intro = (fixate o #intro o AxClass.get_info thy) class;
    1.49      val of_class_sups = if null sups
    1.50        then map (fixate o Thm.class_triv thy) base_sort
    1.51        else map (fixate o #of_class o the_class_data thy) sups;
    1.52 @@ -328,10 +331,18 @@
    1.53          |> (map_types o map_atyps o K) (TFree (Name.aT, base_sort))
    1.54          |> (Thm.assume o Thm.cterm_of thy)
    1.55          |> replicate num_trivs;
    1.56 -    val of_class = (class_intro OF of_class_sups OF locale_dests OF pred_trivs)
    1.57 +    val of_class = (fixate class_intro OF of_class_sups OF locale_dests OF pred_trivs)
    1.58        |> Drule.standard'
    1.59        |> Goal.close_result;
    1.60 -  in (morphism, axiom, assm_intro, of_class) end;
    1.61 +    val this_intro = assm_intro |> the_default class_intro;
    1.62 +  in
    1.63 +    thy
    1.64 +    |> Sign.sticky_prefix (class_prefix class ^ "_" ^ AxClass.axiomsN)
    1.65 +    |> PureThy.note Thm.internalK (AxClass.introN, this_intro)
    1.66 +    |> snd
    1.67 +    |> Sign.restore_naming thy
    1.68 +    |> pair (morphism, axiom, assm_intro, of_class)
    1.69 +  end;
    1.70  
    1.71  fun class_interpretation class facts defs thy =
    1.72    let
    1.73 @@ -423,14 +434,8 @@
    1.74      ctxt
    1.75      |> fold declare_const local_constraints
    1.76      |> fold (ProofContext.add_const_constraint o apsnd SOME) local_constraints
    1.77 -    |> Overloading.map_improvable_syntax (K {
    1.78 -        local_constraints = local_constraints,
    1.79 -        global_constraints = global_constraints,
    1.80 -        improve = improve,
    1.81 -        subst = subst,
    1.82 -        unchecks = unchecks,
    1.83 -        passed = false
    1.84 -      })
    1.85 +    |> Overloading.map_improvable_syntax (K (((local_constraints, global_constraints),
    1.86 +        ((improve, subst), unchecks)), false))
    1.87    end;
    1.88  
    1.89  fun refresh_syntax class ctxt =
    1.90 @@ -456,7 +461,7 @@
    1.91  
    1.92  local
    1.93  
    1.94 -fun gen_class_spec prep_class prep_expr process_expr thy raw_supclasses raw_includes_elems =
    1.95 +fun gen_class_spec prep_class process_expr thy raw_supclasses raw_elems =
    1.96    let
    1.97      val supclasses = map (prep_class thy) raw_supclasses;
    1.98      val supsort = Sign.minimize_sort thy supclasses;
    1.99 @@ -465,11 +470,9 @@
   1.100        foldr1 (Sorts.inter_sort (Sign.classes_of thy))
   1.101          (map (#base_sort o the_class_data thy) sups);
   1.102      val suplocales = map Locale.Locale sups;
   1.103 -    val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
   1.104 -      | Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []);
   1.105      val supexpr = Locale.Merge suplocales;
   1.106      val supparams = (map fst o Locale.parameters_of_expr thy) supexpr;
   1.107 -    val mergeexpr = Locale.Merge (suplocales @ includes);
   1.108 +    val mergeexpr = Locale.Merge (suplocales);
   1.109      val constrain = Element.Constrains ((map o apsnd o map_atyps)
   1.110        (K (TFree (Name.aT, base_sort))) supparams);
   1.111      fun fork_syn (Element.Fixes xs) =
   1.112 @@ -479,7 +482,7 @@
   1.113      fun fork_syntax elems =
   1.114        let
   1.115          val (elems', global_syntax) = fold_map fork_syn elems [];
   1.116 -      in (if null includes (*FIXME*) then constrain :: elems' else elems', global_syntax) end;
   1.117 +      in (constrain :: elems', global_syntax) end;
   1.118      val (elems, global_syntax) =
   1.119        ProofContext.init thy
   1.120        |> Locale.cert_expr supexpr [constrain]
   1.121 @@ -490,8 +493,8 @@
   1.122        |> fork_syntax
   1.123    in (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) end;
   1.124  
   1.125 -val read_class_spec = gen_class_spec Sign.intern_class Locale.intern_expr Locale.read_expr;
   1.126 -val check_class_spec = gen_class_spec (K I) (K I) Locale.cert_expr;
   1.127 +val read_class_spec = gen_class_spec Sign.intern_class Locale.read_expr;
   1.128 +val check_class_spec = gen_class_spec (K I) Locale.cert_expr;
   1.129  
   1.130  fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax other_consts thy =
   1.131    let
   1.132 @@ -540,11 +543,11 @@
   1.133    end;
   1.134  
   1.135  fun gen_class prep_spec prep_param bname
   1.136 -    raw_supclasses raw_includes_elems raw_other_consts thy =
   1.137 +    raw_supclasses raw_elems raw_other_consts thy =
   1.138    let
   1.139      val class = Sign.full_name thy bname;
   1.140      val (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) =
   1.141 -      prep_spec thy raw_supclasses raw_includes_elems;
   1.142 +      prep_spec thy raw_supclasses raw_elems;
   1.143      val other_consts = map (tap (Sign.the_const_type thy) o prep_param thy) raw_other_consts;
   1.144    in
   1.145      thy
   1.146 @@ -553,7 +556,7 @@
   1.147      |> ProofContext.theory_of
   1.148      |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax other_consts
   1.149      |-> (fn (param_map, params, assm_axiom) =>
   1.150 -         `(fn thy => calculate thy sups base_sort assm_axiom param_map class)
   1.151 +        calculate sups base_sort assm_axiom param_map class
   1.152      #-> (fn (morphism, axiom, assm_intro, of_class) =>
   1.153          add_class_data ((class, sups), (params, base_sort,
   1.154            map snd param_map, morphism, axiom, assm_intro, of_class))
   1.155 @@ -586,7 +589,7 @@
   1.156      val ty' = Term.fastype_of dict_def;
   1.157      val ty'' = Type.strip_sorts ty';
   1.158      val def_eq = Logic.mk_equals (Const (c', ty'), dict_def);
   1.159 -    fun get_axiom thy = ((Thm.varifyT o Thm.symmetric o Thm.get_axiom_i thy) c', thy);
   1.160 +    fun get_axiom thy = ((Thm.varifyT o Thm.get_axiom_i thy) c', thy);
   1.161    in
   1.162      thy'
   1.163      |> Sign.declare_const pos (c, ty'', mx) |> snd
   1.164 @@ -594,7 +597,9 @@
   1.165      |>> Thm.symmetric
   1.166      ||>> get_axiom
   1.167      |-> (fn (def, def') => class_interpretation class [def] [Thm.prop_of def]
   1.168 -          #> register_operation class (c', (dict', SOME def')))
   1.169 +      #> register_operation class (c', (dict', SOME (Thm.symmetric def')))
   1.170 +      #> PureThy.note Thm.internalK (c, def')
   1.171 +      #> snd)
   1.172      |> Sign.restore_naming thy
   1.173      |> Sign.add_const_constraint (c', SOME ty')
   1.174    end;
   1.175 @@ -688,14 +693,8 @@
   1.176    in
   1.177      ctxt
   1.178      |> fold (ProofContext.add_const_constraint o apsnd SOME) local_constraints
   1.179 -    |> Overloading.map_improvable_syntax (K {
   1.180 -        local_constraints = local_constraints,
   1.181 -        global_constraints = global_constraints,
   1.182 -        improve = improve,
   1.183 -        subst = subst,
   1.184 -        unchecks = unchecks,
   1.185 -        passed = false
   1.186 -      })
   1.187 +    |> Overloading.map_improvable_syntax (K (((local_constraints, global_constraints),
   1.188 +        ((improve, subst), unchecks)), false))
   1.189    end;
   1.190  
   1.191