20894

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 init: xstring option > theory > local_theory


11 
val init_i: string option > theory > local_theory


12 
val exit: local_theory > local_theory * theory


13 
val mapping: xstring option > (local_theory > local_theory) > theory > local_theory * theory


14 
end;


15 


16 
structure TheoryTarget: THEORY_TARGET =


17 
struct


18 


19 
(** locale targets **)


20 


21 
(* pretty *)


22 


23 
fun pretty loc ctxt =


24 
let


25 
val thy = ProofContext.theory_of ctxt;


26 
val fixes = map (fn (x, T) => (x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));


27 
val assumes = map (fn A => (("", []), [(A, [])])) (Assumption.assms_of ctxt);


28 
val elems =


29 
(if null fixes then [] else [Element.Fixes fixes]) @


30 
(if null assumes then [] else [Element.Assumes assumes]);


31 
in


32 
([Pretty.block


33 
[Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy),


34 
Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]] @


35 
(if loc = "" then []


36 
else if null elems then [Pretty.str ("locale " ^ Locale.extern thy loc)]


37 
else


38 
[Pretty.big_list ("locale " ^ Locale.extern thy loc ^ " =")


39 
(map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)]))


40 
> Pretty.chunks


41 
end;


42 


43 


44 
(* consts *)


45 


46 
fun consts loc depends decls lthy =


47 
let


48 
val xs = filter depends (#1 (ProofContext.inferred_fixes lthy));


49 
val ys = filter (Variable.newly_fixed lthy (LocalTheory.target_of lthy) o #1) xs;


50 


51 
fun const ((c, T), mx) thy =


52 
let


53 
val U = map #2 xs > T;


54 
val mx' = if null ys then mx else NoSyn;


55 
val mx'' = Syntax.unlocalize_mixfix (loc <> "") mx';


56 


57 
val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs);


58 
val defn = ((c, if loc <> "" then mx else NoSyn (* FIXME !? *)), (("", []), t));


59 
val abbr = ((c, mx'), fold_rev (lambda o Free) ys t);


60 
val thy' = Sign.add_consts_authentic [(c, U, mx'')] thy;


61 
in ((defn, abbr), thy') end;


62 


63 
val ((defns, abbrs), lthy') = lthy


64 
> LocalTheory.theory_result (fold_map const decls) >> split_list;


65 
in


66 
lthy'


67 
> K (loc <> "") ? LocalTheory.abbrevs Syntax.default_mode abbrs


68 
> LocalDefs.add_defs defns >> map (apsnd snd)


69 
end;


70 


71 


72 
(* axioms *)


73 


74 
local


75 


76 
fun add_axiom hyps (name, prop) thy =


77 
let


78 
val name' = if name = "" then "axiom_" ^ serial_string () else name;


79 
val prop' = Logic.list_implies (hyps, prop);


80 
val thy' = thy > Theory.add_axioms_i [(name', prop')];


81 
val axm = Drule.unvarify (Thm.get_axiom_i thy' (Sign.full_name thy' name'));


82 
val prems = map (Thm.assume o Thm.cterm_of thy') hyps;


83 
in (Drule.implies_elim_list axm prems, thy') end;


84 


85 
in


86 


87 
fun axioms specs =


88 
fold (fold Variable.fix_frees o snd) specs #> (* FIXME !? *)


89 
(fn lthy =>


90 
let


91 
val hyps = Assumption.assms_of lthy;


92 
fun axiom ((name, atts), props) thy = thy


93 
> fold_map (add_axiom hyps) (PureThy.name_multi name props)


94 
> (fn ths => pair ((name, atts), [(ths, [])]));


95 
in


96 
lthy


97 
> LocalTheory.theory_result (fold_map axiom specs)


98 
> LocalTheory.notes


99 
end);


100 


101 
end;


102 


103 


104 
(* defs *)


105 


106 
local


107 


108 
fun add_def (name, prop) =


109 
Theory.add_defs_i false false [(name, prop)] #>


110 
(fn thy => (Drule.unvarify (Thm.get_axiom_i thy (Sign.full_name thy name)), thy));


111 


112 
fun expand_defs lthy =


113 
Drule.term_rule (ProofContext.theory_of lthy)


114 
(Assumption.export false lthy (LocalTheory.target_of lthy));


115 


116 
in


117 


118 
fun defs args lthy =


119 
let


120 
fun def ((x, mx), ((name, atts), rhs)) lthy1 =


121 
let


122 
val name' = Thm.def_name_optional x name;


123 
val T = Term.fastype_of rhs;


124 
val rhs' = expand_defs lthy1 rhs;


125 
val depends = member (op =) (Term.add_frees rhs' []);


126 
val defined = filter_out depends (Term.add_frees rhs []);


127 


128 
val rhs_conv = rhs


129 
> Thm.cterm_of (ProofContext.theory_of lthy1)


130 
> Tactic.rewrite true (map_filter (LocalDefs.find_def lthy1 o #1) defined);


131 


132 
val ([(lhs, local_def)], lthy2) = lthy1


133 
> LocalTheory.consts depends [((x, T), mx)];


134 
val lhs' = #2 (Logic.dest_equals (Thm.prop_of local_def));


135 


136 
val (global_def, lthy3) = lthy2


137 
> LocalTheory.theory_result (add_def (name', Logic.mk_equals (lhs', rhs')));


138 


139 
val eq = Thm.transitive (Thm.transitive local_def global_def) (Thm.symmetric rhs_conv);


140 
in ((lhs, ((name', atts), [([eq], [])])), lthy3) end;


141 


142 
val ((lhss, facts), lthy') = lthy > fold_map def args >> split_list;


143 
val (res, lthy'') = lthy' > LocalTheory.notes facts;


144 
in (lhss ~~ map (apsnd the_single) res, lthy'') end;


145 


146 
end;


147 


148 


149 
(* notes *)


150 


151 
fun context_notes facts lthy =


152 
let


153 
val facts' = facts


154 
> Element.export_standard_facts lthy lthy


155 
> Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of lthy));


156 
in


157 
lthy


158 
> ProofContext.qualified_names


159 
> ProofContext.note_thmss_i facts'


160 
> ProofContext.restore_naming lthy


161 
end;


162 


163 
fun theory_notes facts lthy = lthy > LocalTheory.theory (fn thy =>


164 
let


165 
val facts' = facts


166 
> Element.export_standard_facts lthy (ProofContext.init thy)


167 
> Attrib.map_facts (Attrib.attribute_i thy);


168 
in


169 
thy


170 
> Sign.qualified_names


171 
> PureThy.note_thmss_i "" facts' > #2


172 
> Sign.restore_naming thy


173 
end);


174 


175 
fun locale_notes loc facts lthy = lthy > LocalTheory.target (fn ctxt =>


176 
#2 (Locale.add_thmss "" loc (Element.export_standard_facts lthy ctxt facts) ctxt));


177 


178 
fun notes "" facts = theory_notes facts #> context_notes facts


179 
 notes loc facts = locale_notes loc facts #> context_notes facts


180 


181 


182 
(* declarations *)


183 


184 
fun term_syntax "" f = LocalTheory.theory (Context.theory_map f)


185 
 term_syntax loc f = LocalTheory.target (Locale.add_term_syntax loc (Context.proof_map f));


186 


187 
fun declaration "" f = LocalTheory.theory (Context.theory_map f)


188 
 declaration loc f = I; (* FIXME *)


189 


190 


191 


192 
(* init and exit *)


193 


194 
fun target_operations loc : LocalTheory.operations =


195 
{pretty = pretty loc,


196 
consts = consts loc,


197 
axioms = axioms,


198 
defs = defs,


199 
notes = notes loc,


200 
term_syntax = term_syntax loc,


201 
declaration = declaration loc};


202 


203 
fun init_i NONE thy = LocalTheory.init (SOME "") (target_operations "") (ProofContext.init thy)


204 
 init_i (SOME loc) thy =


205 
LocalTheory.init (SOME (NameSpace.base loc)) (target_operations loc) (Locale.init loc thy);


206 


207 
fun init loc thy = init_i (Option.map (Locale.intern thy) loc) thy;


208 


209 
fun exit lthy = (lthy, ProofContext.theory_of lthy);


210 


211 
fun mapping loc f = init loc #> f #> exit;


212 


213 
end;
