295 show "symp (invariant P)" by (auto intro: sympI simp: invariant_def) |
295 show "symp (invariant P)" by (auto intro: sympI simp: invariant_def) |
296 next |
296 next |
297 show "transp (invariant P)" by (auto intro: transpI simp: invariant_def) |
297 show "transp (invariant P)" by (auto intro: transpI simp: invariant_def) |
298 qed |
298 qed |
299 |
299 |
|
300 text {* Generating transfer rules for quotients. *} |
|
301 |
|
302 lemma Quotient_right_unique: |
|
303 assumes "Quotient R Abs Rep T" shows "right_unique T" |
|
304 using assms unfolding Quotient_alt_def right_unique_def by metis |
|
305 |
|
306 lemma Quotient_right_total: |
|
307 assumes "Quotient R Abs Rep T" shows "right_total T" |
|
308 using assms unfolding Quotient_alt_def right_total_def by metis |
|
309 |
|
310 lemma Quotient_rel_eq_transfer: |
|
311 assumes "Quotient R Abs Rep T" |
|
312 shows "(T ===> T ===> op =) R (op =)" |
|
313 using assms unfolding Quotient_alt_def fun_rel_def by simp |
|
314 |
|
315 lemma Quotient_bi_total: |
|
316 assumes "Quotient R Abs Rep T" and "reflp R" |
|
317 shows "bi_total T" |
|
318 using assms unfolding Quotient_alt_def bi_total_def reflp_def by auto |
|
319 |
|
320 lemma Quotient_id_abs_transfer: |
|
321 assumes "Quotient R Abs Rep T" and "reflp R" |
|
322 shows "(op = ===> T) (\<lambda>x. x) Abs" |
|
323 using assms unfolding Quotient_alt_def reflp_def fun_rel_def by simp |
|
324 |
300 text {* Generating transfer rules for a type defined with @{text "typedef"}. *} |
325 text {* Generating transfer rules for a type defined with @{text "typedef"}. *} |
301 |
326 |
302 lemma typedef_bi_unique: |
327 lemma typedef_bi_unique: |
303 assumes type: "type_definition Rep Abs A" |
328 assumes type: "type_definition Rep Abs A" |
304 assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" |
329 assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" |