nipkow@10213: (* Title: HOL/Product_Type.thy nipkow@10213: ID: $Id$ nipkow@10213: Author: Lawrence C Paulson, Cambridge University Computer Laboratory nipkow@10213: Copyright 1992 University of Cambridge wenzelm@11777: *) nipkow@10213: wenzelm@11777: header {* Finite products (including unit) *} nipkow@10213: oheimb@11025: theory Product_Type = Fun wenzelm@11032: files ("Product_Type_lemmas.ML") ("Tools/split_rule.ML"): nipkow@10213: nipkow@10213: wenzelm@11777: subsection {* Products *} nipkow@10213: wenzelm@11777: subsubsection {* Type definition *} nipkow@10213: nipkow@10213: constdefs oheimb@11025: Pair_Rep :: "['a, 'b] => ['a, 'b] => bool" wenzelm@11032: "Pair_Rep == (%a b. %x y. x=a & y=b)" nipkow@10213: nipkow@10213: global nipkow@10213: nipkow@10213: typedef (Prod) nipkow@10213: ('a, 'b) "*" (infixr 20) wenzelm@11032: = "{f. EX a b. f = Pair_Rep (a::'a) (b::'b)}" oheimb@11025: proof oheimb@11025: fix a b show "Pair_Rep a b : ?Prod" oheimb@11025: by blast oheimb@11025: qed nipkow@10213: nipkow@10213: syntax (symbols) oheimb@11493: "*" :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) nipkow@10213: syntax (HTML output) oheimb@11493: "*" :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) nipkow@10213: wenzelm@11777: local nipkow@10213: wenzelm@11777: wenzelm@11777: subsubsection {* Abstract constants and syntax *} wenzelm@11777: wenzelm@11777: global nipkow@10213: nipkow@10213: consts oheimb@11025: fst :: "'a * 'b => 'a" oheimb@11025: snd :: "'a * 'b => 'b" oheimb@11025: split :: "[['a, 'b] => 'c, 'a * 'b] => 'c" oheimb@11025: prod_fun :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd" oheimb@11025: Pair :: "['a, 'b] => 'a * 'b" oheimb@11025: Sigma :: "['a set, 'a => 'b set] => ('a * 'b) set" nipkow@10213: wenzelm@11777: local nipkow@10213: wenzelm@11777: text {* wenzelm@11777: Patterns -- extends pre-defined type @{typ pttrn} used in wenzelm@11777: abstractions. wenzelm@11777: *} nipkow@10213: nipkow@10213: nonterminals nipkow@10213: tuple_args patterns nipkow@10213: nipkow@10213: syntax nipkow@10213: "_tuple" :: "'a => tuple_args => 'a * 'b" ("(1'(_,/ _'))") nipkow@10213: "_tuple_arg" :: "'a => tuple_args" ("_") nipkow@10213: "_tuple_args" :: "'a => tuple_args => tuple_args" ("_,/ _") oheimb@11025: "_pattern" :: "[pttrn, patterns] => pttrn" ("'(_,/ _')") oheimb@11025: "" :: "pttrn => patterns" ("_") oheimb@11025: "_patterns" :: "[pttrn, patterns] => patterns" ("_,/ _") oheimb@11025: "@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10) oheimb@11025: "@Times" ::"['a set, 'a => 'b set] => ('a * 'b) set" (infixr "<*>" 80) nipkow@10213: nipkow@10213: translations nipkow@10213: "(x, y)" == "Pair x y" nipkow@10213: "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))" nipkow@10213: "%(x,y,zs).b" == "split(%x (y,zs).b)" nipkow@10213: "%(x,y).b" == "split(%x y. b)" nipkow@10213: "_abs (Pair x y) t" => "%(x,y).t" nipkow@10213: (* The last rule accommodates tuples in `case C ... (x,y) ... => ...' nipkow@10213: The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *) nipkow@10213: nipkow@10213: "SIGMA x:A. B" => "Sigma A (%x. B)" nipkow@10213: "A <*> B" => "Sigma A (_K B)" nipkow@10213: nipkow@10213: syntax (symbols) oheimb@11493: "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\ _\_./ _)" 10) oheimb@11493: "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \ _" [81, 80] 80) oheimb@11025: wenzelm@11032: print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *} nipkow@10213: nipkow@10213: wenzelm@11777: subsubsection {* Definitions *} nipkow@10213: nipkow@10213: defs oheimb@11025: Pair_def: "Pair a b == Abs_Prod(Pair_Rep a b)" paulson@11451: fst_def: "fst p == THE a. EX b. p = (a, b)" paulson@11451: snd_def: "snd p == THE b. EX a. p = (a, b)" oheimb@11025: split_def: "split == (%c p. c (fst p) (snd p))" oheimb@11025: prod_fun_def: "prod_fun f g == split(%x y.(f(x), g(y)))" oheimb@11025: Sigma_def: "Sigma A B == UN x:A. UN y:B(x). {(x, y)}" nipkow@10213: nipkow@10213: wenzelm@11777: subsection {* Unit *} nipkow@10213: wenzelm@11032: typedef unit = "{True}" oheimb@11025: proof oheimb@11025: show "True : ?unit" oheimb@11025: by blast oheimb@11025: qed nipkow@10213: wenzelm@11602: constdefs wenzelm@11602: Unity :: unit ("'(')") wenzelm@11602: "() == Abs_unit True" oheimb@11025: wenzelm@11032: wenzelm@11777: subsection {* Lemmas and tool setup *} wenzelm@11032: oheimb@11025: use "Product_Type_lemmas.ML" oheimb@11025: wenzelm@11820: lemma (*split_paired_all:*) "(!!x. PROP P x) == (!!a b. PROP P (a, b))" (* FIXME unused *) wenzelm@11820: proof wenzelm@11820: fix a b wenzelm@11820: assume "!!x. PROP P x" wenzelm@11820: thus "PROP P (a, b)" . wenzelm@11820: next wenzelm@11820: fix x wenzelm@11820: assume "!!a b. PROP P (a, b)" wenzelm@11820: hence "PROP P (fst x, snd x)" . wenzelm@11820: thus "PROP P x" by simp wenzelm@11820: qed wenzelm@11820: oheimb@11493: lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A" wenzelm@11777: apply (rule_tac x = "(a, b)" in image_eqI) wenzelm@11777: apply auto wenzelm@11777: done wenzelm@11777: oheimb@11493: wenzelm@11032: constdefs wenzelm@11425: internal_split :: "('a => 'b => 'c) => 'a * 'b => 'c" wenzelm@11032: "internal_split == split" wenzelm@11032: wenzelm@11032: lemma internal_split_conv: "internal_split c (a, b) = c a b" wenzelm@11032: by (simp only: internal_split_def split_conv) wenzelm@11032: wenzelm@11032: hide const internal_split wenzelm@11032: oheimb@11025: use "Tools/split_rule.ML" wenzelm@11032: setup SplitRule.setup nipkow@10213: nipkow@10213: end