author  wenzelm 
Mon, 04 Sep 2000 11:21:24 +0200  
changeset 9827  ce6e22ff89c3 
parent 9811  39ffdb8cab03 
child 9906  5c027cca6262 
permissions  rwrr 
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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

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

8 

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

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

10 

1120  11 

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

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

13 

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

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

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

16 
 App dB dB (infixl "$" 200) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

17 
 Abs dB 
1120  18 

19 
consts 

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

20 
subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

21 
lift :: "[dB, nat] => dB" 
1153  22 

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

25 
"lift (s $ t) k = lift s k $ lift t k" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

26 
"lift (Abs s) k = Abs (lift s (k + 1))" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

27 

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

28 
primrec (* FIXME base names *) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

29 
subst_Var: "(Var i)[s/k] = 
39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle 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 newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

33 

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

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

35 

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

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

37 

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

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

39 
substn :: "[dB, dB, nat] => dB" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

40 
liftn :: "[nat, dB, nat] => dB" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

41 

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

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

48 
"substn (Var i) s k = 
39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle 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 newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

53 

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

54 
subsection {* Betareduction *} 
1153  55 

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

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

57 
beta :: "(dB \<times> dB) set" 
1120  58 

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

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

60 
"_beta" :: "[dB, dB] => bool" (infixl ">" 50) 
39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

67 
intros [simp, intro!] 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

68 
beta: "Abs s $ t > s[t/0]" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

69 
appL: "s > t ==> s $ u > t $ u" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

70 
appR: "s > t ==> u $ s > u $ t" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

71 
abs: "s > t ==> Abs s > Abs t" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

72 

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

73 
inductive_cases beta_cases [elim!]: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

74 
"Var i > t" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

75 
"Abs r > s" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

76 
"s $ t > u" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

77 

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

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

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

80 

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

83 

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

84 
lemma rtrancl_beta_Abs [intro!]: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

85 
"s >> s' ==> Abs s >> Abs s'" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

86 
apply (erule rtrancl_induct) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

87 
apply (blast intro: rtrancl_into_rtrancl)+ 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

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

91 
"s >> s' ==> s $ t >> s' $ t" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

92 
apply (erule rtrancl_induct) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

93 
apply (blast intro: rtrancl_into_rtrancl)+ 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

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

95 

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

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

97 
"t >> t' ==> s $ t >> s $ t'" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

98 
apply (erule rtrancl_induct) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

99 
apply (blast intro: rtrancl_into_rtrancl)+ 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

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

101 

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

102 
lemma rtrancl_beta_App [intro]: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

103 
"[ s >> s'; t >> t' ] ==> s $ t >> s' $ t'" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

104 
apply (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

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

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

107 

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

108 

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

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

110 

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

111 
lemma subst_eq [simp]: "(Var k)[u/k] = u" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

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

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

114 

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

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

117 
done 
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 subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

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

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

125 
apply (induct_tac t) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

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

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

128 

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

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

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

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

134 

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

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

137 
apply (induct_tac t) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

138 
apply (simp_all add: subst_Var lift_lift) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

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

140 

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

141 
lemma subst_lift [simp]: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

142 
"\<forall>k s. (lift t k)[s/k] = t" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

143 
apply (induct_tac t) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

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

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

146 

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

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

149 
apply (induct_tac t) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

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

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

153 
apply (auto elim: nat_neqE) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

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

155 

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

156 

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

157 
subsection {* Equivalence proof for optimized substitution *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

158 

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

160 
apply (induct_tac t) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

161 
apply (simp_all add: subst_Var) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

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

163 

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

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

166 
apply (induct_tac t) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

167 
apply (simp_all add: subst_Var) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

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

169 

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

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

172 
apply (induct_tac t) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

173 
apply (simp_all add: subst_Var) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

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

175 

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

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

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

179 

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

180 

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

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

182 

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

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

184 
Normalization. \medskip *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

185 

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

186 
theorem subst_preserves_beta [rulify, simp]: 
39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

188 
apply (erule beta.induct) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

189 
apply (simp_all add: subst_subst [symmetric]) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

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

191 

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

192 
theorem lift_preserves_beta [rulify, simp]: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

193 
"r > s ==> \<forall>i. lift r i > lift s i" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

194 
apply (erule beta.induct) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

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

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

197 

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

198 
theorem subst_preserves_beta2 [rulify, simp]: 
39ffdb8cab03
HOL/Lambda: converted into newstyle 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 newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

200 
apply (induct_tac t) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
6453
diff
changeset

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

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

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

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

205 

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

206 
end 