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.7 -header {*
     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.60 -by (simp add: Pi_def)
    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.64 -by (simp add: Pi_def)
    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.68 -by (simp add: Pi_def)
    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.72 -by (simp add: Pi_def)
    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.85 -by (simp add: Pi_def)
    1.86 +  by (simp add: Pi_def)
    1.87  
    1.88  lemma Pi_UNIV [simp]: "A -> UNIV = UNIV"
    1.89 -by (simp add: Pi_def)
    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.146 -by (simp add: restrict_def)
   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.177 -by (simp add: extensional_def)
   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.185 -by (simp add: compose_def)
   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.206 -apply (simp add: compose_def)
   1.207 -apply (rule restrict_ext, auto)
   1.208 -apply (erule subst)
   1.209 -apply (simp add: Inv_f_f)
   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)"
   1.219 -apply (simp add: compose_def)
   1.220 -apply (rule restrict_ext)
   1.221 -apply (simp add: f_Inv_f)
   1.222 -done
   1.223 +    "f ` A = B ==> compose B f (\<lambda>y\<in>B. Inv A f y) = (\<lambda>x\<in>B. x)"
   1.224 +  apply (simp add: compose_def)
   1.225 +  apply (rule restrict_ext)
   1.226 +  apply (simp add: f_Inv_f)
   1.227 +  done
   1.228  
   1.229  end