--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Jul 02 22:17:08 2009 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Jul 02 22:18:02 2009 +0200
@@ -81,7 +81,7 @@
\end{matharray}
\begin{rail}
- 'split\_format' (((name *) + 'and') | ('(' 'complete' ')'))
+ 'split\_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
;
\end{rail}
@@ -369,7 +369,7 @@
dtspec: parname? typespec infix? '=' (cons + '|')
;
- cons: name (type *) mixfix?
+ cons: name ( type * ) mixfix?
\end{rail}
\begin{description}
@@ -515,7 +515,7 @@
\begin{rail}
'relation' term
;
- 'lexicographic\_order' (clasimpmod *)
+ 'lexicographic\_order' ( clasimpmod * )
;
\end{rail}
@@ -565,7 +565,7 @@
;
recdeftc thmdecl? tc
;
- hints: '(' 'hints' (recdefmod *) ')'
+ hints: '(' 'hints' ( recdefmod * ) ')'
;
recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
;
@@ -783,7 +783,7 @@
\end{matharray}
\begin{rail}
- 'iprover' ('!' ?) (rulemod *)
+ 'iprover' ('!' ?) ( rulemod * )
;
\end{rail}
@@ -824,6 +824,74 @@
*}
+section {* Checking and refuting propositions *}
+
+text {*
+ Identifying incorrect propositions usually involves evaluation of
+ particular assignments and systematic counter example search. This
+ is supported by the following commands.
+
+ \begin{matharray}{rcl}
+ @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def (HOL) "quickcheck"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
+ @{command_def (HOL) "quickcheck_params"} & : & @{text "theory \<rightarrow> theory"}
+ \end{matharray}
+
+ \begin{rail}
+ 'value' ( ( '[' name ']' ) ? ) modes? term
+ ;
+
+ 'quickcheck' ( ( '[' args ']' ) ? ) nat?
+ ;
+
+ 'quickcheck_params' ( ( '[' args ']' ) ? )
+ ;
+
+ modes: '(' (name + ) ')'
+ ;
+
+ args: ( name '=' value + ',' )
+ ;
+ \end{rail}
+
+ \begin{description}
+
+ \item @{command (HOL) "value"}~@{text t} evaluates and prints a
+ term; optionally @{text modes} can be specified, which are
+ appended to the current print mode (see also \cite{isabelle-ref}).
+ Internally, the evaluation is performed by registered evaluators,
+ which are invoked sequentially until a result is returned.
+ Alternatively a specific evaluator can be selected using square
+ brackets; available evaluators include @{text nbe} for
+ \emph{normalization by evaluation} and \emph{code} for code
+ generation in SML.
+
+ \item @{command (HOL) "quickcheck"} tests the current goal for
+ counter examples using a series of arbitrary assignments for its
+ free variables; by default the first subgoal is tested, an other
+ can be selected explicitly using an optional goal index.
+ A number of configuration options are supported for
+ @{command (HOL) "quickcheck"}, notably:
+
+ \begin{description}
+
+ \item[size] specifies the maximum size of the search space for
+ assignment values.
+
+ \item[iterations] sets how many sets of assignments are
+ generated for each particular size.
+
+ \end{description}
+
+ These option can be given within square brackets.
+
+ \item @{command (HOL) "quickcheck_params"} changes quickcheck
+ configuration options persitently.
+
+ \end{description}
+*}
+
+
section {* Invoking automated reasoning tools -- The Sledgehammer *}
text {*
@@ -860,7 +928,7 @@
\end{matharray}
\begin{rail}
- 'sledgehammer' (nameref *)
+ 'sledgehammer' ( nameref * )
;
'atp\_messages' ('(' nat ')')?
;
@@ -989,7 +1057,6 @@
(this actually covers the new-style theory format as well).
\begin{matharray}{rcl}
- @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def (HOL) "code_module"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_library"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\
@@ -998,9 +1065,6 @@
\end{matharray}
\begin{rail}
- 'value' term
- ;
-
( 'code\_module' | 'code\_library' ) modespec ? name ? \\
( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
'contains' ( ( name '=' term ) + | term + )
@@ -1034,13 +1098,6 @@
;
\end{rail}
- \begin{description}
-
- \item @{command (HOL) "value"}~@{text t} evaluates and prints a term
- using the code generator.
-
- \end{description}
-
\medskip The other framework generates code from functional programs
(including overloading using type classes) to SML \cite{SML}, OCaml
\cite{OCaml} and Haskell \cite{haskell-revised-report}.
--- a/doc-src/IsarRef/Thy/Spec.thy Thu Jul 02 22:17:08 2009 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Thu Jul 02 22:18:02 2009 +0200
@@ -600,7 +600,7 @@
;
'instance'
;
- 'instance' nameref '::' arity
+ 'instance' (nameref + 'and') '::' arity
;
'subclass' target? nameref
;
@@ -644,7 +644,7 @@
concluded by an @{command_ref (local) "end"} command.
Note that a list of simultaneous type constructors may be given;
- this corresponds nicely to mutual recursive type definitions, e.g.\
+ this corresponds nicely to mutually recursive type definitions, e.g.\
in Isabelle/HOL.
\item @{command "instance"} in an instantiation target body sets
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Jul 02 22:17:08 2009 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Jul 02 22:18:02 2009 +0200
@@ -98,7 +98,7 @@
\end{matharray}
\begin{rail}
- 'split\_format' (((name *) + 'and') | ('(' 'complete' ')'))
+ 'split\_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
;
\end{rail}
@@ -374,7 +374,7 @@
dtspec: parname? typespec infix? '=' (cons + '|')
;
- cons: name (type *) mixfix?
+ cons: name ( type * ) mixfix?
\end{rail}
\begin{description}
@@ -520,7 +520,7 @@
\begin{rail}
'relation' term
;
- 'lexicographic\_order' (clasimpmod *)
+ 'lexicographic\_order' ( clasimpmod * )
;
\end{rail}
@@ -570,7 +570,7 @@
;
recdeftc thmdecl? tc
;
- hints: '(' 'hints' (recdefmod *) ')'
+ hints: '(' 'hints' ( recdefmod * ) ')'
;
recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
;
@@ -793,7 +793,7 @@
\end{matharray}
\begin{rail}
- 'iprover' ('!' ?) (rulemod *)
+ 'iprover' ('!' ?) ( rulemod * )
;
\end{rail}
@@ -835,6 +835,76 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsection{Checking and refuting propositions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Identifying incorrect propositions usually involves evaluation of
+ particular assignments and systematic counter example search. This
+ is supported by the following commands.
+
+ \begin{matharray}{rcl}
+ \indexdef{HOL}{command}{value}\hypertarget{command.HOL.value}{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
+ \indexdef{HOL}{command}{quickcheck}\hypertarget{command.HOL.quickcheck}{\hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}{\isachardoublequote}} \\
+ \indexdef{HOL}{command}{quickcheck\_params}\hypertarget{command.HOL.quickcheck-params}{\hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isacharunderscore}params}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}}
+ \end{matharray}
+
+ \begin{rail}
+ 'value' ( ( '[' name ']' ) ? ) modes? term
+ ;
+
+ 'quickcheck' ( ( '[' args ']' ) ? ) nat?
+ ;
+
+ 'quickcheck_params' ( ( '[' args ']' ) ? )
+ ;
+
+ modes: '(' (name + ) ')'
+ ;
+
+ args: ( name '=' value + ',' )
+ ;
+ \end{rail}
+
+ \begin{description}
+
+ \item \hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}~\isa{t} evaluates and prints a
+ term; optionally \isa{modes} can be specified, which are
+ appended to the current print mode (see also \cite{isabelle-ref}).
+ Internally, the evaluation is performed by registered evaluators,
+ which are invoked sequentially until a result is returned.
+ Alternatively a specific evaluator can be selected using square
+ brackets; available evaluators include \isa{nbe} for
+ \emph{normalization by evaluation} and \emph{code} for code
+ generation in SML.
+
+ \item \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} tests the current goal for
+ counter examples using a series of arbitrary assignments for its
+ free variables; by default the first subgoal is tested, an other
+ can be selected explicitly using an optional goal index.
+ A number of configuration options are supported for
+ \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, notably:
+
+ \begin{description}
+
+ \item[size] specifies the maximum size of the search space for
+ assignment values.
+
+ \item[iterations] sets how many sets of assignments are
+ generated for each particular size.
+
+ \end{description}
+
+ These option can be given within square brackets.
+
+ \item \hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isacharunderscore}params}}}} changes quickcheck
+ configuration options persitently.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Invoking automated reasoning tools -- The Sledgehammer%
}
\isamarkuptrue%
@@ -873,7 +943,7 @@
\end{matharray}
\begin{rail}
- 'sledgehammer' (nameref *)
+ 'sledgehammer' ( nameref * )
;
'atp\_messages' ('(' nat ')')?
;
@@ -998,7 +1068,6 @@
(this actually covers the new-style theory format as well).
\begin{matharray}{rcl}
- \indexdef{HOL}{command}{value}\hypertarget{command.HOL.value}{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
\indexdef{HOL}{command}{code\_module}\hypertarget{command.HOL.code-module}{\hyperlink{command.HOL.code-module}{\mbox{\isa{\isacommand{code{\isacharunderscore}module}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
\indexdef{HOL}{command}{code\_library}\hypertarget{command.HOL.code-library}{\hyperlink{command.HOL.code-library}{\mbox{\isa{\isacommand{code{\isacharunderscore}library}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
\indexdef{HOL}{command}{consts\_code}\hypertarget{command.HOL.consts-code}{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
@@ -1007,9 +1076,6 @@
\end{matharray}
\begin{rail}
- 'value' term
- ;
-
( 'code\_module' | 'code\_library' ) modespec ? name ? \\
( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
'contains' ( ( name '=' term ) + | term + )
@@ -1043,13 +1109,6 @@
;
\end{rail}
- \begin{description}
-
- \item \hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}~\isa{t} evaluates and prints a term
- using the code generator.
-
- \end{description}
-
\medskip The other framework generates code from functional programs
(including overloading using type classes) to SML \cite{SML}, OCaml
\cite{OCaml} and Haskell \cite{haskell-revised-report}.
--- a/doc-src/IsarRef/Thy/document/Spec.tex Thu Jul 02 22:17:08 2009 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Thu Jul 02 22:18:02 2009 +0200
@@ -614,7 +614,7 @@
;
'instance'
;
- 'instance' nameref '::' arity
+ 'instance' (nameref + 'and') '::' arity
;
'subclass' target? nameref
;
@@ -653,7 +653,7 @@
concluded by an \indexref{local}{command}{end}\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} command.
Note that a list of simultaneous type constructors may be given;
- this corresponds nicely to mutual recursive type definitions, e.g.\
+ this corresponds nicely to mutually recursive type definitions, e.g.\
in Isabelle/HOL.
\item \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} in an instantiation target body sets
@@ -733,7 +733,7 @@
\end{matharray}
Axiomatic type classes are Isabelle/Pure's primitive
- \emph{definitional} interface to type classes. For practical
+ interface to type classes. For practical
applications, you should consider using classes
(cf.~\secref{sec:classes}) which provide high level interface.
--- a/src/HOL/Finite_Set.thy Thu Jul 02 22:17:08 2009 +0200
+++ b/src/HOL/Finite_Set.thy Thu Jul 02 22:18:02 2009 +0200
@@ -1883,14 +1883,14 @@
(if a:A then setprod f A / f a else setprod f A)"
by (erule finite_induct) (auto simp add: insert_Diff_if)
-lemma setprod_inversef: "finite A ==>
- ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
- setprod (inverse \<circ> f) A = inverse (setprod f A)"
+lemma setprod_inversef:
+ fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
+ shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
by (erule finite_induct) auto
lemma setprod_dividef:
- "[|finite A;
- \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
+ fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
+ shows "finite A
==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
apply (subgoal_tac
"setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
--- a/src/HOL/Tools/res_atp.ML Thu Jul 02 22:17:08 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML Thu Jul 02 22:18:02 2009 +0200
@@ -219,8 +219,7 @@
handle ConstFree => false
in
case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) =>
- defs lhs rhs andalso
- (Output.debug (fn () => "Definition found: " ^ name ^ "_" ^ Int.toString n); true)
+ defs lhs rhs
| _ => false
end;
@@ -276,8 +275,7 @@
fun relevance_filter max_new theory_const thy axioms goals =
if run_relevance_filter andalso pass_mark >= 0.1
then
- let val _ = Output.debug (fn () => "Start of relevance filtering");
- val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
+ let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
val goal_const_tab = get_goal_consts_typs thy goals
val _ = Output.debug (fn () => ("Initial constants: " ^
space_implode ", " (Symtab.keys goal_const_tab)));
@@ -406,8 +404,6 @@
fun check_named ("",th) = (warning ("No name for theorem " ^ Display.string_of_thm th); false)
| check_named (_,th) = true;
-fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ Display.string_of_thm th);
-
(* get lemmas from claset, simpset, atpset and extra supplied rules *)
fun get_clasimp_atp_lemmas ctxt =
let val included_thms =
@@ -419,7 +415,6 @@
let val atpset_thms =
if include_atpset then ResAxioms.atpset_rules_of ctxt
else []
- val _ = (Output.debug (fn () => "ATP theorems: "); app display_thm atpset_thms)
in atpset_thms end
in
filter check_named included_thms
--- a/src/HOL/Tools/res_clause.ML Thu Jul 02 22:17:08 2009 +0200
+++ b/src/HOL/Tools/res_clause.ML Thu Jul 02 22:18:02 2009 +0200
@@ -381,8 +381,6 @@
| iter_type_class_pairs thy tycons classes =
let val cpairs = type_class_pairs thy tycons classes
val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) \\ classes \\ HOLogic.typeS
- val _ = if null newclasses then ()
- else Output.debug (fn _ => "New classes: " ^ space_implode ", " newclasses)
val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
in (classes' union classes, cpairs' union cpairs) end;
--- a/src/HOL/Tools/res_hol_clause.ML Thu Jul 02 22:17:08 2009 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML Thu Jul 02 22:18:02 2009 +0200
@@ -419,13 +419,13 @@
val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
fun needed c = valOf (Symtab.lookup ct c) > 0
val IK = if needed "c_COMBI" orelse needed "c_COMBK"
- then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms thy [comb_I,comb_K])
+ then cnf_helper_thms thy [comb_I,comb_K]
else []
val BC = if needed "c_COMBB" orelse needed "c_COMBC"
- then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms thy [comb_B,comb_C])
+ then cnf_helper_thms thy [comb_B,comb_C]
else []
val S = if needed "c_COMBS"
- then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms thy [comb_S])
+ then cnf_helper_thms thy [comb_S]
else []
val other = cnf_helper_thms thy [fequal_imp_equal,equal_imp_fequal]
in