|
1 theory LamEx |
|
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" |
|
3 begin |
|
4 |
|
5 datatype 'a ABS_raw = Abs_raw "atom list" "'a::pt" |
|
6 |
|
7 primrec |
|
8 Abs_raw_map |
|
9 where |
|
10 "Abs_raw_map f (Abs_raw as x) = Abs_raw as (f x)" |
|
11 |
|
12 fun |
|
13 Abs_raw_rel |
|
14 where |
|
15 "Abs_raw_rel R (Abs_raw as x) (Abs_raw bs y) = R x y" |
|
16 |
|
17 declare [[map "ABS_raw" = (Abs_raw_map, Abs_raw_rel)]] |
|
18 |
|
19 instantiation ABS_raw :: (pt) pt |
|
20 begin |
|
21 |
|
22 primrec |
|
23 permute_ABS_raw |
|
24 where |
|
25 "permute_ABS_raw p (Abs_raw as x) = Abs_raw (p \<bullet> as) (p \<bullet> x)" |
|
26 |
|
27 instance |
|
28 apply(default) |
|
29 apply(case_tac [!] x) |
|
30 apply(simp_all) |
|
31 done |
|
32 |
|
33 end |
|
34 |
|
35 inductive |
|
36 alpha_abs :: "('a::pt) ABS_raw \<Rightarrow> 'a ABS_raw \<Rightarrow> bool" |
|
37 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> |
|
39 \<Longrightarrow> alpha_abs (Abs_raw as x) (Abs_raw bs y)" |
|
40 |
|
41 |
|
42 lemma Abs_raw_eq1: |
|
43 assumes "alpha_abs (Abs_raw bs x) (Abs_raw bs y)" |
|
44 shows "x = y" |
|
45 using assms |
|
46 apply(erule_tac alpha_abs.cases) |
|
47 apply(auto) |
|
48 apply(drule sym) |
|
49 apply(simp) |
|
50 sorry |
|
51 |
|
52 |
|
53 quotient_type 'a ABS = "('a::pt) ABS_raw" / "alpha_abs::('a::pt) ABS_raw \<Rightarrow> 'a ABS_raw \<Rightarrow> bool" |
|
54 sorry |
|
55 |
|
56 quotient_definition |
|
57 "Abs::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a ABS" |
|
58 as |
|
59 "Abs_raw" |
|
60 |
|
61 lemma [quot_respect]: |
|
62 shows "((op =) ===> (op =) ===> alpha_abs) Abs_raw Abs_raw" |
|
63 apply(auto) |
|
64 apply(rule alpha_abs.intros) |
|
65 apply(rule_tac x="0" in exI) |
|
66 apply(simp add: fresh_star_def fresh_zero_perm) |
|
67 done |
|
68 |
|
69 lemma [quot_respect]: |
|
70 shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute" |
|
71 apply(auto) |
|
72 sorry |
|
73 |
|
74 lemma ABS_induct: |
|
75 "\<lbrakk>\<And>as (x::'a::pt). P (Abs as x)\<rbrakk> \<Longrightarrow> P t" |
|
76 apply(lifting ABS_raw.induct) |
|
77 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 |
|
87 instantiation ABS :: (pt) pt |
|
88 begin |
|
89 |
|
90 quotient_definition |
|
91 "permute_ABS::perm \<Rightarrow> ('a::pt ABS) \<Rightarrow> 'a ABS" |
|
92 as |
|
93 "permute::perm \<Rightarrow> ('a::pt ABS_raw) \<Rightarrow> 'a ABS_raw" |
|
94 |
|
95 lemma permute_ABS [simp]: |
|
96 fixes x::"'b::pt" (* ??? has to be 'b \<dots> 'a doe not work *) |
|
97 shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)" |
|
98 apply(lifting permute_ABS_raw.simps(1)) |
|
99 done |
|
100 |
|
101 instance |
|
102 apply(default) |
|
103 apply(induct_tac [!] x rule: ABS_induct) |
|
104 apply(simp_all) |
|
105 done |
|
106 |
|
107 end |
|
108 |
|
109 lemma Abs_supports: |
|
110 shows "(supp (as, x)) supports (Abs as x) " |
|
111 unfolding supports_def |
|
112 unfolding fresh_def[symmetric] |
|
113 apply(simp add: fresh_Pair swap_fresh_fresh) |
|
114 done |
|
115 |
|
116 instance ABS :: (fs) fs |
|
117 apply(default) |
|
118 apply(induct_tac x rule: ABS_induct) |
|
119 thm supports_finite |
|
120 apply(rule supports_finite) |
|
121 apply(rule Abs_supports) |
|
122 apply(simp add: supp_Pair finite_supp) |
|
123 done |
|
124 |
|
125 lemma Abs_fresh1: |
|
126 fixes x::"'a::fs" |
|
127 assumes a1: "a \<sharp> bs" |
|
128 and a2: "a \<sharp> x" |
|
129 shows "a \<sharp> Abs bs x" |
|
130 proof - |
|
131 obtain c where |
|
132 fr: "c \<sharp> bs" "c \<sharp> x" "c \<sharp> Abs bs x" "sort_of c = sort_of a" |
|
133 apply(rule_tac X="supp (bs, x, Abs bs x)" in obtain_atom) |
|
134 unfolding fresh_def[symmetric] |
|
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 |