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