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