# HG changeset patch # User paulson # Date 1033115781 -7200 # Node ID e39f0751e4bf3d4e621ba8e946d15ae617940daf # Parent dfe0c719112573e801f8ebe3179a0ad67be01a3b Tidied. New Pi-theorem. diff -r dfe0c7191125 -r e39f0751e4bf src/HOL/Library/FuncSet.thy --- a/src/HOL/Library/FuncSet.thy Fri Sep 27 10:35:10 2002 +0200 +++ b/src/HOL/Library/FuncSet.thy Fri Sep 27 10:36:21 2002 +0200 @@ -50,26 +50,24 @@ by (simp add: Pi_def) lemma Pi_mem: "[|f: Pi A B; x \ A|] ==> f x \ B x" -apply (simp add: Pi_def) -done +by (simp add: Pi_def) lemma funcset_mem: "[|f \ A -> B; x \ A|] ==> f x \ B" by (simp add: Pi_def) lemma Pi_eq_empty: "((PI x: A. B x) = {}) = (\x\A. B(x) = {})" -apply (simp add: Pi_def) -apply auto +apply (simp add: Pi_def, auto) txt{*Converse direction requires Axiom of Choice to exhibit a function picking an element from each non-empty @{term "B x"}*} -apply (drule_tac x = "%u. SOME y. y \ B u" in spec) -apply (auto ); -apply (cut_tac P= "%y. y \ B x" in some_eq_ex) -apply (auto ); +apply (drule_tac x = "%u. SOME y. y \ B u" in spec, auto) +apply (cut_tac P= "%y. y \ B x" in some_eq_ex, auto) done -lemma Pi_empty: "Pi {} B = UNIV" -apply (simp add: Pi_def) -done +lemma Pi_empty [simp]: "Pi {} B = UNIV" +by (simp add: Pi_def) + +lemma Pi_UNIV [simp]: "A -> UNIV = UNIV" +by (simp add: Pi_def) text{*Covariance of Pi-sets in their second argument*} lemma Pi_mono: "(!!x. x \ A ==> B x <= C x) ==> Pi A B <= Pi A C" @@ -92,12 +90,10 @@ by (simp add: expand_fun_eq Pi_def compose_def restrict_def) lemma compose_eq: "x \ A ==> compose A g f x = g(f(x))" -apply (simp add: compose_def restrict_def) -done +by (simp add: compose_def restrict_def) lemma surj_compose: "[| f ` A = B; g ` B = C |] ==> compose A g f ` A = C" -apply (auto simp add: image_def compose_eq) -done +by (auto simp add: image_def compose_eq) lemma inj_on_compose: "[| f ` A = B; inj_on f A; inj_on g B |] ==> inj_on (compose A g f) A" @@ -122,8 +118,7 @@ by (simp add: expand_fun_eq Pi_def Pi_def restrict_def) lemma inj_on_restrict_eq: "inj_on (restrict f A) A = inj_on f A" -apply (simp add: inj_on_def restrict_def) -done +by (simp add: inj_on_def restrict_def) lemma Id_compose: @@ -138,8 +133,7 @@ subsection{*Extensionality*} lemma extensional_arb: "[|f \ extensional A; x\ A|] ==> f x = arbitrary" -apply (simp add: extensional_def) -done +by (simp add: extensional_def) lemma restrict_extensional [simp]: "restrict f A \ extensional A" by (simp add: restrict_def extensional_def) @@ -161,8 +155,7 @@ "[| inj_on f A; f ` A = B |] ==> compose A (\y\B. Inv A f y) f = (\x\A. x)" apply (simp add: compose_def) -apply (rule restrict_ext) -apply auto +apply (rule restrict_ext, auto) apply (erule subst) apply (simp add: Inv_f_f) done