src/HOL/Prod.thy
 author berghofe Tue May 21 13:42:53 1996 +0200 (1996-05-21) changeset 1755 17001ecd546e parent 1674 33aff4d854e4 child 1765 5db6b3ea0e28 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)" ``` oheimb@1660 ` 56` ```(*<<<<<<< Prod.thy*) ``` oheimb@1660 ` 57` ```(* The <= direction fails if split has more than one argument because ``` oheimb@1660 ` 58` ``` ast-matching fails. Otherwise it would work fine *) ``` oheimb@1660 ` 59` oheimb@1660 ` 60` ```(*=======*) ``` nipkow@1068 ` 61` nipkow@1636 ` 62` ``` "SIGMA x:A. B" => "Sigma A (%x.B)" ``` nipkow@1636 ` 63` ``` "A Times B" => "Sigma A (_K B)" ``` nipkow@1636 ` 64` oheimb@1660 ` 65` ```(*>>>>>>> 1.13*) ``` clasohm@923 ` 66` ```defs ``` clasohm@923 ` 67` ``` Pair_def "Pair a b == Abs_Prod(Pair_Rep a b)" ``` clasohm@972 ` 68` ``` fst_def "fst(p) == @a. ? b. p = (a, b)" ``` clasohm@972 ` 69` ``` snd_def "snd(p) == @b. ? a. p = (a, b)" ``` nipkow@1655 ` 70` ``` split_def "split == (%c p. c (fst p) (snd p))" ``` clasohm@972 ` 71` ``` prod_fun_def "prod_fun f g == split(%x y.(f(x), g(y)))" ``` clasohm@972 ` 72` ``` Sigma_def "Sigma A B == UN x:A. UN y:B(x). {(x, y)}" ``` clasohm@923 ` 73` clasohm@923 ` 74` ```(** Unit **) ``` clasohm@923 ` 75` clasohm@1475 ` 76` ```typedef (Unit) ``` clasohm@923 ` 77` ``` unit = "{p. p = True}" ``` clasohm@923 ` 78` clasohm@923 ` 79` ```consts ``` clasohm@1370 ` 80` ``` "()" :: unit ("'(')") ``` clasohm@923 ` 81` clasohm@923 ` 82` ```defs ``` clasohm@972 ` 83` ``` Unity_def "() == Abs_Unit(True)" ``` clasohm@923 ` 84` regensbu@1273 ` 85` ```(* start 8bit 1 *) ``` regensbu@1273 ` 86` ```(* end 8bit 1 *) ``` regensbu@1273 ` 87` clasohm@923 ` 88` ```end ``` oheimb@1660 ` 89` ```(*<<<<<<< Prod.thy*) ``` oheimb@1660 ` 90` ```(* ``` oheimb@1660 ` 91` ```ML ``` oheimb@1660 ` 92` oheimb@1660 ` 93` ```local open Syntax ``` oheimb@1660 ` 94` oheimb@1660 ` 95` ```fun pttrn(_ \$ s \$ t) = const"@pttrn" \$ s \$ t; ``` oheimb@1660 ` 96` ```fun pttrns s t = const"@pttrns" \$ s \$ t; ``` oheimb@1660 ` 97` oheimb@1660 ` 98` ```fun split2(Abs(x,T,t)) = ``` oheimb@1660 ` 99` ``` let val (pats,u) = split1 t ``` oheimb@1660 ` 100` ``` in (pttrns (Free(x,T)) pats, subst_bounds([free x],u)) end ``` oheimb@1660 ` 101` ``` | split2(Const("split",_) \$ r) = ``` oheimb@1660 ` 102` ``` let val (pats,s) = split2(r) ``` oheimb@1660 ` 103` ``` val (pats2,t) = split1(s) ``` oheimb@1660 ` 104` ``` in (pttrns (pttrn pats) pats2, t) end ``` oheimb@1660 ` 105` ```and split1(Abs(x,T,t)) = (Free(x,T), subst_bounds([free x],t)) ``` oheimb@1660 ` 106` ``` | split1(Const("split",_)\$t) = split2(t); ``` oheimb@1660 ` 107` oheimb@1660 ` 108` ```fun split_tr'(t::args) = ``` oheimb@1660 ` 109` ``` let val (pats,ft) = split2(t) ``` oheimb@1660 ` 110` ``` in list_comb(const"_lambda" \$ pttrn pats \$ ft, args) end; ``` oheimb@1660 ` 111` oheimb@1660 ` 112` ```in ``` oheimb@1660 ` 113` oheimb@1660 ` 114` ```val print_translation = [("split", split_tr')]; ``` oheimb@1660 ` 115` oheimb@1660 ` 116` ```end; ``` oheimb@1660 ` 117` ```*) ``` oheimb@1660 ` 118` ```(*=======*) ``` nipkow@1636 ` 119` nipkow@1636 ` 120` ```ML ``` nipkow@1636 ` 121` nipkow@1636 ` 122` ```val print_translation = [("Sigma", dependent_tr' ("@Sigma", "@Times"))]; ``` nipkow@1636 ` 123` oheimb@1660 ` 124` ```(*>>>>>>> 1.13*) ```