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