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

21006

10 
val peek: local_theory > string option

20962

11 
val begin: bstring > Proof.context > local_theory

20894

12 
val init: xstring option > theory > local_theory


13 
val init_i: string option > theory > local_theory

20984

14 
val mapping: xstring option > (local_theory > local_theory) > theory > Proof.context * theory

20894

15 
end;


16 


17 
structure TheoryTarget: THEORY_TARGET =


18 
struct


19 


20 
(** locale targets **)


21 

21006

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 

20894

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

20984

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)]

20894

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 <> "") ? 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 

20915

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

20984

109 
> fold (fold Variable.declare_term o snd) specs

20915

110 
> LocalTheory.theory_result (fold_map axiom specs)


111 
> LocalTheory.notes


112 
end;

20894

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 

20915

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

20894

177 
let


178 
val facts' = facts


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

20915

180 
> Attrib.map_facts (if keep_atts then Attrib.attribute_i thy else K I);

20894

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 

20915

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;

20894

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 

20962

207 
fun begin loc =


208 
LocalTheory.init (SOME (NameSpace.base loc))


209 
{pretty = pretty loc,


210 
consts = consts loc,


211 
axioms = axioms,


212 
defs = defs,


213 
notes = notes loc,


214 
term_syntax = term_syntax loc,


215 
declaration = declaration loc,

21006

216 
exit = K I}


217 
#> Data.put (SOME loc);

20894

218 

20962

219 
fun init_i NONE thy = begin "" (ProofContext.init thy)


220 
 init_i (SOME loc) thy = begin loc (Locale.init loc thy);

20894

221 


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


223 

20984

224 
fun mapping loc f = init loc #> f #> LocalTheory.exit false;

20894

225 


226 
end;
