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