nipkow@15469: (*  Title:      HOL/Library/OptionalSugar.thy
nipkow@15469:     Author:     Gerwin Klain, Tobias Nipkow
nipkow@15469:     Copyright   2005 NICTA and TUM
nipkow@15469: *)
nipkow@15476: (*<*)
nipkow@15469: theory OptionalSugar
haftmann@30663: imports Complex_Main LaTeXsugar
nipkow@15469: begin
nipkow@15469: 
nipkow@30474: (* hiding set *)
nipkow@22835: translations
wenzelm@30404:   "xs" <= "CONST set xs"
nipkow@22835: 
nipkow@30474: (* hiding numeric conversions - embeddings only *)
nipkow@30474: translations
nipkow@30474:   "n" <= "CONST of_nat n"
nipkow@30474:   "n" <= "CONST int n"
wenzelm@35115:   "n" <= "CONST real n"
nipkow@30474:   "n" <= "CONST real_of_nat n"
nipkow@30474:   "n" <= "CONST real_of_int n"
nipkow@30502:   "n" <= "CONST of_real n"
nipkow@30502:   "n" <= "CONST complex_of_real n"
nipkow@30474: 
nipkow@15469: (* append *)
nipkow@15469: syntax (latex output)
wenzelm@35115:   "_appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
nipkow@15469: translations
wenzelm@35115:   "_appendL xs ys" <= "xs @ ys" 
wenzelm@35115:   "_appendL (_appendL xs ys) zs" <= "_appendL xs (_appendL ys zs)"
nipkow@15469: 
nipkow@15469: 
haftmann@32891: (* deprecated, use thm with style instead, will be removed *)
nipkow@15469: (* aligning equations *)
wenzelm@21210: notation (tab output)
haftmann@38864:   "HOL.eq"  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
wenzelm@19674:   "=="  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
nipkow@15469: 
nipkow@15469: (* Let *)
nipkow@15469: translations 
wenzelm@35250:   "_bind (p, CONST DUMMY) e" <= "_bind p (CONST fst e)"
wenzelm@35250:   "_bind (CONST DUMMY, p) e" <= "_bind p (CONST snd e)"
nipkow@15469: 
nipkow@15469:   "_tuple_args x (_tuple_args y z)" ==
nipkow@15469:     "_tuple_args x (_tuple_arg (_tuple y z))"
nipkow@15469: 
wenzelm@35250:   "_bind (CONST Some p) e" <= "_bind p (CONST the e)"
wenzelm@35250:   "_bind (p # CONST DUMMY) e" <= "_bind p (CONST hd e)"
wenzelm@35250:   "_bind (CONST DUMMY # p) e" <= "_bind p (CONST tl e)"
nipkow@15469: 
haftmann@29494: (* type constraints with spacing *)
haftmann@29494: setup {*
haftmann@29494: let
wenzelm@33384:   val typ = Simple_Syntax.read_typ;
haftmann@29494: in
wenzelm@42293:   Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
wenzelm@42293:    [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
wenzelm@42293:     ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
wenzelm@42293:   Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
wenzelm@42293:    [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
wenzelm@42293:     ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
haftmann@29494: end
haftmann@29494: *}
haftmann@29494: 
haftmann@29494: (* sorts as intersections *)
haftmann@29494: setup {*
haftmann@29494: let
haftmann@29494:   val sortT = Type ("sort", []); (*FIXME*)
haftmann@29494:   val classesT = Type ("classes", []); (*FIXME*)
haftmann@29494: in
haftmann@29494:   Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
wenzelm@42297:     ("_topsort", sortT, Mixfix ("\<top>", [], 1000)),
wenzelm@42297:     ("_sort", classesT --> sortT, Mixfix ("'(_')", [], 1000)),
wenzelm@42297:     ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], 1000)),
wenzelm@42297:     ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], 1000))
haftmann@29494:   ]
haftmann@29494: end
haftmann@29494: *}
nipkow@15469: 
nipkow@15476: end
nipkow@15476: (*>*)