20 |
20 |
21 method_setup all_trivials = {* all_trivials *} {* solves trivial goals *} |
21 method_setup all_trivials = {* all_trivials *} {* solves trivial goals *} |
22 |
22 |
23 |
23 |
24 lemma Abs_lst1_fcb: |
24 lemma Abs_lst1_fcb: |
25 fixes x y :: "'a :: at_base" |
25 fixes x y :: "'a :: at" |
26 and S T :: "'b :: fs" |
26 and S T :: "'b :: fs" |
27 assumes e: "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)" |
27 assumes e: "[[atom x]]lst. T = [[atom y]]lst. S" |
28 and f1: "\<lbrakk>x \<noteq> y; atom y \<sharp> T; atom x \<sharp> (atom y \<rightleftharpoons> atom x) \<bullet> T\<rbrakk> \<Longrightarrow> atom x \<sharp> f x T" |
28 and f1: "\<lbrakk>x \<noteq> y; atom y \<sharp> T; atom x \<sharp> (y \<leftrightarrow> x) \<bullet> T\<rbrakk> \<Longrightarrow> atom x \<sharp> f x T" |
29 and f2: "\<lbrakk>x \<noteq> y; atom y \<sharp> T; atom x \<sharp> (atom y \<rightleftharpoons> atom x) \<bullet> T\<rbrakk> \<Longrightarrow> atom y \<sharp> f x T" |
29 and f2: "\<lbrakk>x \<noteq> y; atom y \<sharp> T; atom x \<sharp> (y \<leftrightarrow> x) \<bullet> T\<rbrakk> \<Longrightarrow> atom y \<sharp> f x T" |
30 and p: "\<lbrakk>S = (atom x \<rightleftharpoons> atom y) \<bullet> T; x \<noteq> y; atom y \<sharp> T; atom x \<sharp> S\<rbrakk> |
30 and p: "\<lbrakk>S = (x \<leftrightarrow> y) \<bullet> T; x \<noteq> y; atom y \<sharp> T; atom x \<sharp> S\<rbrakk> |
31 \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> (f x T) = f y S" |
31 \<Longrightarrow> (x \<leftrightarrow> y) \<bullet> (f x T) = f y S" |
32 and s: "sort_of (atom x) = sort_of (atom y)" |
|
33 shows "f x T = f y S" |
32 shows "f x T = f y S" |
34 using e |
33 using e |
35 apply(case_tac "atom x \<sharp> S") |
34 apply(case_tac "atom x \<sharp> S") |
36 apply(simp add: Abs1_eq_iff'[OF s s]) |
35 apply(simp add: Abs1_eq_iff') |
37 apply(elim conjE disjE) |
36 apply(elim conjE disjE) |
38 apply(simp) |
37 apply(simp) |
39 apply(rule trans) |
38 apply(rule trans) |
40 apply(rule_tac p="(atom x \<rightleftharpoons> atom y)" in supp_perm_eq[symmetric]) |
39 apply(rule_tac p="(x \<leftrightarrow> y)" in supp_perm_eq[symmetric]) |
41 apply(rule fresh_star_supp_conv) |
40 apply(rule fresh_star_supp_conv) |
42 apply(simp add: supp_swap fresh_star_def s f1 f2) |
41 apply(simp add: flip_def supp_swap fresh_star_def f1 f2) |
43 apply(simp add: swap_commute p) |
42 apply(simp add: flip_commute p) |
44 apply(simp add: Abs1_eq_iff[OF s s]) |
43 apply(simp add: Abs1_eq_iff) |
45 done |
44 done |
46 |
45 |
47 lemma Abs_lst_fcb: |
46 lemma Abs_lst_fcb: |
48 fixes xs ys :: "'a :: fs" |
47 fixes xs ys :: "'a :: fs" |
49 and S T :: "'b :: fs" |
48 and S T :: "'b :: fs" |
381 |
380 |
382 lemma Abs_lst1_fcb2: |
381 lemma Abs_lst1_fcb2: |
383 fixes a b :: "atom" |
382 fixes a b :: "atom" |
384 and x y :: "'b :: fs" |
383 and x y :: "'b :: fs" |
385 and c::"'c :: fs" |
384 and c::"'c :: fs" |
386 assumes e: "(Abs_lst [a] x) = (Abs_lst [b] y)" |
385 assumes e: "[[a]]lst. x = [[b]]lst. y" |
387 and fcb1: "a \<sharp> f a x c" |
386 and fcb1: "a \<sharp> f a x c" |
388 and fresh: "{a, b} \<sharp>* c" |
387 and fresh: "{a, b} \<sharp>* c" |
389 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c" |
388 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c" |
390 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b y c) = f (p \<bullet> b) (p \<bullet> y) c" |
389 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b y c) = f (p \<bullet> b) (p \<bullet> y) c" |
391 shows "f a x c = f b y c" |
390 shows "f a x c = f b y c" |
398 |
397 |
399 lemma Abs_lst1_fcb2': |
398 lemma Abs_lst1_fcb2': |
400 fixes a b :: "'a::at" |
399 fixes a b :: "'a::at" |
401 and x y :: "'b :: fs" |
400 and x y :: "'b :: fs" |
402 and c::"'c :: fs" |
401 and c::"'c :: fs" |
403 assumes e: "(Abs_lst [atom a] x) = (Abs_lst [atom b] y)" |
402 assumes e: "[[atom a]]lst. x = [[atom b]]lst. y" |
404 and fcb1: "atom a \<sharp> f a x c" |
403 and fcb1: "atom a \<sharp> f a x c" |
405 and fresh: "{atom a, atom b} \<sharp>* c" |
404 and fresh: "{atom a, atom b} \<sharp>* c" |
406 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c" |
405 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c" |
407 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b y c) = f (p \<bullet> b) (p \<bullet> y) c" |
406 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b y c) = f (p \<bullet> b) (p \<bullet> y) c" |
408 shows "f a x c = f b y c" |
407 shows "f a x c = f b y c" |