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