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