src/HOL/Library/LaTeXsugar.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (4 months ago)
changeset 69946 494934c30f38
parent 69593 3dda49e08b9d
permissions -rw-r--r--
improved code equations taken over from AFP
nipkow@15469
     1
(*  Title:      HOL/Library/LaTeXsugar.thy
blanchet@55077
     2
    Author:     Gerwin Klein, Tobias Nipkow, Norbert Schirmer
nipkow@15469
     3
    Copyright   2005 NICTA and TUM
nipkow@15469
     4
*)
nipkow@15469
     5
nipkow@15469
     6
(*<*)
nipkow@15469
     7
theory LaTeXsugar
haftmann@30663
     8
imports Main
nipkow@15469
     9
begin
nipkow@15469
    10
nipkow@15469
    11
(* LOGIC *)
wenzelm@21210
    12
notation (latex output)
wenzelm@63935
    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)
wenzelm@19674
    14
nipkow@15469
    15
syntax (latex output)
nipkow@15469
    16
nipkow@15469
    17
  "_Let"        :: "[letbinds, 'a] => 'a"
wenzelm@63935
    18
  ("(\<^latex>\<open>\\textsf{\<close>let\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textsf{\<close>in\<^latex>\<open>}\<close> (_))" 10)
nipkow@15469
    19
nipkow@15469
    20
  "_case_syntax":: "['a, cases_syn] => 'b"
wenzelm@63935
    21
  ("(\<^latex>\<open>\\textsf{\<close>case\<^latex>\<open>}\<close> _ \<^latex>\<open>\\textsf{\<close>of\<^latex>\<open>}\<close>/ _)" 10)
nipkow@15469
    22
nipkow@16110
    23
nipkow@15469
    24
(* SETS *)
nipkow@15469
    25
nipkow@15469
    26
(* empty set *)
nipkow@27688
    27
notation (latex)
haftmann@30304
    28
  "Set.empty" ("\<emptyset>")
nipkow@15469
    29
nipkow@15469
    30
(* insert *)
nipkow@15469
    31
translations 
haftmann@31462
    32
  "{x} \<union> A" <= "CONST insert x A"
nipkow@15690
    33
  "{x,y}" <= "{x} \<union> {y}"
nipkow@15469
    34
  "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
nipkow@27688
    35
  "{x}" <= "{x} \<union> \<emptyset>"
nipkow@15469
    36
nipkow@15469
    37
(* set comprehension *)
nipkow@15469
    38
syntax (latex output)
nipkow@15469
    39
  "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ | _})")
nipkow@41757
    40
  "_CollectIn" :: "pttrn => 'a set => bool => 'a set"   ("(1{_ \<in> _ | _})")
nipkow@15469
    41
translations
nipkow@15469
    42
  "_Collect p P"      <= "{p. P}"
nipkow@15690
    43
  "_Collect p P"      <= "{p|xs. P}"
nipkow@41757
    44
  "_CollectIn p A P"  <= "{p : A. P}"
nipkow@15469
    45
nipkow@56977
    46
(* card *)
nipkow@56977
    47
notation (latex output)
nipkow@56977
    48
  card  ("|_|")
nipkow@56977
    49
nipkow@15469
    50
(* LISTS *)
nipkow@15469
    51
nipkow@15469
    52
(* Cons *)
wenzelm@21210
    53
notation (latex)
nipkow@56977
    54
  Cons  ("_ \<cdot>/ _" [66,65] 65)
nipkow@15469
    55
nipkow@15469
    56
(* length *)
wenzelm@21210
    57
notation (latex output)
wenzelm@19674
    58
  length  ("|_|")
nipkow@15469
    59
nipkow@15469
    60
(* nth *)
wenzelm@21210
    61
notation (latex output)
wenzelm@63935
    62
  nth  ("_\<^latex>\<open>\\ensuremath{_{[\\mathit{\<close>_\<^latex>\<open>}]}}\<close>" [1000,0] 1000)
nipkow@15469
    63
nipkow@15469
    64
(* DUMMY *)
wenzelm@63935
    65
consts DUMMY :: 'a ("\<^latex>\<open>\\_\<close>")
nipkow@15469
    66
nipkow@15469
    67
(* THEOREMS *)
wenzelm@35251
    68
notation (Rule output)
wenzelm@63935
    69
  Pure.imp  ("\<^latex>\<open>\\mbox{}\\inferrule{\\mbox{\<close>_\<^latex>\<open>}}\<close>\<^latex>\<open>{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
wenzelm@35251
    70
nipkow@15469
    71
syntax (Rule output)
nipkow@15469
    72
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
wenzelm@63935
    73
  ("\<^latex>\<open>\\mbox{}\\inferrule{\<close>_\<^latex>\<open>}\<close>\<^latex>\<open>{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
nipkow@15469
    74
nipkow@15469
    75
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
wenzelm@63935
    76
  ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\\\\\<close>/ _")
nipkow@15469
    77
wenzelm@63935
    78
  "_asm" :: "prop \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>")
nipkow@15469
    79
wenzelm@35251
    80
notation (Axiom output)
wenzelm@63935
    81
  "Trueprop"  ("\<^latex>\<open>\\mbox{}\\inferrule{\\mbox{}}{\\mbox{\<close>_\<^latex>\<open>}}\<close>")
schirmer@22328
    82
wenzelm@35251
    83
notation (IfThen output)
wenzelm@63935
    84
  Pure.imp  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _/ \<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
nipkow@15469
    85
syntax (IfThen output)
nipkow@15469
    86
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
wenzelm@63935
    87
  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
wenzelm@63935
    88
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close> /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
wenzelm@63935
    89
  "_asm" :: "prop \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>")
nipkow@15469
    90
wenzelm@35251
    91
notation (IfThenNoBox output)
wenzelm@63935
    92
  Pure.imp  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _/ \<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
nipkow@15469
    93
syntax (IfThenNoBox output)
nipkow@15469
    94
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
wenzelm@63935
    95
  ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
wenzelm@63935
    96
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
nipkow@15469
    97
  "_asm" :: "prop \<Rightarrow> asms" ("_")
nipkow@15469
    98
wenzelm@67463
    99
setup \<open>
wenzelm@69592
   100
  Thy_Output.antiquotation_pretty_source_embedded \<^binding>\<open>const_typ\<close>
wenzelm@69592
   101
    (Scan.lift Args.embedded_inner_syntax)
wenzelm@67463
   102
    (fn ctxt => fn c =>
nipkow@69081
   103
      let val tc = Proof_Context.read_const {proper = false, strict = false} ctxt c in
wenzelm@67505
   104
        Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
wenzelm@67505
   105
          Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
wenzelm@67463
   106
      end)
wenzelm@60500
   107
\<close>
nipkow@49628
   108
nipkow@63414
   109
setup\<open>
nipkow@63414
   110
let
nipkow@63414
   111
  fun dummy_pats (wrap $ (eq $ lhs $ rhs)) =
nipkow@63414
   112
    let
nipkow@63414
   113
      val rhs_vars = Term.add_vars rhs [];
nipkow@63414
   114
      fun dummy (v as Var (ixn as (_, T))) =
wenzelm@69593
   115
            if member ((=) ) rhs_vars ixn then v else Const (\<^const_name>\<open>DUMMY\<close>, T)
nipkow@63414
   116
        | dummy (t $ u) = dummy t $ dummy u
nipkow@63414
   117
        | dummy (Abs (n, T, b)) = Abs (n, T, dummy b)
nipkow@63414
   118
        | dummy t = t;
nipkow@63414
   119
    in wrap $ (eq $ dummy lhs $ rhs) end
nipkow@63414
   120
in
wenzelm@69593
   121
  Term_Style.setup \<^binding>\<open>dummy_pats\<close> (Scan.succeed (K dummy_pats))
nipkow@63414
   122
end
nipkow@63414
   123
\<close>
nipkow@63414
   124
nipkow@66527
   125
setup \<open>
nipkow@66527
   126
let
nipkow@66527
   127
nipkow@66527
   128
fun eta_expand Ts t xs = case t of
nipkow@66527
   129
    Abs(x,T,t) =>
nipkow@66527
   130
      let val (t', xs') = eta_expand (T::Ts) t xs
nipkow@66527
   131
      in (Abs (x, T, t'), xs') end
nipkow@66527
   132
  | _ =>
nipkow@66527
   133
      let
nipkow@66527
   134
        val (a,ts) = strip_comb t (* assume a atomic *)
nipkow@66527
   135
        val (ts',xs') = fold_map (eta_expand Ts) ts xs
nipkow@66527
   136
        val t' = list_comb (a, ts');
nipkow@66527
   137
        val Bs = binder_types (fastype_of1 (Ts,t));
nipkow@66527
   138
        val n = Int.min (length Bs, length xs');
nipkow@66527
   139
        val bs = map Bound ((n - 1) downto 0);
nipkow@66527
   140
        val xBs = ListPair.zip (xs',Bs);
nipkow@66527
   141
        val xs'' = drop n xs';
nipkow@66527
   142
        val t'' = fold_rev Term.abs xBs (list_comb(t', bs))
nipkow@66527
   143
      in (t'', xs'') end
nipkow@66527
   144
nipkow@66527
   145
val style_eta_expand =
nipkow@66527
   146
  (Scan.repeat Args.name) >> (fn xs => fn ctxt => fn t => fst (eta_expand [] t xs))
nipkow@66527
   147
wenzelm@69593
   148
in Term_Style.setup \<^binding>\<open>eta_expand\<close> style_eta_expand end
nipkow@66527
   149
\<close>
nipkow@66527
   150
nipkow@15469
   151
end
blanchet@55077
   152
(*>*)