prod.thy

renamed theory files

(*  Title: 	HOL/prod
    ID:         $Id$
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge

Ordered Pairs and the Cartesian product type
The unit type

The type definition admits the following unused axiom:
  Abs_Unit_inverse 	"f: Unit ==> Rep_Unit(Abs_Unit(f)) = f"
*)

Prod = Set +

types   
  ('a,'b) "*"          (infixr 20)
  unit

arities 
  "*"      :: (term,term)term
  unit     :: term

consts
  Pair_Rep :: "['a,'b] => ['a,'b] => bool"
  Prod	   :: "('a => 'b => bool)set"
  Rep_Prod :: "'a * 'b => ('a => 'b => bool)"
  Abs_Prod :: "('a => 'b => bool) => 'a * 'b"
  fst	   :: "'a * 'b => 'a"
  snd	   :: "'a * 'b => 'b"
  split    :: "['a * 'b, ['a,'b]=>'c] => 'c"
  prod_fun :: "['a=>'b, 'c=>'d, 'a*'c] => 'b*'d"
  Pair	   :: "['a,'b] => 'a * 'b"
  "@Tuple" :: "args => 'a*'b"			("(1<_>)")
  Sigma    :: "['a set, 'a => 'b set] => ('a*'b)set"

  Unit	   :: "bool set"
  Rep_Unit :: "unit => bool"
  Abs_Unit :: "bool => unit"
  Unity    :: "unit"					("<>")

translations

  "<x,y,z>" == "<x,<y,z>>"
  "<x,y>"   == "Pair(x,y)"
  "<x>"     => "x"

rules

  Pair_Rep_def     "Pair_Rep == (%a b. %x y. x=a & y=b)"
  Prod_def         "Prod == {f. ? a b. f = Pair_Rep(a,b)}"
    (*faking a type definition...*)
  Rep_Prod         "Rep_Prod(p): Prod"
  Rep_Prod_inverse "Abs_Prod(Rep_Prod(p)) = p"
  Abs_Prod_inverse "f: Prod ==> Rep_Prod(Abs_Prod(f)) = f"
    (*defining the abstract constants*)
  Pair_def         "Pair(a,b) == Abs_Prod(Pair_Rep(a,b))"
  fst_def          "fst(p) == @a. ? b. p = <a,b>"
  snd_def          "snd(p) == @b. ? a. p = <a,b>"
  split_def        "split(p,c) == c(fst(p),snd(p))"
  prod_fun_def     "prod_fun(f,g) == (%z.split(z, %x y.<f(x), g(y)>))"
  Sigma_def        "Sigma(A,B) == UN x:A. UN y:B(x). {<x,y>}"

  Unit_def         "Unit == {p. p=True}"
    (*faking a type definition...*)
  Rep_Unit         "Rep_Unit(u): Unit"
  Rep_Unit_inverse "Abs_Unit(Rep_Unit(u)) = u"
    (*defining the abstract constants*)
  Unity_def        "Unity == Abs_Unit(True)"
end