added set inclusion symbol syntax;
authorwenzelm
Fri Dec 13 17:42:36 1996 +0100 (1996-12-13)
changeset 2388d1f0505fc602
parent 2387 1b37895b607a
child 2389 d472c732bc21
added set inclusion symbol syntax;
src/HOL/Set.thy
     1.1 --- a/src/HOL/Set.thy	Fri Dec 13 17:38:56 1996 +0100
     1.2 +++ b/src/HOL/Set.thy	Fri Dec 13 17:42:36 1996 +0100
     1.3 @@ -84,8 +84,13 @@
     1.4    "ALL x:A. P"  => "Ball A (%x. P)"
     1.5    "EX x:A. P"   => "Bex A (%x. P)"
     1.6  
     1.7 +syntax ("" output)
     1.8 +  "_setle"      :: ['a set, 'a set] => bool           ("(_/ <= _)" [50, 51] 50)
     1.9 +  "_setle"      :: ['a set, 'a set] => bool           ("op <=")
    1.10  
    1.11  syntax (symbols)
    1.12 +  "_setle"      :: ['a set, 'a set] => bool           ("(_/ \\<subseteq> _)" [50, 51] 50)
    1.13 +  "_setle"      :: ['a set, 'a set] => bool           ("op \\<subseteq>")
    1.14    "op Int"      :: ['a set, 'a set] => 'a set         (infixl "\\<inter>" 70)
    1.15    "op Un"       :: ['a set, 'a set] => 'a set         (infixl "\\<union>" 65)
    1.16    "op :"        :: ['a, 'a set] => bool               ("(_/ \\<in> _)" [50, 51] 50)
    1.17 @@ -140,8 +145,6 @@
    1.18    inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    1.19    surj_def      "surj(f)        == ! y. ? x. y=f(x)"
    1.20  
    1.21 -(* start 8bit 1 *)
    1.22 -(* end 8bit 1 *)
    1.23  
    1.24  end
    1.25  
    1.26 @@ -150,6 +153,13 @@
    1.27  
    1.28  local
    1.29  
    1.30 +(* Set inclusion *)
    1.31 +
    1.32 +fun le_tr' (*op <=*) (Type ("fun", (Type ("set", _) :: _))) ts =
    1.33 +      list_comb (Syntax.const "_setle", ts)
    1.34 +  | le_tr' (*op <=*) _ _ = raise Match;
    1.35 +
    1.36 +
    1.37  (* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P}      *)
    1.38  (* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *)
    1.39  
    1.40 @@ -182,6 +192,7 @@
    1.41  
    1.42  val parse_translation = [("@SetCompr", setcompr_tr)];
    1.43  val print_translation = [("Collect", setcompr_tr')];
    1.44 +val typed_print_translation = [("op <=", le_tr')];
    1.45  val print_ast_translation =
    1.46    map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];
    1.47