src/HOL/Quotient.thy
author blanchet
Thu Nov 21 21:33:34 2013 +0100 (2013-11-21)
changeset 54555 e8c5e95d338b
parent 53011 aeee0a4be6cf
child 54867 c21a2465cac1
permissions -rw-r--r--
rationalize imports
     1 (*  Title:      HOL/Quotient.thy
     2     Author:     Cezary Kaliszyk and Christian Urban
     3 *)
     4 
     5 header {* Definition of Quotient Types *}
     6 
     7 theory Quotient
     8 imports Lifting
     9 keywords
    10   "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and
    11   "quotient_type" :: thy_goal and "/" and
    12   "quotient_definition" :: thy_goal
    13 begin
    14 
    15 text {*
    16   Basic definition for equivalence relations
    17   that are represented by predicates.
    18 *}
    19 
    20 text {* Composition of Relations *}
    21 
    22 abbreviation
    23   rel_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" (infixr "OOO" 75)
    24 where
    25   "r1 OOO r2 \<equiv> r1 OO r2 OO r1"
    26 
    27 lemma eq_comp_r:
    28   shows "((op =) OOO R) = R"
    29   by (auto simp add: fun_eq_iff)
    30 
    31 context
    32 begin
    33 interpretation lifting_syntax .
    34 
    35 subsection {* Quotient Predicate *}
    36 
    37 definition
    38   "Quotient3 R Abs Rep \<longleftrightarrow>
    39      (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. R (Rep a) (Rep a)) \<and>
    40      (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s)"
    41 
    42 lemma Quotient3I:
    43   assumes "\<And>a. Abs (Rep a) = a"
    44     and "\<And>a. R (Rep a) (Rep a)"
    45     and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s"
    46   shows "Quotient3 R Abs Rep"
    47   using assms unfolding Quotient3_def by blast
    48 
    49 lemma Quotient3_abs_rep:
    50   assumes a: "Quotient3 R Abs Rep"
    51   shows "Abs (Rep a) = a"
    52   using a
    53   unfolding Quotient3_def
    54   by simp
    55 
    56 lemma Quotient3_rep_reflp:
    57   assumes a: "Quotient3 R Abs Rep"
    58   shows "R (Rep a) (Rep a)"
    59   using a
    60   unfolding Quotient3_def
    61   by blast
    62 
    63 lemma Quotient3_rel:
    64   assumes a: "Quotient3 R Abs Rep"
    65   shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
    66   using a
    67   unfolding Quotient3_def
    68   by blast
    69 
    70 lemma Quotient3_refl1: 
    71   assumes a: "Quotient3 R Abs Rep" 
    72   shows "R r s \<Longrightarrow> R r r"
    73   using a unfolding Quotient3_def 
    74   by fast
    75 
    76 lemma Quotient3_refl2: 
    77   assumes a: "Quotient3 R Abs Rep" 
    78   shows "R r s \<Longrightarrow> R s s"
    79   using a unfolding Quotient3_def 
    80   by fast
    81 
    82 lemma Quotient3_rel_rep:
    83   assumes a: "Quotient3 R Abs Rep"
    84   shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
    85   using a
    86   unfolding Quotient3_def
    87   by metis
    88 
    89 lemma Quotient3_rep_abs:
    90   assumes a: "Quotient3 R Abs Rep"
    91   shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
    92   using a unfolding Quotient3_def
    93   by blast
    94 
    95 lemma Quotient3_rel_abs:
    96   assumes a: "Quotient3 R Abs Rep"
    97   shows "R r s \<Longrightarrow> Abs r = Abs s"
    98   using a unfolding Quotient3_def
    99   by blast
   100 
   101 lemma Quotient3_symp:
   102   assumes a: "Quotient3 R Abs Rep"
   103   shows "symp R"
   104   using a unfolding Quotient3_def using sympI by metis
   105 
   106 lemma Quotient3_transp:
   107   assumes a: "Quotient3 R Abs Rep"
   108   shows "transp R"
   109   using a unfolding Quotient3_def using transpI by (metis (full_types))
   110 
   111 lemma Quotient3_part_equivp:
   112   assumes a: "Quotient3 R Abs Rep"
   113   shows "part_equivp R"
   114 by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp a part_equivpI)
   115 
   116 lemma identity_quotient3:
   117   shows "Quotient3 (op =) id id"
   118   unfolding Quotient3_def id_def
   119   by blast
   120 
   121 lemma fun_quotient3:
   122   assumes q1: "Quotient3 R1 abs1 rep1"
   123   and     q2: "Quotient3 R2 abs2 rep2"
   124   shows "Quotient3 (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
   125 proof -
   126   have "\<And>a.(rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
   127     using q1 q2 by (simp add: Quotient3_def fun_eq_iff)
   128   moreover
   129   have "\<And>a.(R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
   130     by (rule fun_relI)
   131       (insert q1 q2 Quotient3_rel_abs [of R1 abs1 rep1] Quotient3_rel_rep [of R2 abs2 rep2],
   132         simp (no_asm) add: Quotient3_def, simp)
   133   
   134   moreover
   135   {
   136   fix r s
   137   have "(R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
   138         (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
   139   proof -
   140     
   141     have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) r r" unfolding fun_rel_def
   142       using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] 
   143       by (metis (full_types) part_equivp_def)
   144     moreover have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) s s" unfolding fun_rel_def
   145       using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] 
   146       by (metis (full_types) part_equivp_def)
   147     moreover have "(R1 ===> R2) r s \<Longrightarrow> (rep1 ---> abs2) r  = (rep1 ---> abs2) s"
   148       apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def by metis
   149     moreover have "((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
   150         (rep1 ---> abs2) r  = (rep1 ---> abs2) s) \<Longrightarrow> (R1 ===> R2) r s"
   151       apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def 
   152     by (metis map_fun_apply)
   153   
   154     ultimately show ?thesis by blast
   155  qed
   156  }
   157  ultimately show ?thesis by (intro Quotient3I) (assumption+)
   158 qed
   159 
   160 lemma abs_o_rep:
   161   assumes a: "Quotient3 R Abs Rep"
   162   shows "Abs o Rep = id"
   163   unfolding fun_eq_iff
   164   by (simp add: Quotient3_abs_rep[OF a])
   165 
   166 lemma equals_rsp:
   167   assumes q: "Quotient3 R Abs Rep"
   168   and     a: "R xa xb" "R ya yb"
   169   shows "R xa ya = R xb yb"
   170   using a Quotient3_symp[OF q] Quotient3_transp[OF q]
   171   by (blast elim: sympE transpE)
   172 
   173 lemma lambda_prs:
   174   assumes q1: "Quotient3 R1 Abs1 Rep1"
   175   and     q2: "Quotient3 R2 Abs2 Rep2"
   176   shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
   177   unfolding fun_eq_iff
   178   using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
   179   by simp
   180 
   181 lemma lambda_prs1:
   182   assumes q1: "Quotient3 R1 Abs1 Rep1"
   183   and     q2: "Quotient3 R2 Abs2 Rep2"
   184   shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
   185   unfolding fun_eq_iff
   186   using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
   187   by simp
   188 
   189 lemma rep_abs_rsp:
   190   assumes q: "Quotient3 R Abs Rep"
   191   and     a: "R x1 x2"
   192   shows "R x1 (Rep (Abs x2))"
   193   using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q]
   194   by metis
   195 
   196 lemma rep_abs_rsp_left:
   197   assumes q: "Quotient3 R Abs Rep"
   198   and     a: "R x1 x2"
   199   shows "R (Rep (Abs x1)) x2"
   200   using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q]
   201   by metis
   202 
   203 text{*
   204   In the following theorem R1 can be instantiated with anything,
   205   but we know some of the types of the Rep and Abs functions;
   206   so by solving Quotient assumptions we can get a unique R1 that
   207   will be provable; which is why we need to use @{text apply_rsp} and
   208   not the primed version *}
   209 
   210 lemma apply_rspQ3:
   211   fixes f g::"'a \<Rightarrow> 'c"
   212   assumes q: "Quotient3 R1 Abs1 Rep1"
   213   and     a: "(R1 ===> R2) f g" "R1 x y"
   214   shows "R2 (f x) (g y)"
   215   using a by (auto elim: fun_relE)
   216 
   217 lemma apply_rspQ3'':
   218   assumes "Quotient3 R Abs Rep"
   219   and "(R ===> S) f f"
   220   shows "S (f (Rep x)) (f (Rep x))"
   221 proof -
   222   from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient3_rep_reflp)
   223   then show ?thesis using assms(2) by (auto intro: apply_rsp')
   224 qed
   225 
   226 subsection {* lemmas for regularisation of ball and bex *}
   227 
   228 lemma ball_reg_eqv:
   229   fixes P :: "'a \<Rightarrow> bool"
   230   assumes a: "equivp R"
   231   shows "Ball (Respects R) P = (All P)"
   232   using a
   233   unfolding equivp_def
   234   by (auto simp add: in_respects)
   235 
   236 lemma bex_reg_eqv:
   237   fixes P :: "'a \<Rightarrow> bool"
   238   assumes a: "equivp R"
   239   shows "Bex (Respects R) P = (Ex P)"
   240   using a
   241   unfolding equivp_def
   242   by (auto simp add: in_respects)
   243 
   244 lemma ball_reg_right:
   245   assumes a: "\<And>x. x \<in> R \<Longrightarrow> P x \<longrightarrow> Q x"
   246   shows "All P \<longrightarrow> Ball R Q"
   247   using a by fast
   248 
   249 lemma bex_reg_left:
   250   assumes a: "\<And>x. x \<in> R \<Longrightarrow> Q x \<longrightarrow> P x"
   251   shows "Bex R Q \<longrightarrow> Ex P"
   252   using a by fast
   253 
   254 lemma ball_reg_left:
   255   assumes a: "equivp R"
   256   shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
   257   using a by (metis equivp_reflp in_respects)
   258 
   259 lemma bex_reg_right:
   260   assumes a: "equivp R"
   261   shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
   262   using a by (metis equivp_reflp in_respects)
   263 
   264 lemma ball_reg_eqv_range:
   265   fixes P::"'a \<Rightarrow> bool"
   266   and x::"'a"
   267   assumes a: "equivp R2"
   268   shows   "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
   269   apply(rule iffI)
   270   apply(rule allI)
   271   apply(drule_tac x="\<lambda>y. f x" in bspec)
   272   apply(simp add: in_respects fun_rel_def)
   273   apply(rule impI)
   274   using a equivp_reflp_symp_transp[of "R2"]
   275   apply (auto elim: equivpE reflpE)
   276   done
   277 
   278 lemma bex_reg_eqv_range:
   279   assumes a: "equivp R2"
   280   shows   "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
   281   apply(auto)
   282   apply(rule_tac x="\<lambda>y. f x" in bexI)
   283   apply(simp)
   284   apply(simp add: Respects_def in_respects fun_rel_def)
   285   apply(rule impI)
   286   using a equivp_reflp_symp_transp[of "R2"]
   287   apply (auto elim: equivpE reflpE)
   288   done
   289 
   290 (* Next four lemmas are unused *)
   291 lemma all_reg:
   292   assumes a: "!x :: 'a. (P x --> Q x)"
   293   and     b: "All P"
   294   shows "All Q"
   295   using a b by fast
   296 
   297 lemma ex_reg:
   298   assumes a: "!x :: 'a. (P x --> Q x)"
   299   and     b: "Ex P"
   300   shows "Ex Q"
   301   using a b by fast
   302 
   303 lemma ball_reg:
   304   assumes a: "!x :: 'a. (x \<in> R --> P x --> Q x)"
   305   and     b: "Ball R P"
   306   shows "Ball R Q"
   307   using a b by fast
   308 
   309 lemma bex_reg:
   310   assumes a: "!x :: 'a. (x \<in> R --> P x --> Q x)"
   311   and     b: "Bex R P"
   312   shows "Bex R Q"
   313   using a b by fast
   314 
   315 
   316 lemma ball_all_comm:
   317   assumes "\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)"
   318   shows "(\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y)"
   319   using assms by auto
   320 
   321 lemma bex_ex_comm:
   322   assumes "(\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)"
   323   shows "(\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y)"
   324   using assms by auto
   325 
   326 subsection {* Bounded abstraction *}
   327 
   328 definition
   329   Babs :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
   330 where
   331   "x \<in> p \<Longrightarrow> Babs p m x = m x"
   332 
   333 lemma babs_rsp:
   334   assumes q: "Quotient3 R1 Abs1 Rep1"
   335   and     a: "(R1 ===> R2) f g"
   336   shows      "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
   337   apply (auto simp add: Babs_def in_respects fun_rel_def)
   338   apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
   339   using a apply (simp add: Babs_def fun_rel_def)
   340   apply (simp add: in_respects fun_rel_def)
   341   using Quotient3_rel[OF q]
   342   by metis
   343 
   344 lemma babs_prs:
   345   assumes q1: "Quotient3 R1 Abs1 Rep1"
   346   and     q2: "Quotient3 R2 Abs2 Rep2"
   347   shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
   348   apply (rule ext)
   349   apply (simp add:)
   350   apply (subgoal_tac "Rep1 x \<in> Respects R1")
   351   apply (simp add: Babs_def Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
   352   apply (simp add: in_respects Quotient3_rel_rep[OF q1])
   353   done
   354 
   355 lemma babs_simp:
   356   assumes q: "Quotient3 R1 Abs Rep"
   357   shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
   358   apply(rule iffI)
   359   apply(simp_all only: babs_rsp[OF q])
   360   apply(auto simp add: Babs_def fun_rel_def)
   361   apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
   362   apply(metis Babs_def)
   363   apply (simp add: in_respects)
   364   using Quotient3_rel[OF q]
   365   by metis
   366 
   367 (* If a user proves that a particular functional relation
   368    is an equivalence this may be useful in regularising *)
   369 lemma babs_reg_eqv:
   370   shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
   371   by (simp add: fun_eq_iff Babs_def in_respects equivp_reflp)
   372 
   373 
   374 (* 3 lemmas needed for proving repabs_inj *)
   375 lemma ball_rsp:
   376   assumes a: "(R ===> (op =)) f g"
   377   shows "Ball (Respects R) f = Ball (Respects R) g"
   378   using a by (auto simp add: Ball_def in_respects elim: fun_relE)
   379 
   380 lemma bex_rsp:
   381   assumes a: "(R ===> (op =)) f g"
   382   shows "(Bex (Respects R) f = Bex (Respects R) g)"
   383   using a by (auto simp add: Bex_def in_respects elim: fun_relE)
   384 
   385 lemma bex1_rsp:
   386   assumes a: "(R ===> (op =)) f g"
   387   shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)"
   388   using a by (auto elim: fun_relE simp add: Ex1_def in_respects) 
   389 
   390 (* 2 lemmas needed for cleaning of quantifiers *)
   391 lemma all_prs:
   392   assumes a: "Quotient3 R absf repf"
   393   shows "Ball (Respects R) ((absf ---> id) f) = All f"
   394   using a unfolding Quotient3_def Ball_def in_respects id_apply comp_def map_fun_def
   395   by metis
   396 
   397 lemma ex_prs:
   398   assumes a: "Quotient3 R absf repf"
   399   shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
   400   using a unfolding Quotient3_def Bex_def in_respects id_apply comp_def map_fun_def
   401   by metis
   402 
   403 subsection {* @{text Bex1_rel} quantifier *}
   404 
   405 definition
   406   Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   407 where
   408   "Bex1_rel R P \<longleftrightarrow> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"
   409 
   410 lemma bex1_rel_aux:
   411   "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y"
   412   unfolding Bex1_rel_def
   413   apply (erule conjE)+
   414   apply (erule bexE)
   415   apply rule
   416   apply (rule_tac x="xa" in bexI)
   417   apply metis
   418   apply metis
   419   apply rule+
   420   apply (erule_tac x="xaa" in ballE)
   421   prefer 2
   422   apply (metis)
   423   apply (erule_tac x="ya" in ballE)
   424   prefer 2
   425   apply (metis)
   426   apply (metis in_respects)
   427   done
   428 
   429 lemma bex1_rel_aux2:
   430   "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R y\<rbrakk> \<Longrightarrow> Bex1_rel R x"
   431   unfolding Bex1_rel_def
   432   apply (erule conjE)+
   433   apply (erule bexE)
   434   apply rule
   435   apply (rule_tac x="xa" in bexI)
   436   apply metis
   437   apply metis
   438   apply rule+
   439   apply (erule_tac x="xaa" in ballE)
   440   prefer 2
   441   apply (metis)
   442   apply (erule_tac x="ya" in ballE)
   443   prefer 2
   444   apply (metis)
   445   apply (metis in_respects)
   446   done
   447 
   448 lemma bex1_rel_rsp:
   449   assumes a: "Quotient3 R absf repf"
   450   shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
   451   apply (simp add: fun_rel_def)
   452   apply clarify
   453   apply rule
   454   apply (simp_all add: bex1_rel_aux bex1_rel_aux2)
   455   apply (erule bex1_rel_aux2)
   456   apply assumption
   457   done
   458 
   459 
   460 lemma ex1_prs:
   461   assumes a: "Quotient3 R absf repf"
   462   shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f"
   463 apply (simp add:)
   464 apply (subst Bex1_rel_def)
   465 apply (subst Bex_def)
   466 apply (subst Ex1_def)
   467 apply simp
   468 apply rule
   469  apply (erule conjE)+
   470  apply (erule_tac exE)
   471  apply (erule conjE)
   472  apply (subgoal_tac "\<forall>y. R y y \<longrightarrow> f (absf y) \<longrightarrow> R x y")
   473   apply (rule_tac x="absf x" in exI)
   474   apply (simp)
   475   apply rule+
   476   using a unfolding Quotient3_def
   477   apply metis
   478  apply rule+
   479  apply (erule_tac x="x" in ballE)
   480   apply (erule_tac x="y" in ballE)
   481    apply simp
   482   apply (simp add: in_respects)
   483  apply (simp add: in_respects)
   484 apply (erule_tac exE)
   485  apply rule
   486  apply (rule_tac x="repf x" in exI)
   487  apply (simp only: in_respects)
   488   apply rule
   489  apply (metis Quotient3_rel_rep[OF a])
   490 using a unfolding Quotient3_def apply (simp)
   491 apply rule+
   492 using a unfolding Quotient3_def in_respects
   493 apply metis
   494 done
   495 
   496 lemma bex1_bexeq_reg:
   497   shows "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
   498   apply (simp add: Ex1_def Bex1_rel_def in_respects)
   499   apply clarify
   500   apply auto
   501   apply (rule bexI)
   502   apply assumption
   503   apply (simp add: in_respects)
   504   apply (simp add: in_respects)
   505   apply auto
   506   done
   507 
   508 lemma bex1_bexeq_reg_eqv:
   509   assumes a: "equivp R"
   510   shows "(\<exists>!x. P x) \<longrightarrow> Bex1_rel R P"
   511   using equivp_reflp[OF a]
   512   apply (intro impI)
   513   apply (elim ex1E)
   514   apply (rule mp[OF bex1_bexeq_reg])
   515   apply (rule_tac a="x" in ex1I)
   516   apply (subst in_respects)
   517   apply (rule conjI)
   518   apply assumption
   519   apply assumption
   520   apply clarify
   521   apply (erule_tac x="xa" in allE)
   522   apply simp
   523   done
   524 
   525 subsection {* Various respects and preserve lemmas *}
   526 
   527 lemma quot_rel_rsp:
   528   assumes a: "Quotient3 R Abs Rep"
   529   shows "(R ===> R ===> op =) R R"
   530   apply(rule fun_relI)+
   531   apply(rule equals_rsp[OF a])
   532   apply(assumption)+
   533   done
   534 
   535 lemma o_prs:
   536   assumes q1: "Quotient3 R1 Abs1 Rep1"
   537   and     q2: "Quotient3 R2 Abs2 Rep2"
   538   and     q3: "Quotient3 R3 Abs3 Rep3"
   539   shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) op \<circ> = op \<circ>"
   540   and   "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) op \<circ> = op \<circ>"
   541   using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] Quotient3_abs_rep[OF q3]
   542   by (simp_all add: fun_eq_iff)
   543 
   544 lemma o_rsp:
   545   "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
   546   "(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
   547   by (force elim: fun_relE)+
   548 
   549 lemma cond_prs:
   550   assumes a: "Quotient3 R absf repf"
   551   shows "absf (if a then repf b else repf c) = (if a then b else c)"
   552   using a unfolding Quotient3_def by auto
   553 
   554 lemma if_prs:
   555   assumes q: "Quotient3 R Abs Rep"
   556   shows "(id ---> Rep ---> Rep ---> Abs) If = If"
   557   using Quotient3_abs_rep[OF q]
   558   by (auto simp add: fun_eq_iff)
   559 
   560 lemma if_rsp:
   561   assumes q: "Quotient3 R Abs Rep"
   562   shows "(op = ===> R ===> R ===> R) If If"
   563   by force
   564 
   565 lemma let_prs:
   566   assumes q1: "Quotient3 R1 Abs1 Rep1"
   567   and     q2: "Quotient3 R2 Abs2 Rep2"
   568   shows "(Rep2 ---> (Abs2 ---> Rep1) ---> Abs1) Let = Let"
   569   using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
   570   by (auto simp add: fun_eq_iff)
   571 
   572 lemma let_rsp:
   573   shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
   574   by (force elim: fun_relE)
   575 
   576 lemma id_rsp:
   577   shows "(R ===> R) id id"
   578   by auto
   579 
   580 lemma id_prs:
   581   assumes a: "Quotient3 R Abs Rep"
   582   shows "(Rep ---> Abs) id = id"
   583   by (simp add: fun_eq_iff Quotient3_abs_rep [OF a])
   584 
   585 end
   586 
   587 locale quot_type =
   588   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   589   and   Abs :: "'a set \<Rightarrow> 'b"
   590   and   Rep :: "'b \<Rightarrow> 'a set"
   591   assumes equivp: "part_equivp R"
   592   and     rep_prop: "\<And>y. \<exists>x. R x x \<and> Rep y = Collect (R x)"
   593   and     rep_inverse: "\<And>x. Abs (Rep x) = x"
   594   and     abs_inverse: "\<And>c. (\<exists>x. ((R x x) \<and> (c = Collect (R x)))) \<Longrightarrow> (Rep (Abs c)) = c"
   595   and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
   596 begin
   597 
   598 definition
   599   abs :: "'a \<Rightarrow> 'b"
   600 where
   601   "abs x = Abs (Collect (R x))"
   602 
   603 definition
   604   rep :: "'b \<Rightarrow> 'a"
   605 where
   606   "rep a = (SOME x. x \<in> Rep a)"
   607 
   608 lemma some_collect:
   609   assumes "R r r"
   610   shows "R (SOME x. x \<in> Collect (R r)) = R r"
   611   apply simp
   612   by (metis assms exE_some equivp[simplified part_equivp_def])
   613 
   614 lemma Quotient:
   615   shows "Quotient3 R abs rep"
   616   unfolding Quotient3_def abs_def rep_def
   617   proof (intro conjI allI)
   618     fix a r s
   619     show x: "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" proof -
   620       obtain x where r: "R x x" and rep: "Rep a = Collect (R x)" using rep_prop[of a] by auto
   621       have "R (SOME x. x \<in> Rep a) x"  using r rep some_collect by metis
   622       then have "R x (SOME x. x \<in> Rep a)" using part_equivp_symp[OF equivp] by fast
   623       then show "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)"
   624         using part_equivp_transp[OF equivp] by (metis `R (SOME x. x \<in> Rep a) x`)
   625     qed
   626     have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop)
   627     then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto
   628     have "R r r \<Longrightarrow> R s s \<Longrightarrow> Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s"
   629     proof -
   630       assume "R r r" and "R s s"
   631       then have "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> Collect (R r) = Collect (R s)"
   632         by (metis abs_inverse)
   633       also have "Collect (R r) = Collect (R s) \<longleftrightarrow> (\<lambda>A x. x \<in> A) (Collect (R r)) = (\<lambda>A x. x \<in> A) (Collect (R s))"
   634         by rule simp_all
   635       finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" by simp
   636     qed
   637     then show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (Collect (R r)) = Abs (Collect (R s)))"
   638       using equivp[simplified part_equivp_def] by metis
   639     qed
   640 
   641 end
   642 
   643 subsection {* Quotient composition *}
   644 
   645 lemma OOO_quotient3:
   646   fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   647   fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a"
   648   fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b"
   649   fixes R2' :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   650   fixes R2 :: "'b \<Rightarrow> 'b \<Rightarrow> bool"
   651   assumes R1: "Quotient3 R1 Abs1 Rep1"
   652   assumes R2: "Quotient3 R2 Abs2 Rep2"
   653   assumes Abs1: "\<And>x y. R2' x y \<Longrightarrow> R1 x x \<Longrightarrow> R1 y y \<Longrightarrow> R2 (Abs1 x) (Abs1 y)"
   654   assumes Rep1: "\<And>x y. R2 x y \<Longrightarrow> R2' (Rep1 x) (Rep1 y)"
   655   shows "Quotient3 (R1 OO R2' OO R1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
   656 apply (rule Quotient3I)
   657    apply (simp add: o_def Quotient3_abs_rep [OF R2] Quotient3_abs_rep [OF R1])
   658   apply simp
   659   apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI)
   660    apply (rule Quotient3_rep_reflp [OF R1])
   661   apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI [rotated])
   662    apply (rule Quotient3_rep_reflp [OF R1])
   663   apply (rule Rep1)
   664   apply (rule Quotient3_rep_reflp [OF R2])
   665  apply safe
   666     apply (rename_tac x y)
   667     apply (drule Abs1)
   668       apply (erule Quotient3_refl2 [OF R1])
   669      apply (erule Quotient3_refl1 [OF R1])
   670     apply (drule Quotient3_refl1 [OF R2], drule Rep1)
   671     apply (subgoal_tac "R1 r (Rep1 (Abs1 x))")
   672      apply (rule_tac b="Rep1 (Abs1 x)" in relcomppI, assumption)
   673      apply (erule relcomppI)
   674      apply (erule Quotient3_symp [OF R1, THEN sympD])
   675     apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
   676     apply (rule conjI, erule Quotient3_refl1 [OF R1])
   677     apply (rule conjI, rule Quotient3_rep_reflp [OF R1])
   678     apply (subst Quotient3_abs_rep [OF R1])
   679     apply (erule Quotient3_rel_abs [OF R1])
   680    apply (rename_tac x y)
   681    apply (drule Abs1)
   682      apply (erule Quotient3_refl2 [OF R1])
   683     apply (erule Quotient3_refl1 [OF R1])
   684    apply (drule Quotient3_refl2 [OF R2], drule Rep1)
   685    apply (subgoal_tac "R1 s (Rep1 (Abs1 y))")
   686     apply (rule_tac b="Rep1 (Abs1 y)" in relcomppI, assumption)
   687     apply (erule relcomppI)
   688     apply (erule Quotient3_symp [OF R1, THEN sympD])
   689    apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
   690    apply (rule conjI, erule Quotient3_refl2 [OF R1])
   691    apply (rule conjI, rule Quotient3_rep_reflp [OF R1])
   692    apply (subst Quotient3_abs_rep [OF R1])
   693    apply (erule Quotient3_rel_abs [OF R1, THEN sym])
   694   apply simp
   695   apply (rule Quotient3_rel_abs [OF R2])
   696   apply (rule Quotient3_rel_abs [OF R1, THEN ssubst], assumption)
   697   apply (rule Quotient3_rel_abs [OF R1, THEN subst], assumption)
   698   apply (erule Abs1)
   699    apply (erule Quotient3_refl2 [OF R1])
   700   apply (erule Quotient3_refl1 [OF R1])
   701  apply (rename_tac a b c d)
   702  apply simp
   703  apply (rule_tac b="Rep1 (Abs1 r)" in relcomppI)
   704   apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
   705   apply (rule conjI, erule Quotient3_refl1 [OF R1])
   706   apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1])
   707  apply (rule_tac b="Rep1 (Abs1 s)" in relcomppI [rotated])
   708   apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
   709   apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1])
   710   apply (erule Quotient3_refl2 [OF R1])
   711  apply (rule Rep1)
   712  apply (drule Abs1)
   713    apply (erule Quotient3_refl2 [OF R1])
   714   apply (erule Quotient3_refl1 [OF R1])
   715  apply (drule Abs1)
   716   apply (erule Quotient3_refl2 [OF R1])
   717  apply (erule Quotient3_refl1 [OF R1])
   718  apply (drule Quotient3_rel_abs [OF R1])
   719  apply (drule Quotient3_rel_abs [OF R1])
   720  apply (drule Quotient3_rel_abs [OF R1])
   721  apply (drule Quotient3_rel_abs [OF R1])
   722  apply simp
   723  apply (rule Quotient3_rel[symmetric, OF R2, THEN iffD2])
   724  apply simp
   725 done
   726 
   727 lemma OOO_eq_quotient3:
   728   fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   729   fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a"
   730   fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b"
   731   assumes R1: "Quotient3 R1 Abs1 Rep1"
   732   assumes R2: "Quotient3 op= Abs2 Rep2"
   733   shows "Quotient3 (R1 OOO op=) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
   734 using assms
   735 by (rule OOO_quotient3) auto
   736 
   737 subsection {* Quotient3 to Quotient *}
   738 
   739 lemma Quotient3_to_Quotient:
   740 assumes "Quotient3 R Abs Rep"
   741 and "T \<equiv> \<lambda>x y. R x x \<and> Abs x = y"
   742 shows "Quotient R Abs Rep T"
   743 using assms unfolding Quotient3_def by (intro QuotientI) blast+
   744 
   745 lemma Quotient3_to_Quotient_equivp:
   746 assumes q: "Quotient3 R Abs Rep"
   747 and T_def: "T \<equiv> \<lambda>x y. Abs x = y"
   748 and eR: "equivp R"
   749 shows "Quotient R Abs Rep T"
   750 proof (intro QuotientI)
   751   fix a
   752   show "Abs (Rep a) = a" using q by(rule Quotient3_abs_rep)
   753 next
   754   fix a
   755   show "R (Rep a) (Rep a)" using q by(rule Quotient3_rep_reflp)
   756 next
   757   fix r s
   758   show "R r s = (R r r \<and> R s s \<and> Abs r = Abs s)" using q by(rule Quotient3_rel[symmetric])
   759 next
   760   show "T = (\<lambda>x y. R x x \<and> Abs x = y)" using T_def equivp_reflp[OF eR] by simp
   761 qed
   762 
   763 subsection {* ML setup *}
   764 
   765 text {* Auxiliary data for the quotient package *}
   766 
   767 ML_file "Tools/Quotient/quotient_info.ML"
   768 setup Quotient_Info.setup
   769 
   770 declare [[mapQ3 "fun" = (fun_rel, fun_quotient3)]]
   771 
   772 lemmas [quot_thm] = fun_quotient3
   773 lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp
   774 lemmas [quot_preserve] = if_prs o_prs let_prs id_prs
   775 lemmas [quot_equiv] = identity_equivp
   776 
   777 
   778 text {* Lemmas about simplifying id's. *}
   779 lemmas [id_simps] =
   780   id_def[symmetric]
   781   map_fun_id
   782   id_apply
   783   id_o
   784   o_id
   785   eq_comp_r
   786   vimage_id
   787 
   788 text {* Translation functions for the lifting process. *}
   789 ML_file "Tools/Quotient/quotient_term.ML"
   790 
   791 
   792 text {* Definitions of the quotient types. *}
   793 ML_file "Tools/Quotient/quotient_type.ML"
   794 
   795 
   796 text {* Definitions for quotient constants. *}
   797 ML_file "Tools/Quotient/quotient_def.ML"
   798 
   799 
   800 text {*
   801   An auxiliary constant for recording some information
   802   about the lifted theorem in a tactic.
   803 *}
   804 definition
   805   Quot_True :: "'a \<Rightarrow> bool"
   806 where
   807   "Quot_True x \<longleftrightarrow> True"
   808 
   809 lemma
   810   shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
   811   and   QT_ex:  "Quot_True (Ex P) \<Longrightarrow> Quot_True P"
   812   and   QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P"
   813   and   QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))"
   814   and   QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"
   815   by (simp_all add: Quot_True_def ext)
   816 
   817 lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
   818   by (simp add: Quot_True_def)
   819 
   820 context 
   821 begin
   822 interpretation lifting_syntax .
   823 
   824 text {* Tactics for proving the lifted theorems *}
   825 ML_file "Tools/Quotient/quotient_tacs.ML"
   826 
   827 end
   828 
   829 subsection {* Methods / Interface *}
   830 
   831 method_setup lifting =
   832   {* Attrib.thms >> (fn thms => fn ctxt => 
   833        SIMPLE_METHOD' (Quotient_Tacs.lift_tac ctxt [] thms)) *}
   834   {* lift theorems to quotient types *}
   835 
   836 method_setup lifting_setup =
   837   {* Attrib.thm >> (fn thm => fn ctxt => 
   838        SIMPLE_METHOD' (Quotient_Tacs.lift_procedure_tac ctxt [] thm)) *}
   839   {* set up the three goals for the quotient lifting procedure *}
   840 
   841 method_setup descending =
   842   {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_tac ctxt [])) *}
   843   {* decend theorems to the raw level *}
   844 
   845 method_setup descending_setup =
   846   {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_procedure_tac ctxt [])) *}
   847   {* set up the three goals for the decending theorems *}
   848 
   849 method_setup partiality_descending =
   850   {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_tac ctxt [])) *}
   851   {* decend theorems to the raw level *}
   852 
   853 method_setup partiality_descending_setup =
   854   {* Scan.succeed (fn ctxt => 
   855        SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_procedure_tac ctxt [])) *}
   856   {* set up the three goals for the decending theorems *}
   857 
   858 method_setup regularize =
   859   {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.regularize_tac ctxt)) *}
   860   {* prove the regularization goals from the quotient lifting procedure *}
   861 
   862 method_setup injection =
   863   {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.all_injection_tac ctxt)) *}
   864   {* prove the rep/abs injection goals from the quotient lifting procedure *}
   865 
   866 method_setup cleaning =
   867   {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.clean_tac ctxt)) *}
   868   {* prove the cleaning goals from the quotient lifting procedure *}
   869 
   870 attribute_setup quot_lifted =
   871   {* Scan.succeed Quotient_Tacs.lifted_attrib *}
   872   {* lift theorems to quotient types *}
   873 
   874 no_notation
   875   rel_conj (infixr "OOO" 75)
   876 
   877 end
   878