24 apply(simp) |
24 apply(simp) |
25 apply(simp) |
25 apply(simp) |
26 done |
26 done |
27 |
27 |
28 |
28 |
29 datatype 'a rabst = |
29 fun |
30 RAbst "atom set" "'a::pt" |
30 alpha_gen |
31 |
|
32 fun map_fun |
|
33 where "map_fun f (RAbst bs x) = RAbst bs (f x)" |
|
34 |
|
35 fun map_rel |
|
36 where "map_rel R (RAbst bs x) (RAbst cs y) = R x y" |
|
37 |
|
38 declare [[map "rabst" = (map_fun, map_rel)]] |
|
39 |
|
40 instantiation rabst :: (pt) pt |
|
41 begin |
|
42 |
|
43 primrec |
|
44 permute_rabst |
|
45 where |
31 where |
46 "p \<bullet> (RAbst bs x) = RAbst (p \<bullet> bs) (p \<bullet> x)" |
32 alpha_gen[simp del]: |
47 |
33 "(alpha_gen (bs, x) R f pi (cs, y)) \<longleftrightarrow> (f x - bs = f y - cs) \<and> ((f x - bs) \<sharp>* pi) \<and> (R (pi \<bullet> x) y)" |
48 instance |
|
49 apply(default) |
|
50 apply(case_tac [!] x) |
|
51 apply(simp_all) |
|
52 done |
|
53 |
|
54 end |
|
55 |
|
56 fun |
|
57 alpha_gen |
|
58 where |
|
59 alpha_gen[simp del]: |
|
60 "(alpha_gen (bs, x) R f pi (cs, y)) \<longleftrightarrow> (f x - bs = f y - cs) \<and> ((f x - bs) \<sharp>* pi) \<and> (R (pi \<bullet> x) y)" |
|
61 |
34 |
62 notation |
35 notation |
63 alpha_gen ("_ \<approx>gen _ _ _ _") |
36 alpha_gen ("_ \<approx>gen _ _ _ _") |
64 |
37 |
65 lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2" |
38 lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2" |
98 apply(simp add: fresh_star_permute_iff) |
71 apply(simp add: fresh_star_permute_iff) |
99 apply(clarsimp) |
72 apply(clarsimp) |
100 done |
73 done |
101 |
74 |
102 fun |
75 fun |
103 alpha_rabst :: "('a::pt) rabst \<Rightarrow> 'a rabst \<Rightarrow> bool" ("_ \<approx>raw _") |
76 alpha_abst |
104 where |
77 where |
105 "(RAbst bs x) \<approx>raw (RAbst cs y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" |
78 "alpha_abst (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" |
106 |
79 |
107 lemma alpha_reflp: |
80 notation |
108 shows "abst \<approx>raw abst" |
81 alpha_abst ("_ \<approx>abst _") |
109 apply(induct abst) |
|
110 apply(simp) |
|
111 apply(rule exI) |
|
112 apply(rule alpha_gen_refl) |
|
113 apply(simp) |
|
114 done |
|
115 |
|
116 lemma alpha_symp: |
|
117 assumes a: "abst1 \<approx>raw abst2" |
|
118 shows "abst2 \<approx>raw abst1" |
|
119 using a |
|
120 apply(induct rule: alpha_rabst.induct) |
|
121 apply(simp) |
|
122 apply(erule exE) |
|
123 apply(rule exI) |
|
124 apply(rule alpha_gen_sym) |
|
125 apply(assumption) |
|
126 apply(clarsimp) |
|
127 done |
|
128 |
|
129 lemma alpha_transp: |
|
130 assumes a1: "abst1 \<approx>raw abst2" |
|
131 and a2: "abst2 \<approx>raw abst3" |
|
132 shows "abst1 \<approx>raw abst3" |
|
133 using a1 a2 |
|
134 apply(induct rule: alpha_rabst.induct) |
|
135 apply(induct rule: alpha_rabst.induct) |
|
136 apply(simp) |
|
137 apply(erule exE)+ |
|
138 apply(rule exI) |
|
139 apply(rule alpha_gen_trans) |
|
140 apply(assumption) |
|
141 apply(assumption) |
|
142 apply(simp) |
|
143 done |
|
144 |
|
145 lemma alpha_eqvt: |
|
146 assumes a: "abst1 \<approx>raw abst2" |
|
147 shows "(p \<bullet> abst1) \<approx>raw(p \<bullet> abst2)" |
|
148 using a |
|
149 apply(induct abst1 abst2 rule: alpha_rabst.induct) |
|
150 apply(simp) |
|
151 apply(erule exE) |
|
152 apply(rule exI) |
|
153 apply(rule alpha_gen_eqvt) |
|
154 apply(assumption) |
|
155 apply(simp) |
|
156 apply(simp add: supp_eqvt) |
|
157 apply(simp add: supp_eqvt) |
|
158 done |
|
159 |
82 |
160 lemma test1: |
83 lemma test1: |
161 assumes a1: "a \<notin> (supp x) - bs" |
84 assumes a1: "a \<notin> (supp x) - bs" |
162 and a2: "b \<notin> (supp x) - bs" |
85 and a2: "b \<notin> (supp x) - bs" |
163 shows "(RAbst bs x) \<approx>raw (RAbst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))" |
86 shows "(bs, x) \<approx>abst ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)" |
164 apply(simp) |
87 apply(simp) |
165 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI) |
88 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI) |
166 apply(simp add: alpha_gen) |
89 apply(simp add: alpha_gen) |
167 apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric]) |
90 apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric]) |
168 apply(simp add: swap_set_fresh[OF a1 a2]) |
91 apply(simp add: swap_set_fresh[OF a1 a2]) |
174 done |
97 done |
175 |
98 |
176 fun |
99 fun |
177 s_test |
100 s_test |
178 where |
101 where |
179 "s_test (RAbst bs x) = (supp x) - bs" |
102 "s_test (bs, x) = (supp x) - bs" |
180 |
103 |
181 lemma s_test_lemma: |
104 lemma s_test_lemma: |
182 assumes a: "x \<approx>raw y" |
105 assumes a: "x \<approx>abst y" |
183 shows "s_test x = s_test y" |
106 shows "s_test x = s_test y" |
184 using a |
107 using a |
185 apply(induct rule: alpha_rabst.induct) |
108 apply(induct rule: alpha_abst.induct) |
186 apply(simp add: alpha_gen) |
109 apply(simp add: alpha_gen) |
187 done |
110 done |
188 |
111 |
189 |
112 quotient_type 'a abst = "(atom set \<times> 'a::pt)" / "alpha_abst" |
190 quotient_type 'a abst = "('a::pt) rabst" / "alpha_rabst::('a::pt) rabst \<Rightarrow> 'a rabst \<Rightarrow> bool" |
|
191 apply(rule equivpI) |
113 apply(rule equivpI) |
192 unfolding reflp_def symp_def transp_def |
114 unfolding reflp_def symp_def transp_def |
193 apply(auto intro: alpha_reflp alpha_symp alpha_transp) |
115 apply(simp_all) |
|
116 apply(clarify) |
|
117 apply(rule exI) |
|
118 apply(rule alpha_gen_refl) |
|
119 apply(simp) |
|
120 apply(clarify) |
|
121 apply(rule exI) |
|
122 apply(rule alpha_gen_sym) |
|
123 apply(assumption) |
|
124 apply(clarsimp) |
|
125 apply(clarify) |
|
126 apply(rule exI) |
|
127 apply(rule alpha_gen_trans) |
|
128 apply(assumption) |
|
129 apply(assumption) |
|
130 apply(simp) |
194 done |
131 done |
195 |
132 |
196 quotient_definition |
133 quotient_definition |
197 "Abst::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abst" |
134 "Abst::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abst" |
198 as |
135 as |
199 "RAbst" |
136 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" |
200 |
137 |
201 lemma [quot_respect]: |
138 lemma [quot_respect]: |
202 shows "((op =) ===> (op =) ===> alpha_rabst) RAbst RAbst" |
139 shows "((op =) ===> (op =) ===> alpha_abst) Pair Pair" |
203 apply(simp del: alpha_rabst.simps add: alpha_reflp) |
140 apply(clarsimp) |
|
141 apply(rule exI) |
|
142 apply(rule alpha_gen_refl) |
|
143 apply(simp) |
204 done |
144 done |
205 |
145 |
206 lemma [quot_respect]: |
146 lemma [quot_respect]: |
207 shows "((op =) ===> alpha_rabst ===> alpha_rabst) permute permute" |
147 shows "((op =) ===> alpha_abst ===> alpha_abst) permute permute" |
208 apply(simp add: alpha_eqvt) |
148 apply(clarsimp) |
|
149 apply(rule exI) |
|
150 apply(rule alpha_gen_eqvt) |
|
151 apply(assumption) |
|
152 apply(simp_all add: supp_eqvt) |
209 done |
153 done |
210 |
154 |
211 lemma [quot_respect]: |
155 lemma [quot_respect]: |
212 shows "(alpha_rabst ===> (op =)) s_test s_test" |
156 shows "(alpha_abst ===> (op =)) s_test s_test" |
213 apply(simp add: s_test_lemma) |
157 apply(simp add: s_test_lemma) |
214 done |
158 done |
215 |
159 |
216 lemma abst_induct: |
160 lemma abst_induct: |
217 "\<lbrakk>\<And>as (x::'a::pt). P (Abst as x)\<rbrakk> \<Longrightarrow> P t" |
161 "\<lbrakk>\<And>as (x::'a::pt). P (Abst as x)\<rbrakk> \<Longrightarrow> P t" |
218 apply(lifting rabst.induct) |
162 apply(lifting prod.induct[where 'a="atom set" and 'b="'a"]) |
219 done |
163 done |
220 |
164 |
221 instantiation abst :: (pt) pt |
165 instantiation abst :: (pt) pt |
222 begin |
166 begin |
223 |
167 |
224 quotient_definition |
168 quotient_definition |
225 "permute_abst::perm \<Rightarrow> ('a::pt abst) \<Rightarrow> 'a abst" |
169 "permute_abst::perm \<Rightarrow> ('a::pt abst) \<Rightarrow> 'a abst" |
226 as |
170 as |
227 "permute::perm \<Rightarrow> ('a::pt rabst) \<Rightarrow> 'a rabst" |
171 "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)" |
228 |
172 |
229 lemma permute_ABS [simp]: |
173 lemma permute_ABS [simp]: |
230 fixes x::"'a::pt" (* ??? has to be 'a \<dots> 'b does not work *) |
174 fixes x::"'a::pt" (* ??? has to be 'a \<dots> 'b does not work *) |
231 shows "(p \<bullet> (Abst as x)) = Abst (p \<bullet> as) (p \<bullet> x)" |
175 shows "(p \<bullet> (Abst as x)) = Abst (p \<bullet> as) (p \<bullet> x)" |
232 apply(lifting permute_rabst.simps(1)) |
176 apply(lifting permute_prod.simps(1)[where 'a="atom set" and 'b="'a"]) |
233 done |
177 done |
234 |
178 |
235 instance |
179 instance |
236 apply(default) |
180 apply(default) |
237 apply(induct_tac [!] x rule: abst_induct) |
181 apply(induct_tac [!] x rule: abst_induct) |
313 shows "((supp x) - as) \<subseteq> (supp (Abst as x))" |
258 shows "((supp x) - as) \<subseteq> (supp (Abst as x))" |
314 apply(rule subsetI) |
259 apply(rule subsetI) |
315 apply(rule contrapos_pp) |
260 apply(rule contrapos_pp) |
316 apply(assumption) |
261 apply(assumption) |
317 unfolding fresh_def[symmetric] |
262 unfolding fresh_def[symmetric] |
|
263 thm s_test_fresh_lemma |
318 apply(drule_tac s_test_fresh_lemma) |
264 apply(drule_tac s_test_fresh_lemma) |
319 apply(simp only: s_test_lifted_simp) |
265 apply(simp only: s_test_lifted_simp) |
320 apply(simp add: fresh_def) |
266 apply(simp add: fresh_def) |
321 apply(subgoal_tac "finite (supp x - as)") |
267 apply(subgoal_tac "finite (supp x - as)") |
322 apply(simp add: supp_finite_set) |
268 apply(simp add: supp_finite_set) |