49 by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric]) |
49 by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric]) |
50 |
50 |
51 ML_file "measurable.ML" |
51 ML_file "measurable.ML" |
52 |
52 |
53 attribute_setup measurable = {* |
53 attribute_setup measurable = {* |
54 Scan.lift (Scan.optional (Args.$$$ "del" >> K false) true -- |
54 Scan.lift ( |
55 Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false -- |
55 (Args.add >> K true || Args.del >> K false || Scan.succeed true) -- |
|
56 Scan.optional (Args.parens ( |
|
57 Scan.optional (Args.$$$ "raw" >> K true) false -- |
56 Scan.optional (Args.$$$ "generic" >> K Measurable.Generic) Measurable.Concrete)) |
58 Scan.optional (Args.$$$ "generic" >> K Measurable.Generic) Measurable.Concrete)) |
57 (false, Measurable.Concrete) >> (Thm.declaration_attribute o uncurry Measurable.add_del_thm)) |
59 (false, Measurable.Concrete) >> |
|
60 Measurable.measurable_thm_attr) |
58 *} "declaration of measurability theorems" |
61 *} "declaration of measurability theorems" |
59 |
62 |
60 attribute_setup measurable_dest = {* |
63 attribute_setup measurable_dest = Measurable.dest_thm_attr |
61 Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_dest)) |
64 "add dest rule for measurability prover" |
62 *} "add dest rule for measurability prover" |
65 |
63 |
66 attribute_setup measurable_app = Measurable.app_thm_attr |
64 attribute_setup measurable_app = {* |
67 "add application rule for measurability prover" |
65 Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_app)) |
68 |
66 *} "add application rule for measurability prover" |
69 method_setup measurable = \<open> Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \<close> |
67 |
70 "measurability prover" |
68 method_setup measurable = {* |
|
69 Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => Measurable.measurable_tac ctxt facts))) |
|
70 *} "measurability prover" |
|
71 |
71 |
72 simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *} |
72 simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *} |
73 |
73 |
74 setup {* |
74 setup {* |
75 Global_Theory.add_thms_dynamic (@{binding measurable}, Measurable.get_all o Context.proof_of) |
75 Global_Theory.add_thms_dynamic (@{binding measurable}, Measurable.get_all o Context.proof_of) |