98 Pair :: "['a, 'b] => 'a * 'b" |
98 Pair :: "['a, 'b] => 'a * 'b" |
99 Sigma :: "['a set, 'a => 'b set] => ('a * 'b) set" |
99 Sigma :: "['a set, 'a => 'b set] => ('a * 'b) set" |
100 |
100 |
101 local |
101 local |
102 |
102 |
|
103 defs |
|
104 Pair_def: "Pair a b == Abs_Prod (Pair_Rep a b)" |
|
105 fst_def: "fst p == THE a. EX b. p = Pair a b" |
|
106 snd_def: "snd p == THE b. EX a. p = Pair a b" |
|
107 split_def: "split == (%c p. c (fst p) (snd p))" |
|
108 curry_def: "curry == (%c x y. c (Pair x y))" |
|
109 prod_fun_def: "prod_fun f g == split (%x y. Pair (f x) (g y))" |
|
110 Sigma_def: "Sigma A B == UN x:A. UN y:B x. {Pair x y}" |
|
111 |
|
112 abbreviation |
|
113 Times :: "['a set, 'b set] => ('a * 'b) set" (infixr "<*>" 80) |
|
114 "A <*> B == Sigma A (%_. B)" |
|
115 |
|
116 abbreviation (xsymbols) |
|
117 Times1 (infixr "\<times>" 80) |
|
118 "Times1 == Times" |
|
119 |
|
120 abbreviation (HTML output) |
|
121 Times2 (infixr "\<times>" 80) |
|
122 "Times2 == Times" |
|
123 |
|
124 |
|
125 subsubsection {* Concrete syntax *} |
|
126 |
103 text {* |
127 text {* |
104 Patterns -- extends pre-defined type @{typ pttrn} used in |
128 Patterns -- extends pre-defined type @{typ pttrn} used in |
105 abstractions. |
129 abstractions. |
106 *} |
130 *} |
107 |
131 |
114 "_tuple_args" :: "'a => tuple_args => tuple_args" ("_,/ _") |
138 "_tuple_args" :: "'a => tuple_args => tuple_args" ("_,/ _") |
115 "_pattern" :: "[pttrn, patterns] => pttrn" ("'(_,/ _')") |
139 "_pattern" :: "[pttrn, patterns] => pttrn" ("'(_,/ _')") |
116 "" :: "pttrn => patterns" ("_") |
140 "" :: "pttrn => patterns" ("_") |
117 "_patterns" :: "[pttrn, patterns] => patterns" ("_,/ _") |
141 "_patterns" :: "[pttrn, patterns] => patterns" ("_,/ _") |
118 "@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10) |
142 "@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10) |
119 "@Times" ::"['a set, 'a => 'b set] => ('a * 'b) set" (infixr "<*>" 80) |
|
120 |
143 |
121 translations |
144 translations |
122 "(x, y)" == "Pair x y" |
145 "(x, y)" == "Pair x y" |
123 "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))" |
146 "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))" |
124 "%(x,y,zs).b" == "split(%x (y,zs).b)" |
147 "%(x,y,zs).b" == "split(%x (y,zs).b)" |
125 "%(x,y).b" == "split(%x y. b)" |
148 "%(x,y).b" == "split(%x y. b)" |
126 "_abs (Pair x y) t" => "%(x,y).t" |
149 "_abs (Pair x y) t" => "%(x,y).t" |
127 (* The last rule accommodates tuples in `case C ... (x,y) ... => ...' |
150 (* The last rule accommodates tuples in `case C ... (x,y) ... => ...' |
128 The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *) |
151 The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *) |
129 |
152 "SIGMA x:A. B" == "Sigma A (%x. B)" |
130 "SIGMA x:A. B" => "Sigma A (%x. B)" |
|
131 "A <*> B" => "Sigma A (%_. B)" |
|
132 |
153 |
133 (* reconstructs pattern from (nested) splits, avoiding eta-contraction of body*) |
154 (* reconstructs pattern from (nested) splits, avoiding eta-contraction of body*) |
134 (* works best with enclosing "let", if "let" does not avoid eta-contraction *) |
155 (* works best with enclosing "let", if "let" does not avoid eta-contraction *) |
135 print_translation {* |
156 print_translation {* |
136 let fun split_tr' [Abs (x,T,t as (Abs abs))] = |
157 let fun split_tr' [Abs (x,T,t as (Abs abs))] = |
155 | split_tr' _ = raise Match; |
176 | split_tr' _ = raise Match; |
156 in [("split", split_tr')] |
177 in [("split", split_tr')] |
157 end |
178 end |
158 *} |
179 *} |
159 |
180 |
160 |
|
161 (* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *) |
181 (* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *) |
162 typed_print_translation {* |
182 typed_print_translation {* |
163 let |
183 let |
164 fun split_guess_names_tr' _ T [Abs (x,_,Abs _)] = raise Match |
184 fun split_guess_names_tr' _ T [Abs (x,_,Abs _)] = raise Match |
165 | split_guess_names_tr' _ T [Abs (x,xT,t)] = |
185 | split_guess_names_tr' _ T [Abs (x,xT,t)] = |
182 | split_guess_names_tr' _ _ _ = raise Match; |
202 | split_guess_names_tr' _ _ _ = raise Match; |
183 in [("split", split_guess_names_tr')] |
203 in [("split", split_guess_names_tr')] |
184 end |
204 end |
185 *} |
205 *} |
186 |
206 |
187 text{*Deleted x-symbol and html support using @{text"\<Sigma>"} (Sigma) because of the danger of confusion with Sum.*} |
|
188 |
|
189 syntax (xsymbols) |
|
190 "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80) |
|
191 |
|
192 syntax (HTML output) |
|
193 "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80) |
|
194 |
|
195 print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *} |
|
196 |
|
197 |
|
198 subsubsection {* Definitions *} |
|
199 |
|
200 defs |
|
201 Pair_def: "Pair a b == Abs_Prod(Pair_Rep a b)" |
|
202 fst_def: "fst p == THE a. EX b. p = (a, b)" |
|
203 snd_def: "snd p == THE b. EX a. p = (a, b)" |
|
204 split_def: "split == (%c p. c (fst p) (snd p))" |
|
205 curry_def: "curry == (%c x y. c (x,y))" |
|
206 prod_fun_def: "prod_fun f g == split(%x y.(f(x), g(y)))" |
|
207 Sigma_def: "Sigma A B == UN x:A. UN y:B(x). {(x, y)}" |
|
208 |
|
209 |
207 |
210 subsubsection {* Lemmas and proof tool setup *} |
208 subsubsection {* Lemmas and proof tool setup *} |
211 |
209 |
212 lemma ProdI: "Pair_Rep a b : Prod" |
210 lemma ProdI: "Pair_Rep a b : Prod" |
213 by (unfold Prod_def) blast |
211 unfolding Prod_def by blast |
214 |
212 |
215 lemma Pair_Rep_inject: "Pair_Rep a b = Pair_Rep a' b' ==> a = a' & b = b'" |
213 lemma Pair_Rep_inject: "Pair_Rep a b = Pair_Rep a' b' ==> a = a' & b = b'" |
216 apply (unfold Pair_Rep_def) |
214 apply (unfold Pair_Rep_def) |
217 apply (drule fun_cong [THEN fun_cong], blast) |
215 apply (drule fun_cong [THEN fun_cong], blast) |
218 done |
216 done |
233 |
231 |
234 lemma Pair_eq [iff]: "((a, b) = (a', b')) = (a = a' & b = b')" |
232 lemma Pair_eq [iff]: "((a, b) = (a', b')) = (a = a' & b = b')" |
235 by (blast elim!: Pair_inject) |
233 by (blast elim!: Pair_inject) |
236 |
234 |
237 lemma fst_conv [simp]: "fst (a, b) = a" |
235 lemma fst_conv [simp]: "fst (a, b) = a" |
238 by (unfold fst_def) blast |
236 unfolding fst_def by blast |
239 |
237 |
240 lemma snd_conv [simp]: "snd (a, b) = b" |
238 lemma snd_conv [simp]: "snd (a, b) = b" |
241 by (unfold snd_def) blast |
239 unfolding snd_def by blast |
242 |
240 |
243 lemma fst_eqD: "fst (x, y) = a ==> x = a" |
241 lemma fst_eqD: "fst (x, y) = a ==> x = a" |
244 by simp |
242 by simp |
245 |
243 |
246 lemma snd_eqD: "snd (x, y) = a ==> y = a" |
244 lemma snd_eqD: "snd (x, y) = a ==> y = a" |
253 apply (rule Rep_Prod_inverse [symmetric, THEN trans]) |
251 apply (rule Rep_Prod_inverse [symmetric, THEN trans]) |
254 apply (erule arg_cong) |
252 apply (erule arg_cong) |
255 done |
253 done |
256 |
254 |
257 lemma PairE [cases type: *]: "(!!x y. p = (x, y) ==> Q) ==> Q" |
255 lemma PairE [cases type: *]: "(!!x y. p = (x, y) ==> Q) ==> Q" |
258 by (insert PairE_lemma [of p]) blast |
256 using PairE_lemma [of p] by blast |
259 |
257 |
260 ML {* |
258 ML {* |
261 local val PairE = thm "PairE" in |
259 local val PairE = thm "PairE" in |
262 fun pair_tac s = |
260 fun pair_tac s = |
263 EVERY' [res_inst_tac [("p", s)] PairE, hyp_subst_tac, K prune_params_tac]; |
261 EVERY' [res_inst_tac [("p", s)] PairE, hyp_subst_tac, K prune_params_tac]; |
279 |
277 |
280 lemma split_paired_all: "(!!x. PROP P x) == (!!a b. PROP P (a, b))" |
278 lemma split_paired_all: "(!!x. PROP P x) == (!!a b. PROP P (a, b))" |
281 proof |
279 proof |
282 fix a b |
280 fix a b |
283 assume "!!x. PROP P x" |
281 assume "!!x. PROP P x" |
284 thus "PROP P (a, b)" . |
282 then show "PROP P (a, b)" . |
285 next |
283 next |
286 fix x |
284 fix x |
287 assume "!!a b. PROP P (a, b)" |
285 assume "!!a b. PROP P (a, b)" |
288 hence "PROP P (fst x, snd x)" . |
286 from `PROP P (fst x, snd x)` show "PROP P x" by simp |
289 thus "PROP P x" by simp |
|
290 qed |
287 qed |
291 |
288 |
292 lemmas split_tupled_all = split_paired_all unit_all_eq2 |
289 lemmas split_tupled_all = split_paired_all unit_all_eq2 |
293 |
290 |
294 text {* |
291 text {* |