63026
|
1 |
theory Setup
|
63555
|
2 |
imports Complex_Main "~~/src/HOL/Library/Multiset" "~~/src/HOL/Library/Lattice_Syntax"
|
63026
|
3 |
begin
|
|
4 |
|
|
5 |
ML_file "../antiquote_setup.ML"
|
|
6 |
ML_file "../more_antiquote.ML"
|
|
7 |
|
|
8 |
attribute_setup all =
|
|
9 |
\<open>Scan.succeed (Thm.rule_attribute [] (K Drule.forall_intr_vars))\<close>
|
|
10 |
"quantified schematic vars"
|
|
11 |
|
|
12 |
setup \<open>Config.put_global Printer.show_type_emphasis false\<close>
|
|
13 |
|
63555
|
14 |
setup \<open>
|
|
15 |
let
|
|
16 |
fun strip_all t =
|
|
17 |
if Logic.is_all t
|
|
18 |
then
|
|
19 |
case snd (dest_comb t) of Abs (w, T, t') =>
|
|
20 |
strip_all t' |>> cons (w, T)
|
|
21 |
else ([], t);
|
|
22 |
fun frugal (w, T as TFree (v, sort)) visited =
|
|
23 |
if member (op =) visited v
|
|
24 |
then ((w, dummyT), visited) else ((w, T), v :: visited)
|
|
25 |
| frugal (w, T) visited = ((w, dummyT), visited);
|
|
26 |
fun frugal_sorts t =
|
|
27 |
let
|
|
28 |
val (vTs, body) = strip_all t
|
|
29 |
val (vTs', _) = fold_map frugal vTs [];
|
|
30 |
in Logic.list_all (vTs', map_types (K dummyT) body) end;
|
|
31 |
in
|
|
32 |
Term_Style.setup @{binding frugal_sorts}
|
|
33 |
(Scan.succeed (K frugal_sorts))
|
|
34 |
end
|
|
35 |
\<close>
|
|
36 |
|
63026
|
37 |
declare [[show_sorts]]
|
|
38 |
|
|
39 |
end
|