(* 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)
¤
|
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.
|