src/Pure/Isar/theory_target.ML
author wenzelm
Thu, 30 Nov 2006 14:17:37 +0100
changeset 21611 fc95ff1fe738
parent 21594 2859c94d67d4
child 21613 ae3bb930b50f
permissions -rw-r--r--
notes: proper import/export of proofs (still inactive); Goal.norm/close_result; tuned;
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
21594
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
     5
Common theory/locale targets.
20894
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
21594
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
    19
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    20
(** locale targets **)
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    21
21006
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    22
(* context data *)
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    23
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    24
structure Data = ProofDataFun
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    25
(
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    26
  val name = "Isar/theory_target";
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    27
  type T = string option;
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    28
  fun init _ = NONE;
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    29
  fun print _ _ = ();
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    30
);
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    31
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    32
val _ = Context.add_setup Data.init;
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    33
val peek = Data.get;
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    34
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    35
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    36
(* pretty *)
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    37
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    38
fun pretty loc ctxt =
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    39
  let
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    40
    val thy = ProofContext.theory_of ctxt;
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    41
    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
    42
    val assumes = map (fn A => (("", []), [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt));
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    43
    val elems =
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    44
      (if null fixes then [] else [Element.Fixes fixes]) @
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    45
      (if null assumes then [] else [Element.Assumes assumes]);
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    46
  in
20984
d09f388fa9db exit: pass interactive flag;
wenzelm
parents: 20962
diff changeset
    47
    if loc = "" then
d09f388fa9db exit: pass interactive flag;
wenzelm
parents: 20962
diff changeset
    48
      [Pretty.block
d09f388fa9db exit: pass interactive flag;
wenzelm
parents: 20962
diff changeset
    49
        [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy),
d09f388fa9db exit: pass interactive flag;
wenzelm
parents: 20962
diff changeset
    50
          Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]]
d09f388fa9db exit: pass interactive flag;
wenzelm
parents: 20962
diff changeset
    51
    else if null elems then [Pretty.str ("locale " ^ Locale.extern thy loc)]
d09f388fa9db exit: pass interactive flag;
wenzelm
parents: 20962
diff changeset
    52
    else
d09f388fa9db exit: pass interactive flag;
wenzelm
parents: 20962
diff changeset
    53
      [Pretty.big_list ("locale " ^ Locale.extern thy loc ^ " =")
d09f388fa9db exit: pass interactive flag;
wenzelm
parents: 20962
diff changeset
    54
        (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)]
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    55
  end;
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    56
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    57
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    58
(* consts *)
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    59
21594
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
    60
fun consts is_loc depends decls lthy =
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    61
  let
21533
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
21611
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
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
(* defs *)
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    81
21594
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
    82
local
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
    83
21570
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
    84
infix also;
21611
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
    85
21570
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
    86
fun eq1 also eq2 =
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
    87
  eq2 COMP (eq1 COMP (Drule.incr_indexes2 eq1 eq2 transitive_thm));
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
    88
21594
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
    89
fun expand_term ctxt t =
21570
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
    90
  let
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
    91
    val thy = ProofContext.theory_of ctxt;
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
    92
    val thy_ctxt = ProofContext.init thy;
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
    93
    val ct = Thm.cterm_of thy t;
21594
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
    94
    val (defs, ct') = LocalDefs.export ctxt thy_ctxt (Drule.mk_term ct) ||> Drule.dest_term;
21570
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
    95
  in (Thm.term_of ct', Tactic.rewrite true defs ct) end;
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
    96
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    97
fun add_def (name, prop) =
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    98
  Theory.add_defs_i false false [(name, prop)] #>
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    99
  (fn thy => (Drule.unvarify (Thm.get_axiom_i thy (Sign.full_name thy name)), thy));
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   100
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   101
in
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   102
21570
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
   103
fun defs kind args lthy0 =
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   104
  let
21533
bada5ac1216a simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents: 21498
diff changeset
   105
    fun def ((c, mx), ((name, atts), rhs)) lthy1 =
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   106
      let
21594
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
   107
        val (rhs', rhs_conv) = expand_term lthy0 rhs;
21570
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
   108
        val xs = Variable.add_fixed (LocalTheory.target_of lthy0) rhs' [];
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   109
21570
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
   110
        val ([(lhs, lhs_def)], lthy2) = lthy1
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
   111
          |> LocalTheory.consts (member (op =) xs) [((c, Term.fastype_of rhs), mx)];
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
   112
        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
   113
21570
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
   114
        val name' = Thm.def_name_optional c name;
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
   115
        val (def, lthy3) = lthy2
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   116
          |> LocalTheory.theory_result (add_def (name', Logic.mk_equals (lhs', rhs')));
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   117
21533
bada5ac1216a simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents: 21498
diff changeset
   118
        val eq =
21570
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
   119
          (*c == loc.c xs*) lhs_def
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
   120
          (*lhs' == rhs'*)  also def
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
   121
          (*rhs' == rhs*)   also Thm.symmetric rhs_conv;
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   122
      in ((lhs, ((name', atts), [([eq], [])])), lthy3) end;
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   123
21570
f20f9304ab48 simplified '?' operator;
wenzelm
parents: 21533
diff changeset
   124
    val ((lhss, facts), lthy') = lthy0 |> fold_map def args |>> split_list;
21433
89104dca628e LocalTheory.axioms/notes/defs: proper kind;
wenzelm
parents: 21293
diff changeset
   125
    val (res, lthy'') = lthy' |> LocalTheory.notes kind facts;
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   126
  in (lhss ~~ map (apsnd the_single) res, lthy'') end;
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   127
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   128
end;
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   129
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   130
21611
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   131
(* axioms *)
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   132
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   133
local
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   134
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   135
fun add_axiom hyps (name, prop) thy =
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   136
  let
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   137
    val name' = if name = "" then "axiom_" ^ serial_string () else name;
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   138
    val prop' = Logic.list_implies (hyps, prop);
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   139
    val thy' = thy |> Theory.add_axioms_i [(name', prop')];
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   140
    val axm = Drule.unvarify (Thm.get_axiom_i thy' (Sign.full_name thy' name'));
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   141
    val prems = map (Thm.assume o Thm.cterm_of thy') hyps;
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   142
  in (Drule.implies_elim_list axm prems, thy') end;
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   143
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   144
in
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   145
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   146
fun axioms kind specs lthy =
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   147
  let
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   148
    val hyps = map Thm.term_of (Assumption.assms_of lthy);
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   149
    fun axiom ((name, atts), props) thy = thy
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   150
      |> fold_map (add_axiom hyps) (PureThy.name_multi name props)
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   151
      |-> (fn ths => pair ((name, atts), [(ths, [])]));
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   152
  in
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   153
    lthy
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   154
    |> fold (fold Variable.declare_term o snd) specs
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   155
    |> LocalTheory.theory_result (fold_map axiom specs)
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   156
    |-> LocalTheory.notes kind
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   157
  end;
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   158
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   159
end;
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   160
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   161
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   162
(* notes *)
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   163
21611
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   164
fun import_export_proof ctxt (name, raw_th) =
21594
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
   165
  let
21611
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   166
    val thy = ProofContext.theory_of ctxt;
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   167
    val thy_ctxt = ProofContext.init thy;
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   168
    val certT = Thm.ctyp_of thy;
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   169
    val cert = Thm.cterm_of thy;
21594
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
   170
21611
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   171
    (*export assumes/defines*)
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   172
    val th = Goal.norm_result raw_th;
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   173
    val (defs, th') = LocalDefs.export ctxt thy_ctxt th;
21594
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
   174
    val concl_conv = Tactic.rewrite true defs (Thm.cprop_of th);
21611
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   175
    val assms = map (Tactic.rewrite_rule defs o Thm.assume) (Assumption.assms_of ctxt);
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   176
    val nprems = Thm.nprems_of th' - Thm.nprems_of th;
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   177
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   178
    (*export fixes*)
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   179
    val tfrees = map TFree (Drule.fold_terms Term.add_tfrees th' []);
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   180
    val frees = map Free (Drule.fold_terms Term.add_frees th' []);
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   181
    val (th'' :: vs) = (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees))
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   182
      |> Variable.export ctxt thy_ctxt
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   183
      |> Drule.zero_var_indexes_list;
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   184
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   185
    (*thm definition*)
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   186
    val result = PureThy.name_thm true (name, th'');
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   187
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   188
    (*import fixes*)
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   189
    val (tvars, vars) =
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   190
      chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs)
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   191
      |>> map Logic.dest_type;
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   192
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   193
    val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   194
    val inst = filter (is_Var o fst) (vars ~~ frees);
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   195
    val cinstT = map (pairself certT o apfst TVar) instT;
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   196
    val cinst = map (pairself (cert o Term.map_types (TermSubst.instantiateT instT))) inst;
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   197
    val result' = Thm.instantiate (cinstT, cinst) result;
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   198
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   199
    (*import assumes/defines*)
21594
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
   200
    val assm_tac = FIRST' (map (fn assm => Tactic.compose_tac (false, assm, 0)) assms);
21611
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   201
    val result'' =
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   202
      (case SINGLE (Seq.INTERVAL assm_tac 1 nprems) result' of
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   203
        NONE => raise THM ("Failed to re-import result", 0, [result'])
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   204
      | SOME res => res) COMP (concl_conv COMP_INCR Drule.equal_elim_rule2)
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   205
      |> Goal.norm_result
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   206
      |> Goal.close_result;
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   207
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   208
    val _ = result'' COMP (th COMP_INCR Drule.remdups_rl);  (* FIXME *)
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   209
  in (result'', result) end;
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   210
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   211
fun import_export ctxt (_, raw_th) =
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   212
  let
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   213
    val thy_ctxt = ProofContext.init (ProofContext.theory_of ctxt);
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   214
    val result'' = Goal.close_result (Goal.norm_result raw_th);
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   215
    val result = Goal.norm_result (singleton (ProofContext.export ctxt thy_ctxt) result'');
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   216
  in (result'', result) end;
21585
2444f1d1127b Assumption.assms_of: cterm;
wenzelm
parents: 21570
diff changeset
   217
21594
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
   218
fun notes loc kind facts lthy =
21585
2444f1d1127b Assumption.assms_of: cterm;
wenzelm
parents: 21570
diff changeset
   219
  let
21594
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
   220
    val is_loc = loc <> "";
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
   221
    val thy = ProofContext.theory_of lthy;
21585
2444f1d1127b Assumption.assms_of: cterm;
wenzelm
parents: 21570
diff changeset
   222
21594
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
   223
    val facts' = facts
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
   224
      |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi (fst a)) bs))
21611
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   225
      |> PureThy.map_facts (import_export lthy);
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   226
    val local_facts = PureThy.map_facts #1 facts'
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   227
      |> Attrib.map_facts (Attrib.attribute_i thy);
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   228
    val target_facts = PureThy.map_facts #1 facts'
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   229
      |> is_loc ? Element.facts_map (Element.morph_ctxt (LocalTheory.target_morphism lthy));
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   230
    val global_facts = PureThy.map_facts #2 facts'
21594
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
   231
      |> Attrib.map_facts (if is_loc then K I else Attrib.attribute_i thy);
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
   232
  in
21611
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   233
    lthy |> LocalTheory.theory
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   234
      (Sign.qualified_names
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   235
        #> PureThy.note_thmss_i kind global_facts #> snd
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   236
        #> Sign.restore_naming thy)
21585
2444f1d1127b Assumption.assms_of: cterm;
wenzelm
parents: 21570
diff changeset
   237
21611
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   238
    |> is_loc ? LocalTheory.target (Locale.add_thmss loc kind target_facts)
21594
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
   239
21433
89104dca628e LocalTheory.axioms/notes/defs: proper kind;
wenzelm
parents: 21293
diff changeset
   240
    |> ProofContext.set_stmt true
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   241
    |> ProofContext.qualified_names
21611
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   242
    |> ProofContext.note_thmss_i kind local_facts
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   243
    ||> ProofContext.restore_naming lthy
21433
89104dca628e LocalTheory.axioms/notes/defs: proper kind;
wenzelm
parents: 21293
diff changeset
   244
    ||> ProofContext.restore_stmt lthy
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   245
  end;
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   246
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   247
21533
bada5ac1216a simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents: 21498
diff changeset
   248
(* target declarations *)
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   249
21611
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   250
fun target_decl _ "" f =
21533
bada5ac1216a simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents: 21498
diff changeset
   251
      LocalTheory.theory (Context.theory_map (f Morphism.identity)) #>
bada5ac1216a simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents: 21498
diff changeset
   252
      LocalTheory.target (Context.proof_map (f Morphism.identity))
21611
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   253
  | target_decl add loc f =
21533
bada5ac1216a simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents: 21498
diff changeset
   254
      LocalTheory.target (add loc (Context.proof_map o f));
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   255
21611
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   256
val type_syntax = target_decl Locale.add_type_syntax;
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   257
val term_syntax = target_decl Locale.add_term_syntax;
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   258
val declaration = target_decl Locale.add_declaration;
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   259
21533
bada5ac1216a simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents: 21498
diff changeset
   260
fun target_morphism loc lthy =
21594
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
   261
  ProofContext.export_morphism lthy (LocalTheory.target_of lthy) $>
21611
fc95ff1fe738 notes: proper import/export of proofs (still inactive);
wenzelm
parents: 21594
diff changeset
   262
  Morphism.thm_morphism (Goal.close_result o Goal.norm_result);
21533
bada5ac1216a simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents: 21498
diff changeset
   263
bada5ac1216a simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents: 21498
diff changeset
   264
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
   265
  | target_name _ lthy = ProofContext.full_name (LocalTheory.target_of lthy);
bada5ac1216a simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents: 21498
diff changeset
   266
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   267
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   268
(* init and exit *)
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   269
21293
5f5162f40ac7 removed mapping;
wenzelm
parents: 21276
diff changeset
   270
fun begin loc =
5f5162f40ac7 removed mapping;
wenzelm
parents: 21276
diff changeset
   271
  Data.put (if loc = "" then NONE else SOME loc) #>
21533
bada5ac1216a simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents: 21498
diff changeset
   272
  LocalTheory.init (NameSpace.base loc)
21293
5f5162f40ac7 removed mapping;
wenzelm
parents: 21276
diff changeset
   273
   {pretty = pretty loc,
21594
2859c94d67d4 reworked notes: towards proper import/export of proof terms;
wenzelm
parents: 21585
diff changeset
   274
    consts = consts (loc <> ""),
21293
5f5162f40ac7 removed mapping;
wenzelm
parents: 21276
diff changeset
   275
    axioms = axioms,
5f5162f40ac7 removed mapping;
wenzelm
parents: 21276
diff changeset
   276
    defs = defs,
5f5162f40ac7 removed mapping;
wenzelm
parents: 21276
diff changeset
   277
    notes = notes loc,
21498
6382c3a1e7cf uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents: 21467
diff changeset
   278
    type_syntax = type_syntax loc,
21293
5f5162f40ac7 removed mapping;
wenzelm
parents: 21276
diff changeset
   279
    term_syntax = term_syntax loc,
5f5162f40ac7 removed mapping;
wenzelm
parents: 21276
diff changeset
   280
    declaration = declaration loc,
21533
bada5ac1216a simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents: 21498
diff changeset
   281
    target_morphism = target_morphism loc,
bada5ac1216a simplified consts: no auxiliary params, sane mixfix syntax;
wenzelm
parents: 21498
diff changeset
   282
    target_name = target_name loc,
21293
5f5162f40ac7 removed mapping;
wenzelm
parents: 21276
diff changeset
   283
    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
   284
    exit = LocalTheory.target_of};
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   285
20962
e404275bff33 added begin;
wenzelm
parents: 20915
diff changeset
   286
fun init_i NONE thy = begin "" (ProofContext.init thy)
e404275bff33 added begin;
wenzelm
parents: 20915
diff changeset
   287
  | init_i (SOME loc) thy = begin loc (Locale.init loc thy);
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   288
21276
2285cf5a7560 init: '-' refers to global context;
wenzelm
parents: 21037
diff changeset
   289
fun init (SOME "-") thy = init_i NONE thy
2285cf5a7560 init: '-' refers to global context;
wenzelm
parents: 21037
diff changeset
   290
  | init loc thy = init_i (Option.map (Locale.intern thy) loc) thy;
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   291
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   292
end;