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 \ 'b \ 'a \ 'b \ bool" where "Pair_Rep a b = (\x y. x = a \ y = b)" -global - -typedef (Prod) - ('a, 'b) "*" (infixr "*" 20) - = "{f. \a b. f = Pair_Rep (a\'a) (b\'b)}" +typedef (prod) ('a, 'b) "*" (infixr "*" 20) + = "{f. \a b. f = Pair_Rep (a\'a) (b\'b)}" proof - fix a b show "Pair_Rep a b \ ?Prod" + fix a b show "Pair_Rep a b \ ?prod" by rule+ qed @@ -143,35 +141,27 @@ type_notation (HTML output) "*" ("(_ \/ _)" [21, 20] 20) -consts - Pair :: "'a \ 'b \ 'a \ 'b" - -local - -defs - Pair_def: "Pair a b == Abs_Prod (Pair_Rep a b)" +definition Pair :: "'a \ 'b \ 'a \ 'b" where + "Pair a b = Abs_prod (Pair_Rep a b)" rep_datatype (prod) Pair proof - fix P :: "'a \ 'b \ bool" and p assume "\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 \ a = c \ b = d" by (auto simp add: Pair_Rep_def expand_fun_eq) - moreover have "Pair_Rep a b \ Prod" and "Pair_Rep c d \ Prod" - by (auto simp add: Prod_def) + moreover have "Pair_Rep a b \ prod" and "Pair_Rep c d \ prod" + by (auto simp add: prod_def) ultimately show "Pair a b = Pair c d \ a = c \ 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 \ 'b \ 'c) \ 'a \ 'b \ 'c" - -local defs +definition split :: "('a \ 'b \ 'c) \ 'a \ 'b \ '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 \ 'b \ 'a" - snd :: "'a \ 'b \ 'b" +definition fst :: "'a \ 'b \ 'a" where + "fst p = (case p of (a, b) \ a)" -local defs - fst_def: "fst p == case p of (a, b) \ a" - snd_def: "snd p == case p of (a, b) \ b" +definition snd :: "'a \ 'b \ 'b" where + "snd p = (case p of (a, b) \ 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