src/HOL/Lifting.thy
author nipkow
Wed Dec 20 14:53:34 2017 +0100 (18 months ago)
changeset 67229 4ecf0ef70efb
parent 63343 fb5d8a50c641
child 67399 eab6ce8368fa
permissions -rw-r--r--
tuned op's
     1 (*  Title:      HOL/Lifting.thy
     2     Author:     Brian Huffman and Ondrej Kuncar
     3     Author:     Cezary Kaliszyk and Christian Urban
     4 *)
     5 
     6 section \<open>Lifting package\<close>
     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" "lifting_forget" "lifting_update" :: thy_decl
    15 begin
    16 
    17 subsection \<open>Function map\<close>
    18 
    19 context includes lifting_syntax
    20 begin
    21 
    22 lemma map_fun_id:
    23   "(id ---> id) = id"
    24   by (simp add: fun_eq_iff)
    25 
    26 subsection \<open>Quotient Predicate\<close>
    27 
    28 definition
    29   "Quotient R Abs Rep T \<longleftrightarrow>
    30      (\<forall>a. Abs (Rep a) = a) \<and>
    31      (\<forall>a. R (Rep a) (Rep a)) \<and>
    32      (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s) \<and>
    33      T = (\<lambda>x y. R x x \<and> Abs x = y)"
    34 
    35 lemma QuotientI:
    36   assumes "\<And>a. Abs (Rep a) = a"
    37     and "\<And>a. R (Rep a) (Rep a)"
    38     and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s"
    39     and "T = (\<lambda>x y. R x x \<and> Abs x = y)"
    40   shows "Quotient R Abs Rep T"
    41   using assms unfolding Quotient_def by blast
    42 
    43 context
    44   fixes R Abs Rep T
    45   assumes a: "Quotient R Abs Rep T"
    46 begin
    47 
    48 lemma Quotient_abs_rep: "Abs (Rep a) = a"
    49   using a unfolding Quotient_def
    50   by simp
    51 
    52 lemma Quotient_rep_reflp: "R (Rep a) (Rep a)"
    53   using a unfolding Quotient_def
    54   by blast
    55 
    56 lemma Quotient_rel:
    57   "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" \<comment> \<open>orientation does not loop on rewriting\<close>
    58   using a unfolding Quotient_def
    59   by blast
    60 
    61 lemma Quotient_cr_rel: "T = (\<lambda>x y. R x x \<and> Abs x = y)"
    62   using a unfolding Quotient_def
    63   by blast
    64 
    65 lemma Quotient_refl1: "R r s \<Longrightarrow> R r r"
    66   using a unfolding Quotient_def
    67   by fast
    68 
    69 lemma Quotient_refl2: "R r s \<Longrightarrow> R s s"
    70   using a unfolding Quotient_def
    71   by fast
    72 
    73 lemma Quotient_rel_rep: "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
    74   using a unfolding Quotient_def
    75   by metis
    76 
    77 lemma Quotient_rep_abs: "R r r \<Longrightarrow> R (Rep (Abs r)) r"
    78   using a unfolding Quotient_def
    79   by blast
    80 
    81 lemma Quotient_rep_abs_eq: "R t t \<Longrightarrow> R \<le> op= \<Longrightarrow> Rep (Abs t) = t"
    82   using a unfolding Quotient_def
    83   by blast
    84 
    85 lemma Quotient_rep_abs_fold_unmap:
    86   assumes "x' \<equiv> Abs x" and "R x x" and "Rep x' \<equiv> Rep' x'"
    87   shows "R (Rep' x') x"
    88 proof -
    89   have "R (Rep x') x" using assms(1-2) Quotient_rep_abs by auto
    90   then show ?thesis using assms(3) by simp
    91 qed
    92 
    93 lemma Quotient_Rep_eq:
    94   assumes "x' \<equiv> Abs x"
    95   shows "Rep x' \<equiv> Rep x'"
    96 by simp
    97 
    98 lemma Quotient_rel_abs: "R r s \<Longrightarrow> Abs r = Abs s"
    99   using a unfolding Quotient_def
   100   by blast
   101 
   102 lemma Quotient_rel_abs2:
   103   assumes "R (Rep x) y"
   104   shows "x = Abs y"
   105 proof -
   106   from assms have "Abs (Rep x) = Abs y" by (auto intro: Quotient_rel_abs)
   107   then show ?thesis using assms(1) by (simp add: Quotient_abs_rep)
   108 qed
   109 
   110 lemma Quotient_symp: "symp R"
   111   using a unfolding Quotient_def using sympI by (metis (full_types))
   112 
   113 lemma Quotient_transp: "transp R"
   114   using a unfolding Quotient_def using transpI by (metis (full_types))
   115 
   116 lemma Quotient_part_equivp: "part_equivp R"
   117 by (metis Quotient_rep_reflp Quotient_symp Quotient_transp part_equivpI)
   118 
   119 end
   120 
   121 lemma identity_quotient: "Quotient (op =) id id (op =)"
   122 unfolding Quotient_def by simp
   123 
   124 text \<open>TODO: Use one of these alternatives as the real definition.\<close>
   125 
   126 lemma Quotient_alt_def:
   127   "Quotient R Abs Rep T \<longleftrightarrow>
   128     (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and>
   129     (\<forall>b. T (Rep b) b) \<and>
   130     (\<forall>x y. R x y \<longleftrightarrow> T x (Abs x) \<and> T y (Abs y) \<and> Abs x = Abs y)"
   131 apply safe
   132 apply (simp (no_asm_use) only: Quotient_def, fast)
   133 apply (simp (no_asm_use) only: Quotient_def, fast)
   134 apply (simp (no_asm_use) only: Quotient_def, fast)
   135 apply (simp (no_asm_use) only: Quotient_def, fast)
   136 apply (simp (no_asm_use) only: Quotient_def, fast)
   137 apply (simp (no_asm_use) only: Quotient_def, fast)
   138 apply (rule QuotientI)
   139 apply simp
   140 apply metis
   141 apply simp
   142 apply (rule ext, rule ext, metis)
   143 done
   144 
   145 lemma Quotient_alt_def2:
   146   "Quotient R Abs Rep T \<longleftrightarrow>
   147     (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and>
   148     (\<forall>b. T (Rep b) b) \<and>
   149     (\<forall>x y. R x y \<longleftrightarrow> T x (Abs y) \<and> T y (Abs x))"
   150   unfolding Quotient_alt_def by (safe, metis+)
   151 
   152 lemma Quotient_alt_def3:
   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>
   155     (\<forall>x y. R x y \<longleftrightarrow> (\<exists>z. T x z \<and> T y z))"
   156   unfolding Quotient_alt_def2 by (safe, metis+)
   157 
   158 lemma Quotient_alt_def4:
   159   "Quotient R Abs Rep T \<longleftrightarrow>
   160     (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> (\<forall>b. T (Rep b) b) \<and> R = T OO conversep T"
   161   unfolding Quotient_alt_def3 fun_eq_iff by auto
   162 
   163 lemma Quotient_alt_def5:
   164   "Quotient R Abs Rep T \<longleftrightarrow>
   165     T \<le> BNF_Def.Grp UNIV Abs \<and> BNF_Def.Grp UNIV Rep \<le> T\<inverse>\<inverse> \<and> R = T OO T\<inverse>\<inverse>"
   166   unfolding Quotient_alt_def4 Grp_def by blast
   167 
   168 lemma fun_quotient:
   169   assumes 1: "Quotient R1 abs1 rep1 T1"
   170   assumes 2: "Quotient R2 abs2 rep2 T2"
   171   shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2) (T1 ===> T2)"
   172   using assms unfolding Quotient_alt_def2
   173   unfolding rel_fun_def fun_eq_iff map_fun_apply
   174   by (safe, metis+)
   175 
   176 lemma apply_rsp:
   177   fixes f g::"'a \<Rightarrow> 'c"
   178   assumes q: "Quotient R1 Abs1 Rep1 T1"
   179   and     a: "(R1 ===> R2) f g" "R1 x y"
   180   shows "R2 (f x) (g y)"
   181   using a by (auto elim: rel_funE)
   182 
   183 lemma apply_rsp':
   184   assumes a: "(R1 ===> R2) f g" "R1 x y"
   185   shows "R2 (f x) (g y)"
   186   using a by (auto elim: rel_funE)
   187 
   188 lemma apply_rsp'':
   189   assumes "Quotient R Abs Rep T"
   190   and "(R ===> S) f f"
   191   shows "S (f (Rep x)) (f (Rep x))"
   192 proof -
   193   from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp)
   194   then show ?thesis using assms(2) by (auto intro: apply_rsp')
   195 qed
   196 
   197 subsection \<open>Quotient composition\<close>
   198 
   199 lemma Quotient_compose:
   200   assumes 1: "Quotient R1 Abs1 Rep1 T1"
   201   assumes 2: "Quotient R2 Abs2 Rep2 T2"
   202   shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2) (T1 OO T2)"
   203   using assms unfolding Quotient_alt_def4 by fastforce
   204 
   205 lemma equivp_reflp2:
   206   "equivp R \<Longrightarrow> reflp R"
   207   by (erule equivpE)
   208 
   209 subsection \<open>Respects predicate\<close>
   210 
   211 definition Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set"
   212   where "Respects R = {x. R x x}"
   213 
   214 lemma in_respects: "x \<in> Respects R \<longleftrightarrow> R x x"
   215   unfolding Respects_def by simp
   216 
   217 lemma UNIV_typedef_to_Quotient:
   218   assumes "type_definition Rep Abs UNIV"
   219   and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   220   shows "Quotient (op =) Abs Rep T"
   221 proof -
   222   interpret type_definition Rep Abs UNIV by fact
   223   from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
   224     by (fastforce intro!: QuotientI fun_eq_iff)
   225 qed
   226 
   227 lemma UNIV_typedef_to_equivp:
   228   fixes Abs :: "'a \<Rightarrow> 'b"
   229   and Rep :: "'b \<Rightarrow> 'a"
   230   assumes "type_definition Rep Abs (UNIV::'a set)"
   231   shows "equivp (op= ::'a\<Rightarrow>'a\<Rightarrow>bool)"
   232 by (rule identity_equivp)
   233 
   234 lemma typedef_to_Quotient:
   235   assumes "type_definition Rep Abs S"
   236   and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   237   shows "Quotient (eq_onp (\<lambda>x. x \<in> S)) Abs Rep T"
   238 proof -
   239   interpret type_definition Rep Abs S by fact
   240   from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
   241     by (auto intro!: QuotientI simp: eq_onp_def fun_eq_iff)
   242 qed
   243 
   244 lemma typedef_to_part_equivp:
   245   assumes "type_definition Rep Abs S"
   246   shows "part_equivp (eq_onp (\<lambda>x. x \<in> S))"
   247 proof (intro part_equivpI)
   248   interpret type_definition Rep Abs S by fact
   249   show "\<exists>x. eq_onp (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: eq_onp_def)
   250 next
   251   show "symp (eq_onp (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: eq_onp_def)
   252 next
   253   show "transp (eq_onp (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: eq_onp_def)
   254 qed
   255 
   256 lemma open_typedef_to_Quotient:
   257   assumes "type_definition Rep Abs {x. P x}"
   258   and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
   259   shows "Quotient (eq_onp P) Abs Rep T"
   260   using typedef_to_Quotient [OF assms] by simp
   261 
   262 lemma open_typedef_to_part_equivp:
   263   assumes "type_definition Rep Abs {x. P x}"
   264   shows "part_equivp (eq_onp P)"
   265   using typedef_to_part_equivp [OF assms] by simp
   266 
   267 lemma type_definition_Quotient_not_empty: "Quotient (eq_onp P) Abs Rep T \<Longrightarrow> \<exists>x. P x"
   268 unfolding eq_onp_def by (drule Quotient_rep_reflp) blast
   269 
   270 lemma type_definition_Quotient_not_empty_witness: "Quotient (eq_onp P) Abs Rep T \<Longrightarrow> P (Rep undefined)"
   271 unfolding eq_onp_def by (drule Quotient_rep_reflp) blast
   272 
   273 
   274 text \<open>Generating transfer rules for quotients.\<close>
   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 rel_fun_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 end
   295 
   296 text \<open>Generating transfer rules for total quotients.\<close>
   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_left_total: "left_total T"
   304   using 1 2 unfolding Quotient_alt_def left_total_def reflp_def by auto
   305 
   306 lemma Quotient_bi_total: "bi_total T"
   307   using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto
   308 
   309 lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs"
   310   using 1 2 unfolding Quotient_alt_def reflp_def rel_fun_def by simp
   311 
   312 lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x"
   313   using 1 2 unfolding Quotient_alt_def reflp_def by metis
   314 
   315 lemma Quotient_total_abs_eq_iff: "Abs x = Abs y \<longleftrightarrow> R x y"
   316   using Quotient_rel [OF 1] 2 unfolding reflp_def by simp
   317 
   318 end
   319 
   320 text \<open>Generating transfer rules for a type defined with \<open>typedef\<close>.\<close>
   321 
   322 context
   323   fixes Rep Abs A T
   324   assumes type: "type_definition Rep Abs A"
   325   assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)"
   326 begin
   327 
   328 lemma typedef_left_unique: "left_unique T"
   329   unfolding left_unique_def T_def
   330   by (simp add: type_definition.Rep_inject [OF type])
   331 
   332 lemma typedef_bi_unique: "bi_unique T"
   333   unfolding bi_unique_def T_def
   334   by (simp add: type_definition.Rep_inject [OF type])
   335 
   336 (* the following two theorems are here only for convinience *)
   337 
   338 lemma typedef_right_unique: "right_unique T"
   339   using T_def type Quotient_right_unique typedef_to_Quotient
   340   by blast
   341 
   342 lemma typedef_right_total: "right_total T"
   343   using T_def type Quotient_right_total typedef_to_Quotient
   344   by blast
   345 
   346 lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
   347   unfolding rel_fun_def T_def by simp
   348 
   349 end
   350 
   351 text \<open>Generating the correspondence rule for a constant defined with
   352   \<open>lift_definition\<close>.\<close>
   353 
   354 lemma Quotient_to_transfer:
   355   assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c"
   356   shows "T c c'"
   357   using assms by (auto dest: Quotient_cr_rel)
   358 
   359 text \<open>Proving reflexivity\<close>
   360 
   361 lemma Quotient_to_left_total:
   362   assumes q: "Quotient R Abs Rep T"
   363   and r_R: "reflp R"
   364   shows "left_total T"
   365 using r_R Quotient_cr_rel[OF q] unfolding left_total_def by (auto elim: reflpE)
   366 
   367 lemma Quotient_composition_ge_eq:
   368   assumes "left_total T"
   369   assumes "R \<ge> op="
   370   shows "(T OO R OO T\<inverse>\<inverse>) \<ge> op="
   371 using assms unfolding left_total_def by fast
   372 
   373 lemma Quotient_composition_le_eq:
   374   assumes "left_unique T"
   375   assumes "R \<le> op="
   376   shows "(T OO R OO T\<inverse>\<inverse>) \<le> op="
   377 using assms unfolding left_unique_def by blast
   378 
   379 lemma eq_onp_le_eq:
   380   "eq_onp P \<le> op=" unfolding eq_onp_def by blast
   381 
   382 lemma reflp_ge_eq:
   383   "reflp R \<Longrightarrow> R \<ge> op=" unfolding reflp_def by blast
   384 
   385 text \<open>Proving a parametrized correspondence relation\<close>
   386 
   387 definition POS :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
   388 "POS A B \<equiv> A \<le> B"
   389 
   390 definition  NEG :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
   391 "NEG A B \<equiv> B \<le> A"
   392 
   393 lemma pos_OO_eq:
   394   shows "POS (A OO op=) A"
   395 unfolding POS_def OO_def by blast
   396 
   397 lemma pos_eq_OO:
   398   shows "POS (op= OO A) A"
   399 unfolding POS_def OO_def by blast
   400 
   401 lemma neg_OO_eq:
   402   shows "NEG (A OO op=) A"
   403 unfolding NEG_def OO_def by auto
   404 
   405 lemma neg_eq_OO:
   406   shows "NEG (op= OO A) A"
   407 unfolding NEG_def OO_def by blast
   408 
   409 lemma POS_trans:
   410   assumes "POS A B"
   411   assumes "POS B C"
   412   shows "POS A C"
   413 using assms unfolding POS_def by auto
   414 
   415 lemma NEG_trans:
   416   assumes "NEG A B"
   417   assumes "NEG B C"
   418   shows "NEG A C"
   419 using assms unfolding NEG_def by auto
   420 
   421 lemma POS_NEG:
   422   "POS A B \<equiv> NEG B A"
   423   unfolding POS_def NEG_def by auto
   424 
   425 lemma NEG_POS:
   426   "NEG A B \<equiv> POS B A"
   427   unfolding POS_def NEG_def by auto
   428 
   429 lemma POS_pcr_rule:
   430   assumes "POS (A OO B) C"
   431   shows "POS (A OO B OO X) (C OO X)"
   432 using assms unfolding POS_def OO_def by blast
   433 
   434 lemma NEG_pcr_rule:
   435   assumes "NEG (A OO B) C"
   436   shows "NEG (A OO B OO X) (C OO X)"
   437 using assms unfolding NEG_def OO_def by blast
   438 
   439 lemma POS_apply:
   440   assumes "POS R R'"
   441   assumes "R f g"
   442   shows "R' f g"
   443 using assms unfolding POS_def by auto
   444 
   445 text \<open>Proving a parametrized correspondence relation\<close>
   446 
   447 lemma fun_mono:
   448   assumes "A \<ge> C"
   449   assumes "B \<le> D"
   450   shows   "(A ===> B) \<le> (C ===> D)"
   451 using assms unfolding rel_fun_def by blast
   452 
   453 lemma pos_fun_distr: "((R ===> S) OO (R' ===> S')) \<le> ((R OO R') ===> (S OO S'))"
   454 unfolding OO_def rel_fun_def by blast
   455 
   456 lemma functional_relation: "right_unique R \<Longrightarrow> left_total R \<Longrightarrow> \<forall>x. \<exists>!y. R x y"
   457 unfolding right_unique_def left_total_def by blast
   458 
   459 lemma functional_converse_relation: "left_unique R \<Longrightarrow> right_total R \<Longrightarrow> \<forall>y. \<exists>!x. R x y"
   460 unfolding left_unique_def right_total_def by blast
   461 
   462 lemma neg_fun_distr1:
   463 assumes 1: "left_unique R" "right_total R"
   464 assumes 2: "right_unique R'" "left_total R'"
   465 shows "(R OO R' ===> S OO S') \<le> ((R ===> S) OO (R' ===> S')) "
   466   using functional_relation[OF 2] functional_converse_relation[OF 1]
   467   unfolding rel_fun_def OO_def
   468   apply clarify
   469   apply (subst all_comm)
   470   apply (subst all_conj_distrib[symmetric])
   471   apply (intro choice)
   472   by metis
   473 
   474 lemma neg_fun_distr2:
   475 assumes 1: "right_unique R'" "left_total R'"
   476 assumes 2: "left_unique S'" "right_total S'"
   477 shows "(R OO R' ===> S OO S') \<le> ((R ===> S) OO (R' ===> S'))"
   478   using functional_converse_relation[OF 2] functional_relation[OF 1]
   479   unfolding rel_fun_def OO_def
   480   apply clarify
   481   apply (subst all_comm)
   482   apply (subst all_conj_distrib[symmetric])
   483   apply (intro choice)
   484   by metis
   485 
   486 subsection \<open>Domains\<close>
   487 
   488 lemma composed_equiv_rel_eq_onp:
   489   assumes "left_unique R"
   490   assumes "(R ===> op=) P P'"
   491   assumes "Domainp R = P''"
   492   shows "(R OO eq_onp P' OO R\<inverse>\<inverse>) = eq_onp (inf P'' P)"
   493 using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def rel_fun_def eq_onp_def
   494 fun_eq_iff by blast
   495 
   496 lemma composed_equiv_rel_eq_eq_onp:
   497   assumes "left_unique R"
   498   assumes "Domainp R = P"
   499   shows "(R OO op= OO R\<inverse>\<inverse>) = eq_onp P"
   500 using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def eq_onp_def
   501 fun_eq_iff is_equality_def by metis
   502 
   503 lemma pcr_Domainp_par_left_total:
   504   assumes "Domainp B = P"
   505   assumes "left_total A"
   506   assumes "(A ===> op=) P' P"
   507   shows "Domainp (A OO B) = P'"
   508 using assms
   509 unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def rel_fun_def
   510 by (fast intro: fun_eq_iff)
   511 
   512 lemma pcr_Domainp_par:
   513 assumes "Domainp B = P2"
   514 assumes "Domainp A = P1"
   515 assumes "(A ===> op=) P2' P2"
   516 shows "Domainp (A OO B) = (inf P1 P2')"
   517 using assms unfolding rel_fun_def Domainp_iff[abs_def] OO_def
   518 by (fast intro: fun_eq_iff)
   519 
   520 definition rel_pred_comp :: "('a => 'b => bool) => ('b => bool) => 'a => bool"
   521 where "rel_pred_comp R P \<equiv> \<lambda>x. \<exists>y. R x y \<and> P y"
   522 
   523 lemma pcr_Domainp:
   524 assumes "Domainp B = P"
   525 shows "Domainp (A OO B) = (\<lambda>x. \<exists>y. A x y \<and> P y)"
   526 using assms by blast
   527 
   528 lemma pcr_Domainp_total:
   529   assumes "left_total B"
   530   assumes "Domainp A = P"
   531   shows "Domainp (A OO B) = P"
   532 using assms unfolding left_total_def
   533 by fast
   534 
   535 lemma Quotient_to_Domainp:
   536   assumes "Quotient R Abs Rep T"
   537   shows "Domainp T = (\<lambda>x. R x x)"
   538 by (simp add: Domainp_iff[abs_def] Quotient_cr_rel[OF assms])
   539 
   540 lemma eq_onp_to_Domainp:
   541   assumes "Quotient (eq_onp P) Abs Rep T"
   542   shows "Domainp T = P"
   543 by (simp add: eq_onp_def Domainp_iff[abs_def] Quotient_cr_rel[OF assms])
   544 
   545 end
   546 
   547 (* needed for lifting_def_code_dt.ML (moved from Lifting_Set) *)
   548 lemma right_total_UNIV_transfer: 
   549   assumes "right_total A"
   550   shows "(rel_set A) (Collect (Domainp A)) UNIV"
   551   using assms unfolding right_total_def rel_set_def Domainp_iff by blast
   552 
   553 subsection \<open>ML setup\<close>
   554 
   555 ML_file "Tools/Lifting/lifting_util.ML"
   556 
   557 named_theorems relator_eq_onp
   558   "theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate"
   559 ML_file "Tools/Lifting/lifting_info.ML"
   560 
   561 (* setup for the function type *)
   562 declare fun_quotient[quot_map]
   563 declare fun_mono[relator_mono]
   564 lemmas [relator_distr] = pos_fun_distr neg_fun_distr1 neg_fun_distr2
   565 
   566 ML_file "Tools/Lifting/lifting_bnf.ML"
   567 ML_file "Tools/Lifting/lifting_term.ML"
   568 ML_file "Tools/Lifting/lifting_def.ML"
   569 ML_file "Tools/Lifting/lifting_setup.ML"
   570 ML_file "Tools/Lifting/lifting_def_code_dt.ML"
   571 
   572 lemma pred_prod_beta: "pred_prod P Q xy \<longleftrightarrow> P (fst xy) \<and> Q (snd xy)"
   573 by(cases xy) simp
   574 
   575 lemma pred_prod_split: "P (pred_prod Q R xy) \<longleftrightarrow> (\<forall>x y. xy = (x, y) \<longrightarrow> P (Q x \<and> R y))"
   576 by(cases xy) simp
   577 
   578 hide_const (open) POS NEG
   579 
   580 end