author | nipkow |
Mon, 30 May 2022 20:58:45 +0200 | |
changeset 75496 | 99b37c391433 |
parent 74563 | 042041c0ebeb |
child 78471 | 7c3d681f11d4 |
permissions | -rw-r--r-- |
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" <= "{p|xs. 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 print-mode 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> |
73761 | 100 |
Document_Output.antiquotation_pretty_source_embedded \<^binding>\<open>const_typ\<close> |
74563 | 101 |
(Scan.lift Parse.embedded_inner_syntax) |
67463 | 102 |
(fn ctxt => fn c => |
69081
0b403ce1e8f8
const_typ also works for fixed variables - useful primarily for locales
nipkow
parents:
67505
diff
changeset
|
103 |
let val tc = Proof_Context.read_const {proper = false, strict = false} ctxt c in |
73761 | 104 |
Pretty.block [Document_Output.pretty_term ctxt tc, Pretty.str " ::", |
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67463
diff
changeset
|
105 |
Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)] |
67463 | 106 |
end) |
60500 | 107 |
\<close> |
49628 | 108 |
|
63414 | 109 |
setup\<open> |
110 |
let |
|
111 |
fun dummy_pats (wrap $ (eq $ lhs $ rhs)) = |
|
112 |
let |
|
113 |
val rhs_vars = Term.add_vars rhs []; |
|
114 |
fun dummy (v as Var (ixn as (_, T))) = |
|
69593 | 115 |
if member ((=) ) rhs_vars ixn then v else Const (\<^const_name>\<open>DUMMY\<close>, T) |
63414 | 116 |
| dummy (t $ u) = dummy t $ dummy u |
117 |
| dummy (Abs (n, T, b)) = Abs (n, T, dummy b) |
|
118 |
| dummy t = t; |
|
119 |
in wrap $ (eq $ dummy lhs $ rhs) end |
|
120 |
in |
|
69593 | 121 |
Term_Style.setup \<^binding>\<open>dummy_pats\<close> (Scan.succeed (K dummy_pats)) |
63414 | 122 |
end |
123 |
\<close> |
|
124 |
||
66527 | 125 |
setup \<open> |
126 |
let |
|
127 |
||
128 |
fun eta_expand Ts t xs = case t of |
|
129 |
Abs(x,T,t) => |
|
130 |
let val (t', xs') = eta_expand (T::Ts) t xs |
|
131 |
in (Abs (x, T, t'), xs') end |
|
132 |
| _ => |
|
133 |
let |
|
134 |
val (a,ts) = strip_comb t (* assume a atomic *) |
|
135 |
val (ts',xs') = fold_map (eta_expand Ts) ts xs |
|
136 |
val t' = list_comb (a, ts'); |
|
137 |
val Bs = binder_types (fastype_of1 (Ts,t)); |
|
138 |
val n = Int.min (length Bs, length xs'); |
|
139 |
val bs = map Bound ((n - 1) downto 0); |
|
140 |
val xBs = ListPair.zip (xs',Bs); |
|
141 |
val xs'' = drop n xs'; |
|
142 |
val t'' = fold_rev Term.abs xBs (list_comb(t', bs)) |
|
143 |
in (t'', xs'') end |
|
144 |
||
145 |
val style_eta_expand = |
|
146 |
(Scan.repeat Args.name) >> (fn xs => fn ctxt => fn t => fst (eta_expand [] t xs)) |
|
147 |
||
69593 | 148 |
in Term_Style.setup \<^binding>\<open>eta_expand\<close> style_eta_expand end |
66527 | 149 |
\<close> |
150 |
||
15469 | 151 |
end |
55077 | 152 |
(*>*) |