3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 ML {* val _ = recursive := false *} |
7 ML {* val _ = recursive := false *} |
8 |
|
9 nominal_datatype lm = |
|
10 Vr "name" |
|
11 | Ap "lm" "lm" |
|
12 | Lm x::"name" l::"lm" bind x in l |
|
13 |
|
14 lemmas supp_fn' = lm.fv[simplified lm.supp] |
|
15 |
|
16 lemma |
|
17 fixes c::"'a::fs" |
|
18 assumes a1: "\<And>name c. P c (Vr name)" |
|
19 and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)" |
|
20 and a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)" |
|
21 shows "P c lm" |
|
22 proof - |
|
23 have "\<And>p. P c (p \<bullet> lm)" |
|
24 apply(induct lm arbitrary: c rule: lm.induct) |
|
25 apply(simp only: lm.perm) |
|
26 apply(rule a1) |
|
27 apply(simp only: lm.perm) |
|
28 apply(rule a2) |
|
29 apply(blast)[1] |
|
30 apply(assumption) |
|
31 apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))") |
|
32 defer |
|
33 apply(simp add: fresh_def) |
|
34 apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base) |
|
35 apply(simp add: supp_Pair finite_supp) |
|
36 apply(blast) |
|
37 apply(erule exE) |
|
38 apply(rule_tac t="p \<bullet> Lm name lm" and |
|
39 s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst) |
|
40 apply(simp del: lm.perm) |
|
41 apply(subst lm.perm) |
|
42 apply(subst (2) lm.perm) |
|
43 apply(rule flip_fresh_fresh) |
|
44 apply(simp add: fresh_def) |
|
45 apply(simp only: supp_fn') |
|
46 apply(simp) |
|
47 apply(simp add: fresh_Pair) |
|
48 apply(simp) |
|
49 apply(rule a3) |
|
50 apply(simp add: fresh_Pair) |
|
51 apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec) |
|
52 apply(simp) |
|
53 done |
|
54 then have "P c (0 \<bullet> lm)" by blast |
|
55 then show "P c lm" by simp |
|
56 qed |
|
57 |
|
58 |
|
59 lemma |
|
60 fixes c::"'a::fs" |
|
61 assumes a1: "\<And>name c. P c (Vr name)" |
|
62 and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)" |
|
63 and a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)" |
|
64 shows "P c lm" |
|
65 proof - |
|
66 have "\<And>p. P c (p \<bullet> lm)" |
|
67 apply(induct lm arbitrary: c rule: lm.induct) |
|
68 apply(simp only: lm.perm) |
|
69 apply(rule a1) |
|
70 apply(simp only: lm.perm) |
|
71 apply(rule a2) |
|
72 apply(blast)[1] |
|
73 apply(assumption) |
|
74 thm at_set_avoiding |
|
75 apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lm name lm) \<sharp>* q") |
|
76 apply(erule exE) |
|
77 apply(rule_tac t="p \<bullet> Lm name lm" and |
|
78 s="q \<bullet> p \<bullet> Lm name lm" in subst) |
|
79 defer |
|
80 apply(simp add: lm.perm) |
|
81 apply(rule a3) |
|
82 apply(simp add: eqvts fresh_star_def) |
|
83 apply(drule_tac x="q + p" in meta_spec) |
|
84 apply(simp) |
|
85 sorry |
|
86 then have "P c (0 \<bullet> lm)" by blast |
|
87 then show "P c lm" by simp |
|
88 qed |
|
89 |
8 |
90 text {* example 1, equivalent to example 2 from Terms *} |
9 text {* example 1, equivalent to example 2 from Terms *} |
91 |
10 |
92 nominal_datatype lam = |
11 nominal_datatype lam = |
93 VAR "name" |
12 VAR "name" |