--- a/src/HOL/Product_Type.thy Tue Jun 08 16:37:22 2010 +0200
+++ b/src/HOL/Product_Type.thy Thu Jun 10 12:24:01 2010 +0200
@@ -9,6 +9,7 @@
imports Typedef Inductive Fun
uses
("Tools/split_rule.ML")
+ ("Tools/inductive_codegen.ML")
("Tools/inductive_set.ML")
begin
@@ -128,13 +129,10 @@
definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
"Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
-global
-
-typedef (Prod)
- ('a, 'b) "*" (infixr "*" 20)
- = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
+typedef (prod) ('a, 'b) "*" (infixr "*" 20)
+ = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
proof
- fix a b show "Pair_Rep a b \<in> ?Prod"
+ fix a b show "Pair_Rep a b \<in> ?prod"
by rule+
qed
@@ -143,35 +141,27 @@
type_notation (HTML output)
"*" ("(_ \<times>/ _)" [21, 20] 20)
-consts
- Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b"
-
-local
-
-defs
- Pair_def: "Pair a b == Abs_Prod (Pair_Rep a b)"
+definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where
+ "Pair a b = Abs_prod (Pair_Rep a b)"
rep_datatype (prod) Pair proof -
fix P :: "'a \<times> 'b \<Rightarrow> bool" and p
assume "\<And>a b. P (Pair a b)"
- then show "P p" by (cases p) (auto simp add: Prod_def Pair_def Pair_Rep_def)
+ then show "P p" by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
next
fix a c :: 'a and b d :: 'b
have "Pair_Rep a b = Pair_Rep c d \<longleftrightarrow> a = c \<and> b = d"
by (auto simp add: Pair_Rep_def expand_fun_eq)
- moreover have "Pair_Rep a b \<in> Prod" and "Pair_Rep c d \<in> Prod"
- by (auto simp add: Prod_def)
+ moreover have "Pair_Rep a b \<in> prod" and "Pair_Rep c d \<in> prod"
+ by (auto simp add: prod_def)
ultimately show "Pair a b = Pair c d \<longleftrightarrow> a = c \<and> b = d"
- by (simp add: Pair_def Abs_Prod_inject)
+ by (simp add: Pair_def Abs_prod_inject)
qed
subsubsection {* Tuple syntax *}
-global consts
- split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"
-
-local defs
+definition split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
split_prod_case: "split == prod_case"
text {*
@@ -393,13 +383,11 @@
lemma surj_pair [simp]: "EX x y. p = (x, y)"
by (cases p) simp
-global consts
- fst :: "'a \<times> 'b \<Rightarrow> 'a"
- snd :: "'a \<times> 'b \<Rightarrow> 'b"
+definition fst :: "'a \<times> 'b \<Rightarrow> 'a" where
+ "fst p = (case p of (a, b) \<Rightarrow> a)"
-local defs
- fst_def: "fst p == case p of (a, b) \<Rightarrow> a"
- snd_def: "snd p == case p of (a, b) \<Rightarrow> b"
+definition snd :: "'a \<times> 'b \<Rightarrow> 'b" where
+ "snd p = (case p of (a, b) \<Rightarrow> b)"
lemma fst_conv [simp, code]: "fst (a, b) = a"
unfolding fst_def by simp
@@ -1189,6 +1177,9 @@
subsection {* Inductively defined sets *}
+use "Tools/inductive_codegen.ML"
+setup Inductive_Codegen.setup
+
use "Tools/inductive_set.ML"
setup Inductive_Set.setup
--- a/src/HOL/Tools/hologic.ML Tue Jun 08 16:37:22 2010 +0200
+++ b/src/HOL/Tools/hologic.ML Thu Jun 10 12:24:01 2010 +0200
@@ -289,42 +289,42 @@
(* prod *)
-fun mk_prodT (T1, T2) = Type ("*", [T1, T2]);
+fun mk_prodT (T1, T2) = Type ("Product_Type.*", [T1, T2]);
-fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2)
+fun dest_prodT (Type ("Product_Type.*", [T1, T2])) = (T1, T2)
| dest_prodT T = raise TYPE ("dest_prodT", [T], []);
-fun pair_const T1 T2 = Const ("Pair", [T1, T2] ---> mk_prodT (T1, T2));
+fun pair_const T1 T2 = Const ("Product_Type.Pair", [T1, T2] ---> mk_prodT (T1, T2));
fun mk_prod (t1, t2) =
let val T1 = fastype_of t1 and T2 = fastype_of t2 in
pair_const T1 T2 $ t1 $ t2
end;
-fun dest_prod (Const ("Pair", _) $ t1 $ t2) = (t1, t2)
+fun dest_prod (Const ("Product_Type.Pair", _) $ t1 $ t2) = (t1, t2)
| dest_prod t = raise TERM ("dest_prod", [t]);
fun mk_fst p =
let val pT = fastype_of p in
- Const ("fst", pT --> fst (dest_prodT pT)) $ p
+ Const ("Product_Type.fst", pT --> fst (dest_prodT pT)) $ p
end;
fun mk_snd p =
let val pT = fastype_of p in
- Const ("snd", pT --> snd (dest_prodT pT)) $ p
+ Const ("Product_Type.snd", pT --> snd (dest_prodT pT)) $ p
end;
fun split_const (A, B, C) =
- Const ("split", (A --> B --> C) --> mk_prodT (A, B) --> C);
+ Const ("Product_Type.split", (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 ("split", T --> mk_prodT (A, B) --> C) $ t
+ Const ("Product_Type.split", 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*)
-fun flatten_tupleT (Type ("*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
+fun flatten_tupleT (Type ("Product_Type.*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
| flatten_tupleT T = [T];
@@ -334,14 +334,14 @@
| mk_tupleT Ts = foldr1 mk_prodT Ts;
fun strip_tupleT (Type ("Product_Type.unit", [])) = []
- | strip_tupleT (Type ("*", [T1, T2])) = T1 :: strip_tupleT T2
+ | strip_tupleT (Type ("Product_Type.*", [T1, T2])) = T1 :: strip_tupleT T2
| strip_tupleT T = [T];
fun mk_tuple [] = unit
| mk_tuple ts = foldr1 mk_prod ts;
fun strip_tuple (Const ("Product_Type.Unity", _)) = []
- | strip_tuple (Const ("Pair", _) $ t1 $ t2) = t1 :: strip_tuple t2
+ | strip_tuple (Const ("Product_Type.Pair", _) $ t1 $ t2) = t1 :: strip_tuple t2
| strip_tuple t = [t];
@@ -367,14 +367,14 @@
fun strip_ptupleT ps =
let
fun factors p T = if member (op =) ps p then (case T of
- Type ("*", [T1, T2]) =>
+ Type ("Product_Type.*", [T1, T2]) =>
factors (1::p) T1 @ factors (2::p) T2
| _ => ptuple_err "strip_ptupleT") else [T]
in factors [] end;
val flat_tupleT_paths =
let
- fun factors p (Type ("*", [T1, T2])) =
+ fun factors p (Type ("Product_Type.*", [T1, T2])) =
p :: factors (1::p) T1 @ factors (2::p) T2
| factors p _ = []
in factors [] end;
@@ -383,7 +383,7 @@
let
fun mk p T ts =
if member (op =) ps p then (case T of
- Type ("*", [T1, T2]) =>
+ Type ("Product_Type.*", [T1, T2]) =>
let
val (t, ts') = mk (1::p) T1 ts;
val (u, ts'') = mk (2::p) T2 ts'
@@ -395,14 +395,14 @@
fun strip_ptuple ps =
let
fun dest p t = if member (op =) ps p then (case t of
- Const ("Pair", _) $ t $ u =>
+ Const ("Product_Type.Pair", _) $ t $ u =>
dest (1::p) t @ dest (2::p) u
| _ => ptuple_err "strip_ptuple") else [t]
in dest [] end;
val flat_tuple_paths =
let
- fun factors p (Const ("Pair", _) $ t $ u) =
+ fun factors p (Const ("Product_Type.Pair", _) $ t $ u) =
p :: factors (1::p) t @ factors (2::p) u
| factors p _ = []
in factors [] end;
@@ -414,7 +414,7 @@
let
fun ap ((p, T) :: pTs) =
if member (op =) ps p then (case T of
- Type ("*", [T1, T2]) =>
+ Type ("Product_Type.*", [T1, T2]) =>
split_const (T1, T2, map snd pTs ---> T3) $
ap ((1::p, T1) :: (2::p, T2) :: pTs)
| _ => ptuple_err "mk_psplits")
@@ -427,7 +427,7 @@
val strip_psplits =
let
fun strip [] qs Ts t = (t, rev Ts, qs)
- | strip (p :: ps) qs Ts (Const ("split", _) $ t) =
+ | strip (p :: ps) qs Ts (Const ("Product_Type.split", _) $ 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