3987

1 
(* Title: Pure/pure_thy.ML


2 
ID: $Id$


3 
Author: Markus Wenzel, TU Muenchen


4 


5 
Init 'theorems' data. The Pure theories.


6 
*)


7 


8 
signature PURE_THY =


9 
sig


10 
val put_thms: (bstring * thm) list > theory > theory (*DESTRUCTIVE*)


11 
val put_thmss: (bstring * thm list) list > theory > theory (*DESTRUCTIVE*)


12 
val store_thm: (bstring * thm) > thm (*DESTRUCTIVE*)


13 
val get_thm: theory > xstring > thm


14 
val get_thms: theory > xstring > thm list


15 
val proto_pure: theory


16 
val pure: theory


17 
val cpure: theory


18 
end;


19 


20 
structure PureThy: PURE_THY =


21 
struct


22 


23 


24 
(** init theorems data **)


25 


26 
(* data kind theorems *)


27 


28 
val theorems = "theorems";


29 


30 
exception Theorems of


31 
{space: NameSpace.T, thms_tab: thm list Symtab.table} ref;


32 


33 


34 
(* methods *)


35 


36 
local


37 


38 
val empty =


39 
Theorems (ref {space = NameSpace.empty, thms_tab = Symtab.null});


40 


41 
fun ext (Theorems (ref {space, ...})) =


42 
Theorems (ref {space = space, thms_tab = Symtab.null});


43 


44 
fun merge (Theorems (ref {space = space1, ...}), Theorems (ref {space = space2, ...})) =


45 
Theorems (ref {space = NameSpace.merge (space1, space2), thms_tab = Symtab.null});


46 


47 
fun print (Theorems (ref {space, thms_tab})) =


48 
let


49 
val prt_thm = Pretty.quote o pretty_thm;


50 
fun prt_thms (name, [th]) =


51 
Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, (prt_thm th)]


52 
 prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths);


53 


54 
fun extrn name =


55 
if ! long_names then name else NameSpace.extern space name;


56 
val thmss = sort_wrt fst (map (apfst extrn) (Symtab.dest thms_tab));


57 
in


58 
Pretty.writeln (Pretty.strs ("theorem name space:" :: map quote (NameSpace.dest space)));


59 
Pretty.writeln (Pretty.big_list "theorems:" (map prt_thms thmss))


60 
end;


61 


62 
in


63 


64 
val theorems_methods = (empty, ext, merge, print);


65 


66 
end;


67 


68 


69 
(* get data record *)


70 


71 
fun get_theorems sg =


72 
(case Sign.get_data sg theorems of


73 
Theorems r => r


74 
 _ => sys_error "get_theorems");


75 


76 


77 
(* retrieve theorems *)


78 


79 
fun lookup_thms theory full_name =


80 
let


81 
val tab_of = #thms_tab o ! o get_theorems o sign_of;


82 
fun lookup [] = raise Match


83 
 lookup (thy :: thys) =


84 
(case Symtab.lookup (tab_of thy, full_name) of


85 
Some thms => thms


86 
 None => lookup (Theory.parents_of thy) handle Match => lookup thys)


87 
in


88 
lookup [theory] handle Match


89 
=> raise THEORY ("No theorems " ^ quote full_name ^ " stored in theory", [theory])


90 
end;


91 


92 
fun get_thms thy name =


93 
let


94 
val ref {space, ...} = get_theorems (sign_of thy);


95 
val full_name = NameSpace.intern space name;


96 
in lookup_thms thy full_name end;


97 


98 
fun get_thm thy name =


99 
(case get_thms thy name of


100 
[thm] => thm


101 
 _ => raise THEORY ("Singleton theorem list expected " ^ quote name, [thy]));


102 


103 


104 
(* store theorems *) (*DESTRUCTIVE*)


105 


106 
fun err_dup name =


107 
error ("Duplicate theorems " ^ quote name);


108 


109 
fun warn_overwrite name =


110 
warning ("Replaced old copy of theorems " ^ quote name);


111 


112 
fun warn_same name =


113 
warning ("Theorem database already contains a copy of " ^ quote name);


114 


115 


116 
fun enter_thms sg single (raw_name, thms) =


117 
let


118 
val len = length thms;


119 
val name = Sign.full_name sg raw_name;


120 
val names =


121 
if single then replicate len name


122 
else map (fn i => name ^ "_" ^ string_of_int i) (0 upto (len  1));


123 
val named_thms = ListPair.map Thm.name_thm (names, thms);


124 


125 
val eq_thms = ListPair.all Thm.eq_thm;


126 
val r as ref {space, thms_tab = tab} = get_theorems sg;


127 
in


128 
(case Symtab.lookup (tab, name) of


129 
None =>


130 
if NameSpace.declared space name then err_dup name else ()


131 
 Some thms' =>


132 
if length thms' = len andalso eq_thms (thms', named_thms) then


133 
warn_overwrite name


134 
else warn_same name);


135 


136 
r :=


137 
{space = NameSpace.extend ([name], space),


138 
thms_tab = Symtab.update ((name, named_thms), tab)};


139 


140 
named_thms


141 
end;


142 


143 
fun do_enter_thms sg single name_thms =


144 
(enter_thms sg single name_thms; ());


145 


146 


147 
fun put_thmss thmss thy =


148 
(seq (do_enter_thms (sign_of thy) false) thmss; thy);


149 


150 
fun put_thms thms thy =


151 
(seq (do_enter_thms (sign_of thy) true) (map (apsnd (fn th => [th])) thms); thy);


152 


153 
fun store_thm (name, thm) =


154 
let val [named_thm] = enter_thms (Thm.sign_of_thm thm) true (name, [thm])


155 
in named_thm end;


156 


157 


158 


159 
(** the Pure theories **)


160 


161 
val proto_pure =


162 
Theory.pre_pure


163 
> Theory.init_data theorems theorems_methods


164 
> Theory.add_types


165 
(("fun", 2, NoSyn) ::


166 
("prop", 0, NoSyn) ::


167 
("itself", 1, NoSyn) ::


168 
Syntax.pure_types)


169 
> Theory.add_classes_i [(logicC, [])]


170 
> Theory.add_defsort_i logicS


171 
> Theory.add_arities_i


172 
[("fun", [logicS, logicS], logicS),


173 
("prop", [], logicS),


174 
("itself", [logicS], logicS)]


175 
> Theory.add_syntax Syntax.pure_syntax


176 
> Theory.add_modesyntax ("symbols", true) Syntax.pure_sym_syntax


177 
> Theory.add_trfuns Syntax.pure_trfuns


178 
> Theory.add_trfunsT Syntax.pure_trfunsT


179 
> Theory.add_syntax


180 
[("==>", "[prop, prop] => prop", Delimfix "op ==>")]


181 
> Theory.add_consts


182 
[("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),


183 
("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),


184 
("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),


185 
("all", "('a => prop) => prop", Binder ("!!", 0, 0)),


186 
("TYPE", "'a itself", NoSyn)]


187 
> Theory.add_defs [("flexpair_def", "(t =?= u) == (t == u::'a::{})")]


188 
> Theory.add_name "ProtoPure";


189 


190 
val pure = proto_pure


191 
> Theory.add_syntax Syntax.pure_appl_syntax


192 
> Theory.add_name "Pure";


193 


194 
val cpure = proto_pure


195 
> Theory.add_syntax Syntax.pure_applC_syntax


196 
> Theory.add_name "CPure";


197 


198 


199 
end;


200 


201 


202 


203 
(** theory structures **)


204 


205 
structure ProtoPure =


206 
struct


207 
val thy = PureThy.proto_pure;


208 
val flexpair_def = get_axiom thy "flexpair_def";


209 
end;


210 


211 
structure Pure = struct val thy = PureThy.pure end;


212 
structure CPure = struct val thy = PureThy.cpure end;
