1 theory Abs |
1 theory Abs |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product" |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product" |
3 begin |
3 begin |
|
4 |
|
5 lemma permute_boolI: |
|
6 fixes P::"bool" |
|
7 shows "p \<bullet> P \<Longrightarrow> P" |
|
8 apply(simp add: permute_bool_def) |
|
9 done |
|
10 |
|
11 lemma permute_boolE: |
|
12 fixes P::"bool" |
|
13 shows "P \<Longrightarrow> p \<bullet> P" |
|
14 apply(simp add: permute_bool_def) |
|
15 done |
4 |
16 |
5 fun |
17 fun |
6 alpha_gen |
18 alpha_gen |
7 where |
19 where |
8 alpha_gen[simp del]: |
20 alpha_gen[simp del]: |
9 "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" |
21 "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow> |
|
22 f x - bs = f y - cs \<and> |
|
23 (f x - bs) \<sharp>* pi \<and> |
|
24 R (pi \<bullet> x) y \<and> |
|
25 pi \<bullet> bs = cs" |
10 |
26 |
11 notation |
27 notation |
12 alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100) |
28 alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100) |
13 |
29 |
14 lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2" |
30 lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2" |
21 |
37 |
22 lemma alpha_gen_sym: |
38 lemma alpha_gen_sym: |
23 assumes a: "(bs, x) \<approx>gen R f p (cs, y)" |
39 assumes a: "(bs, x) \<approx>gen R f p (cs, y)" |
24 and b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x" |
40 and b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x" |
25 shows "(cs, y) \<approx>gen R f (- p) (bs, x)" |
41 shows "(cs, y) \<approx>gen R f (- p) (bs, x)" |
26 using a b by (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm) |
42 using a b |
|
43 apply (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm) |
|
44 apply(clarify) |
|
45 apply(simp) |
|
46 done |
27 |
47 |
28 lemma alpha_gen_trans: |
48 lemma alpha_gen_trans: |
29 assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)" |
49 assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)" |
30 and b: "(cs, y) \<approx>gen R f p2 (ds, z)" |
50 and b: "(cs, y) \<approx>gen R f p2 (ds, z)" |
31 and c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z" |
51 and c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z" |
74 apply(simp add: alpha_gen.simps) |
96 apply(simp add: alpha_gen.simps) |
75 apply(erule conjE)+ |
97 apply(erule conjE)+ |
76 apply(simp add: fresh_star_plus) |
98 apply(simp add: fresh_star_plus) |
77 apply(drule_tac x="- pia \<bullet> sa" in spec) |
99 apply(drule_tac x="- pia \<bullet> sa" in spec) |
78 apply(drule mp) |
100 apply(drule mp) |
79 apply(rotate_tac 4) |
101 apply(rotate_tac 5) |
80 apply(drule_tac pi="- pia" in a) |
102 apply(drule_tac pi="- pia" in a) |
81 apply(simp) |
103 apply(simp) |
82 apply(rotate_tac 6) |
104 apply(rotate_tac 7) |
83 apply(drule_tac pi="pia" in a) |
105 apply(drule_tac pi="pia" in a) |
84 apply(simp) |
106 apply(simp) |
85 done |
107 done |
86 |
108 |
87 lemma alpha_gen_compose_eqvt: |
109 lemma alpha_gen_compose_eqvt: |
100 apply(rule conjI) |
122 apply(rule conjI) |
101 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
123 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
102 apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric]) |
124 apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric]) |
103 apply(subst permute_eqvt[symmetric]) |
125 apply(subst permute_eqvt[symmetric]) |
104 apply(simp) |
126 apply(simp) |
105 done |
127 sorry |
106 |
128 |
107 fun |
129 fun |
108 alpha_abs |
130 alpha_abs |
109 where |
131 where |
110 "alpha_abs (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" |
132 "alpha_abs (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" |
111 |
133 |
112 notation |
134 notation |
113 alpha_abs ("_ \<approx>abs _") |
135 alpha_abs ("_ \<approx>abs _") |
|
136 |
|
137 |
114 |
138 |
115 lemma alpha_abs_swap: |
139 lemma alpha_abs_swap: |
116 assumes a1: "a \<notin> (supp x) - bs" |
140 assumes a1: "a \<notin> (supp x) - bs" |
117 and a2: "b \<notin> (supp x) - bs" |
141 and a2: "b \<notin> (supp x) - bs" |
118 shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)" |
142 shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)" |
344 "alpha2 (a, x) (b, y) \<longleftrightarrow> (\<exists>c. c \<sharp> (a,b,x,y) \<and> ((c \<rightleftharpoons> a) \<bullet> x) = ((c \<rightleftharpoons> b) \<bullet> y))" |
368 "alpha2 (a, x) (b, y) \<longleftrightarrow> (\<exists>c. c \<sharp> (a,b,x,y) \<and> ((c \<rightleftharpoons> a) \<bullet> x) = ((c \<rightleftharpoons> b) \<bullet> y))" |
345 |
369 |
346 notation |
370 notation |
347 alpha2 ("_ \<approx>abs2 _") |
371 alpha2 ("_ \<approx>abs2 _") |
348 |
372 |
349 lemma qq: |
|
350 fixes S::"atom set" |
|
351 assumes a: "supp p \<inter> S = {}" |
|
352 shows "p \<bullet> S = S" |
|
353 using a |
|
354 apply(simp add: supp_perm permute_set_eq) |
|
355 apply(auto) |
|
356 apply(simp only: disjoint_iff_not_equal) |
|
357 apply(simp) |
|
358 apply (metis permute_atom_def_raw) |
|
359 apply(rule_tac x="(- p) \<bullet> x" in exI) |
|
360 apply(simp) |
|
361 apply(simp only: disjoint_iff_not_equal) |
|
362 apply(simp) |
|
363 apply(metis permute_minus_cancel) |
|
364 done |
|
365 |
|
366 lemma alpha_old_new: |
373 lemma alpha_old_new: |
367 assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b" |
374 assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b" |
368 shows "({a}, x) \<approx>abs ({b}, y)" |
375 shows "({a}, x) \<approx>abs ({b}, y)" |
369 using a |
376 using a |
370 apply(simp) |
377 apply(simp) |
383 apply(subst swap_set_not_in) |
390 apply(subst swap_set_not_in) |
384 back |
391 back |
385 apply(simp) |
392 apply(simp) |
386 apply(simp) |
393 apply(simp) |
387 apply(simp add: permute_set_eq) |
394 apply(simp add: permute_set_eq) |
|
395 apply(rule conjI) |
388 apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1]) |
396 apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1]) |
389 apply(simp add: permute_self) |
397 apply(simp add: permute_self) |
390 apply(simp add: Diff_eqvt supp_eqvt) |
398 apply(simp add: Diff_eqvt supp_eqvt) |
391 apply(simp add: permute_set_eq) |
399 apply(simp add: permute_set_eq) |
392 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}") |
400 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}") |
393 apply(simp add: fresh_star_def fresh_def) |
401 apply(simp add: fresh_star_def fresh_def) |
394 apply(blast) |
402 apply(blast) |
395 apply(simp add: supp_swap) |
403 apply(simp add: supp_swap) |
|
404 apply(simp add: eqvts) |
396 done |
405 done |
397 |
406 |
398 lemma perm_zero: |
407 lemma perm_zero: |
399 assumes a: "\<forall>x::atom. p \<bullet> x = x" |
408 assumes a: "\<forall>x::atom. p \<bullet> x = x" |
400 shows "p = 0" |
409 shows "p = 0" |
530 apply(simp add: supp_perm) |
539 apply(simp add: supp_perm) |
531 apply(drule perm_zero) |
540 apply(drule perm_zero) |
532 apply(simp add: zero) |
541 apply(simp add: zero) |
533 apply(rotate_tac 3) |
542 apply(rotate_tac 3) |
534 oops |
543 oops |
535 lemma tt: |
544 |
536 "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x" |
545 lemma ii: |
537 oops |
546 assumes "\<forall>x \<in> A. p \<bullet> x = x" |
|
547 shows "p \<bullet> A = A" |
|
548 using assms |
|
549 apply(auto) |
|
550 apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_bound inf_Int_eq mem_def mem_permute_iff) |
|
551 apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_apply eqvt_bound eqvt_lambda inf_Int_eq mem_def mem_permute_iff permute_minus_cancel(2) permute_pure) |
|
552 done |
|
553 |
|
554 |
|
555 |
|
556 lemma alpha_abs_Pair: |
|
557 shows "(bs, (x1, x2)) \<approx>gen (\<lambda>(x1,x2) (y1,y2). x1=y1 \<and> x2=y2) (\<lambda>(x,y). supp x \<union> supp y) p (cs, (y1, y2)) |
|
558 \<longleftrightarrow> ((bs, x1) \<approx>gen (op=) supp p (cs, y1) \<and> (bs, x2) \<approx>gen (op=) supp p (cs, y2))" |
|
559 apply(simp add: alpha_gen) |
|
560 apply(simp add: fresh_star_def) |
|
561 apply(simp add: ball_Un Un_Diff) |
|
562 apply(rule iffI) |
|
563 apply(simp) |
|
564 defer |
|
565 apply(simp) |
|
566 apply(rule conjI) |
|
567 apply(clarify) |
|
568 apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric]) |
|
569 apply(rule sym) |
|
570 apply(rule ii) |
|
571 apply(simp add: fresh_def supp_perm) |
|
572 apply(clarify) |
|
573 apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric]) |
|
574 apply(simp add: fresh_def supp_perm) |
|
575 apply(rule sym) |
|
576 apply(rule ii) |
|
577 apply(simp) |
|
578 done |
|
579 |
538 |
580 |
539 lemma yy: |
581 lemma yy: |
540 assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2" |
582 assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2" |
541 shows "S1 = S2" |
583 shows "S1 = S2" |
542 using assms |
584 using assms |
543 apply (metis insert_Diff_single insert_absorb) |
585 apply (metis insert_Diff_single insert_absorb) |
544 done |
|
545 |
|
546 lemma permute_boolI: |
|
547 fixes P::"bool" |
|
548 shows "p \<bullet> P \<Longrightarrow> P" |
|
549 apply(simp add: permute_bool_def) |
|
550 done |
|
551 |
|
552 lemma permute_boolE: |
|
553 fixes P::"bool" |
|
554 shows "P \<Longrightarrow> p \<bullet> P" |
|
555 apply(simp add: permute_bool_def) |
|
556 done |
586 done |
557 |
587 |
558 lemma kk: |
588 lemma kk: |
559 assumes a: "p \<bullet> x = y" |
589 assumes a: "p \<bullet> x = y" |
560 shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y" |
590 shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y" |