--- 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"