author  kuncar 
Wed, 04 Apr 2012 17:51:12 +0200  
changeset 47361  87c0eaf04bad 
parent 47354  95846613e414 
child 47369  f483be2fecb9 
permissions  rwrr 
47308  1 
(* Title: HOL/Lifting.thy 
2 
Author: Brian Huffman and Ondrej Kuncar 

3 
Author: Cezary Kaliszyk and Christian Urban 

4 
*) 

5 

6 
header {* Lifting package *} 

7 

8 
theory Lifting 

47325  9 
imports Plain Equiv_Relations Transfer 
47308  10 
keywords 
11 
"print_quotmaps" "print_quotients" :: diag and 

12 
"lift_definition" :: thy_goal and 

13 
"setup_lifting" :: thy_decl 

14 
uses 

15 
("Tools/Lifting/lifting_info.ML") 

16 
("Tools/Lifting/lifting_term.ML") 

17 
("Tools/Lifting/lifting_def.ML") 

18 
("Tools/Lifting/lifting_setup.ML") 

19 
begin 

20 

47325  21 
subsection {* Function map *} 
47308  22 

23 
notation map_fun (infixr ">" 55) 

24 

25 
lemma map_fun_id: 

26 
"(id > id) = id" 

27 
by (simp add: fun_eq_iff) 

28 

29 
subsection {* Quotient Predicate *} 

30 

31 
definition 

32 
"Quotient R Abs Rep T \<longleftrightarrow> 

33 
(\<forall>a. Abs (Rep a) = a) \<and> 

34 
(\<forall>a. R (Rep a) (Rep a)) \<and> 

35 
(\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s) \<and> 

36 
T = (\<lambda>x y. R x x \<and> Abs x = y)" 

37 

38 
lemma QuotientI: 

39 
assumes "\<And>a. Abs (Rep a) = a" 

40 
and "\<And>a. R (Rep a) (Rep a)" 

41 
and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s" 

42 
and "T = (\<lambda>x y. R x x \<and> Abs x = y)" 

43 
shows "Quotient R Abs Rep T" 

44 
using assms unfolding Quotient_def by blast 

45 

46 
lemma Quotient_abs_rep: 

47 
assumes a: "Quotient R Abs Rep T" 

48 
shows "Abs (Rep a) = a" 

49 
using a 

50 
unfolding Quotient_def 

51 
by simp 

52 

53 
lemma Quotient_rep_reflp: 

54 
assumes a: "Quotient R Abs Rep T" 

55 
shows "R (Rep a) (Rep a)" 

56 
using a 

57 
unfolding Quotient_def 

58 
by blast 

59 

60 
lemma Quotient_rel: 

61 
assumes a: "Quotient R Abs Rep T" 

62 
shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s"  {* orientation does not loop on rewriting *} 

63 
using a 

64 
unfolding Quotient_def 

65 
by blast 

66 

67 
lemma Quotient_cr_rel: 

68 
assumes a: "Quotient R Abs Rep T" 

69 
shows "T = (\<lambda>x y. R x x \<and> Abs x = y)" 

70 
using a 

71 
unfolding Quotient_def 

72 
by blast 

73 

74 
lemma Quotient_refl1: 

75 
assumes a: "Quotient R Abs Rep T" 

76 
shows "R r s \<Longrightarrow> R r r" 

77 
using a unfolding Quotient_def 

78 
by fast 

79 

80 
lemma Quotient_refl2: 

81 
assumes a: "Quotient R Abs Rep T" 

82 
shows "R r s \<Longrightarrow> R s s" 

83 
using a unfolding Quotient_def 

84 
by fast 

85 

86 
lemma Quotient_rel_rep: 

87 
assumes a: "Quotient R Abs Rep T" 

88 
shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b" 

89 
using a 

90 
unfolding Quotient_def 

91 
by metis 

92 

93 
lemma Quotient_rep_abs: 

94 
assumes a: "Quotient R Abs Rep T" 

95 
shows "R r r \<Longrightarrow> R (Rep (Abs r)) r" 

96 
using a unfolding Quotient_def 

97 
by blast 

98 

99 
lemma Quotient_rel_abs: 

100 
assumes a: "Quotient R Abs Rep T" 

101 
shows "R r s \<Longrightarrow> Abs r = Abs s" 

102 
using a unfolding Quotient_def 

103 
by blast 

104 

105 
lemma Quotient_symp: 

106 
assumes a: "Quotient R Abs Rep T" 

107 
shows "symp R" 

108 
using a unfolding Quotient_def using sympI by (metis (full_types)) 

109 

110 
lemma Quotient_transp: 

111 
assumes a: "Quotient R Abs Rep T" 

112 
shows "transp R" 

113 
using a unfolding Quotient_def using transpI by (metis (full_types)) 

114 

115 
lemma Quotient_part_equivp: 

116 
assumes a: "Quotient R Abs Rep T" 

117 
shows "part_equivp R" 

118 
by (metis Quotient_rep_reflp Quotient_symp Quotient_transp a part_equivpI) 

119 

120 
lemma identity_quotient: "Quotient (op =) id id (op =)" 

121 
unfolding Quotient_def by simp 

122 

123 
lemma Quotient_alt_def: 

124 
"Quotient R Abs Rep T \<longleftrightarrow> 

125 
(\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> 

126 
(\<forall>b. T (Rep b) b) \<and> 

127 
(\<forall>x y. R x y \<longleftrightarrow> T x (Abs x) \<and> T y (Abs y) \<and> Abs x = Abs y)" 

128 
apply safe 

129 
apply (simp (no_asm_use) only: Quotient_def, fast) 

130 
apply (simp (no_asm_use) only: Quotient_def, fast) 

131 
apply (simp (no_asm_use) only: Quotient_def, fast) 

132 
apply (simp (no_asm_use) only: Quotient_def, fast) 

133 
apply (simp (no_asm_use) only: Quotient_def, fast) 

134 
apply (simp (no_asm_use) only: Quotient_def, fast) 

135 
apply (rule QuotientI) 

136 
apply simp 

137 
apply metis 

138 
apply simp 

139 
apply (rule ext, rule ext, metis) 

140 
done 

141 

142 
lemma Quotient_alt_def2: 

143 
"Quotient R Abs Rep T \<longleftrightarrow> 

144 
(\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> 

145 
(\<forall>b. T (Rep b) b) \<and> 

146 
(\<forall>x y. R x y \<longleftrightarrow> T x (Abs y) \<and> T y (Abs x))" 

147 
unfolding Quotient_alt_def by (safe, metis+) 

148 

149 
lemma fun_quotient: 

150 
assumes 1: "Quotient R1 abs1 rep1 T1" 

151 
assumes 2: "Quotient R2 abs2 rep2 T2" 

152 
shows "Quotient (R1 ===> R2) (rep1 > abs2) (abs1 > rep2) (T1 ===> T2)" 

153 
using assms unfolding Quotient_alt_def2 

154 
unfolding fun_rel_def fun_eq_iff map_fun_apply 

155 
by (safe, metis+) 

156 

157 
lemma apply_rsp: 

158 
fixes f g::"'a \<Rightarrow> 'c" 

159 
assumes q: "Quotient R1 Abs1 Rep1 T1" 

160 
and a: "(R1 ===> R2) f g" "R1 x y" 

161 
shows "R2 (f x) (g y)" 

162 
using a by (auto elim: fun_relE) 

163 

164 
lemma apply_rsp': 

165 
assumes a: "(R1 ===> R2) f g" "R1 x y" 

166 
shows "R2 (f x) (g y)" 

167 
using a by (auto elim: fun_relE) 

168 

169 
lemma apply_rsp'': 

170 
assumes "Quotient R Abs Rep T" 

171 
and "(R ===> S) f f" 

172 
shows "S (f (Rep x)) (f (Rep x))" 

173 
proof  

174 
from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp) 

175 
then show ?thesis using assms(2) by (auto intro: apply_rsp') 

176 
qed 

177 

178 
subsection {* Quotient composition *} 

179 

180 
lemma Quotient_compose: 

181 
assumes 1: "Quotient R1 Abs1 Rep1 T1" 

182 
assumes 2: "Quotient R2 Abs2 Rep2 T2" 

183 
shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2) (T1 OO T2)" 

184 
proof  

185 
from 1 have Abs1: "\<And>a b. T1 a b \<Longrightarrow> Abs1 a = b" 

186 
unfolding Quotient_alt_def by simp 

187 
from 1 have Rep1: "\<And>b. T1 (Rep1 b) b" 

188 
unfolding Quotient_alt_def by simp 

189 
from 2 have Abs2: "\<And>a b. T2 a b \<Longrightarrow> Abs2 a = b" 

190 
unfolding Quotient_alt_def by simp 

191 
from 2 have Rep2: "\<And>b. T2 (Rep2 b) b" 

192 
unfolding Quotient_alt_def by simp 

193 
from 2 have R2: 

194 
"\<And>x y. R2 x y \<longleftrightarrow> T2 x (Abs2 x) \<and> T2 y (Abs2 y) \<and> Abs2 x = Abs2 y" 

195 
unfolding Quotient_alt_def by simp 

196 
show ?thesis 

197 
unfolding Quotient_alt_def 

198 
apply simp 

199 
apply safe 

200 
apply (drule Abs1, simp) 

201 
apply (erule Abs2) 

202 
apply (rule pred_compI) 

203 
apply (rule Rep1) 

204 
apply (rule Rep2) 

205 
apply (rule pred_compI, assumption) 

206 
apply (drule Abs1, simp) 

207 
apply (clarsimp simp add: R2) 

208 
apply (rule pred_compI, assumption) 

209 
apply (drule Abs1, simp)+ 

210 
apply (clarsimp simp add: R2) 

211 
apply (drule Abs1, simp)+ 

212 
apply (clarsimp simp add: R2) 

213 
apply (rule pred_compI, assumption) 

214 
apply (rule pred_compI [rotated]) 

215 
apply (erule conversepI) 

216 
apply (drule Abs1, simp)+ 

217 
apply (simp add: R2) 

218 
done 

219 
qed 

220 

221 
subsection {* Invariant *} 

222 

223 
definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 

224 
where "invariant R = (\<lambda>x y. R x \<and> x = y)" 

225 

226 
lemma invariant_to_eq: 

227 
assumes "invariant P x y" 

228 
shows "x = y" 

229 
using assms by (simp add: invariant_def) 

230 

231 
lemma fun_rel_eq_invariant: 

232 
shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))" 

233 
by (auto simp add: invariant_def fun_rel_def) 

234 

235 
lemma invariant_same_args: 

236 
shows "invariant P x x \<equiv> P x" 

237 
using assms by (auto simp add: invariant_def) 

238 

47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

239 
lemma UNIV_typedef_to_Quotient: 
47308  240 
assumes "type_definition Rep Abs UNIV" 
47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

241 
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" 
47308  242 
shows "Quotient (op =) Abs Rep T" 
243 
proof  

244 
interpret type_definition Rep Abs UNIV by fact 

47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

245 
from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

246 
by (fastforce intro!: QuotientI fun_eq_iff) 
47308  247 
qed 
248 

47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

249 
lemma UNIV_typedef_to_equivp: 
47308  250 
fixes Abs :: "'a \<Rightarrow> 'b" 
251 
and Rep :: "'b \<Rightarrow> 'a" 

252 
assumes "type_definition Rep Abs (UNIV::'a set)" 

253 
shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)" 

254 
by (rule identity_equivp) 

255 

47354  256 
lemma typedef_to_Quotient: 
47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

257 
assumes "type_definition Rep Abs S" 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

258 
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

259 
shows "Quotient (Lifting.invariant (\<lambda>x. x \<in> S)) Abs Rep T" 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

260 
proof  
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

261 
interpret type_definition Rep Abs S by fact 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

262 
from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

263 
by (auto intro!: QuotientI simp: invariant_def fun_eq_iff) 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

264 
qed 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

265 

87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

266 
lemma typedef_to_part_equivp: 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

267 
assumes "type_definition Rep Abs S" 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

268 
shows "part_equivp (Lifting.invariant (\<lambda>x. x \<in> S))" 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

269 
proof (intro part_equivpI) 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

270 
interpret type_definition Rep Abs S by fact 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

271 
show "\<exists>x. Lifting.invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def) 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

272 
next 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

273 
show "symp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def) 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

274 
next 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

275 
show "transp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def) 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

276 
qed 
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

277 

87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

278 
lemma open_typedef_to_Quotient: 
47354  279 
assumes "type_definition Rep Abs {x. P x}" 
280 
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" 

281 
shows "Quotient (invariant P) Abs Rep T" 

282 
proof  

283 
interpret type_definition Rep Abs "{x. P x}" by fact 

284 
from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis 

285 
by (auto intro!: QuotientI simp: invariant_def fun_eq_iff) 

286 
qed 

287 

47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

288 
lemma open_typedef_to_part_equivp: 
47308  289 
assumes "type_definition Rep Abs {x. P x}" 
290 
shows "part_equivp (invariant P)" 

291 
proof (intro part_equivpI) 

292 
interpret type_definition Rep Abs "{x. P x}" by fact 

293 
show "\<exists>x. invariant P x x" using Rep by (auto simp: invariant_def) 

294 
next 

295 
show "symp (invariant P)" by (auto intro: sympI simp: invariant_def) 

296 
next 

297 
show "transp (invariant P)" by (auto intro: transpI simp: invariant_def) 

298 
qed 

299 

47351  300 
lemma Quotient_to_transfer: 
301 
assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c" 

302 
shows "T c c'" 

303 
using assms by (auto dest: Quotient_cr_rel) 

304 

47308  305 
subsection {* ML setup *} 
306 

307 
text {* Auxiliary data for the lifting package *} 

308 

309 
use "Tools/Lifting/lifting_info.ML" 

310 
setup Lifting_Info.setup 

311 

312 
declare [[map "fun" = (fun_rel, fun_quotient)]] 

313 

314 
use "Tools/Lifting/lifting_term.ML" 

315 

316 
use "Tools/Lifting/lifting_def.ML" 

317 

318 
use "Tools/Lifting/lifting_setup.ML" 

319 

320 
hide_const (open) invariant 

321 

322 
end 