# HG changeset patch # User wenzelm # Date 1246565882 -7200 # Node ID 342a0bad5adf30b07a6c508ab2891648cf4198a0 # Parent f3227bb306a45071675b55d8fb3b729439fc6839# Parent 4263be178c8f057ae1a5a1d33489e711966ff31a merged diff -r 4263be178c8f -r 342a0bad5adf doc-src/IsarRef/Thy/HOL_Specific.thy --- 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 \"} \\ + @{command_def (HOL) "quickcheck"}@{text "\<^sup>*"} & : & @{text "proof \"} \\ + @{command_def (HOL) "quickcheck_params"} & : & @{text "theory \ 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 \"} \\ @{command_def (HOL) "code_module"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "code_library"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "consts_code"} & : & @{text "theory \ 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}. diff -r 4263be178c8f -r 342a0bad5adf doc-src/IsarRef/Thy/Spec.thy --- 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 diff -r 4263be178c8f -r 342a0bad5adf doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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}. diff -r 4263be178c8f -r 342a0bad5adf doc-src/IsarRef/Thy/document/Spec.tex --- 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. diff -r 4263be178c8f -r 342a0bad5adf src/HOL/Finite_Set.thy --- 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 \ (0::'a::{field,division_by_zero}) ==> - setprod (inverse \ f) A = inverse (setprod f A)" +lemma setprod_inversef: + fixes f :: "'b \ 'a::{field,division_by_zero}" + shows "finite A ==> setprod (inverse \ f) A = inverse (setprod f A)" by (erule finite_induct) auto lemma setprod_dividef: - "[|finite A; - \x \ A. g x \ (0::'a::{field,division_by_zero})|] + fixes f :: "'b \ '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 \ g) x) A") diff -r 4263be178c8f -r 342a0bad5adf src/HOL/Tools/res_atp.ML --- 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 diff -r 4263be178c8f -r 342a0bad5adf src/HOL/Tools/res_clause.ML --- 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; diff -r 4263be178c8f -r 342a0bad5adf src/HOL/Tools/res_hol_clause.ML --- 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