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