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