src/HOL/Product_Type.thy
changeset 26358 d6a508c16908
parent 26340 a85fe32e7b2f
child 26480 544cef16045b
     1.1 --- a/src/HOL/Product_Type.thy	Thu Mar 20 12:04:53 2008 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Mar 20 12:04:54 2008 +0100
     1.3 @@ -36,6 +36,7 @@
     1.4  code_instance bool :: eq
     1.5    (Haskell -)
     1.6  
     1.7 +
     1.8  subsection {* Unit *}
     1.9  
    1.10  typedef unit = "{True}"
    1.11 @@ -88,22 +89,53 @@
    1.12    by (rule ext) simp
    1.13  
    1.14  
    1.15 +text {* code generator setup *}
    1.16 +
    1.17 +instance unit :: eq ..
    1.18 +
    1.19 +lemma [code func]:
    1.20 +  "(u\<Colon>unit) = v \<longleftrightarrow> True" unfolding unit_eq [of u] unit_eq [of v] by rule+
    1.21 +
    1.22 +code_type unit
    1.23 +  (SML "unit")
    1.24 +  (OCaml "unit")
    1.25 +  (Haskell "()")
    1.26 +
    1.27 +code_instance unit :: eq
    1.28 +  (Haskell -)
    1.29 +
    1.30 +code_const "op = \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
    1.31 +  (Haskell infixl 4 "==")
    1.32 +
    1.33 +code_const Unity
    1.34 +  (SML "()")
    1.35 +  (OCaml "()")
    1.36 +  (Haskell "()")
    1.37 +
    1.38 +code_reserved SML
    1.39 +  unit
    1.40 +
    1.41 +code_reserved OCaml
    1.42 +  unit
    1.43 +
    1.44 +
    1.45  subsection {* Pairs *}
    1.46  
    1.47 -subsubsection {* Type definition *}
    1.48 +subsubsection {* Product type, basic operations and concrete syntax *}
    1.49  
    1.50 -constdefs
    1.51 -  Pair_Rep :: "['a, 'b] => ['a, 'b] => bool"
    1.52 -  "Pair_Rep == (%a b. %x y. x=a & y=b)"
    1.53 +definition
    1.54 +  Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
    1.55 +where
    1.56 +  "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
    1.57  
    1.58  global
    1.59  
    1.60  typedef (Prod)
    1.61    ('a, 'b) "*"    (infixr "*" 20)
    1.62 -    = "{f. EX a b. f = Pair_Rep (a::'a) (b::'b)}"
    1.63 +    = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
    1.64  proof
    1.65 -  fix a b show "Pair_Rep a b : ?Prod"
    1.66 -    by blast
    1.67 +  fix a b show "Pair_Rep a b \<in> ?Prod"
    1.68 +    by rule+
    1.69  qed
    1.70  
    1.71  syntax (xsymbols)
    1.72 @@ -111,20 +143,12 @@
    1.73  syntax (HTML output)
    1.74    "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
    1.75  
    1.76 -local
    1.77 -
    1.78 -subsubsection {* Definitions *}
    1.79 -
    1.80 -global
    1.81 -
    1.82  consts
    1.83 -  fst      :: "'a * 'b => 'a"
    1.84 -  snd      :: "'a * 'b => 'b"
    1.85 -  split    :: "[['a, 'b] => 'c, 'a * 'b] => 'c"
    1.86 -  curry    :: "['a * 'b => 'c, 'a, 'b] => 'c"
    1.87 -  prod_fun :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd"
    1.88 -  Pair     :: "['a, 'b] => 'a * 'b"
    1.89 -  Sigma    :: "['a set, 'a => 'b set] => ('a * 'b) set"
    1.90 +  Pair     :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b"
    1.91 +  fst      :: "'a \<times> 'b \<Rightarrow> 'a"
    1.92 +  snd      :: "'a \<times> 'b \<Rightarrow> 'b"
    1.93 +  split    :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"
    1.94 +  curry    :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c"
    1.95  
    1.96  local
    1.97  
    1.98 @@ -134,22 +158,6 @@
    1.99    snd_def:      "snd p == THE b. EX a. p = Pair a b"
   1.100    split_def:    "split == (%c p. c (fst p) (snd p))"
   1.101    curry_def:    "curry == (%c x y. c (Pair x y))"
   1.102 -  prod_fun_def: "prod_fun f g == split (%x y. Pair (f x) (g y))"
   1.103 -  Sigma_def [code func]:    "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
   1.104 -
   1.105 -abbreviation
   1.106 -  Times :: "['a set, 'b set] => ('a * 'b) set"
   1.107 -    (infixr "<*>" 80) where
   1.108 -  "A <*> B == Sigma A (%_. B)"
   1.109 -
   1.110 -notation (xsymbols)
   1.111 -  Times  (infixr "\<times>" 80)
   1.112 -
   1.113 -notation (HTML output)
   1.114 -  Times  (infixr "\<times>" 80)
   1.115 -
   1.116 -
   1.117 -subsubsection {* Concrete syntax *}
   1.118  
   1.119  text {*
   1.120    Patterns -- extends pre-defined type @{typ pttrn} used in
   1.121 @@ -166,7 +174,6 @@
   1.122    "_pattern"    :: "[pttrn, patterns] => pttrn"         ("'(_,/ _')")
   1.123    ""            :: "pttrn => patterns"                  ("_")
   1.124    "_patterns"   :: "[pttrn, patterns] => patterns"      ("_,/ _")
   1.125 -  "@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
   1.126  
   1.127  translations
   1.128    "(x, y)"       == "Pair x y"
   1.129 @@ -176,7 +183,6 @@
   1.130    "_abs (Pair x y) t" => "%(x,y).t"
   1.131    (* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
   1.132       The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
   1.133 -  "SIGMA x:A. B" == "Sigma A (%x. B)"
   1.134  
   1.135  (* reconstructs pattern from (nested) splits, avoiding eta-contraction of body*)
   1.136  (* works best with enclosing "let", if "let" does not avoid eta-contraction   *)
   1.137 @@ -232,15 +238,29 @@
   1.138  *}
   1.139  
   1.140  
   1.141 -subsubsection {* Lemmas and proof tool setup *}
   1.142 +text {* Towards a datatype declaration *}
   1.143  
   1.144 -lemma ProdI: "Pair_Rep a b : Prod"
   1.145 -  unfolding Prod_def by blast
   1.146 +lemma surj_pair [simp]: "EX x y. p = (x, y)"
   1.147 +  apply (unfold Pair_def)
   1.148 +  apply (rule Rep_Prod [unfolded Prod_def, THEN CollectE])
   1.149 +  apply (erule exE, erule exE, rule exI, rule exI)
   1.150 +  apply (rule Rep_Prod_inverse [symmetric, THEN trans])
   1.151 +  apply (erule arg_cong)
   1.152 +  done
   1.153  
   1.154 -lemma Pair_Rep_inject: "Pair_Rep a b = Pair_Rep a' b' ==> a = a' & b = b'"
   1.155 -  apply (unfold Pair_Rep_def)
   1.156 -  apply (drule fun_cong [THEN fun_cong], blast)
   1.157 -  done
   1.158 +lemma PairE [cases type: *]:
   1.159 +  obtains x y where "p = (x, y)"
   1.160 +  using surj_pair [of p] by blast
   1.161 +
   1.162 +
   1.163 +lemma prod_induct [induct type: *]: "(\<And>a b. P (a, b)) \<Longrightarrow> P x"
   1.164 +  by (cases x) simp
   1.165 +
   1.166 +lemma ProdI: "Pair_Rep a b \<in> Prod"
   1.167 +  unfolding Prod_def by rule+
   1.168 +
   1.169 +lemma Pair_Rep_inject: "Pair_Rep a b = Pair_Rep a' b' \<Longrightarrow> a = a' \<and> b = b'"
   1.170 +  unfolding Pair_Rep_def by (drule fun_cong, drule fun_cong) blast
   1.171  
   1.172  lemma inj_on_Abs_Prod: "inj_on Abs_Prod Prod"
   1.173    apply (rule inj_on_inverseI)
   1.174 @@ -265,42 +285,23 @@
   1.175  lemma snd_conv [simp, code]: "snd (a, b) = b"
   1.176    unfolding snd_def by blast
   1.177  
   1.178 +rep_datatype prod
   1.179 +  inject Pair_eq
   1.180 +  induction prod_induct
   1.181 +
   1.182 +
   1.183 +subsubsection {* Basic rules and proof tools *}
   1.184 +
   1.185  lemma fst_eqD: "fst (x, y) = a ==> x = a"
   1.186    by simp
   1.187  
   1.188  lemma snd_eqD: "snd (x, y) = a ==> y = a"
   1.189    by simp
   1.190  
   1.191 -lemma PairE_lemma: "EX x y. p = (x, y)"
   1.192 -  apply (unfold Pair_def)
   1.193 -  apply (rule Rep_Prod [unfolded Prod_def, THEN CollectE])
   1.194 -  apply (erule exE, erule exE, rule exI, rule exI)
   1.195 -  apply (rule Rep_Prod_inverse [symmetric, THEN trans])
   1.196 -  apply (erule arg_cong)
   1.197 -  done
   1.198 -
   1.199 -lemma PairE [cases type: *]: "(!!x y. p = (x, y) ==> Q) ==> Q"
   1.200 -  using PairE_lemma [of p] by blast
   1.201 -
   1.202 -ML {*
   1.203 -  local val PairE = thm "PairE" in
   1.204 -    fun pair_tac s =
   1.205 -      EVERY' [res_inst_tac [("p", s)] PairE, hyp_subst_tac, K prune_params_tac];
   1.206 -  end;
   1.207 -*}
   1.208 -
   1.209 -lemma surjective_pairing: "p = (fst p, snd p)"
   1.210 -  -- {* Do not add as rewrite rule: invalidates some proofs in IMP *}
   1.211 +lemma pair_collapse [simp]: "(fst p, snd p) = p"
   1.212    by (cases p) simp
   1.213  
   1.214 -lemmas pair_collapse = surjective_pairing [symmetric]
   1.215 -declare pair_collapse [simp]
   1.216 -
   1.217 -lemma surj_pair [simp]: "EX x y. z = (x, y)"
   1.218 -  apply (rule exI)
   1.219 -  apply (rule exI)
   1.220 -  apply (rule surjective_pairing)
   1.221 -  done
   1.222 +lemmas surjective_pairing = pair_collapse [symmetric]
   1.223  
   1.224  lemma split_paired_all: "(!!x. PROP P x) == (!!a b. PROP P (a, b))"
   1.225  proof
   1.226 @@ -313,8 +314,6 @@
   1.227    from `PROP P (fst x, snd x)` show "PROP P x" by simp
   1.228  qed
   1.229  
   1.230 -lemmas split_tupled_all = split_paired_all unit_all_eq2
   1.231 -
   1.232  text {*
   1.233    The rule @{thm [source] split_paired_all} does not work with the
   1.234    Simplifier because it also affects premises in congrence rules,
   1.235 @@ -322,7 +321,9 @@
   1.236    ?P(a, b)"} which cannot be solved by reflexivity.
   1.237  *}
   1.238  
   1.239 -ML {*
   1.240 +lemmas split_tupled_all = split_paired_all unit_all_eq2
   1.241 +
   1.242 +ML_setup {*
   1.243    (* replace parameters of product type by individual component parameters *)
   1.244    val safe_full_simp_tac = generic_simp_tac true (true, false, false);
   1.245    local (* filtering with exists_paired_all is an essential optimization *)
   1.246 @@ -352,71 +353,71 @@
   1.247    -- {* @{text "[iff]"} is not a good idea because it makes @{text blast} loop *}
   1.248    by fast
   1.249  
   1.250 +lemma split_paired_Ex [simp]: "(EX x. P x) = (EX a b. P (a, b))"
   1.251 +  by fast
   1.252 +
   1.253 +lemma Pair_fst_snd_eq: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t"
   1.254 +  by (cases s, cases t) simp
   1.255 +
   1.256 +lemma prod_eqI [intro?]: "fst p = fst q \<Longrightarrow> snd p = snd q \<Longrightarrow> p = q"
   1.257 +  by (simp add: Pair_fst_snd_eq)
   1.258 +
   1.259 +
   1.260 +subsubsection {* @{text split} and @{text curry} *}
   1.261 +
   1.262 +lemma split_conv [simp, code func]: "split f (a, b) = f a b"
   1.263 +  by (simp add: split_def)
   1.264 +
   1.265 +lemma curry_conv [simp, code func]: "curry f a b = f (a, b)"
   1.266 +  by (simp add: curry_def)
   1.267 +
   1.268 +lemmas split = split_conv  -- {* for backwards compatibility *}
   1.269 +
   1.270 +lemma splitI: "f a b \<Longrightarrow> split f (a, b)"
   1.271 +  by (rule split_conv [THEN iffD2])
   1.272 +
   1.273 +lemma splitD: "split f (a, b) \<Longrightarrow> f a b"
   1.274 +  by (rule split_conv [THEN iffD1])
   1.275 +
   1.276 +lemma curryI [intro!]: "f (a, b) \<Longrightarrow> curry f a b"
   1.277 +  by (simp add: curry_def)
   1.278 +
   1.279 +lemma curryD [dest!]: "curry f a b \<Longrightarrow> f (a, b)"
   1.280 +  by (simp add: curry_def)
   1.281 +
   1.282 +lemma curryE: "curry f a b \<Longrightarrow> (f (a, b) \<Longrightarrow> Q) \<Longrightarrow> Q"
   1.283 +  by (simp add: curry_def)
   1.284 +
   1.285  lemma curry_split [simp]: "curry (split f) = f"
   1.286    by (simp add: curry_def split_def)
   1.287  
   1.288  lemma split_curry [simp]: "split (curry f) = f"
   1.289    by (simp add: curry_def split_def)
   1.290  
   1.291 -lemma curryI [intro!]: "f (a,b) ==> curry f a b"
   1.292 -  by (simp add: curry_def)
   1.293 -
   1.294 -lemma curryD [dest!]: "curry f a b ==> f (a,b)"
   1.295 -  by (simp add: curry_def)
   1.296 -
   1.297 -lemma curryE: "[| curry f a b ; f (a,b) ==> Q |] ==> Q"
   1.298 -  by (simp add: curry_def)
   1.299 -
   1.300 -lemma curry_conv [simp, code func]: "curry f a b = f (a,b)"
   1.301 -  by (simp add: curry_def)
   1.302 -
   1.303 -lemma prod_induct [induct type: *]: "!!x. (!!a b. P (a, b)) ==> P x"
   1.304 -  by fast
   1.305 +lemma split_Pair [simp]: "(\<lambda>(x, y). (x, y)) = id"
   1.306 +  by (simp add: split_def id_def)
   1.307  
   1.308 -rep_datatype prod
   1.309 -  inject Pair_eq
   1.310 -  induction prod_induct
   1.311 -
   1.312 -lemma split_paired_Ex [simp]: "(EX x. P x) = (EX a b. P (a, b))"
   1.313 -  by fast
   1.314 -
   1.315 -lemma split_conv [simp, code func]: "split c (a, b) = c a b"
   1.316 -  by (simp add: split_def)
   1.317 +lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
   1.318 +  -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *}
   1.319 +  by (rule ext) auto
   1.320  
   1.321 -lemmas split = split_conv  -- {* for backwards compatibility *}
   1.322 -
   1.323 -lemmas splitI = split_conv [THEN iffD2, standard]
   1.324 -lemmas splitD = split_conv [THEN iffD1, standard]
   1.325 +lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
   1.326 +  by (cases x) simp
   1.327  
   1.328 -lemma split_Pair_apply: "split (%x y. f (x, y)) = f"
   1.329 -  -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *}
   1.330 -  apply (rule ext)
   1.331 -  apply (tactic {* pair_tac "x" 1 *}, simp)
   1.332 -  done
   1.333 +lemma split_twice: "split f (split g p) = split (\<lambda>x y. split f (g x y)) p"
   1.334 +  unfolding split_def ..
   1.335  
   1.336  lemma split_paired_The: "(THE x. P x) = (THE (a, b). P (a, b))"
   1.337    -- {* Can't be added to simpset: loops! *}
   1.338 -  by (simp add: split_Pair_apply)
   1.339 +  by (simp add: split_eta)
   1.340  
   1.341  lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))"
   1.342    by (simp add: split_def)
   1.343  
   1.344 -lemma Pair_fst_snd_eq: "!!s t. (s = t) = (fst s = fst t & snd s = snd t)"
   1.345 -by (simp only: split_tupled_all, simp)
   1.346 -
   1.347 -lemma prod_eqI [intro?]: "fst p = fst q ==> snd p = snd q ==> p = q"
   1.348 -  by (simp add: Pair_fst_snd_eq)
   1.349 -
   1.350 -lemma split_weak_cong: "p = q ==> split c p = split c q"
   1.351 +lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
   1.352    -- {* Prevents simplification of @{term c}: much faster *}
   1.353    by (erule arg_cong)
   1.354  
   1.355 -lemma split_eta: "(%(x, y). f (x, y)) = f"
   1.356 -  apply (rule ext)
   1.357 -  apply (simp only: split_tupled_all)
   1.358 -  apply (rule split_conv)
   1.359 -  done
   1.360 -
   1.361  lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
   1.362    by (simp add: split_eta)
   1.363  
   1.364 @@ -425,7 +426,8 @@
   1.365    @{thm [source] split_eta} as a rewrite rule is not general enough,
   1.366    and using @{thm [source] cond_split_eta} directly would render some
   1.367    existing proofs very inefficient; similarly for @{text
   1.368 -  split_beta}. *}
   1.369 +  split_beta}.
   1.370 +*}
   1.371  
   1.372  ML_setup {*
   1.373  
   1.374 @@ -581,6 +583,11 @@
   1.375    shows "(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))"
   1.376    by (rule ext) auto
   1.377  
   1.378 +lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A"
   1.379 +  apply (rule_tac x = "(a, b)" in image_eqI)
   1.380 +   apply auto
   1.381 +  done
   1.382 +
   1.383  lemma The_split_eq [simp]: "(THE (x',y'). x = x' & y = y') = (x, y)"
   1.384    by blast
   1.385  
   1.386 @@ -597,192 +604,6 @@
   1.387  qed "The_split_eq";
   1.388  *)
   1.389  
   1.390 -lemma injective_fst_snd: "!!x y. [|fst x = fst y; snd x = snd y|] ==> x = y"
   1.391 -  by auto
   1.392 -
   1.393 -
   1.394 -text {*
   1.395 -  \bigskip @{term prod_fun} --- action of the product functor upon
   1.396 -  functions.
   1.397 -*}
   1.398 -
   1.399 -lemma prod_fun [simp, code func]: "prod_fun f g (a, b) = (f a, g b)"
   1.400 -  by (simp add: prod_fun_def)
   1.401 -
   1.402 -lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
   1.403 -  apply (rule ext)
   1.404 -  apply (tactic {* pair_tac "x" 1 *}, simp)
   1.405 -  done
   1.406 -
   1.407 -lemma prod_fun_ident [simp]: "prod_fun (%x. x) (%y. y) = (%z. z)"
   1.408 -  apply (rule ext)
   1.409 -  apply (tactic {* pair_tac "z" 1 *}, simp)
   1.410 -  done
   1.411 -
   1.412 -lemma prod_fun_imageI [intro]: "(a, b) : r ==> (f a, g b) : prod_fun f g ` r"
   1.413 -  apply (rule image_eqI)
   1.414 -  apply (rule prod_fun [symmetric], assumption)
   1.415 -  done
   1.416 -
   1.417 -lemma prod_fun_imageE [elim!]:
   1.418 -  assumes major: "c: (prod_fun f g)`r"
   1.419 -    and cases: "!!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P"
   1.420 -  shows P
   1.421 -  apply (rule major [THEN imageE])
   1.422 -  apply (rule_tac p = x in PairE)
   1.423 -  apply (rule cases)
   1.424 -   apply (blast intro: prod_fun)
   1.425 -  apply blast
   1.426 -  done
   1.427 -
   1.428 -
   1.429 -definition
   1.430 -  upd_fst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
   1.431 -where
   1.432 -  [code func del]: "upd_fst f = prod_fun f id"
   1.433 -
   1.434 -definition
   1.435 -  upd_snd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c"
   1.436 -where
   1.437 -  [code func del]: "upd_snd f = prod_fun id f"
   1.438 -
   1.439 -lemma upd_fst_conv [simp, code]:
   1.440 -  "upd_fst f (x, y) = (f x, y)" 
   1.441 -  by (simp add: upd_fst_def)
   1.442 -
   1.443 -lemma upd_snd_conv [simp, code]:
   1.444 -  "upd_snd f (x, y) = (x, f y)" 
   1.445 -  by (simp add: upd_snd_def)
   1.446 -
   1.447 -text {*
   1.448 -  \bigskip Disjoint union of a family of sets -- Sigma.
   1.449 -*}
   1.450 -
   1.451 -lemma SigmaI [intro!]: "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B"
   1.452 -  by (unfold Sigma_def) blast
   1.453 -
   1.454 -lemma SigmaE [elim!]:
   1.455 -    "[| c: Sigma A B;
   1.456 -        !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P
   1.457 -     |] ==> P"
   1.458 -  -- {* The general elimination rule. *}
   1.459 -  by (unfold Sigma_def) blast
   1.460 -
   1.461 -text {*
   1.462 -  Elimination of @{term "(a, b) : A \<times> B"} -- introduces no
   1.463 -  eigenvariables.
   1.464 -*}
   1.465 -
   1.466 -lemma SigmaD1: "(a, b) : Sigma A B ==> a : A"
   1.467 -  by blast
   1.468 -
   1.469 -lemma SigmaD2: "(a, b) : Sigma A B ==> b : B a"
   1.470 -  by blast
   1.471 -
   1.472 -lemma SigmaE2:
   1.473 -    "[| (a, b) : Sigma A B;
   1.474 -        [| a:A;  b:B(a) |] ==> P
   1.475 -     |] ==> P"
   1.476 -  by blast
   1.477 -
   1.478 -lemma Sigma_cong:
   1.479 -     "\<lbrakk>A = B; !!x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk>
   1.480 -      \<Longrightarrow> (SIGMA x: A. C x) = (SIGMA x: B. D x)"
   1.481 -  by auto
   1.482 -
   1.483 -lemma Sigma_mono: "[| A <= C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"
   1.484 -  by blast
   1.485 -
   1.486 -lemma Sigma_empty1 [simp]: "Sigma {} B = {}"
   1.487 -  by blast
   1.488 -
   1.489 -lemma Sigma_empty2 [simp]: "A <*> {} = {}"
   1.490 -  by blast
   1.491 -
   1.492 -lemma UNIV_Times_UNIV [simp]: "UNIV <*> UNIV = UNIV"
   1.493 -  by auto
   1.494 -
   1.495 -lemma Compl_Times_UNIV1 [simp]: "- (UNIV <*> A) = UNIV <*> (-A)"
   1.496 -  by auto
   1.497 -
   1.498 -lemma Compl_Times_UNIV2 [simp]: "- (A <*> UNIV) = (-A) <*> UNIV"
   1.499 -  by auto
   1.500 -
   1.501 -lemma mem_Sigma_iff [iff]: "((a,b): Sigma A B) = (a:A & b:B(a))"
   1.502 -  by blast
   1.503 -
   1.504 -lemma Times_subset_cancel2: "x:C ==> (A <*> C <= B <*> C) = (A <= B)"
   1.505 -  by blast
   1.506 -
   1.507 -lemma Times_eq_cancel2: "x:C ==> (A <*> C = B <*> C) = (A = B)"
   1.508 -  by (blast elim: equalityE)
   1.509 -
   1.510 -lemma SetCompr_Sigma_eq:
   1.511 -    "Collect (split (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))"
   1.512 -  by blast
   1.513 -
   1.514 -text {*
   1.515 -  \bigskip Complex rules for Sigma.
   1.516 -*}
   1.517 -
   1.518 -lemma Collect_split [simp]: "{(a,b). P a & Q b} = Collect P <*> Collect Q"
   1.519 -  by blast
   1.520 -
   1.521 -lemma UN_Times_distrib:
   1.522 -  "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)"
   1.523 -  -- {* Suggested by Pierre Chartier *}
   1.524 -  by blast
   1.525 -
   1.526 -lemma split_paired_Ball_Sigma [simp,noatp]:
   1.527 -    "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))"
   1.528 -  by blast
   1.529 -
   1.530 -lemma split_paired_Bex_Sigma [simp,noatp]:
   1.531 -    "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))"
   1.532 -  by blast
   1.533 -
   1.534 -lemma Sigma_Un_distrib1: "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))"
   1.535 -  by blast
   1.536 -
   1.537 -lemma Sigma_Un_distrib2: "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))"
   1.538 -  by blast
   1.539 -
   1.540 -lemma Sigma_Int_distrib1: "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))"
   1.541 -  by blast
   1.542 -
   1.543 -lemma Sigma_Int_distrib2: "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))"
   1.544 -  by blast
   1.545 -
   1.546 -lemma Sigma_Diff_distrib1: "(SIGMA i:I - J. C(i)) = (SIGMA i:I. C(i)) - (SIGMA j:J. C(j))"
   1.547 -  by blast
   1.548 -
   1.549 -lemma Sigma_Diff_distrib2: "(SIGMA i:I. A(i) - B(i)) = (SIGMA i:I. A(i)) - (SIGMA i:I. B(i))"
   1.550 -  by blast
   1.551 -
   1.552 -lemma Sigma_Union: "Sigma (Union X) B = (UN A:X. Sigma A B)"
   1.553 -  by blast
   1.554 -
   1.555 -text {*
   1.556 -  Non-dependent versions are needed to avoid the need for higher-order
   1.557 -  matching, especially when the rules are re-oriented.
   1.558 -*}
   1.559 -
   1.560 -lemma Times_Un_distrib1: "(A Un B) <*> C = (A <*> C) Un (B <*> C)"
   1.561 -  by blast
   1.562 -
   1.563 -lemma Times_Int_distrib1: "(A Int B) <*> C = (A <*> C) Int (B <*> C)"
   1.564 -  by blast
   1.565 -
   1.566 -lemma Times_Diff_distrib1: "(A - B) <*> C = (A <*> C) - (B <*> C)"
   1.567 -  by blast
   1.568 -
   1.569 -
   1.570 -lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A"
   1.571 -  apply (rule_tac x = "(a, b)" in image_eqI)
   1.572 -   apply auto
   1.573 -  done
   1.574 -
   1.575 -
   1.576  text {*
   1.577    Setup of internal @{text split_rule}.
   1.578  *}
   1.579 @@ -800,8 +621,6 @@
   1.580  use "Tools/split_rule.ML"
   1.581  setup SplitRule.setup
   1.582  
   1.583 -
   1.584 -
   1.585  lemmas prod_caseI = prod.cases [THEN iffD2, standard]
   1.586  
   1.587  lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
   1.588 @@ -874,45 +693,234 @@
   1.589    by (cases x) blast
   1.590  
   1.591  
   1.592 -subsection {* Further lemmas *}
   1.593 +subsubsection {* Derived operations *}
   1.594 +
   1.595 +text {*
   1.596 +  The composition-uncurry combinator.
   1.597 +*}
   1.598 +
   1.599 +definition
   1.600 +  mbind :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "o->" 60)
   1.601 +where
   1.602 +  "f o-> g = (\<lambda>x. split g (f x))"
   1.603 +
   1.604 +notation (xsymbols)
   1.605 +  mbind  (infixl "\<circ>\<rightarrow>" 60)
   1.606 +
   1.607 +notation (HTML output)
   1.608 +  mbind  (infixl "\<circ>\<rightarrow>" 60)
   1.609 +
   1.610 +lemma mbind_apply:  "(f \<circ>\<rightarrow> g) x = split g (f x)"
   1.611 +  by (simp add: mbind_def)
   1.612 +
   1.613 +lemma Pair_mbind: "Pair x \<circ>\<rightarrow> f = f x"
   1.614 +  by (simp add: expand_fun_eq mbind_apply)
   1.615 +
   1.616 +lemma mbind_Pair: "x \<circ>\<rightarrow> Pair = x"
   1.617 +  by (simp add: expand_fun_eq mbind_apply)
   1.618 +
   1.619 +lemma mbind_mbind: "(f \<circ>\<rightarrow> g) \<circ>\<rightarrow> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>\<rightarrow> h)"
   1.620 +  by (simp add: expand_fun_eq split_twice mbind_def)
   1.621 +
   1.622 +lemma mbind_fcomp: "(f \<circ>\<rightarrow> g) \<circ>> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>> h)"
   1.623 +  by (simp add: expand_fun_eq mbind_apply fcomp_def split_def)
   1.624 +
   1.625 +lemma fcomp_mbind: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> h)"
   1.626 +  by (simp add: expand_fun_eq mbind_apply fcomp_apply)
   1.627 +
   1.628 +
   1.629 +text {*
   1.630 +  @{term prod_fun} --- action of the product functor upon
   1.631 +  functions.
   1.632 +*}
   1.633  
   1.634 -lemma
   1.635 -  split_Pair: "split Pair x = x"
   1.636 -  unfolding split_def by auto
   1.637 +definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
   1.638 +  [code func del]: "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
   1.639 +
   1.640 +lemma prod_fun [simp, code func]: "prod_fun f g (a, b) = (f a, g b)"
   1.641 +  by (simp add: prod_fun_def)
   1.642 +
   1.643 +lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
   1.644 +  by (rule ext) auto
   1.645 +
   1.646 +lemma prod_fun_ident [simp]: "prod_fun (%x. x) (%y. y) = (%z. z)"
   1.647 +  by (rule ext) auto
   1.648 +
   1.649 +lemma prod_fun_imageI [intro]: "(a, b) : r ==> (f a, g b) : prod_fun f g ` r"
   1.650 +  apply (rule image_eqI)
   1.651 +  apply (rule prod_fun [symmetric], assumption)
   1.652 +  done
   1.653  
   1.654 -lemma
   1.655 -  split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
   1.656 -  by (cases x, simp)
   1.657 +lemma prod_fun_imageE [elim!]:
   1.658 +  assumes major: "c: (prod_fun f g)`r"
   1.659 +    and cases: "!!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P"
   1.660 +  shows P
   1.661 +  apply (rule major [THEN imageE])
   1.662 +  apply (rule_tac p = x in PairE)
   1.663 +  apply (rule cases)
   1.664 +   apply (blast intro: prod_fun)
   1.665 +  apply blast
   1.666 +  done
   1.667 +
   1.668 +definition
   1.669 +  apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
   1.670 +where
   1.671 +  [code func del]: "apfst f = prod_fun f id"
   1.672 +
   1.673 +definition
   1.674 +  apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c"
   1.675 +where
   1.676 +  [code func del]: "apsnd f = prod_fun id f"
   1.677 +
   1.678 +lemma apfst_conv [simp, code]:
   1.679 +  "apfst f (x, y) = (f x, y)" 
   1.680 +  by (simp add: apfst_def)
   1.681 +
   1.682 +lemma upd_snd_conv [simp, code]:
   1.683 +  "apsnd f (x, y) = (x, f y)" 
   1.684 +  by (simp add: apsnd_def)
   1.685  
   1.686  
   1.687 -subsection {* Code generator setup *}
   1.688 +text {*
   1.689 +  Disjoint union of a family of sets -- Sigma.
   1.690 +*}
   1.691 +
   1.692 +definition  Sigma :: "['a set, 'a => 'b set] => ('a \<times> 'b) set" where
   1.693 +  Sigma_def: "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
   1.694 +
   1.695 +abbreviation
   1.696 +  Times :: "['a set, 'b set] => ('a * 'b) set"
   1.697 +    (infixr "<*>" 80) where
   1.698 +  "A <*> B == Sigma A (%_. B)"
   1.699 +
   1.700 +notation (xsymbols)
   1.701 +  Times  (infixr "\<times>" 80)
   1.702  
   1.703 -instance unit :: eq ..
   1.704 +notation (HTML output)
   1.705 +  Times  (infixr "\<times>" 80)
   1.706 +
   1.707 +syntax
   1.708 +  "@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
   1.709 +
   1.710 +translations
   1.711 +  "SIGMA x:A. B" == "Product_Type.Sigma A (%x. B)"
   1.712 +
   1.713 +lemma SigmaI [intro!]: "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B"
   1.714 +  by (unfold Sigma_def) blast
   1.715 +
   1.716 +lemma SigmaE [elim!]:
   1.717 +    "[| c: Sigma A B;
   1.718 +        !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P
   1.719 +     |] ==> P"
   1.720 +  -- {* The general elimination rule. *}
   1.721 +  by (unfold Sigma_def) blast
   1.722  
   1.723 -lemma [code func]:
   1.724 -  "(u\<Colon>unit) = v \<longleftrightarrow> True" unfolding unit_eq [of u] unit_eq [of v] by rule+
   1.725 +text {*
   1.726 +  Elimination of @{term "(a, b) : A \<times> B"} -- introduces no
   1.727 +  eigenvariables.
   1.728 +*}
   1.729 +
   1.730 +lemma SigmaD1: "(a, b) : Sigma A B ==> a : A"
   1.731 +  by blast
   1.732 +
   1.733 +lemma SigmaD2: "(a, b) : Sigma A B ==> b : B a"
   1.734 +  by blast
   1.735 +
   1.736 +lemma SigmaE2:
   1.737 +    "[| (a, b) : Sigma A B;
   1.738 +        [| a:A;  b:B(a) |] ==> P
   1.739 +     |] ==> P"
   1.740 +  by blast
   1.741  
   1.742 -code_type unit
   1.743 -  (SML "unit")
   1.744 -  (OCaml "unit")
   1.745 -  (Haskell "()")
   1.746 +lemma Sigma_cong:
   1.747 +     "\<lbrakk>A = B; !!x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk>
   1.748 +      \<Longrightarrow> (SIGMA x: A. C x) = (SIGMA x: B. D x)"
   1.749 +  by auto
   1.750 +
   1.751 +lemma Sigma_mono: "[| A <= C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"
   1.752 +  by blast
   1.753 +
   1.754 +lemma Sigma_empty1 [simp]: "Sigma {} B = {}"
   1.755 +  by blast
   1.756 +
   1.757 +lemma Sigma_empty2 [simp]: "A <*> {} = {}"
   1.758 +  by blast
   1.759 +
   1.760 +lemma UNIV_Times_UNIV [simp]: "UNIV <*> UNIV = UNIV"
   1.761 +  by auto
   1.762  
   1.763 -code_instance unit :: eq
   1.764 -  (Haskell -)
   1.765 +lemma Compl_Times_UNIV1 [simp]: "- (UNIV <*> A) = UNIV <*> (-A)"
   1.766 +  by auto
   1.767 +
   1.768 +lemma Compl_Times_UNIV2 [simp]: "- (A <*> UNIV) = (-A) <*> UNIV"
   1.769 +  by auto
   1.770 +
   1.771 +lemma mem_Sigma_iff [iff]: "((a,b): Sigma A B) = (a:A & b:B(a))"
   1.772 +  by blast
   1.773 +
   1.774 +lemma Times_subset_cancel2: "x:C ==> (A <*> C <= B <*> C) = (A <= B)"
   1.775 +  by blast
   1.776 +
   1.777 +lemma Times_eq_cancel2: "x:C ==> (A <*> C = B <*> C) = (A = B)"
   1.778 +  by (blast elim: equalityE)
   1.779  
   1.780 -code_const "op = \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
   1.781 -  (Haskell infixl 4 "==")
   1.782 +lemma SetCompr_Sigma_eq:
   1.783 +    "Collect (split (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))"
   1.784 +  by blast
   1.785 +
   1.786 +lemma Collect_split [simp]: "{(a,b). P a & Q b} = Collect P <*> Collect Q"
   1.787 +  by blast
   1.788 +
   1.789 +lemma UN_Times_distrib:
   1.790 +  "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)"
   1.791 +  -- {* Suggested by Pierre Chartier *}
   1.792 +  by blast
   1.793 +
   1.794 +lemma split_paired_Ball_Sigma [simp,noatp]:
   1.795 +    "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))"
   1.796 +  by blast
   1.797 +
   1.798 +lemma split_paired_Bex_Sigma [simp,noatp]:
   1.799 +    "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))"
   1.800 +  by blast
   1.801  
   1.802 -code_const Unity
   1.803 -  (SML "()")
   1.804 -  (OCaml "()")
   1.805 -  (Haskell "()")
   1.806 +lemma Sigma_Un_distrib1: "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))"
   1.807 +  by blast
   1.808 +
   1.809 +lemma Sigma_Un_distrib2: "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))"
   1.810 +  by blast
   1.811 +
   1.812 +lemma Sigma_Int_distrib1: "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))"
   1.813 +  by blast
   1.814 +
   1.815 +lemma Sigma_Int_distrib2: "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))"
   1.816 +  by blast
   1.817 +
   1.818 +lemma Sigma_Diff_distrib1: "(SIGMA i:I - J. C(i)) = (SIGMA i:I. C(i)) - (SIGMA j:J. C(j))"
   1.819 +  by blast
   1.820 +
   1.821 +lemma Sigma_Diff_distrib2: "(SIGMA i:I. A(i) - B(i)) = (SIGMA i:I. A(i)) - (SIGMA i:I. B(i))"
   1.822 +  by blast
   1.823  
   1.824 -code_reserved SML
   1.825 -  unit
   1.826 +lemma Sigma_Union: "Sigma (Union X) B = (UN A:X. Sigma A B)"
   1.827 +  by blast
   1.828 +
   1.829 +text {*
   1.830 +  Non-dependent versions are needed to avoid the need for higher-order
   1.831 +  matching, especially when the rules are re-oriented.
   1.832 +*}
   1.833  
   1.834 -code_reserved OCaml
   1.835 -  unit
   1.836 +lemma Times_Un_distrib1: "(A Un B) <*> C = (A <*> C) Un (B <*> C)"
   1.837 +  by blast
   1.838 +
   1.839 +lemma Times_Int_distrib1: "(A Int B) <*> C = (A <*> C) Int (B <*> C)"
   1.840 +  by blast
   1.841 +
   1.842 +lemma Times_Diff_distrib1: "(A - B) <*> C = (A <*> C) - (B <*> C)"
   1.843 +  by blast
   1.844 +
   1.845 +
   1.846 +subsubsection {* Code generator setup *}
   1.847  
   1.848  instance * :: (eq, eq) eq ..
   1.849  
   1.850 @@ -1044,12 +1052,10 @@
   1.851  val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1";
   1.852  val Compl_Times_UNIV2 = thm "Compl_Times_UNIV2";
   1.853  val PairE = thm "PairE";
   1.854 -val PairE_lemma = thm "PairE_lemma";
   1.855  val Pair_Rep_inject = thm "Pair_Rep_inject";
   1.856  val Pair_def = thm "Pair_def";
   1.857  val Pair_eq = thm "Pair_eq";
   1.858  val Pair_fst_snd_eq = thm "Pair_fst_snd_eq";
   1.859 -val Pair_inject = thm "Pair_inject";
   1.860  val ProdI = thm "ProdI";
   1.861  val SetCompr_Sigma_eq = thm "SetCompr_Sigma_eq";
   1.862  val SigmaD1 = thm "SigmaD1";
   1.863 @@ -1084,7 +1090,6 @@
   1.864  val fst_def = thm "fst_def";
   1.865  val fst_eqD = thm "fst_eqD";
   1.866  val inj_on_Abs_Prod = thm "inj_on_Abs_Prod";
   1.867 -val injective_fst_snd = thm "injective_fst_snd";
   1.868  val mem_Sigma_iff = thm "mem_Sigma_iff";
   1.869  val mem_splitE = thm "mem_splitE";
   1.870  val mem_splitI = thm "mem_splitI";
   1.871 @@ -1109,7 +1114,6 @@
   1.872  val splitI = thm "splitI";
   1.873  val splitI2 = thm "splitI2";
   1.874  val splitI2' = thm "splitI2'";
   1.875 -val split_Pair_apply = thm "split_Pair_apply";
   1.876  val split_beta = thm "split_beta";
   1.877  val split_conv = thm "split_conv";
   1.878  val split_def = thm "split_def";
   1.879 @@ -1133,7 +1137,6 @@
   1.880  val unit_all_eq1 = thm "unit_all_eq1";
   1.881  val unit_all_eq2 = thm "unit_all_eq2";
   1.882  val unit_eq = thm "unit_eq";
   1.883 -val unit_induct = thm "unit_induct";
   1.884  *}
   1.885  
   1.886