src/HOL/Library/Quotient.thy
changeset 18372 2bffdf62fe7f
parent 15140 322485b816ac
child 18551 be0705186ff5
     1.1 --- a/src/HOL/Library/Quotient.thy	Thu Dec 08 20:15:41 2005 +0100
     1.2 +++ b/src/HOL/Library/Quotient.thy	Thu Dec 08 20:15:50 2005 +0100
     1.3 @@ -163,15 +163,13 @@
     1.4  *}
     1.5  
     1.6  theorem quot_cond_function:
     1.7 -  "(!!X Y. P 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>
     1.9 -      ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>
    1.10 -    P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
    1.11 -  (is "PROP ?eq ==> PROP ?cong ==> _ ==> _")
    1.12 +  assumes eq: "!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)"
    1.13 +    and cong: "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
    1.14 +      ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
    1.15 +    and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
    1.16 +  shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
    1.17  proof -
    1.18 -  assume cong: "PROP ?cong"
    1.19 -  assume "PROP ?eq" and "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
    1.20 -  hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
    1.21 +  from eq and P have "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
    1.22    also have "... = g a b"
    1.23    proof (rule cong)
    1.24      show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" ..
    1.25 @@ -185,18 +183,16 @@
    1.26  qed
    1.27  
    1.28  theorem quot_function:
    1.29 -  "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
    1.30 -    (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>
    1.31 -    f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
    1.32 -proof -
    1.33 -  case rule_context from this TrueI
    1.34 -  show ?thesis by (rule quot_cond_function)
    1.35 -qed
    1.36 +  assumes "!!X Y. f X Y == g (pick X) (pick Y)"
    1.37 +    and "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
    1.38 +  shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
    1.39 +  using prems and TrueI
    1.40 +  by (rule quot_cond_function)
    1.41  
    1.42  theorem quot_function':
    1.43    "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
    1.44      (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==>
    1.45      f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
    1.46 -  by  (rule quot_function) (simp only: quot_equality)+
    1.47 +  by (rule quot_function) (simp_all only: quot_equality)
    1.48  
    1.49  end