41 type measurable_thm = thm * (bool * level); |
41 type measurable_thm = thm * (bool * level); |
42 |
42 |
43 fun eq_measurable_thm ((th1, d1): measurable_thm, (th2, d2): measurable_thm) = |
43 fun eq_measurable_thm ((th1, d1): measurable_thm, (th2, d2): measurable_thm) = |
44 d1 = d2 andalso Thm.eq_thm_prop (th1, th2) ; |
44 d1 = d2 andalso Thm.eq_thm_prop (th1, th2) ; |
45 |
45 |
46 fun merge_dups (xs:(string * preprocessor) list) ys = |
46 fun merge_preprocessors (xs: (string * preprocessor) list, ys) = |
47 xs @ (filter (fn (name, _) => is_none (find_first (fn (name', _) => name' = name) xs)) ys) |
47 xs @ (filter (fn (name, _) => is_none (find_first (fn (name', _) => name' = name) xs)) ys) |
48 |
48 |
49 structure Data = Generic_Data |
49 structure Data = Generic_Data |
50 ( |
50 ( |
51 type T = |
51 type T = |
52 {measurable_thms : measurable_thm Item_Net.T, |
52 measurable_thm Item_Net.T * |
53 dest_thms : thm Item_Net.T, |
53 (*dest_thms*) thm Item_Net.T * |
54 cong_thms : thm Item_Net.T, |
54 (*cong_thms*) thm Item_Net.T * |
55 preprocessors : (string * preprocessor) list}; |
55 (string * preprocessor) list |
56 val empty: T = |
56 val empty: T = |
57 {measurable_thms = Item_Net.init eq_measurable_thm (single o Thm.prop_of o fst), |
57 (Item_Net.init eq_measurable_thm (single o Thm.prop_of o fst), Thm.item_net, Thm.item_net, []) |
58 dest_thms = Thm.item_net, |
|
59 cong_thms = Thm.item_net, |
|
60 preprocessors = []}; |
|
61 fun merge |
58 fun merge |
62 ({measurable_thms = t1, dest_thms = dt1, cong_thms = ct1, preprocessors = i1}, |
59 ((measurable_thms1, dest_thms1, cong_thms1, preprocessors1), |
63 {measurable_thms = t2, dest_thms = dt2, cong_thms = ct2, preprocessors = i2}) : T = |
60 (measurable_thms2, dest_thms2, cong_thms2, preprocessors2)) : T = |
64 {measurable_thms = Item_Net.merge (t1, t2), |
61 (Item_Net.merge (measurable_thms1, measurable_thms2), |
65 dest_thms = Item_Net.merge (dt1, dt2), |
62 Item_Net.merge (dest_thms1, dest_thms2), |
66 cong_thms = Item_Net.merge (ct1, ct2), |
63 Item_Net.merge (cong_thms1, cong_thms2), |
67 preprocessors = merge_dups i1 i2}; |
64 merge_preprocessors (preprocessors1, preprocessors2)) |
68 ); |
65 ); |
69 |
66 |
70 val debug = |
67 val map_measurable_thms = Data.map o @{apply 4(1)} |
71 Attrib.setup_config_bool \<^binding>\<open>measurable_debug\<close> (K false) |
68 val map_dest_thms = Data.map o @{apply 4(2)} |
72 |
69 val map_cong_thms = Data.map o @{apply 4(3)} |
73 val split = |
70 val map_preprocessors = Data.map o @{apply 4(4)} |
74 Attrib.setup_config_bool \<^binding>\<open>measurable_split\<close> (K true) |
71 |
75 |
72 val debug = Attrib.setup_config_bool \<^binding>\<open>measurable_debug\<close> (K false) |
76 fun map_data f1 f2 f3 f4 |
73 val split = Attrib.setup_config_bool \<^binding>\<open>measurable_split\<close> (K true) |
77 {measurable_thms = t1, dest_thms = t2, cong_thms = t3, preprocessors = t4 } = |
|
78 {measurable_thms = f1 t1, dest_thms = f2 t2, cong_thms = f3 t3, preprocessors = f4 t4} |
|
79 |
|
80 fun map_measurable_thms f = map_data f I I I |
|
81 fun map_dest_thms f = map_data I f I I |
|
82 fun map_cong_thms f = map_data I I f I |
|
83 fun map_preprocessors f = map_data I I I f |
|
84 |
74 |
85 fun generic_add_del map : attribute context_parser = |
75 fun generic_add_del map : attribute context_parser = |
86 Scan.lift |
76 Scan.lift |
87 (Args.add >> K Item_Net.update || Args.del >> K Item_Net.remove || Scan.succeed Item_Net.update) >> |
77 (Args.add >> K Item_Net.update || Args.del >> K Item_Net.remove || Scan.succeed Item_Net.update) >> |
88 (fn f => Thm.declaration_attribute (Data.map o map o f)) |
78 (fn f => Thm.declaration_attribute (map o f)) |
89 |
79 |
90 val dest_thm_attr = generic_add_del map_dest_thms |
80 val dest_thm_attr = generic_add_del map_dest_thms |
91 |
|
92 val cong_thm_attr = generic_add_del map_cong_thms |
81 val cong_thm_attr = generic_add_del map_cong_thms |
93 |
82 |
94 fun del_thm th net = |
83 fun del_thm th net = |
95 let |
84 let |
96 val thms = net |> Item_Net.content |> filter (fn (th', _) => Thm.eq_thm (th, th')) |
85 val thms = net |> Item_Net.content |> filter (fn (th', _) => Thm.eq_thm (th, th')) |
97 in fold Item_Net.remove thms net end ; |
86 in fold Item_Net.remove thms net end ; |
98 |
87 |
99 fun measurable_thm_attr (do_add, d) = Thm.declaration_attribute |
88 fun measurable_thm_attr (do_add, d) = Thm.declaration_attribute |
100 (Data.map o map_measurable_thms o (if do_add then Item_Net.update o rpair d else del_thm)) |
89 (map_measurable_thms o (if do_add then Item_Net.update o rpair d else del_thm)) |
101 |
90 |
102 val get_dest = Item_Net.content o #dest_thms o Data.get; |
91 val get_dest = Item_Net.content o #2 o Data.get; |
103 |
92 |
104 val get_cong = Item_Net.content o #cong_thms o Data.get; |
93 val get_cong = Item_Net.content o #3 o Data.get; |
105 val add_cong = Data.map o map_cong_thms o Item_Net.update; |
94 val add_cong = map_cong_thms o Item_Net.update; |
106 val del_cong = Data.map o map_cong_thms o Item_Net.remove; |
95 val del_cong = map_cong_thms o Item_Net.remove; |
107 fun add_del_cong_thm true = add_cong |
96 fun add_del_cong_thm true = add_cong |
108 | add_del_cong_thm false = del_cong |
97 | add_del_cong_thm false = del_cong |
109 |
98 |
110 fun add_preprocessor name f = Data.map (map_preprocessors (fn xs => xs @ [(name, f)])) |
99 fun add_preprocessor name f = map_preprocessors (fn xs => xs @ [(name, f)]) |
111 fun del_preprocessor name = Data.map (map_preprocessors (filter (fn (n, _) => n <> name))) |
100 fun del_preprocessor name = map_preprocessors (filter (fn (n, _) => n <> name)) |
112 val add_local_cong = Context.proof_map o add_cong |
101 val add_local_cong = Context.proof_map o add_cong |
113 |
102 |
114 val get_preprocessors = Context.Proof #> Data.get #> #preprocessors ; |
103 val get_preprocessors = Context.Proof #> Data.get #> #4; |
115 |
104 |
116 fun is_too_generic thm = |
105 fun is_too_generic thm = |
117 let |
106 let |
118 val concl = Thm.concl_of thm |
107 val concl = Thm.concl_of thm |
119 val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl |
108 val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl |
120 in is_Var (head_of concl') end |
109 in is_Var (head_of concl') end |
121 |
110 |
122 val get_thms = Data.get #> #measurable_thms #> Item_Net.content ; |
111 val get_thms = Data.get #> #1 #> Item_Net.content ; |
123 |
112 |
124 val get_all = get_thms #> map fst ; |
113 val get_all = get_thms #> map fst ; |
125 |
114 |
126 fun debug_tac ctxt msg f = |
115 fun debug_tac ctxt msg f = |
127 if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f |
116 if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f |