src/HOL/Prod.thy
 author nipkow Mon Oct 21 09:50:50 1996 +0200 (1996-10-21) changeset 2115 9709f9188549 parent 1765 5db6b3ea0e28 child 2260 b59781f2b809 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` clasohm@923 ` 12` ```(** Products **) ``` clasohm@923 ` 13` clasohm@923 ` 14` ```(* type definition *) ``` clasohm@923 ` 15` clasohm@1558 ` 16` ```constdefs ``` clasohm@1370 ` 17` ``` Pair_Rep :: ['a, 'b] => ['a, 'b] => bool ``` clasohm@1558 ` 18` ``` "Pair_Rep == (%a b. %x y. x=a & y=b)" ``` clasohm@923 ` 19` clasohm@1475 ` 20` ```typedef (Prod) ``` clasohm@923 ` 21` ``` ('a, 'b) "*" (infixr 20) ``` clasohm@923 ` 22` ``` = "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}" ``` clasohm@923 ` 23` clasohm@923 ` 24` clasohm@923 ` 25` ```(* abstract constants and syntax *) ``` clasohm@923 ` 26` clasohm@923 ` 27` ```consts ``` clasohm@923 ` 28` ``` fst :: "'a * 'b => 'a" ``` clasohm@923 ` 29` ``` snd :: "'a * 'b => 'b" ``` clasohm@923 ` 30` ``` split :: "[['a, 'b] => 'c, 'a * 'b] => 'c" ``` clasohm@923 ` 31` ``` prod_fun :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd" ``` clasohm@923 ` 32` ``` Pair :: "['a, 'b] => 'a * 'b" ``` clasohm@923 ` 33` ``` Sigma :: "['a set, 'a => 'b set] => ('a * 'b) set" ``` clasohm@923 ` 34` nipkow@1068 ` 35` ```(** Patterns -- extends pre-defined type "pttrn" used in abstractions **) ``` nipkow@1068 ` 36` ```types pttrns ``` nipkow@1068 ` 37` clasohm@923 ` 38` ```syntax ``` clasohm@972 ` 39` ``` "@Tuple" :: "['a, args] => 'a * 'b" ("(1'(_,/ _'))") ``` clasohm@923 ` 40` clasohm@1370 ` 41` ``` "@pttrn" :: [pttrn,pttrns] => pttrn ("'(_,/_')") ``` clasohm@1370 ` 42` ``` "" :: pttrn => pttrns ("_") ``` clasohm@1370 ` 43` ``` "@pttrns" :: [pttrn,pttrns] => pttrns ("_,/_") ``` nipkow@1068 ` 44` nipkow@1636 ` 45` ``` "@Sigma" :: "[idt,'a set,'b set] => ('a * 'b)set" ``` nipkow@1636 ` 46` ``` ("(3SIGMA _:_./ _)" 10) ``` nipkow@1636 ` 47` ``` "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ``` nipkow@1636 ` 48` ``` ("_ Times _" [81,80] 80) ``` nipkow@1636 ` 49` clasohm@923 ` 50` ```translations ``` clasohm@972 ` 51` ``` "(x, y, z)" == "(x, (y, z))" ``` clasohm@972 ` 52` ``` "(x, y)" == "Pair x y" ``` clasohm@923 ` 53` nipkow@1114 ` 54` ``` "%(x,y,zs).b" == "split(%x (y,zs).b)" ``` nipkow@1114 ` 55` ``` "%(x,y).b" == "split(%x y.b)" ``` nipkow@1068 ` 56` nipkow@1636 ` 57` ``` "SIGMA x:A. B" => "Sigma A (%x.B)" ``` nipkow@1636 ` 58` ``` "A Times B" => "Sigma A (_K B)" ``` nipkow@1636 ` 59` clasohm@923 ` 60` ```defs ``` clasohm@923 ` 61` ``` Pair_def "Pair a b == Abs_Prod(Pair_Rep a b)" ``` clasohm@972 ` 62` ``` fst_def "fst(p) == @a. ? b. p = (a, b)" ``` clasohm@972 ` 63` ``` snd_def "snd(p) == @b. ? a. p = (a, b)" ``` nipkow@1655 ` 64` ``` split_def "split == (%c p. c (fst p) (snd p))" ``` clasohm@972 ` 65` ``` prod_fun_def "prod_fun f g == split(%x y.(f(x), g(y)))" ``` clasohm@972 ` 66` ``` Sigma_def "Sigma A B == UN x:A. UN y:B(x). {(x, y)}" ``` clasohm@923 ` 67` clasohm@923 ` 68` ```(** Unit **) ``` clasohm@923 ` 69` clasohm@1475 ` 70` ```typedef (Unit) ``` clasohm@923 ` 71` ``` unit = "{p. p = True}" ``` clasohm@923 ` 72` clasohm@923 ` 73` ```consts ``` clasohm@1370 ` 74` ``` "()" :: unit ("'(')") ``` clasohm@923 ` 75` clasohm@923 ` 76` ```defs ``` clasohm@972 ` 77` ``` Unity_def "() == Abs_Unit(True)" ``` clasohm@923 ` 78` regensbu@1273 ` 79` ```(* start 8bit 1 *) ``` regensbu@1273 ` 80` ```(* end 8bit 1 *) ``` regensbu@1273 ` 81` clasohm@923 ` 82` ```end ``` nipkow@1636 ` 83` nipkow@1636 ` 84` ```ML ``` nipkow@1636 ` 85` nipkow@1636 ` 86` ```val print_translation = [("Sigma", dependent_tr' ("@Sigma", "@Times"))]; ```