author | wenzelm |
Sat, 18 Jul 2015 20:47:08 +0200 | |
changeset 60752 | b48830b670a1 |
parent 60642 | 48dd1cefb4ae |
child 61424 | c3658c18b7bc |
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 |
|
41941 | 4 |
Data of the predicate compiler core. |
5 |
*) |
|
40053
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 |
59501 | 12 |
|
40053
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 { |
55543 | 21 |
pos : Position.T, |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
22 |
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
|
23 |
elim : thm option, |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
24 |
preprocessed : bool, |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
25 |
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
|
26 |
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
|
27 |
needs_random : mode list |
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 |
|
58823 | 30 |
structure PredData : THEORY_DATA (* FIXME keep data private *) |
59501 | 31 |
|
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
32 |
(* queries *) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
33 |
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
|
34 |
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
|
35 |
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
|
36 |
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
|
37 |
val has_elim : Proof.context -> string -> bool |
59501 | 38 |
|
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
39 |
val needs_random : Proof.context -> string -> mode -> bool |
59501 | 40 |
|
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
41 |
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
|
42 |
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
|
43 |
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
|
44 |
val predfun_definition_of : Proof.context -> string -> mode -> thm |
59501 | 45 |
|
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
46 |
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
|
47 |
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
|
48 |
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
|
49 |
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
|
50 |
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
|
51 |
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
|
52 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
53 |
val intros_graph_of : Proof.context -> thm list Graph.T |
59501 | 54 |
|
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
55 |
(* updaters *) |
59501 | 56 |
|
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
57 |
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
|
58 |
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
|
59 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
60 |
(* 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
|
61 |
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
|
62 |
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
|
63 |
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
|
64 |
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
|
65 |
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
|
66 |
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
|
67 |
(* sophisticated updaters *) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
68 |
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
|
69 |
val preprocess_intros : string -> theory -> theory |
59501 | 70 |
|
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
71 |
(* alternative function definitions *) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
72 |
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
|
73 |
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
|
74 |
(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
|
75 |
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
|
76 |
(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
|
77 |
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
|
78 |
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
|
79 |
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
|
80 |
(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
|
81 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
82 |
end; |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
83 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
84 |
structure Core_Data : CORE_DATA = |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
85 |
struct |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
86 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
87 |
open Predicate_Compile_Aux; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
88 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
89 |
(* book-keeping *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
90 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
91 |
datatype predfun_data = PredfunData of { |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
92 |
definition : thm, |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
93 |
intro : thm, |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
94 |
elim : thm, |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
95 |
neg_intro : thm option |
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 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
98 |
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
|
99 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
100 |
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
|
101 |
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
|
102 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
103 |
datatype pred_data = PredData of { |
55543 | 104 |
pos: Position.T, |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
105 |
intros : (string option * thm) list, |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
106 |
elim : thm option, |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
107 |
preprocessed : bool, |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
108 |
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
|
109 |
predfun_data : (mode * predfun_data) list, |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
110 |
needs_random : mode list |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
111 |
}; |
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 rep_pred_data (PredData data) = data; |
55543 | 114 |
val pos_of = #pos o rep_pred_data; |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
115 |
|
55543 | 116 |
fun mk_pred_data |
117 |
(pos, (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random)))) = |
|
118 |
PredData {pos = pos, intros = intros, elim = elim, preprocessed = preprocessed, |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
119 |
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
|
120 |
|
55543 | 121 |
fun map_pred_data f |
122 |
(PredData {pos, intros, elim, preprocessed, function_names, predfun_data, needs_random}) = |
|
123 |
mk_pred_data |
|
124 |
(f (pos, (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))))) |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
125 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
126 |
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
|
127 |
| 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
|
128 |
| eq_option eq _ = false |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
129 |
|
59501 | 130 |
fun eq_pred_data (PredData d1, PredData d2) = |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
131 |
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
|
132 |
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
|
133 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
134 |
structure PredData = Theory_Data |
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 |
type T = pred_data Graph.T; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
137 |
val empty = Graph.empty; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
138 |
val extend = I; |
55543 | 139 |
val merge = |
140 |
Graph.join (fn key => fn (x, y) => |
|
141 |
if eq_pred_data (x, y) |
|
142 |
then raise Graph.SAME |
|
143 |
else |
|
144 |
error ("Duplicate predicate declarations for " ^ quote key ^ |
|
145 |
Position.here (pos_of x) ^ Position.here (pos_of y))); |
|
40052
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 |
|
55437 | 148 |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
149 |
(* queries *) |
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 |
fun lookup_pred_data ctxt name = |
42361 | 152 |
Option.map rep_pred_data (try (Graph.get_node (PredData.get (Proof_Context.theory_of ctxt))) name) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
153 |
|
55437 | 154 |
fun the_pred_data ctxt name = |
155 |
(case lookup_pred_data ctxt name of |
|
59501 | 156 |
NONE => error ("No such predicate: " ^ quote name) |
55437 | 157 |
| SOME data => data) |
40052
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 |
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
|
160 |
|
42361 | 161 |
val all_preds_of = Graph.keys o PredData.get o Proof_Context.theory_of |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
162 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
163 |
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
|
164 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
165 |
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
|
166 |
|
55437 | 167 |
fun the_elim_of ctxt name = |
168 |
(case #elim (the_pred_data ctxt name) of |
|
169 |
NONE => error ("No elimination rule for predicate " ^ quote name) |
|
170 |
| SOME thm => thm) |
|
59501 | 171 |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
172 |
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
|
173 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
174 |
fun function_names_of compilation ctxt name = |
55437 | 175 |
(case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of |
176 |
NONE => |
|
177 |
error ("No " ^ string_of_compilation compilation ^ |
|
178 |
" functions defined for predicate " ^ quote name) |
|
179 |
| SOME fun_names => fun_names) |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
180 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
181 |
fun function_name_of compilation ctxt name mode = |
55437 | 182 |
(case AList.lookup eq_mode (function_names_of compilation ctxt name) mode of |
183 |
NONE => |
|
184 |
error ("No " ^ string_of_compilation compilation ^ |
|
185 |
" function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name) |
|
186 |
| SOME function_name => function_name) |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
187 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
188 |
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
|
189 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
190 |
fun all_modes_of compilation ctxt = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
191 |
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
|
192 |
(all_preds_of ctxt) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
193 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
194 |
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
|
195 |
|
55437 | 196 |
fun defined_functions compilation ctxt name = |
197 |
(case lookup_pred_data ctxt name of |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
198 |
NONE => false |
55437 | 199 |
| SOME data => AList.defined (op =) (#function_names data) compilation) |
40052
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 |
fun needs_random ctxt s m = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
202 |
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
|
203 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
204 |
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
|
205 |
Option.map rep_predfun_data |
40140
8282b87f957c
using mode_eq instead of op = for lookup in the predicate compiler
bulwahn
parents:
40101
diff
changeset
|
206 |
(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
|
207 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
208 |
fun the_predfun_data ctxt name mode = |
55437 | 209 |
(case lookup_predfun_data ctxt name mode of |
210 |
NONE => |
|
211 |
error ("No function defined for mode " ^ string_of_mode mode ^ |
|
212 |
" of predicate " ^ name) |
|
213 |
| SOME data => data) |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
214 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
215 |
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
|
216 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
217 |
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
|
218 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
219 |
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
|
220 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
221 |
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
|
222 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
223 |
val intros_graph_of = |
42361 | 224 |
Graph.map (K (map snd o #intros o rep_pred_data)) o PredData.get o Proof_Context.theory_of |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
225 |
|
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
226 |
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
|
227 |
let |
42361 | 228 |
val thy = Proof_Context.theory_of ctxt |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
229 |
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
|
230 |
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
|
231 |
val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}] |
59501 | 232 |
|
233 |
fun instantiate i n ({context = ctxt2, prems, ...}: Subgoal.focus) = |
|
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
234 |
let |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59636
diff
changeset
|
235 |
fun inst_pair_of (ix, (ty, t)) = ((ix, ty), t) |
59501 | 236 |
fun inst_of_matches tts = |
237 |
fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty) |
|
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59636
diff
changeset
|
238 |
|> snd |> Vartab.dest |> map (apsnd (Thm.cterm_of ctxt2) o inst_pair_of) |
59501 | 239 |
val (cases, (eqs, prems1)) = apsnd (chop (nargs - nparams)) (chop n prems) |
52230 | 240 |
val case_th = |
59501 | 241 |
rewrite_rule ctxt2 (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1)) |
242 |
val prems2 = maps (dest_conjunct_prem o rewrite_rule ctxt2 tuple_rew_rules) prems1 |
|
55437 | 243 |
val pats = |
59501 | 244 |
map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) |
245 |
(take nargs (Thm.prems_of case_th)) |
|
246 |
val case_th' = |
|
247 |
Thm.instantiate ([], inst_of_matches pats) case_th |
|
248 |
OF replicate nargs @{thm refl} |
|
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
249 |
val thesis = |
59582 | 250 |
Thm.instantiate ([], inst_of_matches (Thm.prems_of case_th' ~~ map Thm.prop_of prems2)) |
251 |
case_th' OF prems2 |
|
60752 | 252 |
in resolve_tac ctxt2 [thesis] 1 end |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
253 |
in |
59501 | 254 |
Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule |
255 |
(fn {context = ctxt1, ...} => |
|
256 |
eresolve_tac ctxt1 [pre_cases_rule] 1 THEN (fn st => |
|
257 |
let val n = Thm.nprems_of st in |
|
258 |
st |> ALLGOALS (fn i => |
|
259 |
rewrite_goal_tac ctxt1 @{thms split_paired_all} i THEN |
|
260 |
SUBPROOF (instantiate i n) ctxt1 i) |
|
261 |
end)) |
|
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
262 |
end |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
263 |
|
55437 | 264 |
|
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
265 |
(* updaters *) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
266 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
267 |
(* 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
|
268 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
269 |
val no_compilation = ([], ([], [])) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
270 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
271 |
fun fetch_pred_data ctxt name = |
55437 | 272 |
(case try (Inductive.the_inductive ctxt) name of |
59501 | 273 |
SOME (info as (_, result)) => |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
274 |
let |
55543 | 275 |
val thy = Proof_Context.theory_of ctxt |
276 |
||
277 |
val pos = Position.thread_data () |
|
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
278 |
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
|
279 |
let |
59582 | 280 |
val (const, _) = strip_comb (HOLogic.dest_Trueprop (Thm.concl_of intro)) |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
281 |
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
|
282 |
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
|
283 |
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
|
284 |
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
|
285 |
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
|
286 |
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
|
287 |
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
|
288 |
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
|
289 |
in |
55543 | 290 |
mk_pred_data (pos, (((map (pair NONE) intros, SOME elim), true), no_compilation)) |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
291 |
end |
55437 | 292 |
| NONE => error ("No such predicate: " ^ quote name)) |
40053
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_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
|
295 |
let |
55543 | 296 |
val add = (apsnd o apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data)) |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
297 |
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
|
298 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
299 |
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
|
300 |
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
|
301 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
302 |
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
|
303 |
let |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
304 |
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
|
305 |
in |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
306 |
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
|
307 |
|> (fn cs => |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
308 |
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
|
309 |
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
|
310 |
else cs) |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
311 |
|> 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
|
312 |
(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
|
313 |
end; |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
314 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
315 |
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
|
316 |
let |
50056 | 317 |
val (name, _) = dest_Const (fst (strip_intro_concl thm)) |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
318 |
fun cons_intro gr = |
55437 | 319 |
(case try (Graph.get_node gr) name of |
320 |
SOME _ => |
|
321 |
Graph.map_node name (map_pred_data |
|
55543 | 322 |
(apsnd (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)])))))) gr |
55437 | 323 |
| NONE => |
324 |
Graph.new_node |
|
55543 | 325 |
(name, |
326 |
mk_pred_data (Position.thread_data (), |
|
327 |
(((([(opt_case_name, thm)], NONE), false), no_compilation)))) gr) |
|
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
328 |
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
|
329 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
330 |
fun set_elim thm = |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
331 |
let |
55437 | 332 |
val (name, _) = |
59582 | 333 |
dest_Const (fst (strip_comb (HOLogic.dest_Trueprop (hd (Thm.prems_of thm))))) |
55543 | 334 |
in |
335 |
PredData.map (Graph.map_node name (map_pred_data (apsnd (apfst (apfst (apsnd (K (SOME thm)))))))) |
|
336 |
end |
|
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
337 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
338 |
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
|
339 |
let |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
340 |
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
|
341 |
in |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
342 |
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
|
343 |
PredData.map |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
344 |
(Graph.new_node (constname, |
55543 | 345 |
mk_pred_data (Position.thread_data (), |
346 |
(((named_intros, SOME elim), false), no_compilation)))) thy |
|
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
347 |
else thy |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
348 |
end |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
349 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
350 |
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
|
351 |
let |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
352 |
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
|
353 |
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
|
354 |
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
|
355 |
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
|
356 |
"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
|
357 |
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
|
358 |
else () |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
359 |
val pred = Const (constname, T) |
59501 | 360 |
val pre_elim = |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
361 |
(Drule.export_without_context o Skip_Proof.make_thm thy) |
42361 | 362 |
(mk_casesrule (Proof_Context.init_global thy) pred pre_intros) |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
363 |
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
|
364 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
365 |
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
|
366 |
let |
55543 | 367 |
val set = (apsnd o apsnd o apfst) (cons (compilation, [])) |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
368 |
in |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
369 |
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
|
370 |
end |
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 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
|
373 |
let |
55543 | 374 |
val set = (apsnd o apsnd o apfst) |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
375 |
(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
|
376 |
in |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
377 |
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
|
378 |
end |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
379 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
380 |
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
|
381 |
let |
55543 | 382 |
val set = (apsnd o apsnd o apsnd o apsnd) (K modes) |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
383 |
in |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
384 |
PredData.map (Graph.map_node name (map_pred_data set)) |
59501 | 385 |
end |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
386 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
387 |
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
|
388 |
let |
55437 | 389 |
val (G', v) = |
390 |
(case try (Graph.get_node G) key of |
|
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
391 |
SOME v => (G, v) |
55437 | 392 |
| NONE => (Graph.new_node (key, value_of key) G, value_of key)) |
393 |
val (G'', visited') = |
|
394 |
fold (extend' value_of edges_of) |
|
395 |
(subtract (op =) visited (edges_of (key, v))) |
|
396 |
(G', key :: visited) |
|
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
397 |
in |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
398 |
(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
|
399 |
end; |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
400 |
|
59501 | 401 |
fun extend value_of edges_of key G = fst (extend' value_of edges_of key (G, [])) |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
402 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
403 |
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
|
404 |
let |
42361 | 405 |
val ctxt = Proof_Context.init_global thy |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
406 |
in |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
407 |
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
|
408 |
end |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
409 |
|
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
410 |
fun preprocess_intros name thy = |
55543 | 411 |
PredData.map (Graph.map_node name (map_pred_data (apsnd (apfst (fn (rules, preprocessed) => |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
412 |
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
|
413 |
else |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
414 |
let |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
415 |
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
|
416 |
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
|
417 |
val pred = Const (name, Sign.the_const_type thy name) |
42361 | 418 |
val ctxt = Proof_Context.init_global thy |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
419 |
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
|
420 |
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
|
421 |
in |
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
422 |
((named_intros', SOME elim'), true) |
55543 | 423 |
end))))) |
59501 | 424 |
thy |
40053
3fa49ea76cbb
using a signature in core_data and moving some more functions to core_data
bulwahn
parents:
40052
diff
changeset
|
425 |
|
55437 | 426 |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
427 |
(* registration of alternative function names *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
428 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
429 |
structure Alt_Compilations_Data = Theory_Data |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
430 |
( |
55437 | 431 |
type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table |
432 |
val empty = Symtab.empty |
|
433 |
val extend = I |
|
434 |
fun merge data : T = Symtab.merge (K true) data |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
435 |
); |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
436 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
437 |
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
|
438 |
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
|
439 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
440 |
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
|
441 |
AList.lookup eq_mode |
42361 | 442 |
(Symtab.lookup_list (Alt_Compilations_Data.get (Proof_Context.theory_of ctxt)) pred_name) mode |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
443 |
|
55543 | 444 |
fun force_modes_and_compilations pred_name compilations thy = |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
445 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
446 |
(* thm refl is a dummy thm *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
447 |
val modes = map fst compilations |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58823
diff
changeset
|
448 |
val (needs_random, non_random_modes) = |
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58823
diff
changeset
|
449 |
apply2 (map fst) (List.partition (fn (_, (_, random)) => random) compilations) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
450 |
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
|
451 |
val all_dummys = map (rpair "dummy") modes |
55437 | 452 |
val dummy_function_names = |
453 |
map (rpair all_dummys) Predicate_Compile_Aux.random_compilations @ |
|
454 |
map (rpair non_random_dummys) Predicate_Compile_Aux.non_random_compilations |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
455 |
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
|
456 |
in |
55543 | 457 |
thy |> |
55437 | 458 |
PredData.map |
459 |
(Graph.new_node |
|
460 |
(pred_name, |
|
55543 | 461 |
mk_pred_data |
462 |
(Position.thread_data (), |
|
463 |
((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random)))))) |
|
464 |
|> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations)) |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
465 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
466 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
467 |
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
|
468 |
let |
55437 | 469 |
val (inpTs, outpTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
470 |
val bs = map (pair "x") inpTs |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
471 |
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
|
472 |
val f = Const (fun_name, inpTs ---> HOLogic.mk_tupleT outpTs) |
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
42361
diff
changeset
|
473 |
in fold_rev Term.abs bs (mk_single compfuns (list_comb (f, bounds))) end |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
474 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
475 |
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
|
476 |
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
|
477 |
(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
|
478 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
479 |
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
|
480 |
force_modes_and_compilations pred_name |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
481 |
(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
|
482 |
fun_names) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
483 |
|
55437 | 484 |
end |