src/HOL/Set.thy
author nipkow
Sat Apr 22 13:25:31 1995 +0200 (1995-04-22)
changeset 1068 e0f2dffab506
parent 923 ff1574a81019
child 1273 6960ec882bca
permissions -rw-r--r--
HOL.thy:

"@" is no longer introduced as a "binder" but has its own explicit
translation rule "@x.b" == "Eps(%x.b)". If x is a proper pattern, further
translation rules for abstractions with patterns take care of the rest. This
is very modular and avoids problems with "binders" such as "!" mentioned
below.

let now allows pttrn (let (x,y) = t in u) instead of just idt (let x = t in u)


Set.thy:

UN, INT, ALL, EX, etc all use "pttrn" instead of idt. Same change as for "@"
above, except that "@" was a "binder" originally.


Prod.thy:

Added new syntax for pttrn which allows arbitrarily nested tuples. Two
translation rules take care of %pttrn. Unfortunately they cannot be
reversed. Hence a little ML-code is used as well.

Note that now "! (x,y). ..." is syntactically valid but leads to a
translation error. This is because "!" is introduced as a "binder" which
means that its translation into lambda-terms is not done by a rewrite rule
(aka macro) but by some fixed ML-code which comes after the rewriting stage
and does not know how to handle patterns. This looks like a minor blemish
since patterns in unbounded quantifiers are not that useful (well, except
maybe in unique existence ...). Ideally, there should be two syntactic
categories:

idts, as we know and love it, which does not admit patterns.
patterns, which is what idts has become now.

There is one more point where patterns are now allowed but don't make sense:

{e | idts . P}

where idts is the list of local variables.


Univ.thy: converted the defs for <++> and <**> into pattern form. It worked
perfectly.
     1 (*  Title:      HOL/Set.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1993  University of Cambridge
     5 *)
     6 
     7 Set = Ord +
     8 
     9 types
    10   'a set
    11 
    12 arities
    13   set :: (term) term
    14 
    15 instance
    16   set :: (term) {ord, minus}
    17 
    18 consts
    19   "{}"          :: "'a set"                           ("{}")
    20   insert        :: "['a, 'a set] => 'a set"
    21   Collect       :: "('a => bool) => 'a set"               (*comprehension*)
    22   Compl         :: "('a set) => 'a set"                   (*complement*)
    23   Int           :: "['a set, 'a set] => 'a set"       (infixl 70)
    24   Un            :: "['a set, 'a set] => 'a set"       (infixl 65)
    25   UNION, INTER  :: "['a set, 'a => 'b set] => 'b set"     (*general*)
    26   UNION1        :: "['a => 'b set] => 'b set"         (binder "UN " 10)
    27   INTER1        :: "['a => 'b set] => 'b set"         (binder "INT " 10)
    28   Union, Inter  :: "(('a set)set) => 'a set"              (*of a set*)
    29   Pow           :: "'a set => 'a set set"                 (*powerset*)
    30   range         :: "('a => 'b) => 'b set"                 (*of function*)
    31   Ball, Bex     :: "['a set, 'a => bool] => bool"         (*bounded quantifiers*)
    32   inj, surj     :: "('a => 'b) => bool"                   (*inj/surjective*)
    33   inj_onto      :: "['a => 'b, 'a set] => bool"
    34   "``"          :: "['a => 'b, 'a set] => ('b set)"   (infixl 90)
    35   ":"           :: "['a, 'a set] => bool"             (infixl 50) (*membership*)
    36 
    37 
    38 syntax
    39 
    40   "~:"          :: "['a, 'a set] => bool"             (infixl 50)
    41 
    42   "@Finset"     :: "args => 'a set"                   ("{(_)}")
    43 
    44   "@Coll"       :: "[pttrn, bool] => 'a set"          ("(1{_./ _})")
    45   "@SetCompr"   :: "['a, idts, bool] => 'a set"       ("(1{_ |/_./ _})")
    46 
    47   (* Big Intersection / Union *)
    48 
    49   "@INTER"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3INT _:_./ _)" 10)
    50   "@UNION"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3UN _:_./ _)" 10)
    51 
    52   (* Bounded Quantifiers *)
    53 
    54   "@Ball"       :: "[pttrn, 'a set, bool] => bool"      ("(3! _:_./ _)" 10)
    55   "@Bex"        :: "[pttrn, 'a set, bool] => bool"      ("(3? _:_./ _)" 10)
    56   "*Ball"       :: "[pttrn, 'a set, bool] => bool"      ("(3ALL _:_./ _)" 10)
    57   "*Bex"        :: "[pttrn, 'a set, bool] => bool"      ("(3EX _:_./ _)" 10)
    58 
    59 translations
    60   "x ~: y"      == "~ (x : y)"
    61   "{x, xs}"     == "insert x {xs}"
    62   "{x}"         == "insert x {}"
    63   "{x. P}"      == "Collect (%x. P)"
    64   "INT x:A. B"  == "INTER A (%x. B)"
    65   "UN x:A. B"   == "UNION A (%x. B)"
    66   "! x:A. P"    == "Ball A (%x. P)"
    67   "? x:A. P"    == "Bex A (%x. P)"
    68   "ALL x:A. P"  => "Ball A (%x. P)"
    69   "EX x:A. P"   => "Bex A (%x. P)"
    70 
    71 
    72 rules
    73 
    74   (* Isomorphisms between Predicates and Sets *)
    75 
    76   mem_Collect_eq    "(a : {x.P(x)}) = P(a)"
    77   Collect_mem_eq    "{x.x:A} = A"
    78 
    79 
    80 defs
    81   Ball_def      "Ball A P       == ! x. x:A --> P(x)"
    82   Bex_def       "Bex A P        == ? x. x:A & P(x)"
    83   subset_def    "A <= B         == ! x:A. x:B"
    84   Compl_def     "Compl(A)       == {x. ~x:A}"
    85   Un_def        "A Un B         == {x.x:A | x:B}"
    86   Int_def       "A Int B        == {x.x:A & x:B}"
    87   set_diff_def  "A - B          == {x. x:A & ~x:B}"
    88   INTER_def     "INTER A B      == {y. ! x:A. y: B(x)}"
    89   UNION_def     "UNION A B      == {y. ? x:A. y: B(x)}"
    90   INTER1_def    "INTER1(B)      == INTER {x.True} B"
    91   UNION1_def    "UNION1(B)      == UNION {x.True} B"
    92   Inter_def     "Inter(S)       == (INT x:S. x)"
    93   Union_def     "Union(S)       == (UN x:S. x)"
    94   Pow_def       "Pow(A)         == {B. B <= A}"
    95   empty_def     "{}             == {x. False}"
    96   insert_def    "insert a B     == {x.x=a} Un B"
    97   range_def     "range(f)       == {y. ? x. y=f(x)}"
    98   image_def     "f``A           == {y. ? x:A. y=f(x)}"
    99   inj_def       "inj(f)         == ! x y. f(x)=f(y) --> x=y"
   100   inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
   101   surj_def      "surj(f)        == ! y. ? x. y=f(x)"
   102 
   103 end
   104 
   105 ML
   106 
   107 local
   108 
   109 (* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P}      *)
   110 (* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *)
   111 
   112 val ex_tr = snd(mk_binder_tr("? ","Ex"));
   113 
   114 fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1
   115   | nvars(_) = 1;
   116 
   117 fun setcompr_tr[e,idts,b] =
   118   let val eq = Syntax.const("op =") $ Bound(nvars(idts)) $ e
   119       val P = Syntax.const("op &") $ eq $ b
   120       val exP = ex_tr [idts,P]
   121   in Syntax.const("Collect") $ Abs("",dummyT,exP) end;
   122 
   123 val ex_tr' = snd(mk_binder_tr' ("Ex","DUMMY"));
   124 
   125 fun setcompr_tr'[Abs(_,_,P)] =
   126   let fun ok(Const("Ex",_)$Abs(_,_,P),n) = ok(P,n+1)
   127         | ok(Const("op &",_) $ (Const("op =",_) $ Bound(m) $ e) $ _, n) =
   128             if n>0 andalso m=n andalso
   129               ((0 upto (n-1)) subset add_loose_bnos(e,0,[]))
   130             then () else raise Match
   131 
   132       fun tr'(_ $ abs) =
   133         let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr'[abs]
   134         in Syntax.const("@SetCompr") $ e $ idts $ Q end
   135   in ok(P,0); tr'(P) end;
   136 
   137 in
   138 
   139 val parse_translation = [("@SetCompr", setcompr_tr)];
   140 val print_translation = [("Collect", setcompr_tr')];
   141 val print_ast_translation =
   142   map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];
   143 
   144 end;
   145