1 theory Lambda |
1 theory Lambda |
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
4 |
5 |
5 lemma Abs_lst_fcb2: |
6 lemma Abs_lst1_fcb2: |
6 fixes as bs :: "atom list" |
7 fixes a b :: "'a :: at" |
7 and x y :: "'b :: fs" |
8 and S T :: "'b :: fs" |
|
9 and c::"'c::fs" |
8 and c::"'c::fs" |
10 assumes e: "(Abs_lst [atom a] T) = (Abs_lst [atom b] S)" |
9 assumes eq: "[as]lst. x = [bs]lst. y" |
11 and fcb1: "atom a \<sharp> f a T c" |
10 and fcb1: "(set as) \<sharp>* f as x c" |
12 and fcb2: "atom b \<sharp> f b S c" |
11 and fresh1: "set as \<sharp>* c" |
13 and fresh: "{atom a, atom b} \<sharp>* c" |
12 and fresh2: "set bs \<sharp>* c" |
14 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a T c) = f (p \<bullet> a) (p \<bullet> T) c" |
13 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c" |
15 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b S c) = f (p \<bullet> b) (p \<bullet> S) c" |
14 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
16 shows "f a T c = f b S c" |
15 shows "f as x c = f bs y c" |
17 proof - |
16 proof - |
18 have fin1: "finite (supp (f a T c))" |
17 have "supp (as, x, c) supports (f as x c)" |
19 apply(rule_tac S="supp (a, T, c)" in supports_finite) |
18 unfolding supports_def fresh_def[symmetric] |
20 apply(simp add: supports_def) |
19 by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh) |
21 apply(simp add: fresh_def[symmetric]) |
20 then have fin1: "finite (supp (f as x c))" |
22 apply(clarify) |
21 by (auto intro: supports_finite simp add: finite_supp) |
23 apply(subst perm1) |
22 have "supp (bs, y, c) supports (f bs y c)" |
24 apply(simp add: supp_swap fresh_star_def) |
23 unfolding supports_def fresh_def[symmetric] |
25 apply(simp add: swap_fresh_fresh fresh_Pair) |
24 by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh) |
26 apply(simp add: finite_supp) |
25 then have fin2: "finite (supp (f bs y c))" |
|
26 by (auto intro: supports_finite simp add: finite_supp) |
|
27 obtain q::"perm" where |
|
28 fr1: "(q \<bullet> (set as)) \<sharp>* (x, c, f as x c, f bs y c)" and |
|
29 fr2: "supp q \<sharp>* Abs_lst as x" and |
|
30 inc: "supp q \<subseteq> (set as) \<union> q \<bullet> (set as)" |
|
31 using at_set_avoiding3[where xs="set as" and c="(x, c, f as x c, f bs y c)" and x="[as]lst. x"] |
|
32 fin1 fin2 |
|
33 by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv) |
|
34 have "Abs_lst (q \<bullet> as) (q \<bullet> x) = q \<bullet> Abs_lst as x" by simp |
|
35 also have "\<dots> = Abs_lst as x" |
|
36 by (simp only: fr2 perm_supp_eq) |
|
37 finally have "Abs_lst (q \<bullet> as) (q \<bullet> x) = Abs_lst bs y" using eq by simp |
|
38 then obtain r::perm where |
|
39 qq1: "q \<bullet> x = r \<bullet> y" and |
|
40 qq2: "q \<bullet> as = r \<bullet> bs" and |
|
41 qq3: "supp r \<subseteq> (q \<bullet> (set as)) \<union> set bs" |
|
42 apply(drule_tac sym) |
|
43 apply(simp only: Abs_eq_iff2 alphas) |
|
44 apply(erule exE) |
|
45 apply(erule conjE)+ |
|
46 apply(drule_tac x="p" in meta_spec) |
|
47 apply(simp add: set_eqvt) |
|
48 apply(blast) |
27 done |
49 done |
28 have fin2: "finite (supp (f b S c))" |
50 have "(set as) \<sharp>* f as x c" by (rule fcb1) |
29 apply(rule_tac S="supp (b, S, c)" in supports_finite) |
51 then have "q \<bullet> ((set as) \<sharp>* f as x c)" |
30 apply(simp add: supports_def) |
52 by (simp add: permute_bool_def) |
31 apply(simp add: fresh_def[symmetric]) |
53 then have "set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c" |
32 apply(clarify) |
54 apply(simp add: fresh_star_eqvt set_eqvt) |
33 apply(subst perm2) |
55 apply(subst (asm) perm1) |
34 apply(simp add: supp_swap fresh_star_def) |
56 using inc fresh1 fr1 |
35 apply(simp add: swap_fresh_fresh fresh_Pair) |
57 apply(auto simp add: fresh_star_def fresh_Pair) |
36 apply(simp add: finite_supp) |
|
37 done |
58 done |
38 obtain d::"'a::at" where fr: "atom d \<sharp> (a, b, S, T, c, f a T c, f b S c)" |
59 then have "set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
39 using obtain_fresh'[where x="(a, b, S, T, c, f a T c, f b S c)"] |
60 then have "r \<bullet> ((set bs) \<sharp>* f bs y c)" |
40 apply(auto simp add: finite_supp supp_Pair fin1 fin2) |
61 apply(simp add: fresh_star_eqvt set_eqvt) |
|
62 apply(subst (asm) perm2[symmetric]) |
|
63 using qq3 fresh2 fr1 |
|
64 apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) |
41 done |
65 done |
42 have "(a \<leftrightarrow> d) \<bullet> (Abs_lst [atom a] T) = (b \<leftrightarrow> d) \<bullet> (Abs_lst [atom b] S)" |
66 then have fcb2: "(set bs) \<sharp>* f bs y c" by (simp add: permute_bool_def) |
43 apply(simp (no_asm_use) only: flip_def) |
67 have "f as x c = q \<bullet> (f as x c)" |
44 apply(subst swap_fresh_fresh) |
68 apply(rule perm_supp_eq[symmetric]) |
45 apply(simp add: Abs_fresh_iff) |
69 using inc fcb1 fr1 by (auto simp add: fresh_star_def) |
46 using fr |
70 also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" |
47 apply(simp add: Abs_fresh_iff) |
71 apply(rule perm1) |
48 apply(subst swap_fresh_fresh) |
72 using inc fresh1 fr1 by (auto simp add: fresh_star_def) |
49 apply(simp add: Abs_fresh_iff) |
73 also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
50 using fr |
74 also have "\<dots> = r \<bullet> (f bs y c)" |
51 apply(simp add: Abs_fresh_iff) |
75 apply(rule perm2[symmetric]) |
52 apply(rule e) |
76 using qq3 fresh2 fr1 by (auto simp add: fresh_star_def) |
53 done |
77 also have "... = f bs y c" |
54 then have "Abs_lst [atom d] ((a \<leftrightarrow> d) \<bullet> T) = Abs_lst [atom d] ((b \<leftrightarrow> d) \<bullet> S)" |
78 apply(rule perm_supp_eq) |
55 apply (simp add: swap_atom flip_def) |
79 using qq3 fr1 fcb2 by (auto simp add: fresh_star_def) |
56 done |
|
57 then have eq: "(a \<leftrightarrow> d) \<bullet> T = (b \<leftrightarrow> d) \<bullet> S" |
|
58 by (simp add: Abs1_eq_iff) |
|
59 have "f a T c = (a \<leftrightarrow> d) \<bullet> f a T c" |
|
60 unfolding flip_def |
|
61 apply(rule sym) |
|
62 apply(rule swap_fresh_fresh) |
|
63 using fcb1 |
|
64 apply(simp) |
|
65 using fr |
|
66 apply(simp add: fresh_Pair) |
|
67 done |
|
68 also have "... = f d ((a \<leftrightarrow> d) \<bullet> T) c" |
|
69 unfolding flip_def |
|
70 apply(subst perm1) |
|
71 using fresh fr |
|
72 apply(simp add: supp_swap fresh_star_def fresh_Pair) |
|
73 apply(simp) |
|
74 done |
|
75 also have "... = f d ((b \<leftrightarrow> d) \<bullet> S) c" using eq by simp |
|
76 also have "... = (b \<leftrightarrow> d) \<bullet> f b S c" |
|
77 unfolding flip_def |
|
78 apply(subst perm2) |
|
79 using fresh fr |
|
80 apply(simp add: supp_swap fresh_star_def fresh_Pair) |
|
81 apply(simp) |
|
82 done |
|
83 also have "... = f b S c" |
|
84 apply(rule flip_fresh_fresh) |
|
85 using fcb2 |
|
86 apply(simp) |
|
87 using fr |
|
88 apply(simp add: fresh_Pair) |
|
89 done |
|
90 finally show ?thesis by simp |
80 finally show ?thesis by simp |
91 qed |
81 qed |
|
82 |
|
83 lemma Abs_lst1_fcb2: |
|
84 fixes a b :: "atom" |
|
85 and x y :: "'b :: fs" |
|
86 and c::"'c :: fs" |
|
87 assumes e: "(Abs_lst [a] x) = (Abs_lst [b] y)" |
|
88 and fcb1: "a \<sharp> f a x c" |
|
89 and fresh: "{a, b} \<sharp>* c" |
|
90 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c" |
|
91 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b y c) = f (p \<bullet> b) (p \<bullet> y) c" |
|
92 shows "f a x c = f b y c" |
|
93 using e |
|
94 apply(drule_tac Abs_lst_fcb2[where c="c" and f="\<lambda>(as::atom list) . f (hd as)"]) |
|
95 apply(simp_all) |
|
96 using fcb1 fresh perm1 perm2 |
|
97 apply(simp_all add: fresh_star_def) |
|
98 done |
|
99 |
|
100 lemma Abs_lst1_fcb2': |
|
101 fixes a b :: "'a::at" |
|
102 and x y :: "'b :: fs" |
|
103 and c::"'c :: fs" |
|
104 assumes e: "(Abs_lst [atom a] x) = (Abs_lst [atom b] y)" |
|
105 and fcb1: "atom a \<sharp> f a x c" |
|
106 and fresh: "{atom a, atom b} \<sharp>* c" |
|
107 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c" |
|
108 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b y c) = f (p \<bullet> b) (p \<bullet> y) c" |
|
109 shows "f a x c = f b y c" |
|
110 using e |
|
111 apply(drule_tac Abs_lst1_fcb2[where c="c" and f="\<lambda>a . f ((inv atom) a)"]) |
|
112 using fcb1 fresh perm1 perm2 |
|
113 apply(simp_all add: fresh_star_def inv_f_f inj_on_def atom_eqvt) |
|
114 done |
92 |
115 |
93 |
116 |
94 atom_decl name |
117 atom_decl name |
95 |
118 |
96 nominal_datatype lam = |
119 nominal_datatype lam = |
659 apply blast |
677 apply blast |
660 apply (simp add: Abs1_eq_iff fresh_star_def) |
678 apply (simp add: Abs1_eq_iff fresh_star_def) |
661 apply(simp_all) |
679 apply(simp_all) |
662 apply(erule_tac c="()" in Abs_lst1_fcb2) |
680 apply(erule_tac c="()" in Abs_lst1_fcb2) |
663 apply (simp add: Abs_fresh_iff) |
681 apply (simp add: Abs_fresh_iff) |
664 apply (simp add: Abs_fresh_iff) |
|
665 apply(simp add: fresh_star_def fresh_Unit) |
682 apply(simp add: fresh_star_def fresh_Unit) |
666 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
683 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
667 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
684 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
668 apply(erule conjE) |
685 apply(erule conjE) |
669 apply(erule_tac c="t2a" in Abs_lst1_fcb2) |
686 apply(erule_tac c="t2a" in Abs_lst1_fcb2') |
670 apply (erule fresh_eqvt_at) |
687 apply (erule fresh_eqvt_at) |
671 apply (simp add: finite_supp) |
688 apply (simp add: finite_supp) |
672 apply (simp add: fresh_Inl var_fresh_subst) |
689 apply (simp add: fresh_Inl var_fresh_subst) |
673 apply (erule fresh_eqvt_at) |
690 apply(simp add: fresh_star_def) |
674 apply (simp add: finite_supp) |
|
675 apply (simp add: fresh_Inl var_fresh_subst) |
|
676 apply(simp add: fresh_star_def fresh_Unit) |
|
677 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst_eqvt) |
691 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst_eqvt) |
678 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst_eqvt) |
692 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst_eqvt) |
679 done |
693 done |
680 |
694 |
681 |
695 |