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