type constraints and sort intersection
authorhaftmann
Thu Jan 15 14:52:24 2009 +0100 (2009-01-15)
changeset 29494a189c6274c7a
parent 29493 ddcbd5e4041d
child 29495 c49b4c8f2eaa
type constraints and sort intersection
src/HOL/Library/OptionalSugar.thy
     1.1 --- a/src/HOL/Library/OptionalSugar.thy	Thu Jan 15 14:52:24 2009 +0100
     1.2 +++ b/src/HOL/Library/OptionalSugar.thy	Thu Jan 15 14:52:24 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Library/OptionalSugar.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Gerwin Klain, Tobias Nipkow
     1.7      Copyright   2005 NICTA and TUM
     1.8  *)
     1.9 @@ -37,6 +36,36 @@
    1.10    "_bind (p#DUMMY) e" <= "_bind p (hd e)"
    1.11    "_bind (DUMMY#p) e" <= "_bind p (tl e)"
    1.12  
    1.13 +(* type constraints with spacing *)
    1.14 +setup {*
    1.15 +let
    1.16 +  val typ = SimpleSyntax.read_typ;
    1.17 +  val typeT = Syntax.typeT;
    1.18 +  val spropT = Syntax.spropT;
    1.19 +in
    1.20 +  Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
    1.21 +    ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
    1.22 +    ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
    1.23 +  #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
    1.24 +      ("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
    1.25 +      ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))]
    1.26 +end
    1.27 +*}
    1.28 +
    1.29 +(* sorts as intersections *)
    1.30 +setup {*
    1.31 +let
    1.32 +  val sortT = Type ("sort", []); (*FIXME*)
    1.33 +  val classesT = Type ("classes", []); (*FIXME*)
    1.34 +in
    1.35 +  Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
    1.36 +    ("_topsort", sortT, Mixfix ("\<top>", [], Syntax.max_pri)),
    1.37 +    ("_sort", classesT --> sortT, Mixfix ("'(_')", [], Syntax.max_pri)),
    1.38 +    ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri)),
    1.39 +    ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri))
    1.40 +  ]
    1.41 +end
    1.42 +*}
    1.43  
    1.44  end
    1.45  (*>*)