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