1 signature REIFY_TABLE = |
1 signature REIFY_TABLE = |
2 sig |
2 sig |
3 type table |
3 |
4 val empty : table |
4 type table |
5 val get_var : term -> table -> (int * table) |
5 val empty : table |
6 val get_term : int -> table -> term option |
6 val get_var : term -> table -> (int * table) |
|
7 val get_term : int -> table -> term option |
|
8 |
7 end |
9 end |
8 |
10 |
9 structure Reifytab: REIFY_TABLE = |
11 structure Reifytab: REIFY_TABLE = |
10 struct |
12 struct |
11 type table = (int * (term * int) list) |
13 type table = (int * (term * int) list) |
12 |
14 |
13 val empty = (0, []) |
15 val empty = (0, []) |
14 |
16 |
15 fun get_var t (max_var, tis) = |
17 fun get_var t (max_var, tis) = |
16 (case AList.lookup Envir.aeconv tis t of |
18 (case AList.lookup Envir.aeconv tis t of |
17 SOME v => (v, (max_var, tis)) |
19 SOME v => (v, (max_var, tis)) |
18 | NONE => (max_var, (max_var + 1, (t, max_var) :: tis)) |
20 | NONE => (max_var, (max_var + 1, (t, max_var) :: tis)) |
19 ) |
21 ) |
20 |
22 |
21 fun get_term v (_, tis) = Library.find_first (fn (_, v2) => v = v2) tis |
23 fun get_term v (_, tis) = Library.find_first (fn (_, v2) => v = v2) tis |
22 |> Option.map fst |
24 |> Option.map fst |
|
25 |
23 end |
26 end |
24 |
27 |
25 signature LOGIC_SIGNATURE = |
28 signature LOGIC_SIGNATURE = |
26 sig |
29 sig |
27 val mk_Trueprop : term -> term |
30 |
28 val dest_Trueprop : term -> term |
31 val mk_Trueprop : term -> term |
29 val Trueprop_conv : conv -> conv |
32 val dest_Trueprop : term -> term |
30 val Not : term |
33 val Trueprop_conv : conv -> conv |
31 val conj : term |
34 val Not : term |
32 val disj : term |
35 val conj : term |
33 |
36 val disj : term |
34 val notI : thm (* (P \<Longrightarrow> False) \<Longrightarrow> \<not> P *) |
37 |
35 val ccontr : thm (* (\<not> P \<Longrightarrow> False) \<Longrightarrow> P *) |
38 val notI : thm (* (P \<Longrightarrow> False) \<Longrightarrow> \<not> P *) |
36 val conjI : thm (* P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q *) |
39 val ccontr : thm (* (\<not> P \<Longrightarrow> False) \<Longrightarrow> P *) |
37 val conjE : thm (* P \<and> Q \<Longrightarrow> (P \<Longrightarrow> Q \<Longrightarrow> R) \<Longrightarrow> R *) |
40 val conjI : thm (* P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q *) |
38 val disjE : thm (* P \<or> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R *) |
41 val conjE : thm (* P \<and> Q \<Longrightarrow> (P \<Longrightarrow> Q \<Longrightarrow> R) \<Longrightarrow> R *) |
39 |
42 val disjE : thm (* P \<or> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R *) |
40 val not_not_conv : conv (* \<not> (\<not> P) \<equiv> P *) |
43 |
41 val de_Morgan_conj_conv : conv (* \<not> (P \<and> Q) \<equiv> \<not> P \<or> \<not> Q *) |
44 val not_not_conv : conv (* \<not> (\<not> P) \<equiv> P *) |
42 val de_Morgan_disj_conv : conv (* \<not> (P \<or> Q) \<equiv> \<not> P \<and> \<not> Q *) |
45 val de_Morgan_conj_conv : conv (* \<not> (P \<and> Q) \<equiv> \<not> P \<or> \<not> Q *) |
43 val conj_disj_distribL_conv : conv (* P \<and> (Q \<or> R) \<equiv> (P \<and> Q) \<or> (P \<and> R) *) |
46 val de_Morgan_disj_conv : conv (* \<not> (P \<or> Q) \<equiv> \<not> P \<and> \<not> Q *) |
44 val conj_disj_distribR_conv : conv (* (Q \<or> R) \<and> P \<equiv> (Q \<and> P) \<or> (R \<and> P) *) |
47 val conj_disj_distribL_conv : conv (* P \<and> (Q \<or> R) \<equiv> (P \<and> Q) \<or> (P \<and> R) *) |
|
48 val conj_disj_distribR_conv : conv (* (Q \<or> R) \<and> P \<equiv> (Q \<and> P) \<or> (R \<and> P) *) |
|
49 |
45 end |
50 end |
46 |
51 |
47 signature BASE_ORDER_TAC_BASE = |
52 signature BASE_ORDER_TAC_BASE = |
48 sig |
53 sig |
49 |
54 |
50 val order_trace_cfg : bool Config.T |
55 val order_trace_cfg : bool Config.T |
51 val order_split_limit_cfg : int Config.T |
56 val order_split_limit_cfg : int Config.T |
52 |
57 |
53 datatype order_kind = Order | Linorder |
58 datatype order_kind = Order | Linorder |
54 |
59 |
55 type order_literal = (bool * Order_Procedure.order_atom) |
60 type order_literal = (bool * Order_Procedure.order_atom) |
56 |
61 |
57 type order_ops = { eq : term, le : term, lt : term } |
62 type order_ops = { eq : term, le : term, lt : term } |
58 |
63 |
59 val map_order_ops : (term -> term) -> order_ops -> order_ops |
64 val map_order_ops : (term -> term) -> order_ops -> order_ops |
60 |
65 |
61 type order_context = { |
66 type order_context = { |
62 kind : order_kind, |
67 kind : order_kind, |
63 ops : order_ops, |
68 ops : order_ops, |
64 thms : (string * thm) list, conv_thms : (string * thm) list |
69 thms : (string * thm) list, conv_thms : (string * thm) list |
65 } |
70 } |
66 |
71 |
67 end |
72 end |
68 |
73 |
69 structure Base_Order_Tac_Base : BASE_ORDER_TAC_BASE = |
74 structure Base_Order_Tac_Base : BASE_ORDER_TAC_BASE = |
70 struct |
75 struct |
71 |
76 |
72 (* Control tracing output of the solver. *) |
77 (* Control tracing output of the solver. *) |
73 val order_trace_cfg = Attrib.setup_config_bool @{binding "order_trace"} (K false) |
78 val order_trace_cfg = Attrib.setup_config_bool @{binding "order_trace"} (K false) |
74 (* In partial orders, literals of the form \<not> x < y will force the order solver to perform case |
79 (* In partial orders, literals of the form \<not> x < y will force the order solver to perform case |
75 distinctions, which leads to an exponential blowup of the runtime. The split limit controls |
80 distinctions, which leads to an exponential blowup of the runtime. The split limit controls |
76 the number of literals of this form that are passed to the solver. |
81 the number of literals of this form that are passed to the solver. |
77 *) |
82 *) |
78 val order_split_limit_cfg = Attrib.setup_config_int @{binding "order_split_limit"} (K 8) |
83 val order_split_limit_cfg = Attrib.setup_config_int @{binding "order_split_limit"} (K 8) |
79 |
84 |
80 datatype order_kind = Order | Linorder |
85 datatype order_kind = Order | Linorder |
81 |
86 |
82 type order_literal = (bool * Order_Procedure.order_atom) |
87 type order_literal = (bool * Order_Procedure.order_atom) |
83 |
88 |
84 type order_ops = { eq : term, le : term, lt : term } |
89 type order_ops = { eq : term, le : term, lt : term } |
85 |
90 |
86 fun map_order_ops f {eq, le, lt} = {eq = f eq, le = f le, lt = f lt} |
91 fun map_order_ops f {eq, le, lt} = {eq = f eq, le = f le, lt = f lt} |
87 |
92 |
88 type order_context = { |
93 type order_context = { |
89 kind : order_kind, |
94 kind : order_kind, |
90 ops : order_ops, |
95 ops : order_ops, |
91 thms : (string * thm) list, conv_thms : (string * thm) list |
96 thms : (string * thm) list, conv_thms : (string * thm) list |
92 } |
97 } |
93 |
98 |
94 end |
99 end |
95 |
100 |
96 signature BASE_ORDER_TAC = |
101 signature BASE_ORDER_TAC = |
97 sig |
102 sig |
98 include BASE_ORDER_TAC_BASE |
103 |
99 |
104 include BASE_ORDER_TAC_BASE |
100 type insert_prems_hook = |
105 |
101 order_kind -> order_ops -> Proof.context -> (thm * (bool * term * (term * term))) list |
106 type insert_prems_hook = |
102 -> thm list |
107 order_kind -> order_ops -> Proof.context -> (thm * (bool * term * (term * term))) list |
103 |
108 -> thm list |
104 val declare_insert_prems_hook : |
109 |
105 (binding * insert_prems_hook) -> local_theory -> local_theory |
110 val declare_insert_prems_hook : |
106 |
111 (binding * insert_prems_hook) -> local_theory -> local_theory |
107 val insert_prems_hook_names : Proof.context -> binding list |
112 |
108 |
113 val insert_prems_hook_names : Proof.context -> binding list |
109 val tac : |
114 |
110 (order_literal Order_Procedure.fm -> Order_Procedure.prf_trm option) |
115 val tac : |
111 -> order_context -> thm list |
116 (order_literal Order_Procedure.fm -> Order_Procedure.prf_trm option) |
112 -> Proof.context -> int -> tactic |
117 -> order_context -> thm list |
|
118 -> Proof.context -> int -> tactic |
|
119 |
113 end |
120 end |
114 |
121 |
115 functor Base_Order_Tac( |
122 functor Base_Order_Tac( |
116 structure Logic_Sig : LOGIC_SIGNATURE; val excluded_types : typ list) : BASE_ORDER_TAC = |
123 structure Logic_Sig : LOGIC_SIGNATURE; val excluded_types : typ list) : BASE_ORDER_TAC = |
117 struct |
124 struct |
118 open Base_Order_Tac_Base |
125 |
119 open Order_Procedure |
126 open Base_Order_Tac_Base |
120 |
127 open Order_Procedure |
121 fun expect _ (SOME x) = x |
128 |
122 | expect f NONE = f () |
129 fun expect _ (SOME x) = x |
123 |
130 | expect f NONE = f () |
124 fun list_curry0 f = (fn [] => f, 0) |
131 |
125 fun list_curry1 f = (fn [x] => f x, 1) |
132 fun list_curry0 f = (fn [] => f, 0) |
126 fun list_curry2 f = (fn [x, y] => f x y, 2) |
133 fun list_curry1 f = (fn [x] => f x, 1) |
127 |
134 fun list_curry2 f = (fn [x, y] => f x y, 2) |
128 fun dereify_term consts reifytab t = |
135 |
129 let |
136 fun dereify_term consts reifytab t = |
130 fun dereify_term' (App (t1, t2)) = (dereify_term' t1) $ (dereify_term' t2) |
137 let |
131 | dereify_term' (Const s) = |
138 fun dereify_term' (App (t1, t2)) = (dereify_term' t1) $ (dereify_term' t2) |
132 AList.lookup (op =) consts s |
139 | dereify_term' (Const s) = |
133 |> expect (fn () => raise TERM ("Const " ^ s ^ " not in", map snd consts)) |
140 AList.lookup (op =) consts s |
134 | dereify_term' (Var v) = Reifytab.get_term (integer_of_int v) reifytab |> the |
141 |> expect (fn () => raise TERM ("Const " ^ s ^ " not in", map snd consts)) |
135 in |
142 | dereify_term' (Var v) = Reifytab.get_term (integer_of_int v) reifytab |> the |
136 dereify_term' t |
143 in |
137 end |
144 dereify_term' t |
138 |
145 end |
139 fun dereify_order_fm (eq, le, lt) reifytab t = |
146 |
140 let |
147 fun dereify_order_fm (eq, le, lt) reifytab t = |
141 val consts = [ |
148 let |
142 ("eq", eq), ("le", le), ("lt", lt), |
149 val consts = [ |
143 ("Not", Logic_Sig.Not), ("disj", Logic_Sig.disj), ("conj", Logic_Sig.conj) |
150 ("eq", eq), ("le", le), ("lt", lt), |
144 ] |
151 ("Not", Logic_Sig.Not), ("disj", Logic_Sig.disj), ("conj", Logic_Sig.conj) |
145 in |
152 ] |
146 dereify_term consts reifytab t |
153 in |
147 end |
154 dereify_term consts reifytab t |
148 |
155 end |
149 fun strip_AppP t = |
156 |
150 let fun strip (AppP (f, s), ss) = strip (f, s::ss) |
157 fun strip_AppP t = |
151 | strip x = x |
158 let fun strip (AppP (f, s), ss) = strip (f, s::ss) |
152 in strip (t, []) end |
159 | strip x = x |
153 |
160 in strip (t, []) end |
154 fun replay_conv convs cvp = |
161 |
155 let |
162 fun replay_conv convs cvp = |
156 val convs = convs @ |
163 let |
157 [("all_conv", list_curry0 Conv.all_conv)] @ |
164 val convs = convs @ |
158 map (apsnd list_curry1) [ |
165 [("all_conv", list_curry0 Conv.all_conv)] @ |
159 ("atom_conv", I), |
166 map (apsnd list_curry1) [ |
160 ("neg_atom_conv", I), |
167 ("atom_conv", I), |
161 ("arg_conv", Conv.arg_conv)] @ |
168 ("neg_atom_conv", I), |
162 map (apsnd list_curry2) [ |
169 ("arg_conv", Conv.arg_conv)] @ |
163 ("combination_conv", Conv.combination_conv), |
170 map (apsnd list_curry2) [ |
164 ("then_conv", curry (op then_conv))] |
171 ("combination_conv", Conv.combination_conv), |
165 |
172 ("then_conv", curry (op then_conv))] |
166 fun lookup_conv convs c = AList.lookup (op =) convs c |
173 |
167 |> expect (fn () => error ("Can't replay conversion: " ^ c)) |
174 fun lookup_conv convs c = AList.lookup (op =) convs c |
168 |
175 |> expect (fn () => error ("Can't replay conversion: " ^ c)) |
169 fun rp_conv t = |
176 |
170 (case strip_AppP t ||> map rp_conv of |
177 fun rp_conv t = |
171 (PThm c, cvs) => |
178 (case strip_AppP t ||> map rp_conv of |
172 let val (conv, arity) = lookup_conv convs c |
179 (PThm c, cvs) => |
173 in if arity = length cvs |
180 let val (conv, arity) = lookup_conv convs c |
174 then conv cvs |
181 in if arity = length cvs |
175 else error ("Expected " ^ Int.toString arity ^ " arguments for conversion " ^ |
182 then conv cvs |
176 c ^ " but got " ^ (length cvs |> Int.toString) ^ " arguments") |
183 else error ("Expected " ^ Int.toString arity ^ " arguments for conversion " ^ |
177 end |
184 c ^ " but got " ^ (length cvs |> Int.toString) ^ " arguments") |
178 | _ => error "Unexpected constructor in conversion proof") |
185 end |
179 in |
186 | _ => error "Unexpected constructor in conversion proof") |
180 rp_conv cvp |
187 in |
181 end |
188 rp_conv cvp |
182 |
189 end |
183 fun replay_prf_trm replay_conv dereify ctxt thmtab assmtab p = |
190 |
184 let |
191 fun replay_prf_trm replay_conv dereify ctxt thmtab assmtab p = |
185 fun replay_prf_trm' _ (PThm s) = |
192 let |
186 AList.lookup (op =) thmtab s |
193 fun replay_prf_trm' _ (PThm s) = |
187 |> expect (fn () => error ("Cannot replay theorem: " ^ s)) |
194 AList.lookup (op =) thmtab s |
188 | replay_prf_trm' assmtab (Appt (p, t)) = |
195 |> expect (fn () => error ("Cannot replay theorem: " ^ s)) |
189 replay_prf_trm' assmtab p |
196 | replay_prf_trm' assmtab (Appt (p, t)) = |
190 |> Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt (dereify t))] |
197 replay_prf_trm' assmtab p |
191 | replay_prf_trm' assmtab (AppP (p1, p2)) = |
198 |> Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt (dereify t))] |
192 apply2 (replay_prf_trm' assmtab) (p2, p1) |> op COMP |
199 | replay_prf_trm' assmtab (AppP (p1, p2)) = |
193 | replay_prf_trm' assmtab (AbsP (reified_t, p)) = |
200 apply2 (replay_prf_trm' assmtab) (p2, p1) |> op COMP |
194 let |
201 | replay_prf_trm' assmtab (AbsP (reified_t, p)) = |
195 val t = dereify reified_t |
202 let |
196 val t_thm = Logic_Sig.mk_Trueprop t |> Thm.cterm_of ctxt |> Assumption.assume ctxt |
203 val t = dereify reified_t |
197 val rp = replay_prf_trm' (Termtab.update (Thm.prop_of t_thm, t_thm) assmtab) p |
204 val t_thm = Logic_Sig.mk_Trueprop t |> Thm.cterm_of ctxt |> Assumption.assume ctxt |
198 in |
205 val rp = replay_prf_trm' (Termtab.update (Thm.prop_of t_thm, t_thm) assmtab) p |
199 Thm.implies_intr (Thm.cprop_of t_thm) rp |
206 in |
200 end |
207 Thm.implies_intr (Thm.cprop_of t_thm) rp |
201 | replay_prf_trm' assmtab (Bound reified_t) = |
208 end |
202 let |
209 | replay_prf_trm' assmtab (Bound reified_t) = |
203 val t = dereify reified_t |> Logic_Sig.mk_Trueprop |
210 let |
204 in |
211 val t = dereify reified_t |> Logic_Sig.mk_Trueprop |
205 Termtab.lookup assmtab t |
212 in |
206 |> expect (fn () => raise TERM ("Assumption not found:", t::Termtab.keys assmtab)) |
213 Termtab.lookup assmtab t |
207 end |
214 |> expect (fn () => raise TERM ("Assumption not found:", t::Termtab.keys assmtab)) |
208 | replay_prf_trm' assmtab (Conv (t, cp, p)) = |
215 end |
209 let |
216 | replay_prf_trm' assmtab (Conv (t, cp, p)) = |
210 val thm = replay_prf_trm' assmtab (Bound t) |
217 let |
211 val conv = Logic_Sig.Trueprop_conv (replay_conv cp) |
218 val thm = replay_prf_trm' assmtab (Bound t) |
212 val conv_thm = Conv.fconv_rule conv thm |
219 val conv = Logic_Sig.Trueprop_conv (replay_conv cp) |
213 val conv_term = Thm.prop_of conv_thm |
220 val conv_thm = Conv.fconv_rule conv thm |
214 in |
221 val conv_term = Thm.prop_of conv_thm |
215 replay_prf_trm' (Termtab.update (conv_term, conv_thm) assmtab) p |
222 in |
216 end |
223 replay_prf_trm' (Termtab.update (conv_term, conv_thm) assmtab) p |
217 in |
224 end |
218 replay_prf_trm' assmtab p |
225 in |
219 end |
226 replay_prf_trm' assmtab p |
220 |
227 end |
221 fun replay_order_prf_trm ord_ops {thms = thms, conv_thms = conv_thms, ...} ctxt reifytab assmtab = |
228 |
222 let |
229 fun replay_order_prf_trm ord_ops {thms = thms, conv_thms = conv_thms, ...} ctxt reifytab assmtab = |
223 val thmtab = thms @ [ |
230 let |
224 ("conjE", Logic_Sig.conjE), ("conjI", Logic_Sig.conjI), ("disjE", Logic_Sig.disjE) |
231 val thmtab = thms @ [ |
225 ] |
232 ("conjE", Logic_Sig.conjE), ("conjI", Logic_Sig.conjI), ("disjE", Logic_Sig.disjE) |
226 val convs = map (apsnd list_curry0) ( |
233 ] |
227 map (apsnd Conv.rewr_conv) conv_thms @ |
234 val convs = map (apsnd list_curry0) ( |
228 [ |
235 map (apsnd Conv.rewr_conv) conv_thms @ |
229 ("not_not_conv", Logic_Sig.not_not_conv), |
236 [ |
230 ("de_Morgan_conj_conv", Logic_Sig.de_Morgan_conj_conv), |
237 ("not_not_conv", Logic_Sig.not_not_conv), |
231 ("de_Morgan_disj_conv", Logic_Sig.de_Morgan_disj_conv), |
238 ("de_Morgan_conj_conv", Logic_Sig.de_Morgan_conj_conv), |
232 ("conj_disj_distribR_conv", Logic_Sig.conj_disj_distribR_conv), |
239 ("de_Morgan_disj_conv", Logic_Sig.de_Morgan_disj_conv), |
233 ("conj_disj_distribL_conv", Logic_Sig.conj_disj_distribL_conv) |
240 ("conj_disj_distribR_conv", Logic_Sig.conj_disj_distribR_conv), |
234 ]) |
241 ("conj_disj_distribL_conv", Logic_Sig.conj_disj_distribL_conv) |
235 |
242 ]) |
236 val dereify = dereify_order_fm ord_ops reifytab |
243 |
237 in |
244 val dereify = dereify_order_fm ord_ops reifytab |
238 replay_prf_trm (replay_conv convs) dereify ctxt thmtab assmtab |
245 in |
239 end |
246 replay_prf_trm (replay_conv convs) dereify ctxt thmtab assmtab |
240 |
247 end |
241 fun strip_Not (nt $ t) = if nt = Logic_Sig.Not then t else nt $ t |
248 |
242 | strip_Not t = t |
249 fun strip_Not (nt $ t) = if nt = Logic_Sig.Not then t else nt $ t |
243 |
250 | strip_Not t = t |
244 fun limit_not_less lt ctxt decomp_prems = |
251 |
|
252 fun limit_not_less lt ctxt decomp_prems = |
|
253 let |
|
254 val trace = Config.get ctxt order_trace_cfg |
|
255 val limit = Config.get ctxt order_split_limit_cfg |
|
256 |
|
257 fun is_not_less_term t = |
|
258 case try (strip_Not o Logic_Sig.dest_Trueprop) t of |
|
259 SOME (binop $ _ $ _) => binop = lt |
|
260 | _ => false |
|
261 |
|
262 val not_less_prems = filter (is_not_less_term o Thm.prop_of o fst) decomp_prems |
|
263 val _ = if trace andalso length not_less_prems > limit |
|
264 then tracing "order split limit exceeded" |
|
265 else () |
|
266 in |
|
267 filter_out (is_not_less_term o Thm.prop_of o fst) decomp_prems @ |
|
268 take limit not_less_prems |
|
269 end |
|
270 |
|
271 fun decomp {eq, le, lt} ctxt t = |
|
272 let |
|
273 fun decomp'' (binop $ t1 $ t2) = |
|
274 let |
|
275 fun is_excluded t = exists (fn ty => ty = fastype_of t) excluded_types |
|
276 |
|
277 open Order_Procedure |
|
278 val thy = Proof_Context.theory_of ctxt |
|
279 fun try_match pat = try (Pattern.match thy (pat, binop)) (Vartab.empty, Vartab.empty) |
|
280 in if is_excluded t1 then NONE |
|
281 else case (try_match eq, try_match le, try_match lt) of |
|
282 (SOME env, _, _) => SOME ((true, EQ, (t1, t2)), env) |
|
283 | (_, SOME env, _) => SOME ((true, LEQ, (t1, t2)), env) |
|
284 | (_, _, SOME env) => SOME ((true, LESS, (t1, t2)), env) |
|
285 | _ => NONE |
|
286 end |
|
287 | decomp'' _ = NONE |
|
288 |
|
289 fun decomp' (nt $ t) = |
|
290 if nt = Logic_Sig.Not |
|
291 then decomp'' t |> Option.map (fn ((b, c, p), e) => ((not b, c, p), e)) |
|
292 else decomp'' (nt $ t) |
|
293 | decomp' t = decomp'' t |
|
294 in |
|
295 try Logic_Sig.dest_Trueprop t |> Option.mapPartial decomp' |
|
296 end |
|
297 |
|
298 fun maximal_envs envs = |
|
299 let |
|
300 fun test_opt p (SOME x) = p x |
|
301 | test_opt _ NONE = false |
|
302 |
|
303 fun leq_env (tyenv1, tenv1) (tyenv2, tenv2) = |
|
304 Vartab.forall (fn (v, ty) => |
|
305 Vartab.lookup tyenv2 v |> test_opt (fn ty2 => ty2 = ty)) tyenv1 |
|
306 andalso |
|
307 Vartab.forall (fn (v, (ty, t)) => |
|
308 Vartab.lookup tenv2 v |> test_opt (fn (ty2, t2) => ty2 = ty andalso t2 aconv t)) tenv1 |
|
309 |
|
310 fun fold_env (i, env) es = fold_index (fn (i2, env2) => fn es => |
|
311 if i = i2 then es else if leq_env env env2 then (i, i2) :: es else es) envs es |
|
312 |
|
313 val env_order = fold_index fold_env envs [] |
|
314 |
|
315 val graph = fold_index (fn (i, env) => fn g => Int_Graph.new_node (i, env) g) |
|
316 envs Int_Graph.empty |
|
317 val graph = fold Int_Graph.add_edge env_order graph |
|
318 |
|
319 val strong_conns = Int_Graph.strong_conn graph |
|
320 val maximals = |
|
321 filter (fn comp => length comp = length (Int_Graph.all_succs graph comp)) strong_conns |
|
322 in |
|
323 map (Int_Graph.all_preds graph) maximals |
|
324 end |
|
325 |
|
326 fun partition_prems octxt ctxt prems = |
|
327 let |
|
328 fun these' _ [] = [] |
|
329 | these' f (x :: xs) = case f x of NONE => these' f xs | SOME y => (x, y) :: these' f xs |
|
330 |
|
331 val (decomp_prems, envs) = |
|
332 these' (decomp (#ops octxt) ctxt o Thm.prop_of) prems |
|
333 |> map_split (fn (thm, (l, env)) => ((thm, l), env)) |
|
334 |
|
335 val env_groups = maximal_envs envs |
|
336 in |
|
337 map (fn is => (map (nth decomp_prems) is, nth envs (hd is))) env_groups |
|
338 end |
|
339 |
|
340 local |
|
341 fun pretty_term_list ctxt = |
|
342 Pretty.list "" "" o map (Syntax.pretty_term (Config.put show_types true ctxt)) |
|
343 fun pretty_type_of ctxt t = Pretty.block |
|
344 [ Pretty.str "::", Pretty.brk 1 |
|
345 , Pretty.quote (Syntax.pretty_typ ctxt (Term.fastype_of t)) ] |
|
346 in |
|
347 fun pretty_order_kind (okind : order_kind) = Pretty.str (@{make_string} okind) |
|
348 fun pretty_order_ops ctxt ({eq, le, lt} : order_ops) = |
|
349 Pretty.block [pretty_term_list ctxt [eq, le, lt], Pretty.brk 1, pretty_type_of ctxt le] |
|
350 end |
|
351 |
|
352 type insert_prems_hook = |
|
353 order_kind -> order_ops -> Proof.context -> (thm * (bool * term * (term * term))) list |
|
354 -> thm list |
|
355 |
|
356 structure Insert_Prems_Hook_Data = Generic_Data( |
|
357 type T = (binding * insert_prems_hook) list |
|
358 val empty = [] |
|
359 val merge = Library.merge ((op =) o apply2 fst) |
|
360 ) |
|
361 |
|
362 fun declare_insert_prems_hook (binding, hook) lthy = |
|
363 lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>} |
|
364 (fn phi => fn context => |
|
365 let |
|
366 val binding = Morphism.binding phi binding |
|
367 in |
|
368 context |
|
369 |> Insert_Prems_Hook_Data.map (Library.insert ((op =) o apply2 fst) (binding, hook)) |
|
370 end) |
|
371 |
|
372 val insert_prems_hook_names = Context.Proof #> Insert_Prems_Hook_Data.get #> map fst |
|
373 |
|
374 fun eval_insert_prems_hook kind order_ops ctxt decomp_prems (hookN, hook : insert_prems_hook) = |
|
375 let |
|
376 fun dereify_order_op' (EQ _) = #eq order_ops |
|
377 | dereify_order_op' (LEQ _) = #le order_ops |
|
378 | dereify_order_op' (LESS _) = #lt order_ops |
|
379 fun dereify_order_op oop = (~1, ~1) |> apply2 Int_of_integer |> oop |> dereify_order_op' |
|
380 val decomp_prems = |
|
381 decomp_prems |
|
382 |> map (apsnd (fn (b, oop, (t1, t2)) => (b, dereify_order_op oop, (t1, t2)))) |
|
383 fun unzip (acc1, acc2) [] = (rev acc1, rev acc2) |
|
384 | unzip (acc1, acc2) ((thm, NONE) :: ps) = unzip (acc1, thm :: acc2) ps |
|
385 | unzip (acc1, acc2) ((thm, SOME dp) :: ps) = unzip ((thm, dp) :: acc1, acc2) ps |
|
386 val (decomp_extra_prems, invalid_extra_prems) = |
|
387 hook kind order_ops ctxt decomp_prems |
|
388 |> map (swap o ` (decomp order_ops ctxt o Thm.prop_of)) |
|
389 |> unzip ([], []) |
|
390 |
|
391 val pretty_thm_list = Pretty.list "" "" o map (Thm.pretty_thm ctxt) |
|
392 fun pretty_trace () = |
|
393 [ ("order kind:", pretty_order_kind kind) |
|
394 , ("order operators:", pretty_order_ops ctxt order_ops) |
|
395 , ("inserted premises:", pretty_thm_list (map fst decomp_extra_prems)) |
|
396 , ("invalid premises:", pretty_thm_list invalid_extra_prems) |
|
397 ] |
|
398 |> map (fn (t, pp) => Pretty.block [Pretty.str t, Pretty.brk 1, pp]) |
|
399 |> Pretty.big_list ("insert premises hook " ^ Pretty.string_of (Binding.pretty hookN) |
|
400 ^ " called with the parameters") |
|
401 val trace = Config.get ctxt order_trace_cfg |
|
402 val _ = if trace then tracing (Pretty.string_of (pretty_trace ())) else () |
|
403 in |
|
404 map (apsnd fst) decomp_extra_prems |
|
405 end |
|
406 |
|
407 fun order_tac raw_order_proc octxt simp_prems = |
|
408 Subgoal.FOCUS (fn {prems=prems, context=ctxt, ...} => |
245 let |
409 let |
246 val trace = Config.get ctxt order_trace_cfg |
410 val trace = Config.get ctxt order_trace_cfg |
247 val limit = Config.get ctxt order_split_limit_cfg |
|
248 |
|
249 fun is_not_less_term t = |
|
250 case try (strip_Not o Logic_Sig.dest_Trueprop) t of |
|
251 SOME (binop $ _ $ _) => binop = lt |
|
252 | _ => false |
|
253 |
|
254 val not_less_prems = filter (is_not_less_term o Thm.prop_of o fst) decomp_prems |
|
255 val _ = if trace andalso length not_less_prems > limit |
|
256 then tracing "order split limit exceeded" |
|
257 else () |
|
258 in |
|
259 filter_out (is_not_less_term o Thm.prop_of o fst) decomp_prems @ |
|
260 take limit not_less_prems |
|
261 end |
|
262 |
|
263 fun decomp {eq, le, lt} ctxt t = |
|
264 let |
|
265 fun decomp'' (binop $ t1 $ t2) = |
|
266 let |
|
267 fun is_excluded t = exists (fn ty => ty = fastype_of t) excluded_types |
|
268 |
|
269 open Order_Procedure |
|
270 val thy = Proof_Context.theory_of ctxt |
|
271 fun try_match pat = try (Pattern.match thy (pat, binop)) (Vartab.empty, Vartab.empty) |
|
272 in if is_excluded t1 then NONE |
|
273 else case (try_match eq, try_match le, try_match lt) of |
|
274 (SOME env, _, _) => SOME ((true, EQ, (t1, t2)), env) |
|
275 | (_, SOME env, _) => SOME ((true, LEQ, (t1, t2)), env) |
|
276 | (_, _, SOME env) => SOME ((true, LESS, (t1, t2)), env) |
|
277 | _ => NONE |
|
278 end |
|
279 | decomp'' _ = NONE |
|
280 |
|
281 fun decomp' (nt $ t) = |
|
282 if nt = Logic_Sig.Not |
|
283 then decomp'' t |> Option.map (fn ((b, c, p), e) => ((not b, c, p), e)) |
|
284 else decomp'' (nt $ t) |
|
285 | decomp' t = decomp'' t |
|
286 in |
|
287 try Logic_Sig.dest_Trueprop t |> Option.mapPartial decomp' |
|
288 end |
|
289 |
|
290 fun maximal_envs envs = |
|
291 let |
|
292 fun test_opt p (SOME x) = p x |
|
293 | test_opt _ NONE = false |
|
294 |
|
295 fun leq_env (tyenv1, tenv1) (tyenv2, tenv2) = |
|
296 Vartab.forall (fn (v, ty) => |
|
297 Vartab.lookup tyenv2 v |> test_opt (fn ty2 => ty2 = ty)) tyenv1 |
|
298 andalso |
|
299 Vartab.forall (fn (v, (ty, t)) => |
|
300 Vartab.lookup tenv2 v |> test_opt (fn (ty2, t2) => ty2 = ty andalso t2 aconv t)) tenv1 |
|
301 |
|
302 fun fold_env (i, env) es = fold_index (fn (i2, env2) => fn es => |
|
303 if i = i2 then es else if leq_env env env2 then (i, i2) :: es else es) envs es |
|
304 |
411 |
305 val env_order = fold_index fold_env envs [] |
412 fun order_tac' ([], _) = no_tac |
306 |
413 | order_tac' (decomp_prems, env) = |
307 val graph = fold_index (fn (i, env) => fn g => Int_Graph.new_node (i, env) g) |
414 let |
308 envs Int_Graph.empty |
415 val (order_ops as {eq, le, lt}) = |
309 val graph = fold Int_Graph.add_edge env_order graph |
416 #ops octxt |> map_order_ops (Envir.eta_contract o Envir.subst_term env) |
310 |
417 |
311 val strong_conns = Int_Graph.strong_conn graph |
418 val insert_prems_hooks = Insert_Prems_Hook_Data.get (Context.Proof ctxt) |
312 val maximals = |
419 val inserted_decomp_prems = |
313 filter (fn comp => length comp = length (Int_Graph.all_succs graph comp)) strong_conns |
420 insert_prems_hooks |
314 in |
421 |> maps (eval_insert_prems_hook (#kind octxt) order_ops ctxt decomp_prems) |
315 map (Int_Graph.all_preds graph) maximals |
422 |
316 end |
423 val decomp_prems = decomp_prems @ inserted_decomp_prems |
317 |
424 val decomp_prems = |
318 fun partition_prems octxt ctxt prems = |
425 case #kind octxt of |
319 let |
426 Order => limit_not_less lt ctxt decomp_prems |
320 fun these' _ [] = [] |
427 | _ => decomp_prems |
321 | these' f (x :: xs) = case f x of NONE => these' f xs | SOME y => (x, y) :: these' f xs |
428 |
322 |
429 fun reify_prem (_, (b, ctor, (x, y))) (ps, reifytab) = |
323 val (decomp_prems, envs) = |
430 (Reifytab.get_var x ##>> Reifytab.get_var y) reifytab |
324 these' (decomp (#ops octxt) ctxt o Thm.prop_of) prems |
431 |>> (fn vp => (b, ctor (apply2 Int_of_integer vp)) :: ps) |
325 |> map_split (fn (thm, (l, env)) => ((thm, l), env)) |
432 val (reified_prems, reifytab) = fold_rev reify_prem decomp_prems ([], Reifytab.empty) |
326 |
433 |
327 val env_groups = maximal_envs envs |
434 val reified_prems_conj = foldl1 (fn (x, a) => And (x, a)) (map Atom reified_prems) |
328 in |
435 val prems_conj_thm = map fst decomp_prems |
329 map (fn is => (map (nth decomp_prems) is, nth envs (hd is))) env_groups |
436 |> foldl1 (fn (x, a) => Logic_Sig.conjI OF [x, a]) |
330 end |
437 |> Conv.fconv_rule Thm.eta_conversion |
331 |
438 val prems_conj = prems_conj_thm |> Thm.prop_of |
332 local |
439 |
333 fun pretty_term_list ctxt = |
440 val proof = raw_order_proc reified_prems_conj |
334 Pretty.list "" "" o map (Syntax.pretty_term (Config.put show_types true ctxt)) |
441 |
335 fun pretty_type_of ctxt t = Pretty.block |
442 val pretty_thm_list = Pretty.list "" "" o map (Thm.pretty_thm ctxt) |
336 [ Pretty.str "::", Pretty.brk 1 |
443 fun pretty_trace () = |
337 , Pretty.quote (Syntax.pretty_typ ctxt (Term.fastype_of t)) ] |
444 [ ("order kind:", pretty_order_kind (#kind octxt)) |
338 in |
445 , ("order operators:", pretty_order_ops ctxt order_ops) |
339 fun pretty_order_kind (okind : order_kind) = Pretty.str (@{make_string} okind) |
446 , ("premises:", pretty_thm_list prems) |
340 fun pretty_order_ops ctxt ({eq, le, lt} : order_ops) = |
447 , ("selected premises:", pretty_thm_list (map fst decomp_prems)) |
341 Pretty.block [pretty_term_list ctxt [eq, le, lt], Pretty.brk 1, pretty_type_of ctxt le] |
448 , ("reified premises:", Pretty.str (@{make_string} reified_prems)) |
342 end |
449 , ("contradiction:", Pretty.str (@{make_string} (Option.isSome proof))) |
343 |
450 ] |
344 type insert_prems_hook = |
451 |> map (fn (t, pp) => Pretty.block [Pretty.str t, Pretty.brk 1, pp]) |
345 order_kind -> order_ops -> Proof.context -> (thm * (bool * term * (term * term))) list |
452 |> Pretty.big_list "order solver called with the parameters" |
346 -> thm list |
453 val _ = if trace then tracing (Pretty.string_of (pretty_trace ())) else () |
347 |
454 |
348 structure Insert_Prems_Hook_Data = Generic_Data( |
455 val assmtab = Termtab.make [(prems_conj, prems_conj_thm)] |
349 type T = (binding * insert_prems_hook) list |
456 val replay = replay_order_prf_trm (eq, le, lt) octxt ctxt reifytab assmtab |
350 val empty = [] |
457 in |
351 val merge = Library.merge ((op =) o apply2 fst) |
458 case proof of |
352 ) |
459 NONE => no_tac |
353 |
460 | SOME p => SOLVED' (resolve_tac ctxt [replay p]) 1 |
354 fun declare_insert_prems_hook (binding, hook) lthy = |
461 end |
355 lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>} |
462 |
356 (fn phi => fn context => |
463 val prems = simp_prems @ prems |
357 let |
464 |> filter (fn p => null (Term.add_vars (Thm.prop_of p) [])) |
358 val binding = Morphism.binding phi binding |
465 |> map (Conv.fconv_rule Thm.eta_conversion) |
359 in |
466 in |
360 context |
467 partition_prems octxt ctxt prems |> map order_tac' |> FIRST |
361 |> Insert_Prems_Hook_Data.map (Library.insert ((op =) o apply2 fst) (binding, hook)) |
468 end) |
362 end) |
469 |
363 |
470 val ad_absurdum_tac = SUBGOAL (fn (A, i) => |
364 val insert_prems_hook_names = Context.Proof #> Insert_Prems_Hook_Data.get #> map fst |
471 case try (Logic_Sig.dest_Trueprop o Logic.strip_assums_concl) A of |
365 |
472 SOME (nt $ _) => |
366 fun eval_insert_prems_hook kind order_ops ctxt decomp_prems (hookN, hook : insert_prems_hook) = |
473 if nt = Logic_Sig.Not |
367 let |
474 then resolve0_tac [Logic_Sig.notI] i |
368 fun dereify_order_op' (EQ _) = #eq order_ops |
475 else resolve0_tac [Logic_Sig.ccontr] i |
369 | dereify_order_op' (LEQ _) = #le order_ops |
476 | _ => resolve0_tac [Logic_Sig.ccontr] i) |
370 | dereify_order_op' (LESS _) = #lt order_ops |
477 |
371 fun dereify_order_op oop = (~1, ~1) |> apply2 Int_of_integer |> oop |> dereify_order_op' |
478 fun tac raw_order_proc octxt simp_prems ctxt = |
372 val decomp_prems = |
479 ad_absurdum_tac THEN' order_tac raw_order_proc octxt simp_prems ctxt |
373 decomp_prems |
480 |
374 |> map (apsnd (fn (b, oop, (t1, t2)) => (b, dereify_order_op oop, (t1, t2)))) |
481 end |
375 fun unzip (acc1, acc2) [] = (rev acc1, rev acc2) |
482 |
376 | unzip (acc1, acc2) ((thm, NONE) :: ps) = unzip (acc1, thm :: acc2) ps |
483 functor Order_Tac(structure Base_Tac : BASE_ORDER_TAC) = struct |
377 | unzip (acc1, acc2) ((thm, SOME dp) :: ps) = unzip ((thm, dp) :: acc1, acc2) ps |
484 |
378 val (decomp_extra_prems, invalid_extra_prems) = |
485 open Base_Tac |
379 hook kind order_ops ctxt decomp_prems |
486 |
380 |> map (swap o ` (decomp order_ops ctxt o Thm.prop_of)) |
487 fun order_context_eq ({kind = kind1, ops = ops1, ...}, {kind = kind2, ops = ops2, ...}) = |
381 |> unzip ([], []) |
488 let |
382 |
489 fun ops_list ops = [#eq ops, #le ops, #lt ops] |
383 val pretty_thm_list = Pretty.list "" "" o map (Thm.pretty_thm ctxt) |
490 in |
384 fun pretty_trace () = |
491 kind1 = kind2 andalso eq_list (op aconv) (apply2 ops_list (ops1, ops2)) |
385 [ ("order kind:", pretty_order_kind kind) |
492 end |
386 , ("order operators:", pretty_order_ops ctxt order_ops) |
493 val order_data_eq = order_context_eq o apply2 fst |
387 , ("inserted premises:", pretty_thm_list (map fst decomp_extra_prems)) |
494 |
388 , ("invalid premises:", pretty_thm_list invalid_extra_prems) |
495 structure Data = Generic_Data( |
389 ] |
496 type T = (order_context * (order_context -> thm list -> Proof.context -> int -> tactic)) list |
390 |> map (fn (t, pp) => Pretty.block [Pretty.str t, Pretty.brk 1, pp]) |
497 val empty = [] |
391 |> Pretty.big_list ("insert premises hook " ^ Pretty.string_of (Binding.pretty hookN) |
498 fun merge data = Library.merge order_data_eq data |
392 ^ " called with the parameters") |
499 ) |
393 val trace = Config.get ctxt order_trace_cfg |
500 |
394 val _ = if trace then tracing (Pretty.string_of (pretty_trace ())) else () |
501 fun declare (octxt as {kind = kind, raw_proc = raw_proc, ...}) lthy = |
395 in |
502 lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>} |
396 map (apsnd fst) decomp_extra_prems |
503 (fn phi => fn context => |
397 end |
|
398 |
|
399 fun order_tac raw_order_proc octxt simp_prems = |
|
400 Subgoal.FOCUS (fn {prems=prems, context=ctxt, ...} => |
|
401 let |
504 let |
402 val trace = Config.get ctxt order_trace_cfg |
505 val ops = map_order_ops (Morphism.term phi) (#ops octxt) |
403 |
506 val thms = map (fn (s, thm) => (s, Morphism.thm phi thm)) (#thms octxt) |
404 fun order_tac' ([], _) = no_tac |
507 val conv_thms = map (fn (s, thm) => (s, Morphism.thm phi thm)) (#conv_thms octxt) |
405 | order_tac' (decomp_prems, env) = |
508 val octxt' = {kind = kind, ops = ops, thms = thms, conv_thms = conv_thms} |
406 let |
509 in |
407 val (order_ops as {eq, le, lt}) = |
510 context |> Data.map (Library.insert order_data_eq (octxt', raw_proc)) |
408 #ops octxt |> map_order_ops (Envir.eta_contract o Envir.subst_term env) |
511 end) |
409 |
512 |
410 val insert_prems_hooks = Insert_Prems_Hook_Data.get (Context.Proof ctxt) |
513 fun declare_order { |
411 val inserted_decomp_prems = |
514 ops = ops, |
412 insert_prems_hooks |
515 thms = { |
413 |> maps (eval_insert_prems_hook (#kind octxt) order_ops ctxt decomp_prems) |
516 trans = trans, (* x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z *) |
414 |
517 refl = refl, (* x \<le> x *) |
415 val decomp_prems = decomp_prems @ inserted_decomp_prems |
518 eqD1 = eqD1, (* x = y \<Longrightarrow> x \<le> y *) |
416 val decomp_prems = |
519 eqD2 = eqD2, (* x = y \<Longrightarrow> y \<le> x *) |
417 case #kind octxt of |
520 antisym = antisym, (* x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y *) |
418 Order => limit_not_less lt ctxt decomp_prems |
521 contr = contr (* \<not> P \<Longrightarrow> P \<Longrightarrow> R *) |
419 | _ => decomp_prems |
522 }, |
420 |
523 conv_thms = { |
421 fun reify_prem (_, (b, ctor, (x, y))) (ps, reifytab) = |
524 less_le = less_le, (* x < y \<equiv> x \<le> y \<and> x \<noteq> y *) |
422 (Reifytab.get_var x ##>> Reifytab.get_var y) reifytab |
525 nless_le = nless_le (* \<not> a < b \<equiv> \<not> a \<le> b \<or> a = b *) |
423 |>> (fn vp => (b, ctor (apply2 Int_of_integer vp)) :: ps) |
526 } |
424 val (reified_prems, reifytab) = fold_rev reify_prem decomp_prems ([], Reifytab.empty) |
527 } = |
425 |
528 declare { |
426 val reified_prems_conj = foldl1 (fn (x, a) => And (x, a)) (map Atom reified_prems) |
529 kind = Order, |
427 val prems_conj_thm = map fst decomp_prems |
530 ops = ops, |
428 |> foldl1 (fn (x, a) => Logic_Sig.conjI OF [x, a]) |
531 thms = [("trans", trans), ("refl", refl), ("eqD1", eqD1), ("eqD2", eqD2), |
429 |> Conv.fconv_rule Thm.eta_conversion |
532 ("antisym", antisym), ("contr", contr)], |
430 val prems_conj = prems_conj_thm |> Thm.prop_of |
533 conv_thms = [("less_le", less_le), ("nless_le", nless_le)], |
431 |
534 raw_proc = Base_Tac.tac Order_Procedure.po_contr_prf |
432 val proof = raw_order_proc reified_prems_conj |
535 } |
433 |
536 |
434 val pretty_thm_list = Pretty.list "" "" o map (Thm.pretty_thm ctxt) |
537 fun declare_linorder { |
435 fun pretty_trace () = |
538 ops = ops, |
436 [ ("order kind:", pretty_order_kind (#kind octxt)) |
539 thms = { |
437 , ("order operators:", pretty_order_ops ctxt order_ops) |
540 trans = trans, (* x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z *) |
438 , ("premises:", pretty_thm_list prems) |
541 refl = refl, (* x \<le> x *) |
439 , ("selected premises:", pretty_thm_list (map fst decomp_prems)) |
542 eqD1 = eqD1, (* x = y \<Longrightarrow> x \<le> y *) |
440 , ("reified premises:", Pretty.str (@{make_string} reified_prems)) |
543 eqD2 = eqD2, (* x = y \<Longrightarrow> y \<le> x *) |
441 , ("contradiction:", Pretty.str (@{make_string} (Option.isSome proof))) |
544 antisym = antisym, (* x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y *) |
442 ] |
545 contr = contr (* \<not> P \<Longrightarrow> P \<Longrightarrow> R *) |
443 |> map (fn (t, pp) => Pretty.block [Pretty.str t, Pretty.brk 1, pp]) |
546 }, |
444 |> Pretty.big_list "order solver called with the parameters" |
547 conv_thms = { |
445 val _ = if trace then tracing (Pretty.string_of (pretty_trace ())) else () |
548 less_le = less_le, (* x < y \<equiv> x \<le> y \<and> x \<noteq> y *) |
446 |
549 nless_le = nless_le, (* \<not> x < y \<equiv> y \<le> x *) |
447 val assmtab = Termtab.make [(prems_conj, prems_conj_thm)] |
550 nle_le = nle_le (* \<not> a \<le> b \<equiv> b \<le> a \<and> b \<noteq> a *) |
448 val replay = replay_order_prf_trm (eq, le, lt) octxt ctxt reifytab assmtab |
551 } |
449 in |
552 } = |
450 case proof of |
553 declare { |
451 NONE => no_tac |
554 kind = Linorder, |
452 | SOME p => SOLVED' (resolve_tac ctxt [replay p]) 1 |
555 ops = ops, |
453 end |
556 thms = [("trans", trans), ("refl", refl), ("eqD1", eqD1), ("eqD2", eqD2), |
454 |
557 ("antisym", antisym), ("contr", contr)], |
455 val prems = simp_prems @ prems |
558 conv_thms = [("less_le", less_le), ("nless_le", nless_le), ("nle_le", nle_le)], |
456 |> filter (fn p => null (Term.add_vars (Thm.prop_of p) [])) |
559 raw_proc = Base_Tac.tac Order_Procedure.lo_contr_prf |
457 |> map (Conv.fconv_rule Thm.eta_conversion) |
560 } |
458 in |
561 |
459 partition_prems octxt ctxt prems |> map order_tac' |> FIRST |
562 (* Try to solve the goal by calling the order solver with each of the declared orders. *) |
460 end) |
563 fun tac simp_prems ctxt = |
461 |
564 let fun app_tac (octxt, tac0) = CHANGED o tac0 octxt simp_prems ctxt |
462 val ad_absurdum_tac = SUBGOAL (fn (A, i) => |
565 in FIRST' (map app_tac (Data.get (Context.Proof ctxt))) end |
463 case try (Logic_Sig.dest_Trueprop o Logic.strip_assums_concl) A of |
566 |
464 SOME (nt $ _) => |
567 end |
465 if nt = Logic_Sig.Not |
|
466 then resolve0_tac [Logic_Sig.notI] i |
|
467 else resolve0_tac [Logic_Sig.ccontr] i |
|
468 | _ => resolve0_tac [Logic_Sig.ccontr] i) |
|
469 |
|
470 fun tac raw_order_proc octxt simp_prems ctxt = |
|
471 ad_absurdum_tac THEN' order_tac raw_order_proc octxt simp_prems ctxt |
|
472 |
|
473 end |
|
474 |
|
475 functor Order_Tac(structure Base_Tac : BASE_ORDER_TAC) = struct |
|
476 open Base_Tac |
|
477 |
|
478 fun order_context_eq ({kind = kind1, ops = ops1, ...}, {kind = kind2, ops = ops2, ...}) = |
|
479 let |
|
480 fun ops_list ops = [#eq ops, #le ops, #lt ops] |
|
481 in |
|
482 kind1 = kind2 andalso eq_list (op aconv) (apply2 ops_list (ops1, ops2)) |
|
483 end |
|
484 val order_data_eq = order_context_eq o apply2 fst |
|
485 |
|
486 structure Data = Generic_Data( |
|
487 type T = (order_context * (order_context -> thm list -> Proof.context -> int -> tactic)) list |
|
488 val empty = [] |
|
489 fun merge data = Library.merge order_data_eq data |
|
490 ) |
|
491 |
|
492 fun declare (octxt as {kind = kind, raw_proc = raw_proc, ...}) lthy = |
|
493 lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>} |
|
494 (fn phi => fn context => |
|
495 let |
|
496 val ops = map_order_ops (Morphism.term phi) (#ops octxt) |
|
497 val thms = map (fn (s, thm) => (s, Morphism.thm phi thm)) (#thms octxt) |
|
498 val conv_thms = map (fn (s, thm) => (s, Morphism.thm phi thm)) (#conv_thms octxt) |
|
499 val octxt' = {kind = kind, ops = ops, thms = thms, conv_thms = conv_thms} |
|
500 in |
|
501 context |> Data.map (Library.insert order_data_eq (octxt', raw_proc)) |
|
502 end) |
|
503 |
|
504 fun declare_order { |
|
505 ops = ops, |
|
506 thms = { |
|
507 trans = trans, (* x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z *) |
|
508 refl = refl, (* x \<le> x *) |
|
509 eqD1 = eqD1, (* x = y \<Longrightarrow> x \<le> y *) |
|
510 eqD2 = eqD2, (* x = y \<Longrightarrow> y \<le> x *) |
|
511 antisym = antisym, (* x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y *) |
|
512 contr = contr (* \<not> P \<Longrightarrow> P \<Longrightarrow> R *) |
|
513 }, |
|
514 conv_thms = { |
|
515 less_le = less_le, (* x < y \<equiv> x \<le> y \<and> x \<noteq> y *) |
|
516 nless_le = nless_le (* \<not> a < b \<equiv> \<not> a \<le> b \<or> a = b *) |
|
517 } |
|
518 } = |
|
519 declare { |
|
520 kind = Order, |
|
521 ops = ops, |
|
522 thms = [("trans", trans), ("refl", refl), ("eqD1", eqD1), ("eqD2", eqD2), |
|
523 ("antisym", antisym), ("contr", contr)], |
|
524 conv_thms = [("less_le", less_le), ("nless_le", nless_le)], |
|
525 raw_proc = Base_Tac.tac Order_Procedure.po_contr_prf |
|
526 } |
|
527 |
|
528 fun declare_linorder { |
|
529 ops = ops, |
|
530 thms = { |
|
531 trans = trans, (* x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z *) |
|
532 refl = refl, (* x \<le> x *) |
|
533 eqD1 = eqD1, (* x = y \<Longrightarrow> x \<le> y *) |
|
534 eqD2 = eqD2, (* x = y \<Longrightarrow> y \<le> x *) |
|
535 antisym = antisym, (* x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y *) |
|
536 contr = contr (* \<not> P \<Longrightarrow> P \<Longrightarrow> R *) |
|
537 }, |
|
538 conv_thms = { |
|
539 less_le = less_le, (* x < y \<equiv> x \<le> y \<and> x \<noteq> y *) |
|
540 nless_le = nless_le, (* \<not> x < y \<equiv> y \<le> x *) |
|
541 nle_le = nle_le (* \<not> a \<le> b \<equiv> b \<le> a \<and> b \<noteq> a *) |
|
542 } |
|
543 } = |
|
544 declare { |
|
545 kind = Linorder, |
|
546 ops = ops, |
|
547 thms = [("trans", trans), ("refl", refl), ("eqD1", eqD1), ("eqD2", eqD2), |
|
548 ("antisym", antisym), ("contr", contr)], |
|
549 conv_thms = [("less_le", less_le), ("nless_le", nless_le), ("nle_le", nle_le)], |
|
550 raw_proc = Base_Tac.tac Order_Procedure.lo_contr_prf |
|
551 } |
|
552 |
|
553 (* Try to solve the goal by calling the order solver with each of the declared orders. *) |
|
554 fun tac simp_prems ctxt = |
|
555 let fun app_tac (octxt, tac0) = CHANGED o tac0 octxt simp_prems ctxt |
|
556 in FIRST' (map app_tac (Data.get (Context.Proof ctxt))) end |
|
557 end |
|