Theory Setup

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

unbundle lattice_syntax

ML_file ‹../antiquote_setup.ML›
ML_file ‹../more_antiquote.ML›

attribute_setup all =
  ‹Scan.succeed (Thm.rule_attribute [] (K Thm.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