1063 the subset. In general, the type @{text \<tau>} may involve type |
1063 the subset. In general, the type @{text \<tau>} may involve type |
1064 variables @{text "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} which means that the type definition |
1064 variables @{text "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} which means that the type definition |
1065 produces a type constructor @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} depending on |
1065 produces a type constructor @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} depending on |
1066 those type arguments. |
1066 those type arguments. |
1067 |
1067 |
1068 The axiomatization can be considered a ``definition'' in the sense |
1068 The axiomatization can be considered a ``definition'' in the sense of the |
1069 of the particular set-theoretic interpretation of HOL |
1069 particular set-theoretic interpretation of HOL \cite{pitts93}, where the |
1070 \cite{pitts93}, where the universe of types is required to be |
1070 universe of types is required to be downwards-closed wrt.\ arbitrary |
1071 downwards-closed wrt.\ arbitrary non-empty subsets. Thus genuinely |
1071 non-empty subsets. Thus genuinely new types introduced by @{command |
1072 new types introduced by @{command "typedef"} stay within the range |
1072 "typedef"} stay within the range of HOL models by construction. |
1073 of HOL models by construction. Note that @{command_ref |
1073 |
1074 type_synonym} from Isabelle/Pure merely introduces syntactic |
1074 In contrast, the command @{command_ref type_synonym} from Isabelle/Pure |
1075 abbreviations, without any logical significance. |
1075 merely introduces syntactic abbreviations, without any logical |
|
1076 significance. Thus it is more faithful to the idea of a genuine type |
|
1077 definition, but less powerful in practice. |
1076 |
1078 |
1077 @{rail \<open> |
1079 @{rail \<open> |
1078 @@{command (HOL) typedef} abs_type '=' rep_set |
1080 @@{command (HOL) typedef} abs_type '=' rep_set |
1079 ; |
1081 ; |
1080 abs_type: @{syntax typespec_sorts} @{syntax mixfix}? |
1082 abs_type: @{syntax typespec_sorts} @{syntax mixfix}? |
1082 rep_set: @{syntax term} (@'morphisms' @{syntax name} @{syntax name})? |
1084 rep_set: @{syntax term} (@'morphisms' @{syntax name} @{syntax name})? |
1083 \<close>} |
1085 \<close>} |
1084 |
1086 |
1085 \begin{description} |
1087 \begin{description} |
1086 |
1088 |
1087 \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"} |
1089 \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"} produces an |
1088 axiomatizes a type definition in the background theory of the |
1090 axiomatization (\secref{sec:basic-spec}) for a type definition in the |
1089 current context, depending on a non-emptiness result of the set |
1091 background theory of the current context, depending on a non-emptiness |
1090 @{text A} that needs to be proven here. The set @{text A} may |
1092 result of the set @{text A} that needs to be proven here. The set @{text |
1091 contain type variables @{text "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} as specified on the LHS, |
1093 A} may contain type variables @{text "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} as specified on the |
1092 but no term variables. |
1094 LHS, but no term variables. |
1093 |
1095 |
1094 Even though a local theory specification, the newly introduced type |
1096 Even though a local theory specification, the newly introduced type |
1095 constructor cannot depend on parameters or assumptions of the |
1097 constructor cannot depend on parameters or assumptions of the |
1096 context: this is structurally impossible in HOL. In contrast, the |
1098 context: this is structurally impossible in HOL. In contrast, the |
1097 non-emptiness proof may use local assumptions in unusual situations, |
1099 non-emptiness proof may use local assumptions in unusual situations, |