src/HOL/Library/OptionalSugar.thy

bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)

(*  Title:      HOL/Library/OptionalSugar.thy
    Author:     Gerwin Klain, Tobias Nipkow
    Copyright   2005 NICTA and TUM
*)
(*<*)
theory OptionalSugar
imports Complex_Main LaTeXsugar
begin

(* hiding set *)
translations
  "xs" <= "CONST set xs"

(* hiding numeric conversions - embeddings only *)
translations
  "n" <= "CONST of_nat n"
  "n" <= "CONST int n"
  "n" <= "real n"
  "n" <= "CONST real_of_nat n"
  "n" <= "CONST real_of_int n"
  "n" <= "CONST of_real n"
  "n" <= "CONST complex_of_real n"

(* append *)
syntax (latex output)
  "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
translations
  "appendL xs ys" <= "xs @ ys" 
  "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)"


(* deprecated, use thm with style instead, will be removed *)
(* aligning equations *)
notation (tab output)
  "op ="  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
  "=="  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")

(* Let *)
translations 
  "_bind (p,DUMMY) e" <= "_bind p (CONST fst e)"
  "_bind (DUMMY,p) e" <= "_bind p (CONST snd e)"

  "_tuple_args x (_tuple_args y z)" ==
    "_tuple_args x (_tuple_arg (_tuple y z))"

  "_bind (Some p) e" <= "_bind p (CONST the e)"
  "_bind (p#DUMMY) e" <= "_bind p (CONST hd e)"
  "_bind (DUMMY#p) e" <= "_bind p (CONST tl e)"

(* type constraints with spacing *)
setup {*
let
  val typ = Simple_Syntax.read_typ;
  val typeT = Syntax.typeT;
  val spropT = Syntax.spropT;
in
  Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
    ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
    ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
  #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
      ("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
      ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))]
end
*}

(* sorts as intersections *)
setup {*
let
  val sortT = Type ("sort", []); (*FIXME*)
  val classesT = Type ("classes", []); (*FIXME*)
in
  Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
    ("_topsort", sortT, Mixfix ("\<top>", [], Syntax.max_pri)),
    ("_sort", classesT --> sortT, Mixfix ("'(_')", [], Syntax.max_pri)),
    ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri)),
    ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri))
  ]
end
*}

end
(*>*)