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