Theory Types_To_Sets

(*  Title:      HOL/Types_To_Sets/Types_To_Sets.thy
    Author:     Ondřej Kunčar, TU München
*)

section From Types to Sets

text This theory extends Isabelle/HOL's logic by two new inference rules
  to allow translation of types to sets as described in
  O. Kunčar, A. Popescu: From Types to Sets by Local Type Definitions in Higher-Order Logic
  available at https://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.

theory Types_To_Sets
  imports Main
  keywords "unoverload_definition" :: thy_decl
begin

subsection Rules

textThe following file implements the Local Typedef Rule (LT) and extends the logic by the rule.
ML_file local_typedef.ML

textThe following file implements the Unoverloading Rule (UO) and extends the logic by the rule.
ML_file unoverloading.ML

textThe following file implements a derived rule that internalizes type class annotations.
ML_file internalize_sort.ML

textThe following file provides some automation to unoverload and internalize the parameters of
  the sort constraints of a type variable.
ML_file unoverload_type.ML

text The following file provides automation to define unoverloaded constants from overloaded
  definitions.
named_theorems unoverload_def
ML_file unoverload_def.ML

end