src/HOL/Library/FuncSet.thy
changeset 19736 d8d0f8f51d69
parent 19656 09be06943252
child 20362 bbff23c3e2ca
     1.1 --- a/src/HOL/Library/FuncSet.thy	Sat May 27 17:42:00 2006 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Sat May 27 17:42:02 2006 +0200
     1.3 @@ -9,15 +9,15 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -constdefs
     1.8 +definition
     1.9    Pi :: "['a set, 'a => 'b set] => ('a => 'b) set"
    1.10 -  "Pi A B == {f. \<forall>x. x \<in> A --> f x \<in> B x}"
    1.11 +  "Pi A B = {f. \<forall>x. x \<in> A --> f x \<in> B x}"
    1.12  
    1.13    extensional :: "'a set => ('a => 'b) set"
    1.14 -  "extensional A == {f. \<forall>x. x~:A --> f x = arbitrary}"
    1.15 +  "extensional A = {f. \<forall>x. x~:A --> f x = arbitrary}"
    1.16  
    1.17    "restrict" :: "['a => 'b, 'a set] => ('a => 'b)"
    1.18 -  "restrict f A == (%x. if x \<in> A then f x else arbitrary)"
    1.19 +  "restrict f A = (%x. if x \<in> A then f x else arbitrary)"
    1.20  
    1.21  abbreviation
    1.22    funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr "->" 60)
    1.23 @@ -27,24 +27,24 @@
    1.24    funcset  (infixr "\<rightarrow>" 60)
    1.25  
    1.26  syntax
    1.27 -  "@Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
    1.28 -  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3%_:_./ _)" [0,0,3] 3)
    1.29 +  "_Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
    1.30 +  "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3%_:_./ _)" [0,0,3] 3)
    1.31  
    1.32  syntax (xsymbols)
    1.33 -  "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
    1.34 -  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
    1.35 +  "_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
    1.36 +  "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
    1.37  
    1.38  syntax (HTML output)
    1.39 -  "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
    1.40 -  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
    1.41 +  "_Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
    1.42 +  "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
    1.43  
    1.44  translations
    1.45    "PI x:A. B" == "Pi A (%x. B)"
    1.46    "%x:A. f" == "restrict (%x. f) A"
    1.47  
    1.48 -constdefs
    1.49 +definition
    1.50    "compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
    1.51 -  "compose A g f == \<lambda>x\<in>A. g (f x)"
    1.52 +  "compose A g f = (\<lambda>x\<in>A. g (f x))"
    1.53  
    1.54  
    1.55  subsection{*Basic Properties of @{term Pi}*}
    1.56 @@ -62,7 +62,7 @@
    1.57    by (simp add: Pi_def)
    1.58  
    1.59  lemma funcset_image: "f \<in> A\<rightarrow>B ==> f ` A \<subseteq> B"
    1.60 -by (auto simp add: Pi_def)
    1.61 +  by (auto simp add: Pi_def)
    1.62  
    1.63  lemma Pi_eq_empty: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})"
    1.64  apply (simp add: Pi_def, auto)
    1.65 @@ -133,7 +133,7 @@
    1.66    by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
    1.67  
    1.68  lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A"
    1.69 -  by (auto simp add: restrict_def) 
    1.70 +  by (auto simp add: restrict_def)
    1.71  
    1.72  
    1.73  subsection{*Bijections Between Sets*}
    1.74 @@ -141,21 +141,21 @@
    1.75  text{*The basic definition could be moved to @{text "Fun.thy"}, but most of
    1.76  the theorems belong here, or need at least @{term Hilbert_Choice}.*}
    1.77  
    1.78 -constdefs
    1.79 -  bij_betw :: "['a => 'b, 'a set, 'b set] => bool"         (*bijective*)
    1.80 -    "bij_betw f A B == inj_on f A & f ` A = B"
    1.81 +definition
    1.82 +  bij_betw :: "['a => 'b, 'a set, 'b set] => bool"         -- {* bijective *}
    1.83 +  "bij_betw f A B = (inj_on f A & f ` A = B)"
    1.84  
    1.85  lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
    1.86 -by (simp add: bij_betw_def)
    1.87 +  by (simp add: bij_betw_def)
    1.88  
    1.89  lemma bij_betw_imp_funcset: "bij_betw f A B \<Longrightarrow> f \<in> A \<rightarrow> B"
    1.90 -by (auto simp add: bij_betw_def inj_on_Inv Pi_def)
    1.91 +  by (auto simp add: bij_betw_def inj_on_Inv Pi_def)
    1.92  
    1.93  lemma bij_betw_Inv: "bij_betw f A B \<Longrightarrow> bij_betw (Inv A f) B A"
    1.94 -apply (auto simp add: bij_betw_def inj_on_Inv Inv_mem) 
    1.95 -apply (simp add: image_compose [symmetric] o_def) 
    1.96 -apply (simp add: image_def Inv_f_f) 
    1.97 -done
    1.98 +  apply (auto simp add: bij_betw_def inj_on_Inv Inv_mem)
    1.99 +  apply (simp add: image_compose [symmetric] o_def)
   1.100 +  apply (simp add: image_def Inv_f_f)
   1.101 +  done
   1.102  
   1.103  lemma inj_on_compose:
   1.104      "[| bij_betw f A B; inj_on g B |] ==> inj_on (compose A g f) A"
   1.105 @@ -163,9 +163,9 @@
   1.106  
   1.107  lemma bij_betw_compose:
   1.108      "[| bij_betw f A B; bij_betw g B C |] ==> bij_betw (compose A g f) A C"
   1.109 -apply (simp add: bij_betw_def compose_eq inj_on_compose)
   1.110 -apply (auto simp add: compose_def image_def)
   1.111 -done
   1.112 +  apply (simp add: bij_betw_def compose_eq inj_on_compose)
   1.113 +  apply (auto simp add: compose_def image_def)
   1.114 +  done
   1.115  
   1.116  lemma bij_betw_restrict_eq [simp]:
   1.117       "bij_betw (restrict f A) A B = bij_betw f A B"
   1.118 @@ -210,13 +210,13 @@
   1.119  subsection{*Cardinality*}
   1.120  
   1.121  lemma card_inj: "[|f \<in> A\<rightarrow>B; inj_on f A; finite B|] ==> card(A) \<le> card(B)"
   1.122 -apply (rule card_inj_on_le)
   1.123 -apply (auto simp add: Pi_def)
   1.124 -done
   1.125 +  apply (rule card_inj_on_le)
   1.126 +    apply (auto simp add: Pi_def)
   1.127 +  done
   1.128  
   1.129  lemma card_bij:
   1.130       "[|f \<in> A\<rightarrow>B; inj_on f A;
   1.131          g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
   1.132 -by (blast intro: card_inj order_antisym)
   1.133 +  by (blast intro: card_inj order_antisym)
   1.134  
   1.135  end