author  nipkow 
Mon, 28 Aug 2017 18:27:16 +0200  
changeset 66527  7ca69030a2af 
parent 63935  aa1fe1103ab8 
child 67386  998e01d6f8fd 
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 

60500  99 
setup\<open> 
49628  100 
let 
101 
fun pretty ctxt c = 

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

105 
end 

106 
in 

107 
Thy_Output.antiquotation @{binding "const_typ"} 

63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
62522
diff
changeset

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

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

112 
end; 

60500  113 
\<close> 
49628  114 

63414  115 
setup\<open> 
116 
let 

117 
fun dummy_pats (wrap $ (eq $ lhs $ rhs)) = 

118 
let 

119 
val rhs_vars = Term.add_vars rhs []; 

120 
fun dummy (v as Var (ixn as (_, T))) = 

121 
if member (op = ) rhs_vars ixn then v else Const (@{const_name DUMMY}, T) 

122 
 dummy (t $ u) = dummy t $ dummy u 

123 
 dummy (Abs (n, T, b)) = Abs (n, T, dummy b) 

124 
 dummy t = t; 

125 
in wrap $ (eq $ dummy lhs $ rhs) end 

126 
in 

127 
Term_Style.setup @{binding dummy_pats} (Scan.succeed (K dummy_pats)) 

128 
end 

129 
\<close> 

130 

66527  131 
setup \<open> 
132 
let 

133 

134 
fun eta_expand Ts t xs = case t of 

135 
Abs(x,T,t) => 

136 
let val (t', xs') = eta_expand (T::Ts) t xs 

137 
in (Abs (x, T, t'), xs') end 

138 
 _ => 

139 
let 

140 
val (a,ts) = strip_comb t (* assume a atomic *) 

141 
val (ts',xs') = fold_map (eta_expand Ts) ts xs 

142 
val t' = list_comb (a, ts'); 

143 
val Bs = binder_types (fastype_of1 (Ts,t)); 

144 
val n = Int.min (length Bs, length xs'); 

145 
val bs = map Bound ((n  1) downto 0); 

146 
val xBs = ListPair.zip (xs',Bs); 

147 
val xs'' = drop n xs'; 

148 
val t'' = fold_rev Term.abs xBs (list_comb(t', bs)) 

149 
in (t'', xs'') end 

150 

151 
val style_eta_expand = 

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

153 

154 
in Term_Style.setup @{binding eta_expand} style_eta_expand end 

155 
\<close> 

156 

15469  157 
end 
55077  158 
(*>*) 