src/HOL/Prod.thy
 author regensbu Fri Oct 06 16:17:08 1995 +0100 (1995-10-06) changeset 1273 6960ec882bca parent 1114 c8dfb56a7e95 child 1370 7361ac9b024d 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` clasohm@923 ` 10` ```Prod = Fun + ``` clasohm@923 ` 11` clasohm@923 ` 12` ```(** Products **) ``` clasohm@923 ` 13` clasohm@923 ` 14` ```(* type definition *) ``` clasohm@923 ` 15` clasohm@923 ` 16` ```consts ``` clasohm@923 ` 17` ``` Pair_Rep :: "['a, 'b] => ['a, 'b] => bool" ``` clasohm@923 ` 18` clasohm@923 ` 19` ```defs ``` clasohm@923 ` 20` ``` Pair_Rep_def "Pair_Rep == (%a b. %x y. x=a & y=b)" ``` clasohm@923 ` 21` clasohm@923 ` 22` ```subtype (Prod) ``` clasohm@923 ` 23` ``` ('a, 'b) "*" (infixr 20) ``` clasohm@923 ` 24` ``` = "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}" ``` clasohm@923 ` 25` clasohm@923 ` 26` clasohm@923 ` 27` ```(* abstract constants and syntax *) ``` clasohm@923 ` 28` clasohm@923 ` 29` ```consts ``` clasohm@923 ` 30` ``` fst :: "'a * 'b => 'a" ``` clasohm@923 ` 31` ``` snd :: "'a * 'b => 'b" ``` clasohm@923 ` 32` ``` split :: "[['a, 'b] => 'c, 'a * 'b] => 'c" ``` clasohm@923 ` 33` ``` prod_fun :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd" ``` clasohm@923 ` 34` ``` Pair :: "['a, 'b] => 'a * 'b" ``` clasohm@923 ` 35` ``` Sigma :: "['a set, 'a => 'b set] => ('a * 'b) set" ``` clasohm@923 ` 36` nipkow@1068 ` 37` ```(** Patterns -- extends pre-defined type "pttrn" used in abstractions **) ``` nipkow@1068 ` 38` ```types pttrns ``` nipkow@1068 ` 39` clasohm@923 ` 40` ```syntax ``` clasohm@972 ` 41` ``` "@Tuple" :: "['a, args] => 'a * 'b" ("(1'(_,/ _'))") ``` clasohm@923 ` 42` nipkow@1114 ` 43` ``` "@pttrn" :: "[pttrn,pttrns] => pttrn" ("'(_,/_')") ``` nipkow@1114 ` 44` ``` "" :: " pttrn => pttrns" ("_") ``` nipkow@1114 ` 45` ``` "@pttrns" :: "[pttrn,pttrns] => pttrns" ("_,/_") ``` nipkow@1068 ` 46` clasohm@923 ` 47` ```translations ``` clasohm@972 ` 48` ``` "(x, y, z)" == "(x, (y, z))" ``` clasohm@972 ` 49` ``` "(x, y)" == "Pair x y" ``` clasohm@923 ` 50` nipkow@1114 ` 51` ``` "%(x,y,zs).b" == "split(%x (y,zs).b)" ``` nipkow@1114 ` 52` ``` "%(x,y).b" == "split(%x y.b)" ``` nipkow@1068 ` 53` ```(* The <= direction fails if split has more than one argument because ``` nipkow@1068 ` 54` ``` ast-matching fails. Otherwise it would work fine *) ``` nipkow@1068 ` 55` clasohm@923 ` 56` ```defs ``` clasohm@923 ` 57` ``` Pair_def "Pair a b == Abs_Prod(Pair_Rep a b)" ``` clasohm@972 ` 58` ``` fst_def "fst(p) == @a. ? b. p = (a, b)" ``` clasohm@972 ` 59` ``` snd_def "snd(p) == @b. ? a. p = (a, b)" ``` clasohm@923 ` 60` ``` split_def "split c p == c (fst p) (snd p)" ``` clasohm@972 ` 61` ``` prod_fun_def "prod_fun f g == split(%x y.(f(x), g(y)))" ``` clasohm@972 ` 62` ``` Sigma_def "Sigma A B == UN x:A. UN y:B(x). {(x, y)}" ``` clasohm@923 ` 63` clasohm@923 ` 64` clasohm@923 ` 65` clasohm@923 ` 66` ```(** Unit **) ``` clasohm@923 ` 67` clasohm@923 ` 68` ```subtype (Unit) ``` clasohm@923 ` 69` ``` unit = "{p. p = True}" ``` clasohm@923 ` 70` clasohm@923 ` 71` ```consts ``` clasohm@972 ` 72` ``` "()" :: "unit" ("'(')") ``` clasohm@923 ` 73` clasohm@923 ` 74` ```defs ``` clasohm@972 ` 75` ``` Unity_def "() == Abs_Unit(True)" ``` clasohm@923 ` 76` regensbu@1273 ` 77` ```(* start 8bit 1 *) ``` regensbu@1273 ` 78` ```(* end 8bit 1 *) ``` regensbu@1273 ` 79` clasohm@923 ` 80` ```end ``` nipkow@1114 ` 81` ```(* ``` nipkow@1068 ` 82` ```ML ``` nipkow@1068 ` 83` nipkow@1068 ` 84` ```local open Syntax ``` nipkow@1068 ` 85` nipkow@1114 ` 86` ```fun pttrn(_ \$ s \$ t) = const"@pttrn" \$ s \$ t; ``` nipkow@1068 ` 87` ```fun pttrns s t = const"@pttrns" \$ s \$ t; ``` nipkow@1068 ` 88` nipkow@1068 ` 89` ```fun split2(Abs(x,T,t)) = ``` nipkow@1068 ` 90` ``` let val (pats,u) = split1 t ``` nipkow@1068 ` 91` ``` in (pttrns (Free(x,T)) pats, subst_bounds([free x],u)) end ``` nipkow@1068 ` 92` ``` | split2(Const("split",_) \$ r) = ``` nipkow@1068 ` 93` ``` let val (pats,s) = split2(r) ``` nipkow@1068 ` 94` ``` val (pats2,t) = split1(s) ``` nipkow@1068 ` 95` ``` in (pttrns (pttrn pats) pats2, t) end ``` nipkow@1068 ` 96` ```and split1(Abs(x,T,t)) = (Free(x,T), subst_bounds([free x],t)) ``` nipkow@1068 ` 97` ``` | split1(Const("split",_)\$t) = split2(t); ``` nipkow@1068 ` 98` nipkow@1068 ` 99` ```fun split_tr'(t::args) = ``` nipkow@1068 ` 100` ``` let val (pats,ft) = split2(t) ``` nipkow@1081 ` 101` ``` in list_comb(const"_lambda" \$ pttrn pats \$ ft, args) end; ``` nipkow@1068 ` 102` nipkow@1068 ` 103` ```in ``` nipkow@1068 ` 104` nipkow@1068 ` 105` ```val print_translation = [("split", split_tr')]; ``` nipkow@1068 ` 106` nipkow@1068 ` 107` ```end; ``` nipkow@1114 ` 108` ```*) ```