src/HOL/Lifting.thy
author haftmann
Sun Jun 23 21:16:07 2013 +0200 (2013-06-23)
changeset 52435 6646bb548c6b
parent 52307 32c433c38ddd
child 53011 aeee0a4be6cf
permissions -rw-r--r--
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
     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 Equiv_Relations Transfer
    10 keywords
    11   "parametric" and
    12   "print_quotmaps" "print_quotients" :: diag and
    13   "lift_definition" :: thy_goal and
    14   "setup_lifting" :: thy_decl
    15 begin
    16 
    17 subsection {* Function map *}
    18 
    19 notation map_fun (infixr "--->" 55)
    20 
    21 lemma map_fun_id:
    22   "(id ---> id) = id"
    23   by (simp add: fun_eq_iff)
    24 
    25 subsection {* Other predicates on relations *}
    26 
    27 definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
    28   where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
    29 
    30 lemma left_totalI:
    31   "(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R"
    32 unfolding left_total_def by blast
    33 
    34 lemma left_totalE:
    35   assumes "left_total R"
    36   obtains "(\<And>x. \<exists>y. R x y)"
    37 using assms unfolding left_total_def by blast
    38 
    39 definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
    40   where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
    41 
    42 lemma left_total_fun:
    43   "\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
    44   unfolding left_total_def fun_rel_def
    45   apply (rule allI, rename_tac f)
    46   apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
    47   apply clarify
    48   apply (subgoal_tac "(THE x. A x y) = x", simp)
    49   apply (rule someI_ex)
    50   apply (simp)
    51   apply (rule the_equality)
    52   apply assumption
    53   apply (simp add: left_unique_def)
    54   done
    55 
    56 lemma left_unique_fun:
    57   "\<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (A ===> B)"
    58   unfolding left_total_def left_unique_def fun_rel_def
    59   by (clarify, rule ext, fast)
    60 
    61 lemma left_total_eq: "left_total op=" unfolding left_total_def by blast
    62 
    63 lemma left_unique_eq: "left_unique op=" unfolding left_unique_def by blast
    64 
    65 subsection {* Quotient Predicate *}
    66 
    67 definition
    68   "Quotient R Abs Rep T \<longleftrightarrow>
    69      (\<forall>a. Abs (Rep a) = a) \<and> 
    70      (\<forall>a. R (Rep a) (Rep a)) \<and>
    71      (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s) \<and>
    72      T = (\<lambda>x y. R x x \<and> Abs x = y)"
    73 
    74 lemma QuotientI:
    75   assumes "\<And>a. Abs (Rep a) = a"
    76     and "\<And>a. R (Rep a) (Rep a)"
    77     and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s"
    78     and "T = (\<lambda>x y. R x x \<and> Abs x = y)"
    79   shows "Quotient R Abs Rep T"
    80   using assms unfolding Quotient_def by blast
    81 
    82 context
    83   fixes R Abs Rep T
    84   assumes a: "Quotient R Abs Rep T"
    85 begin
    86 
    87 lemma Quotient_abs_rep: "Abs (Rep a) = a"
    88   using a unfolding Quotient_def
    89   by simp
    90 
    91 lemma Quotient_rep_reflp: "R (Rep a) (Rep a)"
    92   using a unfolding Quotient_def
    93   by blast
    94 
    95 lemma Quotient_rel:
    96   "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
    97   using a unfolding Quotient_def
    98   by blast
    99 
   100 lemma Quotient_cr_rel: "T = (\<lambda>x y. R x x \<and> Abs x = y)"
   101   using a unfolding Quotient_def
   102   by blast
   103 
   104 lemma Quotient_refl1: "R r s \<Longrightarrow> R r r"
   105   using a unfolding Quotient_def
   106   by fast
   107 
   108 lemma Quotient_refl2: "R r s \<Longrightarrow> R s s"
   109   using a unfolding Quotient_def
   110   by fast
   111 
   112 lemma Quotient_rel_rep: "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
   113   using a unfolding Quotient_def
   114   by metis
   115 
   116 lemma Quotient_rep_abs: "R r r \<Longrightarrow> R (Rep (Abs r)) r"
   117   using a unfolding Quotient_def
   118   by blast
   119 
   120 lemma Quotient_rep_abs_fold_unmap: 
   121   assumes "x' \<equiv> Abs x" and "R x x" and "Rep x' \<equiv> Rep' x'" 
   122   shows "R (Rep' x') x"
   123 proof -
   124   have "R (Rep x') x" using assms(1-2) Quotient_rep_abs by auto
   125   then show ?thesis using assms(3) by simp
   126 qed
   127 
   128 lemma Quotient_Rep_eq:
   129   assumes "x' \<equiv> Abs x" 
   130   shows "Rep x' \<equiv> Rep x'"
   131 by simp
   132 
   133 lemma Quotient_rel_abs: "R r s \<Longrightarrow> Abs r = Abs s"
   134   using a unfolding Quotient_def
   135   by blast
   136 
   137 lemma Quotient_rel_abs2:
   138   assumes "R (Rep x) y"
   139   shows "x = Abs y"
   140 proof -
   141   from assms have "Abs (Rep x) = Abs y" by (auto intro: Quotient_rel_abs)
   142   then show ?thesis using assms(1) by (simp add: Quotient_abs_rep)
   143 qed
   144 
   145 lemma Quotient_symp: "symp R"
   146   using a unfolding Quotient_def using sympI by (metis (full_types))
   147 
   148 lemma Quotient_transp: "transp R"
   149   using a unfolding Quotient_def using transpI by (metis (full_types))
   150 
   151 lemma Quotient_part_equivp: "part_equivp R"
   152 by (metis Quotient_rep_reflp Quotient_symp Quotient_transp part_equivpI)
   153 
   154 end
   155 
   156 lemma identity_quotient: "Quotient (op =) id id (op =)"
   157 unfolding Quotient_def by simp 
   158 
   159 text {* TODO: Use one of these alternatives as the real definition. *}
   160 
   161 lemma Quotient_alt_def:
   162   "Quotient R Abs Rep T \<longleftrightarrow>
   163     (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and>
   164     (\<forall>b. T (Rep b) b) \<and>
   165     (\<forall>x y. R x y \<longleftrightarrow> T x (Abs x) \<and> T y (Abs y) \<and> Abs x = Abs y)"
   166 apply safe
   167 apply (simp (no_asm_use) only: Quotient_def, fast)
   168 apply (simp (no_asm_use) only: Quotient_def, fast)
   169 apply (simp (no_asm_use) only: Quotient_def, fast)
   170 apply (simp (no_asm_use) only: Quotient_def, fast)
   171 apply (simp (no_asm_use) only: Quotient_def, fast)
   172 apply (simp (no_asm_use) only: Quotient_def, fast)
   173 apply (rule QuotientI)
   174 apply simp
   175 apply metis
   176 apply simp
   177 apply (rule ext, rule ext, metis)
   178 done
   179 
   180 lemma Quotient_alt_def2:
   181   "Quotient R Abs Rep T \<longleftrightarrow>
   182     (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and>
   183     (\<forall>b. T (Rep b) b) \<and>
   184     (\<forall>x y. R x y \<longleftrightarrow> T x (Abs y) \<and> T y (Abs x))"
   185   unfolding Quotient_alt_def by (safe, metis+)
   186 
   187 lemma Quotient_alt_def3:
   188   "Quotient R Abs Rep T \<longleftrightarrow>
   189     (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and>
   190     (\<forall>x y. R x y \<longleftrightarrow> (\<exists>z. T x z \<and> T y z))"
   191   unfolding Quotient_alt_def2 by (safe, metis+)
   192 
   193 lemma Quotient_alt_def4:
   194   "Quotient R Abs Rep T \<longleftrightarrow>
   195     (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> R = T OO conversep T"
   196   unfolding Quotient_alt_def3 fun_eq_iff by auto
   197 
   198 lemma fun_quotient:
   199   assumes 1: "Quotient R1 abs1 rep1 T1"
   200   assumes 2: "Quotient R2 abs2 rep2 T2"
   201   shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2) (T1 ===> T2)"
   202   using assms unfolding Quotient_alt_def2
   203   unfolding fun_rel_def fun_eq_iff map_fun_apply
   204   by (safe, metis+)
   205 
   206 lemma apply_rsp:
   207   fixes f g::"'a \<Rightarrow> 'c"
   208   assumes q: "Quotient R1 Abs1 Rep1 T1"
   209   and     a: "(R1 ===> R2) f g" "R1 x y"
   210   shows "R2 (f x) (g y)"
   211   using a by (auto elim: fun_relE)
   212 
   213 lemma apply_rsp':
   214   assumes a: "(R1 ===> R2) f g" "R1 x y"
   215   shows "R2 (f x) (g y)"
   216   using a by (auto elim: fun_relE)
   217 
   218 lemma apply_rsp'':
   219   assumes "Quotient R Abs Rep T"
   220   and "(R ===> S) f f"
   221   shows "S (f (Rep x)) (f (Rep x))"
   222 proof -
   223   from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp)
   224   then show ?thesis using assms(2) by (auto intro: apply_rsp')
   225 qed
   226 
   227 subsection {* Quotient composition *}
   228 
   229 lemma Quotient_compose:
   230   assumes 1: "Quotient R1 Abs1 Rep1 T1"
   231   assumes 2: "Quotient R2 Abs2 Rep2 T2"
   232   shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2) (T1 OO T2)"
   233   using assms unfolding Quotient_alt_def4 by fastforce
   234 
   235 lemma equivp_reflp2:
   236   "equivp R \<Longrightarrow> reflp R"
   237   by (erule equivpE)
   238 
   239 subsection {* Respects predicate *}
   240 
   241 definition Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set"
   242   where "Respects R = {x. R x x}"
   243 
   244 lemma in_respects: "x \<in> Respects R \<longleftrightarrow> R x x"
   245   unfolding Respects_def by simp
   246 
   247 subsection {* Invariant *}
   248 
   249 definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
   250   where "invariant R = (\<lambda>x y. R x \<and> x = y)"
   251 
   252 lemma invariant_to_eq:
   253   assumes "invariant P x y"
   254   shows "x = y"
   255 using assms by (simp add: invariant_def)
   256 
   257 lemma fun_rel_eq_invariant:
   258   shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
   259 by (auto simp add: invariant_def fun_rel_def)
   260 
   261 lemma invariant_same_args:
   262   shows "invariant P x x \<equiv> P x"
   263 using assms by (auto simp add: invariant_def)
   264 
   265 lemma UNIV_typedef_to_Quotient:
   266   assumes "type_definition Rep Abs UNIV"
   267   and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   268   shows "Quotient (op =) Abs Rep T"
   269 proof -
   270   interpret type_definition Rep Abs UNIV by fact
   271   from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis 
   272     by (fastforce intro!: QuotientI fun_eq_iff)
   273 qed
   274 
   275 lemma UNIV_typedef_to_equivp:
   276   fixes Abs :: "'a \<Rightarrow> 'b"
   277   and Rep :: "'b \<Rightarrow> 'a"
   278   assumes "type_definition Rep Abs (UNIV::'a set)"
   279   shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
   280 by (rule identity_equivp)
   281 
   282 lemma typedef_to_Quotient:
   283   assumes "type_definition Rep Abs S"
   284   and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   285   shows "Quotient (invariant (\<lambda>x. x \<in> S)) Abs Rep T"
   286 proof -
   287   interpret type_definition Rep Abs S by fact
   288   from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
   289     by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
   290 qed
   291 
   292 lemma typedef_to_part_equivp:
   293   assumes "type_definition Rep Abs S"
   294   shows "part_equivp (invariant (\<lambda>x. x \<in> S))"
   295 proof (intro part_equivpI)
   296   interpret type_definition Rep Abs S by fact
   297   show "\<exists>x. invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def)
   298 next
   299   show "symp (invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def)
   300 next
   301   show "transp (invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def)
   302 qed
   303 
   304 lemma open_typedef_to_Quotient:
   305   assumes "type_definition Rep Abs {x. P x}"
   306   and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   307   shows "Quotient (invariant P) Abs Rep T"
   308   using typedef_to_Quotient [OF assms] by simp
   309 
   310 lemma open_typedef_to_part_equivp:
   311   assumes "type_definition Rep Abs {x. P x}"
   312   shows "part_equivp (invariant P)"
   313   using typedef_to_part_equivp [OF assms] by simp
   314 
   315 text {* Generating transfer rules for quotients. *}
   316 
   317 context
   318   fixes R Abs Rep T
   319   assumes 1: "Quotient R Abs Rep T"
   320 begin
   321 
   322 lemma Quotient_right_unique: "right_unique T"
   323   using 1 unfolding Quotient_alt_def right_unique_def by metis
   324 
   325 lemma Quotient_right_total: "right_total T"
   326   using 1 unfolding Quotient_alt_def right_total_def by metis
   327 
   328 lemma Quotient_rel_eq_transfer: "(T ===> T ===> op =) R (op =)"
   329   using 1 unfolding Quotient_alt_def fun_rel_def by simp
   330 
   331 lemma Quotient_abs_induct:
   332   assumes "\<And>y. R y y \<Longrightarrow> P (Abs y)" shows "P x"
   333   using 1 assms unfolding Quotient_def by metis
   334 
   335 end
   336 
   337 text {* Generating transfer rules for total quotients. *}
   338 
   339 context
   340   fixes R Abs Rep T
   341   assumes 1: "Quotient R Abs Rep T" and 2: "reflp R"
   342 begin
   343 
   344 lemma Quotient_bi_total: "bi_total T"
   345   using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto
   346 
   347 lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs"
   348   using 1 2 unfolding Quotient_alt_def reflp_def fun_rel_def by simp
   349 
   350 lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x"
   351   using 1 2 assms unfolding Quotient_alt_def reflp_def by metis
   352 
   353 lemma Quotient_total_abs_eq_iff: "Abs x = Abs y \<longleftrightarrow> R x y"
   354   using Quotient_rel [OF 1] 2 unfolding reflp_def by simp
   355 
   356 end
   357 
   358 text {* Generating transfer rules for a type defined with @{text "typedef"}. *}
   359 
   360 context
   361   fixes Rep Abs A T
   362   assumes type: "type_definition Rep Abs A"
   363   assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)"
   364 begin
   365 
   366 lemma typedef_left_unique: "left_unique T"
   367   unfolding left_unique_def T_def
   368   by (simp add: type_definition.Rep_inject [OF type])
   369 
   370 lemma typedef_bi_unique: "bi_unique T"
   371   unfolding bi_unique_def T_def
   372   by (simp add: type_definition.Rep_inject [OF type])
   373 
   374 (* the following two theorems are here only for convinience *)
   375 
   376 lemma typedef_right_unique: "right_unique T"
   377   using T_def type Quotient_right_unique typedef_to_Quotient 
   378   by blast
   379 
   380 lemma typedef_right_total: "right_total T"
   381   using T_def type Quotient_right_total typedef_to_Quotient 
   382   by blast
   383 
   384 lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
   385   unfolding fun_rel_def T_def by simp
   386 
   387 end
   388 
   389 text {* Generating the correspondence rule for a constant defined with
   390   @{text "lift_definition"}. *}
   391 
   392 lemma Quotient_to_transfer:
   393   assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c"
   394   shows "T c c'"
   395   using assms by (auto dest: Quotient_cr_rel)
   396 
   397 text {* Proving reflexivity *}
   398 
   399 definition reflp' :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where "reflp' R \<equiv> reflp R"
   400 
   401 lemma Quotient_to_left_total:
   402   assumes q: "Quotient R Abs Rep T"
   403   and r_R: "reflp R"
   404   shows "left_total T"
   405 using r_R Quotient_cr_rel[OF q] unfolding left_total_def by (auto elim: reflpE)
   406 
   407 lemma reflp_Quotient_composition:
   408   assumes "left_total R"
   409   assumes "reflp T"
   410   shows "reflp (R OO T OO R\<inverse>\<inverse>)"
   411 using assms unfolding reflp_def left_total_def by fast
   412 
   413 lemma reflp_fun1:
   414   assumes "is_equality R"
   415   assumes "reflp' S"
   416   shows "reflp (R ===> S)"
   417 using assms unfolding is_equality_def reflp'_def reflp_def fun_rel_def by blast
   418 
   419 lemma reflp_fun2:
   420   assumes "is_equality R"
   421   assumes "is_equality S"
   422   shows "reflp (R ===> S)"
   423 using assms unfolding is_equality_def reflp_def fun_rel_def by blast
   424 
   425 lemma is_equality_Quotient_composition:
   426   assumes "is_equality T"
   427   assumes "left_total R"
   428   assumes "left_unique R"
   429   shows "is_equality (R OO T OO R\<inverse>\<inverse>)"
   430 using assms unfolding is_equality_def left_total_def left_unique_def OO_def conversep_iff
   431 by fastforce
   432 
   433 lemma left_total_composition: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
   434 unfolding left_total_def OO_def by fast
   435 
   436 lemma left_unique_composition: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
   437 unfolding left_unique_def OO_def by fast
   438 
   439 lemma reflp_equality: "reflp (op =)"
   440 by (auto intro: reflpI)
   441 
   442 text {* Proving a parametrized correspondence relation *}
   443 
   444 lemma eq_OO: "op= OO R = R"
   445 unfolding OO_def by metis
   446 
   447 definition POS :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
   448 "POS A B \<equiv> A \<le> B"
   449 
   450 definition  NEG :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
   451 "NEG A B \<equiv> B \<le> A"
   452 
   453 (*
   454   The following two rules are here because we don't have any proper
   455   left-unique ant left-total relations. Left-unique and left-total
   456   assumptions show up in distributivity rules for the function type.
   457 *)
   458 
   459 lemma bi_unique_left_unique[transfer_rule]: "bi_unique R \<Longrightarrow> left_unique R"
   460 unfolding bi_unique_def left_unique_def by blast
   461 
   462 lemma bi_total_left_total[transfer_rule]: "bi_total R \<Longrightarrow> left_total R"
   463 unfolding bi_total_def left_total_def by blast
   464 
   465 lemma pos_OO_eq:
   466   shows "POS (A OO op=) A"
   467 unfolding POS_def OO_def by blast
   468 
   469 lemma pos_eq_OO:
   470   shows "POS (op= OO A) A"
   471 unfolding POS_def OO_def by blast
   472 
   473 lemma neg_OO_eq:
   474   shows "NEG (A OO op=) A"
   475 unfolding NEG_def OO_def by auto
   476 
   477 lemma neg_eq_OO:
   478   shows "NEG (op= OO A) A"
   479 unfolding NEG_def OO_def by blast
   480 
   481 lemma POS_trans:
   482   assumes "POS A B"
   483   assumes "POS B C"
   484   shows "POS A C"
   485 using assms unfolding POS_def by auto
   486 
   487 lemma NEG_trans:
   488   assumes "NEG A B"
   489   assumes "NEG B C"
   490   shows "NEG A C"
   491 using assms unfolding NEG_def by auto
   492 
   493 lemma POS_NEG:
   494   "POS A B \<equiv> NEG B A"
   495   unfolding POS_def NEG_def by auto
   496 
   497 lemma NEG_POS:
   498   "NEG A B \<equiv> POS B A"
   499   unfolding POS_def NEG_def by auto
   500 
   501 lemma POS_pcr_rule:
   502   assumes "POS (A OO B) C"
   503   shows "POS (A OO B OO X) (C OO X)"
   504 using assms unfolding POS_def OO_def by blast
   505 
   506 lemma NEG_pcr_rule:
   507   assumes "NEG (A OO B) C"
   508   shows "NEG (A OO B OO X) (C OO X)"
   509 using assms unfolding NEG_def OO_def by blast
   510 
   511 lemma POS_apply:
   512   assumes "POS R R'"
   513   assumes "R f g"
   514   shows "R' f g"
   515 using assms unfolding POS_def by auto
   516 
   517 text {* Proving a parametrized correspondence relation *}
   518 
   519 lemma fun_mono:
   520   assumes "A \<ge> C"
   521   assumes "B \<le> D"
   522   shows   "(A ===> B) \<le> (C ===> D)"
   523 using assms unfolding fun_rel_def by blast
   524 
   525 lemma pos_fun_distr: "((R ===> S) OO (R' ===> S')) \<le> ((R OO R') ===> (S OO S'))"
   526 unfolding OO_def fun_rel_def by blast
   527 
   528 lemma functional_relation: "right_unique R \<Longrightarrow> left_total R \<Longrightarrow> \<forall>x. \<exists>!y. R x y"
   529 unfolding right_unique_def left_total_def by blast
   530 
   531 lemma functional_converse_relation: "left_unique R \<Longrightarrow> right_total R \<Longrightarrow> \<forall>y. \<exists>!x. R x y"
   532 unfolding left_unique_def right_total_def by blast
   533 
   534 lemma neg_fun_distr1:
   535 assumes 1: "left_unique R" "right_total R"
   536 assumes 2: "right_unique R'" "left_total R'"
   537 shows "(R OO R' ===> S OO S') \<le> ((R ===> S) OO (R' ===> S')) "
   538   using functional_relation[OF 2] functional_converse_relation[OF 1]
   539   unfolding fun_rel_def OO_def
   540   apply clarify
   541   apply (subst all_comm)
   542   apply (subst all_conj_distrib[symmetric])
   543   apply (intro choice)
   544   by metis
   545 
   546 lemma neg_fun_distr2:
   547 assumes 1: "right_unique R'" "left_total R'"
   548 assumes 2: "left_unique S'" "right_total S'"
   549 shows "(R OO R' ===> S OO S') \<le> ((R ===> S) OO (R' ===> S'))"
   550   using functional_converse_relation[OF 2] functional_relation[OF 1]
   551   unfolding fun_rel_def OO_def
   552   apply clarify
   553   apply (subst all_comm)
   554   apply (subst all_conj_distrib[symmetric])
   555   apply (intro choice)
   556   by metis
   557 
   558 subsection {* Domains *}
   559 
   560 lemma pcr_Domainp_par_left_total:
   561   assumes "Domainp B = P"
   562   assumes "left_total A"
   563   assumes "(A ===> op=) P' P"
   564   shows "Domainp (A OO B) = P'"
   565 using assms
   566 unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def fun_rel_def 
   567 by (fast intro: fun_eq_iff)
   568 
   569 lemma pcr_Domainp_par:
   570 assumes "Domainp B = P2"
   571 assumes "Domainp A = P1"
   572 assumes "(A ===> op=) P2' P2"
   573 shows "Domainp (A OO B) = (inf P1 P2')"
   574 using assms unfolding fun_rel_def Domainp_iff[abs_def] OO_def
   575 by (fast intro: fun_eq_iff)
   576 
   577 definition rel_pred_comp :: "('a => 'b => bool) => ('b => bool) => 'a => bool"  (infixr "OP" 75)
   578 where "rel_pred_comp R P \<equiv> \<lambda>x. \<exists>y. R x y \<and> P y"
   579 
   580 lemma pcr_Domainp:
   581 assumes "Domainp B = P"
   582 shows "Domainp (A OO B) = (A OP P)"
   583 using assms unfolding rel_pred_comp_def by blast
   584 
   585 lemma pcr_Domainp_total:
   586   assumes "bi_total B"
   587   assumes "Domainp A = P"
   588   shows "Domainp (A OO B) = P"
   589 using assms unfolding bi_total_def 
   590 by fast
   591 
   592 lemma Quotient_to_Domainp:
   593   assumes "Quotient R Abs Rep T"
   594   shows "Domainp T = (\<lambda>x. R x x)"  
   595 by (simp add: Domainp_iff[abs_def] Quotient_cr_rel[OF assms])
   596 
   597 lemma invariant_to_Domainp:
   598   assumes "Quotient (Lifting.invariant P) Abs Rep T"
   599   shows "Domainp T = P"
   600 by (simp add: invariant_def Domainp_iff[abs_def] Quotient_cr_rel[OF assms])
   601 
   602 subsection {* ML setup *}
   603 
   604 ML_file "Tools/Lifting/lifting_util.ML"
   605 
   606 ML_file "Tools/Lifting/lifting_info.ML"
   607 setup Lifting_Info.setup
   608 
   609 lemmas [reflexivity_rule] = 
   610   reflp_equality reflp_Quotient_composition is_equality_Quotient_composition 
   611   left_total_fun left_unique_fun left_total_eq left_unique_eq left_total_composition
   612   left_unique_composition
   613 
   614 text {* add @{thm reflp_fun1} and @{thm reflp_fun2} manually through ML
   615   because we don't want to get reflp' variant of these theorems *}
   616 
   617 setup{*
   618 Context.theory_map 
   619   (fold
   620     (snd oo (Thm.apply_attribute Lifting_Info.add_reflexivity_rule_raw_attribute)) 
   621       [@{thm reflp_fun1}, @{thm reflp_fun2}])
   622 *}
   623 
   624 (* setup for the function type *)
   625 declare fun_quotient[quot_map]
   626 declare fun_mono[relator_mono]
   627 lemmas [relator_distr] = pos_fun_distr neg_fun_distr1 neg_fun_distr2
   628 
   629 ML_file "Tools/Lifting/lifting_term.ML"
   630 
   631 ML_file "Tools/Lifting/lifting_def.ML"
   632 
   633 ML_file "Tools/Lifting/lifting_setup.ML"
   634 
   635 hide_const (open) invariant POS NEG reflp'
   636 
   637 end