author | wenzelm |
Fri, 17 Feb 2012 15:42:26 +0100 | |
changeset 46512 | 4f9f61f9b535 |
parent 46506 | c7faa011bfa7 |
child 58273 | 9f0bfcd15097 |
permissions | -rw-r--r-- |
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39126
diff
changeset
|
1 |
(* Title: HOL/Proofs/Lambda/Lambda.thy |
1120 | 2 |
Author: Tobias Nipkow |
3 |
Copyright 1995 TU Muenchen |
|
4 |
*) |
|
5 |
||
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
6 |
header {* Basic definitions of Lambda-calculus *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
7 |
|
16417 | 8 |
theory Lambda imports Main begin |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
9 |
|
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
10 |
declare [[syntax_ambiguity_warning = false]] |
39126
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
36862
diff
changeset
|
11 |
|
1120 | 12 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
13 |
subsection {* Lambda-terms in de Bruijn notation and substitution *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
14 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
15 |
datatype dB = |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
16 |
Var nat |
12011 | 17 |
| App dB dB (infixl "\<degree>" 200) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
18 |
| Abs dB |
1120 | 19 |
|
25974 | 20 |
primrec |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
21 |
lift :: "[dB, nat] => dB" |
25974 | 22 |
where |
23 |
"lift (Var i) k = (if i < k then Var i else Var (i + 1))" |
|
24 |
| "lift (s \<degree> t) k = lift s k \<degree> lift t k" |
|
25 |
| "lift (Abs s) k = Abs (lift s (k + 1))" |
|
1153 | 26 |
|
5184 | 27 |
primrec |
25974 | 28 |
subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300) |
29 |
where (* FIXME base names *) |
|
30 |
subst_Var: "(Var i)[s/k] = |
|
31 |
(if k < i then Var (i - 1) else if i = k then s else Var i)" |
|
32 |
| subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]" |
|
33 |
| subst_Abs: "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])" |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
34 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
35 |
declare subst_Var [simp del] |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
36 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
37 |
text {* Optimized versions of @{term subst} and @{term lift}. *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
38 |
|
25974 | 39 |
primrec |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
40 |
liftn :: "[nat, dB, nat] => dB" |
25974 | 41 |
where |
42 |
"liftn n (Var i) k = (if i < k then Var i else Var (i + n))" |
|
43 |
| "liftn n (s \<degree> t) k = liftn n s k \<degree> liftn n t k" |
|
44 |
| "liftn n (Abs s) k = Abs (liftn n s (k + 1))" |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
45 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
46 |
primrec |
25974 | 47 |
substn :: "[dB, dB, nat] => dB" |
48 |
where |
|
49 |
"substn (Var i) s k = |
|
50 |
(if k < i then Var (i - 1) else if i = k then liftn k s 0 else Var i)" |
|
51 |
| "substn (t \<degree> u) s k = substn t s k \<degree> substn u s k" |
|
52 |
| "substn (Abs t) s k = Abs (substn t s (k + 1))" |
|
1120 | 53 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
54 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
55 |
subsection {* Beta-reduction *} |
1153 | 56 |
|
23750 | 57 |
inductive beta :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50) |
22271 | 58 |
where |
59 |
beta [simp, intro!]: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]" |
|
60 |
| appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u" |
|
61 |
| appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t" |
|
62 |
| abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs s \<rightarrow>\<^sub>\<beta> Abs t" |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
63 |
|
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
64 |
abbreviation |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset
|
65 |
beta_reds :: "[dB, dB] => bool" (infixl "->>" 50) where |
22271 | 66 |
"s ->> t == beta^** s t" |
19086 | 67 |
|
21210 | 68 |
notation (latex) |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset
|
69 |
beta_reds (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50) |
1120 | 70 |
|
23750 | 71 |
inductive_cases beta_cases [elim!]: |
14065 | 72 |
"Var i \<rightarrow>\<^sub>\<beta> t" |
73 |
"Abs r \<rightarrow>\<^sub>\<beta> s" |
|
74 |
"s \<degree> t \<rightarrow>\<^sub>\<beta> u" |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
75 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
76 |
declare if_not_P [simp] not_less_eq [simp] |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
77 |
-- {* don't add @{text "r_into_rtrancl[intro!]"} *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
78 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
79 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
80 |
subsection {* Congruence rules *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
81 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
82 |
lemma rtrancl_beta_Abs [intro!]: |
14065 | 83 |
"s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<beta>\<^sup>* Abs s'" |
23750 | 84 |
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+ |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
85 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
86 |
lemma rtrancl_beta_AppL: |
14065 | 87 |
"s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t" |
23750 | 88 |
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+ |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
89 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
90 |
lemma rtrancl_beta_AppR: |
14065 | 91 |
"t \<rightarrow>\<^sub>\<beta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree> t'" |
23750 | 92 |
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+ |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
93 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
94 |
lemma rtrancl_beta_App [intro]: |
14065 | 95 |
"[| s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'" |
23750 | 96 |
by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtranclp_trans) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
97 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
98 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
99 |
subsection {* Substitution-lemmas *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
100 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
101 |
lemma subst_eq [simp]: "(Var k)[u/k] = u" |
18241 | 102 |
by (simp add: subst_Var) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
103 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
104 |
lemma subst_gt [simp]: "i < j ==> (Var j)[u/i] = Var (j - 1)" |
18241 | 105 |
by (simp add: subst_Var) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
106 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
107 |
lemma subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j" |
18241 | 108 |
by (simp add: subst_Var) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
109 |
|
18241 | 110 |
lemma lift_lift: |
111 |
"i < k + 1 \<Longrightarrow> lift (lift t i) (Suc k) = lift (lift t k) i" |
|
20503 | 112 |
by (induct t arbitrary: i k) auto |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
113 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
114 |
lemma lift_subst [simp]: |
18241 | 115 |
"j < i + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]" |
20503 | 116 |
by (induct t arbitrary: i j s) |
18241 | 117 |
(simp_all add: diff_Suc subst_Var lift_lift split: nat.split) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
118 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
119 |
lemma lift_subst_lt: |
18241 | 120 |
"i < j + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]" |
20503 | 121 |
by (induct t arbitrary: i j s) (simp_all add: subst_Var lift_lift) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
122 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
123 |
lemma subst_lift [simp]: |
18241 | 124 |
"(lift t k)[s/k] = t" |
20503 | 125 |
by (induct t arbitrary: k s) simp_all |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
126 |
|
18241 | 127 |
lemma subst_subst: |
128 |
"i < j + 1 \<Longrightarrow> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]" |
|
20503 | 129 |
by (induct t arbitrary: i j u v) |
18241 | 130 |
(simp_all add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
131 |
split: nat.split) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
132 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
133 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
134 |
subsection {* Equivalence proof for optimized substitution *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
135 |
|
18241 | 136 |
lemma liftn_0 [simp]: "liftn 0 t k = t" |
20503 | 137 |
by (induct t arbitrary: k) (simp_all add: subst_Var) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
138 |
|
18241 | 139 |
lemma liftn_lift [simp]: "liftn (Suc n) t k = lift (liftn n t k) k" |
20503 | 140 |
by (induct t arbitrary: k) (simp_all add: subst_Var) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
141 |
|
18241 | 142 |
lemma substn_subst_n [simp]: "substn t s n = t[liftn n s 0 / n]" |
20503 | 143 |
by (induct t arbitrary: n) (simp_all add: subst_Var) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
144 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
145 |
theorem substn_subst_0: "substn t s 0 = t[s/0]" |
18241 | 146 |
by simp |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
147 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
148 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
149 |
subsection {* Preservation theorems *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
150 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
151 |
text {* Not used in Church-Rosser proof, but in Strong |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
152 |
Normalization. \medskip *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
153 |
|
13915
28ccb51bd2f3
Eliminated most occurrences of rule_format attribute.
berghofe
parents:
13187
diff
changeset
|
154 |
theorem subst_preserves_beta [simp]: |
18257 | 155 |
"r \<rightarrow>\<^sub>\<beta> s ==> r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i]" |
20503 | 156 |
by (induct arbitrary: t i set: beta) (simp_all add: subst_subst [symmetric]) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
157 |
|
14065 | 158 |
theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]" |
23750 | 159 |
apply (induct set: rtranclp) |
160 |
apply (rule rtranclp.rtrancl_refl) |
|
161 |
apply (erule rtranclp.rtrancl_into_rtrancl) |
|
14065 | 162 |
apply (erule subst_preserves_beta) |
163 |
done |
|
164 |
||
13915
28ccb51bd2f3
Eliminated most occurrences of rule_format attribute.
berghofe
parents:
13187
diff
changeset
|
165 |
theorem lift_preserves_beta [simp]: |
18257 | 166 |
"r \<rightarrow>\<^sub>\<beta> s ==> lift r i \<rightarrow>\<^sub>\<beta> lift s i" |
20503 | 167 |
by (induct arbitrary: i set: beta) auto |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
168 |
|
14065 | 169 |
theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i" |
23750 | 170 |
apply (induct set: rtranclp) |
171 |
apply (rule rtranclp.rtrancl_refl) |
|
172 |
apply (erule rtranclp.rtrancl_into_rtrancl) |
|
14065 | 173 |
apply (erule lift_preserves_beta) |
174 |
done |
|
175 |
||
18241 | 176 |
theorem subst_preserves_beta2 [simp]: "r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]" |
20503 | 177 |
apply (induct t arbitrary: r s i) |
23750 | 178 |
apply (simp add: subst_Var r_into_rtranclp) |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
179 |
apply (simp add: rtrancl_beta_App) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
180 |
apply (simp add: rtrancl_beta_Abs) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
181 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
182 |
|
14065 | 183 |
theorem subst_preserves_beta2': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]" |
23750 | 184 |
apply (induct set: rtranclp) |
185 |
apply (rule rtranclp.rtrancl_refl) |
|
186 |
apply (erule rtranclp_trans) |
|
14065 | 187 |
apply (erule subst_preserves_beta2) |
188 |
done |
|
189 |
||
11638 | 190 |
end |