1.1 --- a/src/HOL/Product_Type.thy Fri May 28 11:23:34 2010 +0200
1.2 +++ b/src/HOL/Product_Type.thy Fri May 28 13:37:47 2010 +0200
1.3 @@ -34,7 +34,7 @@
1.4 (Haskell -)
1.5
1.6
1.7 -subsection {* Unit *}
1.8 +subsection {* The @{text unit} type *}
1.9
1.10 typedef unit = "{True}"
1.11 proof
1.12 @@ -90,8 +90,6 @@
1.13
1.14 end
1.15
1.16 -text {* code generator setup *}
1.17 -
1.18 lemma [code]:
1.19 "eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+
1.20
1.21 @@ -101,18 +99,18 @@
1.22 (Haskell "()")
1.23 (Scala "Unit")
1.24
1.25 +code_const Unity
1.26 + (SML "()")
1.27 + (OCaml "()")
1.28 + (Haskell "()")
1.29 + (Scala "()")
1.30 +
1.31 code_instance unit :: eq
1.32 (Haskell -)
1.33
1.34 code_const "eq_class.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
1.35 (Haskell infixl 4 "==")
1.36
1.37 -code_const Unity
1.38 - (SML "()")
1.39 - (OCaml "()")
1.40 - (Haskell "()")
1.41 - (Scala "()")
1.42 -
1.43 code_reserved SML
1.44 unit
1.45
1.46 @@ -123,13 +121,11 @@
1.47 Unit
1.48
1.49
1.50 -subsection {* Pairs *}
1.51 +subsection {* The product type *}
1.52
1.53 -subsubsection {* Product type, basic operations and concrete syntax *}
1.54 +subsubsection {* Type definition *}
1.55
1.56 -definition
1.57 - Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
1.58 -where
1.59 +definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
1.60 "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
1.61
1.62 global
1.63 @@ -149,19 +145,34 @@
1.64
1.65 consts
1.66 Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b"
1.67 - fst :: "'a \<times> 'b \<Rightarrow> 'a"
1.68 - snd :: "'a \<times> 'b \<Rightarrow> 'b"
1.69 - split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"
1.70 - curry :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c"
1.71
1.72 local
1.73
1.74 defs
1.75 Pair_def: "Pair a b == Abs_Prod (Pair_Rep a b)"
1.76 - fst_def: "fst p == THE a. EX b. p = Pair a b"
1.77 - snd_def: "snd p == THE b. EX a. p = Pair a b"
1.78 - split_def: "split == (%c p. c (fst p) (snd p))"
1.79 - curry_def: "curry == (%c x y. c (Pair x y))"
1.80 +
1.81 +rep_datatype (prod) Pair proof -
1.82 + fix P :: "'a \<times> 'b \<Rightarrow> bool" and p
1.83 + assume "\<And>a b. P (Pair a b)"
1.84 + then show "P p" by (cases p) (auto simp add: Prod_def Pair_def Pair_Rep_def)
1.85 +next
1.86 + fix a c :: 'a and b d :: 'b
1.87 + have "Pair_Rep a b = Pair_Rep c d \<longleftrightarrow> a = c \<and> b = d"
1.88 + by (auto simp add: Pair_Rep_def expand_fun_eq)
1.89 + moreover have "Pair_Rep a b \<in> Prod" and "Pair_Rep c d \<in> Prod"
1.90 + by (auto simp add: Prod_def)
1.91 + ultimately show "Pair a b = Pair c d \<longleftrightarrow> a = c \<and> b = d"
1.92 + by (simp add: Pair_def Abs_Prod_inject)
1.93 +qed
1.94 +
1.95 +
1.96 +subsubsection {* Tuple syntax *}
1.97 +
1.98 +global consts
1.99 + split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"
1.100 +
1.101 +local defs
1.102 + split_prod_case: "split == prod_case"
1.103
1.104 text {*
1.105 Patterns -- extends pre-defined type @{typ pttrn} used in
1.106 @@ -185,8 +196,8 @@
1.107 "%(x, y, zs). b" == "CONST split (%x (y, zs). b)"
1.108 "%(x, y). b" == "CONST split (%x y. b)"
1.109 "_abs (CONST Pair x y) t" => "%(x, y). t"
1.110 - (* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
1.111 - The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
1.112 + -- {* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
1.113 + The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *}
1.114
1.115 (*reconstruct pattern from (nested) splits, avoiding eta-contraction of body;
1.116 works best with enclosing "let", if "let" does not avoid eta-contraction*)
1.117 @@ -258,57 +269,149 @@
1.118 *}
1.119
1.120
1.121 -text {* Towards a datatype declaration *}
1.122 +subsubsection {* Code generator setup *}
1.123 +
1.124 +lemma split_case_cert:
1.125 + assumes "CASE \<equiv> split f"
1.126 + shows "CASE (a, b) \<equiv> f a b"
1.127 + using assms by (simp add: split_prod_case)
1.128 +
1.129 +setup {*
1.130 + Code.add_case @{thm split_case_cert}
1.131 +*}
1.132 +
1.133 +code_type *
1.134 + (SML infix 2 "*")
1.135 + (OCaml infix 2 "*")
1.136 + (Haskell "!((_),/ (_))")
1.137 + (Scala "((_),/ (_))")
1.138 +
1.139 +code_const Pair
1.140 + (SML "!((_),/ (_))")
1.141 + (OCaml "!((_),/ (_))")
1.142 + (Haskell "!((_),/ (_))")
1.143 + (Scala "!((_),/ (_))")
1.144 +
1.145 +code_instance * :: eq
1.146 + (Haskell -)
1.147 +
1.148 +code_const "eq_class.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
1.149 + (Haskell infixl 4 "==")
1.150 +
1.151 +types_code
1.152 + "*" ("(_ */ _)")
1.153 +attach (term_of) {*
1.154 +fun term_of_id_42 aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y;
1.155 +*}
1.156 +attach (test) {*
1.157 +fun gen_id_42 aG aT bG bT i =
1.158 + let
1.159 + val (x, t) = aG i;
1.160 + val (y, u) = bG i
1.161 + in ((x, y), fn () => HOLogic.pair_const aT bT $ t () $ u ()) end;
1.162 +*}
1.163 +
1.164 +consts_code
1.165 + "Pair" ("(_,/ _)")
1.166 +
1.167 +setup {*
1.168 +let
1.169 +
1.170 +fun strip_abs_split 0 t = ([], t)
1.171 + | strip_abs_split i (Abs (s, T, t)) =
1.172 + let
1.173 + val s' = Codegen.new_name t s;
1.174 + val v = Free (s', T)
1.175 + in apfst (cons v) (strip_abs_split (i-1) (subst_bound (v, t))) end
1.176 + | strip_abs_split i (u as Const (@{const_name split}, _) $ t) =
1.177 + (case strip_abs_split (i+1) t of
1.178 + (v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u)
1.179 + | _ => ([], u))
1.180 + | strip_abs_split i t =
1.181 + strip_abs_split i (Abs ("x", hd (binder_types (fastype_of t)), t $ Bound 0));
1.182 +
1.183 +fun let_codegen thy defs dep thyname brack t gr =
1.184 + (case strip_comb t of
1.185 + (t1 as Const (@{const_name Let}, _), t2 :: t3 :: ts) =>
1.186 + let
1.187 + fun dest_let (l as Const (@{const_name Let}, _) $ t $ u) =
1.188 + (case strip_abs_split 1 u of
1.189 + ([p], u') => apfst (cons (p, t)) (dest_let u')
1.190 + | _ => ([], l))
1.191 + | dest_let t = ([], t);
1.192 + fun mk_code (l, r) gr =
1.193 + let
1.194 + val (pl, gr1) = Codegen.invoke_codegen thy defs dep thyname false l gr;
1.195 + val (pr, gr2) = Codegen.invoke_codegen thy defs dep thyname false r gr1;
1.196 + in ((pl, pr), gr2) end
1.197 + in case dest_let (t1 $ t2 $ t3) of
1.198 + ([], _) => NONE
1.199 + | (ps, u) =>
1.200 + let
1.201 + val (qs, gr1) = fold_map mk_code ps gr;
1.202 + val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1;
1.203 + val (pargs, gr3) = fold_map
1.204 + (Codegen.invoke_codegen thy defs dep thyname true) ts gr2
1.205 + in
1.206 + SOME (Codegen.mk_app brack
1.207 + (Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, flat
1.208 + (separate [Codegen.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
1.209 + [Pretty.block [Codegen.str "val ", pl, Codegen.str " =",
1.210 + Pretty.brk 1, pr]]) qs))),
1.211 + Pretty.brk 1, Codegen.str "in ", pu,
1.212 + Pretty.brk 1, Codegen.str "end"])) pargs, gr3)
1.213 + end
1.214 + end
1.215 + | _ => NONE);
1.216 +
1.217 +fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of
1.218 + (t1 as Const (@{const_name split}, _), t2 :: ts) =>
1.219 + let
1.220 + val ([p], u) = strip_abs_split 1 (t1 $ t2);
1.221 + val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr;
1.222 + val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1;
1.223 + val (pargs, gr3) = fold_map
1.224 + (Codegen.invoke_codegen thy defs dep thyname true) ts gr2
1.225 + in
1.226 + SOME (Codegen.mk_app brack
1.227 + (Pretty.block [Codegen.str "(fn ", q, Codegen.str " =>",
1.228 + Pretty.brk 1, pu, Codegen.str ")"]) pargs, gr2)
1.229 + end
1.230 + | _ => NONE);
1.231 +
1.232 +in
1.233 +
1.234 + Codegen.add_codegen "let_codegen" let_codegen
1.235 + #> Codegen.add_codegen "split_codegen" split_codegen
1.236 +
1.237 +end
1.238 +*}
1.239 +
1.240 +
1.241 +subsubsection {* Fundamental operations and properties *}
1.242
1.243 lemma surj_pair [simp]: "EX x y. p = (x, y)"
1.244 - apply (unfold Pair_def)
1.245 - apply (rule Rep_Prod [unfolded Prod_def, THEN CollectE])
1.246 - apply (erule exE, erule exE, rule exI, rule exI)
1.247 - apply (rule Rep_Prod_inverse [symmetric, THEN trans])
1.248 - apply (erule arg_cong)
1.249 - done
1.250 + by (cases p) simp
1.251
1.252 -lemma PairE [cases type: *]:
1.253 - obtains x y where "p = (x, y)"
1.254 - using surj_pair [of p] by blast
1.255 +global consts
1.256 + fst :: "'a \<times> 'b \<Rightarrow> 'a"
1.257 + snd :: "'a \<times> 'b \<Rightarrow> 'b"
1.258
1.259 -lemma ProdI: "Pair_Rep a b \<in> Prod"
1.260 - unfolding Prod_def by rule+
1.261 -
1.262 -lemma Pair_Rep_inject: "Pair_Rep a b = Pair_Rep a' b' \<Longrightarrow> a = a' \<and> b = b'"
1.263 - unfolding Pair_Rep_def by (drule fun_cong, drule fun_cong) blast
1.264 -
1.265 -lemma inj_on_Abs_Prod: "inj_on Abs_Prod Prod"
1.266 - apply (rule inj_on_inverseI)
1.267 - apply (erule Abs_Prod_inverse)
1.268 - done
1.269 -
1.270 -lemma Pair_inject:
1.271 - assumes "(a, b) = (a', b')"
1.272 - and "a = a' ==> b = b' ==> R"
1.273 - shows R
1.274 - apply (insert prems [unfolded Pair_def])
1.275 - apply (rule inj_on_Abs_Prod [THEN inj_onD, THEN Pair_Rep_inject, THEN conjE])
1.276 - apply (assumption | rule ProdI)+
1.277 - done
1.278 -
1.279 -rep_datatype (prod) Pair
1.280 -proof -
1.281 - fix P p
1.282 - assume "\<And>x y. P (x, y)"
1.283 - then show "P p" by (cases p) simp
1.284 -qed (auto elim: Pair_inject)
1.285 -
1.286 -lemmas Pair_eq = prod.inject
1.287 +local defs
1.288 + fst_def: "fst p == case p of (a, b) \<Rightarrow> a"
1.289 + snd_def: "snd p == case p of (a, b) \<Rightarrow> b"
1.290
1.291 lemma fst_conv [simp, code]: "fst (a, b) = a"
1.292 - unfolding fst_def by blast
1.293 + unfolding fst_def by simp
1.294
1.295 lemma snd_conv [simp, code]: "snd (a, b) = b"
1.296 - unfolding snd_def by blast
1.297 + unfolding snd_def by simp
1.298
1.299 +code_const fst and snd
1.300 + (Haskell "fst" and "snd")
1.301
1.302 -subsubsection {* Basic rules and proof tools *}
1.303 +lemma prod_case_unfold: "prod_case = (%c p. c (fst p) (snd p))"
1.304 + by (simp add: expand_fun_eq split: prod.split)
1.305
1.306 lemma fst_eqD: "fst (x, y) = a ==> x = a"
1.307 by simp
1.308 @@ -321,6 +424,44 @@
1.309
1.310 lemmas surjective_pairing = pair_collapse [symmetric]
1.311
1.312 +lemma Pair_fst_snd_eq: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t"
1.313 + by (cases s, cases t) simp
1.314 +
1.315 +lemma prod_eqI [intro?]: "fst p = fst q \<Longrightarrow> snd p = snd q \<Longrightarrow> p = q"
1.316 + by (simp add: Pair_fst_snd_eq)
1.317 +
1.318 +lemma split_conv [simp, code]: "split f (a, b) = f a b"
1.319 + by (simp add: split_prod_case)
1.320 +
1.321 +lemma splitI: "f a b \<Longrightarrow> split f (a, b)"
1.322 + by (rule split_conv [THEN iffD2])
1.323 +
1.324 +lemma splitD: "split f (a, b) \<Longrightarrow> f a b"
1.325 + by (rule split_conv [THEN iffD1])
1.326 +
1.327 +lemma split_Pair [simp]: "(\<lambda>(x, y). (x, y)) = id"
1.328 + by (simp add: split_prod_case expand_fun_eq split: prod.split)
1.329 +
1.330 +lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
1.331 + -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *}
1.332 + by (simp add: split_prod_case expand_fun_eq split: prod.split)
1.333 +
1.334 +lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
1.335 + by (cases x) simp
1.336 +
1.337 +lemma split_twice: "split f (split g p) = split (\<lambda>x y. split f (g x y)) p"
1.338 + by (cases p) simp
1.339 +
1.340 +lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))"
1.341 + by (simp add: split_prod_case prod_case_unfold)
1.342 +
1.343 +lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
1.344 + -- {* Prevents simplification of @{term c}: much faster *}
1.345 + by (erule arg_cong)
1.346 +
1.347 +lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
1.348 + by (simp add: split_eta)
1.349 +
1.350 lemma split_paired_all: "(!!x. PROP P x) == (!!a b. PROP P (a, b))"
1.351 proof
1.352 fix a b
1.353 @@ -374,71 +515,10 @@
1.354 lemma split_paired_Ex [simp]: "(EX x. P x) = (EX a b. P (a, b))"
1.355 by fast
1.356
1.357 -lemma Pair_fst_snd_eq: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t"
1.358 - by (cases s, cases t) simp
1.359 -
1.360 -lemma prod_eqI [intro?]: "fst p = fst q \<Longrightarrow> snd p = snd q \<Longrightarrow> p = q"
1.361 - by (simp add: Pair_fst_snd_eq)
1.362 -
1.363 -
1.364 -subsubsection {* @{text split} and @{text curry} *}
1.365 -
1.366 -lemma split_conv [simp, code]: "split f (a, b) = f a b"
1.367 - by (simp add: split_def)
1.368 -
1.369 -lemma curry_conv [simp, code]: "curry f a b = f (a, b)"
1.370 - by (simp add: curry_def)
1.371 -
1.372 -lemmas split = split_conv -- {* for backwards compatibility *}
1.373 -
1.374 -lemma splitI: "f a b \<Longrightarrow> split f (a, b)"
1.375 - by (rule split_conv [THEN iffD2])
1.376 -
1.377 -lemma splitD: "split f (a, b) \<Longrightarrow> f a b"
1.378 - by (rule split_conv [THEN iffD1])
1.379 -
1.380 -lemma curryI [intro!]: "f (a, b) \<Longrightarrow> curry f a b"
1.381 - by (simp add: curry_def)
1.382 -
1.383 -lemma curryD [dest!]: "curry f a b \<Longrightarrow> f (a, b)"
1.384 - by (simp add: curry_def)
1.385 -
1.386 -lemma curryE: "curry f a b \<Longrightarrow> (f (a, b) \<Longrightarrow> Q) \<Longrightarrow> Q"
1.387 - by (simp add: curry_def)
1.388 -
1.389 -lemma curry_split [simp]: "curry (split f) = f"
1.390 - by (simp add: curry_def split_def)
1.391 -
1.392 -lemma split_curry [simp]: "split (curry f) = f"
1.393 - by (simp add: curry_def split_def)
1.394 -
1.395 -lemma split_Pair [simp]: "(\<lambda>(x, y). (x, y)) = id"
1.396 - by (simp add: split_def id_def)
1.397 -
1.398 -lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
1.399 - -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *}
1.400 - by (rule ext) auto
1.401 -
1.402 -lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
1.403 - by (cases x) simp
1.404 -
1.405 -lemma split_twice: "split f (split g p) = split (\<lambda>x y. split f (g x y)) p"
1.406 - unfolding split_def ..
1.407 -
1.408 lemma split_paired_The: "(THE x. P x) = (THE (a, b). P (a, b))"
1.409 -- {* Can't be added to simpset: loops! *}
1.410 by (simp add: split_eta)
1.411
1.412 -lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))"
1.413 - by (simp add: split_def)
1.414 -
1.415 -lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
1.416 - -- {* Prevents simplification of @{term c}: much faster *}
1.417 - by (erule arg_cong)
1.418 -
1.419 -lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
1.420 - by (simp add: split_eta)
1.421 -
1.422 text {*
1.423 Simplification procedure for @{thm [source] cond_split_eta}. Using
1.424 @{thm [source] split_eta} as a rewrite rule is not general enough,
1.425 @@ -511,7 +591,6 @@
1.426 lemma split_split_asm [no_atp]: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
1.427 by (subst split_split, simp)
1.428
1.429 -
1.430 text {*
1.431 \medskip @{term split} used as a logical connective or set former.
1.432
1.433 @@ -529,10 +608,10 @@
1.434 done
1.435
1.436 lemma splitE: "split c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
1.437 - by (induct p) (auto simp add: split_def)
1.438 + by (induct p) (auto simp add: split_prod_case)
1.439
1.440 lemma splitE': "split c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
1.441 - by (induct p) (auto simp add: split_def)
1.442 + by (induct p) (auto simp add: split_prod_case)
1.443
1.444 lemma splitE2:
1.445 "[| Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
1.446 @@ -555,10 +634,10 @@
1.447 by (simp only: split_tupled_all, simp)
1.448
1.449 lemma mem_splitE:
1.450 - assumes major: "z: split c p"
1.451 - and cases: "!!x y. [| p = (x,y); z: c x y |] ==> Q"
1.452 + assumes major: "z \<in> split c p"
1.453 + and cases: "\<And>x y. p = (x, y) \<Longrightarrow> z \<in> c x y \<Longrightarrow> Q"
1.454 shows Q
1.455 - by (rule major [unfolded split_def] cases surjective_pairing)+
1.456 + by (rule major [unfolded split_prod_case prod_case_unfold] cases surjective_pairing)+
1.457
1.458 declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!]
1.459 declare mem_splitE [elim!] splitE' [elim!] splitE [elim!]
1.460 @@ -626,20 +705,6 @@
1.461 Setup of internal @{text split_rule}.
1.462 *}
1.463
1.464 -definition
1.465 - internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"
1.466 -where
1.467 - "internal_split == split"
1.468 -
1.469 -lemma internal_split_conv: "internal_split c (a, b) = c a b"
1.470 - by (simp only: internal_split_def split_conv)
1.471 -
1.472 -use "Tools/split_rule.ML"
1.473 -setup Split_Rule.setup
1.474 -
1.475 -hide_const internal_split
1.476 -
1.477 -
1.478 lemmas prod_caseI = prod.cases [THEN iffD2, standard]
1.479
1.480 lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
1.481 @@ -654,9 +719,6 @@
1.482 lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
1.483 by (induct p) auto
1.484
1.485 -lemma prod_case_unfold: "prod_case = (%c p. c (fst p) (snd p))"
1.486 - by (simp add: expand_fun_eq)
1.487 -
1.488 declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!]
1.489 declare prod_caseE' [elim!] prod_caseE [elim!]
1.490
1.491 @@ -668,9 +730,6 @@
1.492 "prod_case f p = f (fst p) (snd p)"
1.493 unfolding prod_case_split split_beta ..
1.494
1.495 -
1.496 -subsection {* Further cases/induct rules for tuples *}
1.497 -
1.498 lemma prod_cases3 [cases type]:
1.499 obtains (fields) a b c where "y = (a, b, c)"
1.500 by (cases y, case_tac b) blast
1.501 @@ -711,18 +770,55 @@
1.502 "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
1.503 by (cases x) blast
1.504
1.505 +lemma split_def:
1.506 + "split = (\<lambda>c p. c (fst p) (snd p))"
1.507 + unfolding split_prod_case prod_case_unfold ..
1.508 +
1.509 +definition internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
1.510 + "internal_split == split"
1.511 +
1.512 +lemma internal_split_conv: "internal_split c (a, b) = c a b"
1.513 + by (simp only: internal_split_def split_conv)
1.514 +
1.515 +use "Tools/split_rule.ML"
1.516 +setup Split_Rule.setup
1.517 +
1.518 +hide_const internal_split
1.519 +
1.520
1.521 subsubsection {* Derived operations *}
1.522
1.523 +global consts
1.524 + curry :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c"
1.525 +
1.526 +local defs
1.527 + curry_def: "curry == (%c x y. c (Pair x y))"
1.528 +
1.529 +lemma curry_conv [simp, code]: "curry f a b = f (a, b)"
1.530 + by (simp add: curry_def)
1.531 +
1.532 +lemma curryI [intro!]: "f (a, b) \<Longrightarrow> curry f a b"
1.533 + by (simp add: curry_def)
1.534 +
1.535 +lemma curryD [dest!]: "curry f a b \<Longrightarrow> f (a, b)"
1.536 + by (simp add: curry_def)
1.537 +
1.538 +lemma curryE: "curry f a b \<Longrightarrow> (f (a, b) \<Longrightarrow> Q) \<Longrightarrow> Q"
1.539 + by (simp add: curry_def)
1.540 +
1.541 +lemma curry_split [simp]: "curry (split f) = f"
1.542 + by (simp add: curry_def split_def)
1.543 +
1.544 +lemma split_curry [simp]: "split (curry f) = f"
1.545 + by (simp add: curry_def split_def)
1.546 +
1.547 text {*
1.548 The composition-uncurry combinator.
1.549 *}
1.550
1.551 notation fcomp (infixl "o>" 60)
1.552
1.553 -definition
1.554 - scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "o\<rightarrow>" 60)
1.555 -where
1.556 +definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "o\<rightarrow>" 60) where
1.557 "f o\<rightarrow> g = (\<lambda>x. split g (f x))"
1.558
1.559 lemma scomp_apply: "(f o\<rightarrow> g) x = split g (f x)"
1.560 @@ -749,7 +845,6 @@
1.561 no_notation fcomp (infixl "o>" 60)
1.562 no_notation scomp (infixl "o\<rightarrow>" 60)
1.563
1.564 -
1.565 text {*
1.566 @{term prod_fun} --- action of the product functor upon
1.567 functions.
1.568 @@ -777,21 +872,17 @@
1.569 and cases: "!!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P"
1.570 shows P
1.571 apply (rule major [THEN imageE])
1.572 - apply (rule_tac p = x in PairE)
1.573 + apply (case_tac x)
1.574 apply (rule cases)
1.575 apply (blast intro: prod_fun)
1.576 apply blast
1.577 done
1.578
1.579 -definition
1.580 - apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
1.581 -where
1.582 - [code del]: "apfst f = prod_fun f id"
1.583 +definition apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b" where
1.584 + "apfst f = prod_fun f id"
1.585
1.586 -definition
1.587 - apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c"
1.588 -where
1.589 - [code del]: "apsnd f = prod_fun id f"
1.590 +definition apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c" where
1.591 + "apsnd f = prod_fun id f"
1.592
1.593 lemma apfst_conv [simp, code]:
1.594 "apfst f (x, y) = (f x, y)"
1.595 @@ -1005,7 +1096,7 @@
1.596 by blast
1.597
1.598 lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
1.599 - by (auto, rule_tac p = "f x" in PairE, auto)
1.600 + by (auto, case_tac "f x", auto)
1.601
1.602 lemma swap_inj_on:
1.603 "inj_on (\<lambda>(i, j). (j, i)) A"
1.604 @@ -1023,131 +1114,27 @@
1.605 using * eq[symmetric] by auto
1.606 qed simp_all
1.607
1.608 -subsubsection {* Code generator setup *}
1.609
1.610 -lemma [code]:
1.611 - "eq_class.eq (x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by (simp add: eq)
1.612 -
1.613 -lemma split_case_cert:
1.614 - assumes "CASE \<equiv> split f"
1.615 - shows "CASE (a, b) \<equiv> f a b"
1.616 - using assms by simp
1.617 -
1.618 -setup {*
1.619 - Code.add_case @{thm split_case_cert}
1.620 -*}
1.621 -
1.622 -code_type *
1.623 - (SML infix 2 "*")
1.624 - (OCaml infix 2 "*")
1.625 - (Haskell "!((_),/ (_))")
1.626 - (Scala "((_),/ (_))")
1.627 -
1.628 -code_instance * :: eq
1.629 - (Haskell -)
1.630 -
1.631 -code_const "eq_class.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
1.632 - (Haskell infixl 4 "==")
1.633 -
1.634 -code_const Pair
1.635 - (SML "!((_),/ (_))")
1.636 - (OCaml "!((_),/ (_))")
1.637 - (Haskell "!((_),/ (_))")
1.638 - (Scala "!((_),/ (_))")
1.639 -
1.640 -code_const fst and snd
1.641 - (Haskell "fst" and "snd")
1.642 -
1.643 -types_code
1.644 - "*" ("(_ */ _)")
1.645 -attach (term_of) {*
1.646 -fun term_of_id_42 aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y;
1.647 -*}
1.648 -attach (test) {*
1.649 -fun gen_id_42 aG aT bG bT i =
1.650 - let
1.651 - val (x, t) = aG i;
1.652 - val (y, u) = bG i
1.653 - in ((x, y), fn () => HOLogic.pair_const aT bT $ t () $ u ()) end;
1.654 -*}
1.655 -
1.656 -consts_code
1.657 - "Pair" ("(_,/ _)")
1.658 -
1.659 -setup {*
1.660 -let
1.661 -
1.662 -fun strip_abs_split 0 t = ([], t)
1.663 - | strip_abs_split i (Abs (s, T, t)) =
1.664 - let
1.665 - val s' = Codegen.new_name t s;
1.666 - val v = Free (s', T)
1.667 - in apfst (cons v) (strip_abs_split (i-1) (subst_bound (v, t))) end
1.668 - | strip_abs_split i (u as Const (@{const_name split}, _) $ t) =
1.669 - (case strip_abs_split (i+1) t of
1.670 - (v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u)
1.671 - | _ => ([], u))
1.672 - | strip_abs_split i t =
1.673 - strip_abs_split i (Abs ("x", hd (binder_types (fastype_of t)), t $ Bound 0));
1.674 -
1.675 -fun let_codegen thy defs dep thyname brack t gr =
1.676 - (case strip_comb t of
1.677 - (t1 as Const (@{const_name Let}, _), t2 :: t3 :: ts) =>
1.678 - let
1.679 - fun dest_let (l as Const (@{const_name Let}, _) $ t $ u) =
1.680 - (case strip_abs_split 1 u of
1.681 - ([p], u') => apfst (cons (p, t)) (dest_let u')
1.682 - | _ => ([], l))
1.683 - | dest_let t = ([], t);
1.684 - fun mk_code (l, r) gr =
1.685 - let
1.686 - val (pl, gr1) = Codegen.invoke_codegen thy defs dep thyname false l gr;
1.687 - val (pr, gr2) = Codegen.invoke_codegen thy defs dep thyname false r gr1;
1.688 - in ((pl, pr), gr2) end
1.689 - in case dest_let (t1 $ t2 $ t3) of
1.690 - ([], _) => NONE
1.691 - | (ps, u) =>
1.692 - let
1.693 - val (qs, gr1) = fold_map mk_code ps gr;
1.694 - val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1;
1.695 - val (pargs, gr3) = fold_map
1.696 - (Codegen.invoke_codegen thy defs dep thyname true) ts gr2
1.697 - in
1.698 - SOME (Codegen.mk_app brack
1.699 - (Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, flat
1.700 - (separate [Codegen.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
1.701 - [Pretty.block [Codegen.str "val ", pl, Codegen.str " =",
1.702 - Pretty.brk 1, pr]]) qs))),
1.703 - Pretty.brk 1, Codegen.str "in ", pu,
1.704 - Pretty.brk 1, Codegen.str "end"])) pargs, gr3)
1.705 - end
1.706 - end
1.707 - | _ => NONE);
1.708 -
1.709 -fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of
1.710 - (t1 as Const (@{const_name split}, _), t2 :: ts) =>
1.711 - let
1.712 - val ([p], u) = strip_abs_split 1 (t1 $ t2);
1.713 - val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr;
1.714 - val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1;
1.715 - val (pargs, gr3) = fold_map
1.716 - (Codegen.invoke_codegen thy defs dep thyname true) ts gr2
1.717 - in
1.718 - SOME (Codegen.mk_app brack
1.719 - (Pretty.block [Codegen.str "(fn ", q, Codegen.str " =>",
1.720 - Pretty.brk 1, pu, Codegen.str ")"]) pargs, gr2)
1.721 - end
1.722 - | _ => NONE);
1.723 -
1.724 -in
1.725 -
1.726 - Codegen.add_codegen "let_codegen" let_codegen
1.727 - #> Codegen.add_codegen "split_codegen" split_codegen
1.728 -
1.729 -end
1.730 -*}
1.731 +subsection {* Inductively defined sets *}
1.732
1.733 use "Tools/inductive_set.ML"
1.734 setup Inductive_Set.setup
1.735
1.736 +
1.737 +subsection {* Legacy theorem bindings and duplicates *}
1.738 +
1.739 +lemma PairE:
1.740 + obtains x y where "p = (x, y)"
1.741 + by (fact prod.exhaust)
1.742 +
1.743 +lemma Pair_inject:
1.744 + assumes "(a, b) = (a', b')"
1.745 + and "a = a' ==> b = b' ==> R"
1.746 + shows R
1.747 + using assms by simp
1.748 +
1.749 +lemmas Pair_eq = prod.inject
1.750 +
1.751 +lemmas split = split_conv -- {* for backwards compatibility *}
1.752 +
1.753 end
2.1 --- a/src/HOL/Tools/split_rule.ML Fri May 28 11:23:34 2010 +0200
2.2 +++ b/src/HOL/Tools/split_rule.ML Fri May 28 13:37:47 2010 +0200
2.3 @@ -108,7 +108,7 @@
2.4
2.5
2.6 fun pair_tac ctxt s =
2.7 - res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
2.8 + res_inst_tac ctxt [(("y", 0), s)] @{thm prod.exhaust}
2.9 THEN' hyp_subst_tac
2.10 THEN' K prune_params_tac;
2.11