author | wenzelm |
Thu, 05 Nov 2009 22:08:47 +0100 | |
changeset 33457 | 0fc03a81c27c |
parent 33454 | 485fd398dd33 |
child 33519 | e31a85f92ce9 |
permissions | -rw-r--r-- |
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Isar/spec_rules.ML |
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
3 |
|
33454 | 4 |
Rules that characterize specifications, with rough classification. |
5 |
NB: In the face of arbitrary morphisms, the original shape of |
|
6 |
specifications may get lost. |
|
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
7 |
*) |
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
8 |
|
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
9 |
signature SPEC_RULES = |
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
10 |
sig |
33454 | 11 |
datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive |
12 |
type spec = rough_classification * (term list * thm list) |
|
13 |
val get: Proof.context -> spec list |
|
14 |
val get_global: theory -> spec list |
|
15 |
val add: rough_classification -> term list * thm list -> local_theory -> local_theory |
|
16 |
val add_global: rough_classification -> term list * thm list -> theory -> theory |
|
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
17 |
end; |
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
18 |
|
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
19 |
structure Spec_Rules: SPEC_RULES = |
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
20 |
struct |
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
21 |
|
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
22 |
(* maintain rules *) |
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
23 |
|
33454 | 24 |
datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive; |
25 |
type spec = rough_classification * (term list * thm list); |
|
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
26 |
|
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
27 |
structure Rules = GenericDataFun |
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
28 |
( |
33454 | 29 |
type T = spec Item_Net.T; |
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
30 |
val empty : T = |
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
31 |
Item_Net.init |
33454 | 32 |
(fn ((class1, (ts1, ths1)), (class2, (ts2, ths2))) => |
33 |
class1 = class2 andalso |
|
34 |
eq_list (op aconv) (ts1, ts2) andalso |
|
35 |
eq_list Thm.eq_thm_prop (ths1, ths2)) |
|
36 |
(#1 o #2); |
|
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
37 |
val extend = I; |
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
38 |
fun merge _ = Item_Net.merge; |
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
39 |
); |
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
40 |
|
33454 | 41 |
val get = Item_Net.content o Rules.get o Context.Proof; |
42 |
val get_global = Item_Net.content o Rules.get o Context.Theory; |
|
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
43 |
|
33457 | 44 |
fun add class (ts, ths) = LocalTheory.declaration true |
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
45 |
(fn phi => |
33454 | 46 |
let |
47 |
val ts' = map (Morphism.term phi) ts; |
|
48 |
val ths' = map (Morphism.thm phi) ths; |
|
49 |
in Rules.map (Item_Net.update (class, (ts', ths'))) end); |
|
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
50 |
|
33454 | 51 |
fun add_global class spec = |
52 |
Context.theory_map (Rules.map (Item_Net.update (class, spec))); |
|
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
53 |
|
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
54 |
end; |