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
```