src/HOL/Library/LaTeXsugar.thy
author wenzelm
Tue, 09 Jan 2018 15:40:12 +0100
changeset 67386 998e01d6f8fd
parent 66527 7ca69030a2af
child 67399 eab6ce8368fa
permissions -rw-r--r--
clarified modules;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15469
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Library/LaTeXsugar.thy
55077
4cf280104b85 fixed typo
blanchet
parents: 49628
diff changeset
     2
    Author:     Gerwin Klein, Tobias Nipkow, Norbert Schirmer
15469
nipkow
parents:
diff changeset
     3
    Copyright   2005 NICTA and TUM
nipkow
parents:
diff changeset
     4
*)
nipkow
parents:
diff changeset
     5
nipkow
parents:
diff changeset
     6
(*<*)
nipkow
parents:
diff changeset
     7
theory LaTeXsugar
30663
0b6aff7451b2 Main is (Complex_Main) base entry point in library theories
haftmann
parents: 30304
diff changeset
     8
imports Main
15469
nipkow
parents:
diff changeset
     9
begin
nipkow
parents:
diff changeset
    10
nipkow
parents:
diff changeset
    11
(* LOGIC *)
21210
c17fd2df4e9e renamed 'const_syntax' to 'notation';
wenzelm
parents: 19674
diff changeset
    12
notation (latex output)
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63414
diff changeset
    13
  If  ("(\<^latex>\<open>\\textsf{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textsf{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textsf{\<close>else\<^latex>\<open>}\<close> (_))" 10)
19674
22b635240905 const_syntax;
wenzelm
parents: 16110
diff changeset
    14
15469
nipkow
parents:
diff changeset
    15
syntax (latex output)
nipkow
parents:
diff changeset
    16
nipkow
parents:
diff changeset
    17
  "_Let"        :: "[letbinds, 'a] => 'a"
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63414
diff changeset
    18
  ("(\<^latex>\<open>\\textsf{\<close>let\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textsf{\<close>in\<^latex>\<open>}\<close> (_))" 10)
15469
nipkow
parents:
diff changeset
    19
nipkow
parents:
diff changeset
    20
  "_case_syntax":: "['a, cases_syn] => 'b"
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63414
diff changeset
    21
  ("(\<^latex>\<open>\\textsf{\<close>case\<^latex>\<open>}\<close> _ \<^latex>\<open>\\textsf{\<close>of\<^latex>\<open>}\<close>/ _)" 10)
15469
nipkow
parents:
diff changeset
    22
16110
c423bb89186d added \nexists
nipkow
parents: 15690
diff changeset
    23
15469
nipkow
parents:
diff changeset
    24
(* SETS *)
nipkow
parents:
diff changeset
    25
nipkow
parents:
diff changeset
    26
(* empty set *)
27688
397de75836a1 *** empty log message ***
nipkow
parents: 27487
diff changeset
    27
notation (latex)
30304
d8e4cd2ac2a1 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents: 29493
diff changeset
    28
  "Set.empty" ("\<emptyset>")
15469
nipkow
parents:
diff changeset
    29
nipkow
parents:
diff changeset
    30
(* insert *)
nipkow
parents:
diff changeset
    31
translations 
31462
4fcbf17b5a98 Set.insert with authentic syntax
haftmann
parents: 30663
diff changeset
    32
  "{x} \<union> A" <= "CONST insert x A"
15690
nipkow
parents: 15476
diff changeset
    33
  "{x,y}" <= "{x} \<union> {y}"
15469
nipkow
parents:
diff changeset
    34
  "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
27688
397de75836a1 *** empty log message ***
nipkow
parents: 27487
diff changeset
    35
  "{x}" <= "{x} \<union> \<emptyset>"
15469
nipkow
parents:
diff changeset
    36
nipkow
parents:
diff changeset
    37
(* set comprehension *)
nipkow
parents:
diff changeset
    38
syntax (latex output)
nipkow
parents:
diff changeset
    39
  "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ | _})")
41757
7bbd11360bd3 more pretty set comprehension sugar
nipkow
parents: 35251
diff changeset
    40
  "_CollectIn" :: "pttrn => 'a set => bool => 'a set"   ("(1{_ \<in> _ | _})")
15469
nipkow
parents:
diff changeset
    41
translations
nipkow
parents:
diff changeset
    42
  "_Collect p P"      <= "{p. P}"
15690
nipkow
parents: 15476
diff changeset
    43
  "_Collect p P"      <= "{p|xs. P}"
41757
7bbd11360bd3 more pretty set comprehension sugar
nipkow
parents: 35251
diff changeset
    44
  "_CollectIn p A P"  <= "{p : A. P}"
15469
nipkow
parents:
diff changeset
    45
56977
a33fe940a557 new syntax for card, normalized spacing for #
nipkow
parents: 56245
diff changeset
    46
(* card *)
a33fe940a557 new syntax for card, normalized spacing for #
nipkow
parents: 56245
diff changeset
    47
notation (latex output)
a33fe940a557 new syntax for card, normalized spacing for #
nipkow
parents: 56245
diff changeset
    48
  card  ("|_|")
a33fe940a557 new syntax for card, normalized spacing for #
nipkow
parents: 56245
diff changeset
    49
15469
nipkow
parents:
diff changeset
    50
(* LISTS *)
nipkow
parents:
diff changeset
    51
nipkow
parents:
diff changeset
    52
(* Cons *)
21210
c17fd2df4e9e renamed 'const_syntax' to 'notation';
wenzelm
parents: 19674
diff changeset
    53
notation (latex)
56977
a33fe940a557 new syntax for card, normalized spacing for #
nipkow
parents: 56245
diff changeset
    54
  Cons  ("_ \<cdot>/ _" [66,65] 65)
15469
nipkow
parents:
diff changeset
    55
nipkow
parents:
diff changeset
    56
(* length *)
21210
c17fd2df4e9e renamed 'const_syntax' to 'notation';
wenzelm
parents: 19674
diff changeset
    57
notation (latex output)
19674
22b635240905 const_syntax;
wenzelm
parents: 16110
diff changeset
    58
  length  ("|_|")
15469
nipkow
parents:
diff changeset
    59
nipkow
parents:
diff changeset
    60
(* nth *)
21210
c17fd2df4e9e renamed 'const_syntax' to 'notation';
wenzelm
parents: 19674
diff changeset
    61
notation (latex output)
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63414
diff changeset
    62
  nth  ("_\<^latex>\<open>\\ensuremath{_{[\\mathit{\<close>_\<^latex>\<open>}]}}\<close>" [1000,0] 1000)
15469
nipkow
parents:
diff changeset
    63
nipkow
parents:
diff changeset
    64
(* DUMMY *)
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63414
diff changeset
    65
consts DUMMY :: 'a ("\<^latex>\<open>\\_\<close>")
15469
nipkow
parents:
diff changeset
    66
nipkow
parents:
diff changeset
    67
(* THEOREMS *)
35251
e244adbbc28f modernized notation -- to make it work for authentic syntax;
wenzelm
parents: 31462
diff changeset
    68
notation (Rule output)
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63414
diff changeset
    69
  Pure.imp  ("\<^latex>\<open>\\mbox{}\\inferrule{\\mbox{\<close>_\<^latex>\<open>}}\<close>\<^latex>\<open>{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
35251
e244adbbc28f modernized notation -- to make it work for authentic syntax;
wenzelm
parents: 31462
diff changeset
    70
15469
nipkow
parents:
diff changeset
    71
syntax (Rule output)
nipkow
parents:
diff changeset
    72
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63414
diff changeset
    73
  ("\<^latex>\<open>\\mbox{}\\inferrule{\<close>_\<^latex>\<open>}\<close>\<^latex>\<open>{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
15469
nipkow
parents:
diff changeset
    74
nipkow
parents:
diff changeset
    75
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63414
diff changeset
    76
  ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\\\\\<close>/ _")
15469
nipkow
parents:
diff changeset
    77
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63414
diff changeset
    78
  "_asm" :: "prop \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>")
15469
nipkow
parents:
diff changeset
    79
35251
e244adbbc28f modernized notation -- to make it work for authentic syntax;
wenzelm
parents: 31462
diff changeset
    80
notation (Axiom output)
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63414
diff changeset
    81
  "Trueprop"  ("\<^latex>\<open>\\mbox{}\\inferrule{\\mbox{}}{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
22328
cc403d881873 added print-mode Axiom to print theorems without premises with a rule on top.
schirmer
parents: 21210
diff changeset
    82
35251
e244adbbc28f modernized notation -- to make it work for authentic syntax;
wenzelm
parents: 31462
diff changeset
    83
notation (IfThen output)
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63414
diff changeset
    84
  Pure.imp  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _/ \<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
15469
nipkow
parents:
diff changeset
    85
syntax (IfThen output)
nipkow
parents:
diff changeset
    86
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63414
diff changeset
    87
  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63414
diff changeset
    88
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close> /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63414
diff changeset
    89
  "_asm" :: "prop \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>")
15469
nipkow
parents:
diff changeset
    90
35251
e244adbbc28f modernized notation -- to make it work for authentic syntax;
wenzelm
parents: 31462
diff changeset
    91
notation (IfThenNoBox output)
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63414
diff changeset
    92
  Pure.imp  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _/ \<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
15469
nipkow
parents:
diff changeset
    93
syntax (IfThenNoBox output)
nipkow
parents:
diff changeset
    94
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
63935
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63414
diff changeset
    95
  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
aa1fe1103ab8 raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents: 63414
diff changeset
    96
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
15469
nipkow
parents:
diff changeset
    97
  "_asm" :: "prop \<Rightarrow> asms" ("_")
nipkow
parents:
diff changeset
    98
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 56977
diff changeset
    99
setup\<open>
49628
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   100
  let
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   101
    fun pretty ctxt c =
56002
2028467b4df4 tuned signature;
wenzelm
parents: 55955
diff changeset
   102
      let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c
49628
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   103
      in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   104
            Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   105
      end
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   106
  in
67386
998e01d6f8fd clarified modules;
wenzelm
parents: 66527
diff changeset
   107
    Document_Antiquotation.setup @{binding "const_typ"}
63120
629a4c5e953e embedded content may be delimited via cartouches;
wenzelm
parents: 62522
diff changeset
   108
     (Scan.lift Args.embedded_inner_syntax)
49628
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   109
       (fn {source = src, context = ctxt, ...} => fn arg =>
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   110
          Thy_Output.output ctxt
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   111
            (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   112
  end;
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 56977
diff changeset
   113
\<close>
49628
8262d35eff20 new antiquotation const_typ
nipkow
parents: 41757
diff changeset
   114
63414
beb987127d0f new style dummy_pats
nipkow
parents: 63120
diff changeset
   115
setup\<open>
beb987127d0f new style dummy_pats
nipkow
parents: 63120
diff changeset
   116
let
beb987127d0f new style dummy_pats
nipkow
parents: 63120
diff changeset
   117
  fun dummy_pats (wrap $ (eq $ lhs $ rhs)) =
beb987127d0f new style dummy_pats
nipkow
parents: 63120
diff changeset
   118
    let
beb987127d0f new style dummy_pats
nipkow
parents: 63120
diff changeset
   119
      val rhs_vars = Term.add_vars rhs [];
beb987127d0f new style dummy_pats
nipkow
parents: 63120
diff changeset
   120
      fun dummy (v as Var (ixn as (_, T))) =
beb987127d0f new style dummy_pats
nipkow
parents: 63120
diff changeset
   121
            if member (op = ) rhs_vars ixn then v else Const (@{const_name DUMMY}, T)
beb987127d0f new style dummy_pats
nipkow
parents: 63120
diff changeset
   122
        | dummy (t $ u) = dummy t $ dummy u
beb987127d0f new style dummy_pats
nipkow
parents: 63120
diff changeset
   123
        | dummy (Abs (n, T, b)) = Abs (n, T, dummy b)
beb987127d0f new style dummy_pats
nipkow
parents: 63120
diff changeset
   124
        | dummy t = t;
beb987127d0f new style dummy_pats
nipkow
parents: 63120
diff changeset
   125
    in wrap $ (eq $ dummy lhs $ rhs) end
beb987127d0f new style dummy_pats
nipkow
parents: 63120
diff changeset
   126
in
beb987127d0f new style dummy_pats
nipkow
parents: 63120
diff changeset
   127
  Term_Style.setup @{binding dummy_pats} (Scan.succeed (K dummy_pats))
beb987127d0f new style dummy_pats
nipkow
parents: 63120
diff changeset
   128
end
beb987127d0f new style dummy_pats
nipkow
parents: 63120
diff changeset
   129
\<close>
beb987127d0f new style dummy_pats
nipkow
parents: 63120
diff changeset
   130
66527
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   131
setup \<open>
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   132
let
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   133
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   134
fun eta_expand Ts t xs = case t of
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   135
    Abs(x,T,t) =>
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   136
      let val (t', xs') = eta_expand (T::Ts) t xs
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   137
      in (Abs (x, T, t'), xs') end
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   138
  | _ =>
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   139
      let
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   140
        val (a,ts) = strip_comb t (* assume a atomic *)
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   141
        val (ts',xs') = fold_map (eta_expand Ts) ts xs
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   142
        val t' = list_comb (a, ts');
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   143
        val Bs = binder_types (fastype_of1 (Ts,t));
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   144
        val n = Int.min (length Bs, length xs');
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   145
        val bs = map Bound ((n - 1) downto 0);
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   146
        val xBs = ListPair.zip (xs',Bs);
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   147
        val xs'' = drop n xs';
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   148
        val t'' = fold_rev Term.abs xBs (list_comb(t', bs))
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   149
      in (t'', xs'') end
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   150
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   151
val style_eta_expand =
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   152
  (Scan.repeat Args.name) >> (fn xs => fn ctxt => fn t => fst (eta_expand [] t xs))
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   153
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   154
in Term_Style.setup @{binding eta_expand} style_eta_expand end
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   155
\<close>
7ca69030a2af added eta_expansion and its documentation.
nipkow
parents: 63935
diff changeset
   156
15469
nipkow
parents:
diff changeset
   157
end
55077
4cf280104b85 fixed typo
blanchet
parents: 49628
diff changeset
   158
(*>*)