Theory Setup

theory Setup
imports Complex_Main "HOL-Library.Multiset" "HOL-Library.Lattice_Syntax"
begin

ML_file "../antiquote_setup.ML"
ML_file "../more_antiquote.ML"

attribute_setup all =
  ‹Scan.succeed (Thm.rule_attribute [] (K Drule.forall_intr_vars))›
  "quantified schematic vars"

setup ‹Config.put_global Printer.show_type_emphasis false›

setup ‹
let
  fun strip_all t =
    if Logic.is_all t
    then
      case snd (dest_comb t) of Abs (w, T, t') =>
        strip_all t' |>> cons (w, T)
    else ([], t);
  fun frugal (w, T as TFree (v, sort)) visited =
        if member (op =) visited v
        then ((w, dummyT), visited) else ((w, T), v :: visited)
    | frugal (w, T) visited = ((w, dummyT), visited);
  fun frugal_sorts t =
    let
      val (vTs, body) = strip_all t
      val (vTs', _) = fold_map frugal vTs [];
    in Logic.list_all (vTs', map_types (K dummyT) body) end;
in
  Term_Style.setup @{binding frugal_sorts}
    (Scan.succeed (K frugal_sorts))
end
›

declare [[show_sorts]]

end