src/Pure/Isar/theory_target.ML
author wenzelm
Tue Nov 28 00:35:27 2006 +0100 (2006-11-28)
changeset 21570 f20f9304ab48
parent 21533 bada5ac1216a
child 21585 2444f1d1127b
permissions -rw-r--r--
simplified '?' operator;
defs: more robust transitivity proofs, expand target defs as well;
tuned;
wenzelm@20894
     1
(*  Title:      Pure/Isar/theory_target.ML
wenzelm@20894
     2
    ID:         $Id$
wenzelm@20894
     3
    Author:     Makarius
wenzelm@20894
     4
wenzelm@20894
     5
Common theory targets.
wenzelm@20894
     6
*)
wenzelm@20894
     7
wenzelm@20894
     8
signature THEORY_TARGET =
wenzelm@20894
     9
sig
wenzelm@21006
    10
  val peek: local_theory -> string option
wenzelm@20962
    11
  val begin: bstring -> Proof.context -> local_theory
wenzelm@20894
    12
  val init: xstring option -> theory -> local_theory
wenzelm@20894
    13
  val init_i: string option -> theory -> local_theory
wenzelm@20894
    14
end;
wenzelm@20894
    15
wenzelm@20894
    16
structure TheoryTarget: THEORY_TARGET =
wenzelm@20894
    17
struct
wenzelm@20894
    18
wenzelm@20894
    19
(** locale targets **)
wenzelm@20894
    20
wenzelm@21006
    21
(* context data *)
wenzelm@21006
    22
wenzelm@21006
    23
structure Data = ProofDataFun
wenzelm@21006
    24
(
wenzelm@21006
    25
  val name = "Isar/theory_target";
wenzelm@21006
    26
  type T = string option;
wenzelm@21006
    27
  fun init _ = NONE;
wenzelm@21006
    28
  fun print _ _ = ();
wenzelm@21006
    29
);
wenzelm@21006
    30
wenzelm@21006
    31
val _ = Context.add_setup Data.init;
wenzelm@21006
    32
val peek = Data.get;
wenzelm@21006
    33
wenzelm@21006
    34
wenzelm@20894
    35
(* pretty *)
wenzelm@20894
    36
wenzelm@20894
    37
fun pretty loc ctxt =
wenzelm@20894
    38
  let
wenzelm@20894
    39
    val thy = ProofContext.theory_of ctxt;
wenzelm@20894
    40
    val fixes = map (fn (x, T) => (x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
wenzelm@20894
    41
    val assumes = map (fn A => (("", []), [(A, [])])) (Assumption.assms_of ctxt);
wenzelm@20894
    42
    val elems =
wenzelm@20894
    43
      (if null fixes then [] else [Element.Fixes fixes]) @
wenzelm@20894
    44
      (if null assumes then [] else [Element.Assumes assumes]);
wenzelm@20894
    45
  in
wenzelm@20984
    46
    if loc = "" then
wenzelm@20984
    47
      [Pretty.block
wenzelm@20984
    48
        [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy),
wenzelm@20984
    49
          Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]]
wenzelm@20984
    50
    else if null elems then [Pretty.str ("locale " ^ Locale.extern thy loc)]
wenzelm@20984
    51
    else
wenzelm@20984
    52
      [Pretty.big_list ("locale " ^ Locale.extern thy loc ^ " =")
wenzelm@20984
    53
        (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)]
wenzelm@20894
    54
  end;
wenzelm@20894
    55
wenzelm@20894
    56
wenzelm@20894
    57
(* consts *)
wenzelm@20894
    58
wenzelm@20894
    59
fun consts loc depends decls lthy =
wenzelm@20894
    60
  let
wenzelm@21533
    61
    val is_loc = loc <> "";
wenzelm@21533
    62
    val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
wenzelm@20894
    63
wenzelm@20894
    64
    fun const ((c, T), mx) thy =
wenzelm@20894
    65
      let
wenzelm@20894
    66
        val U = map #2 xs ---> T;
wenzelm@21533
    67
        val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs);
wenzelm@21533
    68
        val thy' = Sign.add_consts_authentic [(c, U, Syntax.unlocalize_mixfix is_loc mx)] thy;
wenzelm@21533
    69
      in (((c, mx), t), thy') end;
wenzelm@20894
    70
wenzelm@21533
    71
    val (abbrs, lthy') = lthy |> LocalTheory.theory_result (fold_map const decls);
wenzelm@21533
    72
    val defs = abbrs |> map (fn (x, t) => (x, (("", []), t)));
wenzelm@20894
    73
  in
wenzelm@20894
    74
    lthy'
wenzelm@21570
    75
    |> is_loc ? LocalTheory.abbrevs Syntax.default_mode abbrs
wenzelm@21533
    76
    |> LocalDefs.add_defs defs |>> map (apsnd snd)
wenzelm@20894
    77
  end;
wenzelm@20894
    78
wenzelm@20894
    79
wenzelm@20894
    80
(* axioms *)
wenzelm@20894
    81
wenzelm@20894
    82
local
wenzelm@20894
    83
wenzelm@20894
    84
fun add_axiom hyps (name, prop) thy =
wenzelm@20894
    85
  let
wenzelm@20894
    86
    val name' = if name = "" then "axiom_" ^ serial_string () else name;
wenzelm@20894
    87
    val prop' = Logic.list_implies (hyps, prop);
wenzelm@20894
    88
    val thy' = thy |> Theory.add_axioms_i [(name', prop')];
wenzelm@20894
    89
    val axm = Drule.unvarify (Thm.get_axiom_i thy' (Sign.full_name thy' name'));
wenzelm@20894
    90
    val prems = map (Thm.assume o Thm.cterm_of thy') hyps;
wenzelm@20894
    91
  in (Drule.implies_elim_list axm prems, thy') end;
wenzelm@20894
    92
wenzelm@20894
    93
in
wenzelm@20894
    94
wenzelm@21433
    95
fun axioms kind specs lthy =
wenzelm@20915
    96
  let
wenzelm@20915
    97
    val hyps = Assumption.assms_of lthy;
wenzelm@20915
    98
    fun axiom ((name, atts), props) thy = thy
wenzelm@20915
    99
      |> fold_map (add_axiom hyps) (PureThy.name_multi name props)
wenzelm@20915
   100
      |-> (fn ths => pair ((name, atts), [(ths, [])]));
wenzelm@20915
   101
  in
wenzelm@20915
   102
    lthy
wenzelm@20984
   103
    |> fold (fold Variable.declare_term o snd) specs
wenzelm@20915
   104
    |> LocalTheory.theory_result (fold_map axiom specs)
wenzelm@21433
   105
    |-> LocalTheory.notes kind
wenzelm@20915
   106
  end;
wenzelm@20894
   107
wenzelm@20894
   108
end;
wenzelm@20894
   109
wenzelm@20894
   110
wenzelm@20894
   111
(* defs *)
wenzelm@20894
   112
wenzelm@21570
   113
infix also;
wenzelm@21570
   114
fun eq1 also eq2 =
wenzelm@21570
   115
  eq2 COMP (eq1 COMP (Drule.incr_indexes2 eq1 eq2 transitive_thm));
wenzelm@21570
   116
wenzelm@20894
   117
local
wenzelm@20894
   118
wenzelm@21570
   119
fun expand_defs ctxt t =
wenzelm@21570
   120
  let
wenzelm@21570
   121
    val thy = ProofContext.theory_of ctxt;
wenzelm@21570
   122
    val thy_ctxt = ProofContext.init thy;
wenzelm@21570
   123
    val ct = Thm.cterm_of thy t;
wenzelm@21570
   124
    val (defs, ct') = LocalDefs.expand_defs ctxt thy_ctxt (Drule.mk_term ct) ||> Drule.dest_term;
wenzelm@21570
   125
  in (Thm.term_of ct', Tactic.rewrite true defs ct) end;
wenzelm@21570
   126
wenzelm@20894
   127
fun add_def (name, prop) =
wenzelm@20894
   128
  Theory.add_defs_i false false [(name, prop)] #>
wenzelm@20894
   129
  (fn thy => (Drule.unvarify (Thm.get_axiom_i thy (Sign.full_name thy name)), thy));
wenzelm@20894
   130
wenzelm@20894
   131
in
wenzelm@20894
   132
wenzelm@21570
   133
fun defs kind args lthy0 =
wenzelm@20894
   134
  let
wenzelm@21533
   135
    fun def ((c, mx), ((name, atts), rhs)) lthy1 =
wenzelm@20894
   136
      let
wenzelm@21570
   137
        val (rhs', rhs_conv) = expand_defs lthy0 rhs;
wenzelm@21570
   138
        val xs = Variable.add_fixed (LocalTheory.target_of lthy0) rhs' [];
wenzelm@20894
   139
wenzelm@21570
   140
        val ([(lhs, lhs_def)], lthy2) = lthy1
wenzelm@21570
   141
          |> LocalTheory.consts (member (op =) xs) [((c, Term.fastype_of rhs), mx)];
wenzelm@21570
   142
        val lhs' = #2 (Logic.dest_equals (Thm.prop_of lhs_def));
wenzelm@21533
   143
wenzelm@21570
   144
        val name' = Thm.def_name_optional c name;
wenzelm@21570
   145
        val (def, lthy3) = lthy2
wenzelm@20894
   146
          |> LocalTheory.theory_result (add_def (name', Logic.mk_equals (lhs', rhs')));
wenzelm@20894
   147
wenzelm@21533
   148
        val eq =
wenzelm@21570
   149
          (*c == loc.c xs*) lhs_def
wenzelm@21570
   150
          (*lhs' == rhs'*)  also def
wenzelm@21570
   151
          (*rhs' == rhs*)   also Thm.symmetric rhs_conv;
wenzelm@20894
   152
      in ((lhs, ((name', atts), [([eq], [])])), lthy3) end;
wenzelm@20894
   153
wenzelm@21570
   154
    val ((lhss, facts), lthy') = lthy0 |> fold_map def args |>> split_list;
wenzelm@21433
   155
    val (res, lthy'') = lthy' |> LocalTheory.notes kind facts;
wenzelm@20894
   156
  in (lhss ~~ map (apsnd the_single) res, lthy'') end;
wenzelm@20894
   157
wenzelm@20894
   158
end;
wenzelm@20894
   159
wenzelm@20894
   160
wenzelm@20894
   161
(* notes *)
wenzelm@20894
   162
wenzelm@21433
   163
fun context_notes kind facts lthy =
wenzelm@20894
   164
  let
wenzelm@20894
   165
    val facts' = facts
wenzelm@20894
   166
      |> Element.export_standard_facts lthy lthy
wenzelm@20894
   167
      |> Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of lthy));
wenzelm@20894
   168
  in
wenzelm@20894
   169
    lthy
wenzelm@21433
   170
    |> ProofContext.set_stmt true
wenzelm@20894
   171
    |> ProofContext.qualified_names
wenzelm@21433
   172
    |> ProofContext.note_thmss_i kind facts'
wenzelm@20894
   173
    ||> ProofContext.restore_naming lthy
wenzelm@21433
   174
    ||> ProofContext.restore_stmt lthy
wenzelm@20894
   175
  end;
wenzelm@20894
   176
wenzelm@21433
   177
fun theory_notes keep_atts kind facts lthy = lthy |> LocalTheory.theory (fn thy =>
wenzelm@20894
   178
  let
wenzelm@20894
   179
    val facts' = facts
wenzelm@20894
   180
      |> Element.export_standard_facts lthy (ProofContext.init thy)
wenzelm@20915
   181
      |> Attrib.map_facts (if keep_atts then Attrib.attribute_i thy else K I);
wenzelm@20894
   182
  in
wenzelm@20894
   183
    thy
wenzelm@20894
   184
    |> Sign.qualified_names
wenzelm@21433
   185
    |> PureThy.note_thmss_i kind facts' |> #2
wenzelm@20894
   186
    |> Sign.restore_naming thy
wenzelm@20894
   187
  end);
wenzelm@20894
   188
wenzelm@21433
   189
fun locale_notes loc kind facts lthy = lthy |> LocalTheory.target (fn ctxt =>
wenzelm@21433
   190
  #2 (Locale.add_thmss loc kind (Element.export_standard_facts lthy ctxt facts) ctxt));
wenzelm@20894
   191
wenzelm@21433
   192
fun notes "" kind facts = theory_notes true kind facts #> context_notes kind facts
wenzelm@21433
   193
  | notes loc kind facts = theory_notes false kind facts #>
wenzelm@21433
   194
      locale_notes loc kind facts #> context_notes kind facts;
wenzelm@20894
   195
wenzelm@20894
   196
wenzelm@21533
   197
(* target declarations *)
wenzelm@20894
   198
wenzelm@21533
   199
fun decl _ "" f =
wenzelm@21533
   200
      LocalTheory.theory (Context.theory_map (f Morphism.identity)) #>
wenzelm@21533
   201
      LocalTheory.target (Context.proof_map (f Morphism.identity))
wenzelm@21533
   202
  | decl add loc f =
wenzelm@21533
   203
      LocalTheory.target (add loc (Context.proof_map o f));
wenzelm@20894
   204
wenzelm@21498
   205
val type_syntax = decl Locale.add_type_syntax;
wenzelm@21498
   206
val term_syntax = decl Locale.add_term_syntax;
wenzelm@21498
   207
val declaration = decl Locale.add_declaration;
wenzelm@20894
   208
wenzelm@21533
   209
fun target_morphism loc lthy =
wenzelm@21533
   210
  ProofContext.export_standard_morphism lthy (LocalTheory.target_of lthy) $>
wenzelm@21533
   211
  Morphism.name_morphism (NameSpace.qualified loc);
wenzelm@21533
   212
wenzelm@21533
   213
fun target_name "" lthy = Sign.full_name (ProofContext.theory_of lthy)
wenzelm@21533
   214
  | target_name _ lthy = ProofContext.full_name (LocalTheory.target_of lthy);
wenzelm@21533
   215
wenzelm@20894
   216
wenzelm@20894
   217
(* init and exit *)
wenzelm@20894
   218
wenzelm@21293
   219
fun begin loc =
wenzelm@21293
   220
  Data.put (if loc = "" then NONE else SOME loc) #>
wenzelm@21533
   221
  LocalTheory.init (NameSpace.base loc)
wenzelm@21293
   222
   {pretty = pretty loc,
wenzelm@21293
   223
    consts = consts loc,
wenzelm@21293
   224
    axioms = axioms,
wenzelm@21293
   225
    defs = defs,
wenzelm@21293
   226
    notes = notes loc,
wenzelm@21498
   227
    type_syntax = type_syntax loc,
wenzelm@21293
   228
    term_syntax = term_syntax loc,
wenzelm@21293
   229
    declaration = declaration loc,
wenzelm@21533
   230
    target_morphism = target_morphism loc,
wenzelm@21533
   231
    target_name = target_name loc,
wenzelm@21293
   232
    reinit = fn _ => begin loc o (if loc = "" then ProofContext.init else Locale.init loc),
wenzelm@21533
   233
    exit = LocalTheory.target_of};
wenzelm@20894
   234
wenzelm@20962
   235
fun init_i NONE thy = begin "" (ProofContext.init thy)
wenzelm@20962
   236
  | init_i (SOME loc) thy = begin loc (Locale.init loc thy);
wenzelm@20894
   237
wenzelm@21276
   238
fun init (SOME "-") thy = init_i NONE thy
wenzelm@21276
   239
  | init loc thy = init_i (Option.map (Locale.intern thy) loc) thy;
wenzelm@20894
   240
wenzelm@20894
   241
end;