author  kuncar 
Mon, 23 Apr 2012 17:18:18 +0200  
changeset 47698  18202d3d5832 
parent 47652  1b722b100301 
child 47777  f29e7dcd7c40 
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 

47698  15 
("Tools/Lifting/lifting_util.ML") 
47308  16 
("Tools/Lifting/lifting_info.ML") 
17 
("Tools/Lifting/lifting_term.ML") 

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

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

20 
begin 

21 

47325  22 
subsection {* Function map *} 
47308  23 

24 
notation map_fun (infixr ">" 55) 

25 

26 
lemma map_fun_id: 

27 
"(id > id) = id" 

28 
by (simp add: fun_eq_iff) 

29 

30 
subsection {* Quotient Predicate *} 

31 

32 
definition 

33 
"Quotient R Abs Rep T \<longleftrightarrow> 

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

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

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

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

38 

39 
lemma QuotientI: 

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

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

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

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

44 
shows "Quotient R Abs Rep T" 

45 
using assms unfolding Quotient_def by blast 

46 

47536  47 
context 
48 
fixes R Abs Rep T 

47308  49 
assumes a: "Quotient R Abs Rep T" 
47536  50 
begin 
51 

52 
lemma Quotient_abs_rep: "Abs (Rep a) = a" 

53 
using a unfolding Quotient_def 

47308  54 
by simp 
55 

47536  56 
lemma Quotient_rep_reflp: "R (Rep a) (Rep a)" 
57 
using a unfolding Quotient_def 

47308  58 
by blast 
59 

60 
lemma Quotient_rel: 

47536  61 
"R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s"  {* orientation does not loop on rewriting *} 
62 
using a unfolding Quotient_def 

47308  63 
by blast 
64 

47536  65 
lemma Quotient_cr_rel: "T = (\<lambda>x y. R x x \<and> Abs x = y)" 
47308  66 
using a unfolding Quotient_def 
67 
by blast 

68 

47536  69 
lemma Quotient_refl1: "R r s \<Longrightarrow> R r r" 
70 
using a unfolding Quotient_def 

71 
by fast 

72 

73 
lemma Quotient_refl2: "R r s \<Longrightarrow> R s s" 

74 
using a unfolding Quotient_def 

75 
by fast 

76 

77 
lemma Quotient_rel_rep: "R (Rep a) (Rep b) \<longleftrightarrow> a = b" 

78 
using a unfolding Quotient_def 

79 
by metis 

80 

81 
lemma Quotient_rep_abs: "R r r \<Longrightarrow> R (Rep (Abs r)) r" 

47308  82 
using a unfolding Quotient_def 
83 
by blast 

84 

47536  85 
lemma Quotient_rel_abs: "R r s \<Longrightarrow> Abs r = Abs s" 
86 
using a unfolding Quotient_def 

87 
by blast 

88 

89 
lemma Quotient_symp: "symp R" 

47308  90 
using a unfolding Quotient_def using sympI by (metis (full_types)) 
91 

47536  92 
lemma Quotient_transp: "transp R" 
47308  93 
using a unfolding Quotient_def using transpI by (metis (full_types)) 
94 

47536  95 
lemma Quotient_part_equivp: "part_equivp R" 
96 
by (metis Quotient_rep_reflp Quotient_symp Quotient_transp part_equivpI) 

97 

98 
end 

47308  99 

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

101 
unfolding Quotient_def by simp 

102 

47652
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

103 
text {* TODO: Use one of these alternatives as the real definition. *} 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

104 

47308  105 
lemma Quotient_alt_def: 
106 
"Quotient R Abs Rep T \<longleftrightarrow> 

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

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

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

110 
apply safe 

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

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

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

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

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

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

117 
apply (rule QuotientI) 

118 
apply simp 

119 
apply metis 

120 
apply simp 

121 
apply (rule ext, rule ext, metis) 

122 
done 

123 

124 
lemma Quotient_alt_def2: 

125 
"Quotient R Abs Rep T \<longleftrightarrow> 

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

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

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

129 
unfolding Quotient_alt_def by (safe, metis+) 

130 

47652
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

131 
lemma Quotient_alt_def3: 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

132 
"Quotient R Abs Rep T \<longleftrightarrow> 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

133 
(\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

134 
(\<forall>x y. R x y \<longleftrightarrow> (\<exists>z. T x z \<and> T y z))" 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

135 
unfolding Quotient_alt_def2 by (safe, metis+) 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

136 

1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

137 
lemma Quotient_alt_def4: 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

138 
"Quotient R Abs Rep T \<longleftrightarrow> 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

139 
(\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> R = T OO conversep T" 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

140 
unfolding Quotient_alt_def3 fun_eq_iff by auto 
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

141 

47308  142 
lemma fun_quotient: 
143 
assumes 1: "Quotient R1 abs1 rep1 T1" 

144 
assumes 2: "Quotient R2 abs2 rep2 T2" 

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

146 
using assms unfolding Quotient_alt_def2 

147 
unfolding fun_rel_def fun_eq_iff map_fun_apply 

148 
by (safe, metis+) 

149 

150 
lemma apply_rsp: 

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

152 
assumes q: "Quotient R1 Abs1 Rep1 T1" 

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

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

155 
using a by (auto elim: fun_relE) 

156 

157 
lemma apply_rsp': 

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

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

160 
using a by (auto elim: fun_relE) 

161 

162 
lemma apply_rsp'': 

163 
assumes "Quotient R Abs Rep T" 

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

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

166 
proof  

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

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

169 
qed 

170 

171 
subsection {* Quotient composition *} 

172 

173 
lemma Quotient_compose: 

174 
assumes 1: "Quotient R1 Abs1 Rep1 T1" 

175 
assumes 2: "Quotient R2 Abs2 Rep2 T2" 

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

47652
1b722b100301
move alternative definition lemmas into Lifting.thy;
huffman
parents:
47651
diff
changeset

177 
using assms unfolding Quotient_alt_def4 by (auto intro!: ext) 
47308  178 

47521
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47501
diff
changeset

179 
lemma equivp_reflp2: 
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47501
diff
changeset

180 
"equivp R \<Longrightarrow> reflp R" 
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47501
diff
changeset

181 
by (erule equivpE) 
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47501
diff
changeset

182 

47544  183 
subsection {* Respects predicate *} 
184 

185 
definition Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set" 

186 
where "Respects R = {x. R x x}" 

187 

188 
lemma in_respects: "x \<in> Respects R \<longleftrightarrow> R x x" 

189 
unfolding Respects_def by simp 

190 

47308  191 
subsection {* Invariant *} 
192 

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

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

195 

196 
lemma invariant_to_eq: 

197 
assumes "invariant P x y" 

198 
shows "x = y" 

199 
using assms by (simp add: invariant_def) 

200 

201 
lemma fun_rel_eq_invariant: 

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

203 
by (auto simp add: invariant_def fun_rel_def) 

204 

205 
lemma invariant_same_args: 

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

207 
using assms by (auto simp add: invariant_def) 

208 

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

209 
lemma UNIV_typedef_to_Quotient: 
47308  210 
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

211 
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" 
47308  212 
shows "Quotient (op =) Abs Rep T" 
213 
proof  

214 
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

215 
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

216 
by (fastforce intro!: QuotientI fun_eq_iff) 
47308  217 
qed 
218 

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

219 
lemma UNIV_typedef_to_equivp: 
47308  220 
fixes Abs :: "'a \<Rightarrow> 'b" 
221 
and Rep :: "'b \<Rightarrow> 'a" 

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

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

224 
by (rule identity_equivp) 

225 

47354  226 
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

227 
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

228 
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" 
47501  229 
shows "Quotient (invariant (\<lambda>x. x \<in> S)) Abs Rep T" 
47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

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

231 
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

232 
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

233 
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

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

235 

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

236 
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

237 
assumes "type_definition Rep Abs S" 
47501  238 
shows "part_equivp (invariant (\<lambda>x. x \<in> S))" 
47361
87c0eaf04bad
support nonopen typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47354
diff
changeset

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

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

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

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

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

247 

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

248 
lemma open_typedef_to_Quotient: 
47308  249 
assumes "type_definition Rep Abs {x. P x}" 
47354  250 
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" 
47308  251 
shows "Quotient (invariant P) Abs Rep T" 
47651  252 
using typedef_to_Quotient [OF assms] by simp 
47308  253 

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

254 
lemma open_typedef_to_part_equivp: 
47308  255 
assumes "type_definition Rep Abs {x. P x}" 
256 
shows "part_equivp (invariant P)" 

47651  257 
using typedef_to_part_equivp [OF assms] by simp 
47308  258 

47376  259 
text {* Generating transfer rules for quotients. *} 
260 

47537  261 
context 
262 
fixes R Abs Rep T 

263 
assumes 1: "Quotient R Abs Rep T" 

264 
begin 

47376  265 

47537  266 
lemma Quotient_right_unique: "right_unique T" 
267 
using 1 unfolding Quotient_alt_def right_unique_def by metis 

268 

269 
lemma Quotient_right_total: "right_total T" 

270 
using 1 unfolding Quotient_alt_def right_total_def by metis 

271 

272 
lemma Quotient_rel_eq_transfer: "(T ===> T ===> op =) R (op =)" 

273 
using 1 unfolding Quotient_alt_def fun_rel_def by simp 

47376  274 

47538  275 
lemma Quotient_abs_induct: 
276 
assumes "\<And>y. R y y \<Longrightarrow> P (Abs y)" shows "P x" 

277 
using 1 assms unfolding Quotient_def by metis 

278 

47544  279 
lemma Quotient_All_transfer: 
280 
"((T ===> op =) ===> op =) (Ball (Respects R)) All" 

281 
unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1] 

282 
by (auto, metis Quotient_abs_induct) 

283 

284 
lemma Quotient_Ex_transfer: 

285 
"((T ===> op =) ===> op =) (Bex (Respects R)) Ex" 

286 
unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1] 

287 
by (auto, metis Quotient_rep_reflp [OF 1] Quotient_abs_rep [OF 1]) 

288 

289 
lemma Quotient_forall_transfer: 

290 
"((T ===> op =) ===> op =) (transfer_bforall (\<lambda>x. R x x)) transfer_forall" 

291 
using Quotient_All_transfer 

292 
unfolding transfer_forall_def transfer_bforall_def 

293 
Ball_def [abs_def] in_respects . 

294 

47537  295 
end 
296 

297 
text {* Generating transfer rules for total quotients. *} 

47376  298 

47537  299 
context 
300 
fixes R Abs Rep T 

301 
assumes 1: "Quotient R Abs Rep T" and 2: "reflp R" 

302 
begin 

47376  303 

47537  304 
lemma Quotient_bi_total: "bi_total T" 
305 
using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto 

306 

307 
lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs" 

308 
using 1 2 unfolding Quotient_alt_def reflp_def fun_rel_def by simp 

309 

47575  310 
lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x" 
311 
using 1 2 assms unfolding Quotient_alt_def reflp_def by metis 

312 

47537  313 
end 
47376  314 

47368
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

315 
text {* Generating transfer rules for a type defined with @{text "typedef"}. *} 
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

316 

47534
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

317 
context 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

318 
fixes Rep Abs A T 
47368
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

319 
assumes type: "type_definition Rep Abs A" 
47534
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

320 
assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)" 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

321 
begin 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

322 

06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

323 
lemma typedef_bi_unique: "bi_unique T" 
47368
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

324 
unfolding bi_unique_def T_def 
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

325 
by (simp add: type_definition.Rep_inject [OF type]) 
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

326 

47535
0f94b02fda1c
lifting_setup generates transfer rule for rep of typedefs
huffman
parents:
47534
diff
changeset

327 
lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep" 
0f94b02fda1c
lifting_setup generates transfer rule for rep of typedefs
huffman
parents:
47534
diff
changeset

328 
unfolding fun_rel_def T_def by simp 
0f94b02fda1c
lifting_setup generates transfer rule for rep of typedefs
huffman
parents:
47534
diff
changeset

329 

47545  330 
lemma typedef_All_transfer: "((T ===> op =) ===> op =) (Ball A) All" 
47534
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

331 
unfolding T_def fun_rel_def 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

332 
by (metis type_definition.Rep [OF type] 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

333 
type_definition.Abs_inverse [OF type]) 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

334 

47545  335 
lemma typedef_Ex_transfer: "((T ===> op =) ===> op =) (Bex A) Ex" 
336 
unfolding T_def fun_rel_def 

337 
by (metis type_definition.Rep [OF type] 

338 
type_definition.Abs_inverse [OF type]) 

339 

340 
lemma typedef_forall_transfer: 

47534
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

341 
"((T ===> op =) ===> op =) 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

342 
(transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall" 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

343 
unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric] 
47545  344 
by (rule typedef_All_transfer) 
47534
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

345 

06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

346 
end 
06cc372a80ed
use context block to organize typedef lifting theorems
huffman
parents:
47521
diff
changeset

347 

47368
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

348 
text {* Generating the correspondence rule for a constant defined with 
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

349 
@{text "lift_definition"}. *} 
4c522dff1f4d
add lemmas for generating transfer rules for typedefs
huffman
parents:
47354
diff
changeset

350 

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

353 
shows "T c c'" 

354 
using assms by (auto dest: Quotient_cr_rel) 

355 

47308  356 
subsection {* ML setup *} 
357 

47698  358 
use "Tools/Lifting/lifting_util.ML" 
47308  359 

360 
use "Tools/Lifting/lifting_info.ML" 

361 
setup Lifting_Info.setup 

362 

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

364 

365 
use "Tools/Lifting/lifting_term.ML" 

366 

367 
use "Tools/Lifting/lifting_def.ML" 

368 

369 
use "Tools/Lifting/lifting_setup.ML" 

370 

371 
hide_const (open) invariant 

372 

373 
end 