src/Pure/Isar/class.ML
author haftmann
Sun Jan 18 10:11:12 2009 +0100 (2009-01-18)
changeset 29547 f2587922591e
parent 29526 0b32c8b84d3e
child 29558 9846af6c6d6a
permissions -rw-r--r--
improved calculation of morphisms and rules
haftmann@29358
     1
(*  Title:      Pure/Isar/ML
haftmann@24218
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@24218
     3
haftmann@29358
     4
Type classes derived from primitive axclasses and locales - interfaces
haftmann@24218
     5
*)
haftmann@24218
     6
haftmann@24218
     7
signature CLASS =
haftmann@24218
     8
sig
haftmann@29358
     9
  include CLASS_TARGET
haftmann@29439
    10
    (*FIXME the split into class_target.ML, theory_target.ML and
haftmann@29439
    11
      class.ML is artificial*)
haftmann@29358
    12
haftmann@26247
    13
  val class: bstring -> class list -> Element.context_i list
haftmann@29378
    14
    -> theory -> string * local_theory
haftmann@26247
    15
  val class_cmd: bstring -> xstring list -> Element.context list
haftmann@29378
    16
    -> theory -> string * local_theory
haftmann@29358
    17
  val prove_subclass: tactic -> class -> local_theory -> local_theory
haftmann@29358
    18
  val subclass: class -> local_theory -> Proof.state
haftmann@29358
    19
  val subclass_cmd: xstring -> local_theory -> Proof.state
haftmann@24218
    20
end;
haftmann@24218
    21
haftmann@24218
    22
structure Class : CLASS =
haftmann@24218
    23
struct
haftmann@24218
    24
haftmann@29358
    25
open Class_Target;
haftmann@28715
    26
haftmann@29358
    27
(** define classes **)
haftmann@24218
    28
haftmann@24218
    29
local
haftmann@24218
    30
haftmann@29547
    31
fun calculate thy class sups base_sort param_map assm_axiom =
haftmann@29547
    32
  let
haftmann@29547
    33
    val empty_ctxt = ProofContext.init thy;
haftmann@29547
    34
haftmann@29547
    35
    (* instantiation of canonical interpretation *)
haftmann@29547
    36
    (*FIXME inst_morph should be calculated manually and not instantiate constraint*)
haftmann@29547
    37
    val aT = TFree ("'a", base_sort);
haftmann@29547
    38
    val (([props], [(_, inst_morph)], export_morph), _) = empty_ctxt
haftmann@29547
    39
      |> Expression.cert_goal_expression ([(class, (("", false),
haftmann@29547
    40
           Expression.Named ((map o apsnd) Const param_map)))], []);
haftmann@29547
    41
haftmann@29547
    42
    (* witness for canonical interpretation *)
haftmann@29547
    43
    val prop = try the_single props;
haftmann@29547
    44
    val wit = Option.map (fn prop => let
haftmann@29547
    45
        val sup_axioms = map_filter (fst o rules thy) sups;
haftmann@29547
    46
        val loc_intro_tac = case Locale.intros_of thy class
haftmann@29547
    47
          of (_, NONE) => all_tac
haftmann@29547
    48
           | (_, SOME intro) => ALLGOALS (Tactic.rtac intro);
haftmann@29547
    49
        val tac = loc_intro_tac
haftmann@29547
    50
          THEN ALLGOALS (ProofContext.fact_tac (sup_axioms @ the_list assm_axiom))
haftmann@29547
    51
      in Element.prove_witness empty_ctxt prop tac end) prop;
haftmann@29547
    52
    val axiom = Option.map Element.conclude_witness wit;
haftmann@29547
    53
haftmann@29547
    54
    (* canonical interpretation *)
haftmann@29547
    55
    val base_morph = inst_morph
haftmann@29547
    56
      $> Morphism.binding_morphism
haftmann@29547
    57
           (Binding.add_prefix false (class_prefix class))
haftmann@29547
    58
      $> Element.satisfy_morphism (the_list wit);
haftmann@29547
    59
    val defs = these_defs thy sups;
haftmann@29547
    60
    val eq_morph = Element.eq_morphism thy defs;
haftmann@29547
    61
    val morph = base_morph $> eq_morph;
haftmann@29547
    62
haftmann@29547
    63
    (* assm_intro *)
haftmann@29547
    64
    fun prove_assm_intro thm = 
haftmann@29547
    65
      let
haftmann@29547
    66
        val prop = thm |> Thm.prop_of |> Logic.unvarify
haftmann@29547
    67
          |> Morphism.term (inst_morph $> eq_morph) 
haftmann@29547
    68
          |> (map_types o map_atyps) (K aT);
haftmann@29547
    69
        fun tac ctxt = LocalDefs.unfold_tac ctxt (map Thm.symmetric defs) (*FIXME*)
haftmann@29547
    70
          THEN ALLGOALS (ProofContext.fact_tac [thm]);
haftmann@29547
    71
      in Goal.prove_global thy [] [] prop (tac o #context) end;
haftmann@29547
    72
    val assm_intro = Option.map prove_assm_intro
haftmann@29547
    73
      (fst (Locale.intros_of thy class));
haftmann@29547
    74
haftmann@29547
    75
    (* of_class *)
haftmann@29547
    76
    val of_class_prop_concl = Logic.mk_inclass (aT, class);
haftmann@29547
    77
    val of_class_prop = case prop of NONE => of_class_prop_concl
haftmann@29547
    78
      | SOME prop => Logic.mk_implies (Morphism.term inst_morph prop,
haftmann@29547
    79
          of_class_prop_concl) |> (map_types o map_atyps) (K aT)
haftmann@29547
    80
    val sup_of_classes = map (snd o rules thy) sups;
haftmann@29547
    81
    val loc_axiom_intros = map Drule.standard' (Locale.axioms_of thy class);
haftmann@29547
    82
    val axclass_intro = #intro (AxClass.get_info thy class);
haftmann@29547
    83
    val base_sort_trivs = Drule.sort_triv thy (aT, base_sort);
haftmann@29547
    84
    val tac = REPEAT (SOMEGOAL
haftmann@29547
    85
      (Tactic.match_tac (axclass_intro :: sup_of_classes
haftmann@29547
    86
         @ loc_axiom_intros @ base_sort_trivs)
haftmann@29547
    87
           ORELSE' Tactic.assume_tac));
haftmann@29547
    88
    val of_class = Goal.prove_global thy [] [] of_class_prop (K tac);
haftmann@29547
    89
haftmann@29547
    90
  in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end;
haftmann@29547
    91
haftmann@29509
    92
fun gen_class_spec prep_class process_decl thy raw_supclasses raw_elems =
haftmann@24218
    93
  let
haftmann@29526
    94
    (*FIXME 2009 simplify*)
haftmann@24748
    95
    val supclasses = map (prep_class thy) raw_supclasses;
haftmann@24748
    96
    val supsort = Sign.minimize_sort thy supclasses;
haftmann@29547
    97
    val (sups, bases) = List.partition (is_class thy) supsort;
haftmann@29509
    98
    val base_sort = if null sups then supsort else
haftmann@29547
    99
      Library.foldr (Sorts.inter_sort (Sign.classes_of thy))
haftmann@29547
   100
        (map (base_sort thy) sups, bases);
haftmann@29509
   101
    val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
haftmann@29509
   102
    val supparam_names = map fst supparams;
haftmann@26995
   103
    val _ = if has_duplicates (op =) supparam_names
haftmann@26995
   104
      then error ("Duplicate parameter(s) in superclasses: "
haftmann@26995
   105
        ^ (commas o map quote o duplicates (op =)) supparam_names)
haftmann@26995
   106
      else ();
haftmann@29509
   107
haftmann@29509
   108
    val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional [])))
haftmann@29509
   109
      sups, []);
haftmann@24748
   110
    val constrain = Element.Constrains ((map o apsnd o map_atyps)
haftmann@26167
   111
      (K (TFree (Name.aT, base_sort))) supparams);
haftmann@29526
   112
      (*FIXME 2009 perhaps better: control type variable by explicit
haftmann@29509
   113
      parameter instantiation of import expression*)
haftmann@29509
   114
    val begin_ctxt = begin sups base_sort
haftmann@29509
   115
      #> fold (Variable.declare_constraints o Free) ((map o apsnd o map_atyps)
haftmann@29509
   116
          (K (TFree (Name.aT, base_sort))) supparams) (*FIXME
haftmann@29509
   117
            should constraints be issued in begin?*)
haftmann@29509
   118
    val ((_, _, syntax_elems), _) = ProofContext.init thy
haftmann@29509
   119
      |> begin_ctxt
haftmann@29509
   120
      |> process_decl supexpr raw_elems;
haftmann@25683
   121
    fun fork_syn (Element.Fixes xs) =
haftmann@29006
   122
          fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs
haftmann@25683
   123
          #>> Element.Fixes
haftmann@25683
   124
      | fork_syn x = pair x;
haftmann@29509
   125
    val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
haftmann@29509
   126
  in (((sups, supparam_names), (supsort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end;
haftmann@24748
   127
haftmann@29509
   128
val cert_class_spec = gen_class_spec (K I) Expression.cert_declaration;
haftmann@29509
   129
val read_class_spec = gen_class_spec Sign.intern_class Expression.cert_read_declaration;
haftmann@24748
   130
haftmann@28715
   131
fun add_consts bname class base_sort sups supparams global_syntax thy =
wenzelm@24968
   132
  let
haftmann@29526
   133
    (*FIXME 2009 simplify*)
haftmann@29509
   134
    val supconsts = supparams
haftmann@26518
   135
      |> AList.make (snd o the o AList.lookup (op =) (these_params thy sups))
haftmann@25683
   136
      |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
haftmann@29509
   137
    val all_params = Locale.params_of thy class;
haftmann@28715
   138
    val raw_params = (snd o chop (length supparams)) all_params;
haftmann@29509
   139
    fun add_const (b, SOME raw_ty, _) thy =
haftmann@25683
   140
      let
haftmann@29509
   141
        val v = Binding.base_name b;
haftmann@28965
   142
        val c = Sign.full_bname thy v;
haftmann@25683
   143
        val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
haftmann@25683
   144
        val ty0 = Type.strip_sorts ty;
haftmann@25683
   145
        val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0;
haftmann@25683
   146
        val syn = (the_default NoSyn o AList.lookup (op =) global_syntax) v;
haftmann@25683
   147
      in
haftmann@25683
   148
        thy
haftmann@28965
   149
        |> Sign.declare_const [] ((Binding.name v, ty0), syn)
haftmann@25683
   150
        |> snd
haftmann@25683
   151
        |> pair ((v, ty), (c, ty'))
haftmann@25683
   152
      end;
haftmann@28715
   153
  in
haftmann@28715
   154
    thy
haftmann@29547
   155
    |> Sign.add_path (class_prefix class)
haftmann@28715
   156
    |> fold_map add_const raw_params
haftmann@28715
   157
    ||> Sign.restore_naming thy
haftmann@28715
   158
    |-> (fn params => pair (supconsts @ (map o apfst) fst params, params))
haftmann@28715
   159
  end;
haftmann@28715
   160
haftmann@28715
   161
fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax thy =
haftmann@28715
   162
  let
haftmann@29526
   163
    (*FIXME 2009 simplify*)
haftmann@25683
   164
    fun globalize param_map = map_aterms
haftmann@25683
   165
      (fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty)
haftmann@25683
   166
        | t => t);
haftmann@29509
   167
    val raw_pred = Locale.intros_of thy class
haftmann@25683
   168
      |> fst
haftmann@29509
   169
      |> Option.map (Logic.unvarify o Logic.strip_imp_concl o Thm.prop_of);
haftmann@25683
   170
    fun get_axiom thy = case (#axioms o AxClass.get_info thy) class
haftmann@25683
   171
     of [] => NONE
haftmann@25683
   172
      | [thm] => SOME thm;
wenzelm@24968
   173
  in
wenzelm@24968
   174
    thy
haftmann@28715
   175
    |> add_consts bname class base_sort sups supparams global_syntax
haftmann@25683
   176
    |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
haftmann@26518
   177
          (map (fst o snd) params)
haftmann@29526
   178
          [((Binding.empty, []),
haftmann@29509
   179
            Option.map (globalize param_map) raw_pred |> the_list)]
haftmann@25683
   180
    #> snd
haftmann@25683
   181
    #> `get_axiom
haftmann@25683
   182
    #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
haftmann@29526
   183
    #> pair (param_map, params, assm_axiom)))
wenzelm@24968
   184
  end;
wenzelm@24968
   185
haftmann@26518
   186
fun gen_class prep_spec bname raw_supclasses raw_elems thy =
haftmann@24748
   187
  let
haftmann@28965
   188
    val class = Sign.full_bname thy bname;
haftmann@29509
   189
    val (((sups, supparams), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
haftmann@26247
   190
      prep_spec thy raw_supclasses raw_elems;
haftmann@24218
   191
  in
haftmann@24218
   192
    thy
haftmann@29509
   193
    |> Expression.add_locale bname "" supexpr elems
haftmann@29509
   194
    |> snd |> LocalTheory.exit_global
haftmann@26518
   195
    |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
haftmann@29526
   196
    |-> (fn (param_map, params, assm_axiom) =>
haftmann@29547
   197
       `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
haftmann@29547
   198
    #-> (fn (base_morph, morph, export_morph, axiom, assm_intro, of_class) =>
haftmann@29547
   199
       Locale.add_registration (class, (morph, export_morph))
haftmann@29547
   200
    #> Locale.activate_global_facts (class, morph $> export_morph)
haftmann@29547
   201
    #> register class sups params base_sort base_morph axiom assm_intro of_class))
haftmann@29378
   202
    |> TheoryTarget.init (SOME class)
haftmann@25038
   203
    |> pair class
haftmann@24218
   204
  end;
haftmann@24218
   205
haftmann@24218
   206
in
haftmann@24218
   207
haftmann@29509
   208
val class = gen_class cert_class_spec;
haftmann@26518
   209
val class_cmd = gen_class read_class_spec;
haftmann@24218
   210
haftmann@24218
   211
end; (*local*)
haftmann@24218
   212
haftmann@24218
   213
haftmann@29358
   214
(** subclass relations **)
haftmann@25462
   215
haftmann@29358
   216
local
haftmann@25462
   217
haftmann@29358
   218
fun gen_subclass prep_class do_proof raw_sup lthy =
haftmann@25462
   219
  let
haftmann@29358
   220
    val thy = ProofContext.theory_of lthy;
haftmann@29358
   221
    val sup = prep_class thy raw_sup;
haftmann@29358
   222
    val sub = case TheoryTarget.peek lthy
haftmann@29358
   223
     of {is_class = false, ...} => error "Not a class context"
haftmann@29358
   224
      | {target, ...} => target;
haftmann@29526
   225
haftmann@29358
   226
    val _ = if Sign.subsort thy ([sup], [sub])
haftmann@29358
   227
      then error ("Class " ^ Syntax.string_of_sort lthy [sup]
haftmann@29358
   228
        ^ " is subclass of class " ^ Syntax.string_of_sort lthy [sub])
haftmann@29358
   229
      else ();
haftmann@29358
   230
    val sub_params = map fst (these_params thy [sub]);
haftmann@29358
   231
    val sup_params = map fst (these_params thy [sup]);
haftmann@29358
   232
    val err_params = subtract (op =) sub_params sup_params;
haftmann@29358
   233
    val _ = if null err_params then [] else
haftmann@29358
   234
      error ("Class " ^ Syntax.string_of_sort lthy [sub] ^ " lacks parameter(s) " ^
haftmann@29358
   235
        commas_quote err_params ^ " of " ^ Syntax.string_of_sort lthy [sup]);
haftmann@29509
   236
haftmann@29509
   237
    val expr = ([(sup, (("", false), Expression.Positional []))], []);
haftmann@29509
   238
    val (([props], _, _), goal_ctxt) =
haftmann@29509
   239
      Expression.cert_goal_expression expr lthy;
haftmann@29526
   240
    val some_prop = try the_single props;
haftmann@29526
   241
haftmann@29526
   242
    fun tac some_thm = ALLGOALS (ProofContext.fact_tac (the_list some_thm));
haftmann@29526
   243
    fun prove_sublocale some_thm =
haftmann@29526
   244
      Expression.sublocale sub expr
haftmann@29526
   245
      #> Proof.global_terminal_proof
haftmann@29526
   246
          (Method.Basic (K (Method.SIMPLE_METHOD (tac some_thm)), Position.none), NONE)
haftmann@29526
   247
      #> ProofContext.theory_of;
haftmann@29358
   248
    fun after_qed some_thm =
haftmann@29509
   249
      LocalTheory.theory (register_subclass (sub, sup) some_thm)
haftmann@29526
   250
      #> is_some some_thm ? LocalTheory.theory (prove_sublocale some_thm)
haftmann@29526
   251
          (*FIXME should also go to register_subclass*)
haftmann@29526
   252
      #> ProofContext.theory_of
haftmann@29526
   253
      #> TheoryTarget.init (SOME sub);
haftmann@29526
   254
  in do_proof after_qed some_prop lthy end;
haftmann@25485
   255
haftmann@29358
   256
fun user_proof after_qed NONE =
haftmann@29358
   257
      Proof.theorem_i NONE (K (after_qed NONE)) [[]]
haftmann@29358
   258
  | user_proof after_qed (SOME prop) =
haftmann@29358
   259
      Proof.theorem_i NONE (after_qed o try the_single o the_single) [[(prop, [])]];
haftmann@25485
   260
haftmann@29358
   261
fun tactic_proof tac after_qed NONE lthy =
haftmann@29358
   262
      after_qed NONE lthy
haftmann@29358
   263
  | tactic_proof tac after_qed (SOME prop) lthy =
haftmann@29358
   264
      after_qed (SOME (Goal.prove (LocalTheory.target_of lthy) [] [] prop
haftmann@29358
   265
        (K tac))) lthy;
haftmann@28666
   266
haftmann@29358
   267
in
haftmann@28666
   268
haftmann@29358
   269
val subclass = gen_subclass (K I) user_proof;
haftmann@29358
   270
fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
haftmann@29358
   271
val subclass_cmd = gen_subclass Sign.read_class user_proof;
haftmann@25462
   272
haftmann@29358
   273
end; (*local*)
haftmann@29358
   274
haftmann@24218
   275
end;