author  wenzelm 
Mon, 04 Sep 2000 11:21:24 +0200  
changeset 9827  ce6e22ff89c3 
parent 9811  39ffdb8cab03 
child 9858  c3ac6128b649 
permissions  rwrr 
1269  1 
(* Title: HOL/Lambda/Eta.thy 
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:
9102
diff
changeset

7 
header {* Etareduction *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

8 

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

9 
theory Eta = ParRed: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

10 

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

11 

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

12 
subsection {* Definition of etareduction and relatives *} 
1269  13 

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

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

15 
free :: "dB => nat => bool" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

17 
"free (Var j) i = (j = i)" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

18 
"free (s $ t) i = (free s i \<or> free t i)" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

19 
"free (Abs s) i = free s (i + 1)" 
1269  20 

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

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

22 
eta :: "(dB \<times> dB) set" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

23 

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

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

25 
"_eta" :: "[dB, dB] => bool" (infixl "e>" 50) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

26 
"_eta_rtrancl" :: "[dB, dB] => bool" (infixl "e>>" 50) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

27 
"_eta_reflcl" :: "[dB, dB] => bool" (infixl "e>=" 50) 
1269  28 
translations 
9827  29 
"s e> t" == "(s, t) \<in> eta" 
30 
"s e>> t" == "(s, t) \<in> eta^*" 

31 
"s e>= t" == "(s, t) \<in> eta^=" 

1269  32 

1789  33 
inductive eta 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

35 
eta: "\<not> free s 0 ==> Abs (s $ Var 0) e> s[dummy/0]" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

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

39 

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

40 
inductive_cases eta_cases [elim!]: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

41 
"Abs s e> z" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

44 

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

45 

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

46 
subsection "Properties of eta, subst and free" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

47 

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

48 
lemma subst_not_free [rulify, simp]: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

49 
"\<forall>i t u. \<not> free s i > s[t/i] = s[u/i]" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

50 
apply (induct_tac s) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

53 

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

54 
lemma free_lift [simp]: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

55 
"\<forall>i k. free (lift t k) i = 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

56 
(i < k \<and> free t i \<or> k < i \<and> free t (i  1))" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

58 
apply (auto cong: conj_cong) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

59 
apply arith 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

61 

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

62 
lemma free_subst [simp]: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

64 
(free s k \<and> free t i \<or> free s (if i < k then i else i + 1))" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

65 
apply (induct_tac s) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

66 
prefer 2 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

68 
apply blast 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

69 
prefer 2 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

71 
apply (simp add: diff_Suc subst_Var split: nat.split) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

72 
apply clarify 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

73 
apply (erule linorder_neqE) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

76 

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

77 
lemma free_eta [rulify]: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

78 
"s e> t ==> \<forall>i. free t i = free s i" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

79 
apply (erule eta.induct) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

80 
apply (simp_all cong: conj_cong) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

82 

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

83 
lemma not_free_eta: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

84 
"[ s e> t; \<not> free s i ] ==> \<not> free t i" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

85 
apply (simp add: free_eta) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

87 

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

88 
lemma eta_subst [rulify, simp]: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

89 
"s e> t ==> \<forall>u i. s[u/i] e> t[u/i]" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

90 
apply (erule eta.induct) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

93 

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

94 

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

95 
subsection "Confluence of eta" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

96 

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

97 
lemma square_eta: "square eta eta (eta^=) (eta^=)" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

98 
apply (unfold square_def id_def) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

99 
apply (rule impI [THEN allI [THEN allI]]) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

101 
apply (erule eta.induct) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

102 
apply (slowsimp intro: subst_not_free eta_subst free_eta [THEN iffD1]) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

103 
apply safe 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

104 
prefer 5 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

105 
apply (blast intro!: eta_subst intro: free_eta [THEN iffD1]) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

106 
apply blast+ 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

108 

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

109 
theorem eta_confluent: "confluent eta" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

110 
apply (rule square_eta [THEN square_reflcl_confluent]) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

112 

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

113 

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

114 
subsection "Congruence rules for eta*" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

115 

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

116 
lemma rtrancl_eta_Abs: "s e>> s' ==> Abs s e>> Abs s'" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

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

120 

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

121 
lemma rtrancl_eta_AppL: "s e>> s' ==> s $ t e>> s' $ t" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

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

125 

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

126 
lemma rtrancl_eta_AppR: "t e>> t' ==> s $ t e>> s $ t'" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

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

130 

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

131 
lemma rtrancl_eta_App: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

133 
apply (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

135 

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

136 

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

137 
subsection "Commutation of beta and eta" 
1900  138 

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

139 
lemma free_beta [rulify]: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

140 
"s > t ==> \<forall>i. free t i > free s i" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

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

144 

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

145 
lemma beta_subst [rulify, intro]: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

146 
"s > t ==> \<forall>u i. s[u/i] > t[u/i]" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

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

150 

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

151 
lemma subst_Var_Suc [simp]: "\<forall>i. t[Var i/i] = t[Var(i)/i + 1]" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

153 
apply (auto elim!: linorder_neqE simp: subst_Var) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

155 

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

156 
lemma eta_lift [rulify, simp]: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

157 
"s e> t ==> \<forall>i. lift s i e> lift t i" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

158 
apply (erule eta.induct) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

161 

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

162 
lemma rtrancl_eta_subst [rulify]: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

163 
"\<forall>s t i. s e> t > u[s/i] e>> u[t/i]" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

164 
apply (induct_tac u) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

166 
apply (blast intro: r_into_rtrancl) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

167 
apply (blast intro: rtrancl_eta_App) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

168 
apply (blast intro!: rtrancl_eta_Abs eta_lift) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

170 

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

171 
lemma square_beta_eta: "square beta eta (eta^*) (beta^=)" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

172 
apply (unfold square_def) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

173 
apply (rule impI [THEN allI [THEN allI]]) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

175 
apply (slowsimp intro: r_into_rtrancl rtrancl_eta_subst eta_subst) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

176 
apply (blast intro: r_into_rtrancl rtrancl_eta_AppL) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

177 
apply (blast intro: r_into_rtrancl rtrancl_eta_AppR) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

178 
apply (slowsimp intro: r_into_rtrancl rtrancl_eta_Abs free_beta 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

179 
other: dB.distinct [iff del, simp]) (*23 seconds?*) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

181 

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

182 
lemma confluent_beta_eta: "confluent (beta \<union> eta)" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

183 
apply (assumption  
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

184 
rule square_rtrancl_reflcl_commute confluent_Un 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

185 
beta_confluent eta_confluent square_beta_eta)+ 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

187 

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

188 

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

189 
subsection "Implicit definition of eta" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

190 

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

191 
text {* @{term "Abs (lift s 0 $ Var 0) e> s"} *} 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

192 

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

193 
lemma not_free_iff_lifted [rulify]: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

194 
"\<forall>i. (\<not> free s i) = (\<exists>t. s = lift t i)" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

195 
apply (induct_tac s) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

197 
apply clarify 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

198 
apply (rule iffI) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

199 
apply (erule linorder_neqE) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

200 
apply (rule_tac x = "Var nat" in exI) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

202 
apply (rule_tac x = "Var (nat  1)" in exI) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

204 
apply clarify 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

205 
apply (rule notE) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

206 
prefer 2 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

207 
apply assumption 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

208 
apply (erule thin_rl) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

209 
apply (case_tac t) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

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

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

214 
apply (erule thin_rl) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

215 
apply (erule thin_rl) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

216 
apply (rule allI) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

217 
apply (rule iffI) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

218 
apply (elim conjE exE) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

219 
apply (rename_tac u1 u2) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

220 
apply (rule_tac x = "u1 $ u2" in exI) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

222 
apply (erule exE) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

223 
apply (erule rev_mp) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

224 
apply (case_tac t) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

227 
apply blast 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

230 
apply (erule thin_rl) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

231 
apply (rule allI) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

232 
apply (rule iffI) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

233 
apply (erule exE) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

234 
apply (rule_tac x = "Abs t" in exI) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

236 
apply (erule exE) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

237 
apply (erule rev_mp) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

238 
apply (case_tac t) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

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

242 
apply blast 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

244 

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

245 
theorem explicit_is_implicit: 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

246 
"(\<forall>s u. (\<not> free s 0) > R (Abs (s $ Var 0)) (s[u/0])) = 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

247 
(\<forall>s. R (Abs (lift s 0 $ Var 0)) s)" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

248 
apply (auto simp add: not_free_iff_lifted) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

250 

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

251 
end 