src/HOL/Library/Quotient.thy
 changeset 10473 4f15b844fea6 parent 10459 df3cd3e76046 child 10477 c21bee84cefe
```     1.1 --- a/src/HOL/Library/Quotient.thy	Wed Nov 15 19:42:58 2000 +0100
1.2 +++ b/src/HOL/Library/Quotient.thy	Wed Nov 15 19:43:42 2000 +0100
1.3 @@ -4,7 +4,7 @@
1.4  *)
1.5
1.7 -  \title{Quotients}
1.8 +  \title{Quotient types}
1.9    \author{Gertrud Bauer and Markus Wenzel}
1.10  *}
1.11
1.12 @@ -136,71 +136,114 @@
1.13   on quotient types.
1.14  *}
1.15
1.16 -theorem quot_cond_definition1:
1.17 +theorem quot_cond_function1:
1.18 +  "(!!X. f X == g (pick X)) ==>
1.19 +    (!!x x'. x \<sim> x' ==> P x ==> P x' ==> g x = g x') ==>
1.20 +    (!!x x'. x \<sim> x' ==> P x = P x') ==>
1.21 +  P a ==> f \<lfloor>a\<rfloor> = g a"
1.22 +proof -
1.23 +  assume cong_g: "!!x x'. x \<sim> x' ==> P x ==> P x' ==> g x = g x'"
1.24 +  assume cong_P: "!!x x'. x \<sim> x' ==> P x = P x'"
1.25 +  assume P: "P a"
1.26 +  assume "!!X. f X == g (pick X)"
1.27 +  hence "f \<lfloor>a\<rfloor> = g (pick \<lfloor>a\<rfloor>)" by (simp only:)
1.28 +  also have "\<dots> = g a"
1.29 +  proof (rule cong_g)
1.30 +    show "pick \<lfloor>a\<rfloor> \<sim> a" ..
1.31 +    hence "P (pick \<lfloor>a\<rfloor>) = P a" by (rule cong_P)
1.32 +    also note P
1.33 +    finally show "P (pick \<lfloor>a\<rfloor>)" .
1.34 +  qed
1.35 +  finally show ?thesis .
1.36 +qed
1.37 +
1.38 +theorem quot_function1:
1.39 +  "(!!X. f X == g (pick X)) ==>
1.40 +    (!!x x'. x \<sim> x' ==> g x = g x') ==>
1.41 +    f \<lfloor>a\<rfloor> = g a"
1.42 +proof -
1.43 +  case antecedent from this refl TrueI
1.44 +  show ?thesis by (rule quot_cond_function1)
1.45 +qed
1.46 +
1.47 +theorem quot_cond_operation1:
1.48    "(!!X. f X == \<lfloor>g (pick X)\<rfloor>) ==>
1.49      (!!x x'. x \<sim> x' ==> P x ==> P x' ==> g x \<sim> g x') ==>
1.50      (!!x x'. x \<sim> x' ==> P x = P x') ==>
1.51    P a ==> f \<lfloor>a\<rfloor> = \<lfloor>g a\<rfloor>"
1.52  proof -
1.53 -  assume cong_g: "!!x x'. x \<sim> x' ==> P x ==> P x' ==> g x \<sim> g x'"
1.54 -  assume cong_P: "!!x x'. x \<sim> x' ==> P x = P x'"
1.55 -  assume P: "P a"
1.56 -  assume "!!X. f X == \<lfloor>g (pick X)\<rfloor>"
1.57 -  hence "f \<lfloor>a\<rfloor> = \<lfloor>g (pick \<lfloor>a\<rfloor>)\<rfloor>" by (simp only:)
1.58 -  also have "\<dots> = \<lfloor>g a\<rfloor>"
1.59 -  proof
1.60 -    show "g (pick \<lfloor>a\<rfloor>) \<sim> g a"
1.61 -    proof (rule cong_g)
1.62 -      show "pick \<lfloor>a\<rfloor> \<sim> a" ..
1.63 -      hence "P (pick \<lfloor>a\<rfloor>) = P a" by (rule cong_P)
1.64 -      also show "P a" .
1.65 -      finally show "P (pick \<lfloor>a\<rfloor>)" .
1.66 -    qed
1.67 -  qed
1.68 -  finally show ?thesis .
1.69 +  assume defn: "!!X. f X == \<lfloor>g (pick X)\<rfloor>"
1.70 +  assume "!!x x'. x \<sim> x' ==> P x ==> P x' ==> g x \<sim> g x'"
1.71 +  hence cong_g: "!!x x'. x \<sim> x' ==> P x ==> P x' ==> \<lfloor>g x\<rfloor> = \<lfloor>g x'\<rfloor>" ..
1.72 +  assume "!!x x'. x \<sim> x' ==> P x = P x'" and "P a"
1.73 +  with defn cong_g show ?thesis by (rule quot_cond_function1)
1.74  qed
1.75
1.76 -theorem quot_definition1:
1.77 +theorem quot_operation1:
1.78    "(!!X. f X == \<lfloor>g (pick X)\<rfloor>) ==>
1.79      (!!x x'. x \<sim> x' ==> g x \<sim> g x') ==>
1.80      f \<lfloor>a\<rfloor> = \<lfloor>g a\<rfloor>"
1.81  proof -
1.82    case antecedent from this refl TrueI
1.83 -  show ?thesis by (rule quot_cond_definition1)
1.84 +  show ?thesis by (rule quot_cond_operation1)
1.85  qed
1.86
1.87 -theorem quot_cond_definition2:
1.88 -  "(!!X Y. f X Y == \<lfloor>g (pick X) (pick Y)\<rfloor>) ==>
1.89 -    (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y ==> P x' y' ==> g x y \<sim> g x' y') ==>
1.90 +theorem quot_cond_function2:
1.91 +  "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
1.92 +    (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y ==> P x' y'
1.93 +      ==> g x y = g x' y') ==>
1.94      (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y = P x' y') ==>
1.95 -    P a b ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = \<lfloor>g a b\<rfloor>"
1.96 +    P a b ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
1.97  proof -
1.98 -  assume cong_g: "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y ==> P x' y' ==> g x y \<sim> g x' y'"
1.99 +  assume cong_g: "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y ==> P x' y'
1.100 +    ==> g x y = g x' y'"
1.101    assume cong_P: "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y = P x' y'"
1.102    assume P: "P a b"
1.103 -  assume "!!X Y. f X Y == \<lfloor>g (pick X) (pick Y)\<rfloor>"
1.104 -  hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = \<lfloor>g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)\<rfloor>" by (simp only:)
1.105 -  also have "\<dots> = \<lfloor>g a b\<rfloor>"
1.106 -  proof
1.107 -    show "g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>) \<sim> g a b"
1.108 -    proof (rule cong_g)
1.109 -      show "pick \<lfloor>a\<rfloor> \<sim> a" ..
1.110 -      moreover show "pick \<lfloor>b\<rfloor> \<sim> b" ..
1.111 -      ultimately have "P (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>) = P a b" by (rule cong_P)
1.112 -      also show "P a b" .
1.113 -      finally show "P (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" .
1.114 -    qed
1.115 +  assume "!!X Y. f X Y == g (pick X) (pick Y)"
1.116 +  hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
1.117 +  also have "\<dots> = g a b"
1.118 +  proof (rule cong_g)
1.119 +    show "pick \<lfloor>a\<rfloor> \<sim> a" ..
1.120 +    moreover show "pick \<lfloor>b\<rfloor> \<sim> b" ..
1.121 +    ultimately have "P (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>) = P a b" by (rule cong_P)
1.122 +    also show "P a b" .
1.123 +    finally show "P (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" .
1.124    qed
1.125    finally show ?thesis .
1.126  qed
1.127
1.128 -theorem quot_definition2:
1.129 +theorem quot_function2:
1.130 +  "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
1.131 +    (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==>
1.132 +    f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
1.133 +proof -
1.134 +  case antecedent from this refl TrueI
1.135 +  show ?thesis by (rule quot_cond_function2)
1.136 +qed
1.137 +
1.138 +theorem quot_cond_operation2:
1.139 +  "(!!X Y. f X Y == \<lfloor>g (pick X) (pick Y)\<rfloor>) ==>
1.140 +    (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y ==> P x' y'
1.141 +      ==> g x y \<sim> g x' y') ==>
1.142 +    (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y = P x' y') ==>
1.143 +    P a b ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = \<lfloor>g a b\<rfloor>"
1.144 +proof -
1.145 +  assume defn: "!!X Y. f X Y == \<lfloor>g (pick X) (pick Y)\<rfloor>"
1.146 +  assume "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y ==> P x' y'
1.147 +    ==> g x y \<sim> g x' y'"
1.148 +  hence cong_g: "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y ==> P x' y'
1.149 +    ==> \<lfloor>g x y\<rfloor> = \<lfloor>g x' y'\<rfloor>" ..
1.150 +  assume "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y = P x' y'" and "P a b"
1.151 +  with defn cong_g show ?thesis by (rule quot_cond_function2)
1.152 +qed
1.153 +
1.154 +theorem quot_operation2:
1.155    "(!!X Y. f X Y == \<lfloor>g (pick X) (pick Y)\<rfloor>) ==>
1.156      (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y \<sim> g x' y') ==>
1.157      f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = \<lfloor>g a b\<rfloor>"
1.158  proof -
1.159    case antecedent from this refl TrueI
1.160 -  show ?thesis by (rule quot_cond_definition2)
1.161 +  show ?thesis by (rule quot_cond_operation2)
1.162  qed
1.163
1.164  text {*
```