summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | huffman |

Wed, 04 Apr 2012 16:48:39 +0200 | |

changeset 47368 | 4c522dff1f4d |

parent 47356 | 19fb95255ec9 |

child 47369 | f483be2fecb9 |

add lemmas for generating transfer rules for typedefs

--- a/src/HOL/Lifting.thy Wed Apr 04 16:05:52 2012 +0200 +++ b/src/HOL/Lifting.thy Wed Apr 04 16:48:39 2012 +0200 @@ -283,6 +283,54 @@ show "transp (invariant P)" by (auto intro: transpI simp: invariant_def) qed +text {* Generating transfer rules for a type defined with @{text "typedef"}. *} + +lemma typedef_bi_unique: + assumes type: "type_definition Rep Abs A" + assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" + shows "bi_unique T" + unfolding bi_unique_def T_def + by (simp add: type_definition.Rep_inject [OF type]) + +lemma typedef_right_total: + assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" + shows "right_total T" + unfolding right_total_def T_def by simp + +lemma copy_type_bi_total: + assumes type: "type_definition Rep Abs UNIV" + assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" + shows "bi_total T" + unfolding bi_total_def T_def + by (metis type_definition.Abs_inverse [OF type] UNIV_I) + +lemma typedef_transfer_All: + assumes type: "type_definition Rep Abs A" + assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" + shows "((T ===> op =) ===> op =) (Ball A) All" + unfolding T_def fun_rel_def + by (metis type_definition.Rep [OF type] + type_definition.Abs_inverse [OF type]) + +lemma typedef_transfer_Ex: + assumes type: "type_definition Rep Abs A" + assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" + shows "((T ===> op =) ===> op =) (Bex A) Ex" + unfolding T_def fun_rel_def + by (metis type_definition.Rep [OF type] + type_definition.Abs_inverse [OF type]) + +lemma typedef_transfer_bforall: + assumes type: "type_definition Rep Abs A" + assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)" + shows "((T ===> op =) ===> op =) + (transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall" + unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric] + by (rule typedef_transfer_All [OF assms]) + +text {* Generating the correspondence rule for a constant defined with + @{text "lift_definition"}. *} + lemma Quotient_to_transfer: assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c" shows "T c c'"