author  haftmann 
Sat, 05 Jul 2014 11:01:53 +0200  
changeset 57514  bdc2c6b40bf2 
parent 46512  4f9f61f9b535 
child 58273  9f0bfcd15097 
permissions  rwrr 
39157
b98909faaea8
more explicit HOLProofs 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

6 
header {* Basic definitions of Lambdacalculus *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

7 

16417  8 
theory Lambda imports Main begin 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

13 
subsection {* Lambdaterms in de Bruijn notation and substitution *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

14 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

15 
datatype dB = 
39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

18 
 Abs dB 
1120  19 

25974  20 
primrec 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

34 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

35 
declare subst_Var [simp del] 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

36 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

37 
text {* Optimized versions of @{term subst} and @{term lift}. *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

38 

25974  39 
primrec 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

45 

39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

54 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

55 
subsection {* Betareduction *} 
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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

75 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

76 
declare if_not_P [simp] not_less_eq [simp] 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

77 
 {* don't add @{text "r_into_rtrancl[intro!]"} *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

78 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

79 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

80 
subsection {* Congruence rules *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

81 

39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

85 

39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

89 

39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

93 

39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

97 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

98 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

99 
subsection {* Substitutionlemmas *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

100 

39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

103 

39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

106 

39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

113 

39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

118 

39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

122 

39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

131 
split: nat.split) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

132 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

133 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

134 
subsection {* Equivalence proof for optimized substitution *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle 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 newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

144 

39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

147 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

148 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

149 
subsection {* Preservation theorems *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

150 

39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

151 
text {* Not used in ChurchRosser proof, but in Strong 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

152 
Normalization. \medskip *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle 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 newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

179 
apply (simp add: rtrancl_beta_App) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

180 
apply (simp add: rtrancl_beta_Abs) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

181 
done 
39ffdb8cab03
HOL/Lambda: converted into newstyle 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 