merged constants "split" and "prod_case"
authorhaftmann
Mon Jun 28 15:03:07 2010 +0200 (2010-06-28)
changeset 37591d3daea901123
parent 37590 180e80b4eac1
child 37592 e16495cfdde0
merged constants "split" and "prod_case"
NEWS
src/HOL/Hoare/Hoare_Logic.thy
src/HOL/Hoare/Hoare_Logic_Abort.thy
src/HOL/Hoare/hoare_tac.ML
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Import/HOL/pair.imp
src/HOL/Library/AssocList.thy
src/HOL/Library/Nat_Bijection.thy
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Probability/Borel.thy
src/HOL/Probability/Caratheodory.thy
src/HOL/Product_Type.thy
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
src/HOL/Tools/Quotient/quotient_term.ML
src/HOL/Tools/TFL/usyntax.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/quickcheck_generators.ML
src/HOL/Word/Num_Lemmas.thy
     1.1 --- a/NEWS	Mon Jun 28 15:03:07 2010 +0200
     1.2 +++ b/NEWS	Mon Jun 28 15:03:07 2010 +0200
     1.3 @@ -17,6 +17,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Constant "split" has been merged with constant "prod_case";  names
     1.8 +of ML functions, facts etc. involving split have been retained so far,
     1.9 +though.  INCOMPATIBILITY.
    1.10 +
    1.11  * Some previously unqualified names have been qualified:
    1.12  
    1.13    types
     2.1 --- a/src/HOL/Hoare/Hoare_Logic.thy	Mon Jun 28 15:03:07 2010 +0200
     2.2 +++ b/src/HOL/Hoare/Hoare_Logic.thy	Mon Jun 28 15:03:07 2010 +0200
     2.3 @@ -68,7 +68,7 @@
     2.4  
     2.5  fun mk_abstuple [x] body = abs (x, body)
     2.6    | mk_abstuple (x::xs) body =
     2.7 -      Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body);
     2.8 +      Syntax.const @{const_syntax prod_case} $ abs (x, mk_abstuple xs body);
     2.9  
    2.10  fun mk_fbody a e [x as (b,_)] = if a=b then e else Syntax.free b
    2.11    | mk_fbody a e ((b,_)::xs) =
    2.12 @@ -128,21 +128,21 @@
    2.13  
    2.14  (*** print translations ***)
    2.15  ML{*
    2.16 -fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) =
    2.17 +fun dest_abstuple (Const (@{const_syntax prod_case},_) $ (Abs(v,_, body))) =
    2.18                              subst_bound (Syntax.free v, dest_abstuple body)
    2.19    | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
    2.20    | dest_abstuple trm = trm;
    2.21  
    2.22 -fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
    2.23 +fun abs2list (Const (@{const_syntax prod_case},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
    2.24    | abs2list (Abs(x,T,t)) = [Free (x, T)]
    2.25    | abs2list _ = [];
    2.26  
    2.27 -fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t
    2.28 +fun mk_ts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = mk_ts t
    2.29    | mk_ts (Abs(x,_,t)) = mk_ts t
    2.30    | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
    2.31    | mk_ts t = [t];
    2.32  
    2.33 -fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) =
    2.34 +fun mk_vts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) =
    2.35             ((Syntax.free x)::(abs2list t), mk_ts t)
    2.36    | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
    2.37    | mk_vts t = raise Match;
    2.38 @@ -152,7 +152,7 @@
    2.39        if t = Bound i then find_ch vts (i-1) xs
    2.40        else (true, (v, subst_bounds (xs, t)));
    2.41  
    2.42 -fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true
    2.43 +fun is_f (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = true
    2.44    | is_f (Abs(x,_,t)) = true
    2.45    | is_f t = false;
    2.46  *}
     3.1 --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Mon Jun 28 15:03:07 2010 +0200
     3.2 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Mon Jun 28 15:03:07 2010 +0200
     3.3 @@ -70,7 +70,7 @@
     3.4  
     3.5  fun mk_abstuple [x] body = abs (x, body)
     3.6    | mk_abstuple (x::xs) body =
     3.7 -      Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body);
     3.8 +      Syntax.const @{const_syntax prod_case} $ abs (x, mk_abstuple xs body);
     3.9  
    3.10  fun mk_fbody a e [x as (b,_)] = if a=b then e else free b
    3.11    | mk_fbody a e ((b,_)::xs) =
    3.12 @@ -130,21 +130,21 @@
    3.13  
    3.14  (*** print translations ***)
    3.15  ML{*
    3.16 -fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) =
    3.17 +fun dest_abstuple (Const (@{const_syntax prod_case},_) $ (Abs(v,_, body))) =
    3.18        subst_bound (Syntax.free v, dest_abstuple body)
    3.19    | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
    3.20    | dest_abstuple trm = trm;
    3.21  
    3.22 -fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
    3.23 +fun abs2list (Const (@{const_syntax prod_case},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
    3.24    | abs2list (Abs(x,T,t)) = [Free (x, T)]
    3.25    | abs2list _ = [];
    3.26  
    3.27 -fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t
    3.28 +fun mk_ts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = mk_ts t
    3.29    | mk_ts (Abs(x,_,t)) = mk_ts t
    3.30    | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
    3.31    | mk_ts t = [t];
    3.32  
    3.33 -fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) =
    3.34 +fun mk_vts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) =
    3.35             ((Syntax.free x)::(abs2list t), mk_ts t)
    3.36    | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
    3.37    | mk_vts t = raise Match;
    3.38 @@ -154,7 +154,7 @@
    3.39        if t = Bound i then find_ch vts (i-1) xs
    3.40        else (true, (v, subst_bounds (xs,t)));
    3.41  
    3.42 -fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true
    3.43 +fun is_f (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = true
    3.44    | is_f (Abs(x,_,t)) = true
    3.45    | is_f t = false;
    3.46  *}
     4.1 --- a/src/HOL/Hoare/hoare_tac.ML	Mon Jun 28 15:03:07 2010 +0200
     4.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Mon Jun 28 15:03:07 2010 +0200
     4.3 @@ -16,7 +16,7 @@
     4.4  local open HOLogic in
     4.5  
     4.6  (** maps (%x1 ... xn. t) to [x1,...,xn] **)
     4.7 -fun abs2list (Const (@{const_name split}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
     4.8 +fun abs2list (Const (@{const_name prod_case}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
     4.9    | abs2list (Abs (x, T, t)) = [Free (x, T)]
    4.10    | abs2list _ = [];
    4.11  
    4.12 @@ -32,7 +32,7 @@
    4.13          else let val z  = mk_abstupleC w body;
    4.14                   val T2 = case z of Abs(_,T,_) => T
    4.15                          | Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T;
    4.16 -       in Const (@{const_name split}, (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT)
    4.17 +       in Const (@{const_name prod_case}, (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT)
    4.18            $ absfree (n, T, z) end end;
    4.19  
    4.20  (** maps [x1,...,xn] to (x1,...,xn) and types**)
     5.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jun 28 15:03:07 2010 +0200
     5.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jun 28 15:03:07 2010 +0200
     5.3 @@ -379,7 +379,7 @@
     5.4          from this Inl 1(1) exec_f mrec show ?thesis
     5.5          proof (cases "ret_mrec")
     5.6            case (Inl aaa)
     5.7 -          from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2)[OF exec_f Inl' Inr', of "aaa" "h2"] 1(3)
     5.8 +          from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2) [OF exec_f [symmetric] Inl' Inr', of "aaa" "h2"] 1(3)
     5.9              show ?thesis
    5.10                apply auto
    5.11                apply (rule rec_case)
     6.1 --- a/src/HOL/Import/HOL/pair.imp	Mon Jun 28 15:03:07 2010 +0200
     6.2 +++ b/src/HOL/Import/HOL/pair.imp	Mon Jun 28 15:03:07 2010 +0200
     6.3 @@ -10,8 +10,8 @@
     6.4    "prod" > "Product_Type.*"
     6.5  
     6.6  const_maps
     6.7 -  "pair_case" > "Product_Type.split"
     6.8 -  "UNCURRY" > "Product_Type.split"
     6.9 +  "pair_case" > "Product_Type.prod_case"
    6.10 +  "UNCURRY" > "Product_Type.prod_case"
    6.11    "FST" > "Product_Type.fst"
    6.12    "SND" > "Product_Type.snd"
    6.13    "RPROD" > "HOL4Base.pair.RPROD"
     7.1 --- a/src/HOL/Library/AssocList.thy	Mon Jun 28 15:03:07 2010 +0200
     7.2 +++ b/src/HOL/Library/AssocList.thy	Mon Jun 28 15:03:07 2010 +0200
     7.3 @@ -427,8 +427,7 @@
     7.4  
     7.5  lemma merge_updates:
     7.6    "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
     7.7 -  by (simp add: merge_def updates_def split_prod_case
     7.8 -    foldr_fold_rev zip_rev zip_map_fst_snd)
     7.9 +  by (simp add: merge_def updates_def foldr_fold_rev zip_rev zip_map_fst_snd)
    7.10  
    7.11  lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
    7.12    by (induct ys arbitrary: xs) (auto simp add: dom_update)
    7.13 @@ -449,7 +448,7 @@
    7.14      More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
    7.15      by (rule fold_apply) (simp add: update_conv' prod_case_beta split_def expand_fun_eq)
    7.16    then show ?thesis
    7.17 -    by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev split_prod_case expand_fun_eq)
    7.18 +    by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev expand_fun_eq)
    7.19  qed
    7.20  
    7.21  corollary merge_conv:
     8.1 --- a/src/HOL/Library/Nat_Bijection.thy	Mon Jun 28 15:03:07 2010 +0200
     8.2 +++ b/src/HOL/Library/Nat_Bijection.thy	Mon Jun 28 15:03:07 2010 +0200
     8.3 @@ -213,6 +213,7 @@
     8.4  termination list_decode
     8.5  apply (relation "measure id", simp_all)
     8.6  apply (drule arg_cong [where f="prod_encode"])
     8.7 +apply (drule sym)
     8.8  apply (simp add: le_imp_less_Suc le_prod_encode_2)
     8.9  done
    8.10  
     9.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Jun 28 15:03:07 2010 +0200
     9.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Jun 28 15:03:07 2010 +0200
     9.3 @@ -18,7 +18,7 @@
     9.4  
     9.5  section {* Pairs *}
     9.6  
     9.7 -setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name split}] *}
     9.8 +setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name prod_case}] *}
     9.9  
    9.10  section {* Bounded quantifiers *}
    9.11  
    10.1 --- a/src/HOL/Library/RBT_Impl.thy	Mon Jun 28 15:03:07 2010 +0200
    10.2 +++ b/src/HOL/Library/RBT_Impl.thy	Mon Jun 28 15:03:07 2010 +0200
    10.3 @@ -1076,7 +1076,7 @@
    10.4    from this Empty_is_rbt have
    10.5      "lookup (More_List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs"
    10.6       by (simp add: `ys = rev xs`)
    10.7 -  then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev prod_case_split)
    10.8 +  then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev)
    10.9  qed
   10.10  
   10.11  hide_const (open) Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
    11.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Mon Jun 28 15:03:07 2010 +0200
    11.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Mon Jun 28 15:03:07 2010 +0200
    11.3 @@ -323,7 +323,7 @@
    11.4      let val VarAbs = Syntax.variant_abs(s,tp,trm);
    11.5      in get_decls sign (Const(fst VarAbs,tp)::Clist) (snd VarAbs)
    11.6      end
    11.7 -  | get_decls sign Clist ((Const (@{const_name split}, _)) $ trm) = get_decls sign Clist trm
    11.8 +  | get_decls sign Clist ((Const (@{const_name prod_case}, _)) $ trm) = get_decls sign Clist trm
    11.9    | get_decls sign Clist trm = (Clist,trm);
   11.10  
   11.11  fun make_mu_def sign ((tt $ LHS) $ (ttt $ RHS)) =
   11.12 @@ -389,7 +389,7 @@
   11.13        val t2 = t1 $ ParamDeclTerm
   11.14    in t2 end;
   11.15  
   11.16 -fun is_fundef (Const("==", _) $ _ $ (Const (@{const_name split}, _) $ _)) = true
   11.17 +fun is_fundef (Const("==", _) $ _ $ (Const (@{const_name prod_case}, _) $ _)) = true
   11.18    | is_fundef (Const("==", _) $ _ $ Abs _) = true 
   11.19    | is_fundef _ = false; 
   11.20  
    12.1 --- a/src/HOL/Probability/Borel.thy	Mon Jun 28 15:03:07 2010 +0200
    12.2 +++ b/src/HOL/Probability/Borel.thy	Mon Jun 28 15:03:07 2010 +0200
    12.3 @@ -203,7 +203,7 @@
    12.4          by (metis surj_def)
    12.5  
    12.6        from Fract i j n show ?thesis
    12.7 -        by (metis prod.cases prod_case_split)
    12.8 +        by (metis prod.cases)
    12.9    qed
   12.10  qed
   12.11  
    13.1 --- a/src/HOL/Probability/Caratheodory.thy	Mon Jun 28 15:03:07 2010 +0200
    13.2 +++ b/src/HOL/Probability/Caratheodory.thy	Mon Jun 28 15:03:07 2010 +0200
    13.3 @@ -829,7 +829,7 @@
    13.4          with sbBB [of i] obtain j where "x \<in> BB i j"
    13.5            by blast        
    13.6          thus "\<exists>i. x \<in> split BB (prod_decode i)"
    13.7 -          by (metis prod_encode_inverse prod.cases prod_case_split)
    13.8 +          by (metis prod_encode_inverse prod.cases)
    13.9        qed 
   13.10      have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
   13.11        by (rule ext)  (auto simp add: C_def) 
    14.1 --- a/src/HOL/Product_Type.thy	Mon Jun 28 15:03:07 2010 +0200
    14.2 +++ b/src/HOL/Product_Type.thy	Mon Jun 28 15:03:07 2010 +0200
    14.3 @@ -163,8 +163,8 @@
    14.4  
    14.5  subsubsection {* Tuple syntax *}
    14.6  
    14.7 -definition split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
    14.8 -  split_prod_case: "split == prod_case"
    14.9 +abbreviation (input) split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
   14.10 +  "split \<equiv> prod_case"
   14.11  
   14.12  text {*
   14.13    Patterns -- extends pre-defined type @{typ pttrn} used in
   14.14 @@ -185,8 +185,8 @@
   14.15  translations
   14.16    "(x, y)" == "CONST Pair x y"
   14.17    "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))"
   14.18 -  "%(x, y, zs). b" == "CONST split (%x (y, zs). b)"
   14.19 -  "%(x, y). b" == "CONST split (%x y. b)"
   14.20 +  "%(x, y, zs). b" == "CONST prod_case (%x (y, zs). b)"
   14.21 +  "%(x, y). b" == "CONST prod_case (%x y. b)"
   14.22    "_abs (CONST Pair x y) t" => "%(x, y). t"
   14.23    -- {* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
   14.24       The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *}
   14.25 @@ -204,7 +204,7 @@
   14.26            Syntax.const @{syntax_const "_abs"} $
   14.27              (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
   14.28          end
   14.29 -    | split_tr' [Abs (x, T, (s as Const (@{const_syntax split}, _) $ t))] =
   14.30 +    | split_tr' [Abs (x, T, (s as Const (@{const_syntax prod_case}, _) $ t))] =
   14.31          (* split (%x. (split (%y z. t))) => %(x,y,z). t *)
   14.32          let
   14.33            val Const (@{syntax_const "_abs"}, _) $
   14.34 @@ -215,7 +215,7 @@
   14.35              (Syntax.const @{syntax_const "_pattern"} $ x' $
   14.36                (Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t''
   14.37          end
   14.38 -    | split_tr' [Const (@{const_syntax split}, _) $ t] =
   14.39 +    | split_tr' [Const (@{const_syntax prod_case}, _) $ t] =
   14.40          (* split (split (%x y z. t)) => %((x, y), z). t *)
   14.41          split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
   14.42      | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
   14.43 @@ -225,7 +225,7 @@
   14.44              (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
   14.45          end
   14.46      | split_tr' _ = raise Match;
   14.47 -in [(@{const_syntax split}, split_tr')] end
   14.48 +in [(@{const_syntax prod_case}, split_tr')] end
   14.49  *}
   14.50  
   14.51  (* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *) 
   14.52 @@ -234,7 +234,7 @@
   14.53    fun split_guess_names_tr' _ T [Abs (x, _, Abs _)] = raise Match
   14.54      | split_guess_names_tr' _ T [Abs (x, xT, t)] =
   14.55          (case (head_of t) of
   14.56 -          Const (@{const_syntax split}, _) => raise Match
   14.57 +          Const (@{const_syntax prod_case}, _) => raise Match
   14.58          | _ =>
   14.59            let 
   14.60              val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
   14.61 @@ -246,7 +246,7 @@
   14.62            end)
   14.63      | split_guess_names_tr' _ T [t] =
   14.64          (case head_of t of
   14.65 -          Const (@{const_syntax split}, _) => raise Match
   14.66 +          Const (@{const_syntax prod_case}, _) => raise Match
   14.67          | _ =>
   14.68            let
   14.69              val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
   14.70 @@ -257,21 +257,12 @@
   14.71                (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
   14.72            end)
   14.73      | split_guess_names_tr' _ _ _ = raise Match;
   14.74 -in [(@{const_syntax split}, split_guess_names_tr')] end
   14.75 +in [(@{const_syntax prod_case}, split_guess_names_tr')] end
   14.76  *}
   14.77  
   14.78  
   14.79  subsubsection {* Code generator setup *}
   14.80  
   14.81 -lemma split_case_cert:
   14.82 -  assumes "CASE \<equiv> split f"
   14.83 -  shows "CASE (a, b) \<equiv> f a b"
   14.84 -  using assms by (simp add: split_prod_case)
   14.85 -
   14.86 -setup {*
   14.87 -  Code.add_case @{thm split_case_cert}
   14.88 -*}
   14.89 -
   14.90  code_type *
   14.91    (SML infix 2 "*")
   14.92    (OCaml infix 2 "*")
   14.93 @@ -315,7 +306,7 @@
   14.94          val s' = Codegen.new_name t s;
   14.95          val v = Free (s', T)
   14.96        in apfst (cons v) (strip_abs_split (i-1) (subst_bound (v, t))) end
   14.97 -  | strip_abs_split i (u as Const (@{const_name split}, _) $ t) =
   14.98 +  | strip_abs_split i (u as Const (@{const_name prod_case}, _) $ t) =
   14.99        (case strip_abs_split (i+1) t of
  14.100          (v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u)
  14.101        | _ => ([], u))
  14.102 @@ -357,7 +348,7 @@
  14.103    | _ => NONE);
  14.104  
  14.105  fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of
  14.106 -    (t1 as Const (@{const_name split}, _), t2 :: ts) =>
  14.107 +    (t1 as Const (@{const_name prod_case}, _), t2 :: ts) =>
  14.108        let
  14.109          val ([p], u) = strip_abs_split 1 (t1 $ t2);
  14.110          val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr;
  14.111 @@ -421,7 +412,7 @@
  14.112    by (simp add: Pair_fst_snd_eq)
  14.113  
  14.114  lemma split_conv [simp, code]: "split f (a, b) = f a b"
  14.115 -  by (simp add: split_prod_case)
  14.116 +  by (fact prod.cases)
  14.117  
  14.118  lemma splitI: "f a b \<Longrightarrow> split f (a, b)"
  14.119    by (rule split_conv [THEN iffD2])
  14.120 @@ -430,11 +421,11 @@
  14.121    by (rule split_conv [THEN iffD1])
  14.122  
  14.123  lemma split_Pair [simp]: "(\<lambda>(x, y). (x, y)) = id"
  14.124 -  by (simp add: split_prod_case expand_fun_eq split: prod.split)
  14.125 +  by (simp add: expand_fun_eq split: prod.split)
  14.126  
  14.127  lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
  14.128    -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *}
  14.129 -  by (simp add: split_prod_case expand_fun_eq split: prod.split)
  14.130 +  by (simp add: expand_fun_eq split: prod.split)
  14.131  
  14.132  lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
  14.133    by (cases x) simp
  14.134 @@ -443,7 +434,7 @@
  14.135    by (cases p) simp
  14.136  
  14.137  lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))"
  14.138 -  by (simp add: split_prod_case prod_case_unfold)
  14.139 +  by (simp add: prod_case_unfold)
  14.140  
  14.141  lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
  14.142    -- {* Prevents simplification of @{term c}: much faster *}
  14.143 @@ -529,7 +520,7 @@
  14.144      | no_args k i (Bound m) = m < k orelse m > k + i
  14.145      | no_args _ _ _ = true;
  14.146    fun split_pat tp i (Abs  (_, _, t)) = if tp 0 i t then SOME (i, t) else NONE
  14.147 -    | split_pat tp i (Const (@{const_name split}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
  14.148 +    | split_pat tp i (Const (@{const_name prod_case}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
  14.149      | split_pat tp i _ = NONE;
  14.150    fun metaeq ss lhs rhs = mk_meta_eq (Goal.prove (Simplifier.the_context ss) [] []
  14.151          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
  14.152 @@ -546,12 +537,12 @@
  14.153          if Pair_pat k i (t $ u) then incr_boundvars k arg
  14.154          else (subst arg k i t $ subst arg k i u)
  14.155      | subst arg k i t = t;
  14.156 -  fun beta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t) $ arg) =
  14.157 +  fun beta_proc ss (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t) $ arg) =
  14.158          (case split_pat beta_term_pat 1 t of
  14.159            SOME (i, f) => SOME (metaeq ss s (subst arg 0 i f))
  14.160          | NONE => NONE)
  14.161      | beta_proc _ _ = NONE;
  14.162 -  fun eta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t)) =
  14.163 +  fun eta_proc ss (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t)) =
  14.164          (case split_pat eta_term_pat 1 t of
  14.165            SOME (_, ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end))
  14.166          | NONE => NONE)
  14.167 @@ -598,10 +589,10 @@
  14.168    done
  14.169  
  14.170  lemma splitE: "split c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
  14.171 -  by (induct p) (auto simp add: split_prod_case)
  14.172 +  by (induct p) auto
  14.173  
  14.174  lemma splitE': "split c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
  14.175 -  by (induct p) (auto simp add: split_prod_case)
  14.176 +  by (induct p) auto
  14.177  
  14.178  lemma splitE2:
  14.179    "[| Q (split P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
  14.180 @@ -627,14 +618,14 @@
  14.181    assumes major: "z \<in> split c p"
  14.182      and cases: "\<And>x y. p = (x, y) \<Longrightarrow> z \<in> c x y \<Longrightarrow> Q"
  14.183    shows Q
  14.184 -  by (rule major [unfolded split_prod_case prod_case_unfold] cases surjective_pairing)+
  14.185 +  by (rule major [unfolded prod_case_unfold] cases surjective_pairing)+
  14.186  
  14.187  declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!]
  14.188  declare mem_splitE [elim!] splitE' [elim!] splitE [elim!]
  14.189  
  14.190  ML {*
  14.191  local (* filtering with exists_p_split is an essential optimization *)
  14.192 -  fun exists_p_split (Const (@{const_name split},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
  14.193 +  fun exists_p_split (Const (@{const_name prod_case},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
  14.194      | exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u
  14.195      | exists_p_split (Abs (_, _, t)) = exists_p_split t
  14.196      | exists_p_split _ = false;
  14.197 @@ -712,13 +703,9 @@
  14.198  declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!]
  14.199  declare prod_caseE' [elim!] prod_caseE [elim!]
  14.200  
  14.201 -lemma prod_case_split:
  14.202 -  "prod_case = split"
  14.203 -  by (auto simp add: expand_fun_eq)
  14.204 -
  14.205  lemma prod_case_beta:
  14.206    "prod_case f p = f (fst p) (snd p)"
  14.207 -  unfolding prod_case_split split_beta ..
  14.208 +  by (fact split_beta)
  14.209  
  14.210  lemma prod_cases3 [cases type]:
  14.211    obtains (fields) a b c where "y = (a, b, c)"
  14.212 @@ -762,7 +749,7 @@
  14.213  
  14.214  lemma split_def:
  14.215    "split = (\<lambda>c p. c (fst p) (snd p))"
  14.216 -  unfolding split_prod_case prod_case_unfold ..
  14.217 +  by (fact prod_case_unfold)
  14.218  
  14.219  definition internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
  14.220    "internal_split == split"
    15.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Jun 28 15:03:07 2010 +0200
    15.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Jun 28 15:03:07 2010 +0200
    15.3 @@ -2080,7 +2080,7 @@
    15.4      list_abs (outer,
    15.5                Const (@{const_name Image}, uncurried_T --> set_T --> set_T)
    15.6                $ (Const (@{const_name rtrancl}, uncurried_T --> uncurried_T)
    15.7 -                 $ (Const (@{const_name split}, curried_T --> uncurried_T)
    15.8 +                 $ (Const (@{const_name prod_case}, curried_T --> uncurried_T)
    15.9                      $ list_comb (Const step_x, outer_bounds)))
   15.10                $ list_comb (Const base_x, outer_bounds)
   15.11                |> ap_curry tuple_arg_Ts tuple_T)
    16.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Jun 28 15:03:07 2010 +0200
    16.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Jun 28 15:03:07 2010 +0200
    16.3 @@ -2015,7 +2015,7 @@
    16.4    | split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t)
    16.5    | split_lambda t _ = raise (TERM ("split_lambda", [t]))
    16.6  
    16.7 -fun strip_split_abs (Const (@{const_name split}, _) $ t) = strip_split_abs t
    16.8 +fun strip_split_abs (Const (@{const_name prod_case}, _) $ t) = strip_split_abs t
    16.9    | strip_split_abs (Abs (_, _, t)) = strip_split_abs t
   16.10    | strip_split_abs t = t
   16.11  
    17.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Jun 28 15:03:07 2010 +0200
    17.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Jun 28 15:03:07 2010 +0200
    17.3 @@ -179,7 +179,7 @@
    17.4                |> maps (fn (res, (names, prems)) =>
    17.5                  flatten' (betapply (g, res)) (names, prems))
    17.6              end)
    17.7 -        | Const (@{const_name split}, _) => 
    17.8 +        | Const (@{const_name prod_case}, _) => 
    17.9              (let
   17.10                val (_, g :: res :: args) = strip_comb t
   17.11                val [res1, res2] = Name.variant_list names ["res1", "res2"]
    18.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Mon Jun 28 15:03:07 2010 +0200
    18.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Mon Jun 28 15:03:07 2010 +0200
    18.3 @@ -560,12 +560,12 @@
    18.4             end
    18.5         end
    18.6  
    18.7 -  | (((t1 as Const (@{const_name split}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
    18.8 -     ((t2 as Const (@{const_name split}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
    18.9 +  | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
   18.10 +     ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
   18.11         regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
   18.12  
   18.13 -  | (((t1 as Const (@{const_name split}, _)) $ Abs (v1, ty, s1)),
   18.14 -     ((t2 as Const (@{const_name split}, _)) $ Abs (v2, _ , s2))) =>
   18.15 +  | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, s1)),
   18.16 +     ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , s2))) =>
   18.17         regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
   18.18  
   18.19    | (t1 $ t2, t1' $ t2') =>
    19.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Mon Jun 28 15:03:07 2010 +0200
    19.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Mon Jun 28 15:03:07 2010 +0200
    19.3 @@ -196,7 +196,7 @@
    19.4  
    19.5  local
    19.6  fun mk_uncurry (xt, yt, zt) =
    19.7 -    Const(@{const_name split}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
    19.8 +    Const(@{const_name prod_case}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
    19.9  fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
   19.10    | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
   19.11  fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
   19.12 @@ -276,7 +276,7 @@
   19.13    | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
   19.14  
   19.15  
   19.16 -local  fun ucheck t = (if #Name (dest_const t) = @{const_name split} then t
   19.17 +local  fun ucheck t = (if #Name (dest_const t) = @{const_name prod_case} then t
   19.18                         else raise Match)
   19.19  in
   19.20  fun dest_pabs used tm =
    20.1 --- a/src/HOL/Tools/hologic.ML	Mon Jun 28 15:03:07 2010 +0200
    20.2 +++ b/src/HOL/Tools/hologic.ML	Mon Jun 28 15:03:07 2010 +0200
    20.3 @@ -315,12 +315,12 @@
    20.4    end;
    20.5  
    20.6  fun split_const (A, B, C) =
    20.7 -  Const ("Product_Type.split", (A --> B --> C) --> mk_prodT (A, B) --> C);
    20.8 +  Const ("Product_Type.prod.prod_case", (A --> B --> C) --> mk_prodT (A, B) --> C);
    20.9  
   20.10  fun mk_split t =
   20.11    (case Term.fastype_of t of
   20.12      T as (Type ("fun", [A, Type ("fun", [B, C])])) =>
   20.13 -      Const ("Product_Type.split", T --> mk_prodT (A, B) --> C) $ t
   20.14 +      Const ("Product_Type.prod.prod_case", T --> mk_prodT (A, B) --> C) $ t
   20.15    | _ => raise TERM ("mk_split: bad body type", [t]));
   20.16  
   20.17  (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
   20.18 @@ -427,7 +427,7 @@
   20.19  val strip_psplits =
   20.20    let
   20.21      fun strip [] qs Ts t = (t, rev Ts, qs)
   20.22 -      | strip (p :: ps) qs Ts (Const ("Product_Type.split", _) $ t) =
   20.23 +      | strip (p :: ps) qs Ts (Const ("Product_Type.prod.prod_case", _) $ t) =
   20.24            strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
   20.25        | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
   20.26        | strip (p :: ps) qs Ts t = strip ps qs
    21.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Mon Jun 28 15:03:07 2010 +0200
    21.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Mon Jun 28 15:03:07 2010 +0200
    21.3 @@ -374,7 +374,7 @@
    21.4      fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
    21.5        liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
    21.6      fun mk_split T = Sign.mk_const thy
    21.7 -      (@{const_name split}, [T, @{typ "unit => term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
    21.8 +      (@{const_name prod_case}, [T, @{typ "unit => term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
    21.9      fun mk_scomp_split T t t' =
   21.10        mk_scomp (mk_termtyp T) @{typ "term list option"} @{typ Random.seed} t
   21.11          (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
   21.12 @@ -414,7 +414,7 @@
   21.13      fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
   21.14        liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
   21.15      fun mk_split T = Sign.mk_const thy
   21.16 -      (@{const_name split}, [T, @{typ "unit => term"},
   21.17 +      (@{const_name prod_case}, [T, @{typ "unit => term"},
   21.18          liftT @{typ "term list option * (bool list * bool)"} @{typ Random.seed}]);
   21.19      fun mk_scomp_split T t t' =
   21.20        mk_scomp (mk_termtyp T) @{typ "term list option * (bool list * bool)"} @{typ Random.seed} t
    22.1 --- a/src/HOL/Word/Num_Lemmas.thy	Mon Jun 28 15:03:07 2010 +0200
    22.2 +++ b/src/HOL/Word/Num_Lemmas.thy	Mon Jun 28 15:03:07 2010 +0200
    22.3 @@ -11,8 +11,8 @@
    22.4  lemma contentsI: "y = {x} ==> contents y = x" 
    22.5    unfolding contents_def by auto -- {* FIXME move *}
    22.6  
    22.7 -lemmas split_split = prod.split [unfolded prod_case_split]
    22.8 -lemmas split_split_asm = prod.split_asm [unfolded prod_case_split]
    22.9 +lemmas split_split = prod.split
   22.10 +lemmas split_split_asm = prod.split_asm
   22.11  lemmas split_splits = split_split split_split_asm
   22.12  
   22.13  lemmas funpow_0 = funpow.simps(1)