author | wenzelm |
Fri, 17 Dec 2010 17:08:56 +0100 | |
changeset 41228 | e1fce873b814 |
parent 41225 | bd4ecd48c21f |
child 41941 | f823f7fae9a2 |
permissions | -rw-r--r-- |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
1 |
(* Title: HOL/Tools/Predicate_Compile/core_data.ML |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
2 |
Author: Lukas Bulwahn, TU Muenchen |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
3 |
|
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
4 |
Data of the predicate compiler core |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
5 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
6 |
*) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
7 |
signature CORE_DATA = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
8 |
sig |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
9 |
type mode = Predicate_Compile_Aux.mode |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
10 |
type compilation = Predicate_Compile_Aux.compilation |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
11 |
type compilation_funs = Predicate_Compile_Aux.compilation_funs |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
12 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
13 |
datatype predfun_data = PredfunData of { |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
14 |
definition : thm, |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
15 |
intro : thm, |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
16 |
elim : thm, |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
17 |
neg_intro : thm option |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
18 |
}; |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
19 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
20 |
datatype pred_data = PredData of { |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
21 |
intros : (string option * thm) list, |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
22 |
elim : thm option, |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
23 |
preprocessed : bool, |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
24 |
function_names : (compilation * (mode * string) list) list, |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
25 |
predfun_data : (mode * predfun_data) list, |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
26 |
needs_random : mode list |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
27 |
}; |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
28 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
29 |
structure PredData : THEORY_DATA |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
30 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
31 |
(* queries *) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
32 |
val defined_functions : compilation -> Proof.context -> string -> bool |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
33 |
val is_registered : Proof.context -> string -> bool |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
34 |
val function_name_of : compilation -> Proof.context -> string -> mode -> string |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
35 |
val the_elim_of : Proof.context -> string -> thm |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
36 |
val has_elim : Proof.context -> string -> bool |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
37 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
38 |
val needs_random : Proof.context -> string -> mode -> bool |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
39 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
40 |
val predfun_intro_of : Proof.context -> string -> mode -> thm |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
41 |
val predfun_neg_intro_of : Proof.context -> string -> mode -> thm option |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
42 |
val predfun_elim_of : Proof.context -> string -> mode -> thm |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
43 |
val predfun_definition_of : Proof.context -> string -> mode -> thm |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
44 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
45 |
val all_preds_of : Proof.context -> string list |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
46 |
val modes_of: compilation -> Proof.context -> string -> mode list |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
47 |
val all_modes_of : compilation -> Proof.context -> (string * mode list) list |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
48 |
val all_random_modes_of : Proof.context -> (string * mode list) list |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
49 |
val intros_of : Proof.context -> string -> thm list |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
50 |
val names_of : Proof.context -> string -> string option list |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
51 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
52 |
val intros_graph_of : Proof.context -> thm list Graph.T |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
53 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
54 |
(* updaters *) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
55 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
56 |
val register_predicate : (string * thm list * thm) -> theory -> theory |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
57 |
val register_intros : string * thm list -> theory -> theory |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
58 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
59 |
(* FIXME: naming of function is strange *) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
60 |
val defined_function_of : compilation -> string -> theory -> theory |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
61 |
val add_intro : string option * thm -> theory -> theory |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
62 |
val set_elim : thm -> theory -> theory |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
63 |
val set_function_name : compilation -> string -> mode -> string -> theory -> theory |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
64 |
val add_predfun_data : string -> mode -> thm * ((thm * thm) * thm option) -> theory -> theory |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
65 |
val set_needs_random : string -> mode list -> theory -> theory |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
66 |
(* sophisticated updaters *) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
67 |
val extend_intro_graph : string list -> theory -> theory |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
68 |
val preprocess_intros : string -> theory -> theory |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
69 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
70 |
(* alternative function definitions *) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
71 |
val register_alternative_function : string -> mode -> string -> theory -> theory |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
72 |
val alternative_compilation_of_global : theory -> string -> mode -> |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
73 |
(compilation_funs -> typ -> term) option |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
74 |
val alternative_compilation_of : Proof.context -> string -> mode -> |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
75 |
(compilation_funs -> typ -> term) option |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
76 |
val functional_compilation : string -> mode -> compilation_funs -> typ -> term |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
77 |
val force_modes_and_functions : string -> (mode * (string * bool)) list -> theory -> theory |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
78 |
val force_modes_and_compilations : string -> |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
79 |
(mode * ((compilation_funs -> typ -> term) * bool)) list -> theory -> theory |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
80 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
81 |
end; |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
82 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
83 |
structure Core_Data : CORE_DATA = |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
84 |
struct |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
85 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
86 |
open Predicate_Compile_Aux; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
87 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
88 |
(* book-keeping *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
89 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
90 |
datatype predfun_data = PredfunData of { |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
91 |
definition : thm, |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
92 |
intro : thm, |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
93 |
elim : thm, |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
94 |
neg_intro : thm option |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
95 |
}; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
96 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
97 |
fun rep_predfun_data (PredfunData data) = data; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
98 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
99 |
fun mk_predfun_data (definition, ((intro, elim), neg_intro)) = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
100 |
PredfunData {definition = definition, intro = intro, elim = elim, neg_intro = neg_intro} |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
101 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
102 |
datatype pred_data = PredData of { |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
103 |
intros : (string option * thm) list, |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
104 |
elim : thm option, |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
105 |
preprocessed : bool, |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
106 |
function_names : (compilation * (mode * string) list) list, |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
107 |
predfun_data : (mode * predfun_data) list, |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
108 |
needs_random : mode list |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
109 |
}; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
110 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
111 |
fun rep_pred_data (PredData data) = data; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
112 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
113 |
fun mk_pred_data (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))) = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
114 |
PredData {intros = intros, elim = elim, preprocessed = preprocessed, |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
115 |
function_names = function_names, predfun_data = predfun_data, needs_random = needs_random} |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
116 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
117 |
fun map_pred_data f (PredData {intros, elim, preprocessed, function_names, predfun_data, needs_random}) = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
118 |
mk_pred_data (f (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random)))) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
119 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
120 |
fun eq_option eq (NONE, NONE) = true |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
121 |
| eq_option eq (SOME x, SOME y) = eq (x, y) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
122 |
| eq_option eq _ = false |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
123 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
124 |
fun eq_pred_data (PredData d1, PredData d2) = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
125 |
eq_list (eq_pair (op =) Thm.eq_thm) (#intros d1, #intros d2) andalso |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
126 |
eq_option Thm.eq_thm (#elim d1, #elim d2) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
127 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
128 |
structure PredData = Theory_Data |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
129 |
( |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
130 |
type T = pred_data Graph.T; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
131 |
val empty = Graph.empty; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
132 |
val extend = I; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
133 |
val merge = Graph.merge eq_pred_data; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
134 |
); |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
135 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
136 |
(* queries *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
137 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
138 |
fun lookup_pred_data ctxt name = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
139 |
Option.map rep_pred_data (try (Graph.get_node (PredData.get (ProofContext.theory_of ctxt))) name) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
140 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
141 |
fun the_pred_data ctxt name = case lookup_pred_data ctxt name |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
142 |
of NONE => error ("No such predicate " ^ quote name) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
143 |
| SOME data => data; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
144 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
145 |
val is_registered = is_some oo lookup_pred_data |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
146 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
147 |
val all_preds_of = Graph.keys o PredData.get o ProofContext.theory_of |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
148 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
149 |
val intros_of = map snd o #intros oo the_pred_data |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
150 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
151 |
val names_of = map fst o #intros oo the_pred_data |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
152 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
153 |
fun the_elim_of ctxt name = case #elim (the_pred_data ctxt name) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
154 |
of NONE => error ("No elimination rule for predicate " ^ quote name) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
155 |
| SOME thm => thm |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
156 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
157 |
val has_elim = is_some o #elim oo the_pred_data |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
158 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
159 |
fun function_names_of compilation ctxt name = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
160 |
case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
161 |
NONE => error ("No " ^ string_of_compilation compilation |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
162 |
^ " functions defined for predicate " ^ quote name) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
163 |
| SOME fun_names => fun_names |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
164 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
165 |
fun function_name_of compilation ctxt name mode = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
166 |
case AList.lookup eq_mode |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
167 |
(function_names_of compilation ctxt name) mode of |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
168 |
NONE => error ("No " ^ string_of_compilation compilation |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
169 |
^ " function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
170 |
| SOME function_name => function_name |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
171 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
172 |
fun modes_of compilation ctxt name = map fst (function_names_of compilation ctxt name) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
173 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
174 |
fun all_modes_of compilation ctxt = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
175 |
map_filter (fn name => Option.map (pair name) (try (modes_of compilation ctxt) name)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
176 |
(all_preds_of ctxt) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
177 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
178 |
val all_random_modes_of = all_modes_of Random |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
179 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
180 |
fun defined_functions compilation ctxt name = case lookup_pred_data ctxt name of |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
181 |
NONE => false |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
182 |
| SOME data => AList.defined (op =) (#function_names data) compilation |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
183 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
184 |
fun needs_random ctxt s m = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
185 |
member (op =) (#needs_random (the_pred_data ctxt s)) m |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
186 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
187 |
fun lookup_predfun_data ctxt name mode = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
188 |
Option.map rep_predfun_data |
40140
8282b87f957c
using mode_eq instead of op = for lookup in the predicate compiler
bulwahn
parents:
40101
diff
changeset
|
189 |
(AList.lookup eq_mode (#predfun_data (the_pred_data ctxt name)) mode) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
190 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
191 |
fun the_predfun_data ctxt name mode = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
192 |
case lookup_predfun_data ctxt name mode of |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
193 |
NONE => error ("No function defined for mode " ^ string_of_mode mode ^ |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
194 |
" of predicate " ^ name) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
195 |
| SOME data => data; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
196 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
197 |
val predfun_definition_of = #definition ooo the_predfun_data |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
198 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
199 |
val predfun_intro_of = #intro ooo the_predfun_data |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
200 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
201 |
val predfun_elim_of = #elim ooo the_predfun_data |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
202 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
203 |
val predfun_neg_intro_of = #neg_intro ooo the_predfun_data |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
204 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
205 |
val intros_graph_of = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
206 |
Graph.map (K (map snd o #intros o rep_pred_data)) o PredData.get o ProofContext.theory_of |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
207 |
|
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
208 |
fun prove_casesrule ctxt (pred, (pre_cases_rule, nparams)) cases_rule = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
209 |
let |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
210 |
val thy = ProofContext.theory_of ctxt |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
211 |
val nargs = length (binder_types (fastype_of pred)) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
212 |
fun PEEK f dependent_tactic st = dependent_tactic (f st) st |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
213 |
fun meta_eq_of th = th RS @{thm eq_reflection} |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
214 |
val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}] |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
215 |
fun instantiate i n {context = ctxt, params = p, prems = prems, |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
216 |
asms = a, concl = cl, schematics = s} = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
217 |
let |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
218 |
fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
219 |
fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
220 |
|> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
221 |
val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems) |
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41225
diff
changeset
|
222 |
val case_th = Raw_Simplifier.simplify true |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
223 |
(@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1)) |
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41225
diff
changeset
|
224 |
val prems' = maps (dest_conjunct_prem o Raw_Simplifier.simplify true tuple_rew_rules) prems |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
225 |
val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th)) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
226 |
val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
227 |
OF (replicate nargs @{thm refl}) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
228 |
val thesis = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
229 |
Thm.instantiate ([], inst_of_matches (prems_of case_th' ~~ map prop_of prems')) case_th' |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
230 |
OF prems' |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
231 |
in |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
232 |
(rtac thesis 1) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
233 |
end |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
234 |
val tac = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
235 |
etac pre_cases_rule 1 |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
236 |
THEN |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
237 |
(PEEK nprems_of |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
238 |
(fn n => |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
239 |
ALLGOALS (fn i => |
41225 | 240 |
Simplifier.rewrite_goal_tac [@{thm split_paired_all}] i |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
241 |
THEN (SUBPROOF (instantiate i n) ctxt i)))) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
242 |
in |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
243 |
Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
244 |
end |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
245 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
246 |
(* updaters *) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
247 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
248 |
(* fetching introduction rules or registering introduction rules *) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
249 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
250 |
val no_compilation = ([], ([], [])) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
251 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
252 |
fun fetch_pred_data ctxt name = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
253 |
case try (Inductive.the_inductive ctxt) name of |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
254 |
SOME (info as (_, result)) => |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
255 |
let |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
256 |
fun is_intro_of intro = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
257 |
let |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
258 |
val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro)) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
259 |
in (fst (dest_Const const) = name) end; |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
260 |
val thy = ProofContext.theory_of ctxt |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
261 |
val intros = map (preprocess_intro thy) (filter is_intro_of (#intrs result)) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
262 |
val index = find_index (fn s => s = name) (#names (fst info)) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
263 |
val pre_elim = nth (#elims result) index |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
264 |
val pred = nth (#preds result) index |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
265 |
val elim_t = mk_casesrule ctxt pred intros |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
266 |
val nparams = length (Inductive.params_of (#raw_induct result)) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
267 |
val elim = prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
268 |
in |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
269 |
mk_pred_data (((map (pair NONE) intros, SOME elim), true), no_compilation) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
270 |
end |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
271 |
| NONE => error ("No such predicate: " ^ quote name) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
272 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
273 |
fun add_predfun_data name mode data = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
274 |
let |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
275 |
val add = (apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data)) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
276 |
in PredData.map (Graph.map_node name (map_pred_data add)) end |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
277 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
278 |
fun is_inductive_predicate ctxt name = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
279 |
is_some (try (Inductive.the_inductive ctxt) name) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
280 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
281 |
fun depending_preds_of ctxt (key, value) = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
282 |
let |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
283 |
val intros = map (Thm.prop_of o snd) ((#intros o rep_pred_data) value) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
284 |
in |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
285 |
fold Term.add_const_names intros [] |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
286 |
|> (fn cs => |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
287 |
if member (op =) cs @{const_name "HOL.eq"} then |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
288 |
insert (op =) @{const_name Predicate.eq} cs |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
289 |
else cs) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
290 |
|> filter (fn c => (not (c = key)) andalso |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
291 |
(is_inductive_predicate ctxt c orelse is_registered ctxt c)) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
292 |
end; |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
293 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
294 |
fun add_intro (opt_case_name, thm) thy = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
295 |
let |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
296 |
val (name, T) = dest_Const (fst (strip_intro_concl thm)) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
297 |
fun cons_intro gr = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
298 |
case try (Graph.get_node gr) name of |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
299 |
SOME pred_data => Graph.map_node name (map_pred_data |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
300 |
(apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)]))))) gr |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
301 |
| NONE => Graph.new_node (name, mk_pred_data ((([(opt_case_name, thm)], NONE), false), no_compilation)) gr |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
302 |
in PredData.map cons_intro thy end |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
303 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
304 |
fun set_elim thm = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
305 |
let |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
306 |
val (name, _) = dest_Const (fst |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
307 |
(strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm))))) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
308 |
in PredData.map (Graph.map_node name (map_pred_data (apfst (apfst (apsnd (K (SOME thm))))))) end |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
309 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
310 |
fun register_predicate (constname, intros, elim) thy = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
311 |
let |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
312 |
val named_intros = map (pair NONE) intros |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
313 |
in |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
314 |
if not (member (op =) (Graph.keys (PredData.get thy)) constname) then |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
315 |
PredData.map |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
316 |
(Graph.new_node (constname, |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
317 |
mk_pred_data (((named_intros, SOME elim), false), no_compilation))) thy |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
318 |
else thy |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
319 |
end |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
320 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
321 |
fun register_intros (constname, pre_intros) thy = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
322 |
let |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
323 |
val T = Sign.the_const_type thy constname |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
324 |
fun constname_of_intro intr = fst (dest_Const (fst (strip_intro_concl intr))) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
325 |
val _ = if not (forall (fn intr => constname_of_intro intr = constname) pre_intros) then |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
326 |
error ("register_intros: Introduction rules of different constants are used\n" ^ |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
327 |
"expected rules for " ^ constname ^ ", but received rules for " ^ |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
328 |
commas (map constname_of_intro pre_intros)) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
329 |
else () |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
330 |
val pred = Const (constname, T) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
331 |
val pre_elim = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
332 |
(Drule.export_without_context o Skip_Proof.make_thm thy) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
333 |
(mk_casesrule (ProofContext.init_global thy) pred pre_intros) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
334 |
in register_predicate (constname, pre_intros, pre_elim) thy end |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
335 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
336 |
fun defined_function_of compilation pred = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
337 |
let |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
338 |
val set = (apsnd o apfst) (cons (compilation, [])) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
339 |
in |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
340 |
PredData.map (Graph.map_node pred (map_pred_data set)) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
341 |
end |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
342 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
343 |
fun set_function_name compilation pred mode name = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
344 |
let |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
345 |
val set = (apsnd o apfst) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
346 |
(AList.map_default (op =) (compilation, [(mode, name)]) (cons (mode, name))) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
347 |
in |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
348 |
PredData.map (Graph.map_node pred (map_pred_data set)) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
349 |
end |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
350 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
351 |
fun set_needs_random name modes = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
352 |
let |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
353 |
val set = (apsnd o apsnd o apsnd) (K modes) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
354 |
in |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
355 |
PredData.map (Graph.map_node name (map_pred_data set)) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
356 |
end |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
357 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
358 |
fun extend' value_of edges_of key (G, visited) = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
359 |
let |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
360 |
val (G', v) = case try (Graph.get_node G) key of |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
361 |
SOME v => (G, v) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
362 |
| NONE => (Graph.new_node (key, value_of key) G, value_of key) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
363 |
val (G'', visited') = fold (extend' value_of edges_of) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
364 |
(subtract (op =) visited (edges_of (key, v))) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
365 |
(G', key :: visited) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
366 |
in |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
367 |
(fold (Graph.add_edge o (pair key)) (edges_of (key, v)) G'', visited') |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
368 |
end; |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
369 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
370 |
fun extend value_of edges_of key G = fst (extend' value_of edges_of key (G, [])) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
371 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
372 |
fun extend_intro_graph names thy = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
373 |
let |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
374 |
val ctxt = ProofContext.init_global thy |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
375 |
in |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
376 |
PredData.map (fold (extend (fetch_pred_data ctxt) (depending_preds_of ctxt)) names) thy |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
377 |
end |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
378 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
379 |
fun preprocess_intros name thy = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
380 |
PredData.map (Graph.map_node name (map_pred_data (apfst (fn (rules, preprocessed) => |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
381 |
if preprocessed then (rules, preprocessed) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
382 |
else |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
383 |
let |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
384 |
val (named_intros, SOME elim) = rules |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
385 |
val named_intros' = map (apsnd (preprocess_intro thy)) named_intros |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
386 |
val pred = Const (name, Sign.the_const_type thy name) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
387 |
val ctxt = ProofContext.init_global thy |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
388 |
val elim_t = mk_casesrule ctxt pred (map snd named_intros') |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
389 |
val nparams = (case try (Inductive.the_inductive ctxt) name of |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
390 |
SOME (_, result) => length (Inductive.params_of (#raw_induct result)) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
391 |
| NONE => 0) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
392 |
val elim' = prove_casesrule ctxt (pred, (elim, 0)) elim_t |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
393 |
in |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
394 |
((named_intros', SOME elim'), true) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
395 |
end)))) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
396 |
thy |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
397 |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
398 |
(* registration of alternative function names *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
399 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
400 |
structure Alt_Compilations_Data = Theory_Data |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
401 |
( |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
402 |
type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
403 |
val empty = Symtab.empty; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
404 |
val extend = I; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
405 |
fun merge data : T = Symtab.merge (K true) data; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
406 |
); |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
407 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
408 |
fun alternative_compilation_of_global thy pred_name mode = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
409 |
AList.lookup eq_mode (Symtab.lookup_list (Alt_Compilations_Data.get thy) pred_name) mode |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
410 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
411 |
fun alternative_compilation_of ctxt pred_name mode = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
412 |
AList.lookup eq_mode |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
413 |
(Symtab.lookup_list (Alt_Compilations_Data.get (ProofContext.theory_of ctxt)) pred_name) mode |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
414 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
415 |
fun force_modes_and_compilations pred_name compilations = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
416 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
417 |
(* thm refl is a dummy thm *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
418 |
val modes = map fst compilations |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
419 |
val (needs_random, non_random_modes) = pairself (map fst) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
420 |
(List.partition (fn (m, (fun_name, random)) => random) compilations) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
421 |
val non_random_dummys = map (rpair "dummy") non_random_modes |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
422 |
val all_dummys = map (rpair "dummy") modes |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
423 |
val dummy_function_names = map (rpair all_dummys) Predicate_Compile_Aux.random_compilations |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
424 |
@ map (rpair non_random_dummys) Predicate_Compile_Aux.non_random_compilations |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
425 |
val alt_compilations = map (apsnd fst) compilations |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
426 |
in |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
427 |
PredData.map (Graph.new_node |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
428 |
(pred_name, mk_pred_data ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random))))) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
429 |
#> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
430 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
431 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
432 |
fun functional_compilation fun_name mode compfuns T = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
433 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
434 |
val (inpTs, outpTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
435 |
mode (binder_types T) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
436 |
val bs = map (pair "x") inpTs |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
437 |
val bounds = map Bound (rev (0 upto (length bs) - 1)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
438 |
val f = Const (fun_name, inpTs ---> HOLogic.mk_tupleT outpTs) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
439 |
in list_abs (bs, mk_single compfuns (list_comb (f, bounds))) end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
440 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
441 |
fun register_alternative_function pred_name mode fun_name = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
442 |
Alt_Compilations_Data.map (Symtab.insert_list (eq_pair eq_mode (K false)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
443 |
(pred_name, (mode, functional_compilation fun_name mode))) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
444 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
445 |
fun force_modes_and_functions pred_name fun_names = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
446 |
force_modes_and_compilations pred_name |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
447 |
(map (fn (mode, (fun_name, random)) => (mode, (functional_compilation fun_name mode, random))) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
448 |
fun_names) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
449 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
450 |
end; |