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