# HG changeset patch # User huffman # Date 1232633381 28800 # Node ID 8096dc59d7794c128d2782a2caf5cf9d94d0f258 # Parent d59918e668b7a3f632a4d73de61c7242391d0991# Parent b36bcbc1be3a93b6b0c10ab2be5c68e4d0504ed7 merged diff -r d59918e668b7 -r 8096dc59d779 NEWS --- 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 diff -r d59918e668b7 -r 8096dc59d779 doc-src/IsarImplementation/Thy/ML.thy --- 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} *} diff -r d59918e668b7 -r 8096dc59d779 doc-src/IsarImplementation/Thy/document/ML.tex --- 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}% diff -r d59918e668b7 -r 8096dc59d779 doc-src/IsarImplementation/Thy/document/logic.tex --- 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} diff -r d59918e668b7 -r 8096dc59d779 doc-src/IsarImplementation/Thy/logic.thy --- 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} diff -r d59918e668b7 -r 8096dc59d779 doc-src/IsarRef/Thy/Spec.thy --- 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 \ proof(prove)"} \\ @{command_def "interpret"} & : & @{text "proof(state) | proof(chain \ proof(prove)"} \\ - @{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ \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} diff -r d59918e668b7 -r 8096dc59d779 doc-src/IsarRef/Thy/document/Spec.tex --- 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} diff -r d59918e668b7 -r 8096dc59d779 src/HOL/ATP_Linkup.thy --- 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" diff -r d59918e668b7 -r 8096dc59d779 src/HOL/Datatype.thy --- 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 diff -r d59918e668b7 -r 8096dc59d779 src/HOL/Finite_Set.thy --- 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 \ range"}. *} - apply (induct set: finite) - apply (auto simp add: Field_def Domain_insert Range_insert) - done - -lemma trancl_subset_Field2: "r^+ <= Field r \ 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 *} diff -r d59918e668b7 -r 8096dc59d779 src/HOL/HOL.thy --- 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 \ 'a \ 'a" (infixl "+" 65) -class minus = type + +class minus = fixes minus :: "'a \ 'a \ 'a" (infixl "-" 65) -class uminus = type + +class uminus = fixes uminus :: "'a \ 'a" ("- _" [81] 80) -class times = type + +class times = fixes times :: "'a \ 'a \ 'a" (infixl "*" 70) -class inverse = type + +class inverse = fixes inverse :: "'a \ 'a" and divide :: "'a \ 'a \ 'a" (infixl "'/" 70) -class abs = type + +class abs = fixes abs :: "'a \ 'a" begin @@ -247,10 +247,10 @@ end -class sgn = type + +class sgn = fixes sgn :: "'a \ 'a" -class ord = type + +class ord = fixes less_eq :: "'a \ 'a \ bool" and less :: "'a \ 'a \ bool" begin @@ -1675,7 +1675,7 @@ text {* Equality *} -class eq = type + +class eq = fixes eq :: "'a \ 'a \ bool" assumes eq_equals: "eq x y \ x = y" begin diff -r d59918e668b7 -r 8096dc59d779 src/HOL/Int.thy --- 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 \ 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 \ 'a" use "Tools/numeral.ML" diff -r d59918e668b7 -r 8096dc59d779 src/HOL/Library/Eval_Witness.thy --- 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, diff -r d59918e668b7 -r 8096dc59d779 src/HOL/Library/Quotient.thy --- 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 @@ "\ :: 'a => 'a => bool"}. *} -class eqv = type + +class eqv = fixes eqv :: "'a \ 'a \ bool" (infixl "\" 50) class equiv = eqv + diff -r d59918e668b7 -r 8096dc59d779 src/HOL/Nat.thy --- 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 \ nat" -- {* see further theory @{text Wellfounded} *} end diff -r d59918e668b7 -r 8096dc59d779 src/HOL/Nominal/Examples/W.thy --- 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 \ tvar list" instantiation * :: (ftv, ftv) ftv diff -r d59918e668b7 -r 8096dc59d779 src/HOL/Parity.thy --- 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 \ bool" abbreviation diff -r d59918e668b7 -r 8096dc59d779 src/HOL/Plain.thy --- 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 diff -r d59918e668b7 -r 8096dc59d779 src/HOL/Power.thy --- 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 \ nat \ 'a" (infixr "^" 80) subsection{*Powers for Arbitrary Monoids*} diff -r d59918e668b7 -r 8096dc59d779 src/HOL/RealVector.thy --- 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 \ 'a \ 'a" (infixr "*\<^sub>R" 75) begin @@ -418,7 +418,7 @@ subsection {* Real normed vector spaces *} -class norm = type + +class norm = fixes norm :: "'a \ real" instantiation real :: norm diff -r d59918e668b7 -r 8096dc59d779 src/HOL/Relation.thy --- 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 \ 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 = diff -r d59918e668b7 -r 8096dc59d779 src/HOL/SizeChange/Kleene_Algebras.thy --- 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 \ 'a" class idem_add = ab_semigroup_add + diff -r d59918e668b7 -r 8096dc59d779 src/HOL/Transitive_Closure.thy --- 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 \ 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. *} diff -r d59918e668b7 -r 8096dc59d779 src/HOL/Typedef.thy --- 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 {* diff -r d59918e668b7 -r 8096dc59d779 src/HOL/Wellfounded.thy --- 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 diff -r d59918e668b7 -r 8096dc59d779 src/HOL/Word/BitSyntax.thy --- 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 \ 'a" ("NOT _" [70] 71) and bitAND :: "'a \ 'a \ 'a" (infixr "AND" 64) and bitOR :: "'a \ 'a \ 'a" (infixr "OR" 59) diff -r d59918e668b7 -r 8096dc59d779 src/HOL/Word/Size.thy --- 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 \ nat" text {* diff -r d59918e668b7 -r 8096dc59d779 src/HOLCF/Bifinite.thy --- 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 \ 'a \ 'a" assumes chain_approx [simp]: "chain approx" assumes lub_approx_app [simp]: "(\i. approx i\x) = x" diff -r d59918e668b7 -r 8096dc59d779 src/HOLCF/Pcpo.thy --- 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 \ \x. range S <<| x" + assumes cpo: "chain S \ \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: "\x. \y. x \ y" +class pcpo = cpo + + assumes least: "\x. \y. x \ 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 \ \n. max_in_chain n Y" +class chfin = po + + assumes chfin: "chain Y \ \n. max_in_chain n Y" -axclass flat < pcpo - ax_flat: "x \ y \ (x = \) \ (x = y)" +class flat = pcpo + + assumes ax_flat: "x \ y \ (x = \) \ (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 \ y \ x = y" +class discrete_cpo = sq_ord + + assumes discrete_cpo [simp]: "x \ y \ 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 *} diff -r d59918e668b7 -r 8096dc59d779 src/HOLCF/Porder.thy --- 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 \ 'a \ bool" notation diff -r d59918e668b7 -r 8096dc59d779 src/Pure/General/binding.ML --- 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; diff -r d59918e668b7 -r 8096dc59d779 src/Pure/Isar/class.ML --- 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*) diff -r d59918e668b7 -r 8096dc59d779 src/Pure/Isar/class_target.ML --- 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; diff -r d59918e668b7 -r 8096dc59d779 src/Pure/Isar/isar_syn.ML --- 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)));