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