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