| author | Christian Urban <urbanc@in.tum.de> |
| Thu, 25 Mar 2010 09:08:42 +0100 | |
| changeset 1639 | a98d03fb9d53 |
| parent 1599 | 8b5a1ad60487 |
| permissions | -rw-r--r-- |
|
1599
8b5a1ad60487
Move Leroy out of Test, rename accordingly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1594
diff
changeset
|
1 |
theory ExLam |
|
8b5a1ad60487
Move Leroy out of Test, rename accordingly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1594
diff
changeset
|
2 |
imports "Parser" |
| 1594 | 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 |