src/HOL/Product_Type.thy
changeset 37591 d3daea901123
parent 37411 c88c44156083
child 37678 0040bafffdef
     1.1 --- a/src/HOL/Product_Type.thy	Mon Jun 28 15:03:07 2010 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Mon Jun 28 15:03:07 2010 +0200
     1.3 @@ -163,8 +163,8 @@
     1.4  
     1.5  subsubsection {* Tuple syntax *}
     1.6  
     1.7 -definition split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
     1.8 -  split_prod_case: "split == prod_case"
     1.9 +abbreviation (input) split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
    1.10 +  "split \<equiv> prod_case"
    1.11  
    1.12  text {*
    1.13    Patterns -- extends pre-defined type @{typ pttrn} used in
    1.14 @@ -185,8 +185,8 @@
    1.15  translations
    1.16    "(x, y)" == "CONST Pair x y"
    1.17    "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))"
    1.18 -  "%(x, y, zs). b" == "CONST split (%x (y, zs). b)"
    1.19 -  "%(x, y). b" == "CONST split (%x y. b)"
    1.20 +  "%(x, y, zs). b" == "CONST prod_case (%x (y, zs). b)"
    1.21 +  "%(x, y). b" == "CONST prod_case (%x y. b)"
    1.22    "_abs (CONST Pair x y) t" => "%(x, y). t"
    1.23    -- {* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
    1.24       The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *}
    1.25 @@ -204,7 +204,7 @@
    1.26            Syntax.const @{syntax_const "_abs"} $
    1.27              (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
    1.28          end
    1.29 -    | split_tr' [Abs (x, T, (s as Const (@{const_syntax split}, _) $ t))] =
    1.30 +    | split_tr' [Abs (x, T, (s as Const (@{const_syntax prod_case}, _) $ t))] =
    1.31          (* split (%x. (split (%y z. t))) => %(x,y,z). t *)
    1.32          let
    1.33            val Const (@{syntax_const "_abs"}, _) $
    1.34 @@ -215,7 +215,7 @@
    1.35              (Syntax.const @{syntax_const "_pattern"} $ x' $
    1.36                (Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t''
    1.37          end
    1.38 -    | split_tr' [Const (@{const_syntax split}, _) $ t] =
    1.39 +    | split_tr' [Const (@{const_syntax prod_case}, _) $ t] =
    1.40          (* split (split (%x y z. t)) => %((x, y), z). t *)
    1.41          split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
    1.42      | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
    1.43 @@ -225,7 +225,7 @@
    1.44              (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
    1.45          end
    1.46      | split_tr' _ = raise Match;
    1.47 -in [(@{const_syntax split}, split_tr')] end
    1.48 +in [(@{const_syntax prod_case}, split_tr')] end
    1.49  *}
    1.50  
    1.51  (* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *) 
    1.52 @@ -234,7 +234,7 @@
    1.53    fun split_guess_names_tr' _ T [Abs (x, _, Abs _)] = raise Match
    1.54      | split_guess_names_tr' _ T [Abs (x, xT, t)] =
    1.55          (case (head_of t) of
    1.56 -          Const (@{const_syntax split}, _) => raise Match
    1.57 +          Const (@{const_syntax prod_case}, _) => raise Match
    1.58          | _ =>
    1.59            let 
    1.60              val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
    1.61 @@ -246,7 +246,7 @@
    1.62            end)
    1.63      | split_guess_names_tr' _ T [t] =
    1.64          (case head_of t of
    1.65 -          Const (@{const_syntax split}, _) => raise Match
    1.66 +          Const (@{const_syntax prod_case}, _) => raise Match
    1.67          | _ =>
    1.68            let
    1.69              val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
    1.70 @@ -257,21 +257,12 @@
    1.71                (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
    1.72            end)
    1.73      | split_guess_names_tr' _ _ _ = raise Match;
    1.74 -in [(@{const_syntax split}, split_guess_names_tr')] end
    1.75 +in [(@{const_syntax prod_case}, split_guess_names_tr')] end
    1.76  *}
    1.77  
    1.78  
    1.79  subsubsection {* Code generator setup *}
    1.80  
    1.81 -lemma split_case_cert:
    1.82 -  assumes "CASE \<equiv> split f"
    1.83 -  shows "CASE (a, b) \<equiv> f a b"
    1.84 -  using assms by (simp add: split_prod_case)
    1.85 -
    1.86 -setup {*
    1.87 -  Code.add_case @{thm split_case_cert}
    1.88 -*}
    1.89 -
    1.90  code_type *
    1.91    (SML infix 2 "*")
    1.92    (OCaml infix 2 "*")
    1.93 @@ -315,7 +306,7 @@
    1.94          val s' = Codegen.new_name t s;
    1.95          val v = Free (s', T)
    1.96        in apfst (cons v) (strip_abs_split (i-1) (subst_bound (v, t))) end
    1.97 -  | strip_abs_split i (u as Const (@{const_name split}, _) $ t) =
    1.98 +  | strip_abs_split i (u as Const (@{const_name prod_case}, _) $ t) =
    1.99        (case strip_abs_split (i+1) t of
   1.100          (v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u)
   1.101        | _ => ([], u))
   1.102 @@ -357,7 +348,7 @@
   1.103    | _ => NONE);
   1.104  
   1.105  fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of
   1.106 -    (t1 as Const (@{const_name split}, _), t2 :: ts) =>
   1.107 +    (t1 as Const (@{const_name prod_case}, _), t2 :: ts) =>
   1.108        let
   1.109          val ([p], u) = strip_abs_split 1 (t1 $ t2);
   1.110          val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr;
   1.111 @@ -421,7 +412,7 @@
   1.112    by (simp add: Pair_fst_snd_eq)
   1.113  
   1.114  lemma split_conv [simp, code]: "split f (a, b) = f a b"
   1.115 -  by (simp add: split_prod_case)
   1.116 +  by (fact prod.cases)
   1.117  
   1.118  lemma splitI: "f a b \<Longrightarrow> split f (a, b)"
   1.119    by (rule split_conv [THEN iffD2])
   1.120 @@ -430,11 +421,11 @@
   1.121    by (rule split_conv [THEN iffD1])
   1.122  
   1.123  lemma split_Pair [simp]: "(\<lambda>(x, y). (x, y)) = id"
   1.124 -  by (simp add: split_prod_case expand_fun_eq split: prod.split)
   1.125 +  by (simp add: expand_fun_eq split: prod.split)
   1.126  
   1.127  lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
   1.128    -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *}
   1.129 -  by (simp add: split_prod_case expand_fun_eq split: prod.split)
   1.130 +  by (simp add: expand_fun_eq split: prod.split)
   1.131  
   1.132  lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
   1.133    by (cases x) simp
   1.134 @@ -443,7 +434,7 @@
   1.135    by (cases p) simp
   1.136  
   1.137  lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))"
   1.138 -  by (simp add: split_prod_case prod_case_unfold)
   1.139 +  by (simp add: prod_case_unfold)
   1.140  
   1.141  lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
   1.142    -- {* Prevents simplification of @{term c}: much faster *}
   1.143 @@ -529,7 +520,7 @@
   1.144      | no_args k i (Bound m) = m < k orelse m > k + i
   1.145      | no_args _ _ _ = true;
   1.146    fun split_pat tp i (Abs  (_, _, t)) = if tp 0 i t then SOME (i, t) else NONE
   1.147 -    | split_pat tp i (Const (@{const_name split}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
   1.148 +    | split_pat tp i (Const (@{const_name prod_case}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
   1.149      | split_pat tp i _ = NONE;
   1.150    fun metaeq ss lhs rhs = mk_meta_eq (Goal.prove (Simplifier.the_context ss) [] []
   1.151          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
   1.152 @@ -546,12 +537,12 @@
   1.153          if Pair_pat k i (t $ u) then incr_boundvars k arg
   1.154          else (subst arg k i t $ subst arg k i u)
   1.155      | subst arg k i t = t;
   1.156 -  fun beta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t) $ arg) =
   1.157 +  fun beta_proc ss (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t) $ arg) =
   1.158          (case split_pat beta_term_pat 1 t of
   1.159            SOME (i, f) => SOME (metaeq ss s (subst arg 0 i f))
   1.160          | NONE => NONE)
   1.161      | beta_proc _ _ = NONE;
   1.162 -  fun eta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t)) =
   1.163 +  fun eta_proc ss (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t)) =
   1.164          (case split_pat eta_term_pat 1 t of
   1.165            SOME (_, ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end))
   1.166          | NONE => NONE)
   1.167 @@ -598,10 +589,10 @@
   1.168    done
   1.169  
   1.170  lemma splitE: "split c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
   1.171 -  by (induct p) (auto simp add: split_prod_case)
   1.172 +  by (induct p) auto
   1.173  
   1.174  lemma splitE': "split c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
   1.175 -  by (induct p) (auto simp add: split_prod_case)
   1.176 +  by (induct p) auto
   1.177  
   1.178  lemma splitE2:
   1.179    "[| Q (split P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
   1.180 @@ -627,14 +618,14 @@
   1.181    assumes major: "z \<in> split c p"
   1.182      and cases: "\<And>x y. p = (x, y) \<Longrightarrow> z \<in> c x y \<Longrightarrow> Q"
   1.183    shows Q
   1.184 -  by (rule major [unfolded split_prod_case prod_case_unfold] cases surjective_pairing)+
   1.185 +  by (rule major [unfolded prod_case_unfold] cases surjective_pairing)+
   1.186  
   1.187  declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!]
   1.188  declare mem_splitE [elim!] splitE' [elim!] splitE [elim!]
   1.189  
   1.190  ML {*
   1.191  local (* filtering with exists_p_split is an essential optimization *)
   1.192 -  fun exists_p_split (Const (@{const_name split},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
   1.193 +  fun exists_p_split (Const (@{const_name prod_case},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
   1.194      | exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u
   1.195      | exists_p_split (Abs (_, _, t)) = exists_p_split t
   1.196      | exists_p_split _ = false;
   1.197 @@ -712,13 +703,9 @@
   1.198  declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!]
   1.199  declare prod_caseE' [elim!] prod_caseE [elim!]
   1.200  
   1.201 -lemma prod_case_split:
   1.202 -  "prod_case = split"
   1.203 -  by (auto simp add: expand_fun_eq)
   1.204 -
   1.205  lemma prod_case_beta:
   1.206    "prod_case f p = f (fst p) (snd p)"
   1.207 -  unfolding prod_case_split split_beta ..
   1.208 +  by (fact split_beta)
   1.209  
   1.210  lemma prod_cases3 [cases type]:
   1.211    obtains (fields) a b c where "y = (a, b, c)"
   1.212 @@ -762,7 +749,7 @@
   1.213  
   1.214  lemma split_def:
   1.215    "split = (\<lambda>c p. c (fst p) (snd p))"
   1.216 -  unfolding split_prod_case prod_case_unfold ..
   1.217 +  by (fact prod_case_unfold)
   1.218  
   1.219  definition internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
   1.220    "internal_split == split"