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