--- a/NEWS Wed Jan 21 21:01:15 2009 -0800
+++ b/NEWS Thu Jan 22 06:09:41 2009 -0800
@@ -66,13 +66,19 @@
*** Pure ***
-* Type Binding.T gradually replaces formerly used type bstring for names
+* Class declaration: sc. "base sort" must not be given in import list
+any longer but is inferred from the specification. Particularly in HOL,
+write
+
+ class foo = ... instead of class foo = type + ...
+
+* Type binding gradually replaces formerly used type bstring for names
to be bound. Name space interface for declarations has been simplified:
NameSpace.declare: NameSpace.naming
- -> Binding.T -> NameSpace.T -> string * NameSpace.T
+ -> binding -> NameSpace.T -> string * NameSpace.T
NameSpace.bind: NameSpace.naming
- -> Binding.T * 'a -> 'a NameSpace.table -> string * 'a NameSpace.table
+ -> binding * 'a -> 'a NameSpace.table -> string * 'a NameSpace.table
(*exception Symtab.DUP*)
See further modules src/Pure/General/binding.ML and
--- a/doc-src/IsarImplementation/Thy/ML.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/doc-src/IsarImplementation/Thy/ML.thy Thu Jan 22 06:09:41 2009 -0800
@@ -319,7 +319,7 @@
\smallskip\begin{mldecls}
@{ML "Sign.declare_const: Properties.T -> (binding * typ) * mixfix
-> theory -> term * theory"} \\
- @{ML "Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory"}
+ @{ML "Thm.add_def: bool -> bool -> binding * term -> theory -> thm * theory"}
\end{mldecls}
\noindent Written with naive application, an addition of constant
@@ -328,7 +328,7 @@
\smallskip\begin{mldecls}
@{ML "(fn (t, thy) => Thm.add_def false false
- (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
+ (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
(Sign.declare_const []
((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn) thy)"}
\end{mldecls}
@@ -347,7 +347,7 @@
|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
|> (fn (t, thy) => thy
|> Thm.add_def false false
- (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))"}
+ (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))"}
\end{mldecls}
*}
@@ -370,7 +370,7 @@
@{ML "thy
|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
|-> (fn t => Thm.add_def false false
- (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
+ (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
"}
\end{mldecls}
@@ -380,7 +380,7 @@
@{ML "thy
|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
|>> (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
-|-> (fn def => Thm.add_def false false (\"bar_def\", def))
+|-> (fn def => Thm.add_def false false (Binding.name \"bar_def\", def))
"}
\end{mldecls}
@@ -392,7 +392,7 @@
|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
||> Sign.add_path \"foobar\"
|-> (fn t => Thm.add_def false false
- (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
+ (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
||> Sign.restore_naming thy
"}
\end{mldecls}
@@ -404,7 +404,7 @@
|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
||>> Sign.declare_const [] ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn)
|-> (fn (t1, t2) => Thm.add_def false false
- (\"bar_def\", Logic.mk_equals (t1, t2)))
+ (Binding.name \"bar_def\", Logic.mk_equals (t1, t2)))
"}
\end{mldecls}
*}
@@ -451,7 +451,7 @@
((Binding.name const, @{typ \"foo => foo\"}), NoSyn)) consts
|>> map (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
|-> (fn defs => fold_map (fn def =>
- Thm.add_def false false (\"\", def)) defs)
+ Thm.add_def false false (Binding.empty, def)) defs)
end"}
\end{mldecls}
*}
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Wed Jan 21 21:01:15 2009 -0800
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Thu Jan 22 06:09:41 2009 -0800
@@ -368,7 +368,7 @@
\smallskip\begin{mldecls}
\verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix|\isasep\isanewline%
\verb| -> theory -> term * theory| \\
- \verb|Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory|
+ \verb|Thm.add_def: bool -> bool -> binding * term -> theory -> thm * theory|
\end{mldecls}
\noindent Written with naive application, an addition of constant
@@ -377,7 +377,7 @@
\smallskip\begin{mldecls}
\verb|(fn (t, thy) => Thm.add_def false false|\isasep\isanewline%
-\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline%
+\verb| (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline%
\verb| (Sign.declare_const []|\isasep\isanewline%
\verb| ((Binding.name "bar", @{typ "foo => foo"}), NoSyn) thy)|
\end{mldecls}
@@ -397,7 +397,7 @@
\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
\verb||\verb,|,\verb|> (fn (t, thy) => thy|\isasep\isanewline%
\verb||\verb,|,\verb|> Thm.add_def false false|\isasep\isanewline%
-\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|
+\verb| (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|
\end{mldecls}%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -435,7 +435,7 @@
\verb|thy|\isasep\isanewline%
\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
\verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline%
-\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
+\verb| (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
\end{mldecls}
@@ -445,7 +445,7 @@
\verb|thy|\isasep\isanewline%
\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
\verb||\verb,|,\verb|>> (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
-\verb||\verb,|,\verb|-> (fn def => Thm.add_def false false ("bar_def", def))|\isasep\isanewline%
+\verb||\verb,|,\verb|-> (fn def => Thm.add_def false false (Binding.name "bar_def", def))|\isasep\isanewline%
\end{mldecls}
@@ -457,7 +457,7 @@
\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
\verb||\verb,|,\verb||\verb,|,\verb|> Sign.add_path "foobar"|\isasep\isanewline%
\verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline%
-\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
+\verb| (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
\verb||\verb,|,\verb||\verb,|,\verb|> Sign.restore_naming thy|\isasep\isanewline%
\end{mldecls}
@@ -469,7 +469,7 @@
\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const [] ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
\verb||\verb,|,\verb|-> (fn (t1, t2) => Thm.add_def false false|\isasep\isanewline%
-\verb| ("bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline%
+\verb| (Binding.name "bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline%
\end{mldecls}%
\end{isamarkuptext}%
@@ -531,7 +531,7 @@
\verb| ((Binding.name const, @{typ "foo => foo"}), NoSyn)) consts|\isasep\isanewline%
\verb| |\verb,|,\verb|>> map (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
\verb| |\verb,|,\verb|-> (fn defs => fold_map (fn def =>|\isasep\isanewline%
-\verb| Thm.add_def false false ("", def)) defs)|\isasep\isanewline%
+\verb| Thm.add_def false false (Binding.empty, def)) defs)|\isasep\isanewline%
\verb|end|
\end{mldecls}%
\end{isamarkuptext}%
--- a/doc-src/IsarImplementation/Thy/document/logic.tex Wed Jan 21 21:01:15 2009 -0800
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex Thu Jan 22 06:09:41 2009 -0800
@@ -594,9 +594,9 @@
\verb| -> (string * ('a -> thm)) * theory| \\
\end{mldecls}
\begin{mldecls}
- \indexml{Theory.add\_axioms\_i}\verb|Theory.add_axioms_i: (string * term) list -> theory -> theory| \\
+ \indexml{Theory.add\_axioms\_i}\verb|Theory.add_axioms_i: (binding * term) list -> theory -> theory| \\
\indexml{Theory.add\_deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
- \indexml{Theory.add\_defs\_i}\verb|Theory.add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory| \\
+ \indexml{Theory.add\_defs\_i}\verb|Theory.add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory| \\
\end{mldecls}
\begin{description}
--- a/doc-src/IsarImplementation/Thy/logic.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/doc-src/IsarImplementation/Thy/logic.thy Thu Jan 22 06:09:41 2009 -0800
@@ -596,9 +596,9 @@
-> (string * ('a -> thm)) * theory"} \\
\end{mldecls}
\begin{mldecls}
- @{index_ML Theory.add_axioms_i: "(string * term) list -> theory -> theory"} \\
+ @{index_ML Theory.add_axioms_i: "(binding * term) list -> theory -> theory"} \\
@{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
- @{index_ML Theory.add_defs_i: "bool -> bool -> (bstring * term) list -> theory -> theory"} \\
+ @{index_ML Theory.add_defs_i: "bool -> bool -> (binding * term) list -> theory -> theory"} \\
\end{mldecls}
\begin{description}
--- a/doc-src/IsarRef/Thy/Spec.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/doc-src/IsarRef/Thy/Spec.thy Thu Jan 22 06:09:41 2009 -0800
@@ -436,7 +436,6 @@
\begin{matharray}{rcl}
@{command_def "interpretation"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
@{command_def "interpret"} & : & @{text "proof(state) | proof(chain \<rightarrow> proof(prove)"} \\
- @{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
\end{matharray}
\indexouternonterm{interp}
@@ -445,8 +444,6 @@
;
'interpret' interp
;
- 'print\_interps' '!'? name
- ;
instantiation: ('[' (inst+) ']')?
;
interp: (name ':')? \\ (contextexpr instantiation |
@@ -531,13 +528,6 @@
interprets @{text expr} in the proof context and is otherwise
similar to interpretation in theories.
- \item @{command "print_interps"}~@{text loc} prints the
- interpretations of a particular locale @{text loc} that are active
- in the current context, either theory or proof context. The
- exclamation point argument triggers printing of \emph{witness}
- theorems justifying interpretations. These are normally omitted
- from the output.
-
\end{description}
\begin{warn}
--- a/doc-src/IsarRef/Thy/document/Spec.tex Wed Jan 21 21:01:15 2009 -0800
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Thu Jan 22 06:09:41 2009 -0800
@@ -453,7 +453,6 @@
\begin{matharray}{rcl}
\indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
\indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ proof{\isacharparenleft}chain\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
- \indexdef{}{command}{print\_interps}\hypertarget{command.print-interps}{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
\end{matharray}
\indexouternonterm{interp}
@@ -462,8 +461,6 @@
;
'interpret' interp
;
- 'print\_interps' '!'? name
- ;
instantiation: ('[' (inst+) ']')?
;
interp: (name ':')? \\ (contextexpr instantiation |
@@ -543,13 +540,6 @@
interprets \isa{expr} in the proof context and is otherwise
similar to interpretation in theories.
- \item \hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{loc} prints the
- interpretations of a particular locale \isa{loc} that are active
- in the current context, either theory or proof context. The
- exclamation point argument triggers printing of \emph{witness}
- theorems justifying interpretations. These are normally omitted
- from the output.
-
\end{description}
\begin{warn}
--- a/src/HOL/ATP_Linkup.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOL/ATP_Linkup.thy Thu Jan 22 06:09:41 2009 -0800
@@ -7,7 +7,7 @@
header {* The Isabelle-ATP Linkup *}
theory ATP_Linkup
-imports Record Hilbert_Choice
+imports Divides Record Hilbert_Choice
uses
"Tools/polyhash.ML"
"Tools/res_clause.ML"
--- a/src/HOL/Datatype.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOL/Datatype.thy Thu Jan 22 06:09:41 2009 -0800
@@ -8,7 +8,7 @@
header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
theory Datatype
-imports Nat Relation
+imports Nat Product_Type
begin
typedef (Node)
@@ -509,15 +509,6 @@
lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma, standard]
-(*** Domain ***)
-
-lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
-by auto
-
-lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
-by auto
-
-
text {* hides popular names *}
hide (open) type node item
hide (open) const Push Node Atom Leaf Numb Lim Split Case
--- a/src/HOL/Finite_Set.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOL/Finite_Set.thy Thu Jan 22 06:09:41 2009 -0800
@@ -6,7 +6,7 @@
header {* Finite sets *}
theory Finite_Set
-imports Datatype Divides Transitive_Closure
+imports Nat Product_Type Power
begin
subsection {* Definition and basic properties *}
@@ -380,46 +380,6 @@
by(blast intro: finite_subset[OF subset_Pow_Union])
-lemma finite_converse [iff]: "finite (r^-1) = finite r"
- apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
- apply simp
- apply (rule iffI)
- apply (erule finite_imageD [unfolded inj_on_def])
- apply (simp split add: split_split)
- apply (erule finite_imageI)
- apply (simp add: converse_def image_def, auto)
- apply (rule bexI)
- prefer 2 apply assumption
- apply simp
- done
-
-
-text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
-Ehmety) *}
-
-lemma finite_Field: "finite r ==> finite (Field r)"
- -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
- apply (induct set: finite)
- apply (auto simp add: Field_def Domain_insert Range_insert)
- done
-
-lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
- apply clarify
- apply (erule trancl_induct)
- apply (auto simp add: Field_def)
- done
-
-lemma finite_trancl: "finite (r^+) = finite r"
- apply auto
- prefer 2
- apply (rule trancl_subset_Field2 [THEN finite_subset])
- apply (rule finite_SigmaI)
- prefer 3
- apply (blast intro: r_into_trancl' finite_subset)
- apply (auto simp add: finite_Field)
- done
-
-
subsection {* Class @{text finite} *}
setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
@@ -471,9 +431,6 @@
instance "+" :: (finite, finite) finite
by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
-instance option :: (finite) finite
- by default (simp add: insert_None_conv_UNIV [symmetric])
-
subsection {* A fold functional for finite sets *}
--- a/src/HOL/HOL.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOL/HOL.thy Thu Jan 22 06:09:41 2009 -0800
@@ -208,34 +208,34 @@
subsubsection {* Generic classes and algebraic operations *}
-class default = type +
+class default =
fixes default :: 'a
-class zero = type +
+class zero =
fixes zero :: 'a ("0")
-class one = type +
+class one =
fixes one :: 'a ("1")
hide (open) const zero one
-class plus = type +
+class plus =
fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65)
-class minus = type +
+class minus =
fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "-" 65)
-class uminus = type +
+class uminus =
fixes uminus :: "'a \<Rightarrow> 'a" ("- _" [81] 80)
-class times = type +
+class times =
fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
-class inverse = type +
+class inverse =
fixes inverse :: "'a \<Rightarrow> 'a"
and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70)
-class abs = type +
+class abs =
fixes abs :: "'a \<Rightarrow> 'a"
begin
@@ -247,10 +247,10 @@
end
-class sgn = type +
+class sgn =
fixes sgn :: "'a \<Rightarrow> 'a"
-class ord = type +
+class ord =
fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
begin
@@ -1675,7 +1675,7 @@
text {* Equality *}
-class eq = type +
+class eq =
fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
begin
--- a/src/HOL/Int.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOL/Int.thy Thu Jan 22 06:09:41 2009 -0800
@@ -599,7 +599,7 @@
Bit1 :: "int \<Rightarrow> int" where
[code del]: "Bit1 k = 1 + k + k"
-class number = type + -- {* for numeric types: nat, int, real, \dots *}
+class number = -- {* for numeric types: nat, int, real, \dots *}
fixes number_of :: "int \<Rightarrow> 'a"
use "Tools/numeral.ML"
--- a/src/HOL/Library/Eval_Witness.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOL/Library/Eval_Witness.thy Thu Jan 22 06:09:41 2009 -0800
@@ -32,7 +32,7 @@
with the oracle.
*}
-class ml_equiv = type
+class ml_equiv
text {*
Instances of @{text "ml_equiv"} should only be declared for those types,
--- a/src/HOL/Library/Quotient.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOL/Library/Quotient.thy Thu Jan 22 06:09:41 2009 -0800
@@ -21,7 +21,7 @@
"\<sim> :: 'a => 'a => bool"}.
*}
-class eqv = type +
+class eqv =
fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sim>" 50)
class equiv = eqv +
--- a/src/HOL/Nat.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOL/Nat.thy Thu Jan 22 06:09:41 2009 -0800
@@ -1515,7 +1515,7 @@
subsection {* size of a datatype value *}
-class size = type +
+class size =
fixes size :: "'a \<Rightarrow> nat" -- {* see further theory @{text Wellfounded} *}
end
--- a/src/HOL/Nominal/Examples/W.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOL/Nominal/Examples/W.thy Thu Jan 22 06:09:41 2009 -0800
@@ -49,7 +49,7 @@
text {* free type variables *}
-class ftv = type +
+class ftv =
fixes ftv :: "'a \<Rightarrow> tvar list"
instantiation * :: (ftv, ftv) ftv
--- a/src/HOL/Parity.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOL/Parity.thy Thu Jan 22 06:09:41 2009 -0800
@@ -8,7 +8,7 @@
imports Plain Presburger
begin
-class even_odd = type +
+class even_odd =
fixes even :: "'a \<Rightarrow> bool"
abbreviation
--- a/src/HOL/Plain.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOL/Plain.thy Thu Jan 22 06:09:41 2009 -0800
@@ -1,7 +1,7 @@
header {* Plain HOL *}
theory Plain
-imports Datatype FunDef Record SAT Extraction
+imports Datatype FunDef Record SAT Extraction Divides
begin
text {*
@@ -9,6 +9,9 @@
include @{text Hilbert_Choice}.
*}
+instance option :: (finite) finite
+ by default (simp add: insert_None_conv_UNIV [symmetric])
+
ML {* path_add "~~/src/HOL/Library" *}
end
--- a/src/HOL/Power.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOL/Power.thy Thu Jan 22 06:09:41 2009 -0800
@@ -11,7 +11,7 @@
imports Nat
begin
-class power = type +
+class power =
fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80)
subsection{*Powers for Arbitrary Monoids*}
--- a/src/HOL/RealVector.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOL/RealVector.thy Thu Jan 22 06:09:41 2009 -0800
@@ -124,7 +124,7 @@
subsection {* Real vector spaces *}
-class scaleR = type +
+class scaleR =
fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "*\<^sub>R" 75)
begin
@@ -418,7 +418,7 @@
subsection {* Real normed vector spaces *}
-class norm = type +
+class norm =
fixes norm :: "'a \<Rightarrow> real"
instantiation real :: norm
--- a/src/HOL/Relation.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOL/Relation.thy Thu Jan 22 06:09:41 2009 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/Relation.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
*)
@@ -7,7 +6,7 @@
header {* Relations *}
theory Relation
-imports Product_Type
+imports Datatype Finite_Set
begin
subsection {* Definitions *}
@@ -379,6 +378,12 @@
lemma fst_eq_Domain: "fst ` R = Domain R";
by (auto intro!:image_eqI)
+lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
+by auto
+
+lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
+by auto
+
subsection {* Range *}
@@ -566,6 +571,31 @@
done
+subsection {* Finiteness *}
+
+lemma finite_converse [iff]: "finite (r^-1) = finite r"
+ apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
+ apply simp
+ apply (rule iffI)
+ apply (erule finite_imageD [unfolded inj_on_def])
+ apply (simp split add: split_split)
+ apply (erule finite_imageI)
+ apply (simp add: converse_def image_def, auto)
+ apply (rule bexI)
+ prefer 2 apply assumption
+ apply simp
+ done
+
+text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
+Ehmety) *}
+
+lemma finite_Field: "finite r ==> finite (Field r)"
+ -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
+ apply (induct set: finite)
+ apply (auto simp add: Field_def Domain_insert Range_insert)
+ done
+
+
subsection {* Version of @{text lfp_induct} for binary relations *}
lemmas lfp_induct2 =
--- a/src/HOL/SizeChange/Kleene_Algebras.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOL/SizeChange/Kleene_Algebras.thy Thu Jan 22 06:09:41 2009 -0800
@@ -11,7 +11,7 @@
text {* A type class of kleene algebras *}
-class star = type +
+class star =
fixes star :: "'a \<Rightarrow> 'a"
class idem_add = ab_semigroup_add +
--- a/src/HOL/Transitive_Closure.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOL/Transitive_Closure.thy Thu Jan 22 06:09:41 2009 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/Transitive_Closure.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
*)
@@ -568,6 +567,22 @@
apply auto
done
+lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
+ apply clarify
+ apply (erule trancl_induct)
+ apply (auto simp add: Field_def)
+ done
+
+lemma finite_trancl: "finite (r^+) = finite r"
+ apply auto
+ prefer 2
+ apply (rule trancl_subset_Field2 [THEN finite_subset])
+ apply (rule finite_SigmaI)
+ prefer 3
+ apply (blast intro: r_into_trancl' finite_subset)
+ apply (auto simp add: finite_Field)
+ done
+
text {* More about converse @{text rtrancl} and @{text trancl}, should
be merged with main body. *}
--- a/src/HOL/Typedef.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOL/Typedef.thy Thu Jan 22 06:09:41 2009 -0800
@@ -123,7 +123,7 @@
text {* This class is just a workaround for classes without parameters;
it shall disappear as soon as possible. *}
-class itself = type +
+class itself =
fixes itself :: "'a itself"
setup {*
--- a/src/HOL/Wellfounded.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOL/Wellfounded.thy Thu Jan 22 06:09:41 2009 -0800
@@ -7,7 +7,7 @@
header {*Well-founded Recursion*}
theory Wellfounded
-imports Finite_Set Nat
+imports Finite_Set Transitive_Closure Nat
uses ("Tools/function_package/size.ML")
begin
--- a/src/HOL/Word/BitSyntax.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOL/Word/BitSyntax.thy Thu Jan 22 06:09:41 2009 -0800
@@ -12,7 +12,7 @@
imports BinGeneral
begin
-class bit = type +
+class bit =
fixes bitNOT :: "'a \<Rightarrow> 'a" ("NOT _" [70] 71)
and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64)
and bitOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR" 59)
--- a/src/HOL/Word/Size.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOL/Word/Size.thy Thu Jan 22 06:09:41 2009 -0800
@@ -18,7 +18,7 @@
some duplication with the definitions in @{text "Numeral_Type"}.
*}
-class len0 = type +
+class len0 =
fixes len_of :: "'a itself \<Rightarrow> nat"
text {*
--- a/src/HOLCF/Bifinite.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOLCF/Bifinite.thy Thu Jan 22 06:09:41 2009 -0800
@@ -10,7 +10,7 @@
subsection {* Omega-profinite and bifinite domains *}
-class profinite = cpo +
+class profinite =
fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a"
assumes chain_approx [simp]: "chain approx"
assumes lub_approx_app [simp]: "(\<Squnion>i. approx i\<cdot>x) = x"
--- a/src/HOLCF/Pcpo.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOLCF/Pcpo.thy Thu Jan 22 06:09:41 2009 -0800
@@ -12,9 +12,9 @@
text {* The class cpo of chain complete partial orders *}
-axclass cpo < po
+class cpo = po +
-- {* class axiom: *}
- cpo: "chain S \<Longrightarrow> \<exists>x. range S <<| x"
+ assumes cpo: "chain S \<Longrightarrow> \<exists>x. range S <<| x"
text {* in cpo's everthing equal to THE lub has lub properties for every chain *}
@@ -170,8 +170,8 @@
text {* The class pcpo of pointed cpos *}
-axclass pcpo < cpo
- least: "\<exists>x. \<forall>y. x \<sqsubseteq> y"
+class pcpo = cpo +
+ assumes least: "\<exists>x. \<forall>y. x \<sqsubseteq> y"
definition
UU :: "'a::pcpo" where
@@ -254,13 +254,13 @@
text {* further useful classes for HOLCF domains *}
-axclass finite_po < finite, po
+class finite_po = finite + po
-axclass chfin < po
- chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y"
+class chfin = po +
+ assumes chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y"
-axclass flat < pcpo
- ax_flat: "x \<sqsubseteq> y \<Longrightarrow> (x = \<bottom>) \<or> (x = y)"
+class flat = pcpo +
+ assumes ax_flat: "x \<sqsubseteq> y \<Longrightarrow> (x = \<bottom>) \<or> (x = y)"
text {* finite partial orders are chain-finite *}
@@ -310,11 +310,11 @@
text {* Discrete cpos *}
-axclass discrete_cpo < sq_ord
- discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y"
+class discrete_cpo = sq_ord +
+ assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y"
-instance discrete_cpo < po
-by (intro_classes, simp_all)
+subclass (in discrete_cpo) po
+proof qed simp_all
text {* In a discrete cpo, every chain is constant *}
--- a/src/HOLCF/Porder.thy Wed Jan 21 21:01:15 2009 -0800
+++ b/src/HOLCF/Porder.thy Thu Jan 22 06:09:41 2009 -0800
@@ -10,7 +10,7 @@
subsection {* Type class for partial orders *}
-class sq_ord = type +
+class sq_ord =
fixes sq_le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
notation
--- a/src/Pure/General/binding.ML Wed Jan 21 21:01:15 2009 -0800
+++ b/src/Pure/General/binding.ML Thu Jan 22 06:09:41 2009 -0800
@@ -15,22 +15,21 @@
signature BINDING =
sig
include BASIC_BINDING
- type T
- val name_pos: string * Position.T -> T
- val name: string -> T
- val empty: T
- val map_base: (string -> string) -> T -> T
- val qualify: string -> T -> T
- val add_prefix: bool -> string -> T -> T
- val map_prefix: ((string * bool) list -> T -> T) -> T -> T
- val is_empty: T -> bool
- val base_name: T -> string
- val pos_of: T -> Position.T
- val dest: T -> (string * bool) list * string
+ val name_pos: string * Position.T -> binding
+ val name: string -> binding
+ val empty: binding
+ val map_base: (string -> string) -> binding -> binding
+ val qualify: string -> binding -> binding
+ val add_prefix: bool -> string -> binding -> binding
+ val map_prefix: ((string * bool) list -> binding -> binding) -> binding -> binding
+ val is_empty: binding -> bool
+ val base_name: binding -> string
+ val pos_of: binding -> Position.T
+ val dest: binding -> (string * bool) list * string
val separator: string
val is_qualified: string -> bool
- val display: T -> string
-end
+ val display: binding -> string
+end;
structure Binding : BINDING =
struct
@@ -55,7 +54,7 @@
(** binding representation **)
-datatype T = Binding of ((string * bool) list * string) * Position.T;
+datatype binding = Binding of ((string * bool) list * string) * Position.T;
(* (prefix components (with mandatory flag), base name, position) *)
fun name_pos (name, pos) = Binding (([], name), pos);
@@ -93,8 +92,6 @@
else space_implode "." (map mk_prefix prefix) ^ ":" ^ name
end;
-type binding = T;
-
end;
structure Basic_Binding : BASIC_BINDING = Binding;
--- a/src/Pure/Isar/class.ML Wed Jan 21 21:01:15 2009 -0800
+++ b/src/Pure/Isar/class.ML Thu Jan 22 06:09:41 2009 -0800
@@ -92,8 +92,8 @@
fun add_typ_check level name f = Context.proof_map (Syntax.add_typ_check level name (fn xs => fn ctxt =>
let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
-fun singleton_infer_param change_sort = (map o map_atyps) (fn T as TVar (vi as (_, i), sort) =>
- if TypeInfer.is_param vi then TypeInfer.param i (Name.aT, change_sort sort)
+val singleton_infer_param = (map o map_atyps) (fn T as TVar (vi as (_, i), sort) =>
+ if TypeInfer.is_param vi then TypeInfer.param i (Name.aT, sort)
else error ("Illegal schematic type variable in class specification: " ^ Term.string_of_vname vi)
(*FIXME does not occur*)
| T as TFree (v, sort) =>
@@ -119,11 +119,12 @@
let
(* prepare import *)
val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy));
- val (sups, others_basesort) = map (prep_class thy) raw_supclasses
- |> Sign.minimize_sort thy
- |> List.partition (is_class thy);
-
- val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
+ val sups = map (prep_class thy) raw_supclasses
+ |> Sign.minimize_sort thy;
+ val _ = case filter_out (is_class thy) sups
+ of [] => ()
+ | no_classes => error ("These are not classes: " ^ commas (map quote no_classes));
+ val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
val supparam_names = map fst supparams;
val _ = if has_duplicates (op =) supparam_names
then error ("Duplicate parameter(s) in superclasses: "
@@ -131,7 +132,7 @@
else ();
val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional [])))
sups, []);
- val given_basesort = fold inter_sort (map (base_sort thy) sups) others_basesort;
+ val given_basesort = fold inter_sort (map (base_sort thy) sups) [];
(* infer types and base sort *)
val base_constraints = (map o apsnd)
@@ -139,10 +140,9 @@
(these_operations thy sups);
val ((_, _, inferred_elems), _) = ProofContext.init thy
|> fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
- |> add_typ_check ~1 "singleton_infer_param" (singleton_infer_param (inter_sort given_basesort))
+ |> add_typ_check ~1 "singleton_infer_param" singleton_infer_param
|> add_typ_check ~2 "singleton_fixate" singleton_fixate
|> prep_decl supexpr raw_elems;
- (*FIXME propagation of given base sort into class spec broken*)
(*FIXME check for *all* side conditions here, extra check function for elements,
less side-condition checks in check phase*)
val base_sort = if null inferred_elems then given_basesort else
@@ -170,45 +170,6 @@
val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration;
val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration;
-(*fun prep_class_spec prep_class process_decl thy raw_supclasses raw_elems =
- let
- (*FIXME 2009 simplify*)
- val supclasses = map (prep_class thy) raw_supclasses;
- val supsort = Sign.minimize_sort thy supclasses;
- val (sups, bases) = List.partition (is_class thy) supsort;
- val base_sort = if null sups then supsort else
- Library.foldr (Sorts.inter_sort (Sign.classes_of thy))
- (map (base_sort thy) sups, bases);
- val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
- val supparam_names = map fst supparams;
- val _ = if has_duplicates (op =) supparam_names
- then error ("Duplicate parameter(s) in superclasses: "
- ^ (commas o map quote o duplicates (op =)) supparam_names)
- else ();
-
- val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional [])))
- sups, []);
- val constrain = Element.Constrains ((map o apsnd o map_atyps)
- (K (TFree (Name.aT, base_sort))) supparams);
- (*FIXME 2009 perhaps better: control type variable by explicit
- parameter instantiation of import expression*)
- val begin_ctxt = begin sups base_sort
- #> fold (Variable.declare_constraints o Free) ((map o apsnd o map_atyps)
- (K (TFree (Name.aT, base_sort))) supparams) (*FIXME
- should constraints be issued in begin?*)
- val ((_, _, syntax_elems), _) = ProofContext.init thy
- |> begin_ctxt
- |> process_decl supexpr raw_elems;
- fun fork_syn (Element.Fixes xs) =
- fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs
- #>> Element.Fixes
- | fork_syn x = pair x;
- val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
- in (((sups, supparam_names), (supsort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end;
-
-val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration;
-val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration;*)
-
fun add_consts bname class base_sort sups supparams global_syntax thy =
let
(*FIXME 2009 simplify*)
--- a/src/Pure/Isar/class_target.ML Wed Jan 21 21:01:15 2009 -0800
+++ b/src/Pure/Isar/class_target.ML Thu Jan 22 06:09:41 2009 -0800
@@ -55,8 +55,6 @@
-> (Attrib.binding * string list) list
-> theory -> class * theory
val classrel_cmd: xstring * xstring -> theory -> Proof.state
-
- (*old instance layer*)
val instance_arity: (theory -> theory) -> arity -> theory -> Proof.state
val instance_arity_cmd: bstring * xstring list * xstring -> theory -> Proof.state
end;
@@ -275,7 +273,7 @@
val intros = (snd o rules thy) sup :: map_filter I
[Option.map (Drule.standard' o Element.conclude_witness) some_wit,
(fst o rules thy) sub];
- val tac = ALLGOALS (EVERY' (map Tactic.rtac intros));
+ val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
val classrel = Goal.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
(K tac);
val diff_sort = Sign.complete_sort thy [sup]
@@ -285,9 +283,9 @@
|> AxClass.add_classrel classrel
|> ClassData.map (Graph.add_edge (sub, sup))
|> activate_defs sub (these_defs thy diff_sort)
- |> fold2 (fn dep_morph => fn wit => Locale.add_dependency sub (sup,
- dep_morph $> Element.satisfy_morphism [wit] $> export))
- (the_list some_dep_morph) (the_list some_wit)
+ |> fold (fn dep_morph => Locale.add_dependency sub (sup,
+ dep_morph $> Element.satisfy_morphism (the_list some_wit) $> export))
+ (the_list some_dep_morph)
|> (fn thy => fold_rev Locale.activate_global_facts
(Locale.get_registrations thy) thy)
end;
--- a/src/Pure/Isar/isar_syn.ML Wed Jan 21 21:01:15 2009 -0800
+++ b/src/Pure/Isar/isar_syn.ML Thu Jan 22 06:09:41 2009 -0800
@@ -428,7 +428,7 @@
val _ =
OuterSyntax.command "class" "define type class" K.thy_decl
- (P.name -- (P.$$$ "=" |-- class_val) -- P.opt_begin
+ (P.name -- Scan.optional (P.$$$ "=" |-- class_val) ([], []) -- P.opt_begin
>> (fn ((name, (supclasses, elems)), begin) =>
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin
(Class.class_cmd name supclasses elems #> snd)));