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