266 apply (rename_tac l r lst h t hl hr) |
266 apply (rename_tac l r lst h t hl hr) |
267 apply (rule_tac x="(l, r, hl, hr, t)" and ?'a="name" in obtain_fresh) |
267 apply (rule_tac x="(l, r, hl, hr, t)" and ?'a="name" in obtain_fresh) |
268 apply simp |
268 apply simp |
269 apply simp |
269 apply simp |
270 apply simp |
270 apply simp |
|
271 (* The last subgoal would be obvious if we'd define it with a recusor |
|
272 and have eqvt for the function *) |
271 sorry |
273 sorry |
272 |
274 |
273 termination (eqvt) by lexicographic_order |
275 termination (eqvt) by lexicographic_order |
|
276 |
|
277 lemma var_eq_swapequal: "atom ab \<sharp> xs \<Longrightarrow> swapequal (Var ab) (Var ab) xs" |
|
278 apply (induct xs) |
|
279 apply simp |
|
280 apply (case_tac a) |
|
281 apply (simp add: fresh_Cons) |
|
282 apply (rule_tac x="(ab, aa, b, xs)" and ?'a="name" in obtain_fresh) |
|
283 apply (subst swapequal.simps) |
|
284 apply (simp add: fresh_Pair lam.fresh) |
|
285 apply (simp add: fresh_Pair_elim) |
|
286 by (metis flip_at_base_simps(3) fresh_Pair fresh_at_base(2)) |
|
287 |
|
288 lemma var_neq_swapequal: "atom ab \<sharp> xs \<Longrightarrow> ab \<noteq> m \<Longrightarrow> \<not> swapequal (Var ab) (Var m) xs" |
|
289 apply (induct xs arbitrary: m) |
|
290 apply simp |
|
291 apply (case_tac a) |
|
292 apply (simp add: fresh_Cons) |
|
293 apply (rule_tac x="(ab, aa, b, m, xs)" and ?'a="name" in obtain_fresh) |
|
294 apply (subst swapequal.simps) |
|
295 apply (simp add: fresh_Pair lam.fresh) |
|
296 apply auto[1] |
|
297 apply (elim conjE) |
|
298 apply (simp add: fresh_Pair_elim) |
|
299 apply (simp add: flip_at_base_simps(3) fresh_Pair fresh_at_base(2)) |
|
300 apply (subgoal_tac "ab \<noteq> (b \<leftrightarrow> aba) \<bullet> m") |
|
301 apply simp |
|
302 by (metis (lifting) permute_flip_at) |
|
303 lemma var_neq_swapequal2: "atom ab \<sharp> xs \<Longrightarrow> ab \<noteq> m \<Longrightarrow> \<not> swapequal (Var m) (Var ab) xs" |
|
304 apply (induct xs arbitrary: m) |
|
305 apply simp |
|
306 apply (case_tac a) |
|
307 apply (simp add: fresh_Cons) |
|
308 apply (rule_tac x="(ab, aa, b, m, xs)" and ?'a="name" in obtain_fresh) |
|
309 apply (subst swapequal.simps) |
|
310 apply (simp add: fresh_Pair lam.fresh) |
|
311 apply auto[1] |
|
312 apply (elim conjE) |
|
313 apply (simp add: fresh_Pair_elim) |
|
314 apply (simp add: flip_at_base_simps(3) fresh_Pair fresh_at_base(2)) |
|
315 apply (subgoal_tac "ab \<noteq> (aa \<leftrightarrow> aba) \<bullet> m") |
|
316 apply simp |
|
317 by (metis (lifting) permute_flip_at) |
|
318 |
274 |
319 |
275 lemma lookup_swapequal: "lookup n m xs = swapequal (Var n) (Var m) xs" |
320 lemma lookup_swapequal: "lookup n m xs = swapequal (Var n) (Var m) xs" |
276 apply (induct xs arbitrary: m n) |
321 apply (induct xs arbitrary: m n) |
277 apply simp |
322 apply simp |
278 apply (case_tac a) |
323 apply (case_tac a) |
280 apply (rule_tac x="(n, m, aa, b, xs)" and ?'a="name" in obtain_fresh) |
325 apply (rule_tac x="(n, m, aa, b, xs)" and ?'a="name" in obtain_fresh) |
281 apply (subst swapequal.simps) |
326 apply (subst swapequal.simps) |
282 apply (simp add: fresh_Pair lam.fresh fresh_Nil) |
327 apply (simp add: fresh_Pair lam.fresh fresh_Nil) |
283 apply (case_tac "n = aa \<and> m = b") |
328 apply (case_tac "n = aa \<and> m = b") |
284 apply simp |
329 apply simp |
285 defer |
330 apply (simp add: var_eq_swapequal fresh_Pair_elim) |
286 apply (case_tac "n = aa") |
331 apply (case_tac "n = aa") |
287 apply (simp add: fresh_Pair_elim fresh_at_base) |
332 apply (simp add: fresh_Pair_elim fresh_at_base) |
288 defer |
333 apply (simp add: var_neq_swapequal fresh_Pair_elim) |
289 apply (simp add: fresh_Pair_elim fresh_at_base flip_def) |
334 apply (simp add: fresh_Pair_elim fresh_at_base flip_def) |
290 apply (case_tac "m = b") |
335 apply (case_tac "m = b") |
291 apply simp |
336 apply simp |
292 defer |
337 apply (simp add: var_neq_swapequal2 fresh_at_base) |
293 apply simp |
338 apply simp |
294 sorry |
339 done |
295 |
340 |
296 (* |
341 lemma swapequal_reorder: " |
297 lemma lookup_property: |
|
298 assumes "distinct (map fst xs @ map snd xs)" |
|
299 shows "aux (Var n) (Var m) xs = swapequal (Var n) (Var m) xs" |
|
300 using assms |
|
301 apply (induct xs arbitrary: n m) |
|
302 apply simp |
|
303 apply simp |
|
304 apply (case_tac a) |
|
305 apply simp |
|
306 apply (rule_tac x="(n, m, aa, b, xs)" and ?'a="name" in obtain_fresh) |
|
307 apply (subst swapequal.simps) |
|
308 apply (simp add: fresh_Pair lam.fresh fresh_Cons) |
|
309 apply auto[1] |
|
310 |
|
311 apply (case_tac "n = aa \<and> m = b") |
|
312 apply simp |
|
313 proof - |
|
314 have "lookup n m xs = (fold (\<lambda>(x, y) t. if n = t then y else t) xs n = m)" |
|
315 using assms |
|
316 proof (induct xs, simp) |
|
317 fix a b xs |
|
318 assume d: "distinct (map fst xs @ map snd xs) \<Longrightarrow> |
|
319 lookup n m xs = (fold (\<lambda>(x\<Colon>name, y\<Colon>name) t\<Colon>name. if n = t then y else t) xs n = m)" |
|
320 assume "distinct (map fst (a # xs) @ map snd (a # xs))" |
|
321 then have "lookup n m xs = (fold (\<lambda>(x\<Colon>name, y\<Colon>name) t\<Colon>name. if n = t then y else t) xs n = m)" |
|
322 using d by simp |
|
323 then show "lookup n m (a # xs) = |
|
324 (fold (\<lambda>(x\<Colon>name, y\<Colon>name) t\<Colon>name. if n = t then y else t) (a # xs) n = m)" |
|
325 proof (cases a) |
|
326 case (Pair b c) |
|
327 assume "lookup n m xs = (fold (\<lambda>(x\<Colon>name, y\<Colon>name) t\<Colon>name. if n = t then y else t) xs n = m)" "a = (b, c)" |
|
328 then show "lookup n m (a # xs) = (fold (\<lambda>(x\<Colon>name, y\<Colon>name) t\<Colon>name. if n = t then y else t) (a # xs) n = m)" |
|
329 apply simp |
|
330 apply auto |
|
331 sledgehammer |
|
332 |
|
333 apply - |
|
334 apply (case_tac a) |
|
335 apply auto |
|
336 |
|
337 |
|
338 apply simp |
|
339 apply (case_tac a) |
|
340 apply simp |
|
341 apply metis |
|
342 also have "... = (Var (foldr (\<lambda>(x, y) t. if n = t then y else t) xs n) = Var m)" by simp |
|
343 also have "... = (foldr (\<lambda>(x, y) t. subst t x (Var y)) xs (Var n) = Var m)" |
|
344 apply (rule arg_cong) back |
|
345 apply (induct xs) |
|
346 apply simp |
|
347 apply (case_tac a) |
|
348 apply simp |
|
349 apply auto |
|
350 find_theorems "fold _ _ _ = fold _ _ _" |
|
351 apply (induct xs) apply simp |
|
352 apply simp |
|
353 apply (case_tac a) |
|
354 apply simp |
|
355 apply (simp only: lookup.simps) |
|
356 apply simp |
|
357 apply clarify |
|
358 apply (case_tac "n = aa") |
|
359 apply (case_tac "m = ba") |
|
360 apply simp |
|
361 apply (induct_tac xs) |
|
362 apply simp |
|
363 apply simp |
|
364 sorry*) |
|
365 |
|
366 lemma reord: " |
|
367 a \<noteq> x \<Longrightarrow> a \<noteq> y \<Longrightarrow> b \<noteq> x \<Longrightarrow> b \<noteq> y \<Longrightarrow> |
342 a \<noteq> x \<Longrightarrow> a \<noteq> y \<Longrightarrow> b \<noteq> x \<Longrightarrow> b \<noteq> y \<Longrightarrow> |
368 swapequal t s ((x, y) # (a, b) # xs) = swapequal t s ((a, b) # (x, y) # xs)" |
343 swapequal t s ((x, y) # (a, b) # xs) = swapequal t s ((a, b) # (x, y) # xs)" |
369 sorry |
344 sorry |
370 |
345 |
371 lemma need: |
346 lemma swapequal_lambda: |
372 assumes "distinct xs \<and> atom x \<sharp> xs \<and> atom y \<sharp> xs" |
347 assumes "distinct xs \<and> atom x \<sharp> xs \<and> atom y \<sharp> xs" |
373 shows "swapequal (Lam [x]. t) (Lam [y]. s) xs = swapequal t s ((x, y) # xs)" |
348 shows "swapequal (Lam [x]. t) (Lam [y]. s) xs = swapequal t s ((x, y) # xs)" |
374 using assms |
349 using assms |
375 apply (induct xs arbitrary: t s x y) |
350 apply (induct xs arbitrary: t s x y) |
376 apply (rule_tac x="(x, y, t, s)" and ?'a="name" in obtain_fresh) |
351 apply (rule_tac x="(x, y, t, s)" and ?'a="name" in obtain_fresh) |
389 apply (auto simp add: Abs1_eq_iff flip_def fresh_at_base)[1] |
364 apply (auto simp add: Abs1_eq_iff flip_def fresh_at_base)[1] |
390 apply (smt atom_eqvt eq_eqvt flip_at_simps(2) flip_def fresh_eqvt) |
365 apply (smt atom_eqvt eq_eqvt flip_at_simps(2) flip_def fresh_eqvt) |
391 apply clarify |
366 apply clarify |
392 apply (simp add: fresh_Cons fresh_Pair fresh_at_base) |
367 apply (simp add: fresh_Cons fresh_Pair fresh_at_base) |
393 apply clarify |
368 apply clarify |
394 apply (subst reord) |
369 apply (subst swapequal_reorder) |
395 apply auto[4] |
370 apply auto[4] |
396 apply (rule_tac x="(x, y, t, s, a, b, xs)" and ?'a="name" in obtain_fresh) |
371 apply (rule_tac x="(x, y, t, s, a, b, xs)" and ?'a="name" in obtain_fresh) |
397 apply (rename_tac f) |
372 apply (rename_tac f) |
398 apply (subst (2) swapequal.simps) |
373 apply (subst (2) swapequal.simps) |
399 apply (simp add: lam.fresh fresh_Pair fresh_at_base fresh_Cons) |
374 apply (simp add: lam.fresh fresh_Pair fresh_at_base fresh_Cons) |