1 (* Title: HOL/Library/FuncSet.thy |
1 (* Title: HOL/Library/FuncSet.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Florian Kammueller and Lawrence C Paulson |
3 Author: Florian Kammueller and Lawrence C Paulson |
4 *) |
4 *) |
5 |
5 |
6 header {* |
6 header {* Pi and Function Sets *} |
7 \title{Pi and Function Sets} |
|
8 \author{Florian Kammueller and Lawrence C Paulson} |
|
9 *} |
|
10 |
7 |
11 theory FuncSet = Main: |
8 theory FuncSet = Main: |
12 |
9 |
13 constdefs |
10 constdefs |
14 Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" |
11 Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" |
15 "Pi A B == {f. \<forall>x. x \<in> A --> f(x) \<in> B(x)}" |
12 "Pi A B == {f. \<forall>x. x \<in> A --> f x \<in> B x}" |
16 |
13 |
17 extensional :: "'a set => ('a => 'b) set" |
14 extensional :: "'a set => ('a => 'b) set" |
18 "extensional A == {f. \<forall>x. x~:A --> f(x) = arbitrary}" |
15 "extensional A == {f. \<forall>x. x~:A --> f x = arbitrary}" |
19 |
16 |
20 restrict :: "['a => 'b, 'a set] => ('a => 'b)" |
17 "restrict" :: "['a => 'b, 'a set] => ('a => 'b)" |
21 "restrict f A == (%x. if x \<in> A then f x else arbitrary)" |
18 "restrict f A == (%x. if x \<in> A then f x else arbitrary)" |
22 |
19 |
23 syntax |
20 syntax |
24 "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10) |
21 "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10) |
25 funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr "->" 60) |
22 funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr "->" 60) |
26 "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3%_:_./ _)" [0,0,3] 3) |
23 "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3%_:_./ _)" [0,0,3] 3) |
27 |
24 |
28 syntax (xsymbols) |
25 syntax (xsymbols) |
29 "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi> _\<in>_./ _)" 10) |
26 "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi> _\<in>_./ _)" 10) |
30 funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr "\<rightarrow>" 60) |
27 funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr "\<rightarrow>" 60) |
31 "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3) |
28 "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3) |
32 |
29 |
33 syntax (HTML output) |
30 syntax (HTML output) |
34 "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi> _\<in>_./ _)" 10) |
31 "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi> _\<in>_./ _)" 10) |
35 "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3) |
32 "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3) |
36 |
33 |
37 translations |
34 translations |
38 "PI x:A. B" => "Pi A (%x. B)" |
35 "PI x:A. B" => "Pi A (%x. B)" |
39 "A -> B" => "Pi A (_K B)" |
36 "A -> B" => "Pi A (_K B)" |
40 "%x:A. f" == "restrict (%x. f) A" |
37 "%x:A. f" == "restrict (%x. f) A" |
41 |
38 |
42 constdefs |
39 constdefs |
43 compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)" |
40 "compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)" |
44 "compose A g f == \<lambda>x\<in>A. g (f x)" |
41 "compose A g f == \<lambda>x\<in>A. g (f x)" |
45 |
42 |
46 print_translation {* [("Pi", dependent_tr' ("@Pi", "funcset"))] *} |
43 print_translation {* [("Pi", dependent_tr' ("@Pi", "funcset"))] *} |
47 |
44 |
48 |
45 |
49 subsection{*Basic Properties of @{term Pi}*} |
46 subsection{*Basic Properties of @{term Pi}*} |
50 |
47 |
51 lemma Pi_I: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B" |
48 lemma Pi_I: "(!!x. x \<in> A ==> f x \<in> B x) ==> f \<in> Pi A B" |
52 by (simp add: Pi_def) |
49 by (simp add: Pi_def) |
53 |
50 |
54 lemma funcsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f \<in> A -> B" |
51 lemma funcsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f \<in> A -> B" |
55 by (simp add: Pi_def) |
52 by (simp add: Pi_def) |
56 |
53 |
57 lemma Pi_mem: "[|f: Pi A B; x \<in> A|] ==> f x \<in> B x" |
54 lemma Pi_mem: "[|f: Pi A B; x \<in> A|] ==> f x \<in> B x" |
58 by (simp add: Pi_def) |
55 by (simp add: Pi_def) |
59 |
56 |
60 lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B" |
57 lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B" |
61 by (simp add: Pi_def) |
58 by (simp add: Pi_def) |
62 |
59 |
63 lemma Pi_eq_empty: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})" |
60 lemma Pi_eq_empty: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})" |
64 apply (simp add: Pi_def, auto) |
61 apply (simp add: Pi_def, auto) |
65 txt{*Converse direction requires Axiom of Choice to exhibit a function |
62 txt{*Converse direction requires Axiom of Choice to exhibit a function |
66 picking an element from each non-empty @{term "B x"}*} |
63 picking an element from each non-empty @{term "B x"}*} |
67 apply (drule_tac x = "%u. SOME y. y \<in> B u" in spec, auto) |
64 apply (drule_tac x = "%u. SOME y. y \<in> B u" in spec, auto) |
68 apply (cut_tac P= "%y. y \<in> B x" in some_eq_ex, auto) |
65 apply (cut_tac P= "%y. y \<in> B x" in some_eq_ex, auto) |
69 done |
66 done |
70 |
67 |
71 lemma Pi_empty [simp]: "Pi {} B = UNIV" |
68 lemma Pi_empty [simp]: "Pi {} B = UNIV" |
72 by (simp add: Pi_def) |
69 by (simp add: Pi_def) |
73 |
70 |
74 lemma Pi_UNIV [simp]: "A -> UNIV = UNIV" |
71 lemma Pi_UNIV [simp]: "A -> UNIV = UNIV" |
75 by (simp add: Pi_def) |
72 by (simp add: Pi_def) |
76 |
73 |
77 text{*Covariance of Pi-sets in their second argument*} |
74 text{*Covariance of Pi-sets in their second argument*} |
78 lemma Pi_mono: "(!!x. x \<in> A ==> B x <= C x) ==> Pi A B <= Pi A C" |
75 lemma Pi_mono: "(!!x. x \<in> A ==> B x <= C x) ==> Pi A B <= Pi A C" |
79 by (simp add: Pi_def, blast) |
76 by (simp add: Pi_def, blast) |
80 |
77 |
81 text{*Contravariance of Pi-sets in their first argument*} |
78 text{*Contravariance of Pi-sets in their first argument*} |
82 lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B" |
79 lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B" |
83 by (simp add: Pi_def, blast) |
80 by (simp add: Pi_def, blast) |
84 |
81 |
85 |
82 |
86 subsection{*Composition With a Restricted Domain: @{term compose}*} |
83 subsection{*Composition With a Restricted Domain: @{term compose}*} |
87 |
84 |
88 lemma funcset_compose: |
85 lemma funcset_compose: |
89 "[| f \<in> A -> B; g \<in> B -> C |]==> compose A g f \<in> A -> C" |
86 "[| f \<in> A -> B; g \<in> B -> C |]==> compose A g f \<in> A -> C" |
90 by (simp add: Pi_def compose_def restrict_def) |
87 by (simp add: Pi_def compose_def restrict_def) |
91 |
88 |
92 lemma compose_assoc: |
89 lemma compose_assoc: |
93 "[| f \<in> A -> B; g \<in> B -> C; h \<in> C -> D |] |
90 "[| f \<in> A -> B; g \<in> B -> C; h \<in> C -> D |] |
94 ==> compose A h (compose A g f) = compose A (compose B h g) f" |
91 ==> compose A h (compose A g f) = compose A (compose B h g) f" |
95 by (simp add: expand_fun_eq Pi_def compose_def restrict_def) |
92 by (simp add: expand_fun_eq Pi_def compose_def restrict_def) |
96 |
93 |
97 lemma compose_eq: "x \<in> A ==> compose A g f x = g(f(x))" |
94 lemma compose_eq: "x \<in> A ==> compose A g f x = g(f(x))" |
98 by (simp add: compose_def restrict_def) |
95 by (simp add: compose_def restrict_def) |
99 |
96 |
100 lemma surj_compose: "[| f ` A = B; g ` B = C |] ==> compose A g f ` A = C" |
97 lemma surj_compose: "[| f ` A = B; g ` B = C |] ==> compose A g f ` A = C" |
101 by (auto simp add: image_def compose_eq) |
98 by (auto simp add: image_def compose_eq) |
102 |
99 |
103 lemma inj_on_compose: |
100 lemma inj_on_compose: |
104 "[| f ` A = B; inj_on f A; inj_on g B |] ==> inj_on (compose A g f) A" |
101 "[| f ` A = B; inj_on f A; inj_on g B |] ==> inj_on (compose A g f) A" |
105 by (auto simp add: inj_on_def compose_eq) |
102 by (auto simp add: inj_on_def compose_eq) |
106 |
103 |
107 |
104 |
108 subsection{*Bounded Abstraction: @{term restrict}*} |
105 subsection{*Bounded Abstraction: @{term restrict}*} |
109 |
106 |
110 lemma restrict_in_funcset: "(!!x. x \<in> A ==> f x \<in> B) ==> (\<lambda>x\<in>A. f x) \<in> A -> B" |
107 lemma restrict_in_funcset: "(!!x. x \<in> A ==> f x \<in> B) ==> (\<lambda>x\<in>A. f x) \<in> A -> B" |
111 by (simp add: Pi_def restrict_def) |
108 by (simp add: Pi_def restrict_def) |
112 |
109 |
113 lemma restrictI: "(!!x. x \<in> A ==> f x \<in> B x) ==> (\<lambda>x\<in>A. f x) \<in> Pi A B" |
110 lemma restrictI: "(!!x. x \<in> A ==> f x \<in> B x) ==> (\<lambda>x\<in>A. f x) \<in> Pi A B" |
114 by (simp add: Pi_def restrict_def) |
111 by (simp add: Pi_def restrict_def) |
115 |
112 |
116 lemma restrict_apply [simp]: |
113 lemma restrict_apply [simp]: |
117 "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else arbitrary)" |
114 "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else arbitrary)" |
118 by (simp add: restrict_def) |
115 by (simp add: restrict_def) |
119 |
116 |
120 lemma restrict_ext: |
117 lemma restrict_ext: |
121 "(!!x. x \<in> A ==> f x = g x) ==> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)" |
118 "(!!x. x \<in> A ==> f x = g x) ==> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)" |
122 by (simp add: expand_fun_eq Pi_def Pi_def restrict_def) |
119 by (simp add: expand_fun_eq Pi_def Pi_def restrict_def) |
123 |
120 |
124 lemma inj_on_restrict_eq: "inj_on (restrict f A) A = inj_on f A" |
121 lemma inj_on_restrict_eq: "inj_on (restrict f A) A = inj_on f A" |
125 by (simp add: inj_on_def restrict_def) |
122 by (simp add: inj_on_def restrict_def) |
126 |
|
127 |
123 |
128 lemma Id_compose: |
124 lemma Id_compose: |
129 "[|f \<in> A -> B; f \<in> extensional A|] ==> compose A (\<lambda>y\<in>B. y) f = f" |
125 "[|f \<in> A -> B; f \<in> extensional A|] ==> compose A (\<lambda>y\<in>B. y) f = f" |
130 by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def) |
126 by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def) |
131 |
127 |
132 lemma compose_Id: |
128 lemma compose_Id: |
133 "[|g \<in> A -> B; g \<in> extensional A|] ==> compose A g (\<lambda>x\<in>A. x) = g" |
129 "[|g \<in> A -> B; g \<in> extensional A|] ==> compose A g (\<lambda>x\<in>A. x) = g" |
134 by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def) |
130 by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def) |
135 |
131 |
136 |
132 |
137 subsection{*Extensionality*} |
133 subsection{*Extensionality*} |
138 |
134 |
139 lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = arbitrary" |
135 lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = arbitrary" |
140 by (simp add: extensional_def) |
136 by (simp add: extensional_def) |
141 |
137 |
142 lemma restrict_extensional [simp]: "restrict f A \<in> extensional A" |
138 lemma restrict_extensional [simp]: "restrict f A \<in> extensional A" |
143 by (simp add: restrict_def extensional_def) |
139 by (simp add: restrict_def extensional_def) |
144 |
140 |
145 lemma compose_extensional [simp]: "compose A f g \<in> extensional A" |
141 lemma compose_extensional [simp]: "compose A f g \<in> extensional A" |
146 by (simp add: compose_def) |
142 by (simp add: compose_def) |
147 |
143 |
148 lemma extensionalityI: |
144 lemma extensionalityI: |
149 "[| f \<in> extensional A; g \<in> extensional A; |
145 "[| f \<in> extensional A; g \<in> extensional A; |
150 !!x. x\<in>A ==> f x = g x |] ==> f = g" |
146 !!x. x\<in>A ==> f x = g x |] ==> f = g" |
151 by (force simp add: expand_fun_eq extensional_def) |
147 by (force simp add: expand_fun_eq extensional_def) |
152 |
148 |
153 lemma Inv_funcset: "f ` A = B ==> (\<lambda>x\<in>B. Inv A f x) : B -> A" |
149 lemma Inv_funcset: "f ` A = B ==> (\<lambda>x\<in>B. Inv A f x) : B -> A" |
154 apply (unfold Inv_def) |
150 by (unfold Inv_def) (fast intro: restrict_in_funcset someI2) |
155 apply (fast intro: restrict_in_funcset someI2) |
|
156 done |
|
157 |
151 |
158 lemma compose_Inv_id: |
152 lemma compose_Inv_id: |
159 "[| inj_on f A; f ` A = B |] |
153 "[| inj_on f A; f ` A = B |] |
160 ==> compose A (\<lambda>y\<in>B. Inv A f y) f = (\<lambda>x\<in>A. x)" |
154 ==> compose A (\<lambda>y\<in>B. Inv A f y) f = (\<lambda>x\<in>A. x)" |
161 apply (simp add: compose_def) |
155 apply (simp add: compose_def) |
162 apply (rule restrict_ext, auto) |
156 apply (rule restrict_ext, auto) |
163 apply (erule subst) |
157 apply (erule subst) |
164 apply (simp add: Inv_f_f) |
158 apply (simp add: Inv_f_f) |
165 done |
159 done |
166 |
160 |
167 lemma compose_id_Inv: |
161 lemma compose_id_Inv: |
168 "f ` A = B ==> compose B f (\<lambda>y\<in>B. Inv A f y) = (\<lambda>x\<in>B. x)" |
162 "f ` A = B ==> compose B f (\<lambda>y\<in>B. Inv A f y) = (\<lambda>x\<in>B. x)" |
169 apply (simp add: compose_def) |
163 apply (simp add: compose_def) |
170 apply (rule restrict_ext) |
164 apply (rule restrict_ext) |
171 apply (simp add: f_Inv_f) |
165 apply (simp add: f_Inv_f) |
172 done |
166 done |
173 |
167 |
174 end |
168 end |