author | paulson |
Thu, 14 Jun 2018 14:23:48 +0100 | |
changeset 68446 | 92ddca1edc43 |
parent 66453 | cc19f7ca2ed6 |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
63026 | 1 |
theory Setup |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
63555
diff
changeset
|
2 |
imports Complex_Main "HOL-Library.Multiset" "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 |