src/HOL/Library/FuncSet.thy
 author hoelzl Mon Aug 23 19:35:57 2010 +0200 (2010-08-23) changeset 38656 d5d342611edb parent 33271 7be66dee1a5a child 39198 f967a16dfcdd permissions -rw-r--r--
Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.
```     1 (*  Title:      HOL/Library/FuncSet.thy
```
```     2     Author:     Florian Kammueller and Lawrence C Paulson
```
```     3 *)
```
```     4
```
```     5 header {* Pi and Function Sets *}
```
```     6
```
```     7 theory FuncSet
```
```     8 imports Hilbert_Choice Main
```
```     9 begin
```
```    10
```
```    11 definition
```
```    12   Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" where
```
```    13   "Pi A B = {f. \<forall>x. x \<in> A --> f x \<in> B x}"
```
```    14
```
```    15 definition
```
```    16   extensional :: "'a set => ('a => 'b) set" where
```
```    17   "extensional A = {f. \<forall>x. x~:A --> f x = undefined}"
```
```    18
```
```    19 definition
```
```    20   "restrict" :: "['a => 'b, 'a set] => ('a => 'b)" where
```
```    21   "restrict f A = (%x. if x \<in> A then f x else undefined)"
```
```    22
```
```    23 abbreviation
```
```    24   funcset :: "['a set, 'b set] => ('a => 'b) set"
```
```    25     (infixr "->" 60) where
```
```    26   "A -> B == Pi A (%_. B)"
```
```    27
```
```    28 notation (xsymbols)
```
```    29   funcset  (infixr "\<rightarrow>" 60)
```
```    30
```
```    31 syntax
```
```    32   "_Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
```
```    33   "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3%_:_./ _)" [0,0,3] 3)
```
```    34
```
```    35 syntax (xsymbols)
```
```    36   "_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
```
```    37   "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
```
```    38
```
```    39 syntax (HTML output)
```
```    40   "_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
```
```    41   "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
```
```    42
```
```    43 translations
```
```    44   "PI x:A. B" == "CONST Pi A (%x. B)"
```
```    45   "%x:A. f" == "CONST restrict (%x. f) A"
```
```    46
```
```    47 definition
```
```    48   "compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)" where
```
```    49   "compose A g f = (\<lambda>x\<in>A. g (f x))"
```
```    50
```
```    51
```
```    52 subsection{*Basic Properties of @{term Pi}*}
```
```    53
```
```    54 lemma Pi_I[intro!]: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B"
```
```    55   by (simp add: Pi_def)
```
```    56
```
```    57 lemma Pi_I'[simp]: "(!!x. x : A --> f x : B x) ==> f : Pi A B"
```
```    58 by(simp add:Pi_def)
```
```    59
```
```    60 lemma funcsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f \<in> A -> B"
```
```    61   by (simp add: Pi_def)
```
```    62
```
```    63 lemma Pi_mem: "[|f: Pi A B; x \<in> A|] ==> f x \<in> B x"
```
```    64   by (simp add: Pi_def)
```
```    65
```
```    66 lemma PiE [elim]:
```
```    67   "f : Pi A B ==> (f x : B x ==> Q) ==> (x ~: A ==> Q) ==> Q"
```
```    68 by(auto simp: Pi_def)
```
```    69
```
```    70 lemma Pi_cong:
```
```    71   "(\<And> w. w \<in> A \<Longrightarrow> f w = g w) \<Longrightarrow> f \<in> Pi A B \<longleftrightarrow> g \<in> Pi A B"
```
```    72   by (auto simp: Pi_def)
```
```    73
```
```    74 lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A"
```
```    75   by (auto intro: Pi_I)
```
```    76
```
```    77 lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B"
```
```    78   by (simp add: Pi_def)
```
```    79
```
```    80 lemma funcset_image: "f \<in> A\<rightarrow>B ==> f ` A \<subseteq> B"
```
```    81 by auto
```
```    82
```
```    83 lemma Pi_eq_empty[simp]: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})"
```
```    84 apply (simp add: Pi_def, auto)
```
```    85 txt{*Converse direction requires Axiom of Choice to exhibit a function
```
```    86 picking an element from each non-empty @{term "B x"}*}
```
```    87 apply (drule_tac x = "%u. SOME y. y \<in> B u" in spec, auto)
```
```    88 apply (cut_tac P= "%y. y \<in> B x" in some_eq_ex, auto)
```
```    89 done
```
```    90
```
```    91 lemma Pi_empty [simp]: "Pi {} B = UNIV"
```
```    92 by (simp add: Pi_def)
```
```    93
```
```    94 lemma Pi_UNIV [simp]: "A -> UNIV = UNIV"
```
```    95 by (simp add: Pi_def)
```
```    96 (*
```
```    97 lemma funcset_id [simp]: "(%x. x): A -> A"
```
```    98   by (simp add: Pi_def)
```
```    99 *)
```
```   100 text{*Covariance of Pi-sets in their second argument*}
```
```   101 lemma Pi_mono: "(!!x. x \<in> A ==> B x <= C x) ==> Pi A B <= Pi A C"
```
```   102 by auto
```
```   103
```
```   104 text{*Contravariance of Pi-sets in their first argument*}
```
```   105 lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B"
```
```   106 by auto
```
```   107
```
```   108 lemma prod_final:
```
```   109   assumes 1: "fst \<circ> f \<in> Pi A B" and 2: "snd \<circ> f \<in> Pi A C"
```
```   110   shows "f \<in> (\<Pi> z \<in> A. B z \<times> C z)"
```
```   111 proof (rule Pi_I)
```
```   112   fix z
```
```   113   assume z: "z \<in> A"
```
```   114   have "f z = (fst (f z), snd (f z))"
```
```   115     by simp
```
```   116   also have "...  \<in> B z \<times> C z"
```
```   117     by (metis SigmaI PiE o_apply 1 2 z)
```
```   118   finally show "f z \<in> B z \<times> C z" .
```
```   119 qed
```
```   120
```
```   121
```
```   122 subsection{*Composition With a Restricted Domain: @{term compose}*}
```
```   123
```
```   124 lemma funcset_compose:
```
```   125   "[| f \<in> A -> B; g \<in> B -> C |]==> compose A g f \<in> A -> C"
```
```   126 by (simp add: Pi_def compose_def restrict_def)
```
```   127
```
```   128 lemma compose_assoc:
```
```   129     "[| f \<in> A -> B; g \<in> B -> C; h \<in> C -> D |]
```
```   130       ==> compose A h (compose A g f) = compose A (compose B h g) f"
```
```   131 by (simp add: expand_fun_eq Pi_def compose_def restrict_def)
```
```   132
```
```   133 lemma compose_eq: "x \<in> A ==> compose A g f x = g(f(x))"
```
```   134 by (simp add: compose_def restrict_def)
```
```   135
```
```   136 lemma surj_compose: "[| f ` A = B; g ` B = C |] ==> compose A g f ` A = C"
```
```   137   by (auto simp add: image_def compose_eq)
```
```   138
```
```   139
```
```   140 subsection{*Bounded Abstraction: @{term restrict}*}
```
```   141
```
```   142 lemma restrict_in_funcset: "(!!x. x \<in> A ==> f x \<in> B) ==> (\<lambda>x\<in>A. f x) \<in> A -> B"
```
```   143   by (simp add: Pi_def restrict_def)
```
```   144
```
```   145 lemma restrictI[intro!]: "(!!x. x \<in> A ==> f x \<in> B x) ==> (\<lambda>x\<in>A. f x) \<in> Pi A B"
```
```   146   by (simp add: Pi_def restrict_def)
```
```   147
```
```   148 lemma restrict_apply [simp]:
```
```   149     "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else undefined)"
```
```   150   by (simp add: restrict_def)
```
```   151
```
```   152 lemma restrict_ext:
```
```   153     "(!!x. x \<in> A ==> f x = g x) ==> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)"
```
```   154   by (simp add: expand_fun_eq Pi_def restrict_def)
```
```   155
```
```   156 lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A"
```
```   157   by (simp add: inj_on_def restrict_def)
```
```   158
```
```   159 lemma Id_compose:
```
```   160     "[|f \<in> A -> B;  f \<in> extensional A|] ==> compose A (\<lambda>y\<in>B. y) f = f"
```
```   161   by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
```
```   162
```
```   163 lemma compose_Id:
```
```   164     "[|g \<in> A -> B;  g \<in> extensional A|] ==> compose A g (\<lambda>x\<in>A. x) = g"
```
```   165   by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
```
```   166
```
```   167 lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A"
```
```   168   by (auto simp add: restrict_def)
```
```   169
```
```   170
```
```   171 subsection{*Bijections Between Sets*}
```
```   172
```
```   173 text{*The definition of @{const bij_betw} is in @{text "Fun.thy"}, but most of
```
```   174 the theorems belong here, or need at least @{term Hilbert_Choice}.*}
```
```   175
```
```   176 lemma bij_betw_imp_funcset: "bij_betw f A B \<Longrightarrow> f \<in> A \<rightarrow> B"
```
```   177 by (auto simp add: bij_betw_def)
```
```   178
```
```   179 lemma inj_on_compose:
```
```   180   "[| bij_betw f A B; inj_on g B |] ==> inj_on (compose A g f) A"
```
```   181 by (auto simp add: bij_betw_def inj_on_def compose_eq)
```
```   182
```
```   183 lemma bij_betw_compose:
```
```   184   "[| bij_betw f A B; bij_betw g B C |] ==> bij_betw (compose A g f) A C"
```
```   185 apply (simp add: bij_betw_def compose_eq inj_on_compose)
```
```   186 apply (auto simp add: compose_def image_def)
```
```   187 done
```
```   188
```
```   189 lemma bij_betw_restrict_eq [simp]:
```
```   190   "bij_betw (restrict f A) A B = bij_betw f A B"
```
```   191 by (simp add: bij_betw_def)
```
```   192
```
```   193
```
```   194 subsection{*Extensionality*}
```
```   195
```
```   196 lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = undefined"
```
```   197 by (simp add: extensional_def)
```
```   198
```
```   199 lemma restrict_extensional [simp]: "restrict f A \<in> extensional A"
```
```   200 by (simp add: restrict_def extensional_def)
```
```   201
```
```   202 lemma compose_extensional [simp]: "compose A f g \<in> extensional A"
```
```   203 by (simp add: compose_def)
```
```   204
```
```   205 lemma extensionalityI:
```
```   206   "[| f \<in> extensional A; g \<in> extensional A;
```
```   207       !!x. x\<in>A ==> f x = g x |] ==> f = g"
```
```   208 by (force simp add: expand_fun_eq extensional_def)
```
```   209
```
```   210 lemma inv_into_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_into A f x) : B -> A"
```
```   211 by (unfold inv_into_def) (fast intro: someI2)
```
```   212
```
```   213 lemma compose_inv_into_id:
```
```   214   "bij_betw f A B ==> compose A (\<lambda>y\<in>B. inv_into A f y) f = (\<lambda>x\<in>A. x)"
```
```   215 apply (simp add: bij_betw_def compose_def)
```
```   216 apply (rule restrict_ext, auto)
```
```   217 done
```
```   218
```
```   219 lemma compose_id_inv_into:
```
```   220   "f ` A = B ==> compose B f (\<lambda>y\<in>B. inv_into A f y) = (\<lambda>x\<in>B. x)"
```
```   221 apply (simp add: compose_def)
```
```   222 apply (rule restrict_ext)
```
```   223 apply (simp add: f_inv_into_f)
```
```   224 done
```
```   225
```
```   226
```
```   227 subsection{*Cardinality*}
```
```   228
```
```   229 lemma card_inj: "[|f \<in> A\<rightarrow>B; inj_on f A; finite B|] ==> card(A) \<le> card(B)"
```
```   230 by (rule card_inj_on_le) auto
```
```   231
```
```   232 lemma card_bij:
```
```   233   "[|f \<in> A\<rightarrow>B; inj_on f A;
```
```   234      g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
```
```   235 by (blast intro: card_inj order_antisym)
```
```   236
```
```   237 end
```