1 theory LamEx |
1 theory LamEx |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" |
3 begin |
3 begin |
4 |
4 |
5 datatype 'a ABS_raw = Abs_raw "atom list" "'a::pt" |
5 (* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *) |
|
6 lemma in_permute_iff: |
|
7 shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X" |
|
8 apply(unfold mem_def permute_fun_def)[1] |
|
9 apply(simp add: permute_bool_def) |
|
10 done |
|
11 |
|
12 lemma fresh_star_permute_iff: |
|
13 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
|
14 apply(simp add: fresh_star_def) |
|
15 apply(auto) |
|
16 apply(drule_tac x="p \<bullet> xa" in bspec) |
|
17 apply(unfold mem_def permute_fun_def)[1] |
|
18 apply(simp add: eqvts) |
|
19 apply(simp add: fresh_permute_iff) |
|
20 apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1]) |
|
21 apply(simp) |
|
22 apply(drule_tac x="- p \<bullet> xa" in bspec) |
|
23 apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1]) |
|
24 apply(simp) |
|
25 apply(simp) |
|
26 done |
|
27 |
|
28 datatype 'a ABS_raw = Abs_raw "atom set" "'a::pt" |
6 |
29 |
7 primrec |
30 primrec |
8 Abs_raw_map |
31 Abs_raw_map |
9 where |
32 where |
10 "Abs_raw_map f (Abs_raw as x) = Abs_raw as (f x)" |
33 "Abs_raw_map f (Abs_raw as x) = Abs_raw as (f x)" |
33 end |
56 end |
34 |
57 |
35 inductive |
58 inductive |
36 alpha_abs :: "('a::pt) ABS_raw \<Rightarrow> 'a ABS_raw \<Rightarrow> bool" |
59 alpha_abs :: "('a::pt) ABS_raw \<Rightarrow> 'a ABS_raw \<Rightarrow> bool" |
37 where |
60 where |
38 "\<lbrakk>\<exists>pi. (supp x) - (set as) = (supp y) - (set bs) \<and> ((supp x) - (set as)) \<sharp>* pi \<and> pi \<bullet> x = y\<rbrakk> |
61 "\<lbrakk>\<exists>pi. (supp x) - as = (supp y) - bs \<and> ((supp x) - as) \<sharp>* pi \<and> pi \<bullet> x = y\<rbrakk> |
39 \<Longrightarrow> alpha_abs (Abs_raw as x) (Abs_raw bs y)" |
62 \<Longrightarrow> alpha_abs (Abs_raw as x) (Abs_raw bs y)" |
40 |
63 |
41 |
64 lemma alpha_reflp: |
42 lemma Abs_raw_eq1: |
65 shows "alpha_abs ab ab" |
43 assumes "alpha_abs (Abs_raw bs x) (Abs_raw bs y)" |
66 apply(induct ab) |
44 shows "x = y" |
67 apply(rule alpha_abs.intros) |
45 using assms |
68 apply(rule_tac x="0" in exI) |
|
69 apply(simp add: fresh_star_def fresh_zero_perm) |
|
70 done |
|
71 |
|
72 lemma alpha_symp: |
|
73 assumes a: "alpha_abs ab1 ab2" |
|
74 shows "alpha_abs ab2 ab1" |
|
75 using a |
46 apply(erule_tac alpha_abs.cases) |
76 apply(erule_tac alpha_abs.cases) |
47 apply(auto) |
77 apply(clarify) |
48 apply(drule sym) |
78 apply(rule alpha_abs.intros) |
49 apply(simp) |
79 apply(rule_tac x="- pi" in exI) |
50 sorry |
80 apply(auto) |
51 |
81 apply(auto simp add: fresh_star_def) |
|
82 apply(simp add: fresh_def supp_minus_perm) |
|
83 done |
|
84 |
|
85 lemma alpha_transp: |
|
86 assumes a1: "alpha_abs ab1 ab2" |
|
87 and a2: "alpha_abs ab2 ab3" |
|
88 shows "alpha_abs ab1 ab3" |
|
89 using a1 a2 |
|
90 apply(erule_tac alpha_abs.cases) |
|
91 apply(erule_tac alpha_abs.cases) |
|
92 apply(clarify) |
|
93 apply(rule alpha_abs.intros) |
|
94 apply(rule_tac x="pia + pi" in exI) |
|
95 apply(simp) |
|
96 apply(auto simp add: fresh_star_def) |
|
97 using supp_plus_perm |
|
98 apply(simp add: fresh_def) |
|
99 apply(blast) |
|
100 done |
|
101 |
|
102 lemma alpha_eqvt: |
|
103 assumes a: "alpha_abs ab1 ab2" |
|
104 shows "alpha_abs (p \<bullet> ab1) (p \<bullet> ab2)" |
|
105 using a |
|
106 apply(erule_tac alpha_abs.cases) |
|
107 apply(clarify) |
|
108 apply(simp) |
|
109 apply(rule alpha_abs.intros) |
|
110 apply(rule_tac x="p \<bullet> pi" in exI) |
|
111 apply(rule conjI) |
|
112 apply(simp add: supp_eqvt[symmetric]) |
|
113 apply(simp add: Diff_eqvt[symmetric]) |
|
114 apply(rule conjI) |
|
115 apply(simp add: supp_eqvt[symmetric]) |
|
116 apply(simp add: Diff_eqvt[symmetric]) |
|
117 apply(simp only: fresh_star_permute_iff) |
|
118 apply(simp add: permute_eqvt[symmetric]) |
|
119 done |
|
120 |
|
121 lemma test1: |
|
122 assumes a1: "a \<notin> (supp x) - bs" |
|
123 and a2: "b \<notin> (supp x) - bs" |
|
124 shows "alpha_abs (Abs_raw bs x) (Abs_raw ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))" |
|
125 apply(rule alpha_abs.intros) |
|
126 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI) |
|
127 apply(rule_tac conjI) |
|
128 apply(simp add: supp_eqvt[symmetric]) |
|
129 apply(simp add: Diff_eqvt[symmetric]) |
|
130 using a1 a2 |
|
131 apply(simp add: swap_set_fresh) |
|
132 apply(rule conjI) |
|
133 prefer 2 |
|
134 apply(simp) |
|
135 apply(simp add: fresh_star_def) |
|
136 apply(simp add: fresh_def) |
|
137 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}") |
|
138 using a1 a2 |
|
139 apply - |
|
140 apply(blast) |
|
141 apply(simp add: supp_swap) |
|
142 done |
|
143 |
|
144 fun |
|
145 s_test |
|
146 where |
|
147 "s_test (Abs_raw bs x) = (supp x) - bs" |
|
148 |
|
149 lemma s_test_lemma: |
|
150 assumes a: "alpha_abs x y" |
|
151 shows "s_test x = s_test y" |
|
152 using a |
|
153 apply(induct) |
|
154 apply(simp) |
|
155 done |
|
156 |
52 |
157 |
53 quotient_type 'a ABS = "('a::pt) ABS_raw" / "alpha_abs::('a::pt) ABS_raw \<Rightarrow> 'a ABS_raw \<Rightarrow> bool" |
158 quotient_type 'a ABS = "('a::pt) ABS_raw" / "alpha_abs::('a::pt) ABS_raw \<Rightarrow> 'a ABS_raw \<Rightarrow> bool" |
54 sorry |
159 apply(rule equivpI) |
|
160 unfolding reflp_def symp_def transp_def |
|
161 apply(auto intro: alpha_reflp alpha_symp alpha_transp) |
|
162 done |
55 |
163 |
56 quotient_definition |
164 quotient_definition |
57 "Abs::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a ABS" |
165 "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a ABS" |
58 as |
166 as |
59 "Abs_raw" |
167 "Abs_raw" |
60 |
168 |
61 lemma [quot_respect]: |
169 lemma [quot_respect]: |
62 shows "((op =) ===> (op =) ===> alpha_abs) Abs_raw Abs_raw" |
170 shows "((op =) ===> (op =) ===> alpha_abs) Abs_raw Abs_raw" |
63 apply(auto) |
171 apply(auto) |
64 apply(rule alpha_abs.intros) |
172 apply(rule alpha_reflp) |
65 apply(rule_tac x="0" in exI) |
|
66 apply(simp add: fresh_star_def fresh_zero_perm) |
|
67 done |
173 done |
68 |
174 |
69 lemma [quot_respect]: |
175 lemma [quot_respect]: |
70 shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute" |
176 shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute" |
71 apply(auto) |
177 apply(auto) |
72 sorry |
178 apply(simp add: alpha_eqvt) |
|
179 done |
|
180 |
|
181 lemma [quot_respect]: |
|
182 shows "(alpha_abs ===> (op =)) s_test s_test" |
|
183 apply(simp add: s_test_lemma) |
|
184 done |
73 |
185 |
74 lemma ABS_induct: |
186 lemma ABS_induct: |
75 "\<lbrakk>\<And>as (x::'a::pt). P (Abs as x)\<rbrakk> \<Longrightarrow> P t" |
187 "\<lbrakk>\<And>as (x::'a::pt). P (Abs as x)\<rbrakk> \<Longrightarrow> P t" |
76 apply(lifting ABS_raw.induct) |
188 apply(lifting ABS_raw.induct) |
77 done |
189 done |
78 |
|
79 lemma Abs_eq1: |
|
80 assumes "(Abs bs x) = (Abs bs y)" |
|
81 shows "x = y" |
|
82 using assms |
|
83 apply(lifting Abs_raw_eq1) |
|
84 done |
|
85 |
|
86 |
190 |
87 instantiation ABS :: (pt) pt |
191 instantiation ABS :: (pt) pt |
88 begin |
192 begin |
89 |
193 |
90 quotient_definition |
194 quotient_definition |
103 apply(induct_tac [!] x rule: ABS_induct) |
207 apply(induct_tac [!] x rule: ABS_induct) |
104 apply(simp_all) |
208 apply(simp_all) |
105 done |
209 done |
106 |
210 |
107 end |
211 end |
108 |
212 |
|
213 lemma test1_lifted: |
|
214 assumes a1: "a \<notin> (supp x) - bs" |
|
215 and a2: "b \<notin> (supp x) - bs" |
|
216 shows "(Abs bs x) = (Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))" |
|
217 using a1 a2 |
|
218 apply(lifting test1) |
|
219 done |
|
220 |
109 lemma Abs_supports: |
221 lemma Abs_supports: |
110 shows "(supp (as, x)) supports (Abs as x) " |
222 shows "((supp x) - as) supports (Abs as x) " |
111 unfolding supports_def |
223 unfolding supports_def |
|
224 apply(clarify) |
|
225 apply(simp (no_asm)) |
|
226 apply(subst test1_lifted[symmetric]) |
|
227 apply(simp_all) |
|
228 done |
|
229 |
|
230 quotient_definition |
|
231 "s_test_lifted :: ('a::pt) ABS \<Rightarrow> atom \<Rightarrow> bool" |
|
232 as |
|
233 "s_test::('a::pt) ABS_raw \<Rightarrow> atom \<Rightarrow> bool" |
|
234 |
|
235 lemma s_test_lifted_simp: |
|
236 shows "s_test_lifted (Abs bs x) = (supp x) - bs" |
|
237 apply(lifting s_test.simps(1)) |
|
238 done |
|
239 |
|
240 lemma s_test_lifted_eqvt: |
|
241 shows "(p \<bullet> (s_test_lifted ab)) = s_test_lifted (p \<bullet> ab)" |
|
242 apply(induct ab rule: ABS_induct) |
|
243 apply(simp add: s_test_lifted_simp supp_eqvt Diff_eqvt) |
|
244 done |
|
245 |
|
246 lemma fresh_f_empty_supp: |
|
247 assumes a: "\<forall>p. p \<bullet> f = f" |
|
248 shows "a \<sharp> x \<Longrightarrow> a \<sharp> (f x)" |
|
249 apply(simp add: fresh_def) |
|
250 apply(simp add: supp_def) |
|
251 apply(simp add: permute_fun_app_eq) |
|
252 apply(simp add: a) |
|
253 apply(rule finite_subset) |
|
254 prefer 2 |
|
255 apply(assumption) |
|
256 apply(auto) |
|
257 done |
|
258 |
|
259 |
|
260 lemma s_test_fresh_lemma: |
|
261 shows "(a \<sharp> Abs bs x) \<Longrightarrow> (a \<sharp> s_test_lifted (Abs bs x))" |
|
262 apply(rule fresh_f_empty_supp) |
|
263 apply(rule allI) |
|
264 apply(subst permute_fun_def) |
|
265 apply(simp add: s_test_lifted_eqvt) |
|
266 apply(simp) |
|
267 done |
|
268 |
|
269 lemma supp_finite_set: |
|
270 fixes S::"atom set" |
|
271 assumes "finite S" |
|
272 shows "supp S = S" |
|
273 apply(rule finite_supp_unique) |
|
274 apply(simp add: supports_def) |
|
275 apply(auto simp add: permute_set_eq swap_atom)[1] |
|
276 apply(metis) |
|
277 apply(rule assms) |
|
278 apply(auto simp add: permute_set_eq swap_atom)[1] |
|
279 done |
|
280 |
|
281 lemma s_test_subset: |
|
282 fixes x::"'a::fs" |
|
283 shows "((supp x) - as) \<subseteq> (supp (Abs as x))" |
|
284 apply(rule subsetI) |
|
285 apply(rule contrapos_pp) |
|
286 apply(assumption) |
112 unfolding fresh_def[symmetric] |
287 unfolding fresh_def[symmetric] |
113 apply(simp add: fresh_Pair swap_fresh_fresh) |
288 apply(drule_tac s_test_fresh_lemma) |
|
289 apply(simp only: s_test_lifted_simp) |
|
290 apply(simp add: fresh_def) |
|
291 apply(subgoal_tac "finite (supp x - as)") |
|
292 apply(simp add: supp_finite_set) |
|
293 apply(simp add: finite_supp) |
|
294 done |
|
295 |
|
296 lemma supp_Abs: |
|
297 fixes x::"'a::fs" |
|
298 shows "supp (Abs as x) = (supp x) - as" |
|
299 apply(rule subset_antisym) |
|
300 apply(rule supp_is_subset) |
|
301 apply(rule Abs_supports) |
|
302 apply(simp add: finite_supp) |
|
303 apply(rule s_test_subset) |
114 done |
304 done |
115 |
305 |
116 instance ABS :: (fs) fs |
306 instance ABS :: (fs) fs |
117 apply(default) |
307 apply(default) |
118 apply(induct_tac x rule: ABS_induct) |
308 apply(induct_tac x rule: ABS_induct) |
119 thm supports_finite |
309 apply(simp add: supp_Abs) |
120 apply(rule supports_finite) |
310 apply(simp add: finite_supp) |
121 apply(rule Abs_supports) |
311 done |
122 apply(simp add: supp_Pair finite_supp) |
312 |
123 done |
313 lemma fresh_abs1: |
124 |
|
125 lemma Abs_fresh1: |
|
126 fixes x::"'a::fs" |
314 fixes x::"'a::fs" |
127 assumes a1: "a \<sharp> bs" |
315 shows "a \<sharp> Abs bs x = (a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x))" |
128 and a2: "a \<sharp> x" |
316 apply(simp add: fresh_def) |
129 shows "a \<sharp> Abs bs x" |
317 apply(simp add: supp_Abs) |
130 proof - |
318 apply(auto) |
131 obtain c where |
319 done |
132 fr: "c \<sharp> bs" "c \<sharp> x" "c \<sharp> Abs bs x" "sort_of c = sort_of a" |
320 |
133 apply(rule_tac X="supp (bs, x, Abs bs x)" in obtain_atom) |
321 done |
134 unfolding fresh_def[symmetric] |
322 |
135 apply(auto simp add: supp_Pair finite_supp fresh_Pair fresh_atom) |
|
136 done |
|
137 have "(c \<rightleftharpoons> a) \<bullet> (Abs bs x) = Abs bs x" using a1 a2 fr(1) fr(2) |
|
138 by (simp add: swap_fresh_fresh) |
|
139 moreover from fr(3) |
|
140 have "((c \<rightleftharpoons> a) \<bullet> c) \<sharp> ((c \<rightleftharpoons> a) \<bullet>(Abs bs x))" |
|
141 by (simp only: fresh_permute_iff) |
|
142 ultimately show "a \<sharp> Abs bs x" using fr(4) |
|
143 by simp |
|
144 qed |
|
145 |
|
146 lemma Abs_fresh2: |
|
147 fixes x :: "'a::fs" |
|
148 assumes a1: "a \<sharp> Abs bs x" |
|
149 and a2: "a \<sharp> bs" |
|
150 shows "a \<sharp> x" |
|
151 proof - |
|
152 obtain c where |
|
153 fr: "c \<sharp> bs" "c \<sharp> x" "c \<sharp> Abs bs x" "sort_of c = sort_of a" |
|
154 apply(rule_tac X="supp (bs, x, Abs bs x)" in obtain_atom) |
|
155 unfolding fresh_def[symmetric] |
|
156 apply(auto simp add: supp_Pair finite_supp fresh_Pair fresh_atom) |
|
157 done |
|
158 have "Abs bs x = (c \<rightleftharpoons> a) \<bullet> (Abs bs x)" using a1 fr(3) |
|
159 by (simp only: swap_fresh_fresh) |
|
160 also have "\<dots> = Abs bs ((c \<rightleftharpoons> a) \<bullet> x)" using a2 fr(1) |
|
161 by (simp add: swap_fresh_fresh) |
|
162 ultimately have "Abs bs x = Abs bs ((c \<rightleftharpoons> a) \<bullet> x)" by simp |
|
163 then have "x = (c \<rightleftharpoons> a) \<bullet> x" by (rule Abs_eq1) |
|
164 moreover from fr(2) |
|
165 have "((c \<rightleftharpoons> a) \<bullet> c) \<sharp> ((c \<rightleftharpoons> a) \<bullet> x)" |
|
166 by (simp only: fresh_permute_iff) |
|
167 ultimately show "a \<sharp> x" using fr(4) |
|
168 by simp |
|
169 qed |
|
170 |
|
171 lemma Abs_fresh3: |
|
172 fixes x :: "'a::fs" |
|
173 assumes "a \<in> set bs" |
|
174 shows "a \<sharp> Abs bs x" |
|
175 proof - |
|
176 obtain c where |
|
177 fr: "c \<sharp> a" "c \<sharp> x" "c \<sharp> Abs bs x" "sort_of c = sort_of a" |
|
178 apply(rule_tac X="supp (a, x, Abs bs x)" in obtain_atom) |
|
179 unfolding fresh_def[symmetric] |
|
180 apply(auto simp add: supp_Pair finite_supp fresh_Pair fresh_atom) |
|
181 done |
|
182 from fr(3) have "((c \<rightleftharpoons> a) \<bullet> c) \<sharp> ((c \<rightleftharpoons> a) \<bullet> Abs bs x)" |
|
183 by (simp only: fresh_permute_iff) |
|
184 moreover |
|
185 have "((c \<rightleftharpoons> a) \<bullet> Abs bs x) = Abs bs x" using assms fr(1) fr(2) sorry |
|
186 ultimately |
|
187 show "a \<sharp> Abs bs x" using fr(4) by simp |
|
188 qed |
|
189 |
|
190 done |
|
191 |
|