author  haftmann 
Sat, 05 Jul 2014 11:01:53 +0200  
changeset 57514  bdc2c6b40bf2 
parent 47124  960f0a4404c7 
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:
34990
diff
changeset

1 
(* Title: HOL/Proofs/Lambda/Eta.thy 
15522
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

2 
Author: Tobias Nipkow and Stefan Berghofer 
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

3 
Copyright 1995, 2005 TU Muenchen 
1269  4 
*) 
5 

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

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

7 

16417  8 
theory Eta imports ParRed begin 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

9 

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 
subsection {* Definition of etareduction and relatives *} 
1269  12 

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

14 
free :: "dB => nat => bool" 
25973  15 
where 
16 
"free (Var j) i = (j = i)" 

17 
 "free (s \<degree> t) i = (free s i \<or> free t i)" 

18 
 "free (Abs s) i = free s (i + 1)" 

1269  19 

25973  20 
inductive 
21 
eta :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<eta>" 50) 

22 
where 

22272  23 
eta [simp, intro]: "\<not> free s 0 ==> Abs (s \<degree> Var 0) \<rightarrow>\<^sub>\<eta> s[dummy/0]" 
24 
 appL [simp, intro]: "s \<rightarrow>\<^sub>\<eta> t ==> s \<degree> u \<rightarrow>\<^sub>\<eta> t \<degree> u" 

25 
 appR [simp, intro]: "s \<rightarrow>\<^sub>\<eta> t ==> u \<degree> s \<rightarrow>\<^sub>\<eta> u \<degree> t" 

26 
 abs [simp, intro]: "s \<rightarrow>\<^sub>\<eta> t ==> Abs s \<rightarrow>\<^sub>\<eta> Abs t" 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

27 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

28 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

29 
eta_reds :: "[dB, dB] => bool" (infixl "e>>" 50) where 
22272  30 
"s e>> t == eta^** s t" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

31 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

32 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

33 
eta_red0 :: "[dB, dB] => bool" (infixl "e>=" 50) where 
22272  34 
"s e>= t == eta^== s t" 
1269  35 

22272  36 
notation (xsymbols) 
37 
eta_reds (infixl "\<rightarrow>\<^sub>\<eta>\<^sup>*" 50) and 

38 
eta_red0 (infixl "\<rightarrow>\<^sub>\<eta>\<^sup>=" 50) 

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

39 

23750  40 
inductive_cases eta_cases [elim!]: 
22272  41 
"Abs s \<rightarrow>\<^sub>\<eta> z" 
42 
"s \<degree> t \<rightarrow>\<^sub>\<eta> u" 

43 
"Var i \<rightarrow>\<^sub>\<eta> t" 

9811
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 

25973  46 
subsection {* Properties of @{text "eta"}, @{text "subst"} and @{text "free"} *} 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

47 

18241  48 
lemma subst_not_free [simp]: "\<not> free s i \<Longrightarrow> s[t/i] = s[u/i]" 
20503  49 
by (induct s arbitrary: i t u) (simp_all add: subst_Var) 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

50 

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

51 
lemma free_lift [simp]: 
18241  52 
"free (lift t k) i = (i < k \<and> free t i \<or> k < i \<and> free t (i  1))" 
20503  53 
apply (induct t arbitrary: i k) 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19656
diff
changeset

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

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

56 

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

57 
lemma free_subst [simp]: 
18241  58 
"free (s[t/k]) i = 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

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

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

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

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

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

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

68 

22272  69 
lemma free_eta: "s \<rightarrow>\<^sub>\<eta> t ==> free t i = free s i" 
20503  70 
by (induct arbitrary: i set: eta) (simp_all cong: conj_cong) 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

71 

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

72 
lemma not_free_eta: 
22272  73 
"[ s \<rightarrow>\<^sub>\<eta> t; \<not> free s i ] ==> \<not> free t i" 
18241  74 
by (simp add: free_eta) 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

75 

18241  76 
lemma eta_subst [simp]: 
22272  77 
"s \<rightarrow>\<^sub>\<eta> t ==> s[u/i] \<rightarrow>\<^sub>\<eta> t[u/i]" 
20503  78 
by (induct arbitrary: u i set: eta) (simp_all add: subst_subst [symmetric]) 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

79 

18241  80 
theorem lift_subst_dummy: "\<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s" 
20503  81 
by (induct s arbitrary: i dummy) simp_all 
15522
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

82 

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

83 

25973  84 
subsection {* Confluence of @{text "eta"} *} 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

85 

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

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

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

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

90 
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

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

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

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

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

95 
done 
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 
theorem eta_confluent: "confluent eta" 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

100 

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

101 

25973  102 
subsection {* Congruence rules for @{text "eta\<^sup>*"} *} 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

103 

22272  104 
lemma rtrancl_eta_Abs: "s \<rightarrow>\<^sub>\<eta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<eta>\<^sup>* Abs s'" 
23750  105 
by (induct set: rtranclp) 
106 
(blast intro: rtranclp.rtrancl_into_rtrancl)+ 

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

107 

22272  108 
lemma rtrancl_eta_AppL: "s \<rightarrow>\<^sub>\<eta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<eta>\<^sup>* s' \<degree> t" 
23750  109 
by (induct set: rtranclp) 
110 
(blast intro: rtranclp.rtrancl_into_rtrancl)+ 

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

111 

22272  112 
lemma rtrancl_eta_AppR: "t \<rightarrow>\<^sub>\<eta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<eta>\<^sup>* s \<degree> t'" 
23750  113 
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+ 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

114 

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

115 
lemma rtrancl_eta_App: 
22272  116 
"[ s \<rightarrow>\<^sub>\<eta>\<^sup>* s'; t \<rightarrow>\<^sub>\<eta>\<^sup>* t' ] ==> s \<degree> t \<rightarrow>\<^sub>\<eta>\<^sup>* s' \<degree> t'" 
23750  117 
by (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtranclp_trans) 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

118 

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

119 

25973  120 
subsection {* Commutation of @{text "beta"} and @{text "eta"} *} 
1900  121 

18241  122 
lemma free_beta: 
22272  123 
"s \<rightarrow>\<^sub>\<beta> t ==> free t i \<Longrightarrow> free s i" 
20503  124 
by (induct arbitrary: i set: beta) auto 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

125 

22272  126 
lemma beta_subst [intro]: "s \<rightarrow>\<^sub>\<beta> t ==> s[u/i] \<rightarrow>\<^sub>\<beta> t[u/i]" 
20503  127 
by (induct arbitrary: u i set: beta) (simp_all add: subst_subst [symmetric]) 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

128 

18241  129 
lemma subst_Var_Suc [simp]: "t[Var i/i] = t[Var(i)/i + 1]" 
20503  130 
by (induct t arbitrary: i) (auto elim!: linorder_neqE simp: subst_Var) 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

131 

22272  132 
lemma eta_lift [simp]: "s \<rightarrow>\<^sub>\<eta> t ==> lift s i \<rightarrow>\<^sub>\<eta> lift t i" 
20503  133 
by (induct arbitrary: i set: eta) simp_all 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

134 

22272  135 
lemma rtrancl_eta_subst: "s \<rightarrow>\<^sub>\<eta> t \<Longrightarrow> u[s/i] \<rightarrow>\<^sub>\<eta>\<^sup>* u[t/i]" 
20503  136 
apply (induct u arbitrary: s t i) 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

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

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

142 

22272  143 
lemma rtrancl_eta_subst': 
24231
85fb973a8207
added type constraints to resolve syntax ambiguities;
wenzelm
parents:
23750
diff
changeset

144 
fixes s t :: dB 
22272  145 
assumes eta: "s \<rightarrow>\<^sub>\<eta>\<^sup>* t" 
146 
shows "s[u/i] \<rightarrow>\<^sub>\<eta>\<^sup>* t[u/i]" using eta 

147 
by induct (iprover intro: eta_subst)+ 

148 

149 
lemma rtrancl_eta_subst'': 

24231
85fb973a8207
added type constraints to resolve syntax ambiguities;
wenzelm
parents:
23750
diff
changeset

150 
fixes s t :: dB 
22272  151 
assumes eta: "s \<rightarrow>\<^sub>\<eta>\<^sup>* t" 
152 
shows "u[s/i] \<rightarrow>\<^sub>\<eta>\<^sup>* u[t/i]" using eta 

23750  153 
by induct (iprover intro: rtrancl_eta_subst rtranclp_trans)+ 
22272  154 

155 
lemma square_beta_eta: "square beta eta (eta^**) (beta^==)" 

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

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

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

158 
apply (erule beta.induct) 
11183  159 
apply (slowsimp intro: rtrancl_eta_subst eta_subst) 
160 
apply (blast intro: rtrancl_eta_AppL) 

161 
apply (blast intro: rtrancl_eta_AppR) 

47124  162 
apply simp 
11183  163 
apply (slowsimp intro: rtrancl_eta_Abs free_beta 
9858  164 
iff del: dB.distinct simp: dB.distinct) (*23 seconds?*) 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

166 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22272
diff
changeset

167 
lemma confluent_beta_eta: "confluent (sup beta eta)" 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

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

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

172 

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

173 

25973  174 
subsection {* Implicit definition of @{text "eta"} *} 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

175 

22272  176 
text {* @{term "Abs (lift s 0 \<degree> Var 0) \<rightarrow>\<^sub>\<eta> s"} *} 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

177 

18241  178 
lemma not_free_iff_lifted: 
179 
"(\<not> free s i) = (\<exists>t. s = lift t i)" 

20503  180 
apply (induct s arbitrary: i) 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

202 
apply (rename_tac u1 u2) 
12011  203 
apply (rule_tac x = "u1 \<degree> u2" in exI) 
9811
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

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

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

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

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

210 
apply blast 
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 (erule thin_rl) 
39ffdb8cab03
HOL/Lambda: converted into newstyle theory and document;
wenzelm
parents:
9102
diff
changeset

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

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

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

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

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

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

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

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

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

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

226 

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

227 
theorem explicit_is_implicit: 
12011  228 
"(\<forall>s u. (\<not> free s 0) > R (Abs (s \<degree> Var 0)) (s[u/0])) = 
229 
(\<forall>s. R (Abs (lift s 0 \<degree> Var 0)) s)" 

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

231 

15522
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

232 

ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

233 
subsection {* Etapostponement theorem *} 
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

234 

ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

235 
text {* 
22272  236 
Based on a paper proof due to Andreas Abel. 
237 
Unlike the proof by Masako Takahashi \cite{TakahashiIandC}, it does not 

238 
use parallel eta reduction, which only seems to complicate matters unnecessarily. 

15522
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

239 
*} 
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

240 

22272  241 
theorem eta_case: 
24231
85fb973a8207
added type constraints to resolve syntax ambiguities;
wenzelm
parents:
23750
diff
changeset

242 
fixes s :: dB 
22272  243 
assumes free: "\<not> free s 0" 
244 
and s: "s[dummy/0] => u" 

245 
shows "\<exists>t'. Abs (s \<degree> Var 0) => t' \<and> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u" 

246 
proof  

247 
from s have "lift (s[dummy/0]) 0 => lift u 0" by (simp del: lift_subst) 

248 
with free have "s => lift u 0" by (simp add: lift_subst_dummy del: lift_subst) 

249 
hence "Abs (s \<degree> Var 0) => Abs (lift u 0 \<degree> Var 0)" by simp 

250 
moreover have "\<not> free (lift u 0) 0" by simp 

251 
hence "Abs (lift u 0 \<degree> Var 0) \<rightarrow>\<^sub>\<eta> lift u 0[dummy/0]" 

252 
by (rule eta.eta) 

253 
hence "Abs (lift u 0 \<degree> Var 0) \<rightarrow>\<^sub>\<eta>\<^sup>* u" by simp 

254 
ultimately show ?thesis by iprover 

15522
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

255 
qed 
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

256 

22272  257 
theorem eta_par_beta: 
258 
assumes st: "s \<rightarrow>\<^sub>\<eta> t" 

259 
and tu: "t => u" 

260 
shows "\<exists>t'. s => t' \<and> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u" using tu st 

261 
proof (induct arbitrary: s) 

262 
case (var n) 

263 
thus ?case by (iprover intro: par_beta_refl) 

264 
next 

265 
case (abs s' t) 

266 
note abs' = this 

267 
from `s \<rightarrow>\<^sub>\<eta> Abs s'` show ?case 

268 
proof cases 

269 
case (eta s'' dummy) 

270 
from abs have "Abs s' => Abs t" by simp 

271 
with eta have "s''[dummy/0] => Abs t" by simp 

272 
with `\<not> free s'' 0` have "\<exists>t'. Abs (s'' \<degree> Var 0) => t' \<and> t' \<rightarrow>\<^sub>\<eta>\<^sup>* Abs t" 

273 
by (rule eta_case) 

274 
with eta show ?thesis by simp 

275 
next 

34990  276 
case (abs r) 
277 
from `r \<rightarrow>\<^sub>\<eta> s'` 

278 
obtain t' where r: "r => t'" and t': "t' \<rightarrow>\<^sub>\<eta>\<^sup>* t" by (iprover dest: abs') 

22272  279 
from r have "Abs r => Abs t'" .. 
280 
moreover from t' have "Abs t' \<rightarrow>\<^sub>\<eta>\<^sup>* Abs t" by (rule rtrancl_eta_Abs) 

281 
ultimately show ?thesis using abs by simp iprover 

34990  282 
qed 
22272  283 
next 
284 
case (app u u' t t') 

285 
from `s \<rightarrow>\<^sub>\<eta> u \<degree> t` show ?case 

286 
proof cases 

287 
case (eta s' dummy) 

288 
from app have "u \<degree> t => u' \<degree> t'" by simp 

289 
with eta have "s'[dummy/0] => u' \<degree> t'" by simp 

290 
with `\<not> free s' 0` have "\<exists>r. Abs (s' \<degree> Var 0) => r \<and> r \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'" 

291 
by (rule eta_case) 

292 
with eta show ?thesis by simp 

293 
next 

34990  294 
case (appL s') 
295 
from `s' \<rightarrow>\<^sub>\<eta> u` 

296 
obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: app) 

22272  297 
from s' and app have "s' \<degree> t => r \<degree> t'" by simp 
298 
moreover from r have "r \<degree> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'" by (simp add: rtrancl_eta_AppL) 

299 
ultimately show ?thesis using appL by simp iprover 

300 
next 

34990  301 
case (appR s') 
302 
from `s' \<rightarrow>\<^sub>\<eta> t` 

303 
obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: app) 

22272  304 
from s' and app have "u \<degree> s' => u' \<degree> r" by simp 
305 
moreover from r have "u' \<degree> r \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'" by (simp add: rtrancl_eta_AppR) 

306 
ultimately show ?thesis using appR by simp iprover 

34990  307 
qed 
22272  308 
next 
309 
case (beta u u' t t') 

310 
from `s \<rightarrow>\<^sub>\<eta> Abs u \<degree> t` show ?case 

311 
proof cases 

312 
case (eta s' dummy) 

313 
from beta have "Abs u \<degree> t => u'[t'/0]" by simp 

314 
with eta have "s'[dummy/0] => u'[t'/0]" by simp 

315 
with `\<not> free s' 0` have "\<exists>r. Abs (s' \<degree> Var 0) => r \<and> r \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]" 

316 
by (rule eta_case) 

317 
with eta show ?thesis by simp 

318 
next 

34990  319 
case (appL s') 
320 
from `s' \<rightarrow>\<^sub>\<eta> Abs u` show ?thesis 

22272  321 
proof cases 
322 
case (eta s'' dummy) 

323 
have "Abs (lift u 1) = lift (Abs u) 0" by simp 

324 
also from eta have "\<dots> = s''" by (simp add: lift_subst_dummy del: lift_subst) 

325 
finally have s: "s = Abs (Abs (lift u 1) \<degree> Var 0) \<degree> t" using appL and eta by simp 

326 
from beta have "lift u 1 => lift u' 1" by simp 

327 
hence "Abs (lift u 1) \<degree> Var 0 => lift u' 1[Var 0/0]" 

25973  328 
using par_beta.var .. 
22272  329 
hence "Abs (Abs (lift u 1) \<degree> Var 0) \<degree> t => lift u' 1[Var 0/0][t'/0]" 
25973  330 
using `t => t'` .. 
22272  331 
with s have "s => u'[t'/0]" by simp 
332 
thus ?thesis by iprover 

333 
next 

34990  334 
case (abs r) 
335 
from `r \<rightarrow>\<^sub>\<eta> u` 

336 
obtain r'' where r: "r => r''" and r'': "r'' \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: beta) 

22272  337 
from r and beta have "Abs r \<degree> t => r''[t'/0]" by simp 
338 
moreover from r'' have "r''[t'/0] \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]" 

25973  339 
by (rule rtrancl_eta_subst') 
22272  340 
ultimately show ?thesis using abs and appL by simp iprover 
34990  341 
qed 
22272  342 
next 
34990  343 
case (appR s') 
344 
from `s' \<rightarrow>\<^sub>\<eta> t` 

345 
obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: beta) 

22272  346 
from s' and beta have "Abs u \<degree> s' => u'[r/0]" by simp 
347 
moreover from r have "u'[r/0] \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]" 

348 
by (rule rtrancl_eta_subst'') 

349 
ultimately show ?thesis using appR by simp iprover 

34990  350 
qed 
22272  351 
qed 
352 

353 
theorem eta_postponement': 

354 
assumes eta: "s \<rightarrow>\<^sub>\<eta>\<^sup>* t" and beta: "t => u" 

355 
shows "\<exists>t'. s => t' \<and> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u" using eta beta 

20503  356 
proof (induct arbitrary: u) 
26181
fedc257417fc
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
25973
diff
changeset

357 
case base 
15522
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

358 
thus ?case by blast 
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

359 
next 
26181
fedc257417fc
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
25973
diff
changeset

360 
case (step s' s'' s''') 
fedc257417fc
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
25973
diff
changeset

361 
then obtain t' where s': "s' => t'" and t': "t' \<rightarrow>\<^sub>\<eta>\<^sup>* s'''" 
22272  362 
by (auto dest: eta_par_beta) 
26181
fedc257417fc
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
25973
diff
changeset

363 
from s' obtain t'' where s: "s => t''" and t'': "t'' \<rightarrow>\<^sub>\<eta>\<^sup>* t'" using step 
18557
60a0f9caa0a2
Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents:
18460
diff
changeset

364 
by blast 
23750  365 
from t'' and t' have "t'' \<rightarrow>\<^sub>\<eta>\<^sup>* s'''" by (rule rtranclp_trans) 
17589  366 
with s show ?case by iprover 
15522
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

367 
qed 
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

368 

ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

369 
theorem eta_postponement: 
26181
fedc257417fc
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
25973
diff
changeset

370 
assumes "(sup beta eta)\<^sup>*\<^sup>* s t" 
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
26181
diff
changeset

371 
shows "(beta\<^sup>*\<^sup>* OO eta\<^sup>*\<^sup>*) s t" using assms 
15522
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

372 
proof induct 
26181
fedc257417fc
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
25973
diff
changeset

373 
case base 
15522
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

374 
show ?case by blast 
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

375 
next 
26181
fedc257417fc
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
25973
diff
changeset

376 
case (step s' s'') 
fedc257417fc
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
25973
diff
changeset

377 
from step(3) obtain t' where s: "s \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and t': "t' \<rightarrow>\<^sub>\<eta>\<^sup>* s'" by blast 
fedc257417fc
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
25973
diff
changeset

378 
from step(2) show ?case 
15522
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

379 
proof 
22272  380 
assume "s' \<rightarrow>\<^sub>\<beta> s''" 
15522
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

381 
with beta_subset_par_beta have "s' => s''" .. 
22272  382 
with t' obtain t'' where st: "t' => t''" and tu: "t'' \<rightarrow>\<^sub>\<eta>\<^sup>* s''" 
15522
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

383 
by (auto dest: eta_postponement') 
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

384 
from par_beta_subset_beta st have "t' \<rightarrow>\<^sub>\<beta>\<^sup>* t''" .. 
23750  385 
with s have "s \<rightarrow>\<^sub>\<beta>\<^sup>* t''" by (rule rtranclp_trans) 
15522
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

386 
thus ?thesis using tu .. 
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

387 
next 
22272  388 
assume "s' \<rightarrow>\<^sub>\<eta> s''" 
389 
with t' have "t' \<rightarrow>\<^sub>\<eta>\<^sup>* s''" .. 

15522
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

390 
with s show ?thesis .. 
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

391 
qed 
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

392 
qed 
ec0fd05b2f2c
Added proof of etapostponement theorem (using parallel etareduction).
berghofe
parents:
13187
diff
changeset

393 

11638  394 
end 