121 val empty = Symtab.empty |
121 val empty = Symtab.empty |
122 val extend = I |
122 val extend = I |
123 fun merge data = Symtab.merge (K true) data |
123 fun merge data = Symtab.merge (K true) data |
124 ) |
124 ) |
125 |
125 |
126 structure DeflMapData = Named_Thms |
|
127 ( |
|
128 val name = @{binding domain_deflation} |
|
129 val description = "theorems like deflation a ==> deflation (foo_map$a)" |
|
130 ) |
|
131 |
|
132 structure Map_Id_Data = Named_Thms |
|
133 ( |
|
134 val name = @{binding domain_map_ID} |
|
135 val description = "theorems like foo_map$ID = ID" |
|
136 ) |
|
137 |
|
138 fun add_rec_type (tname, bs) = |
126 fun add_rec_type (tname, bs) = |
139 Rec_Data.map (Symtab.insert (K true) (tname, bs)) |
127 Rec_Data.map (Symtab.insert (K true) (tname, bs)) |
140 |
128 |
141 fun add_deflation_thm thm = |
129 fun add_deflation_thm thm = |
142 Context.theory_map (DeflMapData.add_thm thm) |
130 Context.theory_map (Named_Theorems.add_thm @{named_theorems domain_deflation} thm) |
143 |
131 |
144 val get_rec_tab = Rec_Data.get |
132 val get_rec_tab = Rec_Data.get |
145 fun get_deflation_thms thy = DeflMapData.get (Proof_Context.init_global thy) |
133 fun get_deflation_thms thy = |
146 |
134 Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_deflation} |
147 val map_ID_add = Map_Id_Data.add |
135 |
148 val get_map_ID_thms = Map_Id_Data.get o Proof_Context.init_global |
136 val map_ID_add = Named_Theorems.add @{named_theorems domain_map_ID} |
149 |
137 fun get_map_ID_thms thy = |
150 val _ = Theory.setup (DeflMapData.setup #> Map_Id_Data.setup) |
138 Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_map_ID} |
|
139 |
151 |
140 |
152 (******************************************************************************) |
141 (******************************************************************************) |
153 (************************** building types and terms **************************) |
142 (************************** building types and terms **************************) |
154 (******************************************************************************) |
143 (******************************************************************************) |
155 |
144 |