qualified type "*"; qualified constants Pair, fst, snd, split
authorhaftmann
Thu Jun 10 12:24:01 2010 +0200 (2010-06-10)
changeset 3738909467cdfa198
parent 37388 793618618f78
child 37390 8781d80026fc
qualified type "*"; qualified constants Pair, fst, snd, split
NEWS
src/HOL/Product_Type.thy
src/HOL/Tools/hologic.ML
     1.1 --- a/NEWS	Tue Jun 08 16:37:22 2010 +0200
     1.2 +++ b/NEWS	Thu Jun 10 12:24:01 2010 +0200
     1.3 @@ -10,12 +10,17 @@
     1.4  
     1.5    types
     1.6      nat ~> Nat.nat
     1.7 +    * ~> Product_Type,*
     1.8      + ~> Sum_Type.+
     1.9  
    1.10    constants
    1.11      Ball ~> Set.Ball
    1.12      Bex ~> Set.Bex
    1.13      Suc ~> Nat.Suc
    1.14 +    Pair ~> Product_Type.Pair
    1.15 +    fst ~> Product_Type.fst
    1.16 +    snd ~> Product_Type.snd
    1.17 +    split ~> Product_Type.split
    1.18      curry ~> Product_Type.curry
    1.19  
    1.20  INCOMPATIBILITY.
     2.1 --- a/src/HOL/Product_Type.thy	Tue Jun 08 16:37:22 2010 +0200
     2.2 +++ b/src/HOL/Product_Type.thy	Thu Jun 10 12:24:01 2010 +0200
     2.3 @@ -9,6 +9,7 @@
     2.4  imports Typedef Inductive Fun
     2.5  uses
     2.6    ("Tools/split_rule.ML")
     2.7 +  ("Tools/inductive_codegen.ML")
     2.8    ("Tools/inductive_set.ML")
     2.9  begin
    2.10  
    2.11 @@ -128,13 +129,10 @@
    2.12  definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
    2.13    "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
    2.14  
    2.15 -global
    2.16 -
    2.17 -typedef (Prod)
    2.18 -  ('a, 'b) "*"    (infixr "*" 20)
    2.19 -    = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
    2.20 +typedef (prod) ('a, 'b) "*" (infixr "*" 20)
    2.21 +  = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
    2.22  proof
    2.23 -  fix a b show "Pair_Rep a b \<in> ?Prod"
    2.24 +  fix a b show "Pair_Rep a b \<in> ?prod"
    2.25      by rule+
    2.26  qed
    2.27  
    2.28 @@ -143,35 +141,27 @@
    2.29  type_notation (HTML output)
    2.30    "*"  ("(_ \<times>/ _)" [21, 20] 20)
    2.31  
    2.32 -consts
    2.33 -  Pair     :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b"
    2.34 -
    2.35 -local
    2.36 -
    2.37 -defs
    2.38 -  Pair_def:     "Pair a b == Abs_Prod (Pair_Rep a b)"
    2.39 +definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where
    2.40 +  "Pair a b = Abs_prod (Pair_Rep a b)"
    2.41  
    2.42  rep_datatype (prod) Pair proof -
    2.43    fix P :: "'a \<times> 'b \<Rightarrow> bool" and p
    2.44    assume "\<And>a b. P (Pair a b)"
    2.45 -  then show "P p" by (cases p) (auto simp add: Prod_def Pair_def Pair_Rep_def)
    2.46 +  then show "P p" by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
    2.47  next
    2.48    fix a c :: 'a and b d :: 'b
    2.49    have "Pair_Rep a b = Pair_Rep c d \<longleftrightarrow> a = c \<and> b = d"
    2.50      by (auto simp add: Pair_Rep_def expand_fun_eq)
    2.51 -  moreover have "Pair_Rep a b \<in> Prod" and "Pair_Rep c d \<in> Prod"
    2.52 -    by (auto simp add: Prod_def)
    2.53 +  moreover have "Pair_Rep a b \<in> prod" and "Pair_Rep c d \<in> prod"
    2.54 +    by (auto simp add: prod_def)
    2.55    ultimately show "Pair a b = Pair c d \<longleftrightarrow> a = c \<and> b = d"
    2.56 -    by (simp add: Pair_def Abs_Prod_inject)
    2.57 +    by (simp add: Pair_def Abs_prod_inject)
    2.58  qed
    2.59  
    2.60  
    2.61  subsubsection {* Tuple syntax *}
    2.62  
    2.63 -global consts
    2.64 -  split    :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"
    2.65 -
    2.66 -local defs
    2.67 +definition split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
    2.68    split_prod_case: "split == prod_case"
    2.69  
    2.70  text {*
    2.71 @@ -393,13 +383,11 @@
    2.72  lemma surj_pair [simp]: "EX x y. p = (x, y)"
    2.73    by (cases p) simp
    2.74  
    2.75 -global consts
    2.76 -  fst      :: "'a \<times> 'b \<Rightarrow> 'a"
    2.77 -  snd      :: "'a \<times> 'b \<Rightarrow> 'b"
    2.78 +definition fst :: "'a \<times> 'b \<Rightarrow> 'a" where
    2.79 +  "fst p = (case p of (a, b) \<Rightarrow> a)"
    2.80  
    2.81 -local defs
    2.82 -  fst_def:      "fst p == case p of (a, b) \<Rightarrow> a"
    2.83 -  snd_def:      "snd p == case p of (a, b) \<Rightarrow> b"
    2.84 +definition snd :: "'a \<times> 'b \<Rightarrow> 'b" where
    2.85 +  "snd p = (case p of (a, b) \<Rightarrow> b)"
    2.86  
    2.87  lemma fst_conv [simp, code]: "fst (a, b) = a"
    2.88    unfolding fst_def by simp
    2.89 @@ -1189,6 +1177,9 @@
    2.90  
    2.91  subsection {* Inductively defined sets *}
    2.92  
    2.93 +use "Tools/inductive_codegen.ML"
    2.94 +setup Inductive_Codegen.setup
    2.95 +
    2.96  use "Tools/inductive_set.ML"
    2.97  setup Inductive_Set.setup
    2.98  
     3.1 --- a/src/HOL/Tools/hologic.ML	Tue Jun 08 16:37:22 2010 +0200
     3.2 +++ b/src/HOL/Tools/hologic.ML	Thu Jun 10 12:24:01 2010 +0200
     3.3 @@ -289,42 +289,42 @@
     3.4  
     3.5  (* prod *)
     3.6  
     3.7 -fun mk_prodT (T1, T2) = Type ("*", [T1, T2]);
     3.8 +fun mk_prodT (T1, T2) = Type ("Product_Type.*", [T1, T2]);
     3.9  
    3.10 -fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2)
    3.11 +fun dest_prodT (Type ("Product_Type.*", [T1, T2])) = (T1, T2)
    3.12    | dest_prodT T = raise TYPE ("dest_prodT", [T], []);
    3.13  
    3.14 -fun pair_const T1 T2 = Const ("Pair", [T1, T2] ---> mk_prodT (T1, T2));
    3.15 +fun pair_const T1 T2 = Const ("Product_Type.Pair", [T1, T2] ---> mk_prodT (T1, T2));
    3.16  
    3.17  fun mk_prod (t1, t2) =
    3.18    let val T1 = fastype_of t1 and T2 = fastype_of t2 in
    3.19      pair_const T1 T2 $ t1 $ t2
    3.20    end;
    3.21  
    3.22 -fun dest_prod (Const ("Pair", _) $ t1 $ t2) = (t1, t2)
    3.23 +fun dest_prod (Const ("Product_Type.Pair", _) $ t1 $ t2) = (t1, t2)
    3.24    | dest_prod t = raise TERM ("dest_prod", [t]);
    3.25  
    3.26  fun mk_fst p =
    3.27    let val pT = fastype_of p in
    3.28 -    Const ("fst", pT --> fst (dest_prodT pT)) $ p
    3.29 +    Const ("Product_Type.fst", pT --> fst (dest_prodT pT)) $ p
    3.30    end;
    3.31  
    3.32  fun mk_snd p =
    3.33    let val pT = fastype_of p in
    3.34 -    Const ("snd", pT --> snd (dest_prodT pT)) $ p
    3.35 +    Const ("Product_Type.snd", pT --> snd (dest_prodT pT)) $ p
    3.36    end;
    3.37  
    3.38  fun split_const (A, B, C) =
    3.39 -  Const ("split", (A --> B --> C) --> mk_prodT (A, B) --> C);
    3.40 +  Const ("Product_Type.split", (A --> B --> C) --> mk_prodT (A, B) --> C);
    3.41  
    3.42  fun mk_split t =
    3.43    (case Term.fastype_of t of
    3.44      T as (Type ("fun", [A, Type ("fun", [B, C])])) =>
    3.45 -      Const ("split", T --> mk_prodT (A, B) --> C) $ t
    3.46 +      Const ("Product_Type.split", T --> mk_prodT (A, B) --> C) $ t
    3.47    | _ => raise TERM ("mk_split: bad body type", [t]));
    3.48  
    3.49  (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
    3.50 -fun flatten_tupleT (Type ("*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
    3.51 +fun flatten_tupleT (Type ("Product_Type.*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
    3.52    | flatten_tupleT T = [T];
    3.53  
    3.54  
    3.55 @@ -334,14 +334,14 @@
    3.56    | mk_tupleT Ts = foldr1 mk_prodT Ts;
    3.57  
    3.58  fun strip_tupleT (Type ("Product_Type.unit", [])) = []
    3.59 -  | strip_tupleT (Type ("*", [T1, T2])) = T1 :: strip_tupleT T2
    3.60 +  | strip_tupleT (Type ("Product_Type.*", [T1, T2])) = T1 :: strip_tupleT T2
    3.61    | strip_tupleT T = [T];
    3.62  
    3.63  fun mk_tuple [] = unit
    3.64    | mk_tuple ts = foldr1 mk_prod ts;
    3.65  
    3.66  fun strip_tuple (Const ("Product_Type.Unity", _)) = []
    3.67 -  | strip_tuple (Const ("Pair", _) $ t1 $ t2) = t1 :: strip_tuple t2
    3.68 +  | strip_tuple (Const ("Product_Type.Pair", _) $ t1 $ t2) = t1 :: strip_tuple t2
    3.69    | strip_tuple t = [t];
    3.70  
    3.71  
    3.72 @@ -367,14 +367,14 @@
    3.73  fun strip_ptupleT ps =
    3.74    let
    3.75      fun factors p T = if member (op =) ps p then (case T of
    3.76 -        Type ("*", [T1, T2]) =>
    3.77 +        Type ("Product_Type.*", [T1, T2]) =>
    3.78            factors (1::p) T1 @ factors (2::p) T2
    3.79        | _ => ptuple_err "strip_ptupleT") else [T]
    3.80    in factors [] end;
    3.81  
    3.82  val flat_tupleT_paths =
    3.83    let
    3.84 -    fun factors p (Type ("*", [T1, T2])) =
    3.85 +    fun factors p (Type ("Product_Type.*", [T1, T2])) =
    3.86            p :: factors (1::p) T1 @ factors (2::p) T2
    3.87        | factors p _ = []
    3.88    in factors [] end;
    3.89 @@ -383,7 +383,7 @@
    3.90    let
    3.91      fun mk p T ts =
    3.92        if member (op =) ps p then (case T of
    3.93 -          Type ("*", [T1, T2]) =>
    3.94 +          Type ("Product_Type.*", [T1, T2]) =>
    3.95              let
    3.96                val (t, ts') = mk (1::p) T1 ts;
    3.97                val (u, ts'') = mk (2::p) T2 ts'
    3.98 @@ -395,14 +395,14 @@
    3.99  fun strip_ptuple ps =
   3.100    let
   3.101      fun dest p t = if member (op =) ps p then (case t of
   3.102 -        Const ("Pair", _) $ t $ u =>
   3.103 +        Const ("Product_Type.Pair", _) $ t $ u =>
   3.104            dest (1::p) t @ dest (2::p) u
   3.105        | _ => ptuple_err "strip_ptuple") else [t]
   3.106    in dest [] end;
   3.107  
   3.108  val flat_tuple_paths =
   3.109    let
   3.110 -    fun factors p (Const ("Pair", _) $ t $ u) =
   3.111 +    fun factors p (Const ("Product_Type.Pair", _) $ t $ u) =
   3.112            p :: factors (1::p) t @ factors (2::p) u
   3.113        | factors p _ = []
   3.114    in factors [] end;
   3.115 @@ -414,7 +414,7 @@
   3.116    let
   3.117      fun ap ((p, T) :: pTs) =
   3.118            if member (op =) ps p then (case T of
   3.119 -              Type ("*", [T1, T2]) =>
   3.120 +              Type ("Product_Type.*", [T1, T2]) =>
   3.121                  split_const (T1, T2, map snd pTs ---> T3) $
   3.122                    ap ((1::p, T1) :: (2::p, T2) :: pTs)
   3.123              | _ => ptuple_err "mk_psplits")
   3.124 @@ -427,7 +427,7 @@
   3.125  val strip_psplits =
   3.126    let
   3.127      fun strip [] qs Ts t = (t, rev Ts, qs)
   3.128 -      | strip (p :: ps) qs Ts (Const ("split", _) $ t) =
   3.129 +      | strip (p :: ps) qs Ts (Const ("Product_Type.split", _) $ t) =
   3.130            strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
   3.131        | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
   3.132        | strip (p :: ps) qs Ts t = strip ps qs