43 thm trm.eq_iff |
43 thm trm.eq_iff |
44 thm trm.fv_bn_eqvt |
44 thm trm.fv_bn_eqvt |
45 thm trm.size_eqvt |
45 thm trm.size_eqvt |
46 thm trm.supp |
46 thm trm.supp |
47 thm trm.supp[simplified] |
47 thm trm.supp[simplified] |
|
48 |
|
49 lemma Abs_lst1_fcb2: |
|
50 fixes a b :: "'a :: at" |
|
51 and S T :: "'b :: fs" |
|
52 and c::"'c::fs" |
|
53 assumes e: "(Abs_lst [atom a] T) = (Abs_lst [atom b] S)" |
|
54 and fcb: "\<And>a T. atom a \<sharp> f a T c" |
|
55 and fresh: "{atom a, atom b} \<sharp>* c" |
|
56 and p1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a T c) = f (p \<bullet> a) (p \<bullet> T) c" |
|
57 and p2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b S c) = f (p \<bullet> b) (p \<bullet> S) c" |
|
58 shows "f a T c = f b S c" |
|
59 proof - |
|
60 have fin1: "finite (supp (f a T c))" |
|
61 apply(rule_tac S="supp (a, T, c)" in supports_finite) |
|
62 apply(simp add: supports_def) |
|
63 apply(simp add: fresh_def[symmetric]) |
|
64 apply(clarify) |
|
65 apply(subst p1) |
|
66 apply(simp add: supp_swap fresh_star_def) |
|
67 apply(simp add: swap_fresh_fresh fresh_Pair) |
|
68 apply(simp add: finite_supp) |
|
69 done |
|
70 have fin2: "finite (supp (f b S c))" |
|
71 apply(rule_tac S="supp (b, S, c)" in supports_finite) |
|
72 apply(simp add: supports_def) |
|
73 apply(simp add: fresh_def[symmetric]) |
|
74 apply(clarify) |
|
75 apply(subst p2) |
|
76 apply(simp add: supp_swap fresh_star_def) |
|
77 apply(simp add: swap_fresh_fresh fresh_Pair) |
|
78 apply(simp add: finite_supp) |
|
79 done |
|
80 obtain d::"'a::at" where fr: "atom d \<sharp> (a, b, S, T, c, f a T c, f b S c)" |
|
81 using obtain_fresh'[where x="(a, b, S, T, c, f a T c, f b S c)"] |
|
82 apply(auto simp add: finite_supp supp_Pair fin1 fin2) |
|
83 done |
|
84 have "(a \<leftrightarrow> d) \<bullet> (Abs_lst [atom a] T) = (b \<leftrightarrow> d) \<bullet> (Abs_lst [atom b] S)" |
|
85 apply(simp (no_asm_use) only: flip_def) |
|
86 apply(subst swap_fresh_fresh) |
|
87 apply(simp add: Abs_fresh_iff) |
|
88 using fr |
|
89 apply(simp add: Abs_fresh_iff) |
|
90 apply(subst swap_fresh_fresh) |
|
91 apply(simp add: Abs_fresh_iff) |
|
92 using fr |
|
93 apply(simp add: Abs_fresh_iff) |
|
94 apply(rule e) |
|
95 done |
|
96 then have "Abs_lst [atom d] ((a \<leftrightarrow> d) \<bullet> T) = Abs_lst [atom d] ((b \<leftrightarrow> d) \<bullet> S)" |
|
97 apply (simp add: swap_atom flip_def) |
|
98 done |
|
99 then have eq: "(a \<leftrightarrow> d) \<bullet> T = (b \<leftrightarrow> d) \<bullet> S" |
|
100 by (simp add: Abs1_eq_iff) |
|
101 have "f a T c = (a \<leftrightarrow> d) \<bullet> f a T c" |
|
102 unfolding flip_def |
|
103 apply(rule sym) |
|
104 apply(rule swap_fresh_fresh) |
|
105 using fcb[where a="a"] |
|
106 apply(simp) |
|
107 using fr |
|
108 apply(simp add: fresh_Pair) |
|
109 done |
|
110 also have "... = f d ((a \<leftrightarrow> d) \<bullet> T) c" |
|
111 unfolding flip_def |
|
112 apply(subst p1) |
|
113 using fresh fr |
|
114 apply(simp add: supp_swap fresh_star_def fresh_Pair) |
|
115 apply(simp) |
|
116 done |
|
117 also have "... = f d ((b \<leftrightarrow> d) \<bullet> S) c" using eq by simp |
|
118 also have "... = (b \<leftrightarrow> d) \<bullet> f b S c" |
|
119 unfolding flip_def |
|
120 apply(subst p2) |
|
121 using fresh fr |
|
122 apply(simp add: supp_swap fresh_star_def fresh_Pair) |
|
123 apply(simp) |
|
124 done |
|
125 also have "... = f b S c" |
|
126 apply(rule flip_fresh_fresh) |
|
127 using fcb[where a="b"] |
|
128 apply(simp) |
|
129 using fr |
|
130 apply(simp add: fresh_Pair) |
|
131 done |
|
132 finally show ?thesis by simp |
|
133 qed |
|
134 |
48 |
135 |
49 lemma swap_at_base_sort: |
136 lemma swap_at_base_sort: |
50 "sort_of (atom a) \<noteq> sort_of (atom x) \<Longrightarrow> sort_of (atom b) \<noteq> sort_of (atom x) |
137 "sort_of (atom a) \<noteq> sort_of (atom x) \<Longrightarrow> sort_of (atom b) \<noteq> sort_of (atom x) |
51 \<Longrightarrow> (atom a \<rightleftharpoons> atom b) \<bullet> x = x" |
138 \<Longrightarrow> (atom a \<rightleftharpoons> atom b) \<bullet> x = x" |
52 by (rule swap_fresh_fresh) (simp_all add: fresh_at_base(1)) |
139 by (rule swap_fresh_fresh) (simp_all add: fresh_at_base(1)) |
81 apply(metis)+ |
168 apply(metis)+ |
82 -- "compatibility" |
169 -- "compatibility" |
83 apply(simp_all) |
170 apply(simp_all) |
84 apply(rule conjI) |
171 apply(rule conjI) |
85 apply(elim conjE) |
172 apply(elim conjE) |
86 apply(erule Abs_lst1_fcb) |
173 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
87 apply(simp add: Abs_fresh_iff) |
174 apply(simp add: Abs_fresh_iff) |
88 apply(simp add: Abs_fresh_iff) |
175 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
89 apply(erule fresh_eqvt_at) |
176 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
90 apply(simp add: finite_supp) |
177 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
91 apply(simp add: fresh_Pair fresh_at_base(1)) |
178 apply(elim conjE) |
92 apply(simp add: eqvt_at_def swap_at_base_sort) |
179 apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2) |
93 apply simp |
180 apply(simp add: Abs_fresh_iff) |
94 apply(elim conjE) |
181 apply(simp add: fresh_at_base fresh_star_def fresh_Pair) |
95 apply(erule Abs_lst1_fcb) |
182 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
96 apply(simp add: Abs_fresh_iff) |
183 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
97 apply(simp add: Abs_fresh_iff) |
184 -- "old fcb" |
98 apply(erule fresh_eqvt_at) |
|
99 apply(simp add: finite_supp) |
|
100 apply(simp add: fresh_Pair fresh_at_base(1)) |
|
101 apply(simp add: fresh_Pair) |
|
102 apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh) |
|
103 apply simp |
|
104 apply(elim conjE) |
185 apply(elim conjE) |
105 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
186 apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)") |
106 apply(erule Abs_lst1_fcb) |
187 apply(erule Abs_lst1_fcb) |
107 apply(simp add: Abs_fresh_iff) |
188 apply(simp add: Abs_fresh_iff) |
108 apply(simp add: Abs_fresh_iff) |
189 apply(simp add: Abs_fresh_iff) |