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