author | bulwahn |
Thu, 11 Jun 2009 21:37:26 +0200 | |
changeset 31573 | 0047df9eb347 |
parent 31551 | 995d6b90e9d6 |
child 31574 | 3517d6e6a250 |
permissions | -rw-r--r-- |
31217 | 1 |
(* Author: Lukas Bulwahn, TU Muenchen |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
2 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
3 |
(Prototype of) A compiler from predicates specified by intro/elim rules |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
4 |
to equations. |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
5 |
*) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
6 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
7 |
signature PREDICATE_COMPILE = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
8 |
sig |
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
9 |
type mode = int list option list * int list |
31514 | 10 |
val add_equations_of: string list -> theory -> theory |
11 |
val register_predicate : (thm list * thm * int) -> theory -> theory |
|
12 |
val predfun_intro_of: theory -> string -> mode -> thm |
|
13 |
val predfun_elim_of: theory -> string -> mode -> thm |
|
14 |
val strip_intro_concl: int -> term -> term * (term list * term list) |
|
15 |
val predfun_name_of: theory -> string -> mode -> string |
|
16 |
val all_preds_of : theory -> string list |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
17 |
val modes_of: theory -> string -> mode list |
31514 | 18 |
val intros_of: theory -> string -> thm list |
19 |
val nparams_of: theory -> string -> int |
|
31124 | 20 |
val setup: theory -> theory |
21 |
val code_pred: string -> Proof.context -> Proof.state |
|
22 |
val code_pred_cmd: string -> Proof.context -> Proof.state |
|
31514 | 23 |
(* val print_alternative_rules: theory -> theory (*FIXME diagnostic command?*) *) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
24 |
val do_proofs: bool ref |
31217 | 25 |
val analyze_compr: theory -> term -> term |
26 |
val eval_ref: (unit -> term Predicate.pred) option ref |
|
31514 | 27 |
val add_equations : string -> theory -> theory |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
28 |
end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
29 |
|
31124 | 30 |
structure Predicate_Compile : PREDICATE_COMPILE = |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
31 |
struct |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
32 |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
33 |
(** auxiliary **) |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
34 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
35 |
(* debug stuff *) |
31320
72eeb1b4e006
provide local dummy version of makestring -- NB: makestring is fragile and not portable, it should not occur in repository sources;
wenzelm
parents:
31284
diff
changeset
|
36 |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
37 |
fun tracing s = (if ! Toplevel.debug then Output.tracing s else ()); |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
38 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
39 |
fun print_tac s = (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); |
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
40 |
fun new_print_tac s = Tactical.print_tac s |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
41 |
fun debug_tac msg = (fn st => (Output.tracing msg; Seq.single st)); |
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
42 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
43 |
val do_proofs = ref true; |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
44 |
|
31514 | 45 |
fun mycheat_tac thy i st = |
46 |
(Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) i) st |
|
47 |
||
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
48 |
fun remove_last_goal thy st = |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
49 |
(Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) (nprems_of st)) st |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
50 |
|
31514 | 51 |
(* reference to preprocessing of InductiveSet package *) |
52 |
||
53 |
val ind_set_codegen_preproc = InductiveSetPackage.codegen_preproc; |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
54 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
55 |
(** fundamentals **) |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
56 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
57 |
(* syntactic operations *) |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
58 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
59 |
fun mk_eq (x, xs) = |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
60 |
let fun mk_eqs _ [] = [] |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
61 |
| mk_eqs a (b::cs) = |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
62 |
HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
63 |
in mk_eqs x xs end; |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
64 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
65 |
fun mk_tupleT [] = HOLogic.unitT |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
66 |
| mk_tupleT Ts = foldr1 HOLogic.mk_prodT Ts; |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
67 |
|
31514 | 68 |
fun dest_tupleT (Type (@{type_name Product_Type.unit}, [])) = [] |
69 |
| dest_tupleT (Type (@{type_name "*"}, [T1, T2])) = T1 :: (dest_tupleT T2) |
|
70 |
| dest_tupleT t = [t] |
|
71 |
||
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
72 |
fun mk_tuple [] = HOLogic.unit |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
73 |
| mk_tuple ts = foldr1 HOLogic.mk_prod ts; |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
74 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
75 |
fun dest_tuple (Const (@{const_name Product_Type.Unity}, _)) = [] |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
76 |
| dest_tuple (Const (@{const_name Pair}, _) $ t1 $ t2) = t1 :: (dest_tuple t2) |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
77 |
| dest_tuple t = [t] |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
78 |
|
31514 | 79 |
fun mk_pred_enumT T = Type (@{type_name "Predicate.pred"}, [T]) |
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
80 |
|
31514 | 81 |
fun dest_pred_enumT (Type (@{type_name "Predicate.pred"}, [T])) = T |
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
82 |
| dest_pred_enumT T = raise TYPE ("dest_pred_enumT", [T], []); |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
83 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
84 |
fun mk_Enum f = |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
85 |
let val T as Type ("fun", [T', _]) = fastype_of f |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
86 |
in |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
87 |
Const (@{const_name Predicate.Pred}, T --> mk_pred_enumT T') $ f |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
88 |
end; |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
89 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
90 |
fun mk_Eval (f, x) = |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
91 |
let val T = fastype_of x |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
92 |
in |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
93 |
Const (@{const_name Predicate.eval}, mk_pred_enumT T --> T --> HOLogic.boolT) $ f $ x |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
94 |
end; |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
95 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
96 |
fun mk_empty T = Const (@{const_name Orderings.bot}, mk_pred_enumT T); |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
97 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
98 |
fun mk_single t = |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
99 |
let val T = fastype_of t |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
100 |
in Const(@{const_name Predicate.single}, T --> mk_pred_enumT T) $ t end; |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
101 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
102 |
fun mk_bind (x, f) = |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
103 |
let val T as Type ("fun", [_, U]) = fastype_of f |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
104 |
in |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
105 |
Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
106 |
end; |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
107 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
108 |
val mk_sup = HOLogic.mk_binop @{const_name sup}; |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
109 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
110 |
fun mk_if_predenum cond = Const (@{const_name Predicate.if_pred}, |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
111 |
HOLogic.boolT --> mk_pred_enumT HOLogic.unitT) $ cond; |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
112 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
113 |
fun mk_not_pred t = let val T = mk_pred_enumT HOLogic.unitT |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
114 |
in Const (@{const_name Predicate.not_pred}, T --> T) $ t end |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
115 |
|
31514 | 116 |
(* destruction of intro rules *) |
117 |
||
118 |
(* FIXME: look for other place where this functionality was used before *) |
|
119 |
fun strip_intro_concl nparams intro = let |
|
120 |
val _ $ u = Logic.strip_imp_concl intro |
|
121 |
val (pred, all_args) = strip_comb u |
|
122 |
val (params, args) = chop nparams all_args |
|
123 |
in (pred, (params, args)) end |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
124 |
|
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
125 |
(* data structures *) |
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
126 |
|
31514 | 127 |
type mode = int list option list * int list; (*pmode FIMXE*) |
128 |
||
129 |
fun string_of_mode (iss, is) = space_implode " -> " (map |
|
130 |
(fn NONE => "X" |
|
131 |
| SOME js => enclose "[" "]" (commas (map string_of_int js))) |
|
132 |
(iss @ [SOME is])); |
|
133 |
||
134 |
fun print_modes modes = Output.tracing ("Inferred modes:\n" ^ |
|
135 |
cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map |
|
136 |
string_of_mode ms)) modes)); |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
137 |
|
31573
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
138 |
|
31514 | 139 |
datatype predfun_data = PredfunData of { |
140 |
name : string, |
|
141 |
definition : thm, |
|
142 |
intro : thm, |
|
143 |
elim : thm |
|
144 |
}; |
|
145 |
||
146 |
fun rep_predfun_data (PredfunData data) = data; |
|
147 |
fun mk_predfun_data (name, definition, intro, elim) = |
|
148 |
PredfunData {name = name, definition = definition, intro = intro, elim = elim} |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
149 |
|
31514 | 150 |
datatype pred_data = PredData of { |
151 |
intros : thm list, |
|
152 |
elim : thm option, |
|
153 |
nparams : int, |
|
154 |
functions : (mode * predfun_data) list |
|
155 |
}; |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
156 |
|
31514 | 157 |
fun rep_pred_data (PredData data) = data; |
158 |
fun mk_pred_data ((intros, elim, nparams), functions) = |
|
159 |
PredData {intros = intros, elim = elim, nparams = nparams, functions = functions} |
|
160 |
fun map_pred_data f (PredData {intros, elim, nparams, functions}) = |
|
161 |
mk_pred_data (f ((intros, elim, nparams), functions)) |
|
162 |
||
163 |
fun eq_option eq (NONE, NONE) = true |
|
164 |
| eq_option eq (SOME x, SOME y) = eq (x, y) |
|
165 |
| eq_option eq _ = false |
|
166 |
||
167 |
fun eq_pred_data (PredData d1, PredData d2) = |
|
168 |
eq_list (Thm.eq_thm) (#intros d1, #intros d2) andalso |
|
169 |
eq_option (Thm.eq_thm) (#elim d1, #elim d2) andalso |
|
170 |
#nparams d1 = #nparams d2 |
|
171 |
||
172 |
structure PredData = TheoryDataFun |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
173 |
( |
31514 | 174 |
type T = pred_data Graph.T; |
175 |
val empty = Graph.empty; |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
176 |
val copy = I; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
177 |
val extend = I; |
31514 | 178 |
fun merge _ = Graph.merge eq_pred_data; |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
179 |
); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
180 |
|
31514 | 181 |
(* queries *) |
182 |
||
31549 | 183 |
fun lookup_pred_data thy name = |
31573
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
184 |
Option.map rep_pred_data (try (Graph.get_node (PredData.get thy)) name) |
31514 | 185 |
|
186 |
fun the_pred_data thy name = case lookup_pred_data thy name |
|
187 |
of NONE => error ("No such predicate " ^ quote name) |
|
188 |
| SOME data => data; |
|
189 |
||
190 |
val is_pred = is_some oo lookup_pred_data |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
191 |
|
31514 | 192 |
val all_preds_of = Graph.keys o PredData.get |
193 |
||
194 |
val intros_of = #intros oo the_pred_data |
|
195 |
||
196 |
fun the_elim_of thy name = case #elim (the_pred_data thy name) |
|
197 |
of NONE => error ("No elimination rule for predicate " ^ quote name) |
|
198 |
| SOME thm => thm |
|
199 |
||
200 |
val has_elim = is_some o #elim oo the_pred_data; |
|
201 |
||
202 |
val nparams_of = #nparams oo the_pred_data |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
203 |
|
31514 | 204 |
val modes_of = (map fst) o #functions oo the_pred_data |
205 |
||
206 |
fun all_modes_of thy = map (fn name => (name, modes_of thy name)) (all_preds_of thy) |
|
207 |
||
208 |
val is_compiled = not o null o #functions oo the_pred_data |
|
209 |
||
210 |
fun lookup_predfun_data thy name mode = |
|
211 |
Option.map rep_predfun_data (AList.lookup (op =) |
|
212 |
(#functions (the_pred_data thy name)) mode) |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
213 |
|
31514 | 214 |
fun the_predfun_data thy name mode = case lookup_predfun_data thy name mode |
215 |
of NONE => error ("No such mode" ^ string_of_mode mode) |
|
216 |
| SOME data => data; |
|
217 |
||
218 |
val predfun_name_of = #name ooo the_predfun_data |
|
219 |
||
220 |
val predfun_definition_of = #definition ooo the_predfun_data |
|
221 |
||
222 |
val predfun_intro_of = #intro ooo the_predfun_data |
|
223 |
||
224 |
val predfun_elim_of = #elim ooo the_predfun_data |
|
225 |
||
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
226 |
|
31514 | 227 |
(* replaces print_alternative_rules *) |
228 |
(* TODO: |
|
229 |
fun print_alternative_rules thy = let |
|
230 |
val d = IndCodegenData.get thy |
|
231 |
val preds = (Symtab.keys (#intro_rules d)) union (Symtab.keys (#elim_rules d)) |
|
232 |
val _ = tracing ("preds: " ^ (makestring preds)) |
|
233 |
fun print pred = let |
|
234 |
val _ = tracing ("predicate: " ^ pred) |
|
235 |
val _ = tracing ("introrules: ") |
|
236 |
val _ = fold (fn thm => fn u => tracing (makestring thm)) |
|
237 |
(rev (Symtab.lookup_list (#intro_rules d) pred)) () |
|
238 |
val _ = tracing ("casesrule: ") |
|
239 |
val _ = tracing (makestring (Symtab.lookup (#elim_rules d) pred)) |
|
240 |
in () end |
|
241 |
val _ = map print preds |
|
242 |
in thy end; |
|
243 |
*) |
|
244 |
||
31573
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
245 |
|
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
246 |
fun imp_prems_conv cv ct = |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
247 |
case Thm.term_of ct of |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
248 |
Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
249 |
| _ => Conv.all_conv ct |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
250 |
|
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
251 |
fun Trueprop_conv cv ct = |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
252 |
case Thm.term_of ct of |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
253 |
Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
254 |
| _ => error "Trueprop_conv" |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
255 |
|
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
256 |
fun preprocess_intro thy rule = |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
257 |
Conv.fconv_rule |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
258 |
(imp_prems_conv |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
259 |
(Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq}))))) |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
260 |
(Thm.transfer thy rule) |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
261 |
|
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
262 |
fun preprocess_elim thy nargs elimrule = let |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
263 |
fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) = |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
264 |
HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs) |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
265 |
| replace_eqs t = t |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
266 |
fun preprocess_case t = let |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
267 |
val params = Logic.strip_params t |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
268 |
val (assums1, assums2) = chop nargs (Logic.strip_assums_hyp t) |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
269 |
val assums_hyp' = assums1 @ (map replace_eqs assums2) |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
270 |
in list_all (params, Logic.list_implies (assums_hyp', Logic.strip_assums_concl t)) end |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
271 |
val prems = Thm.prems_of elimrule |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
272 |
val cases' = map preprocess_case (tl prems) |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
273 |
val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule) |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
274 |
in |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
275 |
Thm.equal_elim |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
276 |
(Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@{thm eq_is_eq}]) |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
277 |
(cterm_of thy elimrule'))) |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
278 |
elimrule |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
279 |
end; |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
280 |
|
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
281 |
fun fetch_pred_data thy name = |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
282 |
case try (InductivePackage.the_inductive (ProofContext.init thy)) name of |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
283 |
SOME (info as (_, result)) => |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
284 |
let |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
285 |
fun is_intro_of intro = |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
286 |
let |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
287 |
val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro)) |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
288 |
in (fst (dest_Const const) = name) end; |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
289 |
val intros = map (preprocess_intro thy) (filter is_intro_of (#intrs result)) |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
290 |
val elim = nth (#elims result) (find_index (fn s => s = name) (#names (fst info))) |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
291 |
val nparams = length (InductivePackage.params_of (#raw_induct result)) |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
292 |
in (intros, elim, nparams) end |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
293 |
| NONE => error ("No such predicate: " ^ quote name) |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
294 |
|
31514 | 295 |
(* updaters *) |
296 |
||
297 |
fun add_predfun name mode data = let |
|
298 |
val add = apsnd (cons (mode, mk_predfun_data data)) |
|
299 |
in PredData.map (Graph.map_node name (map_pred_data add)) end |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
300 |
|
31573
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
301 |
fun add_intro thm thy = let |
31514 | 302 |
val (name, _) = dest_Const (fst (strip_intro_concl 0 (prop_of thm))) |
31573
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
303 |
fun cons_intro gr = |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
304 |
case try (Graph.get_node gr) name of |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
305 |
SOME pred_data => Graph.map_node name (map_pred_data |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
306 |
(apfst (fn (intro, elim, nparams) => (thm::intro, elim, nparams)))) gr |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
307 |
| NONE => |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
308 |
let |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
309 |
val nparams = the_default 0 (try (#3 o fetch_pred_data thy) name) |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
310 |
in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), [])) gr end; |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
311 |
in PredData.map cons_intro thy end |
31514 | 312 |
|
313 |
fun set_elim thm = let |
|
314 |
val (name, _) = dest_Const (fst |
|
315 |
(strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm))))) |
|
316 |
fun set (intros, _, nparams) = (intros, SOME thm, nparams) |
|
317 |
in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
318 |
|
31514 | 319 |
fun set_nparams name nparams = let |
320 |
fun set (intros, elim, _ ) = (intros, elim, nparams) |
|
321 |
in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
322 |
|
31514 | 323 |
fun register_predicate (intros, elim, nparams) = let |
324 |
val (name, _) = dest_Const (fst (strip_intro_concl nparams (prop_of (hd intros)))) |
|
325 |
fun set _ = (intros, SOME elim, nparams) |
|
326 |
in PredData.map (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), []))) end |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
327 |
|
31514 | 328 |
|
329 |
(* Mode analysis *) |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
330 |
|
31514 | 331 |
(*** check if a term contains only constructor functions ***) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
332 |
fun is_constrt thy = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
333 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
334 |
val cnstrs = flat (maps |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
335 |
(map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
336 |
(Symtab.dest (DatatypePackage.get_datatypes thy))); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
337 |
fun check t = (case strip_comb t of |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
338 |
(Free _, []) => true |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
339 |
| (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
340 |
(SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
341 |
| _ => false) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
342 |
| _ => false) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
343 |
in check end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
344 |
|
31514 | 345 |
(*** check if a type is an equality type (i.e. doesn't contain fun) |
346 |
FIXME this is only an approximation ***) |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
347 |
fun is_eqT (Type (s, Ts)) = s <> "fun" andalso forall is_eqT Ts |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
348 |
| is_eqT _ = true; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
349 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
350 |
fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm []; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
351 |
val terms_vs = distinct (op =) o maps term_vs; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
352 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
353 |
(** collect all Frees in a term (with duplicates!) **) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
354 |
fun term_vTs tm = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
355 |
fold_aterms (fn Free xT => cons xT | _ => I) tm []; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
356 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
357 |
fun get_args is ts = let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
358 |
fun get_args' _ _ [] = ([], []) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
359 |
| get_args' is i (t::ts) = (if i mem is then apfst else apsnd) (cons t) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
360 |
(get_args' is (i+1) ts) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
361 |
in get_args' is 1 ts end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
362 |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
363 |
(*FIXME this function should not be named merge... make it local instead*) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
364 |
fun merge xs [] = xs |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
365 |
| merge [] ys = ys |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
366 |
| merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
367 |
else y::merge (x::xs) ys; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
368 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
369 |
fun subsets i j = if i <= j then |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
370 |
let val is = subsets (i+1) j |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
371 |
in merge (map (fn ks => i::ks) is) is end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
372 |
else [[]]; |
31514 | 373 |
|
374 |
(* FIXME: should be in library - map_prod *) |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
375 |
fun cprod ([], ys) = [] |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
376 |
| cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
377 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
378 |
fun cprods xss = foldr (map op :: o cprod) [[]] xss; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
379 |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
380 |
datatype hmode = Mode of mode * int list * hmode option list; (*FIXME don't understand |
31514 | 381 |
why there is another mode type tmode !?*) |
382 |
||
31515 | 383 |
|
31514 | 384 |
(*TODO: cleanup function and put together with modes_of_term *) |
385 |
fun modes_of_param default modes t = let |
|
386 |
val (vs, t') = strip_abs t |
|
387 |
val b = length vs |
|
388 |
fun mk_modes name args = Option.map (maps (fn (m as (iss, is)) => |
|
389 |
let |
|
390 |
val (args1, args2) = |
|
391 |
if length args < length iss then |
|
392 |
error ("Too few arguments for inductive predicate " ^ name) |
|
393 |
else chop (length iss) args; |
|
394 |
val k = length args2; |
|
395 |
val perm = map (fn i => (find_index_eq (Bound (b - i)) args2) + 1) |
|
31515 | 396 |
(1 upto b) |
31514 | 397 |
val partial_mode = (1 upto k) \\ perm |
398 |
in |
|
399 |
if not (partial_mode subset is) then [] else |
|
400 |
let |
|
401 |
val is' = |
|
402 |
(fold_index (fn (i, j) => if j mem is then cons (i + 1) else I) perm []) |
|
403 |
|> fold (fn i => if i > k then cons (i - k + b) else I) is |
|
404 |
||
405 |
val res = map (fn x => Mode (m, is', x)) (cprods (map |
|
406 |
(fn (NONE, _) => [NONE] |
|
407 |
| (SOME js, arg) => map SOME (filter |
|
408 |
(fn Mode (_, js', _) => js=js') (modes_of_term modes arg))) |
|
409 |
(iss ~~ args1))) |
|
410 |
in res end |
|
411 |
end)) (AList.lookup op = modes name) |
|
412 |
in case strip_comb t' of |
|
413 |
(Const (name, _), args) => the_default default (mk_modes name args) |
|
414 |
| (Var ((name, _), _), args) => the (mk_modes name args) |
|
415 |
| (Free (name, _), args) => the (mk_modes name args) |
|
416 |
| _ => default end |
|
417 |
||
418 |
and modes_of_term modes t = |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
419 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
420 |
val ks = 1 upto length (binder_types (fastype_of t)); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
421 |
val default = [Mode (([], ks), ks, [])]; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
422 |
fun mk_modes name args = Option.map (maps (fn (m as (iss, is)) => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
423 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
424 |
val (args1, args2) = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
425 |
if length args < length iss then |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
426 |
error ("Too few arguments for inductive predicate " ^ name) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
427 |
else chop (length iss) args; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
428 |
val k = length args2; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
429 |
val prfx = 1 upto k |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
430 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
431 |
if not (is_prefix op = prfx is) then [] else |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
432 |
let val is' = map (fn i => i - k) (List.drop (is, k)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
433 |
in map (fn x => Mode (m, is', x)) (cprods (map |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
434 |
(fn (NONE, _) => [NONE] |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
435 |
| (SOME js, arg) => map SOME (filter |
31170 | 436 |
(fn Mode (_, js', _) => js=js') (modes_of_term modes arg))) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
437 |
(iss ~~ args1))) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
438 |
end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
439 |
end)) (AList.lookup op = modes name) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
440 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
441 |
in (case strip_comb t of |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
442 |
(Const (name, _), args) => the_default default (mk_modes name args) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
443 |
| (Var ((name, _), _), args) => the (mk_modes name args) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
444 |
| (Free (name, _), args) => the (mk_modes name args) |
31514 | 445 |
| (Abs _, []) => modes_of_param default modes t |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
446 |
| _ => default) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
447 |
end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
448 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
449 |
datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
450 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
451 |
fun select_mode_prem thy modes vs ps = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
452 |
find_first (is_some o snd) (ps ~~ map |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
453 |
(fn Prem (us, t) => find_first (fn Mode (_, is, _) => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
454 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
455 |
val (in_ts, out_ts) = get_args is us; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
456 |
val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
457 |
val vTs = maps term_vTs out_ts'; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
458 |
val dupTs = map snd (duplicates (op =) vTs) @ |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
459 |
List.mapPartial (AList.lookup (op =) vTs) vs; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
460 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
461 |
terms_vs (in_ts @ in_ts') subset vs andalso |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
462 |
forall (is_eqT o fastype_of) in_ts' andalso |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
463 |
term_vs t subset vs andalso |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
464 |
forall is_eqT dupTs |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
465 |
end) |
31170 | 466 |
(modes_of_term modes t handle Option => |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
467 |
error ("Bad predicate: " ^ Syntax.string_of_term_global thy t)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
468 |
| Negprem (us, t) => find_first (fn Mode (_, is, _) => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
469 |
length us = length is andalso |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
470 |
terms_vs us subset vs andalso |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
471 |
term_vs t subset vs) |
31170 | 472 |
(modes_of_term modes t handle Option => |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
473 |
error ("Bad predicate: " ^ Syntax.string_of_term_global thy t)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
474 |
| Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], [])) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
475 |
else NONE |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
476 |
) ps); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
477 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
478 |
fun check_mode_clause thy param_vs modes (iss, is) (ts, ps) = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
479 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
480 |
val modes' = modes @ List.mapPartial |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
481 |
(fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)])) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
482 |
(param_vs ~~ iss); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
483 |
fun check_mode_prems vs [] = SOME vs |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
484 |
| check_mode_prems vs ps = (case select_mode_prem thy modes' vs ps of |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
485 |
NONE => NONE |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
486 |
| SOME (x, _) => check_mode_prems |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
487 |
(case x of Prem (us, _) => vs union terms_vs us | _ => vs) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
488 |
(filter_out (equal x) ps)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
489 |
val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (get_args is ts)); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
490 |
val in_vs = terms_vs in_ts; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
491 |
val concl_vs = terms_vs ts |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
492 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
493 |
forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
494 |
forall (is_eqT o fastype_of) in_ts' andalso |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
495 |
(case check_mode_prems (param_vs union in_vs) ps of |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
496 |
NONE => false |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
497 |
| SOME vs => concl_vs subset vs) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
498 |
end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
499 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
500 |
fun check_modes_pred thy param_vs preds modes (p, ms) = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
501 |
let val SOME rs = AList.lookup (op =) preds p |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
502 |
in (p, List.filter (fn m => case find_index |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
503 |
(not o check_mode_clause thy param_vs modes m) rs of |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
504 |
~1 => true |
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
505 |
| i => (tracing ("Clause " ^ string_of_int (i+1) ^ " of " ^ |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
506 |
p ^ " violates mode " ^ string_of_mode m); false)) ms) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
507 |
end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
508 |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
509 |
fun fixp f (x : (string * mode list) list) = |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
510 |
let val y = f x |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
511 |
in if x = y then x else fixp f y end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
512 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
513 |
fun infer_modes thy extra_modes arities param_vs preds = fixp (fn modes => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
514 |
map (check_modes_pred thy param_vs preds (modes @ extra_modes)) modes) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
515 |
(map (fn (s, (ks, k)) => (s, cprod (cprods (map |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
516 |
(fn NONE => [NONE] |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
517 |
| SOME k' => map SOME (subsets 1 k')) ks), |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
518 |
subsets 1 k))) arities); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
519 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
520 |
|
31514 | 521 |
(* term construction *) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
522 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
523 |
(* for simple modes (e.g. parameters) only: better call it param_funT *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
524 |
(* or even better: remove it and only use funT'_of - some modifications to funT'_of necessary *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
525 |
fun funT_of T NONE = T |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
526 |
| funT_of T (SOME mode) = let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
527 |
val Ts = binder_types T; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
528 |
val (Us1, Us2) = get_args mode Ts |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
529 |
in Us1 ---> (mk_pred_enumT (mk_tupleT Us2)) end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
530 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
531 |
fun funT'_of (iss, is) T = let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
532 |
val Ts = binder_types T |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
533 |
val (paramTs, argTs) = chop (length iss) Ts |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
534 |
val paramTs' = map2 (fn SOME is => funT'_of ([], is) | NONE => I) iss paramTs |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
535 |
val (inargTs, outargTs) = get_args is argTs |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
536 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
537 |
(paramTs' @ inargTs) ---> (mk_pred_enumT (mk_tupleT outargTs)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
538 |
end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
539 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
540 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
541 |
fun mk_v (names, vs) s T = (case AList.lookup (op =) vs s of |
31514 | 542 |
NONE => (Free (s, T), (names, (s, [])::vs)) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
543 |
| SOME xs => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
544 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
545 |
val s' = Name.variant names s; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
546 |
val v = Free (s', T) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
547 |
in |
31514 | 548 |
(v, (s'::names, AList.update (op =) (s, v::xs) vs)) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
549 |
end); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
550 |
|
31514 | 551 |
fun distinct_v (Free (s, T)) nvs = mk_v nvs s T |
552 |
| distinct_v (t $ u) nvs = |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
553 |
let |
31514 | 554 |
val (t', nvs') = distinct_v t nvs; |
555 |
val (u', nvs'') = distinct_v u nvs'; |
|
556 |
in (t' $ u', nvs'') end |
|
557 |
| distinct_v x nvs = (x, nvs); |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
558 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
559 |
fun compile_match thy eqs eqs' out_ts success_t = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
560 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
561 |
val eqs'' = maps mk_eq eqs @ eqs' |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
562 |
val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) []; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
563 |
val name = Name.variant names "x"; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
564 |
val name' = Name.variant (name :: names) "y"; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
565 |
val T = mk_tupleT (map fastype_of out_ts); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
566 |
val U = fastype_of success_t; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
567 |
val U' = dest_pred_enumT U; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
568 |
val v = Free (name, T); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
569 |
val v' = Free (name', T); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
570 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
571 |
lambda v (fst (DatatypePackage.make_case |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
572 |
(ProofContext.init thy) false [] v |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
573 |
[(mk_tuple out_ts, |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
574 |
if null eqs'' then success_t |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
575 |
else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $ |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
576 |
foldr1 HOLogic.mk_conj eqs'' $ success_t $ |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
577 |
mk_empty U'), |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
578 |
(v', mk_empty U')])) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
579 |
end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
580 |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
581 |
(*FIXME function can be removed*) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
582 |
fun mk_funcomp f t = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
583 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
584 |
val names = Term.add_free_names t []; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
585 |
val Ts = binder_types (fastype_of t); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
586 |
val vs = map Free |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
587 |
(Name.variant_list names (replicate (length Ts) "x") ~~ Ts) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
588 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
589 |
fold_rev lambda vs (f (list_comb (t, vs))) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
590 |
end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
591 |
|
31514 | 592 |
|
593 |
||
594 |
fun compile_param_ext thy modes (NONE, t) = t |
|
595 |
| compile_param_ext thy modes (m as SOME (Mode ((iss, is'), is, ms)), t) = |
|
596 |
let |
|
597 |
val (vs, u) = strip_abs t |
|
31515 | 598 |
val (ivs, ovs) = get_args is vs |
31514 | 599 |
val (f, args) = strip_comb u |
600 |
val (params, args') = chop (length ms) args |
|
601 |
val (inargs, outargs) = get_args is' args' |
|
602 |
val b = length vs |
|
603 |
val perm = map (fn i => (find_index_eq (Bound (b - i)) args') + 1) (1 upto b) |
|
604 |
val outp_perm = |
|
605 |
snd (get_args is perm) |
|
606 |
|> map (fn i => i - length (filter (fn x => x < i) is')) |
|
607 |
val names = [] (* TODO *) |
|
608 |
val out_names = Name.variant_list names (replicate (length outargs) "x") |
|
609 |
val f' = case f of |
|
610 |
Const (name, T) => |
|
611 |
if AList.defined op = modes name then |
|
612 |
Const (predfun_name_of thy name (iss, is'), funT'_of (iss, is') T) |
|
613 |
else error "compile param: Not an inductive predicate with correct mode" |
|
614 |
| Free (name, T) => Free (name, funT_of T (SOME is')) |
|
615 |
val outTs = dest_tupleT (dest_pred_enumT (body_type (fastype_of f'))) |
|
616 |
val out_vs = map Free (out_names ~~ outTs) |
|
617 |
val params' = map (compile_param thy modes) (ms ~~ params) |
|
618 |
val f_app = list_comb (f', params' @ inargs) |
|
619 |
val single_t = (mk_single (mk_tuple (map (fn i => nth out_vs (i - 1)) outp_perm))) |
|
620 |
val match_t = compile_match thy [] [] out_vs single_t |
|
621 |
in list_abs (ivs, |
|
622 |
mk_bind (f_app, match_t)) |
|
623 |
end |
|
624 |
| compile_param_ext _ _ _ = error "compile params" |
|
625 |
||
626 |
and compile_param thy modes (NONE, t) = t |
|
627 |
| compile_param thy modes (m as SOME (Mode ((iss, is'), is, ms)), t) = |
|
628 |
(case t of |
|
629 |
Abs _ => compile_param_ext thy modes (m, t) |
|
630 |
| _ => let |
|
631 |
val (f, args) = strip_comb t |
|
632 |
val (params, args') = chop (length ms) args |
|
633 |
val params' = map (compile_param thy modes) (ms ~~ params) |
|
634 |
val f' = case f of |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
635 |
Const (name, T) => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
636 |
if AList.defined op = modes name then |
31514 | 637 |
Const (predfun_name_of thy name (iss, is'), funT'_of (iss, is') T) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
638 |
else error "compile param: Not an inductive predicate with correct mode" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
639 |
| Free (name, T) => Free (name, funT_of T (SOME is')) |
31514 | 640 |
in list_comb (f', params' @ args') end) |
641 |
| compile_param _ _ _ = error "compile params" |
|
642 |
||
643 |
||
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
644 |
fun compile_expr thy modes (SOME (Mode (mode, is, ms)), t) = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
645 |
(case strip_comb t of |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
646 |
(Const (name, T), params) => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
647 |
if AList.defined op = modes name then |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
648 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
649 |
val (Ts, Us) = get_args is |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
650 |
(curry Library.drop (length ms) (fst (strip_type T))) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
651 |
val params' = map (compile_param thy modes) (ms ~~ params) |
31514 | 652 |
in list_comb (Const (predfun_name_of thy name mode, ((map fastype_of params') @ Ts) ---> |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
653 |
mk_pred_enumT (mk_tupleT Us)), params') |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
654 |
end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
655 |
else error "not a valid inductive expression" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
656 |
| (Free (name, T), args) => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
657 |
(*if name mem param_vs then *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
658 |
(* Higher order mode call *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
659 |
let val r = Free (name, funT_of T (SOME is)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
660 |
in list_comb (r, args) end) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
661 |
| compile_expr _ _ _ = error "not a valid inductive expression" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
662 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
663 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
664 |
fun compile_clause thy all_vs param_vs modes (iss, is) (ts, ps) inp = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
665 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
666 |
val modes' = modes @ List.mapPartial |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
667 |
(fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)])) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
668 |
(param_vs ~~ iss); |
31514 | 669 |
fun check_constrt t (names, eqs) = |
670 |
if is_constrt thy t then (t, (names, eqs)) else |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
671 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
672 |
val s = Name.variant names "x"; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
673 |
val v = Free (s, fastype_of t) |
31514 | 674 |
in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end; |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
675 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
676 |
val (in_ts, out_ts) = get_args is ts; |
31514 | 677 |
val (in_ts', (all_vs', eqs)) = |
678 |
fold_map check_constrt in_ts (all_vs, []); |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
679 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
680 |
fun compile_prems out_ts' vs names [] = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
681 |
let |
31514 | 682 |
val (out_ts'', (names', eqs')) = |
683 |
fold_map check_constrt out_ts' (names, []); |
|
684 |
val (out_ts''', (names'', constr_vs)) = fold_map distinct_v |
|
685 |
out_ts'' (names', map (rpair []) vs); |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
686 |
in |
31514 | 687 |
compile_match thy constr_vs (eqs @ eqs') out_ts''' |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
688 |
(mk_single (mk_tuple out_ts)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
689 |
end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
690 |
| compile_prems out_ts vs names ps = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
691 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
692 |
val vs' = distinct (op =) (flat (vs :: map term_vs out_ts)); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
693 |
val SOME (p, mode as SOME (Mode (_, js, _))) = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
694 |
select_mode_prem thy modes' vs' ps |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
695 |
val ps' = filter_out (equal p) ps |
31514 | 696 |
val (out_ts', (names', eqs)) = |
697 |
fold_map check_constrt out_ts (names, []) |
|
698 |
val (out_ts'', (names'', constr_vs')) = fold_map distinct_v |
|
699 |
out_ts' ((names', map (rpair []) vs)) |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
700 |
val (compiled_clause, rest) = case p of |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
701 |
Prem (us, t) => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
702 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
703 |
val (in_ts, out_ts''') = get_args js us; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
704 |
val u = list_comb (compile_expr thy modes (mode, t), in_ts) |
31514 | 705 |
val rest = compile_prems out_ts''' vs' names'' ps' |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
706 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
707 |
(u, rest) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
708 |
end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
709 |
| Negprem (us, t) => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
710 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
711 |
val (in_ts, out_ts''') = get_args js us |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
712 |
val u = list_comb (compile_expr thy modes (mode, t), in_ts) |
31514 | 713 |
val rest = compile_prems out_ts''' vs' names'' ps' |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
714 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
715 |
(mk_not_pred u, rest) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
716 |
end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
717 |
| Sidecond t => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
718 |
let |
31514 | 719 |
val rest = compile_prems [] vs' names'' ps'; |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
720 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
721 |
(mk_if_predenum t, rest) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
722 |
end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
723 |
in |
31514 | 724 |
compile_match thy constr_vs' eqs out_ts'' |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
725 |
(mk_bind (compiled_clause, rest)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
726 |
end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
727 |
val prem_t = compile_prems in_ts' param_vs all_vs' ps; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
728 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
729 |
mk_bind (mk_single inp, prem_t) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
730 |
end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
731 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
732 |
fun compile_pred thy all_vs param_vs modes s T cls mode = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
733 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
734 |
val Ts = binder_types T; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
735 |
val (Ts1, Ts2) = chop (length param_vs) Ts; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
736 |
val Ts1' = map2 funT_of Ts1 (fst mode) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
737 |
val (Us1, Us2) = get_args (snd mode) Ts2; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
738 |
val xnames = Name.variant_list param_vs |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
739 |
(map (fn i => "x" ^ string_of_int i) (snd mode)); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
740 |
val xs = map2 (fn s => fn T => Free (s, T)) xnames Us1; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
741 |
val cl_ts = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
742 |
map (fn cl => compile_clause thy |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
743 |
all_vs param_vs modes mode cl (mk_tuple xs)) cls; |
31514 | 744 |
val mode_id = predfun_name_of thy s mode |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
745 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
746 |
HOLogic.mk_Trueprop (HOLogic.mk_eq |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
747 |
(list_comb (Const (mode_id, (Ts1' @ Us1) ---> |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
748 |
mk_pred_enumT (mk_tupleT Us2)), |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
749 |
map2 (fn s => fn T => Free (s, T)) param_vs Ts1' @ xs), |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
750 |
foldr1 mk_sup cl_ts)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
751 |
end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
752 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
753 |
fun compile_preds thy all_vs param_vs modes preds = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
754 |
map (fn (s, (T, cls)) => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
755 |
map (compile_pred thy all_vs param_vs modes s T cls) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
756 |
((the o AList.lookup (op =) modes) s)) preds; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
757 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
758 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
759 |
(* special setup for simpset *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
760 |
val HOL_basic_ss' = HOL_basic_ss setSolver |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
761 |
(mk_solver "all_tac_solver" (fn _ => fn _ => all_tac)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
762 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
763 |
|
31514 | 764 |
(* Definition of executable functions and their intro and elim rules *) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
765 |
|
30972
5b65835ccc92
some experiements towards user interface for predicate compiler
haftmann
parents:
30528
diff
changeset
|
766 |
fun print_arities arities = tracing ("Arities:\n" ^ |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
767 |
cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^ |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
768 |
space_implode " -> " (map |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
769 |
(fn NONE => "X" | SOME k' => string_of_int k') |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
770 |
(ks @ [SOME k]))) arities)); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
771 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
772 |
fun mk_Eval_of ((x, T), NONE) names = (x, names) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
773 |
| mk_Eval_of ((x, T), SOME mode) names = let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
774 |
val Ts = binder_types T |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
775 |
val argnames = Name.variant_list names |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
776 |
(map (fn i => "x" ^ string_of_int i) (1 upto (length Ts))); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
777 |
val args = map Free (argnames ~~ Ts) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
778 |
val (inargs, outargs) = get_args mode args |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
779 |
val r = mk_Eval (list_comb (x, inargs), mk_tuple outargs) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
780 |
val t = fold_rev lambda args r |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
781 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
782 |
(t, argnames @ names) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
783 |
end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
784 |
|
31514 | 785 |
fun create_intro_elim_rule nparams mode defthm mode_id funT pred thy = |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
786 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
787 |
val Ts = binder_types (fastype_of pred) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
788 |
val funtrm = Const (mode_id, funT) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
789 |
val argnames = Name.variant_list [] |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
790 |
(map (fn i => "x" ^ string_of_int i) (1 upto (length Ts))); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
791 |
val (Ts1, Ts2) = chop nparams Ts; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
792 |
val Ts1' = map2 funT_of Ts1 (fst mode) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
793 |
val args = map Free (argnames ~~ (Ts1' @ Ts2)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
794 |
val (params, io_args) = chop nparams args |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
795 |
val (inargs, outargs) = get_args (snd mode) io_args |
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
796 |
val param_names = Name.variant_list argnames |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
797 |
(map (fn i => "p" ^ string_of_int i) (1 upto nparams)) |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
798 |
val param_vs = map Free (param_names ~~ Ts1) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
799 |
val (params', names) = fold_map mk_Eval_of ((params ~~ Ts1) ~~ (fst mode)) [] |
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
800 |
val predpropI = HOLogic.mk_Trueprop (list_comb (pred, param_vs @ io_args)) |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
801 |
val predpropE = HOLogic.mk_Trueprop (list_comb (pred, params' @ io_args)) |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
802 |
val param_eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (param_vs ~~ params') |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
803 |
val funargs = params @ inargs |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
804 |
val funpropE = HOLogic.mk_Trueprop (mk_Eval (list_comb (funtrm, funargs), |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
805 |
if null outargs then Free("y", HOLogic.unitT) else mk_tuple outargs)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
806 |
val funpropI = HOLogic.mk_Trueprop (mk_Eval (list_comb (funtrm, funargs), |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
807 |
mk_tuple outargs)) |
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
808 |
val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI) |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
809 |
val _ = Output.tracing (Syntax.string_of_term_global thy introtrm) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
810 |
val simprules = [defthm, @{thm eval_pred}, |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
811 |
@{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}] |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
812 |
val unfolddef_tac = (Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1) |
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
813 |
val introthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ ["y"]) [] introtrm (fn {...} => unfolddef_tac) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
814 |
val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)); |
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
815 |
val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P) |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
816 |
val elimthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ ["y", "P"]) [] elimtrm (fn {...} => unfolddef_tac) |
31514 | 817 |
in |
818 |
(introthm, elimthm) |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
819 |
end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
820 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
821 |
fun create_definitions preds nparams (name, modes) thy = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
822 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
823 |
val _ = tracing "create definitions" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
824 |
val T = AList.lookup (op =) preds name |> the |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
825 |
fun create_definition mode thy = let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
826 |
fun string_of_mode mode = if null mode then "0" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
827 |
else space_implode "_" (map string_of_int mode) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
828 |
val HOmode = let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
829 |
fun string_of_HOmode m s = case m of NONE => s | SOME mode => s ^ "__" ^ (string_of_mode mode) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
830 |
in (fold string_of_HOmode (fst mode) "") end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
831 |
val mode_id = name ^ (if HOmode = "" then "_" else HOmode ^ "___") |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
832 |
^ (string_of_mode (snd mode)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
833 |
val Ts = binder_types T; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
834 |
val (Ts1, Ts2) = chop nparams Ts; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
835 |
val Ts1' = map2 funT_of Ts1 (fst mode) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
836 |
val (Us1, Us2) = get_args (snd mode) Ts2; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
837 |
val names = Name.variant_list [] |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
838 |
(map (fn i => "x" ^ string_of_int i) (1 upto (length Ts))); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
839 |
val xs = map Free (names ~~ (Ts1' @ Ts2)); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
840 |
val (xparams, xargs) = chop nparams xs; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
841 |
val (xparams', names') = fold_map mk_Eval_of ((xparams ~~ Ts1) ~~ (fst mode)) names |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
842 |
val (xins, xouts) = get_args (snd mode) xargs; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
843 |
fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
844 |
| mk_split_lambda [x] t = lambda x t |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
845 |
| mk_split_lambda xs t = let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
846 |
fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
847 |
| mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
848 |
in mk_split_lambda' xs t end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
849 |
val predterm = mk_Enum (mk_split_lambda xouts (list_comb (Const (name, T), xparams' @ xargs))) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
850 |
val funT = (Ts1' @ Us1) ---> (mk_pred_enumT (mk_tupleT Us2)) |
30387 | 851 |
val mode_id = Sign.full_bname thy (Long_Name.base_name mode_id) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
852 |
val lhs = list_comb (Const (mode_id, funT), xparams @ xins) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
853 |
val def = Logic.mk_equals (lhs, predterm) |
31514 | 854 |
val ([definition], thy') = thy |> |
30387 | 855 |
Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_id), funT, NoSyn)] |> |
856 |
PureThy.add_defs false [((Binding.name (Long_Name.base_name mode_id ^ "_def"), def), [])] |
|
31514 | 857 |
val (intro, elim) = create_intro_elim_rule nparams mode definition mode_id funT (Const (name, T)) thy' |
858 |
in thy' |> add_predfun name mode (mode_id, definition, intro, elim) |
|
859 |
|> PureThy.store_thm (Binding.name (Long_Name.base_name mode_id ^ "I"), intro) |> snd |
|
860 |
|> PureThy.store_thm (Binding.name (Long_Name.base_name mode_id ^ "E"), elim) |> snd |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
861 |
end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
862 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
863 |
fold create_definition modes thy |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
864 |
end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
865 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
866 |
(**************************************************************************************) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
867 |
(* Proving equivalence of term *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
868 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
869 |
fun is_Type (Type _) = true |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
870 |
| is_Type _ = false |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
871 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
872 |
(* returns true if t is an application of an datatype constructor *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
873 |
(* which then consequently would be splitted *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
874 |
(* else false *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
875 |
fun is_constructor thy t = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
876 |
if (is_Type (fastype_of t)) then |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
877 |
(case DatatypePackage.get_datatype thy ((fst o dest_Type o fastype_of) t) of |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
878 |
NONE => false |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
879 |
| SOME info => (let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
880 |
val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
881 |
val (c, _) = strip_comb t |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
882 |
in (case c of |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
883 |
Const (name, _) => name mem_string constr_consts |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
884 |
| _ => false) end)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
885 |
else false |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
886 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
887 |
(* MAJOR FIXME: prove_params should be simple |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
888 |
- different form of introrule for parameters ? *) |
31549 | 889 |
fun prove_param thy modes (NONE, t) = |
890 |
all_tac |
|
891 |
| prove_param thy modes (m as SOME (Mode (mode, is, ms)), t) = |
|
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
892 |
REPEAT_DETERM (etac @{thm thin_rl} 1) |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
893 |
THEN REPEAT_DETERM (rtac @{thm ext} 1) |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
894 |
THEN (rtac @{thm iffI} 1) |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
895 |
THEN new_print_tac "prove_param" |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
896 |
(* proof in one direction *) |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
897 |
THEN (atac 1) |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
898 |
(* proof in the other direction *) |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
899 |
THEN (atac 1) |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
900 |
THEN new_print_tac "after prove_param" |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
901 |
(* let |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
902 |
val (f, args) = strip_comb t |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
903 |
val (params, _) = chop (length ms) args |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
904 |
val f_tac = case f of |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
905 |
Const (name, T) => simp_tac (HOL_basic_ss addsimps |
31514 | 906 |
(@{thm eval_pred}::(predfun_definition_of thy name mode):: |
907 |
@{thm "Product_Type.split_conv"}::[])) 1 |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
908 |
| Free _ => all_tac |
31514 | 909 |
| Abs _ => error "TODO: implement here" |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
910 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
911 |
print_tac "before simplification in prove_args:" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
912 |
THEN f_tac |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
913 |
THEN print_tac "after simplification in prove_args" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
914 |
THEN (EVERY (map (prove_param thy modes) (ms ~~ params))) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
915 |
THEN (REPEAT_DETERM (atac 1)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
916 |
end |
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
917 |
*) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
918 |
fun prove_expr thy modes (SOME (Mode (mode, is, ms)), t, us) (premposition : int) = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
919 |
(case strip_comb t of |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
920 |
(Const (name, T), args) => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
921 |
if AList.defined op = modes name then (let |
31514 | 922 |
val introrule = predfun_intro_of thy name mode |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
923 |
(*val (in_args, out_args) = get_args is us |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
924 |
val (pred, rargs) = strip_comb (HOLogic.dest_Trueprop |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
925 |
(hd (Logic.strip_imp_prems (prop_of introrule)))) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
926 |
val nparams = length ms (* get_nparams thy (fst (dest_Const pred)) *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
927 |
val (_, args) = chop nparams rargs |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
928 |
val subst = map (pairself (cterm_of thy)) (args ~~ us) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
929 |
val inst_introrule = Drule.cterm_instantiate subst introrule*) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
930 |
(* the next line is old and probably wrong *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
931 |
val (args1, args2) = chop (length ms) args |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
932 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
933 |
rtac @{thm bindI} 1 |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
934 |
THEN print_tac "before intro rule:" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
935 |
(* for the right assumption in first position *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
936 |
THEN rotate_tac premposition 1 |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
937 |
THEN rtac introrule 1 |
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
938 |
THEN new_print_tac "after intro rule" |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
939 |
(* work with parameter arguments *) |
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
940 |
THEN (atac 1) |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
941 |
THEN (new_print_tac "parameter goal") |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
942 |
THEN (EVERY (map (prove_param thy modes) (ms ~~ args1))) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
943 |
THEN (REPEAT_DETERM (atac 1)) end) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
944 |
else error "Prove expr if case not implemented" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
945 |
| _ => rtac @{thm bindI} 1 |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
946 |
THEN atac 1) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
947 |
| prove_expr _ _ _ _ = error "Prove expr not implemented" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
948 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
949 |
fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
950 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
951 |
fun SOLVEDALL tac st = FILTER (fn st' => nprems_of st' = 0) tac st |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
952 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
953 |
fun prove_match thy (out_ts : term list) = let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
954 |
fun get_case_rewrite t = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
955 |
if (is_constructor thy t) then let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
956 |
val case_rewrites = (#case_rewrites (DatatypePackage.the_datatype thy |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
957 |
((fst o dest_Type o fastype_of) t))) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
958 |
in case_rewrites @ (flat (map get_case_rewrite (snd (strip_comb t)))) end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
959 |
else [] |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
960 |
val simprules = @{thm "unit.cases"} :: @{thm "prod.cases"} :: (flat (map get_case_rewrite out_ts)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
961 |
(* replace TRY by determining if it necessary - are there equations when calling compile match? *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
962 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
963 |
(* make this simpset better! *) |
31515 | 964 |
asm_simp_tac (HOL_basic_ss' addsimps simprules) 1 |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
965 |
THEN print_tac "after prove_match:" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
966 |
THEN (DETERM (TRY (EqSubst.eqsubst_tac (ProofContext.init thy) [0] [@{thm "HOL.if_P"}] 1 |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
967 |
THEN (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac HOL_basic_ss 1)))) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
968 |
THEN (SOLVED (asm_simp_tac HOL_basic_ss 1))))) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
969 |
THEN print_tac "after if simplification" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
970 |
end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
971 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
972 |
(* corresponds to compile_fun -- maybe call that also compile_sidecond? *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
973 |
|
31515 | 974 |
fun prove_sidecond thy modes t = |
975 |
let |
|
976 |
fun preds_of t nameTs = case strip_comb t of |
|
977 |
(f as Const (name, T), args) => |
|
978 |
if AList.defined (op =) modes name then (name, T) :: nameTs |
|
979 |
else fold preds_of args nameTs |
|
980 |
| _ => nameTs |
|
981 |
val preds = preds_of t [] |
|
982 |
val defs = map |
|
983 |
(fn (pred, T) => predfun_definition_of thy pred ([], (1 upto (length (binder_types T))))) |
|
984 |
preds |
|
985 |
in |
|
986 |
(* remove not_False_eq_True when simpset in prove_match is better *) |
|
987 |
simp_tac (HOL_basic_ss addsimps @{thm not_False_eq_True} :: @{thm eval_pred} :: defs) 1 |
|
988 |
(* need better control here! *) |
|
989 |
end |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
990 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
991 |
fun prove_clause thy nargs all_vs param_vs modes (iss, is) (ts, ps) = let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
992 |
val modes' = modes @ List.mapPartial |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
993 |
(fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)])) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
994 |
(param_vs ~~ iss); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
995 |
fun check_constrt ((names, eqs), t) = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
996 |
if is_constrt thy t then ((names, eqs), t) else |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
997 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
998 |
val s = Name.variant names "x"; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
999 |
val v = Free (s, fastype_of t) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1000 |
in ((s::names, HOLogic.mk_eq (v, t)::eqs), v) end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1001 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1002 |
val (in_ts, clause_out_ts) = get_args is ts; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1003 |
val ((all_vs', eqs), in_ts') = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1004 |
(*FIXME*) Library.foldl_map check_constrt ((all_vs, []), in_ts); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1005 |
fun prove_prems out_ts vs [] = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1006 |
(prove_match thy out_ts) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1007 |
THEN asm_simp_tac HOL_basic_ss' 1 |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1008 |
THEN print_tac "before the last rule of singleI:" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1009 |
THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1010 |
| prove_prems out_ts vs rps = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1011 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1012 |
val vs' = distinct (op =) (flat (vs :: map term_vs out_ts)); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1013 |
val SOME (p, mode as SOME (Mode ((iss, js), _, param_modes))) = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1014 |
select_mode_prem thy modes' vs' rps; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1015 |
val premposition = (find_index (equal p) ps) + nargs |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1016 |
val rps' = filter_out (equal p) rps; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1017 |
val rest_tac = (case p of Prem (us, t) => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1018 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1019 |
val (in_ts, out_ts''') = get_args js us |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1020 |
val rec_tac = prove_prems out_ts''' vs' rps' |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1021 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1022 |
print_tac "before clause:" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1023 |
THEN asm_simp_tac HOL_basic_ss 1 |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1024 |
THEN print_tac "before prove_expr:" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1025 |
THEN prove_expr thy modes (mode, t, us) premposition |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1026 |
THEN print_tac "after prove_expr:" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1027 |
THEN rec_tac |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1028 |
end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1029 |
| Negprem (us, t) => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1030 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1031 |
val (in_ts, out_ts''') = get_args js us |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1032 |
val rec_tac = prove_prems out_ts''' vs' rps' |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1033 |
val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1034 |
val (_, params) = strip_comb t |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1035 |
in |
31515 | 1036 |
rtac @{thm bindI} 1 |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1037 |
THEN (if (is_some name) then |
31514 | 1038 |
simp_tac (HOL_basic_ss addsimps [predfun_definition_of thy (the name) (iss, js)]) 1 |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1039 |
THEN rtac @{thm not_predI} 1 |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1040 |
(* FIXME: work with parameter arguments *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1041 |
THEN (EVERY (map (prove_param thy modes) (param_modes ~~ params))) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1042 |
else |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1043 |
rtac @{thm not_predI'} 1) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1044 |
THEN (REPEAT_DETERM (atac 1)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1045 |
THEN rec_tac |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1046 |
end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1047 |
| Sidecond t => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1048 |
rtac @{thm bindI} 1 |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1049 |
THEN rtac @{thm if_predI} 1 |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1050 |
THEN print_tac "before sidecond:" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1051 |
THEN prove_sidecond thy modes t |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1052 |
THEN print_tac "after sidecond:" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1053 |
THEN prove_prems [] vs' rps') |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1054 |
in (prove_match thy out_ts) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1055 |
THEN rest_tac |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1056 |
end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1057 |
val prems_tac = prove_prems in_ts' param_vs ps |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1058 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1059 |
rtac @{thm bindI} 1 |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1060 |
THEN rtac @{thm singleI} 1 |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1061 |
THEN prems_tac |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1062 |
end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1063 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1064 |
fun select_sup 1 1 = [] |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1065 |
| select_sup _ 1 = [rtac @{thm supI1}] |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1066 |
| select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1)); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1067 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1068 |
fun prove_one_direction thy all_vs param_vs modes clauses ((pred, T), mode) = let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1069 |
(* val ind_result = InductivePackage.the_inductive (ProofContext.init thy) pred |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1070 |
val index = find_index (fn s => s = pred) (#names (fst ind_result)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1071 |
val (_, T) = dest_Const (nth (#preds (snd ind_result)) index) *) |
31514 | 1072 |
val nargs = length (binder_types T) - nparams_of thy pred |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1073 |
val pred_case_rule = singleton (ind_set_codegen_preproc thy) |
31514 | 1074 |
(preprocess_elim thy nargs (the_elim_of thy pred)) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1075 |
(* FIXME preprocessor |> Simplifier.full_simplify (HOL_basic_ss addsimps [@ {thm Predicate.memb_code}])*) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1076 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1077 |
REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})) |
31514 | 1078 |
THEN etac (predfun_elim_of thy pred mode) 1 |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1079 |
THEN etac pred_case_rule 1 |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1080 |
THEN (EVERY (map |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1081 |
(fn i => EVERY' (select_sup (length clauses) i) i) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1082 |
(1 upto (length clauses)))) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1083 |
THEN (EVERY (map (prove_clause thy nargs all_vs param_vs modes mode) clauses)) |
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1084 |
THEN new_print_tac "proved one direction" |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1085 |
end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1086 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1087 |
(*******************************************************************************************************) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1088 |
(* Proof in the other direction ************************************************************************) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1089 |
(*******************************************************************************************************) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1090 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1091 |
fun prove_match2 thy out_ts = let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1092 |
fun split_term_tac (Free _) = all_tac |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1093 |
| split_term_tac t = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1094 |
if (is_constructor thy t) then let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1095 |
val info = DatatypePackage.the_datatype thy ((fst o dest_Type o fastype_of) t) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1096 |
val num_of_constrs = length (#case_rewrites info) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1097 |
(* special treatment of pairs -- because of fishing *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1098 |
val split_rules = case (fst o dest_Type o fastype_of) t of |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1099 |
"*" => [@{thm prod.split_asm}] |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1100 |
| _ => PureThy.get_thms thy (((fst o dest_Type o fastype_of) t) ^ ".split_asm") |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1101 |
val (_, ts) = strip_comb t |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1102 |
in |
31515 | 1103 |
(Splitter.split_asm_tac split_rules 1) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1104 |
(* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1105 |
THEN (DETERM (TRY (etac @{thm Pair_inject} 1))) *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1106 |
THEN (REPEAT_DETERM_N (num_of_constrs - 1) (etac @{thm botE} 1 ORELSE etac @{thm botE} 2)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1107 |
THEN (EVERY (map split_term_tac ts)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1108 |
end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1109 |
else all_tac |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1110 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1111 |
split_term_tac (mk_tuple out_ts) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1112 |
THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1) THEN (etac @{thm botE} 2)))) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1113 |
end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1114 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1115 |
(* VERY LARGE SIMILIRATIY to function prove_param |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1116 |
-- join both functions |
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1117 |
*) |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1118 |
(* |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1119 |
fun prove_param2 thy modes (NONE, t) = all_tac |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1120 |
| prove_param2 thy modes (m as SOME (Mode (mode, is, ms)), t) = let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1121 |
val (f, args) = strip_comb t |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1122 |
val (params, _) = chop (length ms) args |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1123 |
val f_tac = case f of |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1124 |
Const (name, T) => full_simp_tac (HOL_basic_ss addsimps |
31514 | 1125 |
(@{thm eval_pred}::(predfun_definition_of thy name mode) |
1126 |
:: @{thm "Product_Type.split_conv"}::[])) 1 |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1127 |
| Free _ => all_tac |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1128 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1129 |
print_tac "before simplification in prove_args:" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1130 |
THEN f_tac |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1131 |
THEN print_tac "after simplification in prove_args" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1132 |
THEN (EVERY (map (prove_param2 thy modes) (ms ~~ params))) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1133 |
end |
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1134 |
*) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1135 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1136 |
fun prove_expr2 thy modes (SOME (Mode (mode, is, ms)), t) = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1137 |
(case strip_comb t of |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1138 |
(Const (name, T), args) => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1139 |
if AList.defined op = modes name then |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1140 |
etac @{thm bindE} 1 |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1141 |
THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))) |
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1142 |
THEN (debug_tac (Syntax.string_of_term_global thy |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1143 |
(prop_of (predfun_elim_of thy name mode)))) |
31514 | 1144 |
THEN (etac (predfun_elim_of thy name mode) 1) |
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1145 |
THEN new_print_tac "prove_expr2" |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1146 |
(* TODO -- FIXME: replace remove_last_goal*) |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1147 |
THEN (EVERY (replicate (length args) (remove_last_goal thy))) |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1148 |
THEN new_print_tac "finished prove_expr2" |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1149 |
(* THEN (EVERY (map (prove_param thy modes) (ms ~~ args))) *) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1150 |
else error "Prove expr2 if case not implemented" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1151 |
| _ => etac @{thm bindE} 1) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1152 |
| prove_expr2 _ _ _ = error "Prove expr2 not implemented" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1153 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1154 |
fun prove_sidecond2 thy modes t = let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1155 |
fun preds_of t nameTs = case strip_comb t of |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1156 |
(f as Const (name, T), args) => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1157 |
if AList.defined (op =) modes name then (name, T) :: nameTs |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1158 |
else fold preds_of args nameTs |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1159 |
| _ => nameTs |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1160 |
val preds = preds_of t [] |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1161 |
val defs = map |
31514 | 1162 |
(fn (pred, T) => predfun_definition_of thy pred ([], (1 upto (length (binder_types T))))) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1163 |
preds |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1164 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1165 |
(* only simplify the one assumption *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1166 |
full_simp_tac (HOL_basic_ss' addsimps @{thm eval_pred} :: defs) 1 |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1167 |
(* need better control here! *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1168 |
THEN print_tac "after sidecond2 simplification" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1169 |
end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1170 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1171 |
fun prove_clause2 thy all_vs param_vs modes (iss, is) (ts, ps) pred i = let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1172 |
val modes' = modes @ List.mapPartial |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1173 |
(fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)])) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1174 |
(param_vs ~~ iss); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1175 |
fun check_constrt ((names, eqs), t) = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1176 |
if is_constrt thy t then ((names, eqs), t) else |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1177 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1178 |
val s = Name.variant names "x"; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1179 |
val v = Free (s, fastype_of t) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1180 |
in ((s::names, HOLogic.mk_eq (v, t)::eqs), v) end; |
31514 | 1181 |
val pred_intro_rule = nth (intros_of thy pred) (i - 1) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1182 |
|> preprocess_intro thy |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1183 |
|> (fn thm => hd (ind_set_codegen_preproc thy [thm])) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1184 |
(* FIXME preprocess |> Simplifier.full_simplify (HOL_basic_ss addsimps [@ {thm Predicate.memb_code}]) *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1185 |
val (in_ts, clause_out_ts) = get_args is ts; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1186 |
val ((all_vs', eqs), in_ts') = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1187 |
(*FIXME*) Library.foldl_map check_constrt ((all_vs, []), in_ts); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1188 |
fun prove_prems2 out_ts vs [] = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1189 |
print_tac "before prove_match2 - last call:" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1190 |
THEN prove_match2 thy out_ts |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1191 |
THEN print_tac "after prove_match2 - last call:" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1192 |
THEN (etac @{thm singleE} 1) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1193 |
THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1194 |
THEN (asm_full_simp_tac HOL_basic_ss' 1) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1195 |
THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1196 |
THEN (asm_full_simp_tac HOL_basic_ss' 1) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1197 |
THEN SOLVED (print_tac "state before applying intro rule:" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1198 |
THEN (rtac pred_intro_rule 1) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1199 |
(* How to handle equality correctly? *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1200 |
THEN (print_tac "state before assumption matching") |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1201 |
THEN (REPEAT (atac 1 ORELSE |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1202 |
(CHANGED (asm_full_simp_tac HOL_basic_ss' 1) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1203 |
THEN print_tac "state after simp_tac:")))) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1204 |
| prove_prems2 out_ts vs ps = let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1205 |
val vs' = distinct (op =) (flat (vs :: map term_vs out_ts)); |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1206 |
val SOME (p, mode as SOME (Mode ((iss, js), _, param_modes))) = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1207 |
select_mode_prem thy modes' vs' ps; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1208 |
val ps' = filter_out (equal p) ps; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1209 |
val rest_tac = (case p of Prem (us, t) => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1210 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1211 |
val (in_ts, out_ts''') = get_args js us |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1212 |
val rec_tac = prove_prems2 out_ts''' vs' ps' |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1213 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1214 |
(prove_expr2 thy modes (mode, t)) THEN rec_tac |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1215 |
end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1216 |
| Negprem (us, t) => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1217 |
let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1218 |
val (in_ts, out_ts''') = get_args js us |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1219 |
val rec_tac = prove_prems2 out_ts''' vs' ps' |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1220 |
val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1221 |
val (_, params) = strip_comb t |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1222 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1223 |
print_tac "before neg prem 2" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1224 |
THEN etac @{thm bindE} 1 |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1225 |
THEN (if is_some name then |
31514 | 1226 |
full_simp_tac (HOL_basic_ss addsimps [predfun_definition_of thy (the name) (iss, js)]) 1 |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1227 |
THEN etac @{thm not_predE} 1 |
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1228 |
THEN (EVERY (map (prove_param thy modes) (param_modes ~~ params))) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1229 |
else |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1230 |
etac @{thm not_predE'} 1) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1231 |
THEN rec_tac |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1232 |
end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1233 |
| Sidecond t => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1234 |
etac @{thm bindE} 1 |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1235 |
THEN etac @{thm if_predE} 1 |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1236 |
THEN prove_sidecond2 thy modes t |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1237 |
THEN prove_prems2 [] vs' ps') |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1238 |
in print_tac "before prove_match2:" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1239 |
THEN prove_match2 thy out_ts |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1240 |
THEN print_tac "after prove_match2:" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1241 |
THEN rest_tac |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1242 |
end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1243 |
val prems_tac = prove_prems2 in_ts' param_vs ps |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1244 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1245 |
print_tac "starting prove_clause2" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1246 |
THEN etac @{thm bindE} 1 |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1247 |
THEN (etac @{thm singleE'} 1) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1248 |
THEN (TRY (etac @{thm Pair_inject} 1)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1249 |
THEN print_tac "after singleE':" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1250 |
THEN prems_tac |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1251 |
end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1252 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1253 |
fun prove_other_direction thy all_vs param_vs modes clauses (pred, mode) = let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1254 |
fun prove_clause (clause, i) = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1255 |
(if i < length clauses then etac @{thm supE} 1 else all_tac) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1256 |
THEN (prove_clause2 thy all_vs param_vs modes mode clause pred i) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1257 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1258 |
(DETERM (TRY (rtac @{thm unit.induct} 1))) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1259 |
THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all}))) |
31514 | 1260 |
THEN (rtac (predfun_intro_of thy pred mode) 1) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1261 |
THEN (EVERY (map prove_clause (clauses ~~ (1 upto (length clauses))))) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1262 |
end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1263 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1264 |
fun prove_pred thy all_vs param_vs modes clauses (((pred, T), mode), t) = let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1265 |
val ctxt = ProofContext.init thy |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1266 |
val clauses' = the (AList.lookup (op =) clauses pred) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1267 |
in |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1268 |
Goal.prove ctxt (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) t []) [] t |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1269 |
(if !do_proofs then |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1270 |
(fn _ => |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1271 |
rtac @{thm pred_iffI} 1 |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1272 |
THEN prove_one_direction thy all_vs param_vs modes clauses' ((pred, T), mode) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1273 |
THEN print_tac "proved one direction" |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1274 |
THEN prove_other_direction thy all_vs param_vs modes clauses' (pred, mode) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1275 |
THEN print_tac "proved other direction") |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1276 |
else (fn _ => mycheat_tac thy 1)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1277 |
end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1278 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1279 |
fun prove_preds thy all_vs param_vs modes clauses pmts = |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1280 |
map (prove_pred thy all_vs param_vs modes clauses) pmts |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1281 |
|
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1282 |
(* special case: inductive predicate with no clauses *) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1283 |
fun noclause (predname, T) thy = let |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1284 |
val Ts = binder_types T |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1285 |
val names = Name.variant_list [] |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1286 |
(map (fn i => "x" ^ (string_of_int i)) (1 upto (length Ts))) |
31124 | 1287 |
val vs = map2 (curry Free) names Ts |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1288 |
val clausehd = HOLogic.mk_Trueprop (list_comb(Const (predname, T), vs)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1289 |
val intro_t = Logic.mk_implies (@{prop False}, clausehd) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1290 |
val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1291 |
val elim_t = Logic.list_implies ([clausehd, Logic.mk_implies (@{prop False}, P)], P) |
31514 | 1292 |
val intro = Goal.prove (ProofContext.init thy) names [] intro_t |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1293 |
(fn {...} => etac @{thm FalseE} 1) |
31514 | 1294 |
val elim = Goal.prove (ProofContext.init thy) ("P" :: names) [] elim_t |
1295 |
(fn {...} => etac (the_elim_of thy predname) 1) |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1296 |
in |
31514 | 1297 |
add_intro intro thy |
1298 |
|> set_elim elim |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1299 |
end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1300 |
|
31514 | 1301 |
fun prepare_intrs thy prednames = |
1302 |
let |
|
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1303 |
(* FIXME: preprocessing moved to fetch_pred_data *) |
31514 | 1304 |
val intrs = map (preprocess_intro thy) (maps (intros_of thy) prednames) |
1305 |
|> ind_set_codegen_preproc thy (*FIXME preprocessor |
|
1306 |
|> map (Simplifier.full_simplify (HOL_basic_ss addsimps [@ {thm Predicate.memb_code}]))*) |
|
1307 |
|> map (Logic.unvarify o prop_of) |
|
1308 |
val nparams = nparams_of thy (hd prednames) |
|
1309 |
val preds = distinct (op =) (map (dest_Const o fst o (strip_intro_concl nparams)) intrs) |
|
1310 |
val extra_modes = all_modes_of thy |> filter_out (fn (name, _) => member (op =) prednames name) |
|
1311 |
val _ $ u = Logic.strip_imp_concl (hd intrs); |
|
1312 |
val params = List.take (snd (strip_comb u), nparams); |
|
1313 |
val param_vs = maps term_vs params |
|
1314 |
val all_vs = terms_vs intrs |
|
1315 |
fun dest_prem t = |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1316 |
(case strip_comb t of |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1317 |
(v as Free _, ts) => if v mem params then Prem (ts, v) else Sidecond t |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1318 |
| (c as Const (@{const_name Not}, _), [t]) => (case dest_prem t of |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1319 |
Prem (ts, t) => Negprem (ts, t) |
31515 | 1320 |
| Negprem _ => error ("Double negation not allowed in premise: " ^ (Syntax.string_of_term_global thy (c $ t))) |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1321 |
| Sidecond t => Sidecond (c $ t)) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1322 |
| (c as Const (s, _), ts) => |
31514 | 1323 |
if is_pred thy s then |
1324 |
let val (ts1, ts2) = chop (nparams_of thy s) ts |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1325 |
in Prem (ts2, list_comb (c, ts1)) end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1326 |
else Sidecond t |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1327 |
| _ => Sidecond t) |
31514 | 1328 |
fun add_clause intr (clauses, arities) = |
1329 |
let |
|
1330 |
val _ $ t = Logic.strip_imp_concl intr; |
|
1331 |
val (Const (name, T), ts) = strip_comb t; |
|
1332 |
val (ts1, ts2) = chop nparams ts; |
|
1333 |
val prems = map (dest_prem o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr); |
|
1334 |
val (Ts, Us) = chop nparams (binder_types T) |
|
1335 |
in |
|
1336 |
(AList.update op = (name, these (AList.lookup op = clauses name) @ |
|
1337 |
[(ts2, prems)]) clauses, |
|
1338 |
AList.update op = (name, (map (fn U => (case strip_type U of |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1339 |
(Rs as _ :: _, Type ("bool", [])) => SOME (length Rs) |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1340 |
| _ => NONE)) Ts, |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1341 |
length Us)) arities) |
31514 | 1342 |
end; |
1343 |
val (clauses, arities) = fold add_clause intrs ([], []); |
|
1344 |
in (preds, nparams, all_vs, param_vs, extra_modes, clauses, arities) end; |
|
1345 |
||
1346 |
fun arrange kvs = |
|
1347 |
let |
|
1348 |
fun add (key, value) table = |
|
1349 |
AList.update op = (key, these (AList.lookup op = table key) @ [value]) table |
|
1350 |
in fold add kvs [] end; |
|
1351 |
||
1352 |
(* main function *) |
|
1353 |
||
1354 |
fun add_equations_of prednames thy = |
|
1355 |
let |
|
1356 |
val _ = tracing ("starting add_equations with " ^ commas prednames ^ "...") |
|
1357 |
(* null clause handling *) |
|
1358 |
(* |
|
1359 |
val thy' = fold (fn pred as (predname, T) => fn thy => |
|
1360 |
if null (intros_of thy predname) then noclause pred thy else thy) preds thy |
|
1361 |
*) |
|
1362 |
val (preds, nparams, all_vs, param_vs, extra_modes, clauses, arities) = |
|
1363 |
prepare_intrs thy prednames |
|
1364 |
val _ = tracing "Infering modes..." |
|
1365 |
val modes = infer_modes thy extra_modes arities param_vs clauses |
|
31549 | 1366 |
val _ = print_modes modes |
31514 | 1367 |
val _ = tracing "Defining executable functions..." |
1368 |
val thy' = fold (create_definitions preds nparams) modes thy |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1369 |
val clauses' = map (fn (s, cls) => (s, (the (AList.lookup (op =) preds s), cls))) clauses |
31514 | 1370 |
val _ = tracing "Compiling equations..." |
1371 |
val ts = compile_preds thy' all_vs param_vs (extra_modes @ modes) clauses' |
|
31549 | 1372 |
val _ = map (Output.tracing o (Syntax.string_of_term_global thy')) (flat ts) |
31514 | 1373 |
val pred_mode = |
1374 |
maps (fn (s, (T, _)) => map (pair (s, T)) ((the o AList.lookup (op =) modes) s)) clauses' |
|
1375 |
val _ = tracing "Proving equations..." |
|
1376 |
val result_thms = |
|
1377 |
prove_preds thy' all_vs param_vs (extra_modes @ modes) clauses (pred_mode ~~ (flat ts)) |
|
1378 |
val thy'' = fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss |
|
1379 |
[((Binding.qualify true (Long_Name.base_name name) (Binding.name "equation"), result_thms), |
|
1380 |
[Attrib.attribute_i thy Code.add_default_eqn_attrib])] thy)) |
|
1381 |
(arrange ((map (fn ((name, _), _) => name) pred_mode) ~~ result_thms)) thy' |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1382 |
in |
31514 | 1383 |
thy'' |
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1384 |
end |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1385 |
|
31106 | 1386 |
(* generation of case rules from user-given introduction rules *) |
1387 |
||
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1388 |
fun mk_casesrule ctxt nparams introrules = |
31124 | 1389 |
let |
31573
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
1390 |
val intros = map (Logic.unvarify o prop_of) introrules |
31514 | 1391 |
val (pred, (params, args)) = strip_intro_concl nparams (hd intros) |
31106 | 1392 |
val ([propname], ctxt1) = Variable.variant_fixes ["thesis"] ctxt |
1393 |
val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT)) |
|
1394 |
val (argnames, ctxt2) = Variable.variant_fixes |
|
1395 |
(map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt1 |
|
31514 | 1396 |
val argvs = map2 (curry Free) argnames (map fastype_of args) |
31106 | 1397 |
fun mk_case intro = let |
31514 | 1398 |
val (_, (_, args)) = strip_intro_concl nparams intro |
31106 | 1399 |
val prems = Logic.strip_imp_prems intro |
1400 |
val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args) |
|
1401 |
val frees = (fold o fold_aterms) |
|
1402 |
(fn t as Free _ => |
|
1403 |
if member (op aconv) params t then I else insert (op aconv) t |
|
1404 |
| _ => I) (args @ prems) [] |
|
1405 |
in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end |
|
1406 |
val assm = HOLogic.mk_Trueprop (list_comb (pred, params @ argvs)) |
|
1407 |
val cases = map mk_case intros |
|
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1408 |
in Logic.list_implies (assm :: cases, prop) end; |
31106 | 1409 |
|
31514 | 1410 |
(* code dependency graph *) |
1411 |
||
31573
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
1412 |
fun dependencies_of thy name = |
31514 | 1413 |
let |
1414 |
fun is_inductive_predicate thy name = |
|
1415 |
is_some (try (InductivePackage.the_inductive (ProofContext.init thy)) name) |
|
31573
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
1416 |
val (intro, elim, nparams) = fetch_pred_data thy name |
0047df9eb347
improved infrastructure of predicate compiler for adding manual introduction rules
bulwahn
parents:
31551
diff
changeset
|
1417 |
val data = mk_pred_data ((intro, SOME elim, nparams), []) |
31514 | 1418 |
val intros = map Thm.prop_of (#intros (rep_pred_data data)) |
1419 |
val keys = fold Term.add_consts intros [] |> map fst |
|
1420 |
|> filter (is_inductive_predicate thy) |
|
1421 |
in |
|
1422 |
(data, keys) |
|
1423 |
end; |
|
1424 |
||
1425 |
fun add_equations name thy = |
|
1426 |
let |
|
31541 | 1427 |
val thy' = PredData.map (Graph.extend (dependencies_of thy) name) thy; |
31514 | 1428 |
(*val preds = Graph.all_preds (PredData.get thy') [name] |> filter_out (has_elim thy') *) |
1429 |
fun strong_conn_of gr keys = |
|
1430 |
Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr) |
|
1431 |
val scc = strong_conn_of (PredData.get thy') [name] |
|
31524
8abf99ab669c
avoiding duplicate definitions of executable functions
bulwahn
parents:
31517
diff
changeset
|
1432 |
val thy'' = fold_rev |
8abf99ab669c
avoiding duplicate definitions of executable functions
bulwahn
parents:
31517
diff
changeset
|
1433 |
(fn preds => fn thy => |
8abf99ab669c
avoiding duplicate definitions of executable functions
bulwahn
parents:
31517
diff
changeset
|
1434 |
if forall (null o modes_of thy) preds then add_equations_of preds thy else thy) |
8abf99ab669c
avoiding duplicate definitions of executable functions
bulwahn
parents:
31517
diff
changeset
|
1435 |
scc thy' |
31514 | 1436 |
in thy'' end |
31124 | 1437 |
|
1438 |
(** user interface **) |
|
1439 |
||
1440 |
local |
|
1441 |
||
1442 |
fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); |
|
1443 |
||
31514 | 1444 |
(* |
1445 |
val add_elim_attrib = attrib set_elim; |
|
1446 |
*) |
|
31106 | 1447 |
|
31514 | 1448 |
|
1449 |
(* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *) |
|
1450 |
(* TODO: must create state to prove multiple cases *) |
|
31124 | 1451 |
fun generic_code_pred prep_const raw_const lthy = |
1452 |
let |
|
31551
995d6b90e9d6
making isatest happy; but misunderstanding remains
bulwahn
parents:
31550
diff
changeset
|
1453 |
|
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1454 |
val thy = ProofContext.theory_of lthy |
31124 | 1455 |
val const = prep_const thy raw_const |
31551
995d6b90e9d6
making isatest happy; but misunderstanding remains
bulwahn
parents:
31550
diff
changeset
|
1456 |
|
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1457 |
val lthy' = LocalTheory.theory (PredData.map (Graph.extend (dependencies_of thy) const)) lthy |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1458 |
val thy' = ProofContext.theory_of lthy' |
31514 | 1459 |
val preds = Graph.all_preds (PredData.get thy') [const] |> filter_out (has_elim thy') |
31551
995d6b90e9d6
making isatest happy; but misunderstanding remains
bulwahn
parents:
31550
diff
changeset
|
1460 |
|
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1461 |
fun mk_cases const = |
31514 | 1462 |
let |
31550
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1463 |
val nparams = nparams_of thy' const |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1464 |
val intros = intros_of thy' const |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1465 |
in mk_casesrule lthy' nparams intros end |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1466 |
val cases_rules = map mk_cases preds |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1467 |
fun after_qed thms = |
b63d253ed9e2
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
bulwahn
parents:
31549
diff
changeset
|
1468 |
LocalTheory.theory (fold set_elim (map the_single thms) #> add_equations const) |
31124 | 1469 |
in |
31551
995d6b90e9d6
making isatest happy; but misunderstanding remains
bulwahn
parents:
31550
diff
changeset
|
1470 |
Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy |
995d6b90e9d6
making isatest happy; but misunderstanding remains
bulwahn
parents:
31550
diff
changeset
|
1471 |
(* FIXME: expected the actual local_theory to be lthy'; but works with lthy ??*) |
31124 | 1472 |
end; |
1473 |
||
1474 |
structure P = OuterParse |
|
31106 | 1475 |
|
31124 | 1476 |
in |
1477 |
||
1478 |
val code_pred = generic_code_pred (K I); |
|
31156 | 1479 |
val code_pred_cmd = generic_code_pred Code.read_const |
31124 | 1480 |
|
31514 | 1481 |
val setup = PredData.put (Graph.empty) #> |
1482 |
Attrib.setup @{binding code_pred_intros} (Scan.succeed (attrib add_intro)) |
|
1483 |
"adding alternative introduction rules for code generation of inductive predicates" |
|
1484 |
(* Attrib.setup @{binding code_ind_cases} (Scan.succeed add_elim_attrib) |
|
31124 | 1485 |
"adding alternative elimination rules for code generation of inductive predicates"; |
31514 | 1486 |
*) |
31124 | 1487 |
(*FIXME name discrepancy in attribs and ML code*) |
1488 |
(*FIXME intros should be better named intro*) |
|
31514 | 1489 |
(*FIXME why distinguished attribute for cases?*) |
31124 | 1490 |
|
1491 |
val _ = OuterSyntax.local_theory_to_proof "code_pred" |
|
1492 |
"prove equations for predicate specified by intro/elim rules" |
|
1493 |
OuterKeyword.thy_goal (P.term_group >> code_pred_cmd) |
|
1494 |
||
1495 |
end |
|
1496 |
||
1497 |
(*FIXME |
|
1498 |
- Naming of auxiliary rules necessary? |
|
31217 | 1499 |
- add default code equations P x y z = P_i_i_i x y z |
31124 | 1500 |
*) |
31106 | 1501 |
|
31169
f4c61cbea49d
added predicate transformation function for code generation
bulwahn
parents:
31107
diff
changeset
|
1502 |
(* transformation for code generation *) |
f4c61cbea49d
added predicate transformation function for code generation
bulwahn
parents:
31107
diff
changeset
|
1503 |
|
31217 | 1504 |
val eval_ref = ref (NONE : (unit -> term Predicate.pred) option); |
1505 |
||
1506 |
fun analyze_compr thy t_compr = |
|
1507 |
let |
|
1508 |
val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t |
|
1509 |
| _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr); |
|
1510 |
val (body, Ts, fp) = HOLogic.strip_split split; |
|
1511 |
(*FIXME former order of tuple positions must be restored*) |
|
1512 |
val (pred as Const (name, T), all_args) = strip_comb body |
|
31514 | 1513 |
val (params, args) = chop (nparams_of thy name) all_args |
31217 | 1514 |
val user_mode = map_filter I (map_index |
1515 |
(fn (i, t) => case t of Bound j => if j < length Ts then NONE |
|
1516 |
else SOME (i+1) | _ => SOME (i+1)) args) (*FIXME dangling bounds should not occur*) |
|
1517 |
val (inargs, _) = get_args user_mode args; |
|
1518 |
val modes = filter (fn Mode (_, is, _) => is = user_mode) |
|
31514 | 1519 |
(modes_of_term (all_modes_of thy) (list_comb (pred, params))); |
31217 | 1520 |
val m = case modes |
1521 |
of [] => error ("No mode possible for comprehension " |
|
1522 |
^ Syntax.string_of_term_global thy t_compr) |
|
1523 |
| [m] => m |
|
1524 |
| m :: _ :: _ => (warning ("Multiple modes possible for comprehension " |
|
1525 |
^ Syntax.string_of_term_global thy t_compr); m); |
|
31514 | 1526 |
val t_eval = list_comb (compile_expr thy (all_modes_of thy) (SOME m, list_comb (pred, params)), |
31217 | 1527 |
inargs) |
1528 |
in t_eval end; |
|
31169
f4c61cbea49d
added predicate transformation function for code generation
bulwahn
parents:
31107
diff
changeset
|
1529 |
|
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1530 |
end; |
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
diff
changeset
|
1531 |