author | wenzelm |
Thu, 07 Sep 2000 21:10:11 +0200 | |
changeset 9906 | 5c027cca6262 |
parent 9827 | ce6e22ff89c3 |
child 9941 | fe05af7ec816 |
permissions | -rw-r--r-- |
1269 | 1 |
(* Title: HOL/Lambda/Lambda.thy |
1120 | 2 |
ID: $Id$ |
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1995 TU Muenchen |
|
5 |
*) |
|
6 |
||
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
7 |
header {* Basic definitions of Lambda-calculus *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
8 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
9 |
theory Lambda = Main: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
10 |
|
1120 | 11 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
12 |
subsection {* Lambda-terms in de Bruijn notation and substitution *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
13 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
14 |
datatype dB = |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
15 |
Var nat |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
16 |
| App dB dB (infixl "$" 200) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
17 |
| Abs dB |
1120 | 18 |
|
19 |
consts |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
20 |
subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
21 |
lift :: "[dB, nat] => dB" |
1153 | 22 |
|
5184 | 23 |
primrec |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
24 |
"lift (Var i) k = (if i < k then Var i else Var (i + 1))" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
25 |
"lift (s $ t) k = lift s k $ lift t k" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
26 |
"lift (Abs s) k = Abs (lift s (k + 1))" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
27 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
28 |
primrec (* FIXME base names *) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
29 |
subst_Var: "(Var i)[s/k] = |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
30 |
(if k < i then Var (i - 1) else if i = k then s else Var i)" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
31 |
subst_App: "(t $ u)[s/k] = t[s/k] $ u[s/k]" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
32 |
subst_Abs: "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
33 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
34 |
declare subst_Var [simp del] |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
35 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
36 |
text {* Optimized versions of @{term subst} and @{term lift}. *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
37 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
38 |
consts |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
39 |
substn :: "[dB, dB, nat] => dB" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
40 |
liftn :: "[nat, dB, nat] => dB" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
41 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
42 |
primrec |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
43 |
"liftn n (Var i) k = (if i < k then Var i else Var (i + n))" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
44 |
"liftn n (s $ t) k = liftn n s k $ liftn n t k" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
45 |
"liftn n (Abs s) k = Abs (liftn n s (k + 1))" |
1120 | 46 |
|
5184 | 47 |
primrec |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
48 |
"substn (Var i) s k = |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
49 |
(if k < i then Var (i - 1) else if i = k then liftn k s 0 else Var i)" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
50 |
"substn (t $ u) s k = substn t s k $ substn u s k" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
51 |
"substn (Abs t) s k = Abs (substn t s (k + 1))" |
1120 | 52 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
53 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
54 |
subsection {* Beta-reduction *} |
1153 | 55 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
56 |
consts |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
57 |
beta :: "(dB \<times> dB) set" |
1120 | 58 |
|
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
59 |
syntax |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
60 |
"_beta" :: "[dB, dB] => bool" (infixl "->" 50) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
61 |
"_beta_rtrancl" :: "[dB, dB] => bool" (infixl "->>" 50) |
1120 | 62 |
translations |
9827 | 63 |
"s -> t" == "(s, t) \<in> beta" |
64 |
"s ->> t" == "(s, t) \<in> beta^*" |
|
1120 | 65 |
|
1789 | 66 |
inductive beta |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
67 |
intros [simp, intro!] |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
68 |
beta: "Abs s $ t -> s[t/0]" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
69 |
appL: "s -> t ==> s $ u -> t $ u" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
70 |
appR: "s -> t ==> u $ s -> u $ t" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
71 |
abs: "s -> t ==> Abs s -> Abs t" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
72 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
73 |
inductive_cases beta_cases [elim!]: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
74 |
"Var i -> t" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
75 |
"Abs r -> s" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
76 |
"s $ t -> u" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
77 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
78 |
declare if_not_P [simp] not_less_eq [simp] |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
79 |
-- {* don't add @{text "r_into_rtrancl[intro!]"} *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
80 |
|
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 |
subsection {* Congruence rules *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
83 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
84 |
lemma rtrancl_beta_Abs [intro!]: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
85 |
"s ->> s' ==> Abs s ->> Abs s'" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
86 |
apply (erule rtrancl_induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
87 |
apply (blast intro: rtrancl_into_rtrancl)+ |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
88 |
done |
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_AppL: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
91 |
"s ->> s' ==> s $ t ->> s' $ t" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
92 |
apply (erule rtrancl_induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
93 |
apply (blast intro: rtrancl_into_rtrancl)+ |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
94 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
95 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
96 |
lemma rtrancl_beta_AppR: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
97 |
"t ->> t' ==> s $ t ->> s $ t'" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
98 |
apply (erule rtrancl_induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
99 |
apply (blast intro: rtrancl_into_rtrancl)+ |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
100 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
101 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
102 |
lemma rtrancl_beta_App [intro]: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
103 |
"[| s ->> s'; t ->> t' |] ==> s $ t ->> s' $ t'" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
104 |
apply (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
105 |
intro: rtrancl_trans) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
106 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
107 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
108 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
109 |
subsection {* Substitution-lemmas *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
110 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
111 |
lemma subst_eq [simp]: "(Var k)[u/k] = u" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
112 |
apply (simp add: subst_Var) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
113 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
114 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
115 |
lemma subst_gt [simp]: "i < j ==> (Var j)[u/i] = Var (j - 1)" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
116 |
apply (simp add: subst_Var) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
117 |
done |
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 subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
120 |
apply (simp add: subst_Var) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
121 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
122 |
|
9906 | 123 |
lemma lift_lift [rulified]: |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
124 |
"\<forall>i k. i < k + 1 --> lift (lift t i) (Suc k) = lift (lift t k) i" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
125 |
apply (induct_tac t) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
126 |
apply auto |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
127 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
128 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
129 |
lemma lift_subst [simp]: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
130 |
"\<forall>i j s. j < i + 1 --> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
131 |
apply (induct_tac t) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
132 |
apply (simp_all add: diff_Suc subst_Var lift_lift split: nat.split) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
133 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
134 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
135 |
lemma lift_subst_lt: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
136 |
"\<forall>i j s. i < j + 1 --> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
137 |
apply (induct_tac t) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
138 |
apply (simp_all add: subst_Var lift_lift) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
139 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
140 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
141 |
lemma subst_lift [simp]: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
142 |
"\<forall>k s. (lift t k)[s/k] = t" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
143 |
apply (induct_tac t) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
144 |
apply simp_all |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
145 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
146 |
|
9906 | 147 |
lemma subst_subst [rulified]: |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
148 |
"\<forall>i j u v. i < j + 1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
149 |
apply (induct_tac t) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
150 |
apply (simp_all |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
151 |
add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
152 |
split: nat.split) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
153 |
apply (auto elim: nat_neqE) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
154 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
155 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
156 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
157 |
subsection {* Equivalence proof for optimized substitution *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
158 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
159 |
lemma liftn_0 [simp]: "\<forall>k. liftn 0 t k = t" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
160 |
apply (induct_tac t) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
161 |
apply (simp_all add: subst_Var) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
162 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
163 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
164 |
lemma liftn_lift [simp]: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
165 |
"\<forall>k. liftn (Suc n) t k = lift (liftn n t k) k" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
166 |
apply (induct_tac t) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
167 |
apply (simp_all add: subst_Var) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
168 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
169 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
170 |
lemma substn_subst_n [simp]: |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
171 |
"\<forall>n. substn t s n = t[liftn n s 0 / n]" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
172 |
apply (induct_tac t) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
173 |
apply (simp_all add: subst_Var) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
174 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
175 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
176 |
theorem substn_subst_0: "substn t s 0 = t[s/0]" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
177 |
apply simp |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
178 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
179 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
180 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
181 |
subsection {* Preservation theorems *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
182 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
183 |
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
|
184 |
Normalization. \medskip *} |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
185 |
|
9906 | 186 |
theorem subst_preserves_beta [rulified, simp]: |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
187 |
"r -> s ==> \<forall>t i. r[t/i] -> s[t/i]" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
188 |
apply (erule beta.induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
189 |
apply (simp_all add: subst_subst [symmetric]) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
190 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
191 |
|
9906 | 192 |
theorem lift_preserves_beta [rulified, simp]: |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
193 |
"r -> s ==> \<forall>i. lift r i -> lift s i" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
194 |
apply (erule beta.induct) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
195 |
apply auto |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
196 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
197 |
|
9906 | 198 |
theorem subst_preserves_beta2 [rulified, simp]: |
9811
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
199 |
"\<forall>r s i. r -> s --> t[r/i] ->> t[s/i]" |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
200 |
apply (induct_tac t) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
201 |
apply (simp add: subst_Var r_into_rtrancl) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
202 |
apply (simp add: rtrancl_beta_App) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
203 |
apply (simp add: rtrancl_beta_Abs) |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
204 |
done |
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
205 |
|
39ffdb8cab03
HOL/Lambda: converted into new-style theory and document;
wenzelm
parents:
6453
diff
changeset
|
206 |
end |