author  wenzelm 
Thu, 18 Jan 2018 21:41:30 +0100  
changeset 67463  a5ca98950a91 
parent 67399  eab6ce8368fa 
child 67505  ceb324e34c14 
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) 
63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63414
diff
changeset

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) 
19674  14 

15469  15 
syntax (latex output) 
16 

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

63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63414
diff
changeset

18 
("(\<^latex>\<open>\\textsf{\<close>let\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textsf{\<close>in\<^latex>\<open>}\<close> (_))" 10) 
15469  19 

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

63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63414
diff
changeset

21 
("(\<^latex>\<open>\\textsf{\<close>case\<^latex>\<open>}\<close> _ \<^latex>\<open>\\textsf{\<close>of\<^latex>\<open>}\<close>/ _)" 10) 
15469  22 

16110  23 

15469  24 
(* SETS *) 
25 

26 
(* empty set *) 

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

28 
"Set.empty" ("\<emptyset>") 
15469  29 

30 
(* insert *) 

31 
translations 

31462  32 
"{x} \<union> A" <= "CONST insert x A" 
15690  33 
"{x,y}" <= "{x} \<union> {y}" 
15469  34 
"{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)" 
27688  35 
"{x}" <= "{x} \<union> \<emptyset>" 
15469  36 

37 
(* set comprehension *) 

38 
syntax (latex output) 

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

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

15690  43 
"_Collect p P" <= "{pxs. P}" 
41757  44 
"_CollectIn p A P" <= "{p : A. P}" 
15469  45 

56977  46 
(* card *) 
47 
notation (latex output) 

48 
card ("_") 

49 

15469  50 
(* LISTS *) 
51 

52 
(* Cons *) 

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

56 
(* length *) 

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

60 
(* nth *) 

21210  61 
notation (latex output) 
63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63414
diff
changeset

62 
nth ("_\<^latex>\<open>\\ensuremath{_{[\\mathit{\<close>_\<^latex>\<open>}]}}\<close>" [1000,0] 1000) 
15469  63 

64 
(* DUMMY *) 

63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63414
diff
changeset

65 
consts DUMMY :: 'a ("\<^latex>\<open>\\_\<close>") 
15469  66 

67 
(* THEOREMS *) 

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

68 
notation (Rule output) 
63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63414
diff
changeset

69 
Pure.imp ("\<^latex>\<open>\\mbox{}\\inferrule{\\mbox{\<close>_\<^latex>\<open>}}\<close>\<^latex>\<open>{\\mbox{\<close>_\<^latex>\<open>}}\<close>") 
35251
e244adbbc28f
modernized notation  to make it work for authentic syntax;
wenzelm
parents:
31462
diff
changeset

70 

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

63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63414
diff
changeset

73 
("\<^latex>\<open>\\mbox{}\\inferrule{\<close>_\<^latex>\<open>}\<close>\<^latex>\<open>{\\mbox{\<close>_\<^latex>\<open>}}\<close>") 
15469  74 

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

63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63414
diff
changeset

76 
("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\\\\\<close>/ _") 
15469  77 

63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63414
diff
changeset

78 
"_asm" :: "prop \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>") 
15469  79 

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

80 
notation (Axiom output) 
63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63414
diff
changeset

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

82 

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

83 
notation (IfThen output) 
63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63414
diff
changeset

84 
Pure.imp ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _/ \<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.") 
15469  85 
syntax (IfThen output) 
86 
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" 

63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63414
diff
changeset

87 
("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.") 
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63414
diff
changeset

88 
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close> /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _") 
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63414
diff
changeset

89 
"_asm" :: "prop \<Rightarrow> asms" ("\<^latex>\<open>\\mbox{\<close>_\<^latex>\<open>}\<close>") 
15469  90 

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

91 
notation (IfThenNoBox output) 
63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63414
diff
changeset

92 
Pure.imp ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _/ \<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.") 
15469  93 
syntax (IfThenNoBox output) 
94 
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" 

63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63414
diff
changeset

95 
("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.") 
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63414
diff
changeset

96 
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _") 
15469  97 
"_asm" :: "prop \<Rightarrow> asms" ("_") 
98 

67463  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) 

60500  106 
\<close> 
49628  107 

63414  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))) = 

67399  114 
if member ((=) ) rhs_vars ixn then v else Const (@{const_name DUMMY}, T) 
63414  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 

66527  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 

15469  150 
end 
55077  151 
(*>*) 