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