--- a/NEWS Mon Jun 28 15:03:07 2010 +0200
+++ b/NEWS Mon Jun 28 15:03:07 2010 +0200
@@ -17,6 +17,10 @@
*** HOL ***
+* Constant "split" has been merged with constant "prod_case"; names
+of ML functions, facts etc. involving split have been retained so far,
+though. INCOMPATIBILITY.
+
* Some previously unqualified names have been qualified:
types
--- a/src/HOL/Hoare/Hoare_Logic.thy Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy Mon Jun 28 15:03:07 2010 +0200
@@ -68,7 +68,7 @@
fun mk_abstuple [x] body = abs (x, body)
| mk_abstuple (x::xs) body =
- Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body);
+ Syntax.const @{const_syntax prod_case} $ abs (x, mk_abstuple xs body);
fun mk_fbody a e [x as (b,_)] = if a=b then e else Syntax.free b
| mk_fbody a e ((b,_)::xs) =
@@ -128,21 +128,21 @@
(*** print translations ***)
ML{*
-fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) =
+fun dest_abstuple (Const (@{const_syntax prod_case},_) $ (Abs(v,_, body))) =
subst_bound (Syntax.free v, dest_abstuple body)
| dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
| dest_abstuple trm = trm;
-fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
+fun abs2list (Const (@{const_syntax prod_case},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
| abs2list (Abs(x,T,t)) = [Free (x, T)]
| abs2list _ = [];
-fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t
+fun mk_ts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = mk_ts t
| mk_ts (Abs(x,_,t)) = mk_ts t
| mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
| mk_ts t = [t];
-fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) =
+fun mk_vts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) =
((Syntax.free x)::(abs2list t), mk_ts t)
| mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
| mk_vts t = raise Match;
@@ -152,7 +152,7 @@
if t = Bound i then find_ch vts (i-1) xs
else (true, (v, subst_bounds (xs, t)));
-fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true
+fun is_f (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = true
| is_f (Abs(x,_,t)) = true
| is_f t = false;
*}
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Mon Jun 28 15:03:07 2010 +0200
@@ -70,7 +70,7 @@
fun mk_abstuple [x] body = abs (x, body)
| mk_abstuple (x::xs) body =
- Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body);
+ Syntax.const @{const_syntax prod_case} $ abs (x, mk_abstuple xs body);
fun mk_fbody a e [x as (b,_)] = if a=b then e else free b
| mk_fbody a e ((b,_)::xs) =
@@ -130,21 +130,21 @@
(*** print translations ***)
ML{*
-fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) =
+fun dest_abstuple (Const (@{const_syntax prod_case},_) $ (Abs(v,_, body))) =
subst_bound (Syntax.free v, dest_abstuple body)
| dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
| dest_abstuple trm = trm;
-fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
+fun abs2list (Const (@{const_syntax prod_case},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
| abs2list (Abs(x,T,t)) = [Free (x, T)]
| abs2list _ = [];
-fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t
+fun mk_ts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = mk_ts t
| mk_ts (Abs(x,_,t)) = mk_ts t
| mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
| mk_ts t = [t];
-fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) =
+fun mk_vts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) =
((Syntax.free x)::(abs2list t), mk_ts t)
| mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
| mk_vts t = raise Match;
@@ -154,7 +154,7 @@
if t = Bound i then find_ch vts (i-1) xs
else (true, (v, subst_bounds (xs,t)));
-fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true
+fun is_f (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = true
| is_f (Abs(x,_,t)) = true
| is_f t = false;
*}
--- a/src/HOL/Hoare/hoare_tac.ML Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Mon Jun 28 15:03:07 2010 +0200
@@ -16,7 +16,7 @@
local open HOLogic in
(** maps (%x1 ... xn. t) to [x1,...,xn] **)
-fun abs2list (Const (@{const_name split}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
+fun abs2list (Const (@{const_name prod_case}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
| abs2list (Abs (x, T, t)) = [Free (x, T)]
| abs2list _ = [];
@@ -32,7 +32,7 @@
else let val z = mk_abstupleC w body;
val T2 = case z of Abs(_,T,_) => T
| Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T;
- in Const (@{const_name split}, (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT)
+ in Const (@{const_name prod_case}, (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT)
$ absfree (n, T, z) end end;
(** maps [x1,...,xn] to (x1,...,xn) and types**)
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Jun 28 15:03:07 2010 +0200
@@ -379,7 +379,7 @@
from this Inl 1(1) exec_f mrec show ?thesis
proof (cases "ret_mrec")
case (Inl aaa)
- from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2)[OF exec_f Inl' Inr', of "aaa" "h2"] 1(3)
+ from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2) [OF exec_f [symmetric] Inl' Inr', of "aaa" "h2"] 1(3)
show ?thesis
apply auto
apply (rule rec_case)
--- a/src/HOL/Import/HOL/pair.imp Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Import/HOL/pair.imp Mon Jun 28 15:03:07 2010 +0200
@@ -10,8 +10,8 @@
"prod" > "Product_Type.*"
const_maps
- "pair_case" > "Product_Type.split"
- "UNCURRY" > "Product_Type.split"
+ "pair_case" > "Product_Type.prod_case"
+ "UNCURRY" > "Product_Type.prod_case"
"FST" > "Product_Type.fst"
"SND" > "Product_Type.snd"
"RPROD" > "HOL4Base.pair.RPROD"
--- a/src/HOL/Library/AssocList.thy Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Library/AssocList.thy Mon Jun 28 15:03:07 2010 +0200
@@ -427,8 +427,7 @@
lemma merge_updates:
"merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
- by (simp add: merge_def updates_def split_prod_case
- foldr_fold_rev zip_rev zip_map_fst_snd)
+ by (simp add: merge_def updates_def foldr_fold_rev zip_rev zip_map_fst_snd)
lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
by (induct ys arbitrary: xs) (auto simp add: dom_update)
@@ -449,7 +448,7 @@
More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
by (rule fold_apply) (simp add: update_conv' prod_case_beta split_def expand_fun_eq)
then show ?thesis
- by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev split_prod_case expand_fun_eq)
+ by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev expand_fun_eq)
qed
corollary merge_conv:
--- a/src/HOL/Library/Nat_Bijection.thy Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Library/Nat_Bijection.thy Mon Jun 28 15:03:07 2010 +0200
@@ -213,6 +213,7 @@
termination list_decode
apply (relation "measure id", simp_all)
apply (drule arg_cong [where f="prod_encode"])
+apply (drule sym)
apply (simp add: le_imp_less_Suc le_prod_encode_2)
done
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Jun 28 15:03:07 2010 +0200
@@ -18,7 +18,7 @@
section {* Pairs *}
-setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name split}] *}
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name prod_case}] *}
section {* Bounded quantifiers *}
--- a/src/HOL/Library/RBT_Impl.thy Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Library/RBT_Impl.thy Mon Jun 28 15:03:07 2010 +0200
@@ -1076,7 +1076,7 @@
from this Empty_is_rbt have
"lookup (More_List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs"
by (simp add: `ys = rev xs`)
- then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev prod_case_split)
+ then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev)
qed
hide_const (open) Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
--- a/src/HOL/Modelcheck/mucke_oracle.ML Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Mon Jun 28 15:03:07 2010 +0200
@@ -323,7 +323,7 @@
let val VarAbs = Syntax.variant_abs(s,tp,trm);
in get_decls sign (Const(fst VarAbs,tp)::Clist) (snd VarAbs)
end
- | get_decls sign Clist ((Const (@{const_name split}, _)) $ trm) = get_decls sign Clist trm
+ | get_decls sign Clist ((Const (@{const_name prod_case}, _)) $ trm) = get_decls sign Clist trm
| get_decls sign Clist trm = (Clist,trm);
fun make_mu_def sign ((tt $ LHS) $ (ttt $ RHS)) =
@@ -389,7 +389,7 @@
val t2 = t1 $ ParamDeclTerm
in t2 end;
-fun is_fundef (Const("==", _) $ _ $ (Const (@{const_name split}, _) $ _)) = true
+fun is_fundef (Const("==", _) $ _ $ (Const (@{const_name prod_case}, _) $ _)) = true
| is_fundef (Const("==", _) $ _ $ Abs _) = true
| is_fundef _ = false;
--- a/src/HOL/Probability/Borel.thy Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Probability/Borel.thy Mon Jun 28 15:03:07 2010 +0200
@@ -203,7 +203,7 @@
by (metis surj_def)
from Fract i j n show ?thesis
- by (metis prod.cases prod_case_split)
+ by (metis prod.cases)
qed
qed
--- a/src/HOL/Probability/Caratheodory.thy Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Probability/Caratheodory.thy Mon Jun 28 15:03:07 2010 +0200
@@ -829,7 +829,7 @@
with sbBB [of i] obtain j where "x \<in> BB i j"
by blast
thus "\<exists>i. x \<in> split BB (prod_decode i)"
- by (metis prod_encode_inverse prod.cases prod_case_split)
+ by (metis prod_encode_inverse prod.cases)
qed
have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
by (rule ext) (auto simp add: C_def)
--- a/src/HOL/Product_Type.thy Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Product_Type.thy Mon Jun 28 15:03:07 2010 +0200
@@ -163,8 +163,8 @@
subsubsection {* Tuple syntax *}
-definition split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
- split_prod_case: "split == prod_case"
+abbreviation (input) split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
+ "split \<equiv> prod_case"
text {*
Patterns -- extends pre-defined type @{typ pttrn} used in
@@ -185,8 +185,8 @@
translations
"(x, y)" == "CONST Pair x y"
"_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))"
- "%(x, y, zs). b" == "CONST split (%x (y, zs). b)"
- "%(x, y). b" == "CONST split (%x y. b)"
+ "%(x, y, zs). b" == "CONST prod_case (%x (y, zs). b)"
+ "%(x, y). b" == "CONST prod_case (%x y. b)"
"_abs (CONST Pair x y) t" => "%(x, y). t"
-- {* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *}
@@ -204,7 +204,7 @@
Syntax.const @{syntax_const "_abs"} $
(Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
end
- | split_tr' [Abs (x, T, (s as Const (@{const_syntax split}, _) $ t))] =
+ | split_tr' [Abs (x, T, (s as Const (@{const_syntax prod_case}, _) $ t))] =
(* split (%x. (split (%y z. t))) => %(x,y,z). t *)
let
val Const (@{syntax_const "_abs"}, _) $
@@ -215,7 +215,7 @@
(Syntax.const @{syntax_const "_pattern"} $ x' $
(Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t''
end
- | split_tr' [Const (@{const_syntax split}, _) $ t] =
+ | split_tr' [Const (@{const_syntax prod_case}, _) $ t] =
(* split (split (%x y z. t)) => %((x, y), z). t *)
split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
| split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
@@ -225,7 +225,7 @@
(Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
end
| split_tr' _ = raise Match;
-in [(@{const_syntax split}, split_tr')] end
+in [(@{const_syntax prod_case}, split_tr')] end
*}
(* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *)
@@ -234,7 +234,7 @@
fun split_guess_names_tr' _ T [Abs (x, _, Abs _)] = raise Match
| split_guess_names_tr' _ T [Abs (x, xT, t)] =
(case (head_of t) of
- Const (@{const_syntax split}, _) => raise Match
+ Const (@{const_syntax prod_case}, _) => raise Match
| _ =>
let
val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
@@ -246,7 +246,7 @@
end)
| split_guess_names_tr' _ T [t] =
(case head_of t of
- Const (@{const_syntax split}, _) => raise Match
+ Const (@{const_syntax prod_case}, _) => raise Match
| _ =>
let
val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
@@ -257,21 +257,12 @@
(Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
end)
| split_guess_names_tr' _ _ _ = raise Match;
-in [(@{const_syntax split}, split_guess_names_tr')] end
+in [(@{const_syntax prod_case}, split_guess_names_tr')] end
*}
subsubsection {* Code generator setup *}
-lemma split_case_cert:
- assumes "CASE \<equiv> split f"
- shows "CASE (a, b) \<equiv> f a b"
- using assms by (simp add: split_prod_case)
-
-setup {*
- Code.add_case @{thm split_case_cert}
-*}
-
code_type *
(SML infix 2 "*")
(OCaml infix 2 "*")
@@ -315,7 +306,7 @@
val s' = Codegen.new_name t s;
val v = Free (s', T)
in apfst (cons v) (strip_abs_split (i-1) (subst_bound (v, t))) end
- | strip_abs_split i (u as Const (@{const_name split}, _) $ t) =
+ | strip_abs_split i (u as Const (@{const_name prod_case}, _) $ t) =
(case strip_abs_split (i+1) t of
(v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u)
| _ => ([], u))
@@ -357,7 +348,7 @@
| _ => NONE);
fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of
- (t1 as Const (@{const_name split}, _), t2 :: ts) =>
+ (t1 as Const (@{const_name prod_case}, _), t2 :: ts) =>
let
val ([p], u) = strip_abs_split 1 (t1 $ t2);
val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr;
@@ -421,7 +412,7 @@
by (simp add: Pair_fst_snd_eq)
lemma split_conv [simp, code]: "split f (a, b) = f a b"
- by (simp add: split_prod_case)
+ by (fact prod.cases)
lemma splitI: "f a b \<Longrightarrow> split f (a, b)"
by (rule split_conv [THEN iffD2])
@@ -430,11 +421,11 @@
by (rule split_conv [THEN iffD1])
lemma split_Pair [simp]: "(\<lambda>(x, y). (x, y)) = id"
- by (simp add: split_prod_case expand_fun_eq split: prod.split)
+ by (simp add: expand_fun_eq split: prod.split)
lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
-- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *}
- by (simp add: split_prod_case expand_fun_eq split: prod.split)
+ by (simp add: expand_fun_eq split: prod.split)
lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
by (cases x) simp
@@ -443,7 +434,7 @@
by (cases p) simp
lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))"
- by (simp add: split_prod_case prod_case_unfold)
+ by (simp add: prod_case_unfold)
lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
-- {* Prevents simplification of @{term c}: much faster *}
@@ -529,7 +520,7 @@
| no_args k i (Bound m) = m < k orelse m > k + i
| no_args _ _ _ = true;
fun split_pat tp i (Abs (_, _, t)) = if tp 0 i t then SOME (i, t) else NONE
- | split_pat tp i (Const (@{const_name split}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
+ | split_pat tp i (Const (@{const_name prod_case}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
| split_pat tp i _ = NONE;
fun metaeq ss lhs rhs = mk_meta_eq (Goal.prove (Simplifier.the_context ss) [] []
(HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
@@ -546,12 +537,12 @@
if Pair_pat k i (t $ u) then incr_boundvars k arg
else (subst arg k i t $ subst arg k i u)
| subst arg k i t = t;
- fun beta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t) $ arg) =
+ fun beta_proc ss (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t) $ arg) =
(case split_pat beta_term_pat 1 t of
SOME (i, f) => SOME (metaeq ss s (subst arg 0 i f))
| NONE => NONE)
| beta_proc _ _ = NONE;
- fun eta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t)) =
+ fun eta_proc ss (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t)) =
(case split_pat eta_term_pat 1 t of
SOME (_, ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end))
| NONE => NONE)
@@ -598,10 +589,10 @@
done
lemma splitE: "split c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
- by (induct p) (auto simp add: split_prod_case)
+ by (induct p) auto
lemma splitE': "split c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
- by (induct p) (auto simp add: split_prod_case)
+ by (induct p) auto
lemma splitE2:
"[| Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
@@ -627,14 +618,14 @@
assumes major: "z \<in> split c p"
and cases: "\<And>x y. p = (x, y) \<Longrightarrow> z \<in> c x y \<Longrightarrow> Q"
shows Q
- by (rule major [unfolded split_prod_case prod_case_unfold] cases surjective_pairing)+
+ by (rule major [unfolded prod_case_unfold] cases surjective_pairing)+
declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!]
declare mem_splitE [elim!] splitE' [elim!] splitE [elim!]
ML {*
local (* filtering with exists_p_split is an essential optimization *)
- fun exists_p_split (Const (@{const_name split},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
+ fun exists_p_split (Const (@{const_name prod_case},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
| exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u
| exists_p_split (Abs (_, _, t)) = exists_p_split t
| exists_p_split _ = false;
@@ -712,13 +703,9 @@
declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!]
declare prod_caseE' [elim!] prod_caseE [elim!]
-lemma prod_case_split:
- "prod_case = split"
- by (auto simp add: expand_fun_eq)
-
lemma prod_case_beta:
"prod_case f p = f (fst p) (snd p)"
- unfolding prod_case_split split_beta ..
+ by (fact split_beta)
lemma prod_cases3 [cases type]:
obtains (fields) a b c where "y = (a, b, c)"
@@ -762,7 +749,7 @@
lemma split_def:
"split = (\<lambda>c p. c (fst p) (snd p))"
- unfolding split_prod_case prod_case_unfold ..
+ by (fact prod_case_unfold)
definition internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
"internal_split == split"
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Jun 28 15:03:07 2010 +0200
@@ -2080,7 +2080,7 @@
list_abs (outer,
Const (@{const_name Image}, uncurried_T --> set_T --> set_T)
$ (Const (@{const_name rtrancl}, uncurried_T --> uncurried_T)
- $ (Const (@{const_name split}, curried_T --> uncurried_T)
+ $ (Const (@{const_name prod_case}, curried_T --> uncurried_T)
$ list_comb (Const step_x, outer_bounds)))
$ list_comb (Const base_x, outer_bounds)
|> ap_curry tuple_arg_Ts tuple_T)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Jun 28 15:03:07 2010 +0200
@@ -2015,7 +2015,7 @@
| split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t)
| split_lambda t _ = raise (TERM ("split_lambda", [t]))
-fun strip_split_abs (Const (@{const_name split}, _) $ t) = strip_split_abs t
+fun strip_split_abs (Const (@{const_name prod_case}, _) $ t) = strip_split_abs t
| strip_split_abs (Abs (_, _, t)) = strip_split_abs t
| strip_split_abs t = t
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Mon Jun 28 15:03:07 2010 +0200
@@ -179,7 +179,7 @@
|> maps (fn (res, (names, prems)) =>
flatten' (betapply (g, res)) (names, prems))
end)
- | Const (@{const_name split}, _) =>
+ | Const (@{const_name prod_case}, _) =>
(let
val (_, g :: res :: args) = strip_comb t
val [res1, res2] = Name.variant_list names ["res1", "res2"]
--- a/src/HOL/Tools/Quotient/quotient_term.ML Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Mon Jun 28 15:03:07 2010 +0200
@@ -560,12 +560,12 @@
end
end
- | (((t1 as Const (@{const_name split}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
- ((t2 as Const (@{const_name split}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) =>
+ | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
+ ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) =>
regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
- | (((t1 as Const (@{const_name split}, _)) $ Abs (v1, ty, s1)),
- ((t2 as Const (@{const_name split}, _)) $ Abs (v2, _ , s2))) =>
+ | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, s1)),
+ ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , s2))) =>
regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
| (t1 $ t2, t1' $ t2') =>
--- a/src/HOL/Tools/TFL/usyntax.ML Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML Mon Jun 28 15:03:07 2010 +0200
@@ -196,7 +196,7 @@
local
fun mk_uncurry (xt, yt, zt) =
- Const(@{const_name split}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
+ Const(@{const_name prod_case}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
| dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
@@ -276,7 +276,7 @@
| dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
-local fun ucheck t = (if #Name (dest_const t) = @{const_name split} then t
+local fun ucheck t = (if #Name (dest_const t) = @{const_name prod_case} then t
else raise Match)
in
fun dest_pabs used tm =
--- a/src/HOL/Tools/hologic.ML Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Tools/hologic.ML Mon Jun 28 15:03:07 2010 +0200
@@ -315,12 +315,12 @@
end;
fun split_const (A, B, C) =
- Const ("Product_Type.split", (A --> B --> C) --> mk_prodT (A, B) --> C);
+ Const ("Product_Type.prod.prod_case", (A --> B --> C) --> mk_prodT (A, B) --> C);
fun mk_split t =
(case Term.fastype_of t of
T as (Type ("fun", [A, Type ("fun", [B, C])])) =>
- Const ("Product_Type.split", T --> mk_prodT (A, B) --> C) $ t
+ Const ("Product_Type.prod.prod_case", T --> mk_prodT (A, B) --> C) $ t
| _ => raise TERM ("mk_split: bad body type", [t]));
(*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
@@ -427,7 +427,7 @@
val strip_psplits =
let
fun strip [] qs Ts t = (t, rev Ts, qs)
- | strip (p :: ps) qs Ts (Const ("Product_Type.split", _) $ t) =
+ | strip (p :: ps) qs Ts (Const ("Product_Type.prod.prod_case", _) $ t) =
strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
| strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
| strip (p :: ps) qs Ts t = strip ps qs
--- a/src/HOL/Tools/quickcheck_generators.ML Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Mon Jun 28 15:03:07 2010 +0200
@@ -374,7 +374,7 @@
fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
fun mk_split T = Sign.mk_const thy
- (@{const_name split}, [T, @{typ "unit => term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
+ (@{const_name prod_case}, [T, @{typ "unit => term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
fun mk_scomp_split T t t' =
mk_scomp (mk_termtyp T) @{typ "term list option"} @{typ Random.seed} t
(mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
@@ -414,7 +414,7 @@
fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
fun mk_split T = Sign.mk_const thy
- (@{const_name split}, [T, @{typ "unit => term"},
+ (@{const_name prod_case}, [T, @{typ "unit => term"},
liftT @{typ "term list option * (bool list * bool)"} @{typ Random.seed}]);
fun mk_scomp_split T t t' =
mk_scomp (mk_termtyp T) @{typ "term list option * (bool list * bool)"} @{typ Random.seed} t
--- a/src/HOL/Word/Num_Lemmas.thy Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Word/Num_Lemmas.thy Mon Jun 28 15:03:07 2010 +0200
@@ -11,8 +11,8 @@
lemma contentsI: "y = {x} ==> contents y = x"
unfolding contents_def by auto -- {* FIXME move *}
-lemmas split_split = prod.split [unfolded prod_case_split]
-lemmas split_split_asm = prod.split_asm [unfolded prod_case_split]
+lemmas split_split = prod.split
+lemmas split_split_asm = prod.split_asm
lemmas split_splits = split_split split_split_asm
lemmas funpow_0 = funpow.simps(1)