11 {is_partial : bool, |
11 {is_partial : bool, |
12 defname : string, |
12 defname : string, |
13 (* contains no logical entities: invariant under morphisms: *) |
13 (* contains no logical entities: invariant under morphisms: *) |
14 add_simps : (binding -> binding) -> string -> (binding -> binding) -> |
14 add_simps : (binding -> binding) -> string -> (binding -> binding) -> |
15 Attrib.src list -> thm list -> local_theory -> thm list * local_theory, |
15 Attrib.src list -> thm list -> local_theory -> thm list * local_theory, |
|
16 fnames : string list, |
16 case_names : string list, |
17 case_names : string list, |
17 fs : term list, |
18 fs : term list, |
18 R : term, |
19 R : term, |
19 dom: term, |
20 dom: term, |
20 psimps: thm list, |
21 psimps: thm list, |
21 pinducts: thm list, |
22 pinducts: thm list, |
22 simps : thm list option, |
23 simps : thm list option, |
23 inducts : thm list option, |
24 inducts : thm list option, |
24 termination : thm, |
25 termination : thm, |
25 cases : thm} |
26 cases : thm list, |
|
27 pelims: thm list list, |
|
28 elims: thm list list option} |
26 |
29 |
27 end |
30 end |
28 |
31 |
29 structure Function_Data : FUNCTION_DATA = |
32 structure Function_Data : FUNCTION_DATA = |
30 struct |
33 struct |
33 {is_partial : bool, |
36 {is_partial : bool, |
34 defname : string, |
37 defname : string, |
35 (* contains no logical entities: invariant under morphisms: *) |
38 (* contains no logical entities: invariant under morphisms: *) |
36 add_simps : (binding -> binding) -> string -> (binding -> binding) -> |
39 add_simps : (binding -> binding) -> string -> (binding -> binding) -> |
37 Attrib.src list -> thm list -> local_theory -> thm list * local_theory, |
40 Attrib.src list -> thm list -> local_theory -> thm list * local_theory, |
|
41 fnames : string list, |
38 case_names : string list, |
42 case_names : string list, |
39 fs : term list, |
43 fs : term list, |
40 R : term, |
44 R : term, |
41 dom: term, |
45 dom: term, |
42 psimps: thm list, |
46 psimps: thm list, |
43 pinducts: thm list, |
47 pinducts: thm list, |
44 simps : thm list option, |
48 simps : thm list option, |
45 inducts : thm list option, |
49 inducts : thm list option, |
46 termination : thm, |
50 termination : thm, |
47 cases : thm} |
51 cases : thm list, |
|
52 pelims : thm list list, |
|
53 elims : thm list list option} |
48 |
54 |
49 end |
55 end |
50 |
56 |
51 signature FUNCTION_COMMON = |
57 signature FUNCTION_COMMON = |
52 sig |
58 sig |
64 G: term, |
70 G: term, |
65 R: term, |
71 R: term, |
66 dom: term, |
72 dom: term, |
67 psimps : thm list, |
73 psimps : thm list, |
68 simple_pinducts : thm list, |
74 simple_pinducts : thm list, |
69 cases : thm, |
75 cases : thm list, |
|
76 pelims : thm list list, |
70 termination : thm, |
77 termination : thm, |
71 domintros : thm list option} |
78 domintros : thm list option} |
72 val transform_function_data : info -> morphism -> info |
79 val transform_function_data : info -> morphism -> info |
73 val get_function : Proof.context -> (term * info) Item_Net.T |
80 val get_function : Proof.context -> (term * info) Item_Net.T |
74 val import_function_data : term -> Proof.context -> info option |
81 val import_function_data : term -> Proof.context -> info option |
144 G: term, |
151 G: term, |
145 R: term, |
152 R: term, |
146 dom: term, |
153 dom: term, |
147 psimps : thm list, |
154 psimps : thm list, |
148 simple_pinducts : thm list, |
155 simple_pinducts : thm list, |
149 cases : thm, |
156 cases : thm list, |
|
157 pelims : thm list list, |
150 termination : thm, |
158 termination : thm, |
151 domintros : thm list option} |
159 domintros : thm list option} |
152 |
160 |
153 fun transform_function_data ({add_simps, case_names, fs, R, dom, psimps, pinducts, |
161 fun transform_function_data ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts, |
154 simps, inducts, termination, defname, is_partial, cases} : info) phi = |
162 simps, inducts, termination, defname, is_partial, cases, pelims, elims} : info) phi = |
155 let |
163 let |
156 val term = Morphism.term phi |
164 val term = Morphism.term phi |
157 val thm = Morphism.thm phi |
165 val thm = Morphism.thm phi |
158 val fact = Morphism.fact phi |
166 val fact = Morphism.fact phi |
159 val name = Binding.name_of o Morphism.binding phi o Binding.name |
167 val name = Binding.name_of o Morphism.binding phi o Binding.name |
160 in |
168 in |
161 { add_simps = add_simps, case_names = case_names, |
169 { add_simps = add_simps, case_names = case_names, fnames = fnames, |
162 fs = map term fs, R = term R, dom = term dom, psimps = fact psimps, |
170 fs = map term fs, R = term R, dom = term dom, psimps = fact psimps, |
163 pinducts = fact pinducts, simps = Option.map fact simps, |
171 pinducts = fact pinducts, simps = Option.map fact simps, |
164 inducts = Option.map fact inducts, termination = thm termination, |
172 inducts = Option.map fact inducts, termination = thm termination, |
165 defname = name defname, is_partial=is_partial, cases = thm cases } |
173 defname = name defname, is_partial=is_partial, cases = fact cases, |
|
174 elims = Option.map (map fact) elims, pelims = map fact pelims } |
166 end |
175 end |
167 |
176 |
168 (* FIXME just one data slot (record) per program unit *) |
177 (* FIXME just one data slot (record) per program unit *) |
169 structure FunctionData = Generic_Data |
178 structure FunctionData = Generic_Data |
170 ( |
179 ( |