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