author wenzelm Sat Nov 18 19:46:48 2000 +0100 (2000-11-18) changeset 10491 e4a408728012 parent 10490 0054c785f495 child 10492 107c7db021a9
quot_cond_function: simplified, support conditional definition;
```     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
```