src/HOL/Library/OptionalSugar.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (21 months ago)
changeset 67003 49850a679c2c
parent 63935 aa1fe1103ab8
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      HOL/Library/OptionalSugar.thy
     2     Author:     Gerwin Klein, Tobias Nipkow
     3     Copyright   2005 NICTA and TUM
     4 *)
     5 (*<*)
     6 theory OptionalSugar
     7 imports Complex_Main LaTeXsugar
     8 begin
     9 
    10 (* displaying theorems with conjunctions between premises: *)
    11 translations
    12   ("prop") "P \<and> Q \<Longrightarrow> R" <= ("prop") "P \<Longrightarrow> Q \<Longrightarrow> R"
    13 
    14 (* hiding set *)
    15 translations
    16   "xs" <= "CONST set xs"
    17 
    18 (* hiding numeric conversions - embeddings only *)
    19 translations
    20   "n" <= "CONST of_nat n"
    21   "n" <= "CONST int n"
    22   "n" <= "CONST real n"
    23   "n" <= "CONST real_of_nat n"
    24   "n" <= "CONST real_of_int n"
    25   "n" <= "CONST of_real n"
    26   "n" <= "CONST complex_of_real n"
    27 
    28 (* append *)
    29 syntax (latex output)
    30   "_appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^latex>\<open>\\isacharat\<close>" 65)
    31 translations
    32   "_appendL xs ys" <= "xs @ ys" 
    33   "_appendL (_appendL xs ys) zs" <= "_appendL xs (_appendL ys zs)"
    34 
    35 
    36 (* deprecated, use thm with style instead, will be removed *)
    37 (* aligning equations *)
    38 notation (tab output)
    39   "HOL.eq"  ("(_) \<^latex>\<open>}\\putisatab\\isa{\\ \<close>=\<^latex>\<open>}\\putisatab\\isa{\<close> (_)" [50,49] 50) and
    40   "Pure.eq"  ("(_) \<^latex>\<open>}\\putisatab\\isa{\\ \<close>\<equiv>\<^latex>\<open>}\\putisatab\\isa{\<close> (_)")
    41 
    42 (* Let *)
    43 translations 
    44   "_bind (p, CONST DUMMY) e" <= "_bind p (CONST fst e)"
    45   "_bind (CONST DUMMY, p) e" <= "_bind p (CONST snd e)"
    46 
    47   "_tuple_args x (_tuple_args y z)" ==
    48     "_tuple_args x (_tuple_arg (_tuple y z))"
    49 
    50   "_bind (CONST Some p) e" <= "_bind p (CONST the e)"
    51   "_bind (p # CONST DUMMY) e" <= "_bind p (CONST hd e)"
    52   "_bind (CONST DUMMY # p) e" <= "_bind p (CONST tl e)"
    53 
    54 (* type constraints with spacing *)
    55 no_syntax (output)
    56   "_constrain" :: "logic => type => logic"  ("_::_" [4, 0] 3)
    57   "_constrain" :: "prop' => type => prop'"  ("_::_" [4, 0] 3)
    58 
    59 syntax (output)
    60   "_constrain" :: "logic => type => logic"  ("_ :: _" [4, 0] 3)
    61   "_constrain" :: "prop' => type => prop'"  ("_ :: _" [4, 0] 3)
    62 
    63 
    64 (* sorts as intersections *)
    65 
    66 syntax (output)
    67   "_topsort" :: "sort"  ("\<top>" 1000)
    68   "_sort" :: "classes => sort"  ("'(_')" 1000)
    69   "_classes" :: "id => classes => classes"  ("_ \<inter> _" 1000)
    70   "_classes" :: "longid => classes => classes"  ("_ \<inter> _" 1000)
    71 
    72 end
    73 (*>*)