# HG changeset patch # User wenzelm # Date 974573208 -3600 # Node ID e4a4087280126a5de4e28c87f6f6602843daf540 # Parent 0054c785f49541b3615f7de27ecb0109abea7fce quot_cond_function: simplified, support conditional definition; diff -r 0054c785f495 -r e4a408728012 src/HOL/Library/Quotient.thy --- a/src/HOL/Library/Quotient.thy Sat Nov 18 19:45:37 2000 +0100 +++ b/src/HOL/Library/Quotient.thy Sat Nov 18 19:46:48 2000 +0100 @@ -176,28 +176,23 @@ *} theorem quot_cond_function: - "(!!X Y. f X Y == g (pick X) (pick Y)) ==> - (!!x x' y y'. \x\ = \x'\ ==> \y\ = \y'\ ==> P x y ==> P x' y' - ==> g x y = g x' y') ==> - (!!x x' y y'. \x\ = \x'\ ==> \y\ = \y'\ ==> P x y = P x' y') ==> - P a b ==> f \a\ \b\ = g a b" - (is "PROP ?eq ==> PROP ?cong_g ==> PROP ?cong_P ==> _ ==> _") + "(!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)) ==> + (!!x x' y y'. \x\ = \x'\ ==> \y\ = \y'\ + ==> P \x\ \y\ ==> P \x'\ \y'\ ==> g x y = g x' y') ==> + P \a\ \b\ ==> f \a\ \b\ = g a b" + (is "PROP ?eq ==> PROP ?cong ==> _ ==> _") proof - - assume cong_g: "PROP ?cong_g" - and cong_P: "PROP ?cong_P" and P: "P a b" - assume "PROP ?eq" - hence "f \a\ \b\ = g (pick \a\) (pick \b\)" - by (simp only:) + assume cong: "PROP ?cong" + assume "PROP ?eq" and "P \a\ \b\" + hence "f \a\ \b\ = g (pick \a\) (pick \b\)" by (simp only:) also have "\ = g a b" - proof (rule cong_g) + proof (rule cong) show "\pick \a\\ = \a\" .. moreover show "\pick \b\\ = \b\" .. - ultimately - have "P (pick \a\) (pick \b\) = P a b" - by (rule cong_P) - also show \ . - finally show "P (pick \a\) (pick \b\)" . + moreover + show "P \a\ \b\" . + ultimately show "P \pick \a\\ \pick \b\\" by (simp only:) qed finally show ?thesis . qed @@ -207,7 +202,7 @@ (!!x x' y y'. \x\ = \x'\ ==> \y\ = \y'\ ==> g x y = g x' y') ==> f \a\ \b\ = g a b" proof - - case antecedent from this refl TrueI + case antecedent from this TrueI show ?thesis by (rule quot_cond_function) qed