8 nominal_datatype lam = |
8 nominal_datatype lam = |
9 Var "name" |
9 Var "name" |
10 | App "lam" "lam" |
10 | App "lam" "lam" |
11 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
11 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
12 |
12 |
13 lemma cheat: "P" sorry |
|
14 |
|
15 thm lam.strong_exhaust |
|
16 |
|
17 lemma lam_strong_exhaust2: |
|
18 "\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P; |
|
19 \<And>lam1 lam2. y = App lam1 lam2 \<Longrightarrow> P; |
|
20 \<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P; |
|
21 finite (supp c)\<rbrakk> |
|
22 \<Longrightarrow> P" |
|
23 sorry |
|
24 |
|
25 abbreviation |
|
26 "FCB f \<equiv> \<forall>x t r. atom x \<sharp> f x t r" |
|
27 |
|
28 nominal_primrec (invariant "\<lambda>x (y::atom set). finite y") |
13 nominal_primrec (invariant "\<lambda>x (y::atom set). finite y") |
29 frees_set :: "lam \<Rightarrow> atom set" |
14 frees_set :: "lam \<Rightarrow> atom set" |
30 where |
15 where |
31 "frees_set (Var x) = {atom x}" |
16 "frees_set (Var x) = {atom x}" |
32 | "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2" |
17 | "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2" |
33 | "frees_set (Lam [x]. t) = (frees_set t) - {atom x}" |
18 | "frees_set (Lam [x]. t) = (frees_set t) - {atom x}" |
34 apply(simp add: eqvt_def frees_set_graph_def) |
19 apply(simp add: eqvt_def frees_set_graph_def) |
35 apply (rule, perm_simp, rule) |
20 apply(rule, perm_simp, rule) |
36 apply(erule frees_set_graph.induct) |
21 apply(erule frees_set_graph.induct) |
37 apply(simp) |
22 apply(auto)[9] |
38 apply(simp) |
23 apply(rule_tac y="x" in lam.exhaust) |
39 apply(simp) |
24 apply(auto)[3] |
40 apply(rule_tac y="x" in lam.exhaust) |
25 apply(simp) |
41 apply(auto)[6] |
26 apply(erule Abs_lst1_fcb) |
42 apply(simp) |
27 apply(simp_all add: fresh_minus_atom_set) |
43 apply(simp) |
28 apply(erule fresh_eqvt_at) |
44 apply(simp) |
29 apply(simp_all add: finite_supp eqvt_at_def eqvts) |
45 apply (erule Abs_lst1_fcb) |
30 done |
46 apply(simp add: fresh_def) |
|
47 apply(subst supp_of_finite_sets) |
|
48 apply(simp) |
|
49 apply(simp add: supp_atom) |
|
50 apply(simp add: fresh_def) |
|
51 apply(subst supp_of_finite_sets) |
|
52 apply(simp) |
|
53 apply(simp add: supp_atom) |
|
54 apply(subst supp_finite_atom_set[symmetric]) |
|
55 apply(simp) |
|
56 apply(simp add: fresh_def[symmetric]) |
|
57 apply(rule fresh_eqvt_at) |
|
58 apply(assumption) |
|
59 apply(simp add: finite_supp) |
|
60 apply(simp) |
|
61 apply(simp add: eqvt_at_def eqvts) |
|
62 apply(simp) |
|
63 done |
|
64 |
31 |
65 termination |
32 termination |
66 by (relation "measure size") (auto simp add: lam.size) |
33 by (relation "measure size") (auto simp add: lam.size) |
67 |
34 |
68 thm frees_set.simps |
|
69 thm frees_set.induct |
|
70 |
|
71 lemma "frees_set t = supp t" |
35 lemma "frees_set t = supp t" |
72 apply(induct rule: frees_set.induct) |
36 by (induct rule: frees_set.induct) (simp_all add: lam.supp supp_at_base) |
73 apply(simp_all add: lam.supp supp_at_base) |
|
74 done |
|
75 |
37 |
76 lemma fresh_fun_eqvt_app3: |
38 lemma fresh_fun_eqvt_app3: |
77 assumes a: "eqvt f" |
39 assumes a: "eqvt f" |
78 and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" |
40 and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" |
79 shows "a \<sharp> f x y z" |
41 shows "a \<sharp> f x y z" |
87 assumes fs: "finite (supp (f1, f2, f3))" |
49 assumes fs: "finite (supp (f1, f2, f3))" |
88 and eq: "eqvt f1" "eqvt f2" "eqvt f3" |
50 and eq: "eqvt f1" "eqvt f2" "eqvt f3" |
89 and fcb: "\<forall>x t r. atom x \<sharp> f3 x t r" |
51 and fcb: "\<forall>x t r. atom x \<sharp> f3 x t r" |
90 begin |
52 begin |
91 |
53 |
92 nominal_primrec |
54 nominal_primrec |
93 f :: "lam \<Rightarrow> ('a::pt)" |
55 f :: "lam \<Rightarrow> ('a::pt)" |
94 where |
56 where |
95 "f (Var x) = f1 x" |
57 "f (Var x) = f1 x" |
96 | "f (App t1 t2) = f2 t1 t2 (f t1) (f t2)" |
58 | "f (App t1 t2) = f2 t1 t2 (f t1) (f t2)" |
97 | "f (Lam [x].t) = f3 x t (f t)" |
59 | "f (Lam [x].t) = f3 x t (f t)" |
221 |
183 |
222 termination |
184 termination |
223 by (relation "measure size") (simp_all add: lam.size) |
185 by (relation "measure size") (simp_all add: lam.size) |
224 |
186 |
225 text {* a small test lemma *} |
187 text {* a small test lemma *} |
226 lemma |
188 lemma shows "supp t = set (frees_lst t)" |
227 shows "supp t = set (frees_lst t)" |
189 by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base) |
228 apply(induct t rule: frees_lst.induct) |
|
229 apply(simp_all add: lam.supp supp_at_base) |
|
230 done |
|
231 |
190 |
232 text {* capture - avoiding substitution *} |
191 text {* capture - avoiding substitution *} |
233 |
192 |
234 nominal_primrec |
193 nominal_primrec |
235 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
194 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
261 shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]" |
220 shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]" |
262 by (induct t x s rule: subst.induct) (simp_all) |
221 by (induct t x s rule: subst.induct) (simp_all) |
263 |
222 |
264 lemma forget: |
223 lemma forget: |
265 shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t" |
224 shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t" |
266 apply(nominal_induct t avoiding: x s rule: lam.strong_induct) |
225 by (nominal_induct t avoiding: x s rule: lam.strong_induct) |
267 apply(auto simp add: lam.fresh fresh_at_base) |
226 (auto simp add: lam.fresh fresh_at_base) |
268 done |
|
269 |
227 |
270 text {* same lemma but with subst.induction *} |
228 text {* same lemma but with subst.induction *} |
271 lemma forget2: |
229 lemma forget2: |
272 shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t" |
230 shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t" |
273 apply(induct t x s rule: subst.induct) |
231 by (induct t x s rule: subst.induct) |
274 apply(auto simp add: lam.fresh fresh_at_base fresh_Pair) |
232 (auto simp add: lam.fresh fresh_at_base fresh_Pair) |
275 done |
|
276 |
233 |
277 lemma fresh_fact: |
234 lemma fresh_fact: |
278 fixes z::"name" |
235 fixes z::"name" |
279 assumes a: "atom z \<sharp> s" |
236 assumes a: "atom z \<sharp> s" |
280 and b: "z = y \<or> atom z \<sharp> t" |
237 and b: "z = y \<or> atom z \<sharp> t" |
281 shows "atom z \<sharp> t[y ::= s]" |
238 shows "atom z \<sharp> t[y ::= s]" |
282 using a b |
239 using a b |
283 apply (nominal_induct t avoiding: z y s rule: lam.strong_induct) |
240 by (nominal_induct t avoiding: z y s rule: lam.strong_induct) |
284 apply (auto simp add: lam.fresh fresh_at_base) |
241 (auto simp add: lam.fresh fresh_at_base) |
285 done |
|
286 |
242 |
287 lemma substitution_lemma: |
243 lemma substitution_lemma: |
288 assumes a: "x \<noteq> y" "atom x \<sharp> u" |
244 assumes a: "x \<noteq> y" "atom x \<sharp> u" |
289 shows "t[x ::= s][y ::= u] = t[y ::= u][x ::= s[y ::= u]]" |
245 shows "t[x ::= s][y ::= u] = t[y ::= u][x ::= s[y ::= u]]" |
290 using a |
246 using a |
495 apply (simp_all add: permute_pure) |
451 apply (simp_all add: permute_pure) |
496 done |
452 done |
497 |
453 |
498 lemma fresh_at_list: "atom x \<sharp> xs \<longleftrightarrow> x \<notin> set xs" |
454 lemma fresh_at_list: "atom x \<sharp> xs \<longleftrightarrow> x \<notin> set xs" |
499 unfolding fresh_def supp_set[symmetric] |
455 unfolding fresh_def supp_set[symmetric] |
500 apply (induct xs) |
456 by (induct xs) (auto simp add: supp_of_finite_insert supp_at_base supp_set_empty) |
501 apply (simp add: supp_set_empty) |
|
502 apply simp |
|
503 apply auto |
|
504 apply (simp_all add: insert_absorb UnI2 finite_set supp_of_finite_insert supp_at_base) |
|
505 done |
|
506 |
457 |
507 fun |
458 fun |
508 vindex :: "name list \<Rightarrow> name \<Rightarrow> nat \<Rightarrow> db option" |
459 vindex :: "name list \<Rightarrow> name \<Rightarrow> nat \<Rightarrow> db option" |
509 where |
460 where |
510 "vindex [] v n = None" |
461 "vindex [] v n = None" |
547 apply (simp add: fresh_at_list[symmetric]) |
498 apply (simp add: fresh_at_list[symmetric]) |
548 apply (drule_tac x="name # l" in meta_spec) |
499 apply (drule_tac x="name # l" in meta_spec) |
549 apply auto |
500 apply auto |
550 done |
501 done |
551 |
502 |
552 (* |
|
553 lemma db_trans_test: |
503 lemma db_trans_test: |
554 assumes a: "y \<noteq> x" |
504 assumes a: "y \<noteq> x" |
555 shows "trans (Lam [x]. Lam [y]. App (Var x) (Var y)) [] 0 = Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))" |
505 shows "transdb (Lam [x]. Lam [y]. App (Var x) (Var y)) [] = Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))" |
556 using a by simp |
506 using a by simp |
557 *) |
|
558 |
507 |
559 abbreviation |
508 abbreviation |
560 mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65) |
509 mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65) |
561 where |
510 where |
562 "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v" |
511 "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v" |