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