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

4012

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


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


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


13 
val smart_store_thm: (bstring * thm) > thm (*DESTRUCTIVE*)

3987

14 
val get_thm: theory > xstring > thm


15 
val get_thms: theory > xstring > thm list


16 
val proto_pure: theory


17 
val pure: theory


18 
val cpure: theory


19 
end;


20 


21 
structure PureThy: PURE_THY =


22 
struct


23 


24 


25 
(** init theorems data **)


26 


27 
(* data kind theorems *)


28 


29 
val theorems = "theorems";


30 


31 
exception Theorems of


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


33 


34 


35 
(* methods *)


36 


37 
local


38 


39 
val empty =


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


41 


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


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


44 


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


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


47 


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


49 
let


50 
val prt_thm = Pretty.quote o pretty_thm;


51 
fun prt_thms (name, [th]) =


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


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


54 


55 
fun extrn name =


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


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


58 
in


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


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


61 
end;


62 


63 
in


64 


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


66 


67 
end;


68 


69 


70 
(* get data record *)


71 


72 
fun get_theorems sg =


73 
(case Sign.get_data sg theorems of


74 
Theorems r => r


75 
 _ => sys_error "get_theorems");


76 


77 


78 
(* retrieve theorems *)


79 


80 
fun lookup_thms theory full_name =


81 
let


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


83 
fun lookup [] = raise Match


84 
 lookup (thy :: thys) =


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


86 
Some thms => thms


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


88 
in


89 
lookup [theory] handle Match


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


91 
end;


92 


93 
fun get_thms thy name =


94 
let


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


96 
val full_name = NameSpace.intern space name;


97 
in lookup_thms thy full_name end;


98 


99 
fun get_thm thy name =


100 
(case get_thms thy name of


101 
[thm] => thm


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


103 


104 


105 
(* store theorems *) (*DESTRUCTIVE*)


106 


107 
fun err_dup name =


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


109 


110 
fun warn_overwrite name =


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


112 


113 
fun warn_same name =


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


115 


116 


117 
fun enter_thms sg single (raw_name, thms) =


118 
let


119 
val len = length thms;


120 
val name = Sign.full_name sg raw_name;


121 
val names =


122 
if single then replicate len name


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


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


125 


126 
val eq_thms = ListPair.all Thm.eq_thm;


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


128 
in


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


130 
None =>


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


132 
 Some thms' =>


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

4002

134 
warn_same name


135 
else warn_overwrite name);

3987

136 


137 
r :=


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


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


140 


141 
named_thms


142 
end;


143 


144 
fun do_enter_thms sg single name_thms =


145 
(enter_thms sg single name_thms; ());


146 


147 

4012

148 
fun store_thmss thmss thy =

3987

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


150 

4012

151 
fun store_thms thms thy =

3987

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


153 

4012

154 
fun smart_store_thm (name, thm) =

3987

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


156 
in named_thm end;


157 


158 


159 


160 
(** the Pure theories **)


161 


162 
val proto_pure =


163 
Theory.pre_pure


164 
> Theory.init_data theorems theorems_methods


165 
> Theory.add_types


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


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


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


169 
Syntax.pure_types)


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


171 
> Theory.add_defsort_i logicS


172 
> Theory.add_arities_i


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


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


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


176 
> Theory.add_syntax Syntax.pure_syntax


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


178 
> Theory.add_trfuns Syntax.pure_trfuns


179 
> Theory.add_trfunsT Syntax.pure_trfunsT


180 
> Theory.add_syntax


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


182 
> Theory.add_consts


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


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


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


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


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


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


189 
> Theory.add_name "ProtoPure";


190 


191 
val pure = proto_pure


192 
> Theory.add_syntax Syntax.pure_appl_syntax


193 
> Theory.add_name "Pure";


194 


195 
val cpure = proto_pure


196 
> Theory.add_syntax Syntax.pure_applC_syntax


197 
> Theory.add_name "CPure";


198 


199 


200 
end;


201 


202 


203 


204 
(** theory structures **)


205 


206 
structure ProtoPure =


207 
struct


208 
val thy = PureThy.proto_pure;


209 
val flexpair_def = get_axiom thy "flexpair_def";


210 
end;


211 


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


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