author  wenzelm 
Thu, 06 Mar 2014 13:44:01 +0100  
changeset 55954  a29aefc88c8d 
parent 55114  0ee5c17f2207 
child 55955  e8f1bf005661 
permissions  rwrr 
15469  1 
(* Title: HOL/Library/LaTeXsugar.thy 
55077  2 
Author: Gerwin Klein, Tobias Nipkow, Norbert Schirmer 
15469  3 
Copyright 2005 NICTA and TUM 
4 
*) 

5 

6 
(*<*) 

7 
theory LaTeXsugar 

30663
0b6aff7451b2
Main is (Complex_Main) base entry point in library theories
haftmann
parents:
30304
diff
changeset

8 
imports Main 
15469  9 
begin 
10 

11 
(* LOGIC *) 

21210  12 
notation (latex output) 
19674  13 
If ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10) 
14 

15469  15 
syntax (latex output) 
16 

17 
"_Let" :: "[letbinds, 'a] => 'a" 

18 
("(\<^raw:\textsf{>let\<^raw:}> (_)/ \<^raw:\textsf{>in\<^raw:}> (_))" 10) 

19 

20 
"_case_syntax":: "['a, cases_syn] => 'b" 

21 
("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10) 

22 

16110  23 
(* should become standard syntax once xsymbols supports it *) 
24 
syntax (latex) 

25 
nexists :: "('a => bool) => bool" (binder "\<nexists>" 10) 

26 
translations 

27 
"\<nexists>x. P" <= "\<not>(\<exists>x. P)" 

28 

15469  29 
(* SETS *) 
30 

31 
(* empty set *) 

27688  32 
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

33 
"Set.empty" ("\<emptyset>") 
15469  34 

35 
(* insert *) 

36 
translations 

31462  37 
"{x} \<union> A" <= "CONST insert x A" 
15690  38 
"{x,y}" <= "{x} \<union> {y}" 
15469  39 
"{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)" 
27688  40 
"{x}" <= "{x} \<union> \<emptyset>" 
15469  41 

42 
(* set comprehension *) 

43 
syntax (latex output) 

44 
"_Collect" :: "pttrn => bool => 'a set" ("(1{_  _})") 

41757  45 
"_CollectIn" :: "pttrn => 'a set => bool => 'a set" ("(1{_ \<in> _  _})") 
15469  46 
translations 
47 
"_Collect p P" <= "{p. P}" 

15690  48 
"_Collect p P" <= "{pxs. P}" 
41757  49 
"_CollectIn p A P" <= "{p : A. P}" 
15469  50 

51 
(* LISTS *) 

52 

53 
(* Cons *) 

21210  54 
notation (latex) 
19674  55 
Cons ("_\<cdot>/_" [66,65] 65) 
15469  56 

57 
(* length *) 

21210  58 
notation (latex output) 
19674  59 
length ("_") 
15469  60 

61 
(* nth *) 

21210  62 
notation (latex output) 
19674  63 
nth ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000) 
15469  64 

65 
(* DUMMY *) 

66 
consts DUMMY :: 'a ("\<^raw:\_>") 

67 

68 
(* THEOREMS *) 

35251
e244adbbc28f
modernized notation  to make it work for authentic syntax;
wenzelm
parents:
31462
diff
changeset

69 
notation (Rule output) 
e244adbbc28f
modernized notation  to make it work for authentic syntax;
wenzelm
parents:
31462
diff
changeset

70 
"==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>") 
e244adbbc28f
modernized notation  to make it work for authentic syntax;
wenzelm
parents:
31462
diff
changeset

71 

15469  72 
syntax (Rule output) 
73 
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" 

74 
("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>") 

75 

76 
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 

77 
("\<^raw:\mbox{>_\<^raw:}\\>/ _") 

78 

79 
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>") 

80 

35251
e244adbbc28f
modernized notation  to make it work for authentic syntax;
wenzelm
parents:
31462
diff
changeset

81 
notation (Axiom output) 
e244adbbc28f
modernized notation  to make it work for authentic syntax;
wenzelm
parents:
31462
diff
changeset

82 
"Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>") 
22328
cc403d881873
added printmode Axiom to print theorems without premises with a rule on top.
schirmer
parents:
21210
diff
changeset

83 

35251
e244adbbc28f
modernized notation  to make it work for authentic syntax;
wenzelm
parents:
31462
diff
changeset

84 
notation (IfThen output) 
e244adbbc28f
modernized notation  to make it work for authentic syntax;
wenzelm
parents:
31462
diff
changeset

85 
"==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") 
15469  86 
syntax (IfThen output) 
87 
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" 

25467  88 
("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") 
89 
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") 

15469  90 
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>") 
91 

35251
e244adbbc28f
modernized notation  to make it work for authentic syntax;
wenzelm
parents:
31462
diff
changeset

92 
notation (IfThenNoBox output) 
e244adbbc28f
modernized notation  to make it work for authentic syntax;
wenzelm
parents:
31462
diff
changeset

93 
"==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") 
15469  94 
syntax (IfThenNoBox output) 
95 
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" 

25467  96 
("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") 
97 
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") 

15469  98 
"_asm" :: "prop \<Rightarrow> asms" ("_") 
99 

49628  100 
setup{* 
101 
let 

102 
fun pretty ctxt c = 

55954  103 
let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} dummyT c 
49628  104 
in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::", 
105 
Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)] 

106 
end 

107 
in 

108 
Thy_Output.antiquotation @{binding "const_typ"} 

55111  109 
(Scan.lift Args.name_inner_syntax) 
49628  110 
(fn {source = src, context = ctxt, ...} => fn arg => 
111 
Thy_Output.output ctxt 

112 
(Thy_Output.maybe_pretty_source pretty ctxt src [arg])) 

113 
end; 

114 
*} 

115 

15469  116 
end 
55077  117 
(*>*) 