src/HOL/Product_Type.thy
changeset 37389 09467cdfa198
parent 37387 3581483cca6c
child 37411 c88c44156083
     1.1 --- a/src/HOL/Product_Type.thy	Tue Jun 08 16:37:22 2010 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Jun 10 12:24:01 2010 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  imports Typedef Inductive Fun
     1.5  uses
     1.6    ("Tools/split_rule.ML")
     1.7 +  ("Tools/inductive_codegen.ML")
     1.8    ("Tools/inductive_set.ML")
     1.9  begin
    1.10  
    1.11 @@ -128,13 +129,10 @@
    1.12  definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
    1.13    "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
    1.14  
    1.15 -global
    1.16 -
    1.17 -typedef (Prod)
    1.18 -  ('a, 'b) "*"    (infixr "*" 20)
    1.19 -    = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
    1.20 +typedef (prod) ('a, 'b) "*" (infixr "*" 20)
    1.21 +  = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
    1.22  proof
    1.23 -  fix a b show "Pair_Rep a b \<in> ?Prod"
    1.24 +  fix a b show "Pair_Rep a b \<in> ?prod"
    1.25      by rule+
    1.26  qed
    1.27  
    1.28 @@ -143,35 +141,27 @@
    1.29  type_notation (HTML output)
    1.30    "*"  ("(_ \<times>/ _)" [21, 20] 20)
    1.31  
    1.32 -consts
    1.33 -  Pair     :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b"
    1.34 -
    1.35 -local
    1.36 -
    1.37 -defs
    1.38 -  Pair_def:     "Pair a b == Abs_Prod (Pair_Rep a b)"
    1.39 +definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where
    1.40 +  "Pair a b = Abs_prod (Pair_Rep a b)"
    1.41  
    1.42  rep_datatype (prod) Pair proof -
    1.43    fix P :: "'a \<times> 'b \<Rightarrow> bool" and p
    1.44    assume "\<And>a b. P (Pair a b)"
    1.45 -  then show "P p" by (cases p) (auto simp add: Prod_def Pair_def Pair_Rep_def)
    1.46 +  then show "P p" by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
    1.47  next
    1.48    fix a c :: 'a and b d :: 'b
    1.49    have "Pair_Rep a b = Pair_Rep c d \<longleftrightarrow> a = c \<and> b = d"
    1.50      by (auto simp add: Pair_Rep_def expand_fun_eq)
    1.51 -  moreover have "Pair_Rep a b \<in> Prod" and "Pair_Rep c d \<in> Prod"
    1.52 -    by (auto simp add: Prod_def)
    1.53 +  moreover have "Pair_Rep a b \<in> prod" and "Pair_Rep c d \<in> prod"
    1.54 +    by (auto simp add: prod_def)
    1.55    ultimately show "Pair a b = Pair c d \<longleftrightarrow> a = c \<and> b = d"
    1.56 -    by (simp add: Pair_def Abs_Prod_inject)
    1.57 +    by (simp add: Pair_def Abs_prod_inject)
    1.58  qed
    1.59  
    1.60  
    1.61  subsubsection {* Tuple syntax *}
    1.62  
    1.63 -global consts
    1.64 -  split    :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"
    1.65 -
    1.66 -local defs
    1.67 +definition split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
    1.68    split_prod_case: "split == prod_case"
    1.69  
    1.70  text {*
    1.71 @@ -393,13 +383,11 @@
    1.72  lemma surj_pair [simp]: "EX x y. p = (x, y)"
    1.73    by (cases p) simp
    1.74  
    1.75 -global consts
    1.76 -  fst      :: "'a \<times> 'b \<Rightarrow> 'a"
    1.77 -  snd      :: "'a \<times> 'b \<Rightarrow> 'b"
    1.78 +definition fst :: "'a \<times> 'b \<Rightarrow> 'a" where
    1.79 +  "fst p = (case p of (a, b) \<Rightarrow> a)"
    1.80  
    1.81 -local defs
    1.82 -  fst_def:      "fst p == case p of (a, b) \<Rightarrow> a"
    1.83 -  snd_def:      "snd p == case p of (a, b) \<Rightarrow> b"
    1.84 +definition snd :: "'a \<times> 'b \<Rightarrow> 'b" where
    1.85 +  "snd p = (case p of (a, b) \<Rightarrow> b)"
    1.86  
    1.87  lemma fst_conv [simp, code]: "fst (a, b) = a"
    1.88    unfolding fst_def by simp
    1.89 @@ -1189,6 +1177,9 @@
    1.90  
    1.91  subsection {* Inductively defined sets *}
    1.92  
    1.93 +use "Tools/inductive_codegen.ML"
    1.94 +setup Inductive_Codegen.setup
    1.95 +
    1.96  use "Tools/inductive_set.ML"
    1.97  setup Inductive_Set.setup
    1.98