| author | Christian Urban <urbanc@in.tum.de> |
| Fri, 09 Apr 2010 11:08:05 +0200 | |
| changeset 1797 | fddb470720f1 |
| parent 1773 | Nominal/Ex/ExLam.thy@c0eac04ae3b4 |
| child 1800 | 78fdc6b36a1c |
| permissions | -rw-r--r-- |
|
1797
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
1 |
theory Lambda |
|
1773
c0eac04ae3b4
added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
1599
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 |
||
|
1797
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
14 |
(* |
|
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
15 |
Old way of establishing strong induction |
|
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
16 |
principles by chosing a fresh name. |
|
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
17 |
*) |
| 1594 | 18 |
lemma |
19 |
fixes c::"'a::fs" |
|
20 |
assumes a1: "\<And>name c. P c (Vr name)" |
|
21 |
and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)" |
|
22 |
and a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)" |
|
23 |
shows "P c lm" |
|
24 |
proof - |
|
25 |
have "\<And>p. P c (p \<bullet> lm)" |
|
26 |
apply(induct lm arbitrary: c rule: lm.induct) |
|
27 |
apply(simp only: lm.perm) |
|
28 |
apply(rule a1) |
|
29 |
apply(simp only: lm.perm) |
|
30 |
apply(rule a2) |
|
|
1797
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
31 |
apply(assumption) |
| 1594 | 32 |
apply(assumption) |
33 |
apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))") |
|
34 |
defer |
|
35 |
apply(simp add: fresh_def) |
|
36 |
apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base) |
|
37 |
apply(simp add: supp_Pair finite_supp) |
|
38 |
apply(blast) |
|
39 |
apply(erule exE) |
|
40 |
apply(rule_tac t="p \<bullet> Lm name lm" and |
|
41 |
s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst) |
|
42 |
apply(simp del: lm.perm) |
|
43 |
apply(subst lm.perm) |
|
44 |
apply(subst (2) lm.perm) |
|
45 |
apply(rule flip_fresh_fresh) |
|
46 |
apply(simp add: fresh_def) |
|
47 |
apply(simp only: supp_fn') |
|
48 |
apply(simp) |
|
49 |
apply(simp add: fresh_Pair) |
|
50 |
apply(simp) |
|
51 |
apply(rule a3) |
|
52 |
apply(simp add: fresh_Pair) |
|
53 |
apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec) |
|
54 |
apply(simp) |
|
55 |
done |
|
56 |
then have "P c (0 \<bullet> lm)" by blast |
|
57 |
then show "P c lm" by simp |
|
58 |
qed |
|
59 |
||
|
1797
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
60 |
(* |
|
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
61 |
New way of establishing strong induction |
|
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
62 |
principles by using a appropriate permutation. |
|
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
63 |
*) |
| 1594 | 64 |
lemma |
65 |
fixes c::"'a::fs" |
|
66 |
assumes a1: "\<And>name c. P c (Vr name)" |
|
67 |
and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)" |
|
68 |
and a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)" |
|
69 |
shows "P c lm" |
|
70 |
proof - |
|
71 |
have "\<And>p. P c (p \<bullet> lm)" |
|
72 |
apply(induct lm arbitrary: c rule: lm.induct) |
|
73 |
apply(simp only: lm.perm) |
|
74 |
apply(rule a1) |
|
75 |
apply(simp only: lm.perm) |
|
76 |
apply(rule a2) |
|
77 |
apply(assumption) |
|
|
1797
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
78 |
apply(assumption) |
| 1594 | 79 |
apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lm name lm) \<sharp>* q")
|
80 |
apply(erule exE) |
|
81 |
apply(rule_tac t="p \<bullet> Lm name lm" and |
|
82 |
s="q \<bullet> p \<bullet> Lm name lm" in subst) |
|
83 |
defer |
|
84 |
apply(simp add: lm.perm) |
|
85 |
apply(rule a3) |
|
86 |
apply(simp add: eqvts fresh_star_def) |
|
87 |
apply(drule_tac x="q + p" in meta_spec) |
|
88 |
apply(simp) |
|
|
1797
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
89 |
apply(rule at_set_avoiding2) |
|
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
90 |
apply(simp add: finite_supp) |
|
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
91 |
apply(simp add: finite_supp) |
|
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
92 |
apply(simp add: finite_supp) |
|
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
93 |
apply(simp only: lm.perm atom_eqvt) |
|
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
94 |
apply(simp add: fresh_star_def fresh_def supp_fn') |
|
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
95 |
apply(rule supp_perm_eq) |
|
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
96 |
apply(simp) |
|
fddb470720f1
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
Christian Urban <urbanc@in.tum.de>
parents:
1773
diff
changeset
|
97 |
done |
| 1594 | 98 |
then have "P c (0 \<bullet> lm)" by blast |
99 |
then show "P c lm" by simp |
|
100 |
qed |
|
101 |
||
102 |
end |
|
103 |
||
104 |
||
105 |