author | wenzelm |
Sat, 30 Nov 2019 15:17:23 +0100 | |
changeset 71202 | 785610ad6bfa |
parent 71179 | 592e2afdd50c |
child 71207 | 8af82f3e03c9 |
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 |
|
71202 | 4 |
Rules that characterize specifications, with optional name and |
5 |
rough classification. |
|
6 |
||
33454 | 7 |
NB: In the face of arbitrary morphisms, the original shape of |
8 |
specifications may get lost. |
|
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
9 |
*) |
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
10 |
|
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
11 |
signature SPEC_RULES = |
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
12 |
sig |
69996
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset
|
13 |
datatype recursion = |
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset
|
14 |
Primrec of string list | Recdef | Primcorec of string list | Corec | Unknown_Recursion |
70586 | 15 |
val recursion_ord: recursion ord |
71202 | 16 |
val encode_recursion: recursion XML.Encode.T |
69992
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69991
diff
changeset
|
17 |
datatype rough_classification = Equational of recursion | Inductive | Co_Inductive | Unknown |
70586 | 18 |
val rough_classification_ord: rough_classification ord |
69992
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69991
diff
changeset
|
19 |
val equational_primrec: string list -> rough_classification |
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69991
diff
changeset
|
20 |
val equational_recdef: rough_classification |
69996
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset
|
21 |
val equational_primcorec: string list -> rough_classification |
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset
|
22 |
val equational_corec: rough_classification |
69992
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69991
diff
changeset
|
23 |
val equational: rough_classification |
69991
6b097aeb3650
clarified signature: avoid direct comparison on type rough_classification;
wenzelm
parents:
67649
diff
changeset
|
24 |
val is_equational: rough_classification -> bool |
6b097aeb3650
clarified signature: avoid direct comparison on type rough_classification;
wenzelm
parents:
67649
diff
changeset
|
25 |
val is_inductive: rough_classification -> bool |
6b097aeb3650
clarified signature: avoid direct comparison on type rough_classification;
wenzelm
parents:
67649
diff
changeset
|
26 |
val is_co_inductive: rough_classification -> bool |
71179 | 27 |
val is_relational: rough_classification -> bool |
69991
6b097aeb3650
clarified signature: avoid direct comparison on type rough_classification;
wenzelm
parents:
67649
diff
changeset
|
28 |
val is_unknown: rough_classification -> bool |
71202 | 29 |
val encode_rough_classification: rough_classification XML.Encode.T |
71179 | 30 |
type spec = |
31 |
{name: string, rough_classification: rough_classification, terms: term list, rules: thm list} |
|
33454 | 32 |
val get: Proof.context -> spec list |
33 |
val get_global: theory -> spec list |
|
71202 | 34 |
val dest_theory: theory -> spec list |
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33702
diff
changeset
|
35 |
val retrieve: Proof.context -> term -> spec list |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33702
diff
changeset
|
36 |
val retrieve_global: theory -> term -> spec list |
71179 | 37 |
val add: string -> rough_classification -> term list -> thm list -> local_theory -> local_theory |
38 |
val add_global: string -> rough_classification -> term list -> thm list -> theory -> theory |
|
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
39 |
end; |
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
40 |
|
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
41 |
structure Spec_Rules: SPEC_RULES = |
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
42 |
struct |
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
43 |
|
69992
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69991
diff
changeset
|
44 |
(* recursion *) |
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69991
diff
changeset
|
45 |
|
69996
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset
|
46 |
datatype recursion = |
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset
|
47 |
Primrec of string list | Recdef | Primcorec of string list | Corec | Unknown_Recursion; |
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset
|
48 |
|
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset
|
49 |
val recursion_index = |
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset
|
50 |
fn Primrec _ => 0 | Recdef => 1 | Primcorec _ => 2 | Corec => 3 | Unknown_Recursion => 4; |
69992
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69991
diff
changeset
|
51 |
|
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69991
diff
changeset
|
52 |
fun recursion_ord (Primrec Ts1, Primrec Ts2) = list_ord fast_string_ord (Ts1, Ts2) |
69996
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset
|
53 |
| recursion_ord (Primcorec Ts1, Primcorec Ts2) = list_ord fast_string_ord (Ts1, Ts2) |
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset
|
54 |
| recursion_ord rs = int_ord (apply2 recursion_index rs); |
69992
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69991
diff
changeset
|
55 |
|
71202 | 56 |
val encode_recursion = |
57 |
let open XML.Encode in |
|
58 |
variant |
|
59 |
[fn Primrec a => ([], list string a), |
|
60 |
fn Recdef => ([], []), |
|
61 |
fn Primcorec a => ([], list string a), |
|
62 |
fn Corec => ([], []), |
|
63 |
fn Unknown_Recursion => ([], [])] |
|
64 |
end; |
|
65 |
||
69992
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69991
diff
changeset
|
66 |
|
69991
6b097aeb3650
clarified signature: avoid direct comparison on type rough_classification;
wenzelm
parents:
67649
diff
changeset
|
67 |
(* rough classification *) |
6b097aeb3650
clarified signature: avoid direct comparison on type rough_classification;
wenzelm
parents:
67649
diff
changeset
|
68 |
|
69992
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69991
diff
changeset
|
69 |
datatype rough_classification = Equational of recursion | Inductive | Co_Inductive | Unknown; |
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69991
diff
changeset
|
70 |
|
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69991
diff
changeset
|
71 |
fun rough_classification_ord (Equational r1, Equational r2) = recursion_ord (r1, r2) |
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69991
diff
changeset
|
72 |
| rough_classification_ord cs = |
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69991
diff
changeset
|
73 |
int_ord (apply2 (fn Equational _ => 0 | Inductive => 1 | Co_Inductive => 2 | Unknown => 3) cs); |
69991
6b097aeb3650
clarified signature: avoid direct comparison on type rough_classification;
wenzelm
parents:
67649
diff
changeset
|
74 |
|
69992
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69991
diff
changeset
|
75 |
val equational_primrec = Equational o Primrec; |
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69991
diff
changeset
|
76 |
val equational_recdef = Equational Recdef; |
69996
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset
|
77 |
val equational_primcorec = Equational o Primcorec; |
8f2d3a27aff0
more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents:
69992
diff
changeset
|
78 |
val equational_corec = Equational Corec; |
69992
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69991
diff
changeset
|
79 |
val equational = Equational Unknown_Recursion; |
69991
6b097aeb3650
clarified signature: avoid direct comparison on type rough_classification;
wenzelm
parents:
67649
diff
changeset
|
80 |
|
69992
bd3c10813cc4
more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents:
69991
diff
changeset
|
81 |
val is_equational = fn Equational _ => true | _ => false; |
69991
6b097aeb3650
clarified signature: avoid direct comparison on type rough_classification;
wenzelm
parents:
67649
diff
changeset
|
82 |
val is_inductive = fn Inductive => true | _ => false; |
6b097aeb3650
clarified signature: avoid direct comparison on type rough_classification;
wenzelm
parents:
67649
diff
changeset
|
83 |
val is_co_inductive = fn Co_Inductive => true | _ => false; |
71179 | 84 |
val is_relational = is_inductive orf is_co_inductive; |
69991
6b097aeb3650
clarified signature: avoid direct comparison on type rough_classification;
wenzelm
parents:
67649
diff
changeset
|
85 |
val is_unknown = fn Unknown => true | _ => false; |
6b097aeb3650
clarified signature: avoid direct comparison on type rough_classification;
wenzelm
parents:
67649
diff
changeset
|
86 |
|
71202 | 87 |
val encode_rough_classification = |
88 |
let open XML.Encode in |
|
89 |
variant |
|
90 |
[fn Equational r => ([], encode_recursion r), |
|
91 |
fn Inductive => ([], []), |
|
92 |
fn Co_Inductive => ([], []), |
|
93 |
fn Unknown => ([], [])] |
|
94 |
end; |
|
95 |
||
69991
6b097aeb3650
clarified signature: avoid direct comparison on type rough_classification;
wenzelm
parents:
67649
diff
changeset
|
96 |
|
61060 | 97 |
(* rules *) |
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
98 |
|
71179 | 99 |
type spec = |
100 |
{name: string, rough_classification: rough_classification, terms: term list, rules: thm list}; |
|
101 |
||
102 |
fun eq_spec (specs: spec * spec) = |
|
103 |
(op =) (apply2 #name specs) andalso |
|
104 |
is_equal (rough_classification_ord (apply2 #rough_classification specs)) andalso |
|
105 |
eq_list (op aconv) (apply2 #terms specs) andalso |
|
106 |
eq_list Thm.eq_thm_prop (apply2 #rules specs); |
|
107 |
||
108 |
fun map_spec_rules f ({name, rough_classification, terms, rules}: spec) : spec = |
|
109 |
{name = name, rough_classification = rough_classification, terms = terms, rules = map f rules}; |
|
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
110 |
|
33519 | 111 |
structure Rules = Generic_Data |
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
112 |
( |
33454 | 113 |
type T = spec Item_Net.T; |
71179 | 114 |
val empty : T = Item_Net.init eq_spec #terms; |
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
115 |
val extend = I; |
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
34948
diff
changeset
|
116 |
val merge = Item_Net.merge; |
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
117 |
); |
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
118 |
|
61060 | 119 |
|
120 |
(* get *) |
|
121 |
||
71202 | 122 |
fun get_generic imports context = |
61060 | 123 |
let |
124 |
val thy = Context.theory_of context; |
|
125 |
val transfer = Global_Theory.transfer_theories thy; |
|
71202 | 126 |
fun imported spec = |
127 |
imports |> exists (fn thy => Item_Net.member (Rules.get (Context.Theory thy)) spec); |
|
71179 | 128 |
in |
129 |
Item_Net.content (Rules.get context) |
|
71202 | 130 |
|> filter_out imported |
71179 | 131 |
|> (map o map_spec_rules) transfer |
132 |
end; |
|
61060 | 133 |
|
71202 | 134 |
val get = get_generic [] o Context.Proof; |
135 |
val get_global = get_generic [] o Context.Theory; |
|
136 |
||
137 |
fun dest_theory thy = rev (get_generic (Theory.parents_of thy) (Context.Theory thy)); |
|
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
138 |
|
61060 | 139 |
|
140 |
(* retrieve *) |
|
141 |
||
142 |
fun retrieve_generic context = |
|
143 |
Item_Net.retrieve (Rules.get context) |
|
71179 | 144 |
#> (map o map_spec_rules) (Thm.transfer'' context); |
61060 | 145 |
|
146 |
val retrieve = retrieve_generic o Context.Proof; |
|
147 |
val retrieve_global = retrieve_generic o Context.Theory; |
|
148 |
||
149 |
||
150 |
(* add *) |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33702
diff
changeset
|
151 |
|
71179 | 152 |
fun add name rough_classification terms rules lthy = |
153 |
let val thms0 = map Thm.trim_context (map (Drule.mk_term o Thm.cterm_of lthy) terms @ rules) in |
|
45291
57cd50f98fdc
uniform Local_Theory.declaration with explicit params;
wenzelm
parents:
42360
diff
changeset
|
154 |
lthy |> Local_Theory.declaration {syntax = false, pervasive = true} |
71179 | 155 |
(fn phi => fn context => |
33702 | 156 |
let |
71179 | 157 |
val (terms', rules') = |
158 |
map (Thm.transfer (Context.theory_of context)) thms0 |
|
159 |
|> Morphism.fact phi |
|
160 |
|> chop (length terms) |
|
61060 | 161 |
|>> map (Thm.term_of o Drule.dest_term) |
162 |
||> map Thm.trim_context; |
|
71179 | 163 |
in |
164 |
context |> (Rules.map o Item_Net.update) |
|
165 |
{name = name, rough_classification = rough_classification, |
|
166 |
terms = terms', rules = rules'} |
|
167 |
end) |
|
33702 | 168 |
end; |
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
169 |
|
71179 | 170 |
fun add_global name rough_classification terms rules = |
171 |
(Context.theory_map o Rules.map o Item_Net.update) |
|
172 |
{name = name, rough_classification = rough_classification, |
|
173 |
terms = terms, rules = map Thm.trim_context rules}; |
|
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
174 |
|
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
diff
changeset
|
175 |
end; |