author | Norbert Schirmer <nschirmer@apple.com> |
Thu, 15 Jul 2021 08:09:10 +0200 | |
changeset 74587 | ebb0b15c66e1 |
parent 74282 | c2ee8d993d6a |
child 74588 | 3cc363e8bfb2 |
permissions | -rw-r--r-- |
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29064
diff
changeset
|
1 |
(* Title: HOL/Statespace/distinct_tree_prover.ML |
25171 | 2 |
Author: Norbert Schirmer, TU Muenchen |
3 |
*) |
|
4 |
||
25408 | 5 |
signature DISTINCT_TREE_PROVER = |
6 |
sig |
|
45355 | 7 |
datatype direction = Left | Right |
29302 | 8 |
val mk_tree : ('a -> term) -> typ -> 'a list -> term |
9 |
val dest_tree : term -> term list |
|
45355 | 10 |
val find_tree : term -> term -> direction list option |
25408 | 11 |
|
74587 | 12 |
val in_set: Proof.context -> direction list -> cterm -> thm |
13 |
val find_in_set: Proof.context -> term -> cterm -> thm |
|
29302 | 14 |
val neq_to_eq_False : thm |
60327 | 15 |
val distinctTreeProver : Proof.context -> thm -> direction list -> direction list -> thm |
45355 | 16 |
val neq_x_y : Proof.context -> term -> term -> string -> thm option |
29302 | 17 |
val distinctFieldSolver : string list -> solver |
42368
3b8498ac2314
proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
wenzelm
parents:
42361
diff
changeset
|
18 |
val distinctTree_tac : string list -> Proof.context -> int -> tactic |
60327 | 19 |
val distinct_implProver : Proof.context -> thm -> cterm -> thm |
20 |
val subtractProver : Proof.context -> term -> cterm -> thm -> thm |
|
29302 | 21 |
val distinct_simproc : string list -> simproc |
45355 | 22 |
|
60639 | 23 |
val discharge : Proof.context -> thm list -> thm -> thm |
25408 | 24 |
end; |
25 |
||
26 |
structure DistinctTreeProver : DISTINCT_TREE_PROVER = |
|
25171 | 27 |
struct |
39159 | 28 |
|
45356 | 29 |
val neq_to_eq_False = @{thm neq_to_eq_False}; |
25171 | 30 |
|
45355 | 31 |
datatype direction = Left | Right; |
25408 | 32 |
|
69597 | 33 |
fun treeT T = Type (\<^type_name>\<open>tree\<close>, [T]); |
45740 | 34 |
|
69597 | 35 |
fun mk_tree' e T n [] = Const (\<^const_name>\<open>Tip\<close>, treeT T) |
25171 | 36 |
| mk_tree' e T n xs = |
37 |
let |
|
38 |
val m = (n - 1) div 2; |
|
39 |
val (xsl,x::xsr) = chop m xs; |
|
40 |
val l = mk_tree' e T m xsl; |
|
41 |
val r = mk_tree' e T (n-(m+1)) xsr; |
|
45355 | 42 |
in |
69597 | 43 |
Const (\<^const_name>\<open>Node\<close>, treeT T --> T --> HOLogic.boolT--> treeT T --> treeT T) $ |
44 |
l $ e x $ \<^term>\<open>False\<close> $ r |
|
25171 | 45 |
end |
46 |
||
45355 | 47 |
fun mk_tree e T xs = mk_tree' e T (length xs) xs; |
25171 | 48 |
|
69597 | 49 |
fun dest_tree (Const (\<^const_name>\<open>Tip\<close>, _)) = [] |
50 |
| dest_tree (Const (\<^const_name>\<open>Node\<close>, _) $ l $ e $ _ $ r) = dest_tree l @ e :: dest_tree r |
|
45355 | 51 |
| dest_tree t = raise TERM ("dest_tree", [t]); |
25171 | 52 |
|
25408 | 53 |
|
25171 | 54 |
|
69597 | 55 |
fun lin_find_tree e (Const (\<^const_name>\<open>Tip\<close>, _)) = NONE |
56 |
| lin_find_tree e (Const (\<^const_name>\<open>Node\<close>, _) $ l $ x $ _ $ r) = |
|
45355 | 57 |
if e aconv x |
25171 | 58 |
then SOME [] |
45355 | 59 |
else |
60 |
(case lin_find_tree e l of |
|
61 |
SOME path => SOME (Left :: path) |
|
62 |
| NONE => |
|
63 |
(case lin_find_tree e r of |
|
64 |
SOME path => SOME (Right :: path) |
|
65 |
| NONE => NONE)) |
|
66 |
| lin_find_tree e t = raise TERM ("find_tree: input not a tree", [t]) |
|
25171 | 67 |
|
69597 | 68 |
fun bin_find_tree order e (Const (\<^const_name>\<open>Tip\<close>, _)) = NONE |
69 |
| bin_find_tree order e (Const (\<^const_name>\<open>Node\<close>, _) $ l $ x $ _ $ r) = |
|
45355 | 70 |
(case order (e, x) of |
71 |
EQUAL => SOME [] |
|
72 |
| LESS => Option.map (cons Left) (bin_find_tree order e l) |
|
73 |
| GREATER => Option.map (cons Right) (bin_find_tree order e r)) |
|
74 |
| bin_find_tree order e t = raise TERM ("find_tree: input not a tree", [t]) |
|
25171 | 75 |
|
76 |
fun find_tree e t = |
|
35408 | 77 |
(case bin_find_tree Term_Ord.fast_term_ord e t of |
45355 | 78 |
NONE => lin_find_tree e t |
79 |
| x => x); |
|
80 |
||
25171 | 81 |
|
45355 | 82 |
fun split_common_prefix xs [] = ([], xs, []) |
83 |
| split_common_prefix [] ys = ([], [], ys) |
|
84 |
| split_common_prefix (xs as (x :: xs')) (ys as (y :: ys')) = |
|
85 |
if x = y |
|
86 |
then let val (ps, xs'', ys'') = split_common_prefix xs' ys' in (x :: ps, xs'', ys'') end |
|
87 |
else ([], xs, ys) |
|
25171 | 88 |
|
89 |
||
90 |
(* Wrapper around Thm.instantiate. The type instiations of instTs are applied to |
|
91 |
* the right hand sides of insts |
|
92 |
*) |
|
60327 | 93 |
fun instantiate ctxt instTs insts = |
25171 | 94 |
let |
59582 | 95 |
val instTs' = map (fn (T, U) => (dest_TVar (Thm.typ_of T), Thm.typ_of U)) instTs; |
25171 | 96 |
fun substT x = (case AList.lookup (op =) instTs' x of NONE => TVar x | SOME T' => T'); |
97 |
fun mapT_and_recertify ct = |
|
60327 | 98 |
(Thm.cterm_of ctxt (Term.map_types (Term.map_type_tvar substT) (Thm.term_of ct))); |
25171 | 99 |
val insts' = map (apfst mapT_and_recertify) insts; |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60639
diff
changeset
|
100 |
in |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60639
diff
changeset
|
101 |
Thm.instantiate |
74282 | 102 |
(TVars.make (map (apfst (dest_TVar o Thm.typ_of)) instTs), |
103 |
Vars.make (map (apfst (dest_Var o Thm.term_of)) insts')) |
|
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60639
diff
changeset
|
104 |
end; |
25171 | 105 |
|
51701
1e29891759c4
tuned exceptions -- avoid composing error messages in low-level situations;
wenzelm
parents:
45740
diff
changeset
|
106 |
fun tvar_clash ixn S S' = |
1e29891759c4
tuned exceptions -- avoid composing error messages in low-level situations;
wenzelm
parents:
45740
diff
changeset
|
107 |
raise TYPE ("Type variable has two distinct sorts", [TVar (ixn, S), TVar (ixn, S')], []); |
25171 | 108 |
|
109 |
fun lookup (tye, (ixn, S)) = |
|
110 |
(case AList.lookup (op =) tye ixn of |
|
111 |
NONE => NONE |
|
112 |
| SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S'); |
|
113 |
||
114 |
val naive_typ_match = |
|
115 |
let |
|
116 |
fun match (TVar (v, S), T) subs = |
|
117 |
(case lookup (subs, (v, S)) of |
|
118 |
NONE => ((v, (S, T))::subs) |
|
119 |
| SOME _ => subs) |
|
120 |
| match (Type (a, Ts), Type (b, Us)) subs = |
|
121 |
if a <> b then raise Type.TYPE_MATCH |
|
122 |
else matches (Ts, Us) subs |
|
123 |
| match (TFree x, TFree y) subs = |
|
124 |
if x = y then subs else raise Type.TYPE_MATCH |
|
125 |
| match _ _ = raise Type.TYPE_MATCH |
|
126 |
and matches (T :: Ts, U :: Us) subs = matches (Ts, Us) (match (T, U) subs) |
|
127 |
| matches _ subs = subs; |
|
128 |
in match end; |
|
129 |
||
130 |
||
45355 | 131 |
(* expects that relevant type variables are already contained in |
25171 | 132 |
* term variables. First instantiation of variables is returned without further |
133 |
* checking. |
|
134 |
*) |
|
45355 | 135 |
fun naive_cterm_first_order_match (t, ct) env = |
25171 | 136 |
let |
45355 | 137 |
fun mtch (env as (tyinsts, insts)) = |
138 |
fn (Var (ixn, T), ct) => |
|
139 |
(case AList.lookup (op =) insts ixn of |
|
59586 | 140 |
NONE => (naive_typ_match (T, Thm.typ_of_cterm ct) tyinsts, (ixn, ct) :: insts) |
45355 | 141 |
| SOME _ => env) |
142 |
| (f $ t, ct) => |
|
143 |
let val (cf, ct') = Thm.dest_comb ct; |
|
144 |
in mtch (mtch env (f, cf)) (t, ct') end |
|
145 |
| _ => env; |
|
146 |
in mtch env (t, ct) end; |
|
25171 | 147 |
|
148 |
||
60639 | 149 |
fun discharge ctxt prems rule = |
25171 | 150 |
let |
45355 | 151 |
val (tyinsts,insts) = |
59582 | 152 |
fold naive_cterm_first_order_match (Thm.prems_of rule ~~ map Thm.cprop_of prems) ([], []); |
45355 | 153 |
val tyinsts' = |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60639
diff
changeset
|
154 |
map (fn (v, (S, U)) => ((v, S), Thm.ctyp_of ctxt U)) tyinsts; |
45355 | 155 |
val insts' = |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60639
diff
changeset
|
156 |
map (fn (idxn, ct) => ((idxn, Thm.typ_of_cterm ct), ct)) insts; |
74282 | 157 |
val rule' = Thm.instantiate (TVars.make tyinsts', Vars.make insts') rule; |
45355 | 158 |
in fold Thm.elim_implies prems rule' end; |
25171 | 159 |
|
160 |
local |
|
161 |
||
45355 | 162 |
val (l_in_set_root, x_in_set_root, r_in_set_root) = |
163 |
let |
|
164 |
val (Node_l_x_d, r) = |
|
59582 | 165 |
Thm.cprop_of @{thm in_set_root} |
45355 | 166 |
|> Thm.dest_comb |> #2 |
167 |
|> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb; |
|
168 |
val (Node_l, x) = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb; |
|
169 |
val l = Node_l |> Thm.dest_comb |> #2; |
|
170 |
in (l,x,r) end; |
|
25171 | 171 |
|
45355 | 172 |
val (x_in_set_left, r_in_set_left) = |
173 |
let |
|
174 |
val (Node_l_x_d, r) = |
|
59582 | 175 |
Thm.cprop_of @{thm in_set_left} |
45355 | 176 |
|> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |
177 |
|> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb; |
|
178 |
val x = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #2; |
|
179 |
in (x, r) end; |
|
180 |
||
181 |
val (x_in_set_right, l_in_set_right) = |
|
182 |
let |
|
183 |
val (Node_l, x) = |
|
59582 | 184 |
Thm.cprop_of @{thm in_set_right} |
45355 | 185 |
|> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |
186 |
|> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |
|
187 |
|> Thm.dest_comb |> #1 |> Thm.dest_comb |> #1 |
|
188 |
|> Thm.dest_comb; |
|
189 |
val l = Node_l |> Thm.dest_comb |> #2; |
|
190 |
in (x, l) end; |
|
25171 | 191 |
|
192 |
in |
|
74587 | 193 |
|
194 |
fun in_set ctxt ps tree = |
|
195 |
let |
|
196 |
val in_set = in_set ctxt |
|
197 |
val (_, [l, x, _, r]) = Drule.strip_comb tree; |
|
198 |
val xT = Thm.ctyp_of_cterm x; |
|
199 |
in |
|
200 |
(case ps of |
|
201 |
[] => |
|
202 |
instantiate ctxt |
|
203 |
[(Thm.ctyp_of_cterm x_in_set_root, xT)] |
|
204 |
[(l_in_set_root, l), (x_in_set_root, x), (r_in_set_root, r)] @{thm in_set_root} |
|
205 |
| Left :: ps' => |
|
206 |
let |
|
207 |
val in_set_l = in_set ps' l; |
|
208 |
val in_set_left' = |
|
209 |
instantiate ctxt |
|
210 |
[(Thm.ctyp_of_cterm x_in_set_left, xT)] |
|
211 |
[(x_in_set_left, x), (r_in_set_left, r)] @{thm in_set_left}; |
|
212 |
in discharge ctxt [in_set_l] in_set_left' end |
|
213 |
| Right :: ps' => |
|
214 |
let |
|
215 |
val in_set_r = in_set ps' r; |
|
216 |
val in_set_right' = |
|
217 |
instantiate ctxt |
|
218 |
[(Thm.ctyp_of_cterm x_in_set_right, xT)] |
|
219 |
[(x_in_set_right, x), (l_in_set_right, l)] @{thm in_set_right}; |
|
220 |
in discharge ctxt [in_set_r] in_set_right' end) |
|
221 |
end; |
|
222 |
||
223 |
fun find_in_set ctxt t ct = |
|
224 |
case find_tree t (Thm.term_of ct) of |
|
225 |
SOME ps => in_set ctxt ps ct |
|
226 |
| NONE => raise TERM ("find_in_set", [t, Thm.term_of ct]) |
|
227 |
||
25171 | 228 |
(* |
229 |
1. First get paths x_path y_path of x and y in the tree. |
|
230 |
2. For the common prefix descend into the tree according to the path |
|
231 |
and lemmas all_distinct_left/right |
|
232 |
3. If one restpath is empty use distinct_left/right, |
|
233 |
otherwise all_distinct_left_right |
|
234 |
*) |
|
235 |
||
60327 | 236 |
fun distinctTreeProver ctxt dist_thm x_path y_path = |
25171 | 237 |
let |
238 |
fun dist_subtree [] thm = thm |
|
45355 | 239 |
| dist_subtree (p :: ps) thm = |
240 |
let |
|
45356 | 241 |
val rule = |
242 |
(case p of Left => @{thm all_distinct_left} | Right => @{thm all_distinct_right}) |
|
60639 | 243 |
in dist_subtree ps (discharge ctxt [thm] rule) end; |
25171 | 244 |
|
45355 | 245 |
val (ps, x_rest, y_rest) = split_common_prefix x_path y_path; |
25171 | 246 |
val dist_subtree_thm = dist_subtree ps dist_thm; |
59582 | 247 |
val subtree = Thm.cprop_of dist_subtree_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; |
45355 | 248 |
val (_, [l, _, _, r]) = Drule.strip_comb subtree; |
249 |
||
74587 | 250 |
val in_set = in_set ctxt |
45355 | 251 |
fun in_set' [] = raise TERM ("distinctTreeProver", []) |
252 |
| in_set' (Left :: ps) = in_set ps l |
|
253 |
| in_set' (Right :: ps) = in_set ps r; |
|
254 |
||
60639 | 255 |
fun distinct_lr node_in_set Left = |
256 |
discharge ctxt [dist_subtree_thm, node_in_set] @{thm distinct_left} |
|
257 |
| distinct_lr node_in_set Right = |
|
258 |
discharge ctxt [dist_subtree_thm, node_in_set] @{thm distinct_right} |
|
25171 | 259 |
|
45355 | 260 |
val (swap, neq) = |
261 |
(case x_rest of |
|
262 |
[] => |
|
263 |
let val y_in_set = in_set' y_rest; |
|
264 |
in (false, distinct_lr y_in_set (hd y_rest)) end |
|
265 |
| xr :: xrs => |
|
266 |
(case y_rest of |
|
267 |
[] => |
|
268 |
let val x_in_set = in_set' x_rest; |
|
269 |
in (true, distinct_lr x_in_set (hd x_rest)) end |
|
270 |
| yr :: yrs => |
|
271 |
let |
|
272 |
val x_in_set = in_set' x_rest; |
|
273 |
val y_in_set = in_set' y_rest; |
|
274 |
in |
|
275 |
(case xr of |
|
45356 | 276 |
Left => |
60639 | 277 |
(false, |
278 |
discharge ctxt [dist_subtree_thm, x_in_set, y_in_set] @{thm distinct_left_right}) |
|
45356 | 279 |
| Right => |
60639 | 280 |
(true, |
281 |
discharge ctxt [dist_subtree_thm, y_in_set, x_in_set] @{thm distinct_left_right})) |
|
45355 | 282 |
end)); |
60639 | 283 |
in if swap then discharge ctxt [neq] @{thm swap_neq} else neq end; |
25171 | 284 |
|
285 |
||
60639 | 286 |
fun deleteProver _ dist_thm [] = @{thm delete_root} OF [dist_thm] |
287 |
| deleteProver ctxt dist_thm (p::ps) = |
|
45355 | 288 |
let |
45356 | 289 |
val dist_rule = |
290 |
(case p of Left => @{thm all_distinct_left} | Right => @{thm all_distinct_right}); |
|
60639 | 291 |
val dist_thm' = discharge ctxt [dist_thm] dist_rule; |
45356 | 292 |
val del_rule = (case p of Left => @{thm delete_left} | Right => @{thm delete_right}); |
60639 | 293 |
val del = deleteProver ctxt dist_thm' ps; |
294 |
in discharge ctxt [dist_thm, del] del_rule end; |
|
25171 | 295 |
|
296 |
local |
|
45355 | 297 |
val (alpha, v) = |
25171 | 298 |
let |
45355 | 299 |
val ct = |
45356 | 300 |
@{thm subtract_Tip} |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |
45355 | 301 |
|> Thm.dest_comb |> #2; |
59586 | 302 |
val [alpha] = ct |> Thm.ctyp_of_cterm |> Thm.dest_ctyp; |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60639
diff
changeset
|
303 |
in (dest_TVar (Thm.typ_of alpha), #1 (dest_Var (Thm.term_of ct))) end; |
25171 | 304 |
in |
305 |
||
69597 | 306 |
fun subtractProver ctxt (Const (\<^const_name>\<open>Tip\<close>, T)) ct dist_thm = |
45355 | 307 |
let |
308 |
val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; |
|
309 |
val [alphaI] = #2 (dest_Type T); |
|
310 |
in |
|
311 |
Thm.instantiate |
|
74282 | 312 |
(TVars.make [(alpha, Thm.ctyp_of ctxt alphaI)], |
313 |
Vars.make [((v, treeT alphaI), ct')]) @{thm subtract_Tip} |
|
45355 | 314 |
end |
69597 | 315 |
| subtractProver ctxt (Const (\<^const_name>\<open>Node\<close>, nT) $ l $ x $ d $ r) ct dist_thm = |
45355 | 316 |
let |
317 |
val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; |
|
318 |
val (_, [cl, _, _, cr]) = Drule.strip_comb ct; |
|
59582 | 319 |
val ps = the (find_tree x (Thm.term_of ct')); |
60639 | 320 |
val del_tree = deleteProver ctxt dist_thm ps; |
321 |
val dist_thm' = discharge ctxt [del_tree, dist_thm] @{thm delete_Some_all_distinct}; |
|
60327 | 322 |
val sub_l = subtractProver ctxt (Thm.term_of cl) cl (dist_thm'); |
45355 | 323 |
val sub_r = |
60327 | 324 |
subtractProver ctxt (Thm.term_of cr) cr |
60639 | 325 |
(discharge ctxt [sub_l, dist_thm'] @{thm subtract_Some_all_distinct_res}); |
326 |
in discharge ctxt [del_tree, sub_l, sub_r] @{thm subtract_Node} end; |
|
45355 | 327 |
|
328 |
end; |
|
329 |
||
60327 | 330 |
fun distinct_implProver ctxt dist_thm ct = |
25171 | 331 |
let |
332 |
val ctree = ct |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; |
|
60327 | 333 |
val sub = subtractProver ctxt (Thm.term_of ctree) ctree dist_thm; |
45356 | 334 |
in @{thm subtract_Some_all_distinct} OF [sub, dist_thm] end; |
25171 | 335 |
|
336 |
fun get_fst_success f [] = NONE |
|
45355 | 337 |
| get_fst_success f (x :: xs) = |
338 |
(case f x of |
|
339 |
NONE => get_fst_success f xs |
|
340 |
| SOME v => SOME v); |
|
25171 | 341 |
|
342 |
fun neq_x_y ctxt x y name = |
|
343 |
(let |
|
42361 | 344 |
val dist_thm = the (try (Proof_Context.get_thm ctxt) name); |
59582 | 345 |
val ctree = Thm.cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; |
346 |
val tree = Thm.term_of ctree; |
|
25171 | 347 |
val x_path = the (find_tree x tree); |
348 |
val y_path = the (find_tree y tree); |
|
60327 | 349 |
val thm = distinctTreeProver ctxt dist_thm x_path y_path; |
45355 | 350 |
in SOME thm |
351 |
end handle Option.Option => NONE); |
|
25171 | 352 |
|
42368
3b8498ac2314
proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
wenzelm
parents:
42361
diff
changeset
|
353 |
fun distinctTree_tac names ctxt = SUBGOAL (fn (goal, i) => |
3b8498ac2314
proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
wenzelm
parents:
42361
diff
changeset
|
354 |
(case goal of |
69597 | 355 |
Const (\<^const_name>\<open>Trueprop\<close>, _) $ |
356 |
(Const (\<^const_name>\<open>Not\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ x $ y)) => |
|
42368
3b8498ac2314
proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
wenzelm
parents:
42361
diff
changeset
|
357 |
(case get_fst_success (neq_x_y ctxt x y) names of |
60754 | 358 |
SOME neq => resolve_tac ctxt [neq] i |
42368
3b8498ac2314
proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
wenzelm
parents:
42361
diff
changeset
|
359 |
| NONE => no_tac) |
3b8498ac2314
proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
wenzelm
parents:
42361
diff
changeset
|
360 |
| _ => no_tac)) |
25171 | 361 |
|
45355 | 362 |
fun distinctFieldSolver names = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51701
diff
changeset
|
363 |
mk_solver "distinctFieldSolver" (distinctTree_tac names); |
25171 | 364 |
|
365 |
fun distinct_simproc names = |
|
69597 | 366 |
Simplifier.make_simproc \<^context> "DistinctTreeProver.distinct_simproc" |
367 |
{lhss = [\<^term>\<open>x = y\<close>], |
|
61144 | 368 |
proc = fn _ => fn ctxt => fn ct => |
369 |
(case Thm.term_of ct of |
|
69597 | 370 |
Const (\<^const_name>\<open>HOL.eq\<close>, _) $ x $ y => |
45356 | 371 |
Option.map (fn neq => @{thm neq_to_eq_False} OF [neq]) |
45355 | 372 |
(get_fst_success (neq_x_y ctxt x y) names) |
62913 | 373 |
| _ => NONE)}; |
25171 | 374 |
|
45355 | 375 |
end; |
376 |
||
62391 | 377 |
end; |