quot_cond_function: simplified, support conditional definition;
authorwenzelm
Sat Nov 18 19:46:48 2000 +0100 (2000-11-18)
changeset 10491e4a408728012
parent 10490 0054c785f495
child 10492 107c7db021a9
quot_cond_function: simplified, support conditional definition;
src/HOL/Library/Quotient.thy
     1.1 --- a/src/HOL/Library/Quotient.thy	Sat Nov 18 19:45:37 2000 +0100
     1.2 +++ b/src/HOL/Library/Quotient.thy	Sat Nov 18 19:46:48 2000 +0100
     1.3 @@ -176,28 +176,23 @@
     1.4  *}
     1.5  
     1.6  theorem quot_cond_function:
     1.7 -  "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
     1.8 -    (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> P x y ==> P x' y'
     1.9 -      ==> g x y = g x' y') ==>
    1.10 -    (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> P x y = P x' y') ==>
    1.11 -    P a b ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
    1.12 -  (is "PROP ?eq ==> PROP ?cong_g ==> PROP ?cong_P ==> _ ==> _")
    1.13 +  "(!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)) ==>
    1.14 +    (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
    1.15 +      ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>
    1.16 +    P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
    1.17 +  (is "PROP ?eq ==> PROP ?cong ==> _ ==> _")
    1.18  proof -
    1.19 -  assume cong_g: "PROP ?cong_g"
    1.20 -    and cong_P: "PROP ?cong_P" and P: "P a b"
    1.21 -  assume "PROP ?eq"
    1.22 -  hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)"
    1.23 -    by (simp only:)
    1.24 +  assume cong: "PROP ?cong"
    1.25 +  assume "PROP ?eq" and "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
    1.26 +  hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
    1.27    also have "\<dots> = g a b"
    1.28 -  proof (rule cong_g)
    1.29 +  proof (rule cong)
    1.30      show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" ..
    1.31      moreover
    1.32      show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" ..
    1.33 -    ultimately
    1.34 -    have "P (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>) = P a b"
    1.35 -      by (rule cong_P)
    1.36 -    also show \<dots> .
    1.37 -    finally show "P (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" .
    1.38 +    moreover
    1.39 +    show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" .
    1.40 +    ultimately show "P \<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> \<lfloor>pick \<lfloor>b\<rfloor>\<rfloor>" by (simp only:)
    1.41    qed
    1.42    finally show ?thesis .
    1.43  qed
    1.44 @@ -207,7 +202,7 @@
    1.45      (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>
    1.46      f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
    1.47  proof -
    1.48 -  case antecedent from this refl TrueI
    1.49 +  case antecedent from this TrueI
    1.50    show ?thesis by (rule quot_cond_function)
    1.51  qed
    1.52