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.6  header {*
     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 {*