author | wenzelm |
Tue, 09 Dec 2014 19:39:40 +0100 | |
changeset 59119 | c90c02940964 |
parent 59048 | 7dc8ac6f0895 |
child 59353 | f0707dc3d9aa |
permissions | -rw-r--r-- |
50387 | 1 |
(* Title: HOL/Probability/measurable.ML |
2 |
Author: Johannes Hölzl <hoelzl@in.tum.de> |
|
3 |
||
4 |
Measurability prover. |
|
5 |
*) |
|
6 |
||
7 |
signature MEASURABLE = |
|
8 |
sig |
|
59048 | 9 |
type preprocessor = thm -> Proof.context -> (thm list * Proof.context) |
10 |
||
50387 | 11 |
datatype level = Concrete | Generic |
12 |
||
59047 | 13 |
val app_thm_attr : attribute context_parser |
14 |
val dest_thm_attr : attribute context_parser |
|
59048 | 15 |
val cong_thm_attr : attribute context_parser |
59047 | 16 |
val measurable_thm_attr : bool * (bool * level) -> attribute |
53043
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
51717
diff
changeset
|
17 |
|
59048 | 18 |
val add_del_cong_thm : bool -> thm -> Context.generic -> Context.generic ; |
19 |
||
20 |
val get_all : Context.generic -> thm list |
|
21 |
val get_dest : Context.generic -> thm list |
|
22 |
val get_cong : Context.generic -> thm list |
|
23 |
||
50387 | 24 |
val measurable_tac : Proof.context -> thm list -> tactic |
25 |
||
53043
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
51717
diff
changeset
|
26 |
val simproc : Proof.context -> cterm -> thm option |
50387 | 27 |
|
59048 | 28 |
val add_preprocessor : string -> preprocessor -> Context.generic -> Context.generic |
29 |
val del_preprocessor : string -> Context.generic -> Context.generic |
|
30 |
val add_local_cong : thm -> Proof.context -> Proof.context |
|
50387 | 31 |
end ; |
32 |
||
33 |
structure Measurable : MEASURABLE = |
|
34 |
struct |
|
35 |
||
59048 | 36 |
type preprocessor = thm -> Proof.context -> (thm list * Proof.context) |
37 |
||
50387 | 38 |
datatype level = Concrete | Generic; |
39 |
||
59047 | 40 |
fun eq_measurable_thms ((th1, d1), (th2, d2)) = |
41 |
d1 = d2 andalso Thm.eq_thm_prop (th1, th2) ; |
|
42 |
||
59048 | 43 |
fun merge_dups (xs:(string * preprocessor) list) ys = |
44 |
xs @ (filter (fn (name, _) => is_none (find_first (fn (name', _) => name' = name) xs)) ys) |
|
45 |
||
50387 | 46 |
structure Data = Generic_Data |
47 |
( |
|
48 |
type T = { |
|
59047 | 49 |
measurable_thms : (thm * (bool * level)) Item_Net.T, |
50387 | 50 |
dest_thms : thm Item_Net.T, |
59048 | 51 |
app_thms : thm Item_Net.T, |
52 |
cong_thms : thm Item_Net.T, |
|
53 |
preprocessors : (string * preprocessor) list } |
|
50387 | 54 |
val empty = { |
59047 | 55 |
measurable_thms = Item_Net.init eq_measurable_thms (single o Thm.prop_of o fst), |
50387 | 56 |
dest_thms = Thm.full_rules, |
59048 | 57 |
app_thms = Thm.full_rules, |
58 |
cong_thms = Thm.full_rules, |
|
59 |
preprocessors = [] }; |
|
50387 | 60 |
val extend = I; |
59048 | 61 |
fun merge ({measurable_thms = t1, dest_thms = dt1, app_thms = at1, cong_thms = ct1, preprocessors = i1 }, |
62 |
{measurable_thms = t2, dest_thms = dt2, app_thms = at2, cong_thms = ct2, preprocessors = i2 }) = { |
|
59047 | 63 |
measurable_thms = Item_Net.merge (t1, t2), |
50387 | 64 |
dest_thms = Item_Net.merge (dt1, dt2), |
59048 | 65 |
app_thms = Item_Net.merge (at1, at2), |
66 |
cong_thms = Item_Net.merge (ct1, ct2), |
|
67 |
preprocessors = merge_dups i1 i2 |
|
68 |
}; |
|
50387 | 69 |
); |
70 |
||
71 |
val debug = |
|
72 |
Attrib.setup_config_bool @{binding measurable_debug} (K false) |
|
73 |
||
74 |
val split = |
|
75 |
Attrib.setup_config_bool @{binding measurable_split} (K true) |
|
76 |
||
59048 | 77 |
fun map_data f1 f2 f3 f4 f5 |
78 |
{measurable_thms = t1, dest_thms = t2, app_thms = t3, cong_thms = t4, preprocessors = t5 } = |
|
79 |
{measurable_thms = f1 t1, dest_thms = f2 t2, app_thms = f3 t3, cong_thms = f4 t4, preprocessors = f5 t5} |
|
50387 | 80 |
|
59048 | 81 |
fun map_measurable_thms f = map_data f I I I I |
82 |
fun map_dest_thms f = map_data I f I I I |
|
83 |
fun map_app_thms f = map_data I I f I I |
|
84 |
fun map_cong_thms f = map_data I I I f I |
|
85 |
fun map_preprocessors f = map_data I I I I f |
|
50387 | 86 |
|
59047 | 87 |
fun generic_add_del map = |
88 |
Scan.lift |
|
89 |
(Args.add >> K Item_Net.update || Args.del >> K Item_Net.remove || Scan.succeed Item_Net.update) >> |
|
90 |
(fn f => Thm.declaration_attribute (Data.map o map o f)) |
|
91 |
||
92 |
val app_thm_attr = generic_add_del map_app_thms |
|
50387 | 93 |
|
59047 | 94 |
val dest_thm_attr = generic_add_del map_dest_thms |
50387 | 95 |
|
59048 | 96 |
val cong_thm_attr = generic_add_del map_cong_thms |
97 |
||
59047 | 98 |
fun del_thm th net = |
99 |
let |
|
100 |
val thms = net |> Item_Net.content |> filter (fn (th', _) => Thm.eq_thm (th, th')) |
|
101 |
in fold Item_Net.remove thms net end ; |
|
102 |
||
103 |
fun measurable_thm_attr (do_add, d) = Thm.declaration_attribute |
|
104 |
(Data.map o map_measurable_thms o (if do_add then Item_Net.update o rpair d else del_thm)) |
|
50387 | 105 |
|
106 |
val get_dest = Item_Net.content o #dest_thms o Data.get; |
|
107 |
val get_app = Item_Net.content o #app_thms o Data.get; |
|
108 |
||
59048 | 109 |
val get_cong = Item_Net.content o #cong_thms o Data.get; |
110 |
val add_cong = Data.map o map_cong_thms o Item_Net.update; |
|
111 |
val del_cong = Data.map o map_cong_thms o Item_Net.remove; |
|
112 |
fun add_del_cong_thm true = add_cong |
|
113 |
| add_del_cong_thm false = del_cong |
|
114 |
||
115 |
fun add_preprocessor name f = Data.map (map_preprocessors (fn xs => xs @ [(name, f)])) |
|
116 |
fun del_preprocessor name = Data.map (map_preprocessors (filter (fn (n, _) => n <> name))) |
|
117 |
val add_local_cong = Context.proof_map o add_cong |
|
118 |
||
119 |
val get_preprocessors = Context.Proof #> Data.get #> #preprocessors ; |
|
120 |
||
50387 | 121 |
fun is_too_generic thm = |
122 |
let |
|
123 |
val concl = concl_of thm |
|
124 |
val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl |
|
125 |
in is_Var (head_of concl') end |
|
126 |
||
59048 | 127 |
val get_thms = Data.get #> #measurable_thms #> Item_Net.content ; |
58965 | 128 |
|
59048 | 129 |
val get_all = get_thms #> map fst ; |
50387 | 130 |
|
59048 | 131 |
fun debug_tac ctxt msg f = |
132 |
if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f |
|
50387 | 133 |
|
134 |
fun nth_hol_goal thm i = |
|
135 |
HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1)))) |
|
136 |
||
137 |
fun dest_measurable_fun t = |
|
138 |
(case t of |
|
139 |
(Const (@{const_name "Set.member"}, _) $ f $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => f |
|
140 |
| _ => raise (TERM ("not a measurability predicate", [t]))) |
|
141 |
||
59048 | 142 |
fun not_measurable_prop n thm = if length (prems_of thm) < n then false else |
50387 | 143 |
(case nth_hol_goal thm n of |
144 |
(Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "sets"}, _) $ _)) => false |
|
145 |
| (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => false |
|
146 |
| _ => true) |
|
147 |
handle TERM _ => true; |
|
148 |
||
149 |
fun indep (Bound i) t b = i < b orelse t <= i |
|
150 |
| indep (f $ t) top bot = indep f top bot andalso indep t top bot |
|
151 |
| indep (Abs (_,_,t)) top bot = indep t (top + 1) (bot + 1) |
|
152 |
| indep _ _ _ = true; |
|
153 |
||
154 |
fun cnt_prefixes ctxt (Abs (n, T, t)) = let |
|
155 |
fun is_countable t = Type.of_sort (Proof_Context.tsig_of ctxt) (t, @{sort countable}) |
|
156 |
fun cnt_walk (Abs (ns, T, t)) Ts = |
|
157 |
map (fn (t', t'') => (Abs (ns, T, t'), t'')) (cnt_walk t (T::Ts)) |
|
158 |
| cnt_walk (f $ g) Ts = let |
|
159 |
val n = length Ts - 1 |
|
160 |
in |
|
161 |
map (fn (f', t) => (f' $ g, t)) (cnt_walk f Ts) @ |
|
162 |
map (fn (g', t) => (f $ g', t)) (cnt_walk g Ts) @ |
|
163 |
(if is_countable (type_of1 (Ts, g)) andalso loose_bvar1 (g, n) |
|
164 |
andalso indep g n 0 andalso g <> Bound n |
|
165 |
then [(f $ Bound (n + 1), incr_boundvars (~ n) g)] |
|
166 |
else []) |
|
167 |
end |
|
168 |
| cnt_walk _ _ = [] |
|
169 |
in map (fn (t1, t2) => let |
|
170 |
val T1 = type_of1 ([T], t2) |
|
171 |
val T2 = type_of1 ([T], t) |
|
172 |
in ([SOME (Abs (n, T1, Abs (n, T, t1))), NONE, NONE, SOME (Abs (n, T, t2))], |
|
173 |
[SOME T1, SOME T, SOME T2]) |
|
174 |
end) (cnt_walk t [T]) |
|
175 |
end |
|
176 |
| cnt_prefixes _ _ = [] |
|
177 |
||
59047 | 178 |
fun measurable_tac ctxt facts = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50387
diff
changeset
|
179 |
let |
59048 | 180 |
fun debug_fact msg thm () = |
181 |
msg ^ " " ^ Pretty.str_of (Syntax.pretty_term ctxt (prop_of thm)) |
|
182 |
||
183 |
fun IF' c t i = COND (c i) (t i) no_tac |
|
184 |
||
185 |
fun r_tac msg = |
|
186 |
if Config.get ctxt debug |
|
187 |
then FIRST' o |
|
188 |
map (fn thm => resolve_tac [thm] |
|
189 |
THEN' K (debug_tac ctxt (debug_fact (msg ^ "resolved using") thm) all_tac)) |
|
190 |
else resolve_tac |
|
191 |
||
192 |
val elem_congI = @{lemma "A = B \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A" by simp} |
|
193 |
||
194 |
val dests = get_dest (Context.Proof ctxt) |
|
195 |
fun prep_dest thm = |
|
196 |
(if is_too_generic thm then [] else [thm] @ map_filter (try (fn th' => thm RS th')) dests) ; |
|
197 |
val preprocessors = (("std", prep_dest #> pair) :: get_preprocessors ctxt) ; |
|
198 |
fun preprocess_thm (thm, raw) = |
|
199 |
if raw then pair [thm] else fold_map (fn (_, proc) => proc thm) preprocessors #>> flat |
|
200 |
||
201 |
fun sel lv (th, (raw, lv')) = if lv = lv' then SOME (th, raw) else NONE ; |
|
202 |
fun get lv = ctxt |> Context.Proof |> get_thms |> rev |> map_filter (sel lv) ; |
|
203 |
val pre_thms = map (Simplifier.norm_hhf ctxt #> rpair false) facts @ get Concrete @ get Generic |
|
204 |
||
205 |
val (thms, ctxt) = fold_map preprocess_thm pre_thms ctxt |>> flat |
|
50387 | 206 |
|
59048 | 207 |
fun is_sets_eq (Const (@{const_name "HOL.eq"}, _) $ |
208 |
(Const (@{const_name "sets"}, _) $ _) $ |
|
209 |
(Const (@{const_name "sets"}, _) $ _)) = true |
|
210 |
| is_sets_eq (Const (@{const_name "HOL.eq"}, _) $ |
|
211 |
(Const (@{const_name "measurable"}, _) $ _ $ _) $ |
|
212 |
(Const (@{const_name "measurable"}, _) $ _ $ _)) = true |
|
213 |
| is_sets_eq _ = false |
|
214 |
||
215 |
val cong_thms = get_cong (Context.Proof ctxt) @ |
|
216 |
filter (fn thm => concl_of thm |> HOLogic.dest_Trueprop |> is_sets_eq handle TERM _ => false) facts |
|
217 |
||
218 |
fun sets_cong_tac i = |
|
219 |
Subgoal.FOCUS (fn {context = ctxt', prems = prems, ...} => ( |
|
220 |
let |
|
221 |
val ctxt'' = Simplifier.add_prems prems ctxt' |
|
222 |
in |
|
223 |
r_tac "cong intro" [elem_congI] |
|
224 |
THEN' SOLVED' (fn i => REPEAT_DETERM ( |
|
225 |
((r_tac "cong solve" (cong_thms @ [@{thm refl}]) |
|
226 |
ORELSE' IF' (fn i => fn thm => nprems_of thm > i) |
|
227 |
(SOLVED' (asm_full_simp_tac ctxt''))) i))) |
|
228 |
end) 1) ctxt i |
|
229 |
THEN flexflex_tac ctxt |
|
230 |
||
231 |
val simp_solver_tac = |
|
232 |
IF' not_measurable_prop (debug_tac ctxt (K "simp ") o SOLVED' (asm_full_simp_tac ctxt)) |
|
233 |
||
234 |
val split_countable_tac = |
|
235 |
Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) => |
|
236 |
let |
|
237 |
val f = dest_measurable_fun (HOLogic.dest_Trueprop t) |
|
238 |
fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt))) |
|
239 |
fun inst (ts, Ts) = |
|
240 |
Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts) @{thm measurable_compose_countable} |
|
241 |
in r_tac "split countable" (cnt_prefixes ctxt f |> map inst) i end |
|
242 |
handle TERM _ => no_tac) 1) |
|
50387 | 243 |
|
244 |
val splitter = if Config.get ctxt split then split_countable_tac ctxt else K no_tac |
|
245 |
||
59048 | 246 |
val split_app_tac = |
247 |
Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) => |
|
248 |
let |
|
249 |
fun app_prefixes (Abs (n, T, (f $ g))) = let |
|
250 |
val ps = (if not (loose_bvar1 (g, 0)) then [(f, g)] else []) |
|
251 |
in map (fn (f, c) => (Abs (n, T, f), c, T, type_of c, type_of1 ([T], f $ c))) ps end |
|
252 |
| app_prefixes _ = [] |
|
253 |
||
254 |
fun dest_app (Abs (_, T, t as ((f $ Bound 0) $ c))) = (f, c, T, type_of c, type_of1 ([T], t)) |
|
255 |
| dest_app t = raise (TERM ("not a measurability predicate of an application", [t])) |
|
256 |
val thy = Proof_Context.theory_of ctxt |
|
257 |
val tunify = Sign.typ_unify thy |
|
258 |
val thms = map |
|
259 |
(fn thm => (thm, dest_app (dest_measurable_fun (HOLogic.dest_Trueprop (concl_of thm))))) |
|
260 |
(get_app (Context.Proof ctxt)) |
|
261 |
fun cert f = map (fn (t, t') => (f thy t, f thy t')) |
|
262 |
fun inst (f, c, T, Tc, Tf) (thm, (thmf, thmc, thmT, thmTc, thmTf)) = |
|
263 |
let |
|
264 |
val inst = |
|
265 |
(Vartab.empty, ~1) |
|
266 |
|> tunify (T, thmT) |
|
267 |
|> tunify (Tf, thmTf) |
|
268 |
|> tunify (Tc, thmTc) |
|
269 |
|> Vartab.dest o fst |
|
270 |
val subst = subst_TVars (map (apsnd snd) inst) |
|
271 |
in |
|
272 |
Thm.instantiate (cert ctyp_of (map (fn (n, (s, T)) => (TVar (n, s), T)) inst), |
|
273 |
cert cterm_of [(subst thmf, f), (subst thmc, c)]) thm |
|
274 |
end |
|
275 |
val cps = map_product inst (app_prefixes (dest_measurable_fun (HOLogic.dest_Trueprop t))) thms |
|
276 |
in if null cps then no_tac |
|
277 |
else r_tac "split app" cps i ORELSE debug_tac ctxt (fn () => "split app fun FAILED") no_tac end |
|
278 |
handle TERM t => debug_tac ctxt (fn () => "TERM " ^ fst t ^ Pretty.str_of (Pretty.list "[" "]" (map (Syntax.pretty_term ctxt) (snd t)))) no_tac |
|
279 |
handle Type.TUNIFY => debug_tac ctxt (fn () => "TUNIFY") no_tac) 1) |
|
50387 | 280 |
|
59048 | 281 |
val single_step_tac = |
282 |
simp_solver_tac |
|
283 |
ORELSE' r_tac "step" thms |
|
284 |
ORELSE' (split_app_tac ctxt) |
|
285 |
ORELSE' splitter |
|
286 |
ORELSE' (CHANGED o sets_cong_tac) |
|
287 |
ORELSE' (K (debug_tac ctxt (K "backtrack") no_tac)) |
|
50387 | 288 |
|
59048 | 289 |
in debug_tac ctxt (K "start") (REPEAT (single_step_tac 1)) end; |
50387 | 290 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50387
diff
changeset
|
291 |
fun simproc ctxt redex = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50387
diff
changeset
|
292 |
let |
50387 | 293 |
val t = HOLogic.mk_Trueprop (term_of redex); |
294 |
fun tac {context = ctxt, prems = _ } = |
|
59047 | 295 |
SOLVE (measurable_tac ctxt (Simplifier.prems_of ctxt)); |
50387 | 296 |
in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end; |
297 |
||
298 |
end |
|
299 |