author | wenzelm |
Tue, 05 Nov 2019 14:28:00 +0100 | |
changeset 71047 | 87c132cf5860 |
parent 69689 | ab5a8a2519b0 |
permissions | -rw-r--r-- |
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 |
|
68224 | 10 |
available at https://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\<close> |
64551 | 11 |
|
12 |
theory Types_To_Sets |
|
13 |
imports Main |
|
69689 | 14 |
keywords "unoverload_definition" :: thy_decl |
64551 | 15 |
begin |
16 |
||
17 |
subsection \<open>Rules\<close> |
|
18 |
||
19 |
text\<open>The following file implements the Local Typedef Rule (LT) and extends the logic by the rule.\<close> |
|
69605 | 20 |
ML_file \<open>local_typedef.ML\<close> |
64551 | 21 |
|
22 |
text\<open>The following file implements the Unoverloading Rule (UO) and extends the logic by the rule.\<close> |
|
69605 | 23 |
ML_file \<open>unoverloading.ML\<close> |
64551 | 24 |
|
25 |
text\<open>The following file implements a derived rule that internalizes type class annotations.\<close> |
|
69605 | 26 |
ML_file \<open>internalize_sort.ML\<close> |
64551 | 27 |
|
69689 | 28 |
text\<open>The following file provides some automation to unoverload and internalize the parameters of |
68428
46beee72fb66
a derived rule combining unoverload and internalize_sort
immler
parents:
68224
diff
changeset
|
29 |
the sort constraints of a type variable.\<close> |
46beee72fb66
a derived rule combining unoverload and internalize_sort
immler
parents:
68224
diff
changeset
|
30 |
ML_file \<open>unoverload_type.ML\<close> |
46beee72fb66
a derived rule combining unoverload and internalize_sort
immler
parents:
68224
diff
changeset
|
31 |
|
69689 | 32 |
text \<open>The following file provides automation to define unoverloaded constants from overloaded |
33 |
definitions.\<close> |
|
34 |
named_theorems unoverload_def |
|
35 |
ML_file \<open>unoverload_def.ML\<close> |
|
36 |
||
64551 | 37 |
end |