author | wenzelm |
Fri, 21 Apr 2023 15:14:14 +0200 | |
changeset 77899 | c6fcf32010d1 |
parent 77898 | b03c64699af0 |
child 77900 | 42214742b44a |
permissions | -rw-r--r-- |
63627 | 1 |
(* Title: HOL/Analysis/measurable.ML |
50387 | 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 dest_thm_attr : attribute context_parser |
59048 | 14 |
val cong_thm_attr : attribute context_parser |
59047 | 15 |
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
|
16 |
|
59048 | 17 |
val add_del_cong_thm : bool -> thm -> Context.generic -> Context.generic ; |
18 |
||
19 |
val get_all : Context.generic -> thm list |
|
20 |
val get_dest : Context.generic -> thm list |
|
21 |
val get_cong : Context.generic -> thm list |
|
22 |
||
50387 | 23 |
val measurable_tac : Proof.context -> thm list -> tactic |
24 |
||
53043
8cbfbeb566a4
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm
parents:
51717
diff
changeset
|
25 |
val simproc : Proof.context -> cterm -> thm option |
50387 | 26 |
|
59048 | 27 |
val add_preprocessor : string -> preprocessor -> Context.generic -> Context.generic |
28 |
val del_preprocessor : string -> Context.generic -> Context.generic |
|
29 |
val add_local_cong : thm -> Proof.context -> Proof.context |
|
59353
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
30 |
|
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
31 |
val prepare_facts : Proof.context -> thm list -> (thm list * Proof.context) |
50387 | 32 |
end ; |
33 |
||
34 |
structure Measurable : MEASURABLE = |
|
35 |
struct |
|
36 |
||
77898 | 37 |
type preprocessor = thm -> Proof.context -> thm list * Proof.context |
59048 | 38 |
|
50387 | 39 |
datatype level = Concrete | Generic; |
40 |
||
77898 | 41 |
type measurable_thm = thm * (bool * level); |
42 |
||
43 |
fun eq_measurable_thm ((th1, d1): measurable_thm, (th2, d2): measurable_thm) = |
|
59047 | 44 |
d1 = d2 andalso Thm.eq_thm_prop (th1, th2) ; |
45 |
||
77899 | 46 |
fun merge_preprocessors (xs: (string * preprocessor) list, ys) = |
77898 | 47 |
xs @ (filter (fn (name, _) => is_none (find_first (fn (name', _) => name' = name) xs)) ys) |
59048 | 48 |
|
50387 | 49 |
structure Data = Generic_Data |
50 |
( |
|
77898 | 51 |
type T = |
77899 | 52 |
measurable_thm Item_Net.T * |
53 |
(*dest_thms*) thm Item_Net.T * |
|
54 |
(*cong_thms*) thm Item_Net.T * |
|
55 |
(string * preprocessor) list |
|
77898 | 56 |
val empty: T = |
77899 | 57 |
(Item_Net.init eq_measurable_thm (single o Thm.prop_of o fst), Thm.item_net, Thm.item_net, []) |
77898 | 58 |
fun merge |
77899 | 59 |
((measurable_thms1, dest_thms1, cong_thms1, preprocessors1), |
60 |
(measurable_thms2, dest_thms2, cong_thms2, preprocessors2)) : T = |
|
61 |
(Item_Net.merge (measurable_thms1, measurable_thms2), |
|
62 |
Item_Net.merge (dest_thms1, dest_thms2), |
|
63 |
Item_Net.merge (cong_thms1, cong_thms2), |
|
64 |
merge_preprocessors (preprocessors1, preprocessors2)) |
|
50387 | 65 |
); |
66 |
||
77899 | 67 |
val map_measurable_thms = Data.map o @{apply 4(1)} |
68 |
val map_dest_thms = Data.map o @{apply 4(2)} |
|
69 |
val map_cong_thms = Data.map o @{apply 4(3)} |
|
70 |
val map_preprocessors = Data.map o @{apply 4(4)} |
|
50387 | 71 |
|
77899 | 72 |
val debug = Attrib.setup_config_bool \<^binding>\<open>measurable_debug\<close> (K false) |
73 |
val split = Attrib.setup_config_bool \<^binding>\<open>measurable_split\<close> (K true) |
|
50387 | 74 |
|
59992 | 75 |
fun generic_add_del map : attribute context_parser = |
59047 | 76 |
Scan.lift |
77 |
(Args.add >> K Item_Net.update || Args.del >> K Item_Net.remove || Scan.succeed Item_Net.update) >> |
|
77899 | 78 |
(fn f => Thm.declaration_attribute (map o f)) |
59047 | 79 |
|
80 |
val dest_thm_attr = generic_add_del map_dest_thms |
|
59048 | 81 |
val cong_thm_attr = generic_add_del map_cong_thms |
82 |
||
59047 | 83 |
fun del_thm th net = |
84 |
let |
|
85 |
val thms = net |> Item_Net.content |> filter (fn (th', _) => Thm.eq_thm (th, th')) |
|
86 |
in fold Item_Net.remove thms net end ; |
|
87 |
||
88 |
fun measurable_thm_attr (do_add, d) = Thm.declaration_attribute |
|
77899 | 89 |
(map_measurable_thms o (if do_add then Item_Net.update o rpair d else del_thm)) |
50387 | 90 |
|
77899 | 91 |
val get_dest = Item_Net.content o #2 o Data.get; |
50387 | 92 |
|
77899 | 93 |
val get_cong = Item_Net.content o #3 o Data.get; |
94 |
val add_cong = map_cong_thms o Item_Net.update; |
|
95 |
val del_cong = map_cong_thms o Item_Net.remove; |
|
59048 | 96 |
fun add_del_cong_thm true = add_cong |
97 |
| add_del_cong_thm false = del_cong |
|
98 |
||
77899 | 99 |
fun add_preprocessor name f = map_preprocessors (fn xs => xs @ [(name, f)]) |
100 |
fun del_preprocessor name = map_preprocessors (filter (fn (n, _) => n <> name)) |
|
59048 | 101 |
val add_local_cong = Context.proof_map o add_cong |
102 |
||
77899 | 103 |
val get_preprocessors = Context.Proof #> Data.get #> #4; |
59048 | 104 |
|
50387 | 105 |
fun is_too_generic thm = |
106 |
let |
|
59582 | 107 |
val concl = Thm.concl_of thm |
50387 | 108 |
val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl |
109 |
in is_Var (head_of concl') end |
|
110 |
||
77899 | 111 |
val get_thms = Data.get #> #1 #> Item_Net.content ; |
58965 | 112 |
|
59048 | 113 |
val get_all = get_thms #> map fst ; |
50387 | 114 |
|
59048 | 115 |
fun debug_tac ctxt msg f = |
116 |
if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f |
|
50387 | 117 |
|
118 |
fun nth_hol_goal thm i = |
|
59582 | 119 |
HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (Thm.prems_of thm) (i - 1)))) |
50387 | 120 |
|
121 |
fun dest_measurable_fun t = |
|
122 |
(case t of |
|
74632 | 123 |
\<^Const_>\<open>Set.member _ for f \<^Const_>\<open>measurable _ _ for _ _\<close>\<close> => f |
50387 | 124 |
| _ => raise (TERM ("not a measurability predicate", [t]))) |
125 |
||
59582 | 126 |
fun not_measurable_prop n thm = |
127 |
if length (Thm.prems_of thm) < n then false |
|
128 |
else |
|
129 |
(case nth_hol_goal thm n of |
|
74632 | 130 |
\<^Const_>\<open>Set.member _ for _ \<^Const_>\<open>sets _ for _\<close>\<close> => false |
131 |
| \<^Const_>\<open>Set.member _ for _ \<^Const_>\<open>measurable _ _ for _ _\<close>\<close> => false |
|
59582 | 132 |
| _ => true) |
133 |
handle TERM _ => true; |
|
50387 | 134 |
|
135 |
fun indep (Bound i) t b = i < b orelse t <= i |
|
136 |
| indep (f $ t) top bot = indep f top bot andalso indep t top bot |
|
137 |
| indep (Abs (_,_,t)) top bot = indep t (top + 1) (bot + 1) |
|
138 |
| indep _ _ _ = true; |
|
139 |
||
59837 | 140 |
fun cnt_prefixes ctxt (Abs (n, T, t)) = |
141 |
let |
|
69597 | 142 |
fun is_countable ty = Sign.of_sort (Proof_Context.theory_of ctxt) (ty, \<^sort>\<open>countable\<close>) |
50387 | 143 |
fun cnt_walk (Abs (ns, T, t)) Ts = |
144 |
map (fn (t', t'') => (Abs (ns, T, t'), t'')) (cnt_walk t (T::Ts)) |
|
145 |
| cnt_walk (f $ g) Ts = let |
|
146 |
val n = length Ts - 1 |
|
147 |
in |
|
148 |
map (fn (f', t) => (f' $ g, t)) (cnt_walk f Ts) @ |
|
149 |
map (fn (g', t) => (f $ g', t)) (cnt_walk g Ts) @ |
|
150 |
(if is_countable (type_of1 (Ts, g)) andalso loose_bvar1 (g, n) |
|
151 |
andalso indep g n 0 andalso g <> Bound n |
|
152 |
then [(f $ Bound (n + 1), incr_boundvars (~ n) g)] |
|
153 |
else []) |
|
154 |
end |
|
155 |
| cnt_walk _ _ = [] |
|
156 |
in map (fn (t1, t2) => let |
|
157 |
val T1 = type_of1 ([T], t2) |
|
158 |
val T2 = type_of1 ([T], t) |
|
159 |
in ([SOME (Abs (n, T1, Abs (n, T, t1))), NONE, NONE, SOME (Abs (n, T, t2))], |
|
160 |
[SOME T1, SOME T, SOME T2]) |
|
161 |
end) (cnt_walk t [T]) |
|
162 |
end |
|
163 |
| cnt_prefixes _ _ = [] |
|
164 |
||
59353
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
165 |
fun apply_dests thm dests = |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
166 |
let |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
167 |
fun apply thm th' = |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
168 |
let |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
169 |
val th'' = thm RS th' |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
170 |
in [th''] @ loop th'' end |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
171 |
handle (THM _) => [] |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
172 |
and loop thm = |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
173 |
flat (map (apply thm) dests) |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
174 |
in |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
175 |
[thm] @ ([thm RS @{thm measurable_compose_rev}] handle (THM _) => []) @ loop thm |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
176 |
end |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
177 |
|
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
178 |
fun prepare_facts ctxt facts = |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
179 |
let |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
180 |
val dests = get_dest (Context.Proof ctxt) |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
181 |
fun prep_dest thm = |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
182 |
(if is_too_generic thm then [] else apply_dests thm dests) ; |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
183 |
val preprocessors = (("std", prep_dest #> pair) :: get_preprocessors ctxt) ; |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
184 |
fun preprocess_thm (thm, raw) = |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
185 |
if raw then pair [thm] else fold_map (fn (_, proc) => proc thm) preprocessors #>> flat |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
186 |
|
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
187 |
fun sel lv (th, (raw, lv')) = if lv = lv' then SOME (th, raw) else NONE ; |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
188 |
fun get lv = ctxt |> Context.Proof |> get_thms |> rev |> map_filter (sel lv) ; |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
189 |
val pre_thms = map (Simplifier.norm_hhf ctxt #> rpair false) facts @ get Concrete @ get Generic |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
190 |
|
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
191 |
val (thms, ctxt) = fold_map preprocess_thm pre_thms ctxt |>> flat |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
192 |
in (thms, ctxt) end |
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
193 |
|
59047 | 194 |
fun measurable_tac ctxt facts = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50387
diff
changeset
|
195 |
let |
59048 | 196 |
fun debug_fact msg thm () = |
61877
276ad4354069
renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
wenzelm
parents:
61424
diff
changeset
|
197 |
msg ^ " " ^ Pretty.unformatted_string_of (Syntax.pretty_term ctxt (Thm.prop_of thm)) |
59048 | 198 |
|
199 |
fun IF' c t i = COND (c i) (t i) no_tac |
|
200 |
||
201 |
fun r_tac msg = |
|
202 |
if Config.get ctxt debug |
|
203 |
then FIRST' o |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59353
diff
changeset
|
204 |
map (fn thm => resolve_tac ctxt [thm] |
59353
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
205 |
THEN' K (debug_tac ctxt (debug_fact (msg ^ " resolved using") thm) all_tac)) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59353
diff
changeset
|
206 |
else resolve_tac ctxt |
59048 | 207 |
|
59353
f0707dc3d9aa
measurability prover: removed app splitting, replaced by more powerful destruction rules
hoelzl
parents:
59048
diff
changeset
|
208 |
val (thms, ctxt) = prepare_facts ctxt facts |
50387 | 209 |
|
74632 | 210 |
fun is_sets_eq \<^Const_>\<open>HOL.eq _ for |
211 |
\<^Const_>\<open>sets _ for _\<close> \<^Const_>\<open>sets _ for _\<close>\<close> = true |
|
212 |
| is_sets_eq \<^Const_>\<open>HOL.eq _ for |
|
213 |
\<^Const_>\<open>measurable _ _ for _ _\<close> \<^Const_>\<open>measurable _ _ for _ _\<close>\<close> = true |
|
59048 | 214 |
| is_sets_eq _ = false |
215 |
||
216 |
val cong_thms = get_cong (Context.Proof ctxt) @ |
|
59582 | 217 |
filter (fn thm => Thm.concl_of thm |> HOLogic.dest_Trueprop |> is_sets_eq handle TERM _ => false) facts |
59048 | 218 |
|
219 |
fun sets_cong_tac i = |
|
220 |
Subgoal.FOCUS (fn {context = ctxt', prems = prems, ...} => ( |
|
221 |
let |
|
222 |
val ctxt'' = Simplifier.add_prems prems ctxt' |
|
223 |
in |
|
74632 | 224 |
r_tac "cong intro" [@{lemma "A = B \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A" by simp}] |
59048 | 225 |
THEN' SOLVED' (fn i => REPEAT_DETERM ( |
226 |
((r_tac "cong solve" (cong_thms @ [@{thm refl}]) |
|
59582 | 227 |
ORELSE' IF' (fn i => fn thm => Thm.nprems_of thm > i) |
59048 | 228 |
(SOLVED' (asm_full_simp_tac ctxt''))) i))) |
229 |
end) 1) ctxt i |
|
230 |
THEN flexflex_tac ctxt |
|
231 |
||
232 |
val simp_solver_tac = |
|
233 |
IF' not_measurable_prop (debug_tac ctxt (K "simp ") o SOLVED' (asm_full_simp_tac ctxt)) |
|
234 |
||
235 |
val split_countable_tac = |
|
236 |
Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) => |
|
237 |
let |
|
238 |
val f = dest_measurable_fun (HOLogic.dest_Trueprop t) |
|
239 |
fun inst (ts, Ts) = |
|
60807 | 240 |
Thm.instantiate' |
241 |
(map (Option.map (Thm.ctyp_of ctxt)) Ts) |
|
242 |
(map (Option.map (Thm.cterm_of ctxt)) ts) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59353
diff
changeset
|
243 |
@{thm measurable_compose_countable} |
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
60807
diff
changeset
|
244 |
in r_tac "case_prod countable" (cnt_prefixes ctxt f |> map inst) i end |
59048 | 245 |
handle TERM _ => no_tac) 1) |
50387 | 246 |
|
247 |
val splitter = if Config.get ctxt split then split_countable_tac ctxt else K no_tac |
|
248 |
||
59048 | 249 |
val single_step_tac = |
250 |
simp_solver_tac |
|
251 |
ORELSE' r_tac "step" thms |
|
252 |
ORELSE' splitter |
|
253 |
ORELSE' (CHANGED o sets_cong_tac) |
|
254 |
ORELSE' (K (debug_tac ctxt (K "backtrack") no_tac)) |
|
50387 | 255 |
|
59048 | 256 |
in debug_tac ctxt (K "start") (REPEAT (single_step_tac 1)) end; |
50387 | 257 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50387
diff
changeset
|
258 |
fun simproc ctxt redex = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50387
diff
changeset
|
259 |
let |
59582 | 260 |
val t = HOLogic.mk_Trueprop (Thm.term_of redex); |
50387 | 261 |
fun tac {context = ctxt, prems = _ } = |
59047 | 262 |
SOLVE (measurable_tac ctxt (Simplifier.prems_of ctxt)); |
73551 | 263 |
in \<^try>\<open>Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}\<close> end; |
50387 | 264 |
|
265 |
end |
|
266 |