add lemmas for generating transfer rules for typedefs
authorhuffman
Wed Apr 04 16:48:39 2012 +0200 (2012-04-04)
changeset 473684c522dff1f4d
parent 47356 19fb95255ec9
child 47369 f483be2fecb9
add lemmas for generating transfer rules for typedefs
src/HOL/Lifting.thy
     1.1 --- a/src/HOL/Lifting.thy	Wed Apr 04 16:05:52 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Wed Apr 04 16:48:39 2012 +0200
     1.3 @@ -283,6 +283,54 @@
     1.4    show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
     1.5  qed
     1.6  
     1.7 +text {* Generating transfer rules for a type defined with @{text "typedef"}. *}
     1.8 +
     1.9 +lemma typedef_bi_unique:
    1.10 +  assumes type: "type_definition Rep Abs A"
    1.11 +  assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.12 +  shows "bi_unique T"
    1.13 +  unfolding bi_unique_def T_def
    1.14 +  by (simp add: type_definition.Rep_inject [OF type])
    1.15 +
    1.16 +lemma typedef_right_total:
    1.17 +  assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.18 +  shows "right_total T"
    1.19 +  unfolding right_total_def T_def by simp
    1.20 +
    1.21 +lemma copy_type_bi_total:
    1.22 +  assumes type: "type_definition Rep Abs UNIV"
    1.23 +  assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.24 +  shows "bi_total T"
    1.25 +  unfolding bi_total_def T_def
    1.26 +  by (metis type_definition.Abs_inverse [OF type] UNIV_I)
    1.27 +
    1.28 +lemma typedef_transfer_All:
    1.29 +  assumes type: "type_definition Rep Abs A"
    1.30 +  assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.31 +  shows "((T ===> op =) ===> op =) (Ball A) All"
    1.32 +  unfolding T_def fun_rel_def
    1.33 +  by (metis type_definition.Rep [OF type]
    1.34 +    type_definition.Abs_inverse [OF type])
    1.35 +
    1.36 +lemma typedef_transfer_Ex:
    1.37 +  assumes type: "type_definition Rep Abs A"
    1.38 +  assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.39 +  shows "((T ===> op =) ===> op =) (Bex A) Ex"
    1.40 +  unfolding T_def fun_rel_def
    1.41 +  by (metis type_definition.Rep [OF type]
    1.42 +    type_definition.Abs_inverse [OF type])
    1.43 +
    1.44 +lemma typedef_transfer_bforall:
    1.45 +  assumes type: "type_definition Rep Abs A"
    1.46 +  assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.47 +  shows "((T ===> op =) ===> op =)
    1.48 +    (transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall"
    1.49 +  unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric]
    1.50 +  by (rule typedef_transfer_All [OF assms])
    1.51 +
    1.52 +text {* Generating the correspondence rule for a constant defined with
    1.53 +  @{text "lift_definition"}. *}
    1.54 +
    1.55  lemma Quotient_to_transfer:
    1.56    assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c"
    1.57    shows "T c c'"