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.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.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
```