src/HOL/Library/Quotient.thy
changeset 10491 e4a408728012
parent 10483 eb93ace45a6e
child 10499 2f33d0fd242e
equal deleted inserted replaced
10490:0054c785f495 10491:e4a408728012
   174  stripped-down version without additional conditions is sufficient
   174  stripped-down version without additional conditions is sufficient
   175  most of the time.
   175  most of the time.
   176 *}
   176 *}
   177 
   177 
   178 theorem quot_cond_function:
   178 theorem quot_cond_function:
   179   "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
   179   "(!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)) ==>
   180     (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> P x y ==> P x' y'
   180     (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
   181       ==> g x y = g x' y') ==>
   181       ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>
   182     (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> P x y = P x' y') ==>
   182     P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   183     P a b ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   183   (is "PROP ?eq ==> PROP ?cong ==> _ ==> _")
   184   (is "PROP ?eq ==> PROP ?cong_g ==> PROP ?cong_P ==> _ ==> _")
   184 proof -
   185 proof -
   185   assume cong: "PROP ?cong"
   186   assume cong_g: "PROP ?cong_g"
   186   assume "PROP ?eq" and "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
   187     and cong_P: "PROP ?cong_P" and P: "P a b"
   187   hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
   188   assume "PROP ?eq"
       
   189   hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)"
       
   190     by (simp only:)
       
   191   also have "\<dots> = g a b"
   188   also have "\<dots> = g a b"
   192   proof (rule cong_g)
   189   proof (rule cong)
   193     show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" ..
   190     show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" ..
   194     moreover
   191     moreover
   195     show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" ..
   192     show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" ..
   196     ultimately
   193     moreover
   197     have "P (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>) = P a b"
   194     show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" .
   198       by (rule cong_P)
   195     ultimately show "P \<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> \<lfloor>pick \<lfloor>b\<rfloor>\<rfloor>" by (simp only:)
   199     also show \<dots> .
       
   200     finally show "P (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" .
       
   201   qed
   196   qed
   202   finally show ?thesis .
   197   finally show ?thesis .
   203 qed
   198 qed
   204 
   199 
   205 theorem quot_function:
   200 theorem quot_function:
   206   "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
   201   "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
   207     (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>
   202     (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>
   208     f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   203     f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   209 proof -
   204 proof -
   210   case antecedent from this refl TrueI
   205   case antecedent from this TrueI
   211   show ?thesis by (rule quot_cond_function)
   206   show ?thesis by (rule quot_cond_function)
   212 qed
   207 qed
   213 
   208 
   214 end
   209 end