src/HOL/Types_To_Sets/Types_To_Sets.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 64551 79e9587dbcca
child 68224 1f7308050349
permissions -rw-r--r--
executable domain membership checks
wenzelm@64551
     1
(*  Title:      HOL/Types_To_Sets/Types_To_Sets.thy
wenzelm@64551
     2
    Author:     Ondřej Kunčar, TU München
wenzelm@64551
     3
*)
wenzelm@64551
     4
wenzelm@64551
     5
section \<open>From Types to Sets\<close>
wenzelm@64551
     6
wenzelm@64551
     7
text \<open>This theory extends Isabelle/HOL's logic by two new inference rules
wenzelm@64551
     8
  to allow translation of types to sets as described in
wenzelm@64551
     9
  O. Kunčar, A. Popescu: From Types to Sets by Local Type Definitions in Higher-Order Logic
wenzelm@64551
    10
  available at http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\<close>
wenzelm@64551
    11
wenzelm@64551
    12
theory Types_To_Sets
wenzelm@64551
    13
  imports Main
wenzelm@64551
    14
begin
wenzelm@64551
    15
wenzelm@64551
    16
subsection \<open>Rules\<close>
wenzelm@64551
    17
wenzelm@64551
    18
text\<open>The following file implements the Local Typedef Rule (LT) and extends the logic by the rule.\<close>
wenzelm@64551
    19
ML_file "local_typedef.ML"
wenzelm@64551
    20
wenzelm@64551
    21
text\<open>The following file implements the Unoverloading Rule (UO) and extends the logic by the rule.\<close>
wenzelm@64551
    22
ML_file "unoverloading.ML"
wenzelm@64551
    23
wenzelm@64551
    24
text\<open>The following file implements a derived rule that internalizes type class annotations.\<close>
wenzelm@64551
    25
ML_file "internalize_sort.ML"
wenzelm@64551
    26
wenzelm@64551
    27
end