1 theory Terms |
|
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 text {* primrec seems to be genarally faster than fun *} |
|
8 |
|
9 section {*** lets with binding patterns ***} |
|
10 |
|
11 datatype rtrm1 = |
|
12 rVr1 "name" |
|
13 | rAp1 "rtrm1" "rtrm1" |
|
14 | rLm1 "name" "rtrm1" --"name is bound in trm1" |
|
15 | rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1" |
|
16 and bp = |
|
17 BUnit |
|
18 | BVr "name" |
|
19 | BPr "bp" "bp" |
|
20 |
|
21 (* to be given by the user *) |
|
22 |
|
23 primrec |
|
24 bv1 |
|
25 where |
|
26 "bv1 (BUnit) = {}" |
|
27 | "bv1 (BVr x) = {atom x}" |
|
28 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
|
29 |
|
30 local_setup {* define_raw_fv "Terms.rtrm1" |
|
31 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], |
|
32 [[], [[]], [[], []]]] *} |
|
33 print_theorems |
|
34 |
|
35 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *} |
|
36 |
|
37 inductive |
|
38 alpha1 :: "rtrm1 \<Rightarrow> rtrm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100) |
|
39 where |
|
40 a1: "a = b \<Longrightarrow> (rVr1 a) \<approx>1 (rVr1 b)" |
|
41 | a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> rAp1 t1 s1 \<approx>1 rAp1 t2 s2" |
|
42 | a3: "(\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 fv_rtrm1 pi ({atom ab}, s))) \<Longrightarrow> rLm1 aa t \<approx>1 rLm1 ab s" |
|
43 | a4: "t1 \<approx>1 t2 \<Longrightarrow> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 fv_rtrm1 pi ((bv1 b2), s2))) \<Longrightarrow> rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2" |
|
44 |
|
45 lemma alpha1_inj: |
|
46 "(rVr1 a \<approx>1 rVr1 b) = (a = b)" |
|
47 "(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)" |
|
48 "(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 fv_rtrm1 pi ({atom ab}, s)))" |
|
49 "(rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2) = (t1 \<approx>1 t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 fv_rtrm1 pi ((bv1 b2), s2))))" |
|
50 apply - |
|
51 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) |
|
52 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) |
|
53 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) |
|
54 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) |
|
55 done |
|
56 |
|
57 (* Shouyld we derive it? But bv is given by the user? *) |
|
58 lemma bv1_eqvt[eqvt]: |
|
59 shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)" |
|
60 apply (induct x) |
|
61 apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt eqvts) |
|
62 done |
|
63 |
|
64 lemma fv_rtrm1_eqvt[eqvt]: |
|
65 "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)" |
|
66 "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)" |
|
67 apply (induct t and b) |
|
68 apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt) |
|
69 done |
|
70 |
|
71 |
|
72 lemma alpha1_eqvt: |
|
73 shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)" |
|
74 apply (induct t s rule: alpha1.inducts) |
|
75 apply (simp_all add:eqvts alpha1_inj) |
|
76 apply (erule exE) |
|
77 apply (rule_tac x="pi \<bullet> pia" in exI) |
|
78 apply (simp add: alpha_gen) |
|
79 apply(erule conjE)+ |
|
80 apply(rule conjI) |
|
81 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
|
82 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt empty_eqvt fv_rtrm1_eqvt) |
|
83 apply(rule conjI) |
|
84 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
|
85 apply(simp add: atom_eqvt Diff_eqvt fv_rtrm1_eqvt insert_eqvt empty_eqvt) |
|
86 apply(simp add: permute_eqvt[symmetric]) |
|
87 apply (erule exE) |
|
88 apply (rule_tac x="pi \<bullet> pia" in exI) |
|
89 apply (simp add: alpha_gen) |
|
90 apply(erule conjE)+ |
|
91 apply(rule conjI) |
|
92 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
|
93 apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) |
|
94 apply(rule conjI) |
|
95 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
|
96 apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) |
|
97 apply(simp add: permute_eqvt[symmetric]) |
|
98 done |
|
99 |
|
100 lemma alpha1_equivp: "equivp alpha1" |
|
101 sorry |
|
102 |
|
103 quotient_type trm1 = rtrm1 / alpha1 |
|
104 by (rule alpha1_equivp) |
|
105 |
|
106 quotient_definition |
|
107 "Vr1 :: name \<Rightarrow> trm1" |
|
108 is |
|
109 "rVr1" |
|
110 |
|
111 quotient_definition |
|
112 "Ap1 :: trm1 \<Rightarrow> trm1 \<Rightarrow> trm1" |
|
113 is |
|
114 "rAp1" |
|
115 |
|
116 quotient_definition |
|
117 "Lm1 :: name \<Rightarrow> trm1 \<Rightarrow> trm1" |
|
118 is |
|
119 "rLm1" |
|
120 |
|
121 quotient_definition |
|
122 "Lt1 :: bp \<Rightarrow> trm1 \<Rightarrow> trm1 \<Rightarrow> trm1" |
|
123 is |
|
124 "rLt1" |
|
125 |
|
126 quotient_definition |
|
127 "fv_trm1 :: trm1 \<Rightarrow> atom set" |
|
128 is |
|
129 "fv_rtrm1" |
|
130 |
|
131 lemma alpha_rfv1: |
|
132 shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s" |
|
133 apply(induct rule: alpha1.induct) |
|
134 apply(simp_all add: alpha_gen.simps) |
|
135 sorry |
|
136 |
|
137 lemma [quot_respect]: |
|
138 "(op = ===> alpha1) rVr1 rVr1" |
|
139 "(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1" |
|
140 "(op = ===> alpha1 ===> alpha1) rLm1 rLm1" |
|
141 "(op = ===> alpha1 ===> alpha1 ===> alpha1) rLt1 rLt1" |
|
142 apply (auto simp add: alpha1_inj) |
|
143 apply (rule_tac x="0" in exI) |
|
144 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen) |
|
145 apply (rule_tac x="0" in exI) |
|
146 apply (simp add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1) |
|
147 done |
|
148 |
|
149 lemma [quot_respect]: |
|
150 "(op = ===> alpha1 ===> alpha1) permute permute" |
|
151 by (simp add: alpha1_eqvt) |
|
152 |
|
153 lemma [quot_respect]: |
|
154 "(alpha1 ===> op =) fv_rtrm1 fv_rtrm1" |
|
155 by (simp add: alpha_rfv1) |
|
156 |
|
157 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
|
158 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
|
159 |
|
160 instantiation trm1 and bp :: pt |
|
161 begin |
|
162 |
|
163 quotient_definition |
|
164 "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1" |
|
165 is |
|
166 "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1" |
|
167 |
|
168 lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted] |
|
169 |
|
170 instance |
|
171 apply default |
|
172 apply(induct_tac [!] x rule: trm1_bp_inducts(1)) |
|
173 apply(simp_all) |
|
174 done |
|
175 |
|
176 end |
|
177 |
|
178 lemmas fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] |
|
179 |
|
180 lemmas fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted] |
|
181 |
|
182 lemmas alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
|
183 |
|
184 lemma lm1_supp_pre: |
|
185 shows "(supp (atom x, t)) supports (Lm1 x t) " |
|
186 apply(simp add: supports_def) |
|
187 apply(fold fresh_def) |
|
188 apply(simp add: fresh_Pair swap_fresh_fresh) |
|
189 apply(clarify) |
|
190 apply(subst swap_at_base_simps(3)) |
|
191 apply(simp_all add: fresh_atom) |
|
192 done |
|
193 |
|
194 lemma lt1_supp_pre: |
|
195 shows "(supp (x, t, s)) supports (Lt1 t x s) " |
|
196 apply(simp add: supports_def) |
|
197 apply(fold fresh_def) |
|
198 apply(simp add: fresh_Pair swap_fresh_fresh) |
|
199 done |
|
200 |
|
201 lemma bp_supp: "finite (supp (bp :: bp))" |
|
202 apply (induct bp) |
|
203 apply(simp_all add: supp_def) |
|
204 apply (fold supp_def) |
|
205 apply (simp add: supp_at_base) |
|
206 apply(simp add: Collect_imp_eq) |
|
207 apply(simp add: Collect_neg_eq[symmetric]) |
|
208 apply (fold supp_def) |
|
209 apply (simp) |
|
210 done |
|
211 |
|
212 instance trm1 :: fs |
|
213 apply default |
|
214 apply(induct_tac x rule: trm1_bp_inducts(1)) |
|
215 apply(simp_all) |
|
216 apply(simp add: supp_def alpha1_INJ eqvts) |
|
217 apply(simp add: supp_def[symmetric] supp_at_base) |
|
218 apply(simp only: supp_def alpha1_INJ eqvts permute_trm1) |
|
219 apply(simp add: Collect_imp_eq Collect_neg_eq) |
|
220 apply(rule supports_finite) |
|
221 apply(rule lm1_supp_pre) |
|
222 apply(simp add: supp_Pair supp_atom) |
|
223 apply(rule supports_finite) |
|
224 apply(rule lt1_supp_pre) |
|
225 apply(simp add: supp_Pair supp_atom bp_supp) |
|
226 done |
|
227 |
|
228 lemma fv_eq_bv: "fv_bp bp = bv1 bp" |
|
229 apply(induct bp rule: trm1_bp_inducts(2)) |
|
230 apply(simp_all) |
|
231 done |
|
232 |
|
233 lemma supp_fv: |
|
234 shows "supp t = fv_trm1 t" |
|
235 apply(induct t rule: trm1_bp_inducts(1)) |
|
236 apply(simp_all) |
|
237 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
|
238 apply(simp only: supp_at_base[simplified supp_def]) |
|
239 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
|
240 apply(simp add: Collect_imp_eq Collect_neg_eq) |
|
241 apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)") |
|
242 apply(simp add: supp_Abs fv_trm1) |
|
243 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) |
|
244 apply(simp add: alpha1_INJ) |
|
245 apply(simp add: Abs_eq_iff) |
|
246 apply(simp add: alpha_gen.simps) |
|
247 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) |
|
248 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)") |
|
249 apply(simp add: supp_Abs fv_trm1 fv_eq_bv) |
|
250 apply(simp (no_asm) add: supp_def) |
|
251 apply(simp add: alpha1_INJ) |
|
252 apply(simp add: Abs_eq_iff) |
|
253 apply(simp add: alpha_gen) |
|
254 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt) |
|
255 apply(simp add: Collect_imp_eq Collect_neg_eq) |
|
256 done |
|
257 |
|
258 lemma trm1_supp: |
|
259 "supp (Vr1 x) = {atom x}" |
|
260 "supp (Ap1 t1 t2) = supp t1 \<union> supp t2" |
|
261 "supp (Lm1 x t) = (supp t) - {atom x}" |
|
262 "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)" |
|
263 by (simp_all add: supp_fv fv_trm1 fv_eq_bv) |
|
264 |
|
265 lemma trm1_induct_strong: |
|
266 assumes "\<And>name b. P b (Vr1 name)" |
|
267 and "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)" |
|
268 and "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)" |
|
269 and "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bv1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)" |
|
270 shows "P a rtrma" |
|
271 sorry |
|
272 |
|
273 section {*** lets with single assignments ***} |
|
274 |
|
275 datatype rtrm2 = |
|
276 rVr2 "name" |
|
277 | rAp2 "rtrm2" "rtrm2" |
|
278 | rLm2 "name" "rtrm2" --"bind (name) in (rtrm2)" |
|
279 | rLt2 "rassign" "rtrm2" --"bind (bv2 rassign) in (rtrm2)" |
|
280 and rassign = |
|
281 rAs "name" "rtrm2" |
|
282 |
|
283 (* to be given by the user *) |
|
284 primrec |
|
285 rbv2 |
|
286 where |
|
287 "rbv2 (rAs x t) = {atom x}" |
|
288 |
|
289 local_setup {* define_raw_fv "Terms.rtrm2" |
|
290 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv2}, 0)], [(SOME @{term rbv2}, 0)]]], |
|
291 [[[], []]]] *} |
|
292 print_theorems |
|
293 |
|
294 setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *} |
|
295 |
|
296 inductive |
|
297 alpha2 :: "rtrm2 \<Rightarrow> rtrm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100) |
|
298 and |
|
299 alpha2a :: "rassign \<Rightarrow> rassign \<Rightarrow> bool" ("_ \<approx>2a _" [100, 100] 100) |
|
300 where |
|
301 a1: "a = b \<Longrightarrow> (rVr2 a) \<approx>2 (rVr2 b)" |
|
302 | a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rAp2 t1 s1 \<approx>2 rAp2 t2 s2" |
|
303 | a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha2 fv_rtrm2 pi ({atom b}, s))) \<Longrightarrow> rLm2 a t \<approx>2 rLm2 b s" |
|
304 | a4: "\<lbrakk>\<exists>pi. ((rbv2 bt, t) \<approx>gen alpha2 fv_rtrm2 pi ((rbv2 bs), s)); |
|
305 \<exists>pi. ((rbv2 bt, bt) \<approx>gen alpha2a fv_rassign pi (rbv2 bs, bs))\<rbrakk> |
|
306 \<Longrightarrow> rLt2 bt t \<approx>2 rLt2 bs s" |
|
307 | a5: "\<lbrakk>a = b; t \<approx>2 s\<rbrakk> \<Longrightarrow> rAs a t \<approx>2a rAs b s" (* This way rbv2 can be lifted *) |
|
308 |
|
309 lemma alpha2_equivp: |
|
310 "equivp alpha2" |
|
311 "equivp alpha2a" |
|
312 sorry |
|
313 |
|
314 quotient_type |
|
315 trm2 = rtrm2 / alpha2 |
|
316 and |
|
317 assign = rassign / alpha2a |
|
318 by (auto intro: alpha2_equivp) |
|
319 |
|
320 |
|
321 |
|
322 section {*** lets with many assignments ***} |
|
323 |
|
324 datatype trm3 = |
|
325 Vr3 "name" |
|
326 | Ap3 "trm3" "trm3" |
|
327 | Lm3 "name" "trm3" --"bind (name) in (trm3)" |
|
328 | Lt3 "assigns" "trm3" --"bind (bv3 assigns) in (trm3)" |
|
329 and assigns = |
|
330 ANil |
|
331 | ACons "name" "trm3" "assigns" |
|
332 |
|
333 (* to be given by the user *) |
|
334 primrec |
|
335 bv3 |
|
336 where |
|
337 "bv3 ANil = {}" |
|
338 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
|
339 |
|
340 local_setup {* define_raw_fv "Terms.trm3" |
|
341 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv3}, 0)], [(SOME @{term bv3}, 0)]]], |
|
342 [[], [[], [], []]]] *} |
|
343 print_theorems |
|
344 |
|
345 setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *} |
|
346 |
|
347 inductive |
|
348 alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100) |
|
349 and |
|
350 alpha3a :: "assigns \<Rightarrow> assigns \<Rightarrow> bool" ("_ \<approx>3a _" [100, 100] 100) |
|
351 where |
|
352 a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)" |
|
353 | a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2" |
|
354 | a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha3 fv_rtrm3 pi ({atom b}, s))) \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s" |
|
355 | a4: "\<lbrakk>\<exists>pi. ((bv3 bt, t) \<approx>gen alpha3 fv_trm3 pi ((bv3 bs), s)); |
|
356 \<exists>pi. ((bv3 bt, bt) \<approx>gen alpha3a fv_assign pi (bv3 bs, bs))\<rbrakk> |
|
357 \<Longrightarrow> Lt3 bt t \<approx>3 Lt3 bs s" |
|
358 | a5: "ANil \<approx>3a ANil" |
|
359 | a6: "\<lbrakk>a = b; t \<approx>3 s; tt \<approx>3a st\<rbrakk> \<Longrightarrow> ACons a t tt \<approx>3a ACons b s st" |
|
360 |
|
361 lemma alpha3_equivp: |
|
362 "equivp alpha3" |
|
363 "equivp alpha3a" |
|
364 sorry |
|
365 |
|
366 quotient_type |
|
367 qtrm3 = trm3 / alpha3 |
|
368 and |
|
369 qassigns = assigns / alpha3a |
|
370 by (auto intro: alpha3_equivp) |
|
371 |
|
372 |
|
373 section {*** lam with indirect list recursion ***} |
|
374 |
|
375 datatype trm4 = |
|
376 Vr4 "name" |
|
377 | Ap4 "trm4" "trm4 list" |
|
378 | Lm4 "name" "trm4" --"bind (name) in (trm)" |
|
379 print_theorems |
|
380 |
|
381 thm trm4.recs |
|
382 |
|
383 local_setup {* define_raw_fv "Terms.trm4" [ |
|
384 [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *} |
|
385 print_theorems |
|
386 |
|
387 (* there cannot be a clause for lists, as *) |
|
388 (* permutations are already defined in Nominal (also functions, options, and so on) *) |
|
389 setup {* snd o define_raw_perms ["trm4"] ["Terms.trm4"] *} |
|
390 |
|
391 (* "repairing" of the permute function *) |
|
392 lemma repaired: |
|
393 fixes ts::"trm4 list" |
|
394 shows "permute_trm4_list p ts = p \<bullet> ts" |
|
395 apply(induct ts) |
|
396 apply(simp_all) |
|
397 done |
|
398 |
|
399 thm permute_trm4_permute_trm4_list.simps |
|
400 thm permute_trm4_permute_trm4_list.simps[simplified repaired] |
|
401 |
|
402 inductive |
|
403 alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100) |
|
404 and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100) |
|
405 where |
|
406 a1: "a = b \<Longrightarrow> (Vr4 a) \<approx>4 (Vr4 b)" |
|
407 | a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2" |
|
408 | a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha4 fv_rtrm4 pi ({atom b}, s))) \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s" |
|
409 | a5: "[] \<approx>4list []" |
|
410 | a6: "\<lbrakk>t \<approx>4 s; ts \<approx>4list ss\<rbrakk> \<Longrightarrow> (t#ts) \<approx>4list (s#ss)" |
|
411 |
|
412 lemma alpha4_equivp: "equivp alpha4" sorry |
|
413 lemma alpha4list_equivp: "equivp alpha4list" sorry |
|
414 |
|
415 quotient_type |
|
416 qtrm4 = trm4 / alpha4 and |
|
417 qtrm4list = "trm4 list" / alpha4list |
|
418 by (simp_all add: alpha4_equivp alpha4list_equivp) |
|
419 |
|
420 |
|
421 datatype rtrm5 = |
|
422 rVr5 "name" |
|
423 | rAp5 "rtrm5" "rtrm5" |
|
424 | rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" |
|
425 and rlts = |
|
426 rLnil |
|
427 | rLcons "name" "rtrm5" "rlts" |
|
428 |
|
429 primrec |
|
430 rbv5 |
|
431 where |
|
432 "rbv5 rLnil = {}" |
|
433 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
|
434 |
|
435 local_setup {* define_raw_fv "Terms.rtrm5" [ |
|
436 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *} |
|
437 print_theorems |
|
438 |
|
439 setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *} |
|
440 print_theorems |
|
441 |
|
442 inductive |
|
443 alpha5 :: "rtrm5 \<Rightarrow> rtrm5 \<Rightarrow> bool" ("_ \<approx>5 _" [100, 100] 100) |
|
444 and |
|
445 alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100) |
|
446 where |
|
447 a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)" |
|
448 | a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2" |
|
449 | a3: "\<lbrakk>\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 fv_rtrm5 pi (rbv5 l2, t2)); |
|
450 \<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts fv_rlts pi (rbv5 l2, l2))\<rbrakk> |
|
451 \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2" |
|
452 | a4: "rLnil \<approx>l rLnil" |
|
453 | a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2" |
|
454 |
|
455 print_theorems |
|
456 |
|
457 lemma alpha5_inj: |
|
458 "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)" |
|
459 "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)" |
|
460 "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = ((\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 fv_rtrm5 pi (rbv5 l2, t2))) \<and> |
|
461 (\<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts fv_rlts pi (rbv5 l2, l2))))" |
|
462 "rLnil \<approx>l rLnil" |
|
463 "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (n1 = n2 \<and> ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2)" |
|
464 apply - |
|
465 apply (simp_all add: alpha5_alphalts.intros) |
|
466 apply rule |
|
467 apply (erule alpha5.cases) |
|
468 apply (simp_all add: alpha5_alphalts.intros) |
|
469 apply rule |
|
470 apply (erule alpha5.cases) |
|
471 apply (simp_all add: alpha5_alphalts.intros) |
|
472 apply rule |
|
473 apply (erule alpha5.cases) |
|
474 apply (simp_all add: alpha5_alphalts.intros) |
|
475 apply rule |
|
476 apply (erule alphalts.cases) |
|
477 apply (simp_all add: alpha5_alphalts.intros) |
|
478 done |
|
479 |
|
480 lemma alpha5_equivps: |
|
481 shows "equivp alpha5" |
|
482 and "equivp alphalts" |
|
483 sorry |
|
484 |
|
485 quotient_type |
|
486 trm5 = rtrm5 / alpha5 |
|
487 and |
|
488 lts = rlts / alphalts |
|
489 by (auto intro: alpha5_equivps) |
|
490 |
|
491 quotient_definition |
|
492 "Vr5 :: name \<Rightarrow> trm5" |
|
493 is |
|
494 "rVr5" |
|
495 |
|
496 quotient_definition |
|
497 "Ap5 :: trm5 \<Rightarrow> trm5 \<Rightarrow> trm5" |
|
498 is |
|
499 "rAp5" |
|
500 |
|
501 quotient_definition |
|
502 "Lt5 :: lts \<Rightarrow> trm5 \<Rightarrow> trm5" |
|
503 is |
|
504 "rLt5" |
|
505 |
|
506 quotient_definition |
|
507 "Lnil :: lts" |
|
508 is |
|
509 "rLnil" |
|
510 |
|
511 quotient_definition |
|
512 "Lcons :: name \<Rightarrow> trm5 \<Rightarrow> lts \<Rightarrow> lts" |
|
513 is |
|
514 "rLcons" |
|
515 |
|
516 quotient_definition |
|
517 "fv_trm5 :: trm5 \<Rightarrow> atom set" |
|
518 is |
|
519 "fv_rtrm5" |
|
520 |
|
521 quotient_definition |
|
522 "fv_lts :: lts \<Rightarrow> atom set" |
|
523 is |
|
524 "fv_rlts" |
|
525 |
|
526 quotient_definition |
|
527 "bv5 :: lts \<Rightarrow> atom set" |
|
528 is |
|
529 "rbv5" |
|
530 |
|
531 lemma rbv5_eqvt: |
|
532 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
|
533 sorry |
|
534 |
|
535 lemma fv_rtrm5_eqvt: |
|
536 "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)" |
|
537 sorry |
|
538 |
|
539 lemma fv_rlts_eqvt: |
|
540 "pi \<bullet> (fv_rlts x) = fv_rlts (pi \<bullet> x)" |
|
541 sorry |
|
542 |
|
543 lemma alpha5_eqvt: |
|
544 "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)" |
|
545 "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)" |
|
546 apply(induct rule: alpha5_alphalts.inducts) |
|
547 apply (simp_all add: alpha5_inj) |
|
548 apply (erule exE)+ |
|
549 apply(unfold alpha_gen) |
|
550 apply (erule conjE)+ |
|
551 apply (rule conjI) |
|
552 apply (rule_tac x="x \<bullet> pi" in exI) |
|
553 apply (rule conjI) |
|
554 apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) |
|
555 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) |
|
556 apply(rule conjI) |
|
557 apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) |
|
558 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) |
|
559 apply (subst permute_eqvt[symmetric]) |
|
560 apply (simp) |
|
561 apply (rule_tac x="x \<bullet> pia" in exI) |
|
562 apply (rule conjI) |
|
563 apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) |
|
564 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) |
|
565 apply(rule conjI) |
|
566 apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) |
|
567 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) |
|
568 apply (subst permute_eqvt[symmetric]) |
|
569 apply (simp) |
|
570 done |
|
571 |
|
572 lemma alpha5_rfv: |
|
573 "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)" |
|
574 "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)" |
|
575 apply(induct rule: alpha5_alphalts.inducts) |
|
576 apply(simp_all add: alpha_gen) |
|
577 done |
|
578 |
|
579 lemma bv_list_rsp: |
|
580 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
|
581 apply(induct rule: alpha5_alphalts.inducts(2)) |
|
582 apply(simp_all) |
|
583 done |
|
584 |
|
585 lemma [quot_respect]: |
|
586 "(alphalts ===> op =) fv_rlts fv_rlts" |
|
587 "(alpha5 ===> op =) fv_rtrm5 fv_rtrm5" |
|
588 "(alphalts ===> op =) rbv5 rbv5" |
|
589 "(op = ===> alpha5) rVr5 rVr5" |
|
590 "(alpha5 ===> alpha5 ===> alpha5) rAp5 rAp5" |
|
591 "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5" |
|
592 "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5" |
|
593 "(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons" |
|
594 "(op = ===> alpha5 ===> alpha5) permute permute" |
|
595 "(op = ===> alphalts ===> alphalts) permute permute" |
|
596 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) |
|
597 apply (clarify) apply (rule conjI) |
|
598 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
|
599 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
|
600 apply (clarify) apply (rule conjI) |
|
601 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
|
602 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
|
603 done |
|
604 |
|
605 lemma |
|
606 shows "(alphalts ===> op =) rbv5 rbv5" |
|
607 by (simp add: bv_list_rsp) |
|
608 |
|
609 lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] |
|
610 |
|
611 instantiation trm5 and lts :: pt |
|
612 begin |
|
613 |
|
614 quotient_definition |
|
615 "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5" |
|
616 is |
|
617 "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5" |
|
618 |
|
619 quotient_definition |
|
620 "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts" |
|
621 is |
|
622 "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts" |
|
623 |
|
624 lemma trm5_lts_zero: |
|
625 "0 \<bullet> (x\<Colon>trm5) = x" |
|
626 "0 \<bullet> (y\<Colon>lts) = y" |
|
627 apply(induct x and y rule: trm5_lts_inducts) |
|
628 apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted]) |
|
629 done |
|
630 |
|
631 lemma trm5_lts_plus: |
|
632 "(p + q) \<bullet> (x\<Colon>trm5) = p \<bullet> q \<bullet> x" |
|
633 "(p + q) \<bullet> (y\<Colon>lts) = p \<bullet> q \<bullet> y" |
|
634 apply(induct x and y rule: trm5_lts_inducts) |
|
635 apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted]) |
|
636 done |
|
637 |
|
638 instance |
|
639 apply default |
|
640 apply (simp_all add: trm5_lts_zero trm5_lts_plus) |
|
641 done |
|
642 |
|
643 end |
|
644 |
|
645 lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] |
|
646 |
|
647 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
|
648 |
|
649 lemmas bv5[simp] = rbv5.simps[quot_lifted] |
|
650 |
|
651 lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] |
|
652 |
|
653 lemma lets_ok: |
|
654 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
|
655 apply (subst alpha5_INJ) |
|
656 apply (rule conjI) |
|
657 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
658 apply (simp only: alpha_gen) |
|
659 apply (simp add: permute_trm5_lts fresh_star_def) |
|
660 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
661 apply (simp only: alpha_gen) |
|
662 apply (simp add: permute_trm5_lts fresh_star_def) |
|
663 done |
|
664 |
|
665 lemma lets_ok2: |
|
666 "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = |
|
667 (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
668 apply (subst alpha5_INJ) |
|
669 apply (rule conjI) |
|
670 apply (rule_tac x="0 :: perm" in exI) |
|
671 apply (simp only: alpha_gen) |
|
672 apply (simp add: permute_trm5_lts fresh_star_def) |
|
673 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
674 apply (simp only: alpha_gen) |
|
675 apply (simp add: permute_trm5_lts fresh_star_def) |
|
676 done |
|
677 |
|
678 |
|
679 lemma lets_not_ok1: |
|
680 "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
|
681 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
682 apply (subst alpha5_INJ(3)) |
|
683 apply(clarify) |
|
684 apply (simp add: alpha_gen) |
|
685 apply (simp add: permute_trm5_lts fresh_star_def) |
|
686 apply (simp add: alpha5_INJ(5)) |
|
687 apply(clarify) |
|
688 apply (simp add: alpha5_INJ(2)) |
|
689 apply (simp only: alpha5_INJ(1)) |
|
690 done |
|
691 |
|
692 lemma distinct_helper: |
|
693 shows "\<not>(rVr5 x \<approx>5 rAp5 y z)" |
|
694 apply auto |
|
695 apply (erule alpha5.cases) |
|
696 apply (simp_all only: rtrm5.distinct) |
|
697 done |
|
698 |
|
699 lemma distinct_helper2: |
|
700 shows "(Vr5 x) \<noteq> (Ap5 y z)" |
|
701 by (lifting distinct_helper) |
|
702 |
|
703 lemma lets_nok: |
|
704 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
|
705 (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
|
706 (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
|
707 apply (subst alpha5_INJ) |
|
708 apply (simp only: alpha_gen permute_trm5_lts fresh_star_def) |
|
709 apply (subst alpha5_INJ(5)) |
|
710 apply (subst alpha5_INJ(5)) |
|
711 apply (simp add: distinct_helper2) |
|
712 done |
|
713 |
|
714 |
|
715 (* example with a bn function defined over the type itself *) |
|
716 datatype rtrm6 = |
|
717 rVr6 "name" |
|
718 | rLm6 "name" "rtrm6" |
|
719 | rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)" |
|
720 |
|
721 primrec |
|
722 rbv6 |
|
723 where |
|
724 "rbv6 (rVr6 n) = {}" |
|
725 | "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t" |
|
726 | "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r" |
|
727 |
|
728 local_setup {* define_raw_fv "Terms.rtrm6" [ |
|
729 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv6}, 0)], [(SOME @{term rbv6}, 0)]]]] *} |
|
730 print_theorems |
|
731 |
|
732 setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *} |
|
733 print_theorems |
|
734 |
|
735 inductive |
|
736 alpha6 :: "rtrm6 \<Rightarrow> rtrm6 \<Rightarrow> bool" ("_ \<approx>6 _" [100, 100] 100) |
|
737 where |
|
738 a1: "a = b \<Longrightarrow> (rVr6 a) \<approx>6 (rVr6 b)" |
|
739 | a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha6 fv_rtrm6 pi ({atom b}, s))) \<Longrightarrow> rLm6 a t \<approx>6 rLm6 b s" |
|
740 | a3: "(\<exists>pi. (((rbv6 t1), s1) \<approx>gen alpha6 fv_rtrm6 pi ((rbv6 t2), s2))) \<Longrightarrow> rLt6 t1 s1 \<approx>6 rLt6 t2 s2" |
|
741 |
|
742 lemma alpha6_equivps: |
|
743 shows "equivp alpha6" |
|
744 sorry |
|
745 |
|
746 quotient_type |
|
747 trm6 = rtrm6 / alpha6 |
|
748 by (auto intro: alpha6_equivps) |
|
749 |
|
750 quotient_definition |
|
751 "Vr6 :: name \<Rightarrow> trm6" |
|
752 is |
|
753 "rVr6" |
|
754 |
|
755 quotient_definition |
|
756 "Lm6 :: name \<Rightarrow> trm6 \<Rightarrow> trm6" |
|
757 is |
|
758 "rLm6" |
|
759 |
|
760 quotient_definition |
|
761 "Lt6 :: trm6 \<Rightarrow> trm6 \<Rightarrow> trm6" |
|
762 is |
|
763 "rLt6" |
|
764 |
|
765 quotient_definition |
|
766 "fv_trm6 :: trm6 \<Rightarrow> atom set" |
|
767 is |
|
768 "fv_rtrm6" |
|
769 |
|
770 quotient_definition |
|
771 "bv6 :: trm6 \<Rightarrow> atom set" |
|
772 is |
|
773 "rbv6" |
|
774 |
|
775 lemma [quot_respect]: |
|
776 "(op = ===> alpha6 ===> alpha6) permute permute" |
|
777 apply auto (* will work with eqvt *) |
|
778 sorry |
|
779 |
|
780 (* Definitely not true , see lemma below *) |
|
781 |
|
782 lemma [quot_respect]:"(alpha6 ===> op =) rbv6 rbv6" |
|
783 apply simp apply clarify |
|
784 apply (erule alpha6.induct) |
|
785 oops |
|
786 |
|
787 lemma "(a :: name) \<noteq> b \<Longrightarrow> \<not> (alpha6 ===> op =) rbv6 rbv6" |
|
788 apply simp |
|
789 apply (rule_tac x="rLm6 (a::name) (rVr6 (a :: name))" in exI) |
|
790 apply (rule_tac x="rLm6 (b::name) (rVr6 (b :: name))" in exI) |
|
791 apply simp |
|
792 apply (rule a2) |
|
793 apply (rule_tac x="(a \<leftrightarrow> b)" in exI) |
|
794 apply (simp add: alpha_gen fresh_star_def) |
|
795 apply (rule a1) |
|
796 apply (rule refl) |
|
797 done |
|
798 |
|
799 lemma [quot_respect]:"(alpha6 ===> op =) fv_rtrm6 fv_rtrm6" |
|
800 apply simp apply clarify |
|
801 apply (induct_tac x y rule: alpha6.induct) |
|
802 apply simp_all |
|
803 apply (erule exE) |
|
804 apply (simp_all add: alpha_gen) |
|
805 apply (erule conjE)+ |
|
806 apply (erule exE) |
|
807 apply (erule conjE)+ |
|
808 apply (simp) |
|
809 oops |
|
810 |
|
811 |
|
812 lemma [quot_respect]: "(op = ===> alpha6) rVr6 rVr6" |
|
813 by (simp_all add: a1) |
|
814 |
|
815 lemma [quot_respect]: |
|
816 "(op = ===> alpha6 ===> alpha6) rLm6 rLm6" |
|
817 "(alpha6 ===> alpha6 ===> alpha6) rLt6 rLt6" |
|
818 apply simp_all apply (clarify) |
|
819 apply (rule a2) |
|
820 apply (rule_tac x="0::perm" in exI) |
|
821 apply (simp add: alpha_gen) |
|
822 (* needs rfv6_rsp *) defer |
|
823 apply clarify |
|
824 apply (rule a3) |
|
825 apply (rule_tac x="0::perm" in exI) |
|
826 apply (simp add: alpha_gen) |
|
827 (* needs rbv6_rsp *) |
|
828 oops |
|
829 |
|
830 instantiation trm6 :: pt begin |
|
831 |
|
832 quotient_definition |
|
833 "permute_trm6 :: perm \<Rightarrow> trm6 \<Rightarrow> trm6" |
|
834 is |
|
835 "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6" |
|
836 |
|
837 instance |
|
838 apply default |
|
839 sorry |
|
840 end |
|
841 |
|
842 lemma lifted_induct: |
|
843 "\<lbrakk>x1 = x2; \<And>a b. a = b \<Longrightarrow> P (Vr6 a) (Vr6 b); |
|
844 \<And>a t b s. |
|
845 \<exists>pi. fv_trm6 t - {atom a} = fv_trm6 s - {atom b} \<and> |
|
846 (fv_trm6 t - {atom a}) \<sharp>* pi \<and> pi \<bullet> t = s \<and> P (pi \<bullet> t) s \<Longrightarrow> |
|
847 P (Lm6 a t) (Lm6 b s); |
|
848 \<And>t1 s1 t2 s2. |
|
849 \<exists>pi. fv_trm6 s1 - bv6 t1 = fv_trm6 s2 - bv6 t2 \<and> |
|
850 (fv_trm6 s1 - bv6 t1) \<sharp>* pi \<and> pi \<bullet> s1 = s2 \<and> P (pi \<bullet> s1) s2 \<Longrightarrow> |
|
851 P (Lt6 t1 s1) (Lt6 t2 s2)\<rbrakk> |
|
852 \<Longrightarrow> P x1 x2" |
|
853 unfolding alpha_gen |
|
854 apply (lifting alpha6.induct[unfolded alpha_gen]) |
|
855 apply injection |
|
856 (* notice unsolvable goals: (alpha6 ===> op =) rbv6 rbv6 *) |
|
857 oops |
|
858 |
|
859 lemma lifted_inject_a3: |
|
860 "\<exists>pi. fv_trm6 s1 - bv6 t1 = fv_trm6 s2 - bv6 t2 \<and> |
|
861 (fv_trm6 s1 - bv6 t1) \<sharp>* pi \<and> pi \<bullet> s1 = s2 \<Longrightarrow> Lt6 t1 s1 = Lt6 t2 s2" |
|
862 apply(lifting a3[unfolded alpha_gen]) |
|
863 apply injection |
|
864 (* notice unsolvable goals: (alpha6 ===> op =) rbv6 rbv6 *) |
|
865 oops |
|
866 |
|
867 |
|
868 |
|
869 |
|
870 (* example with a respectful bn function defined over the type itself *) |
|
871 |
|
872 datatype rtrm7 = |
|
873 rVr7 "name" |
|
874 | rLm7 "name" "rtrm7" |
|
875 | rLt7 "rtrm7" "rtrm7" --"bind (bv7 left) in (right)" |
|
876 |
|
877 primrec |
|
878 rbv7 |
|
879 where |
|
880 "rbv7 (rVr7 n) = {atom n}" |
|
881 | "rbv7 (rLm7 n t) = rbv7 t - {atom n}" |
|
882 | "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r" |
|
883 |
|
884 local_setup {* define_raw_fv "Terms.rtrm7" [ |
|
885 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv7}, 0)], [(SOME @{term rbv7}, 0)]]]] *} |
|
886 print_theorems |
|
887 |
|
888 setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *} |
|
889 print_theorems |
|
890 |
|
891 inductive |
|
892 alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100) |
|
893 where |
|
894 a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)" |
|
895 | a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s" |
|
896 | a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2" |
|
897 |
|
898 lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7" |
|
899 apply simp |
|
900 apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI) |
|
901 apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI) |
|
902 apply simp |
|
903 apply (rule a3) |
|
904 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
905 apply (simp_all add: alpha_gen fresh_star_def) |
|
906 apply (rule a1) |
|
907 apply (rule refl) |
|
908 done |
|
909 |
|
910 |
|
911 |
|
912 |
|
913 |
|
914 datatype rfoo8 = |
|
915 Foo0 "name" |
|
916 | Foo1 "rbar8" "rfoo8" --"bind bv(bar) in foo" |
|
917 and rbar8 = |
|
918 Bar0 "name" |
|
919 | Bar1 "name" "name" "rbar8" --"bind second name in b" |
|
920 |
|
921 primrec |
|
922 rbv8 |
|
923 where |
|
924 "rbv8 (Bar0 x) = {}" |
|
925 | "rbv8 (Bar1 v x b) = {atom v}" |
|
926 |
|
927 local_setup {* define_raw_fv "Terms.rfoo8" [ |
|
928 [[[]], [[(SOME @{term rbv8}, 0)], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *} |
|
929 print_theorems |
|
930 |
|
931 setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *} |
|
932 print_theorems |
|
933 |
|
934 inductive |
|
935 alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100) |
|
936 and |
|
937 alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100) |
|
938 where |
|
939 a1: "a = b \<Longrightarrow> (Foo0 a) \<approx>f (Foo0 b)" |
|
940 | a2: "a = b \<Longrightarrow> (Bar0 a) \<approx>b (Bar0 b)" |
|
941 | a3: "b1 \<approx>b b2 \<Longrightarrow> (\<exists>pi. (((rbv8 b1), t1) \<approx>gen alpha8f fv_rfoo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2" |
|
942 | a4: "v1 = v2 \<Longrightarrow> (\<exists>pi. (({atom x1}, t1) \<approx>gen alpha8b fv_rbar8 pi ({atom x2}, t2))) \<Longrightarrow> Bar1 v1 x1 t1 \<approx>b Bar1 v2 x2 t2" |
|
943 |
|
944 lemma "(alpha8b ===> op =) rbv8 rbv8" |
|
945 apply simp apply clarify |
|
946 apply (erule alpha8f_alpha8b.inducts(2)) |
|
947 apply (simp_all) |
|
948 done |
|
949 |
|
950 lemma fv_rbar8_rsp_hlp: "x \<approx>b y \<Longrightarrow> fv_rbar8 x = fv_rbar8 y" |
|
951 apply (erule alpha8f_alpha8b.inducts(2)) |
|
952 apply (simp_all add: alpha_gen) |
|
953 done |
|
954 lemma "(alpha8b ===> op =) fv_rbar8 fv_rbar8" |
|
955 apply simp apply clarify apply (simp add: fv_rbar8_rsp_hlp) |
|
956 done |
|
957 |
|
958 lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8" |
|
959 apply simp apply clarify |
|
960 apply (erule alpha8f_alpha8b.inducts(1)) |
|
961 apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp) |
|
962 apply clarify |
|
963 apply (erule alpha8f_alpha8b.inducts(2)) |
|
964 apply (simp_all) |
|
965 done |
|
966 |
|
967 |
|
968 |
|
969 |
|
970 |
|
971 |
|
972 datatype rlam9 = |
|
973 Var9 "name" |
|
974 | Lam9 "name" "rlam9" --"bind name in rlam" |
|
975 and rbla9 = |
|
976 Bla9 "rlam9" "rlam9" --"bind bv(first) in second" |
|
977 |
|
978 primrec |
|
979 rbv9 |
|
980 where |
|
981 "rbv9 (Var9 x) = {}" |
|
982 | "rbv9 (Lam9 x b) = {atom x}" |
|
983 |
|
984 local_setup {* define_raw_fv "Terms.rlam9" [ |
|
985 [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[(SOME @{term rbv9}, 0)], [(SOME @{term rbv9}, 0)]]]] *} |
|
986 print_theorems |
|
987 |
|
988 setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *} |
|
989 print_theorems |
|
990 |
|
991 inductive |
|
992 alpha9l :: "rlam9 \<Rightarrow> rlam9 \<Rightarrow> bool" ("_ \<approx>9l _" [100, 100] 100) |
|
993 and |
|
994 alpha9b :: "rbla9 \<Rightarrow> rbla9 \<Rightarrow> bool" ("_ \<approx>9b _" [100, 100] 100) |
|
995 where |
|
996 a1: "a = b \<Longrightarrow> (Var9 a) \<approx>9l (Var9 b)" |
|
997 | a4: "(\<exists>pi. (({atom x1}, t1) \<approx>gen alpha9l fv_rlam9 pi ({atom x2}, t2))) \<Longrightarrow> Lam9 x1 t1 \<approx>9l Lam9 x2 t2" |
|
998 | a3: "b1 \<approx>9l b2 \<Longrightarrow> (\<exists>pi. (((rbv9 b1), t1) \<approx>gen alpha9l fv_rlam9 pi ((rbv9 b2), t2))) \<Longrightarrow> Bla9 b1 t1 \<approx>9b Bla9 b2 t2" |
|
999 |
|
1000 quotient_type |
|
1001 lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b |
|
1002 sorry |
|
1003 |
|
1004 quotient_definition |
|
1005 "qVar9 :: name \<Rightarrow> lam9" |
|
1006 is |
|
1007 "Var9" |
|
1008 |
|
1009 quotient_definition |
|
1010 "qLam :: name \<Rightarrow> lam9 \<Rightarrow> lam9" |
|
1011 is |
|
1012 "Lam9" |
|
1013 |
|
1014 quotient_definition |
|
1015 "qBla9 :: lam9 \<Rightarrow> lam9 \<Rightarrow> bla9" |
|
1016 is |
|
1017 "Bla9" |
|
1018 |
|
1019 quotient_definition |
|
1020 "fv_lam9 :: lam9 \<Rightarrow> atom set" |
|
1021 is |
|
1022 "fv_rlam9" |
|
1023 |
|
1024 quotient_definition |
|
1025 "fv_bla9 :: bla9 \<Rightarrow> atom set" |
|
1026 is |
|
1027 "fv_rbla9" |
|
1028 |
|
1029 quotient_definition |
|
1030 "bv9 :: lam9 \<Rightarrow> atom set" |
|
1031 is |
|
1032 "rbv9" |
|
1033 |
|
1034 instantiation lam9 and bla9 :: pt |
|
1035 begin |
|
1036 |
|
1037 quotient_definition |
|
1038 "permute_lam9 :: perm \<Rightarrow> lam9 \<Rightarrow> lam9" |
|
1039 is |
|
1040 "permute :: perm \<Rightarrow> rlam9 \<Rightarrow> rlam9" |
|
1041 |
|
1042 quotient_definition |
|
1043 "permute_bla9 :: perm \<Rightarrow> bla9 \<Rightarrow> bla9" |
|
1044 is |
|
1045 "permute :: perm \<Rightarrow> rbla9 \<Rightarrow> rbla9" |
|
1046 |
|
1047 instance |
|
1048 sorry |
|
1049 |
|
1050 end |
|
1051 |
|
1052 lemma "\<lbrakk>b1 = b2; \<exists>pi. fv_lam9 t1 - bv9 b1 = fv_lam9 t2 - bv9 b2 \<and> (fv_lam9 t1 - bv9 b1) \<sharp>* pi \<and> pi \<bullet> t1 = t2\<rbrakk> |
|
1053 \<Longrightarrow> qBla9 b1 t1 = qBla9 b2 t2" |
|
1054 apply (lifting a3[unfolded alpha_gen]) |
|
1055 apply injection |
|
1056 sorry |
|
1057 |
|
1058 |
|
1059 |
|
1060 |
|
1061 |
|
1062 |
|
1063 |
|
1064 |
|
1065 text {* type schemes *} |
|
1066 datatype ty = |
|
1067 Var "name" |
|
1068 | Fun "ty" "ty" |
|
1069 |
|
1070 setup {* snd o define_raw_perms ["ty"] ["Terms.ty"] *} |
|
1071 print_theorems |
|
1072 |
|
1073 datatype tyS = |
|
1074 All "name set" "ty" |
|
1075 |
|
1076 setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *} |
|
1077 print_theorems |
|
1078 |
|
1079 abbreviation |
|
1080 "atoms xs \<equiv> {atom x| x. x \<in> xs}" |
|
1081 |
|
1082 local_setup {* define_raw_fv "Terms.ty" [[[[]], [[], []]]] *} |
|
1083 print_theorems |
|
1084 |
|
1085 (* |
|
1086 doesn't work yet |
|
1087 local_setup {* define_raw_fv "Terms.tyS" [[[[], []]]] *} |
|
1088 print_theorems |
|
1089 *) |
|
1090 |
|
1091 primrec |
|
1092 fv_tyS |
|
1093 where |
|
1094 "fv_tyS (All xs T) = (fv_ty T - atoms xs)" |
|
1095 |
|
1096 inductive |
|
1097 alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100) |
|
1098 where |
|
1099 a1: "\<exists>pi. ((atoms xs1, T1) \<approx>gen (op =) fv_ty pi (atoms xs2, T2)) |
|
1100 \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2" |
|
1101 |
|
1102 lemma |
|
1103 shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))" |
|
1104 apply(rule a1) |
|
1105 apply(simp add: alpha_gen) |
|
1106 apply(rule_tac x="0::perm" in exI) |
|
1107 apply(simp add: fresh_star_def) |
|
1108 done |
|
1109 |
|
1110 lemma |
|
1111 shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var b) (Var a))" |
|
1112 apply(rule a1) |
|
1113 apply(simp add: alpha_gen) |
|
1114 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI) |
|
1115 apply(simp add: fresh_star_def) |
|
1116 done |
|
1117 |
|
1118 lemma |
|
1119 shows "All {a, b, c} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var a) (Var b))" |
|
1120 apply(rule a1) |
|
1121 apply(simp add: alpha_gen) |
|
1122 apply(rule_tac x="0::perm" in exI) |
|
1123 apply(simp add: fresh_star_def) |
|
1124 done |
|
1125 |
|
1126 lemma |
|
1127 assumes a: "a \<noteq> b" |
|
1128 shows "\<not>(All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {c} (Fun (Var c) (Var c)))" |
|
1129 using a |
|
1130 apply(clarify) |
|
1131 apply(erule alpha_tyS.cases) |
|
1132 apply(simp add: alpha_gen) |
|
1133 apply(erule conjE)+ |
|
1134 apply(erule exE) |
|
1135 apply(erule conjE)+ |
|
1136 apply(clarify) |
|
1137 apply(simp) |
|
1138 apply(simp add: fresh_star_def) |
|
1139 apply(auto) |
|
1140 done |
|
1141 |
|
1142 |
|
1143 end |
|