src/HOL/Prod.thy
 author wenzelm Wed Nov 27 16:51:15 1996 +0100 (1996-11-27) changeset 2260 b59781f2b809 parent 1765 5db6b3ea0e28 child 2393 651fce76c86c permissions -rw-r--r--
 clasohm@923 ` 1` ```(* Title: HOL/Prod.thy ``` clasohm@923 ` 2` ``` ID: Prod.thy,v 1.5 1994/08/19 09:04:27 lcp Exp ``` clasohm@923 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@923 ` 4` ``` Copyright 1992 University of Cambridge ``` clasohm@923 ` 5` clasohm@923 ` 6` ```Ordered Pairs and the Cartesian product type. ``` clasohm@923 ` 7` ```The unit type. ``` clasohm@923 ` 8` ```*) ``` clasohm@923 ` 9` berghofe@1755 ` 10` ```Prod = Fun + equalities + ``` clasohm@923 ` 11` wenzelm@2260 ` 12` wenzelm@2260 ` 13` ```(** products **) ``` clasohm@923 ` 14` clasohm@923 ` 15` ```(* type definition *) ``` clasohm@923 ` 16` clasohm@1558 ` 17` ```constdefs ``` clasohm@1370 ` 18` ``` Pair_Rep :: ['a, 'b] => ['a, 'b] => bool ``` clasohm@1558 ` 19` ``` "Pair_Rep == (%a b. %x y. x=a & y=b)" ``` clasohm@923 ` 20` clasohm@1475 ` 21` ```typedef (Prod) ``` clasohm@923 ` 22` ``` ('a, 'b) "*" (infixr 20) ``` clasohm@923 ` 23` ``` = "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}" ``` clasohm@923 ` 24` wenzelm@2260 ` 25` ```syntax (symbols) ``` wenzelm@2260 ` 26` ``` "*" :: [type, type] => type ("(_ \\/ _)" [21, 20] 20) ``` wenzelm@2260 ` 27` clasohm@923 ` 28` clasohm@923 ` 29` ```(* abstract constants and syntax *) ``` clasohm@923 ` 30` clasohm@923 ` 31` ```consts ``` clasohm@923 ` 32` ``` fst :: "'a * 'b => 'a" ``` clasohm@923 ` 33` ``` snd :: "'a * 'b => 'b" ``` clasohm@923 ` 34` ``` split :: "[['a, 'b] => 'c, 'a * 'b] => 'c" ``` clasohm@923 ` 35` ``` prod_fun :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd" ``` clasohm@923 ` 36` ``` Pair :: "['a, 'b] => 'a * 'b" ``` clasohm@923 ` 37` ``` Sigma :: "['a set, 'a => 'b set] => ('a * 'b) set" ``` clasohm@923 ` 38` wenzelm@2260 ` 39` wenzelm@2260 ` 40` ```(* patterns -- extends pre-defined type "pttrn" used in abstractions *) ``` wenzelm@2260 ` 41` nipkow@1068 ` 42` ```types pttrns ``` nipkow@1068 ` 43` clasohm@923 ` 44` ```syntax ``` wenzelm@2260 ` 45` ``` "@Tuple" :: "['a, args] => 'a * 'b" ("(1'(_,/ _'))") ``` clasohm@923 ` 46` wenzelm@2260 ` 47` ``` "@pttrn" :: [pttrn, pttrns] => pttrn ("'(_,/_')") ``` wenzelm@2260 ` 48` ``` "" :: pttrn => pttrns ("_") ``` wenzelm@2260 ` 49` ``` "@pttrns" :: [pttrn, pttrns] => pttrns ("_,/_") ``` nipkow@1068 ` 50` wenzelm@2260 ` 51` ``` "@Sigma" :: "[idt, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10) ``` wenzelm@2260 ` 52` ``` "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ Times _" [81, 80] 80) ``` nipkow@1636 ` 53` clasohm@923 ` 54` ```translations ``` clasohm@972 ` 55` ``` "(x, y, z)" == "(x, (y, z))" ``` clasohm@972 ` 56` ``` "(x, y)" == "Pair x y" ``` clasohm@923 ` 57` wenzelm@2260 ` 58` ``` "%(x,y,zs).b" == "split(%x (y,zs).b)" ``` wenzelm@2260 ` 59` ``` "%(x,y).b" == "split(%x y.b)" ``` wenzelm@2260 ` 60` wenzelm@2260 ` 61` ``` "SIGMA x:A.B" => "Sigma A (%x.B)" ``` wenzelm@2260 ` 62` ``` "A Times B" => "Sigma A (_K B)" ``` nipkow@1068 ` 63` wenzelm@2260 ` 64` ```syntax (symbols) ``` wenzelm@2260 ` 65` ``` "@Sigma" :: "[idt, 'a set, 'b set] => ('a * 'b) set" ("(3\\ _\\_./ _)" 10) ``` wenzelm@2260 ` 66` ``` "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \\ _" [81, 80] 80) ``` wenzelm@2260 ` 67` wenzelm@2260 ` 68` wenzelm@2260 ` 69` ```(* definitions *) ``` nipkow@1636 ` 70` clasohm@923 ` 71` ```defs ``` clasohm@923 ` 72` ``` Pair_def "Pair a b == Abs_Prod(Pair_Rep a b)" ``` clasohm@972 ` 73` ``` fst_def "fst(p) == @a. ? b. p = (a, b)" ``` clasohm@972 ` 74` ``` snd_def "snd(p) == @b. ? a. p = (a, b)" ``` nipkow@1655 ` 75` ``` split_def "split == (%c p. c (fst p) (snd p))" ``` clasohm@972 ` 76` ``` prod_fun_def "prod_fun f g == split(%x y.(f(x), g(y)))" ``` clasohm@972 ` 77` ``` Sigma_def "Sigma A B == UN x:A. UN y:B(x). {(x, y)}" ``` clasohm@923 ` 78` wenzelm@2260 ` 79` wenzelm@2260 ` 80` wenzelm@2260 ` 81` ```(** unit **) ``` clasohm@923 ` 82` clasohm@1475 ` 83` ```typedef (Unit) ``` clasohm@923 ` 84` ``` unit = "{p. p = True}" ``` clasohm@923 ` 85` clasohm@923 ` 86` ```consts ``` clasohm@1370 ` 87` ``` "()" :: unit ("'(')") ``` clasohm@923 ` 88` clasohm@923 ` 89` ```defs ``` clasohm@972 ` 90` ``` Unity_def "() == Abs_Unit(True)" ``` clasohm@923 ` 91` regensbu@1273 ` 92` ```(* start 8bit 1 *) ``` regensbu@1273 ` 93` ```(* end 8bit 1 *) ``` regensbu@1273 ` 94` clasohm@923 ` 95` ```end ``` nipkow@1636 ` 96` nipkow@1636 ` 97` ```ML ``` nipkow@1636 ` 98` nipkow@1636 ` 99` ```val print_translation = [("Sigma", dependent_tr' ("@Sigma", "@Times"))]; ```