1 theory Foo1 |
1 theory Foo1 |
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
4 |
5 (* |
5 text {* |
6 Contrived example that has more than one |
6 Contrived example that has more than one |
7 binding function for a datatype |
7 binding function |
8 *) |
8 *} |
9 |
9 |
10 atom_decl name |
10 atom_decl name |
11 |
11 |
12 nominal_datatype foo: trm = |
12 nominal_datatype foo: trm = |
13 Var "name" |
13 Var "name" |
14 | App "trm" "trm" |
14 | App "trm" "trm" |
15 | Lam x::"name" t::"trm" bind x in t |
15 | Lam x::"name" t::"trm" bind x in t |
16 | Let1 a::"assg" t::"trm" bind "bn1 a" in t |
16 | Let1 a::"assg" t::"trm" bind "bn1 a" in t |
17 | Let2 a::"assg" t::"trm" bind "bn2 a" in t |
17 | Let2 a::"assg" t::"trm" bind "bn2 a" in t |
18 | Let3 a::"assg" t::"trm" bind "bn3 a" in t |
18 | Let3 a::"assg" t::"trm" bind "bn3 a" in t |
|
19 | Let4 a::"assg'" t::"trm" bind (set) "bn4 a" in t |
19 and assg = |
20 and assg = |
20 As "name" "name" "trm" |
21 As "name" "name" "trm" |
|
22 and assg' = |
|
23 BNil |
|
24 | BAs "name" "assg'" |
21 binder |
25 binder |
22 bn1::"assg \<Rightarrow> atom list" and |
26 bn1::"assg \<Rightarrow> atom list" and |
23 bn2::"assg \<Rightarrow> atom list" and |
27 bn2::"assg \<Rightarrow> atom list" and |
24 bn3::"assg \<Rightarrow> atom list" |
28 bn3::"assg \<Rightarrow> atom list" and |
|
29 bn4::"assg' \<Rightarrow> atom set" |
25 where |
30 where |
26 "bn1 (As x y t) = [atom x]" |
31 "bn1 (As x y t) = [atom x]" |
27 | "bn2 (As x y t) = [atom y]" |
32 | "bn2 (As x y t) = [atom y]" |
28 | "bn3 (As x y t) = [atom x, atom y]" |
33 | "bn3 (As x y t) = [atom x, atom y]" |
|
34 | "bn4 (BNil) = {}" |
|
35 | "bn4 (BAs a as) = {atom a} \<union> bn4 as" |
|
36 |
29 |
37 |
30 thm foo.distinct |
38 thm foo.distinct |
31 thm foo.induct |
39 thm foo.induct |
32 thm foo.inducts |
40 thm foo.inducts |
33 thm foo.exhaust |
41 thm foo.exhaust |
40 thm foo.supports |
48 thm foo.supports |
41 thm foo.fsupp |
49 thm foo.fsupp |
42 thm foo.supp |
50 thm foo.supp |
43 thm foo.fresh |
51 thm foo.fresh |
44 |
52 |
45 |
|
46 lemmas permute_bn1 = permute_bn1_raw.simps[quot_lifted] |
|
47 lemmas permute_bn2 = permute_bn2_raw.simps[quot_lifted] |
|
48 lemmas permute_bn3 = permute_bn3_raw.simps[quot_lifted] |
|
49 |
|
50 lemma uu1: |
53 lemma uu1: |
51 shows "alpha_bn1 as (permute_bn1 p as)" |
54 shows "alpha_bn1 as (permute_bn1 p as)" |
52 apply(induct as rule: foo.inducts(2)) |
55 apply(induct as rule: foo.inducts(2)) |
53 apply(auto)[6] |
56 apply(auto)[7] |
54 apply(simp add: permute_bn1) |
57 apply(simp add: foo.perm_bn_simps) |
55 apply(simp add: foo.eq_iff) |
58 apply(simp add: foo.eq_iff) |
|
59 apply(auto) |
56 done |
60 done |
57 |
61 |
58 lemma uu2: |
62 lemma uu2: |
59 shows "alpha_bn2 as (permute_bn2 p as)" |
63 shows "alpha_bn2 as (permute_bn2 p as)" |
60 apply(induct as rule: foo.inducts(2)) |
64 apply(induct as rule: foo.inducts(2)) |
61 apply(auto)[6] |
65 apply(auto)[7] |
62 apply(simp add: permute_bn2) |
66 apply(simp add: foo.perm_bn_simps) |
63 apply(simp add: foo.eq_iff) |
67 apply(simp add: foo.eq_iff) |
|
68 apply(auto) |
64 done |
69 done |
65 |
70 |
66 lemma uu3: |
71 lemma uu3: |
67 shows "alpha_bn3 as (permute_bn3 p as)" |
72 shows "alpha_bn3 as (permute_bn3 p as)" |
68 apply(induct as rule: foo.inducts(2)) |
73 apply(induct as rule: foo.inducts(2)) |
69 apply(auto)[6] |
74 apply(auto)[7] |
70 apply(simp add: permute_bn3) |
75 apply(simp add: foo.perm_bn_simps) |
71 apply(simp add: foo.eq_iff) |
76 apply(simp add: foo.eq_iff) |
72 done |
77 apply(auto) |
|
78 done |
|
79 |
|
80 lemma uu4: |
|
81 shows "alpha_bn4 as (permute_bn4 p as)" |
|
82 apply(induct as rule: foo.inducts(3)) |
|
83 apply(auto)[8] |
|
84 apply(simp add: foo.perm_bn_simps) |
|
85 apply(simp add: foo.eq_iff) |
|
86 apply(simp add: foo.perm_bn_simps) |
|
87 apply(simp add: foo.eq_iff) |
|
88 done |
|
89 |
73 |
90 |
74 lemma tt1: |
91 lemma tt1: |
75 shows "(p \<bullet> bn1 as) = bn1 (permute_bn1 p as)" |
92 shows "(p \<bullet> bn1 as) = bn1 (permute_bn1 p as)" |
76 apply(induct as rule: foo.inducts(2)) |
93 apply(induct as rule: foo.inducts(2)) |
77 apply(auto)[6] |
94 apply(auto)[7] |
78 apply(simp add: permute_bn1 foo.bn_defs) |
95 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
79 apply(simp add: atom_eqvt) |
96 apply(simp add: atom_eqvt) |
|
97 apply(auto) |
80 done |
98 done |
81 |
99 |
82 lemma tt2: |
100 lemma tt2: |
83 shows "(p \<bullet> bn2 as) = bn2 (permute_bn2 p as)" |
101 shows "(p \<bullet> bn2 as) = bn2 (permute_bn2 p as)" |
84 apply(induct as rule: foo.inducts(2)) |
102 apply(induct as rule: foo.inducts(2)) |
85 apply(auto)[6] |
103 apply(auto)[7] |
86 apply(simp add: permute_bn2 foo.bn_defs) |
104 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
87 apply(simp add: atom_eqvt) |
105 apply(simp add: atom_eqvt) |
|
106 apply(auto) |
88 done |
107 done |
89 |
108 |
90 lemma tt3: |
109 lemma tt3: |
91 shows "(p \<bullet> bn3 as) = bn3 (permute_bn3 p as)" |
110 shows "(p \<bullet> bn3 as) = bn3 (permute_bn3 p as)" |
92 apply(induct as rule: foo.inducts(2)) |
111 apply(induct as rule: foo.inducts(2)) |
93 apply(auto)[6] |
112 apply(auto)[7] |
94 apply(simp add: permute_bn3 foo.bn_defs) |
113 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
95 apply(simp add: atom_eqvt) |
114 apply(simp add: atom_eqvt) |
|
115 apply(auto) |
|
116 done |
|
117 |
|
118 lemma tt4: |
|
119 shows "(p \<bullet> bn4 as) = bn4 (permute_bn4 p as)" |
|
120 apply(induct as rule: foo.inducts(3)) |
|
121 apply(auto)[8] |
|
122 apply(simp add: foo.perm_bn_simps foo.bn_defs permute_set_eq) |
|
123 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
|
124 apply(simp add: atom_eqvt insert_eqvt) |
|
125 done |
|
126 |
|
127 lemma bn_finite: |
|
128 shows "(\<lambda>x. True) t" |
|
129 and "finite (set (bn1 as)) \<and> finite (set (bn2 as)) \<and> finite (set (bn3 as))" |
|
130 and "finite (bn4 as')" |
|
131 apply(induct "t::trm" and as and as' rule: foo.inducts) |
|
132 apply(simp_all add: foo.bn_defs) |
96 done |
133 done |
97 |
134 |
98 |
135 |
99 lemma strong_exhaust1: |
136 lemma strong_exhaust1: |
100 fixes c::"'a::fs" |
137 fixes c::"'a::fs" |
102 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
139 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
103 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
140 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
104 and "\<And>assn trm. \<lbrakk>set (bn1 assn) \<sharp>* c; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P" |
141 and "\<And>assn trm. \<lbrakk>set (bn1 assn) \<sharp>* c; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P" |
105 and "\<And>assn trm. \<lbrakk>set (bn2 assn) \<sharp>* c; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P" |
142 and "\<And>assn trm. \<lbrakk>set (bn2 assn) \<sharp>* c; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P" |
106 and "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P" |
143 and "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P" |
|
144 and "\<And>assn' trm. \<lbrakk>(bn4 assn') \<sharp>* c; y = Let4 assn' trm\<rbrakk> \<Longrightarrow> P" |
107 shows "P" |
145 shows "P" |
108 apply(rule_tac y="y" in foo.exhaust(1)) |
146 apply(rule_tac y="y" in foo.exhaust(1)) |
109 apply(rule assms(1)) |
147 apply(rule assms(1)) |
110 apply(assumption) |
148 apply(assumption) |
111 apply(rule assms(2)) |
149 apply(rule assms(2)) |
163 apply(drule supp_perm_eq[symmetric]) |
201 apply(drule supp_perm_eq[symmetric]) |
164 apply(simp) |
202 apply(simp) |
165 apply(simp add: tt3 uu3) |
203 apply(simp add: tt3 uu3) |
166 apply(rule at_set_avoiding2) |
204 apply(rule at_set_avoiding2) |
167 apply(simp add: finite_supp) |
205 apply(simp add: finite_supp) |
|
206 apply(simp add: finite_supp) |
|
207 apply(simp add: finite_supp) |
|
208 apply(simp add: Abs_fresh_star) |
|
209 apply(subgoal_tac "\<exists>q. (q \<bullet> (bn4 assg')) \<sharp>* c \<and> supp ([bn4 assg']set.trm) \<sharp>* q") |
|
210 apply(erule exE) |
|
211 apply(erule conjE) |
|
212 apply(rule assms(7)) |
|
213 apply(simp add: tt4) |
|
214 apply(simp add: foo.eq_iff) |
|
215 apply(drule supp_perm_eq[symmetric]) |
|
216 apply(simp) |
|
217 apply(simp add: tt4 uu4) |
|
218 apply(rule at_set_avoiding2) |
|
219 apply(simp add: bn_finite) |
168 apply(simp add: finite_supp) |
220 apply(simp add: finite_supp) |
169 apply(simp add: finite_supp) |
221 apply(simp add: finite_supp) |
170 apply(simp add: Abs_fresh_star) |
222 apply(simp add: Abs_fresh_star) |
171 done |
223 done |
172 |
224 |
176 apply(rule_tac y="as" in foo.exhaust(2)) |
228 apply(rule_tac y="as" in foo.exhaust(2)) |
177 apply(rule assms(1)) |
229 apply(rule assms(1)) |
178 apply(assumption) |
230 apply(assumption) |
179 done |
231 done |
180 |
232 |
|
233 lemma strong_exhaust3: |
|
234 assumes "as' = BNil \<Longrightarrow> P" |
|
235 and "\<And>a as. as' = BAs a as \<Longrightarrow> P" |
|
236 shows "P" |
|
237 apply(rule_tac y="as'" in foo.exhaust(3)) |
|
238 apply(rule assms(1)) |
|
239 apply(assumption) |
|
240 apply(rule assms(2)) |
|
241 apply(assumption) |
|
242 done |
181 |
243 |
182 lemma |
244 lemma |
183 fixes t::trm |
245 fixes t::trm |
184 and as::assg |
246 and as::assg |
|
247 and as'::assg' |
185 and c::"'a::fs" |
248 and c::"'a::fs" |
186 assumes a1: "\<And>x c. P1 c (Var x)" |
249 assumes a1: "\<And>x c. P1 c (Var x)" |
187 and a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)" |
250 and a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)" |
188 and a3: "\<And>x t c. \<lbrakk>{atom x} \<sharp>* c; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Lam x t)" |
251 and a3: "\<And>x t c. \<lbrakk>{atom x} \<sharp>* c; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Lam x t)" |
189 and a4: "\<And>as t c. \<lbrakk>set (bn1 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let1 as t)" |
252 and a4: "\<And>as t c. \<lbrakk>set (bn1 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let1 as t)" |
190 and a5: "\<And>as t c. \<lbrakk>set (bn2 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let2 as t)" |
253 and a5: "\<And>as t c. \<lbrakk>set (bn2 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let2 as t)" |
191 and a6: "\<And>as t c. \<lbrakk>set (bn3 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let3 as t)" |
254 and a6: "\<And>as t c. \<lbrakk>set (bn3 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let3 as t)" |
192 and a7: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)" |
255 and a7: "\<And>as' t c. \<lbrakk>(bn4 as') \<sharp>* c; \<And>d. P3 d as'; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let4 as' t)" |
193 shows "P1 c t" "P2 c as" |
256 and a8: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)" |
|
257 and a9: "\<And>c. P3 c (BNil)" |
|
258 and a10: "\<And>c a as. \<And>d. P3 d as \<Longrightarrow> P3 c (BAs a as)" |
|
259 shows "P1 c t" "P2 c as" "P3 c as'" |
194 using assms |
260 using assms |
195 apply(induction_schema) |
261 apply(induction_schema) |
196 apply(rule_tac y="t" and c="c" in strong_exhaust1) |
262 apply(rule_tac y="t" and c="c" in strong_exhaust1) |
197 apply(simp_all)[6] |
263 apply(simp_all)[7] |
198 apply(rule_tac as="as" in strong_exhaust2) |
264 apply(rule_tac as="as" in strong_exhaust2) |
199 apply(simp) |
265 apply(simp) |
200 apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))") |
266 apply(rule_tac as'="as'" in strong_exhaust3) |
|
267 apply(simp_all)[2] |
|
268 apply(relation "measure (sum_case (size o snd) (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z))))") |
201 apply(simp_all add: foo.size) |
269 apply(simp_all add: foo.size) |
202 done |
270 done |
203 |
271 |
204 end |
272 end |
205 |
273 |