kuncar@48153
|
1 |
(* Title: HOL/Lifting.thy
|
kuncar@48153
|
2 |
Author: Brian Huffman and Ondrej Kuncar
|
kuncar@48153
|
3 |
Author: Cezary Kaliszyk and Christian Urban
|
kuncar@48153
|
4 |
*)
|
kuncar@48153
|
5 |
|
kuncar@48153
|
6 |
header {* Lifting package *}
|
kuncar@48153
|
7 |
|
kuncar@48153
|
8 |
theory Lifting
|
huffman@48196
|
9 |
imports Plain Equiv_Relations Transfer
|
kuncar@48153
|
10 |
keywords
|
kuncar@48153
|
11 |
"print_quotmaps" "print_quotients" :: diag and
|
kuncar@48153
|
12 |
"lift_definition" :: thy_goal and
|
kuncar@48153
|
13 |
"setup_lifting" :: thy_decl
|
kuncar@48153
|
14 |
uses
|
kuncar@48153
|
15 |
("Tools/Lifting/lifting_info.ML")
|
kuncar@48153
|
16 |
("Tools/Lifting/lifting_term.ML")
|
kuncar@48153
|
17 |
("Tools/Lifting/lifting_def.ML")
|
kuncar@48153
|
18 |
("Tools/Lifting/lifting_setup.ML")
|
kuncar@48153
|
19 |
begin
|
kuncar@48153
|
20 |
|
huffman@48196
|
21 |
subsection {* Function map *}
|
kuncar@48153
|
22 |
|
kuncar@48153
|
23 |
notation map_fun (infixr "--->" 55)
|
kuncar@48153
|
24 |
|
kuncar@48153
|
25 |
lemma map_fun_id:
|
kuncar@48153
|
26 |
"(id ---> id) = id"
|
kuncar@48153
|
27 |
by (simp add: fun_eq_iff)
|
kuncar@48153
|
28 |
|
kuncar@48153
|
29 |
subsection {* Quotient Predicate *}
|
kuncar@48153
|
30 |
|
kuncar@48153
|
31 |
definition
|
kuncar@48153
|
32 |
"Quotient R Abs Rep T \<longleftrightarrow>
|
kuncar@48153
|
33 |
(\<forall>a. Abs (Rep a) = a) \<and>
|
kuncar@48153
|
34 |
(\<forall>a. R (Rep a) (Rep a)) \<and>
|
kuncar@48153
|
35 |
(\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s) \<and>
|
kuncar@48153
|
36 |
T = (\<lambda>x y. R x x \<and> Abs x = y)"
|
kuncar@48153
|
37 |
|
kuncar@48153
|
38 |
lemma QuotientI:
|
kuncar@48153
|
39 |
assumes "\<And>a. Abs (Rep a) = a"
|
kuncar@48153
|
40 |
and "\<And>a. R (Rep a) (Rep a)"
|
kuncar@48153
|
41 |
and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s"
|
kuncar@48153
|
42 |
and "T = (\<lambda>x y. R x x \<and> Abs x = y)"
|
kuncar@48153
|
43 |
shows "Quotient R Abs Rep T"
|
kuncar@48153
|
44 |
using assms unfolding Quotient_def by blast
|
kuncar@48153
|
45 |
|
kuncar@48153
|
46 |
lemma Quotient_abs_rep:
|
kuncar@48153
|
47 |
assumes a: "Quotient R Abs Rep T"
|
kuncar@48153
|
48 |
shows "Abs (Rep a) = a"
|
kuncar@48153
|
49 |
using a
|
kuncar@48153
|
50 |
unfolding Quotient_def
|
kuncar@48153
|
51 |
by simp
|
kuncar@48153
|
52 |
|
kuncar@48153
|
53 |
lemma Quotient_rep_reflp:
|
kuncar@48153
|
54 |
assumes a: "Quotient R Abs Rep T"
|
kuncar@48153
|
55 |
shows "R (Rep a) (Rep a)"
|
kuncar@48153
|
56 |
using a
|
kuncar@48153
|
57 |
unfolding Quotient_def
|
kuncar@48153
|
58 |
by blast
|
kuncar@48153
|
59 |
|
kuncar@48153
|
60 |
lemma Quotient_rel:
|
kuncar@48153
|
61 |
assumes a: "Quotient R Abs Rep T"
|
kuncar@48153
|
62 |
shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
|
kuncar@48153
|
63 |
using a
|
kuncar@48153
|
64 |
unfolding Quotient_def
|
kuncar@48153
|
65 |
by blast
|
kuncar@48153
|
66 |
|
kuncar@48153
|
67 |
lemma Quotient_cr_rel:
|
kuncar@48153
|
68 |
assumes a: "Quotient R Abs Rep T"
|
kuncar@48153
|
69 |
shows "T = (\<lambda>x y. R x x \<and> Abs x = y)"
|
kuncar@48153
|
70 |
using a
|
kuncar@48153
|
71 |
unfolding Quotient_def
|
kuncar@48153
|
72 |
by blast
|
kuncar@48153
|
73 |
|
kuncar@48153
|
74 |
lemma Quotient_refl1:
|
kuncar@48153
|
75 |
assumes a: "Quotient R Abs Rep T"
|
kuncar@48153
|
76 |
shows "R r s \<Longrightarrow> R r r"
|
kuncar@48153
|
77 |
using a unfolding Quotient_def
|
kuncar@48153
|
78 |
by fast
|
kuncar@48153
|
79 |
|
kuncar@48153
|
80 |
lemma Quotient_refl2:
|
kuncar@48153
|
81 |
assumes a: "Quotient R Abs Rep T"
|
kuncar@48153
|
82 |
shows "R r s \<Longrightarrow> R s s"
|
kuncar@48153
|
83 |
using a unfolding Quotient_def
|
kuncar@48153
|
84 |
by fast
|
kuncar@48153
|
85 |
|
kuncar@48153
|
86 |
lemma Quotient_rel_rep:
|
kuncar@48153
|
87 |
assumes a: "Quotient R Abs Rep T"
|
kuncar@48153
|
88 |
shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
|
kuncar@48153
|
89 |
using a
|
kuncar@48153
|
90 |
unfolding Quotient_def
|
kuncar@48153
|
91 |
by metis
|
kuncar@48153
|
92 |
|
kuncar@48153
|
93 |
lemma Quotient_rep_abs:
|
kuncar@48153
|
94 |
assumes a: "Quotient R Abs Rep T"
|
kuncar@48153
|
95 |
shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
|
kuncar@48153
|
96 |
using a unfolding Quotient_def
|
kuncar@48153
|
97 |
by blast
|
kuncar@48153
|
98 |
|
kuncar@48153
|
99 |
lemma Quotient_rel_abs:
|
kuncar@48153
|
100 |
assumes a: "Quotient R Abs Rep T"
|
kuncar@48153
|
101 |
shows "R r s \<Longrightarrow> Abs r = Abs s"
|
kuncar@48153
|
102 |
using a unfolding Quotient_def
|
kuncar@48153
|
103 |
by blast
|
kuncar@48153
|
104 |
|
kuncar@48153
|
105 |
lemma Quotient_symp:
|
kuncar@48153
|
106 |
assumes a: "Quotient R Abs Rep T"
|
kuncar@48153
|
107 |
shows "symp R"
|
kuncar@48153
|
108 |
using a unfolding Quotient_def using sympI by (metis (full_types))
|
kuncar@48153
|
109 |
|
kuncar@48153
|
110 |
lemma Quotient_transp:
|
kuncar@48153
|
111 |
assumes a: "Quotient R Abs Rep T"
|
kuncar@48153
|
112 |
shows "transp R"
|
kuncar@48153
|
113 |
using a unfolding Quotient_def using transpI by (metis (full_types))
|
kuncar@48153
|
114 |
|
kuncar@48153
|
115 |
lemma Quotient_part_equivp:
|
kuncar@48153
|
116 |
assumes a: "Quotient R Abs Rep T"
|
kuncar@48153
|
117 |
shows "part_equivp R"
|
kuncar@48153
|
118 |
by (metis Quotient_rep_reflp Quotient_symp Quotient_transp a part_equivpI)
|
kuncar@48153
|
119 |
|
kuncar@48153
|
120 |
lemma identity_quotient: "Quotient (op =) id id (op =)"
|
kuncar@48153
|
121 |
unfolding Quotient_def by simp
|
kuncar@48153
|
122 |
|
kuncar@48153
|
123 |
lemma Quotient_alt_def:
|
kuncar@48153
|
124 |
"Quotient R Abs Rep T \<longleftrightarrow>
|
kuncar@48153
|
125 |
(\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and>
|
kuncar@48153
|
126 |
(\<forall>b. T (Rep b) b) \<and>
|
kuncar@48153
|
127 |
(\<forall>x y. R x y \<longleftrightarrow> T x (Abs x) \<and> T y (Abs y) \<and> Abs x = Abs y)"
|
kuncar@48153
|
128 |
apply safe
|
kuncar@48153
|
129 |
apply (simp (no_asm_use) only: Quotient_def, fast)
|
kuncar@48153
|
130 |
apply (simp (no_asm_use) only: Quotient_def, fast)
|
kuncar@48153
|
131 |
apply (simp (no_asm_use) only: Quotient_def, fast)
|
kuncar@48153
|
132 |
apply (simp (no_asm_use) only: Quotient_def, fast)
|
kuncar@48153
|
133 |
apply (simp (no_asm_use) only: Quotient_def, fast)
|
kuncar@48153
|
134 |
apply (simp (no_asm_use) only: Quotient_def, fast)
|
kuncar@48153
|
135 |
apply (rule QuotientI)
|
kuncar@48153
|
136 |
apply simp
|
kuncar@48153
|
137 |
apply metis
|
kuncar@48153
|
138 |
apply simp
|
kuncar@48153
|
139 |
apply (rule ext, rule ext, metis)
|
kuncar@48153
|
140 |
done
|
kuncar@48153
|
141 |
|
kuncar@48153
|
142 |
lemma Quotient_alt_def2:
|
kuncar@48153
|
143 |
"Quotient R Abs Rep T \<longleftrightarrow>
|
kuncar@48153
|
144 |
(\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and>
|
kuncar@48153
|
145 |
(\<forall>b. T (Rep b) b) \<and>
|
kuncar@48153
|
146 |
(\<forall>x y. R x y \<longleftrightarrow> T x (Abs y) \<and> T y (Abs x))"
|
kuncar@48153
|
147 |
unfolding Quotient_alt_def by (safe, metis+)
|
kuncar@48153
|
148 |
|
kuncar@48153
|
149 |
lemma fun_quotient:
|
kuncar@48153
|
150 |
assumes 1: "Quotient R1 abs1 rep1 T1"
|
kuncar@48153
|
151 |
assumes 2: "Quotient R2 abs2 rep2 T2"
|
kuncar@48153
|
152 |
shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2) (T1 ===> T2)"
|
kuncar@48153
|
153 |
using assms unfolding Quotient_alt_def2
|
kuncar@48153
|
154 |
unfolding fun_rel_def fun_eq_iff map_fun_apply
|
kuncar@48153
|
155 |
by (safe, metis+)
|
kuncar@48153
|
156 |
|
kuncar@48153
|
157 |
lemma apply_rsp:
|
kuncar@48153
|
158 |
fixes f g::"'a \<Rightarrow> 'c"
|
kuncar@48153
|
159 |
assumes q: "Quotient R1 Abs1 Rep1 T1"
|
kuncar@48153
|
160 |
and a: "(R1 ===> R2) f g" "R1 x y"
|
kuncar@48153
|
161 |
shows "R2 (f x) (g y)"
|
kuncar@48153
|
162 |
using a by (auto elim: fun_relE)
|
kuncar@48153
|
163 |
|
kuncar@48153
|
164 |
lemma apply_rsp':
|
kuncar@48153
|
165 |
assumes a: "(R1 ===> R2) f g" "R1 x y"
|
kuncar@48153
|
166 |
shows "R2 (f x) (g y)"
|
kuncar@48153
|
167 |
using a by (auto elim: fun_relE)
|
kuncar@48153
|
168 |
|
kuncar@48153
|
169 |
lemma apply_rsp'':
|
kuncar@48153
|
170 |
assumes "Quotient R Abs Rep T"
|
kuncar@48153
|
171 |
and "(R ===> S) f f"
|
kuncar@48153
|
172 |
shows "S (f (Rep x)) (f (Rep x))"
|
kuncar@48153
|
173 |
proof -
|
kuncar@48153
|
174 |
from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp)
|
kuncar@48153
|
175 |
then show ?thesis using assms(2) by (auto intro: apply_rsp')
|
kuncar@48153
|
176 |
qed
|
kuncar@48153
|
177 |
|
kuncar@48153
|
178 |
subsection {* Quotient composition *}
|
kuncar@48153
|
179 |
|
kuncar@48153
|
180 |
lemma Quotient_compose:
|
kuncar@48153
|
181 |
assumes 1: "Quotient R1 Abs1 Rep1 T1"
|
kuncar@48153
|
182 |
assumes 2: "Quotient R2 Abs2 Rep2 T2"
|
kuncar@48153
|
183 |
shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2) (T1 OO T2)"
|
kuncar@48153
|
184 |
proof -
|
kuncar@48153
|
185 |
from 1 have Abs1: "\<And>a b. T1 a b \<Longrightarrow> Abs1 a = b"
|
kuncar@48153
|
186 |
unfolding Quotient_alt_def by simp
|
kuncar@48153
|
187 |
from 1 have Rep1: "\<And>b. T1 (Rep1 b) b"
|
kuncar@48153
|
188 |
unfolding Quotient_alt_def by simp
|
kuncar@48153
|
189 |
from 2 have Abs2: "\<And>a b. T2 a b \<Longrightarrow> Abs2 a = b"
|
kuncar@48153
|
190 |
unfolding Quotient_alt_def by simp
|
kuncar@48153
|
191 |
from 2 have Rep2: "\<And>b. T2 (Rep2 b) b"
|
kuncar@48153
|
192 |
unfolding Quotient_alt_def by simp
|
kuncar@48153
|
193 |
from 2 have R2:
|
kuncar@48153
|
194 |
"\<And>x y. R2 x y \<longleftrightarrow> T2 x (Abs2 x) \<and> T2 y (Abs2 y) \<and> Abs2 x = Abs2 y"
|
kuncar@48153
|
195 |
unfolding Quotient_alt_def by simp
|
kuncar@48153
|
196 |
show ?thesis
|
kuncar@48153
|
197 |
unfolding Quotient_alt_def
|
kuncar@48153
|
198 |
apply simp
|
kuncar@48153
|
199 |
apply safe
|
kuncar@48153
|
200 |
apply (drule Abs1, simp)
|
kuncar@48153
|
201 |
apply (erule Abs2)
|
griff@48303
|
202 |
apply (rule relcomppI)
|
kuncar@48153
|
203 |
apply (rule Rep1)
|
kuncar@48153
|
204 |
apply (rule Rep2)
|
griff@48303
|
205 |
apply (rule relcomppI, assumption)
|
kuncar@48153
|
206 |
apply (drule Abs1, simp)
|
kuncar@48153
|
207 |
apply (clarsimp simp add: R2)
|
griff@48303
|
208 |
apply (rule relcomppI, assumption)
|
kuncar@48153
|
209 |
apply (drule Abs1, simp)+
|
kuncar@48153
|
210 |
apply (clarsimp simp add: R2)
|
kuncar@48153
|
211 |
apply (drule Abs1, simp)+
|
kuncar@48153
|
212 |
apply (clarsimp simp add: R2)
|
griff@48303
|
213 |
apply (rule relcomppI, assumption)
|
griff@48303
|
214 |
apply (rule relcomppI [rotated])
|
kuncar@48153
|
215 |
apply (erule conversepI)
|
kuncar@48153
|
216 |
apply (drule Abs1, simp)+
|
kuncar@48153
|
217 |
apply (simp add: R2)
|
kuncar@48153
|
218 |
done
|
kuncar@48153
|
219 |
qed
|
kuncar@48153
|
220 |
|
kuncar@48153
|
221 |
subsection {* Invariant *}
|
kuncar@48153
|
222 |
|
kuncar@48153
|
223 |
definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
|
kuncar@48153
|
224 |
where "invariant R = (\<lambda>x y. R x \<and> x = y)"
|
kuncar@48153
|
225 |
|
kuncar@48153
|
226 |
lemma invariant_to_eq:
|
kuncar@48153
|
227 |
assumes "invariant P x y"
|
kuncar@48153
|
228 |
shows "x = y"
|
kuncar@48153
|
229 |
using assms by (simp add: invariant_def)
|
kuncar@48153
|
230 |
|
kuncar@48153
|
231 |
lemma fun_rel_eq_invariant:
|
kuncar@48153
|
232 |
shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
|
kuncar@48153
|
233 |
by (auto simp add: invariant_def fun_rel_def)
|
kuncar@48153
|
234 |
|
kuncar@48153
|
235 |
lemma invariant_same_args:
|
kuncar@48153
|
236 |
shows "invariant P x x \<equiv> P x"
|
kuncar@48153
|
237 |
using assms by (auto simp add: invariant_def)
|
kuncar@48153
|
238 |
|
kuncar@48219
|
239 |
lemma UNIV_typedef_to_Quotient:
|
kuncar@48153
|
240 |
assumes "type_definition Rep Abs UNIV"
|
kuncar@48219
|
241 |
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
|
kuncar@48153
|
242 |
shows "Quotient (op =) Abs Rep T"
|
kuncar@48153
|
243 |
proof -
|
kuncar@48153
|
244 |
interpret type_definition Rep Abs UNIV by fact
|
kuncar@48219
|
245 |
from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
|
kuncar@48219
|
246 |
by (fastforce intro!: QuotientI fun_eq_iff)
|
kuncar@48153
|
247 |
qed
|
kuncar@48153
|
248 |
|
kuncar@48219
|
249 |
lemma UNIV_typedef_to_equivp:
|
kuncar@48153
|
250 |
fixes Abs :: "'a \<Rightarrow> 'b"
|
kuncar@48153
|
251 |
and Rep :: "'b \<Rightarrow> 'a"
|
kuncar@48153
|
252 |
assumes "type_definition Rep Abs (UNIV::'a set)"
|
kuncar@48153
|
253 |
shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
|
kuncar@48153
|
254 |
by (rule identity_equivp)
|
kuncar@48153
|
255 |
|
huffman@48212
|
256 |
lemma typedef_to_Quotient:
|
kuncar@48219
|
257 |
assumes "type_definition Rep Abs S"
|
kuncar@48219
|
258 |
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
|
kuncar@48219
|
259 |
shows "Quotient (Lifting.invariant (\<lambda>x. x \<in> S)) Abs Rep T"
|
kuncar@48219
|
260 |
proof -
|
kuncar@48219
|
261 |
interpret type_definition Rep Abs S by fact
|
kuncar@48219
|
262 |
from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
|
kuncar@48219
|
263 |
by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
|
kuncar@48219
|
264 |
qed
|
kuncar@48219
|
265 |
|
kuncar@48219
|
266 |
lemma typedef_to_part_equivp:
|
kuncar@48219
|
267 |
assumes "type_definition Rep Abs S"
|
kuncar@48219
|
268 |
shows "part_equivp (Lifting.invariant (\<lambda>x. x \<in> S))"
|
kuncar@48219
|
269 |
proof (intro part_equivpI)
|
kuncar@48219
|
270 |
interpret type_definition Rep Abs S by fact
|
kuncar@48219
|
271 |
show "\<exists>x. Lifting.invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def)
|
kuncar@48219
|
272 |
next
|
kuncar@48219
|
273 |
show "symp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def)
|
kuncar@48219
|
274 |
next
|
kuncar@48219
|
275 |
show "transp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def)
|
kuncar@48219
|
276 |
qed
|
kuncar@48219
|
277 |
|
kuncar@48219
|
278 |
lemma open_typedef_to_Quotient:
|
kuncar@48153
|
279 |
assumes "type_definition Rep Abs {x. P x}"
|
huffman@48212
|
280 |
and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
|
kuncar@48153
|
281 |
shows "Quotient (invariant P) Abs Rep T"
|
kuncar@48153
|
282 |
proof -
|
kuncar@48153
|
283 |
interpret type_definition Rep Abs "{x. P x}" by fact
|
huffman@48212
|
284 |
from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
|
huffman@48212
|
285 |
by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
|
kuncar@48153
|
286 |
qed
|
kuncar@48153
|
287 |
|
kuncar@48219
|
288 |
lemma open_typedef_to_part_equivp:
|
kuncar@48153
|
289 |
assumes "type_definition Rep Abs {x. P x}"
|
kuncar@48153
|
290 |
shows "part_equivp (invariant P)"
|
kuncar@48153
|
291 |
proof (intro part_equivpI)
|
kuncar@48153
|
292 |
interpret type_definition Rep Abs "{x. P x}" by fact
|
kuncar@48153
|
293 |
show "\<exists>x. invariant P x x" using Rep by (auto simp: invariant_def)
|
kuncar@48153
|
294 |
next
|
kuncar@48153
|
295 |
show "symp (invariant P)" by (auto intro: sympI simp: invariant_def)
|
kuncar@48153
|
296 |
next
|
kuncar@48153
|
297 |
show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
|
kuncar@48153
|
298 |
qed
|
kuncar@48153
|
299 |
|
huffman@48234
|
300 |
text {* Generating transfer rules for quotients. *}
|
huffman@48234
|
301 |
|
huffman@48234
|
302 |
lemma Quotient_right_unique:
|
huffman@48234
|
303 |
assumes "Quotient R Abs Rep T" shows "right_unique T"
|
huffman@48234
|
304 |
using assms unfolding Quotient_alt_def right_unique_def by metis
|
huffman@48234
|
305 |
|
huffman@48234
|
306 |
lemma Quotient_right_total:
|
huffman@48234
|
307 |
assumes "Quotient R Abs Rep T" shows "right_total T"
|
huffman@48234
|
308 |
using assms unfolding Quotient_alt_def right_total_def by metis
|
huffman@48234
|
309 |
|
huffman@48234
|
310 |
lemma Quotient_rel_eq_transfer:
|
huffman@48234
|
311 |
assumes "Quotient R Abs Rep T"
|
huffman@48234
|
312 |
shows "(T ===> T ===> op =) R (op =)"
|
huffman@48234
|
313 |
using assms unfolding Quotient_alt_def fun_rel_def by simp
|
huffman@48234
|
314 |
|
huffman@48234
|
315 |
lemma Quotient_bi_total:
|
huffman@48234
|
316 |
assumes "Quotient R Abs Rep T" and "reflp R"
|
huffman@48234
|
317 |
shows "bi_total T"
|
huffman@48234
|
318 |
using assms unfolding Quotient_alt_def bi_total_def reflp_def by auto
|
huffman@48234
|
319 |
|
huffman@48234
|
320 |
lemma Quotient_id_abs_transfer:
|
huffman@48234
|
321 |
assumes "Quotient R Abs Rep T" and "reflp R"
|
huffman@48234
|
322 |
shows "(op = ===> T) (\<lambda>x. x) Abs"
|
huffman@48234
|
323 |
using assms unfolding Quotient_alt_def reflp_def fun_rel_def by simp
|
huffman@48234
|
324 |
|
huffman@48226
|
325 |
text {* Generating transfer rules for a type defined with @{text "typedef"}. *}
|
huffman@48226
|
326 |
|
huffman@48226
|
327 |
lemma typedef_bi_unique:
|
huffman@48226
|
328 |
assumes type: "type_definition Rep Abs A"
|
huffman@48226
|
329 |
assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
|
huffman@48226
|
330 |
shows "bi_unique T"
|
huffman@48226
|
331 |
unfolding bi_unique_def T_def
|
huffman@48226
|
332 |
by (simp add: type_definition.Rep_inject [OF type])
|
huffman@48226
|
333 |
|
huffman@48226
|
334 |
lemma typedef_right_total:
|
huffman@48226
|
335 |
assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
|
huffman@48226
|
336 |
shows "right_total T"
|
huffman@48226
|
337 |
unfolding right_total_def T_def by simp
|
huffman@48226
|
338 |
|
huffman@48226
|
339 |
lemma copy_type_bi_total:
|
huffman@48226
|
340 |
assumes type: "type_definition Rep Abs UNIV"
|
huffman@48226
|
341 |
assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
|
huffman@48226
|
342 |
shows "bi_total T"
|
huffman@48226
|
343 |
unfolding bi_total_def T_def
|
huffman@48226
|
344 |
by (metis type_definition.Abs_inverse [OF type] UNIV_I)
|
huffman@48226
|
345 |
|
huffman@48226
|
346 |
lemma typedef_transfer_All:
|
huffman@48226
|
347 |
assumes type: "type_definition Rep Abs A"
|
huffman@48226
|
348 |
assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
|
huffman@48226
|
349 |
shows "((T ===> op =) ===> op =) (Ball A) All"
|
huffman@48226
|
350 |
unfolding T_def fun_rel_def
|
huffman@48226
|
351 |
by (metis type_definition.Rep [OF type]
|
huffman@48226
|
352 |
type_definition.Abs_inverse [OF type])
|
huffman@48226
|
353 |
|
huffman@48226
|
354 |
lemma typedef_transfer_Ex:
|
huffman@48226
|
355 |
assumes type: "type_definition Rep Abs A"
|
huffman@48226
|
356 |
assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
|
huffman@48226
|
357 |
shows "((T ===> op =) ===> op =) (Bex A) Ex"
|
huffman@48226
|
358 |
unfolding T_def fun_rel_def
|
huffman@48226
|
359 |
by (metis type_definition.Rep [OF type]
|
huffman@48226
|
360 |
type_definition.Abs_inverse [OF type])
|
huffman@48226
|
361 |
|
huffman@48226
|
362 |
lemma typedef_transfer_bforall:
|
huffman@48226
|
363 |
assumes type: "type_definition Rep Abs A"
|
huffman@48226
|
364 |
assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
|
huffman@48226
|
365 |
shows "((T ===> op =) ===> op =)
|
huffman@48226
|
366 |
(transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall"
|
huffman@48226
|
367 |
unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric]
|
huffman@48226
|
368 |
by (rule typedef_transfer_All [OF assms])
|
huffman@48226
|
369 |
|
huffman@48226
|
370 |
text {* Generating the correspondence rule for a constant defined with
|
huffman@48226
|
371 |
@{text "lift_definition"}. *}
|
huffman@48226
|
372 |
|
huffman@48209
|
373 |
lemma Quotient_to_transfer:
|
huffman@48209
|
374 |
assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c"
|
huffman@48209
|
375 |
shows "T c c'"
|
huffman@48209
|
376 |
using assms by (auto dest: Quotient_cr_rel)
|
huffman@48209
|
377 |
|
kuncar@48153
|
378 |
subsection {* ML setup *}
|
kuncar@48153
|
379 |
|
kuncar@48153
|
380 |
text {* Auxiliary data for the lifting package *}
|
kuncar@48153
|
381 |
|
kuncar@48153
|
382 |
use "Tools/Lifting/lifting_info.ML"
|
kuncar@48153
|
383 |
setup Lifting_Info.setup
|
kuncar@48153
|
384 |
|
kuncar@48153
|
385 |
declare [[map "fun" = (fun_rel, fun_quotient)]]
|
kuncar@48153
|
386 |
|
kuncar@48153
|
387 |
use "Tools/Lifting/lifting_term.ML"
|
kuncar@48153
|
388 |
|
kuncar@48153
|
389 |
use "Tools/Lifting/lifting_def.ML"
|
kuncar@48153
|
390 |
|
kuncar@48153
|
391 |
use "Tools/Lifting/lifting_setup.ML"
|
kuncar@48153
|
392 |
|
kuncar@48153
|
393 |
hide_const (open) invariant
|
kuncar@48153
|
394 |
|
kuncar@48153
|
395 |
end
|