# HG changeset patch
# User haftmann
# Date 1276165441 -7200
# Node ID 09467cdfa1985512cdc334572d022033c93794b9
# Parent  793618618f7800674f8f6c4900ad7fb5c36c6ca9
qualified type "*"; qualified constants Pair, fst, snd, split

diff -r 793618618f78 -r 09467cdfa198 NEWS
--- a/NEWS	Tue Jun 08 16:37:22 2010 +0200
+++ b/NEWS	Thu Jun 10 12:24:01 2010 +0200
@@ -10,12 +10,17 @@
 
   types
     nat ~> Nat.nat
+    * ~> Product_Type,*
     + ~> Sum_Type.+
 
   constants
     Ball ~> Set.Ball
     Bex ~> Set.Bex
     Suc ~> Nat.Suc
+    Pair ~> Product_Type.Pair
+    fst ~> Product_Type.fst
+    snd ~> Product_Type.snd
+    split ~> Product_Type.split
     curry ~> Product_Type.curry
 
 INCOMPATIBILITY.
diff -r 793618618f78 -r 09467cdfa198 src/HOL/Product_Type.thy
--- 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
 
diff -r 793618618f78 -r 09467cdfa198 src/HOL/Tools/hologic.ML
--- 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