src/HOL/Library/FuncSet.thy
 changeset 14706 71590b7733b7 parent 14565 c6dc17aab88a child 14745 94be403deb84
```     1.1 --- a/src/HOL/Library/FuncSet.thy	Thu May 06 12:43:00 2004 +0200
1.2 +++ b/src/HOL/Library/FuncSet.thy	Thu May 06 14:14:18 2004 +0200
1.3 @@ -3,22 +3,19 @@
1.4      Author:     Florian Kammueller and Lawrence C Paulson
1.5  *)
1.6
1.8 -  \title{Pi and Function Sets}
1.9 -  \author{Florian Kammueller and Lawrence C Paulson}
1.10 -*}
1.11 +header {* Pi and Function Sets *}
1.12
1.13  theory FuncSet = Main:
1.14
1.15  constdefs
1.16 -  Pi      :: "['a set, 'a => 'b set] => ('a => 'b) set"
1.17 -    "Pi A B == {f. \<forall>x. x \<in> A --> f(x) \<in> B(x)}"
1.18 +  Pi :: "['a set, 'a => 'b set] => ('a => 'b) set"
1.19 +  "Pi A B == {f. \<forall>x. x \<in> A --> f x \<in> B x}"
1.20
1.21    extensional :: "'a set => ('a => 'b) set"
1.22 -    "extensional A == {f. \<forall>x. x~:A --> f(x) = arbitrary}"
1.23 +  "extensional A == {f. \<forall>x. x~:A --> f x = arbitrary}"
1.24
1.25 -  restrict :: "['a => 'b, 'a set] => ('a => 'b)"
1.26 -    "restrict f A == (%x. if x \<in> A then f x else arbitrary)"
1.27 +  "restrict" :: "['a => 'b, 'a set] => ('a => 'b)"
1.28 +  "restrict f A == (%x. if x \<in> A then f x else arbitrary)"
1.29
1.30  syntax
1.31    "@Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
1.32 @@ -27,7 +24,7 @@
1.33
1.34  syntax (xsymbols)
1.35    "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
1.36 -  funcset :: "['a set, 'b set] => ('a => 'b) set"  (infixr "\<rightarrow>" 60)
1.37 +  funcset :: "['a set, 'b set] => ('a => 'b) set"  (infixr "\<rightarrow>" 60)
1.38    "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
1.39
1.40  syntax (HTML output)
1.41 @@ -36,11 +33,11 @@
1.42
1.43  translations
1.44    "PI x:A. B" => "Pi A (%x. B)"
1.45 -  "A -> B"    => "Pi A (_K B)"
1.46 -  "%x:A. f"  == "restrict (%x. f) A"
1.47 +  "A -> B" => "Pi A (_K B)"
1.48 +  "%x:A. f" == "restrict (%x. f) A"
1.49
1.50  constdefs
1.51 -  compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
1.52 +  "compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
1.53    "compose A g f == \<lambda>x\<in>A. g (f x)"
1.54
1.55  print_translation {* [("Pi", dependent_tr' ("@Pi", "funcset"))] *}
1.56 @@ -49,126 +46,123 @@
1.57  subsection{*Basic Properties of @{term Pi}*}
1.58
1.59  lemma Pi_I: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B"
1.61 +  by (simp add: Pi_def)
1.62
1.63  lemma funcsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f \<in> A -> B"
1.65 +  by (simp add: Pi_def)
1.66
1.67  lemma Pi_mem: "[|f: Pi A B; x \<in> A|] ==> f x \<in> B x"
1.69 +  by (simp add: Pi_def)
1.70
1.71  lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B"
1.73 +  by (simp add: Pi_def)
1.74
1.75  lemma Pi_eq_empty: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})"
1.76  apply (simp add: Pi_def, auto)
1.77  txt{*Converse direction requires Axiom of Choice to exhibit a function
1.78  picking an element from each non-empty @{term "B x"}*}
1.79  apply (drule_tac x = "%u. SOME y. y \<in> B u" in spec, auto)
1.80 -apply (cut_tac P= "%y. y \<in> B x" in some_eq_ex, auto)
1.81 +apply (cut_tac P= "%y. y \<in> B x" in some_eq_ex, auto)
1.82  done
1.83
1.84  lemma Pi_empty [simp]: "Pi {} B = UNIV"
1.86 +  by (simp add: Pi_def)
1.87
1.88  lemma Pi_UNIV [simp]: "A -> UNIV = UNIV"
1.90 +  by (simp add: Pi_def)
1.91
1.92  text{*Covariance of Pi-sets in their second argument*}
1.93  lemma Pi_mono: "(!!x. x \<in> A ==> B x <= C x) ==> Pi A B <= Pi A C"
1.94 -by (simp add: Pi_def, blast)
1.95 +  by (simp add: Pi_def, blast)
1.96
1.97  text{*Contravariance of Pi-sets in their first argument*}
1.98  lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B"
1.99 -by (simp add: Pi_def, blast)
1.100 +  by (simp add: Pi_def, blast)
1.101
1.102
1.103  subsection{*Composition With a Restricted Domain: @{term compose}*}
1.104
1.105 -lemma funcset_compose:
1.106 -     "[| f \<in> A -> B; g \<in> B -> C |]==> compose A g f \<in> A -> C"
1.107 -by (simp add: Pi_def compose_def restrict_def)
1.108 +lemma funcset_compose:
1.109 +    "[| f \<in> A -> B; g \<in> B -> C |]==> compose A g f \<in> A -> C"
1.110 +  by (simp add: Pi_def compose_def restrict_def)
1.111
1.112  lemma compose_assoc:
1.113 -     "[| f \<in> A -> B; g \<in> B -> C; h \<in> C -> D |]
1.114 +    "[| f \<in> A -> B; g \<in> B -> C; h \<in> C -> D |]
1.115        ==> compose A h (compose A g f) = compose A (compose B h g) f"
1.116 -by (simp add: expand_fun_eq Pi_def compose_def restrict_def)
1.117 +  by (simp add: expand_fun_eq Pi_def compose_def restrict_def)
1.118
1.119  lemma compose_eq: "x \<in> A ==> compose A g f x = g(f(x))"
1.120 -by (simp add: compose_def restrict_def)
1.121 +  by (simp add: compose_def restrict_def)
1.122
1.123  lemma surj_compose: "[| f ` A = B; g ` B = C |] ==> compose A g f ` A = C"
1.124 -by (auto simp add: image_def compose_eq)
1.125 +  by (auto simp add: image_def compose_eq)
1.126
1.127  lemma inj_on_compose:
1.128 -     "[| f ` A = B; inj_on f A; inj_on g B |] ==> inj_on (compose A g f) A"
1.129 -by (auto simp add: inj_on_def compose_eq)
1.130 +    "[| f ` A = B; inj_on f A; inj_on g B |] ==> inj_on (compose A g f) A"
1.131 +  by (auto simp add: inj_on_def compose_eq)
1.132
1.133
1.134  subsection{*Bounded Abstraction: @{term restrict}*}
1.135
1.136  lemma restrict_in_funcset: "(!!x. x \<in> A ==> f x \<in> B) ==> (\<lambda>x\<in>A. f x) \<in> A -> B"
1.137 -by (simp add: Pi_def restrict_def)
1.138 +  by (simp add: Pi_def restrict_def)
1.139
1.140  lemma restrictI: "(!!x. x \<in> A ==> f x \<in> B x) ==> (\<lambda>x\<in>A. f x) \<in> Pi A B"
1.141 -by (simp add: Pi_def restrict_def)
1.142 +  by (simp add: Pi_def restrict_def)
1.143
1.144  lemma restrict_apply [simp]:
1.145 -     "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else arbitrary)"
1.147 +    "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else arbitrary)"
1.148 +  by (simp add: restrict_def)
1.149
1.150 -lemma restrict_ext:
1.151 +lemma restrict_ext:
1.152      "(!!x. x \<in> A ==> f x = g x) ==> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)"
1.153 -by (simp add: expand_fun_eq Pi_def Pi_def restrict_def)
1.154 +  by (simp add: expand_fun_eq Pi_def Pi_def restrict_def)
1.155
1.156  lemma inj_on_restrict_eq: "inj_on (restrict f A) A = inj_on f A"
1.157 -by (simp add: inj_on_def restrict_def)
1.158 -
1.159 +  by (simp add: inj_on_def restrict_def)
1.160
1.161  lemma Id_compose:
1.162 -     "[|f \<in> A -> B;  f \<in> extensional A|] ==> compose A (\<lambda>y\<in>B. y) f = f"
1.163 -by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
1.164 +    "[|f \<in> A -> B;  f \<in> extensional A|] ==> compose A (\<lambda>y\<in>B. y) f = f"
1.165 +  by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
1.166
1.167  lemma compose_Id:
1.168 -     "[|g \<in> A -> B;  g \<in> extensional A|] ==> compose A g (\<lambda>x\<in>A. x) = g"
1.169 -by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
1.170 +    "[|g \<in> A -> B;  g \<in> extensional A|] ==> compose A g (\<lambda>x\<in>A. x) = g"
1.171 +  by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
1.172
1.173
1.174  subsection{*Extensionality*}
1.175
1.176  lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = arbitrary"
1.178 +  by (simp add: extensional_def)
1.179
1.180  lemma restrict_extensional [simp]: "restrict f A \<in> extensional A"
1.181 -by (simp add: restrict_def extensional_def)
1.182 +  by (simp add: restrict_def extensional_def)
1.183
1.184  lemma compose_extensional [simp]: "compose A f g \<in> extensional A"
1.186 +  by (simp add: compose_def)
1.187
1.188  lemma extensionalityI:
1.189 -     "[| f \<in> extensional A; g \<in> extensional A;
1.190 -         !!x. x\<in>A ==> f x = g x |] ==> f = g"
1.191 -by (force simp add: expand_fun_eq extensional_def)
1.192 +    "[| f \<in> extensional A; g \<in> extensional A;
1.193 +      !!x. x\<in>A ==> f x = g x |] ==> f = g"
1.194 +  by (force simp add: expand_fun_eq extensional_def)
1.195
1.196  lemma Inv_funcset: "f ` A = B ==> (\<lambda>x\<in>B. Inv A f x) : B -> A"
1.197 -apply (unfold Inv_def)
1.198 -apply (fast intro: restrict_in_funcset someI2)
1.199 -done
1.200 +  by (unfold Inv_def) (fast intro: restrict_in_funcset someI2)
1.201
1.202  lemma compose_Inv_id:
1.203 -     "[| inj_on f A;  f ` A = B |]
1.204 +    "[| inj_on f A;  f ` A = B |]
1.205        ==> compose A (\<lambda>y\<in>B. Inv A f y) f = (\<lambda>x\<in>A. x)"
1.207 -apply (rule restrict_ext, auto)
1.208 -apply (erule subst)
1.210 -done
1.211 +  apply (simp add: compose_def)
1.212 +  apply (rule restrict_ext, auto)
1.213 +  apply (erule subst)
1.214 +  apply (simp add: Inv_f_f)
1.215 +  done
1.216
1.217  lemma compose_id_Inv:
1.218 -     "f ` A = B ==> compose B f (\<lambda>y\<in>B. Inv A f y) = (\<lambda>x\<in>B. x)"