Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: LaTeXsugar.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Library/LaTeXsugar.thy
    Author:     Gerwin Klein, Tobias Nipkow, Norbert Schirmer
    Copyright   2005 NICTA and TUM
*)

(*<*)
theory LaTeXsugar
imports Main
begin

(* LOGIC *)
notation (latex output)
  If  ("(\<^latex>\\\textsf{\if\<^latex>\}\ (_)/ \<^latex>\\\textsf{\then\<^latex>\}\ (_)/ \<^latex>\\\textsf{\else\<^latex>\}\ (_))" 10)

syntax (latex output)

  "_Let"        :: "[letbinds, 'a] => 'a"
  ("(\<^latex>\\\textsf{\let\<^latex>\}\ (_)/ \<^latex>\\\textsf{\in\<^latex>\}\ (_))" 10)

  "_case_syntax":: "['a, cases_syn] => 'b"
  ("(\<^latex>\\\textsf{\case\<^latex>\}\ _ \<^latex>\\\textsf{\of\<^latex>\}\/ _)" 10)

(* SETS *)

(* empty set *)
notation (latex)
  "Set.empty" ("\")

(* insert *)
translations
  "{x} \ A" <= "CONST insert x A"
  "{x,y}" <= "{x} \ {y}"
  "{x,y} \ A" <= "{x} \ ({y} \ A)"
  "{x}" <= "{x} \ \"

(* set comprehension *)
syntax (latex output)
  "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ | _})")
  "_CollectIn" :: "pttrn => 'a set => bool => 'a set"   ("(1{_ \ _ | _})")
translations
  "_Collect p P"      <= "{p. P}"
  "_Collect p P"      <= "{p|xs. P}"
  "_CollectIn p A P"  <= "{p : A. P}"

(* card *)
notation (latex output)
  card  ("|_|")

(* LISTS *)

(* Cons *)
notation (latex)
  Cons  ("_ \/ _" [66,65] 65)

(* length *)
notation (latex output)
  length  ("|_|")

(* nth *)
notation (latex output)
  nth  ("_\<^latex>\\\ensuremath{_{[\\mathit{\_\<^latex>\}]}}\" [1000,0] 1000)

(* DUMMY *)
consts DUMMY :: 'a ("\<^latex>\\\_\")

(* THEOREMS *)
notation (Rule output)
  Pure.imp  ("\<^latex>\\\mbox{}\\inferrule{\\mbox{\_\<^latex>\}}\\<^latex>\{\\mbox{\_\<^latex>\}}\")

syntax (Rule output)
  "_bigimpl" :: "asms \ prop \ prop"
  ("\<^latex>\\\mbox{}\\inferrule{\_\<^latex>\}\\<^latex>\{\\mbox{\_\<^latex>\}}\")

  "_asms" :: "prop \ asms \ asms"
  ("\<^latex>\\\mbox{\_\<^latex>\}\\\\\/ _")

  "_asm" :: "prop \ asms" ("\<^latex>\\\mbox{\_\<^latex>\}\")

notation (Axiom output)
  "Trueprop"  ("\<^latex>\\\mbox{}\\inferrule{\\mbox{}}{\\mbox{\_\<^latex>\}}\")

notation (IfThen output)
  Pure.imp  ("\<^latex>\{\\normalsize{}\If\<^latex>\\\,}\ _/ \<^latex>\{\\normalsize \\,\then\<^latex>\\\,}\/ _.")
syntax (IfThen output)
  "_bigimpl" :: "asms \ prop \ prop"
  ("\<^latex>\{\\normalsize{}\If\<^latex>\\\,}\ _ /\<^latex>\{\\normalsize \\,\then\<^latex>\\\,}\/ _.")
  "_asms" :: "prop \ asms \ asms" ("\<^latex>\\\mbox{\_\<^latex>\}\ /\<^latex>\{\\normalsize \\,\and\<^latex>\\\,}\/ _")
  "_asm" :: "prop \ asms" ("\<^latex>\\\mbox{\_\<^latex>\}\")

notation (IfThenNoBox output)
  Pure.imp  ("\<^latex>\{\\normalsize{}\If\<^latex>\\\,}\ _/ \<^latex>\{\\normalsize \\,\then\<^latex>\\\,}\/ _.")
syntax (IfThenNoBox output)
  "_bigimpl" :: "asms \ prop \ prop"
  ("\<^latex>\{\\normalsize{}\If\<^latex>\\\,}\ _ /\<^latex>\{\\normalsize \\,\then\<^latex>\\\,}\/ _.")
  "_asms" :: "prop \ asms \ asms" ("_ /\<^latex>\{\\normalsize \\,\and\<^latex>\\\,}\/ _")
  "_asm" :: "prop \ asms" ("_")

setup \<open>
  Thy_Output.antiquotation_pretty_source_embedded \<^binding>\<open>const_typ\<close>
    (Scan.lift Args.embedded_inner_syntax)
    (fn ctxt => fn c =>
      let val tc = Proof_Context.read_const {proper = false, strict = false} ctxt c in
        Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
          Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
      end)
\<close>

setup\<open>
let
  fun dummy_pats (wrap $ (eq $ lhs $ rhs)) =
    let
      val rhs_vars = Term.add_vars rhs [];
      fun dummy (v as Var (ixn as (_, T))) =
            if member ((=) ) rhs_vars ixn then v else Const (\<^const_name>\<open>DUMMY\<close>, T)
        | dummy (t $ u) = dummy t $ dummy u
        | dummy (Abs (n, T, b)) = Abs (n, T, dummy b)
        | dummy t = t;
    in wrap $ (eq $ dummy lhs $ rhs) end
in
  Term_Style.setup \<^binding>\<open>dummy_pats\<close> (Scan.succeed (K dummy_pats))
end
\<close>

setup \<open>
let

fun eta_expand Ts t xs = case t of
    Abs(x,T,t) =>
      let val (t', xs') = eta_expand (T::Ts) t xs
      in (Abs (x, T, t'), xs') end
  | _ =>
      let
        val (a,ts) = strip_comb t (* assume a atomic *)
        val (ts',xs') = fold_map (eta_expand Ts) ts xs
        val t' = list_comb (a, ts');
        val Bs = binder_types (fastype_of1 (Ts,t));
        val n = Int.min (length Bs, length xs');
        val bs = map Bound ((n - 1) downto 0);
        val xBs = ListPair.zip (xs',Bs);
        val xs'' = drop n xs';
        val t'' = fold_rev Term.abs xBs (list_comb(t', bs))
      in (t'', xs'') end

val style_eta_expand =
  (Scan.repeat Args.name) >> (fn xs => fn ctxt => fn t => fst (eta_expand [] t xs))

in Term_Style.setup \<^binding>\<open>eta_expand\<close> style_eta_expand end
\<close>

end
(*>*)

¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.