| author | wenzelm |
| Tue, 14 Feb 2012 12:40:55 +0100 | |
| changeset 46457 | 915af80f74b3 |
| parent 46456 | a1c7b842ff8b (current diff) |
| parent 46455 | ec2e20b27638 (diff) |
| child 46458 | 19ef91d7fbd4 |
| child 46477 | db693eb03a3f |
| doc-src/IsarRef/Thy/HOL_Specific.thy | file | annotate | diff | comparison | revisions | |
| doc-src/IsarRef/Thy/document/HOL_Specific.tex | file | annotate | diff | comparison | revisions |
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Feb 14 11:16:07 2012 +0100 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Feb 14 12:40:55 2012 +0100 @@ -1261,6 +1261,19 @@ @{command_def (HOL) "print_quotmaps"} & : & @{text "context \<rightarrow>"}\\ @{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\ @{command_def (HOL) "print_quotconsts"} & : & @{text "context \<rightarrow>"}\\ + @{method_def (HOL) "lifting"} & : & @{text method} \\ + @{method_def (HOL) "lifting_setup"} & : & @{text method} \\ + @{method_def (HOL) "descending"} & : & @{text method} \\ + @{method_def (HOL) "descending_setup"} & : & @{text method} \\ + @{method_def (HOL) "partiality_descending"} & : & @{text method} \\ + @{method_def (HOL) "partiality_descending_setup"} & : & @{text method} \\ + @{method_def (HOL) "regularize"} & : & @{text method} \\ + @{method_def (HOL) "injection"} & : & @{text method} \\ + @{method_def (HOL) "cleaning"} & : & @{text method} \\ + @{attribute_def (HOL) "quot_thm"} & : & @{text attribute} \\ + @{attribute_def (HOL) "quot_lifted"} & : & @{text attribute} \\ + @{attribute_def (HOL) "quot_respect"} & : & @{text attribute} \\ + @{attribute_def (HOL) "quot_preserve"} & : & @{text attribute} \\ \end{matharray} The quotient package defines a new quotient type given a raw type @@ -1280,16 +1293,30 @@ @{rail " @@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? \\ @{syntax term} 'is' @{syntax term}; - + constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}? "} + @{rail " + @@{method (HOL) lifting} @{syntax thmrefs}? + ; + + @@{method (HOL) lifting_setup} @{syntax thmrefs}? + ; + "} + \begin{description} - - \item @{command (HOL) "quotient_type"} defines quotient types. The + + \item @{command (HOL) "quotient_type"} defines quotient types. The injection from a quotient type to a raw type is called @{text rep_t}, its inverse @{text abs_t} unless explicit @{keyword (HOL) - "morphisms"} specification provides alternative names. + "morphisms"} specification provides alternative names. @{command + (HOL) "quotient_type"} requires the user to prove that the relation + is an equivalence relation (predicate @{text equivp}), unless the + user specifies explicitely @{text partial} in which case the + obligation is @{text part_equivp}. A quotient defined with @{text + partial} is weaker in the sense that less things can be proved + automatically. \item @{command (HOL) "quotient_definition"} defines a constant on the quotient type. @@ -1301,6 +1328,65 @@ \item @{command (HOL) "print_quotconsts"} prints quotient constants. + \item @{method (HOL) "lifting"} and @{method (HOL) "lifting_setup"} + methods match the current goal with the given raw theorem to be + lifted producing three new subgoals: regularization, injection and + cleaning subgoals. @{method (HOL) "lifting"} tries to apply the + heuristics for automatically solving these three subgoals and + leaves only the subgoals unsolved by the heuristics to the user as + opposed to @{method (HOL) "lifting_setup"} which leaves the three + subgoals unsolved. + + \item @{method (HOL) "descending"} and @{method (HOL) + "descending_setup"} try to guess a raw statement that would lift + to the current subgoal. Such statement is assumed as a new subgoal + and @{method (HOL) "descending"} continues in the same way as + @{method (HOL) "lifting"} does. @{method (HOL) "descending"} tries + to solve the arising regularization, injection and cleaning + subgoals with the analoguous method @{method (HOL) + "descending_setup"} which leaves the four unsolved subgoals. + + \item @{method (HOL) "partiality_descending"} finds the regularized + theorem that would lift to the current subgoal, lifts it and + leaves as a subgoal. This method can be used with partial + equivalence quotients where the non regularized statements would + not be true. @{method (HOL) "partiality_descending_setup"} leaves + the injection and cleaning subgoals unchanged. + + \item @{method (HOL) "regularize"} applies the regularization + heuristics to the current subgoal. + + \item @{method (HOL) "injection"} applies the injection heuristics + to the current goal using the stored quotient respectfulness + theorems. + + \item @{method (HOL) "cleaning"} applies the injection cleaning + heuristics to the current subgoal using the stored quotient + preservation theorems. + + \item @{attribute (HOL) quot_lifted} attribute tries to + automatically transport the theorem to the quotient type. + The attribute uses all the defined quotients types and quotient + constants often producing undesired results or theorems that + cannot be lifted. + + \item @{attribute (HOL) quot_respect} and @{attribute (HOL) + quot_preserve} attributes declare a theorem as a respectfulness + and preservation theorem respectively. These are stored in the + local theory store and used by the @{method (HOL) "injection"} + and @{method (HOL) "cleaning"} methods respectively. + + \item @{attribute (HOL) quot_thm} declares that a certain theorem + is a quotient extension theorem. Quotient extension theorems + allow for quotienting inside container types. Given a polymorphic + type that serves as a container, a map function defined for this + container using @{command (HOL) "enriched_type"} and a relation + map defined for for the container type, the quotient extension + theorem should be @{term "Quotient R Abs Rep \<Longrightarrow> Quotient + (rel_map R) (map Abs) (map Rep)"}. Quotient extension theorems + are stored in a database and are used all the steps of lifting + theorems. + \end{description} *}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Feb 14 11:16:07 2012 +0100 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Feb 14 12:40:55 2012 +0100 @@ -1776,6 +1776,19 @@ \indexdef{HOL}{command}{print\_quotmaps}\hypertarget{command.HOL.print-quotmaps}{\hyperlink{command.HOL.print-quotmaps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotmaps}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\ \indexdef{HOL}{command}{print\_quotients}\hypertarget{command.HOL.print-quotients}{\hyperlink{command.HOL.print-quotients}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotients}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\ \indexdef{HOL}{command}{print\_quotconsts}\hypertarget{command.HOL.print-quotconsts}{\hyperlink{command.HOL.print-quotconsts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotconsts}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\ + \indexdef{HOL}{method}{lifting}\hypertarget{method.HOL.lifting}{\hyperlink{method.HOL.lifting}{\mbox{\isa{lifting}}}} & : & \isa{method} \\ + \indexdef{HOL}{method}{lifting\_setup}\hypertarget{method.HOL.lifting-setup}{\hyperlink{method.HOL.lifting-setup}{\mbox{\isa{lifting{\isaliteral{5F}{\isacharunderscore}}setup}}}} & : & \isa{method} \\ + \indexdef{HOL}{method}{descending}\hypertarget{method.HOL.descending}{\hyperlink{method.HOL.descending}{\mbox{\isa{descending}}}} & : & \isa{method} \\ + \indexdef{HOL}{method}{descending\_setup}\hypertarget{method.HOL.descending-setup}{\hyperlink{method.HOL.descending-setup}{\mbox{\isa{descending{\isaliteral{5F}{\isacharunderscore}}setup}}}} & : & \isa{method} \\ + \indexdef{HOL}{method}{partiality\_descending}\hypertarget{method.HOL.partiality-descending}{\hyperlink{method.HOL.partiality-descending}{\mbox{\isa{partiality{\isaliteral{5F}{\isacharunderscore}}descending}}}} & : & \isa{method} \\ + \indexdef{HOL}{method}{partiality\_descending\_setup}\hypertarget{method.HOL.partiality-descending-setup}{\hyperlink{method.HOL.partiality-descending-setup}{\mbox{\isa{partiality{\isaliteral{5F}{\isacharunderscore}}descending{\isaliteral{5F}{\isacharunderscore}}setup}}}} & : & \isa{method} \\ + \indexdef{HOL}{method}{regularize}\hypertarget{method.HOL.regularize}{\hyperlink{method.HOL.regularize}{\mbox{\isa{regularize}}}} & : & \isa{method} \\ + \indexdef{HOL}{method}{injection}\hypertarget{method.HOL.injection}{\hyperlink{method.HOL.injection}{\mbox{\isa{injection}}}} & : & \isa{method} \\ + \indexdef{HOL}{method}{cleaning}\hypertarget{method.HOL.cleaning}{\hyperlink{method.HOL.cleaning}{\mbox{\isa{cleaning}}}} & : & \isa{method} \\ + \indexdef{HOL}{attribute}{quot\_thm}\hypertarget{attribute.HOL.quot-thm}{\hyperlink{attribute.HOL.quot-thm}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}thm}}}} & : & \isa{attribute} \\ + \indexdef{HOL}{attribute}{quot\_lifted}\hypertarget{attribute.HOL.quot-lifted}{\hyperlink{attribute.HOL.quot-lifted}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}lifted}}}} & : & \isa{attribute} \\ + \indexdef{HOL}{attribute}{quot\_respect}\hypertarget{attribute.HOL.quot-respect}{\hyperlink{attribute.HOL.quot-respect}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}respect}}}} & : & \isa{attribute} \\ + \indexdef{HOL}{attribute}{quot\_preserve}\hypertarget{attribute.HOL.quot-preserve}{\hyperlink{attribute.HOL.quot-preserve}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}preserve}}}} & : & \isa{attribute} \\ \end{matharray} The quotient package defines a new quotient type given a raw type @@ -1851,10 +1864,32 @@ \end{railoutput} + \begin{railoutput} +\rail@begin{2}{} +\rail@term{\hyperlink{method.HOL.lifting}{\mbox{\isa{lifting}}}}[] +\rail@bar +\rail@nextbar{1} +\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] +\rail@endbar +\rail@end +\rail@begin{2}{} +\rail@term{\hyperlink{method.HOL.lifting-setup}{\mbox{\isa{lifting{\isaliteral{5F}{\isacharunderscore}}setup}}}}[] +\rail@bar +\rail@nextbar{1} +\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[] +\rail@endbar +\rail@end +\end{railoutput} + + \begin{description} - - \item \hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}} defines quotient types. The - injection from a quotient type to a raw type is called \isa{rep{\isaliteral{5F}{\isacharunderscore}}t}, its inverse \isa{abs{\isaliteral{5F}{\isacharunderscore}}t} unless explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} specification provides alternative names. + + \item \hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}} defines quotient types. The + injection from a quotient type to a raw type is called \isa{rep{\isaliteral{5F}{\isacharunderscore}}t}, its inverse \isa{abs{\isaliteral{5F}{\isacharunderscore}}t} unless explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} specification provides alternative names. \hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}} requires the user to prove that the relation + is an equivalence relation (predicate \isa{equivp}), unless the + user specifies explicitely \isa{partial} in which case the + obligation is \isa{part{\isaliteral{5F}{\isacharunderscore}}equivp}. A quotient defined with \isa{partial} is weaker in the sense that less things can be proved + automatically. \item \hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}} defines a constant on the quotient type. @@ -1866,6 +1901,61 @@ \item \hyperlink{command.HOL.print-quotconsts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotconsts}}}} prints quotient constants. + \item \hyperlink{method.HOL.lifting}{\mbox{\isa{lifting}}} and \hyperlink{method.HOL.lifting-setup}{\mbox{\isa{lifting{\isaliteral{5F}{\isacharunderscore}}setup}}} + methods match the current goal with the given raw theorem to be + lifted producing three new subgoals: regularization, injection and + cleaning subgoals. \hyperlink{method.HOL.lifting}{\mbox{\isa{lifting}}} tries to apply the + heuristics for automatically solving these three subgoals and + leaves only the subgoals unsolved by the heuristics to the user as + opposed to \hyperlink{method.HOL.lifting-setup}{\mbox{\isa{lifting{\isaliteral{5F}{\isacharunderscore}}setup}}} which leaves the three + subgoals unsolved. + + \item \hyperlink{method.HOL.descending}{\mbox{\isa{descending}}} and \hyperlink{method.HOL.descending-setup}{\mbox{\isa{descending{\isaliteral{5F}{\isacharunderscore}}setup}}} try to guess a raw statement that would lift + to the current subgoal. Such statement is assumed as a new subgoal + and \hyperlink{method.HOL.descending}{\mbox{\isa{descending}}} continues in the same way as + \hyperlink{method.HOL.lifting}{\mbox{\isa{lifting}}} does. \hyperlink{method.HOL.descending}{\mbox{\isa{descending}}} tries + to solve the arising regularization, injection and cleaning + subgoals with the analoguous method \hyperlink{method.HOL.descending-setup}{\mbox{\isa{descending{\isaliteral{5F}{\isacharunderscore}}setup}}} which leaves the four unsolved subgoals. + + \item \hyperlink{method.HOL.partiality-descending}{\mbox{\isa{partiality{\isaliteral{5F}{\isacharunderscore}}descending}}} finds the regularized + theorem that would lift to the current subgoal, lifts it and + leaves as a subgoal. This method can be used with partial + equivalence quotients where the non regularized statements would + not be true. \hyperlink{method.HOL.partiality-descending-setup}{\mbox{\isa{partiality{\isaliteral{5F}{\isacharunderscore}}descending{\isaliteral{5F}{\isacharunderscore}}setup}}} leaves + the injection and cleaning subgoals unchanged. + + \item \hyperlink{method.HOL.regularize}{\mbox{\isa{regularize}}} applies the regularization + heuristics to the current subgoal. + + \item \hyperlink{method.HOL.injection}{\mbox{\isa{injection}}} applies the injection heuristics + to the current goal using the stored quotient respectfulness + theorems. + + \item \hyperlink{method.HOL.cleaning}{\mbox{\isa{cleaning}}} applies the injection cleaning + heuristics to the current subgoal using the stored quotient + preservation theorems. + + \item \hyperlink{attribute.HOL.quot-lifted}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}lifted}}} attribute tries to + automatically transport the theorem to the quotient type. + The attribute uses all the defined quotients types and quotient + constants often producing undesired results or theorems that + cannot be lifted. + + \item \hyperlink{attribute.HOL.quot-respect}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}respect}}} and \hyperlink{attribute.HOL.quot-preserve}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}preserve}}} attributes declare a theorem as a respectfulness + and preservation theorem respectively. These are stored in the + local theory store and used by the \hyperlink{method.HOL.injection}{\mbox{\isa{injection}}} + and \hyperlink{method.HOL.cleaning}{\mbox{\isa{cleaning}}} methods respectively. + + \item \hyperlink{attribute.HOL.quot-thm}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}thm}}} declares that a certain theorem + is a quotient extension theorem. Quotient extension theorems + allow for quotienting inside container types. Given a polymorphic + type that serves as a container, a map function defined for this + container using \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}} and a relation + map defined for for the container type, the quotient extension + theorem should be \isa{{\isaliteral{22}{\isachardoublequote}}Quotient\ R\ Abs\ Rep\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Quotient\ {\isaliteral{28}{\isacharparenleft}}rel{\isaliteral{5F}{\isacharunderscore}}map\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ Abs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ Rep{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}. Quotient extension theorems + are stored in a database and are used all the steps of lifting + theorems. + \end{description}% \end{isamarkuptext}% \isamarkuptrue%
--- a/src/HOL/List.thy Tue Feb 14 11:16:07 2012 +0100 +++ b/src/HOL/List.thy Tue Feb 14 12:40:55 2012 +0100 @@ -3372,7 +3372,7 @@ lemma removeAll_id[simp]: "x \<notin> set xs \<Longrightarrow> removeAll x xs = xs" by (induct xs) auto -(* Needs count:: 'a \<Rightarrow> a' list \<Rightarrow> nat +(* Needs count:: 'a \<Rightarrow> 'a list \<Rightarrow> nat lemma length_removeAll: "length(removeAll x xs) = length xs - count x xs" *)
--- a/src/HOL/Mutabelle/MutabelleExtra.thy Tue Feb 14 11:16:07 2012 +0100 +++ b/src/HOL/Mutabelle/MutabelleExtra.thy Tue Feb 14 12:40:55 2012 +0100 @@ -42,7 +42,7 @@ MutabelleExtra.thms_of false thy |> MutabelleExtra.take_random 200 |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report - @{theory} mtds thms (log_directory ^ "/" ^ name))) + @{theory} (1, 50) mtds thms (log_directory ^ "/" ^ name))) *}
--- a/src/HOL/Mutabelle/etc/settings Tue Feb 14 11:16:07 2012 +0100 +++ b/src/HOL/Mutabelle/etc/settings Tue Feb 14 12:40:55 2012 +0100 @@ -4,5 +4,7 @@ MUTABELLE_LOGIC=HOL MUTABELLE_IMPORT_THEORY=Complex_Main +MUTABELLE_NUMBER_OF_MUTANTS=4 +MUTABELLE_NUMBER_OF_MUTATIONS=1 ISABELLE_TOOLS="$ISABELLE_TOOLS:$MUTABELLE_HOME/lib/Tools"
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle Tue Feb 14 11:16:07 2012 +0100 +++ b/src/HOL/Mutabelle/lib/Tools/mutabelle Tue Feb 14 12:40:55 2012 +0100 @@ -17,6 +17,8 @@ echo " -T THEORY parent theory to use (default $MUTABELLE_IMPORT_THEORY)" echo " -O DIR output directory for test data (default $MUTABELLE_OUTPUT_PATH)" echo " -N NUMBER number of lemmas to choose randomly, if not given all lemmas are chosen" + echo " -M NUMBER number of mutants for each lemma (default $MUTABELLE_NUMBER_OF_MUTANTS)" + echo " -X NUMBER number of mutations in a mutant (default $MUTABELLE_NUMBER_OF_MUTATIONS)" echo echo " THEORY is the name of the theory of which all theorems should be" echo " mutated and tested." @@ -31,7 +33,7 @@ MUTABELLE_IMPORTS="" -while getopts "L:T:O:N:" OPT +while getopts "L:T:O:N:M:X:" OPT do case "$OPT" in L) @@ -46,6 +48,12 @@ N) NUMBER_OF_LEMMAS="$OPTARG" ;; + M) + MUTABELLE_NUMBER_OF_MUTANTS="$OPTARG" + ;; + X) + MUTABELLE_NUMBER_OF_MUTATIONS="$OPTARG" + ;; \?) usage ;; @@ -95,16 +103,16 @@ ML {* val mtds = [ MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"])) \"random\", + MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"]) #> Config.put Quickcheck.finite_types false) \"random_int\", MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"])) \"exhaustive\", - MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_no_finite_types\", + MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_int\", MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types true) \"narrowing\", - MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing_no_finite_types\", + MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing_int\", MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ nat}])))) \"narrowing_nat\" -(* -, MutabelleExtra.refute_mtd, - MutabelleExtra.nitpick_mtd -*) +(*, MutabelleExtra.refute_mtd, *) + , MutabelleExtra.nitpick_mtd + ] *} @@ -113,7 +121,7 @@ (MutabelleExtra.random_seed := 1.0; MutabelleExtra.thms_of false thy $MUTABELLE_FILTER |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report - @{theory} mtds thms (\"$MUTABELLE_OUTPUT_PATH/log\"))) + @{theory} ($MUTABELLE_NUMBER_OF_MUTATIONS, $MUTABELLE_NUMBER_OF_MUTANTS) mtds thms (\"$MUTABELLE_OUTPUT_PATH/log\"))) *} ML {*
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Tue Feb 14 11:16:07 2012 +0100 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Tue Feb 14 12:40:55 2012 +0100 @@ -38,7 +38,7 @@ val string_for_report : report -> string val write_report : string -> report -> unit val mutate_theorems_and_write_report : - theory -> mtd list -> thm list -> string -> unit + theory -> int * int -> mtd list -> thm list -> string -> unit val random_seed : real Unsynchronized.ref end; @@ -49,17 +49,6 @@ (* Own seed; can't rely on the Isabelle one to stay the same *) val random_seed = Unsynchronized.ref 1.0; - -(* mutation options *) -val max_mutants = 4 -val num_mutations = 1 -(* soundness check: *) -(*val max_mutants = 10 -val num_mutations = 1*) - -(* quickcheck options *) -(*val quickcheck_generator = "SML"*) - (* Another Random engine *) exception RANDOM; @@ -117,7 +106,7 @@ (** quickcheck **) fun invoke_quickcheck change_options quickcheck_generator thy t = - TimeLimit.timeLimit (seconds (!Try.auto_time_limit)) + TimeLimit.timeLimit (seconds 30.0) (fn _ => let val ctxt' = change_options (Proof_Context.init_global thy) @@ -324,7 +313,7 @@ let val ctxt = Proof_Context.init_global thy in - can (TimeLimit.timeLimit (seconds 2.0) + can (TimeLimit.timeLimit (seconds 30.0) (Quickcheck.test_terms ((Context.proof_map (Quickcheck.set_active_testers ["exhaustive"]) #> Config.put Quickcheck.finite_types true #> @@ -396,7 +385,7 @@ end (* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *) -fun mutate_theorem create_entry thy mtds thm = +fun mutate_theorem create_entry thy (num_mutations, max_mutants) mtds thm = let val exec = is_executable_thm thy thm val _ = tracing (if exec then "EXEC" else "NOEXEC") @@ -434,7 +423,7 @@ end (* theory -> mtd list -> thm list -> report *) -val mutate_theorems = map ooo mutate_theorem +val mutate_theorems = map oooo mutate_theorem fun string_of_mutant_subentry thy thm_name (t, results) = "mutant: " ^ Syntax.string_of_term_global thy t ^ "\n" ^ @@ -499,7 +488,7 @@ File.write (Path.explode file_name) o string_for_report (* theory -> mtd list -> thm list -> string -> unit *) -fun mutate_theorems_and_write_report thy mtds thms file_name = +fun mutate_theorems_and_write_report thy (num_mutations, max_mutants) mtds thms file_name = let val _ = Output.urgent_message "Starting Mutabelle..." val ctxt = Proof_Context.init_global thy @@ -522,7 +511,7 @@ "size: " ^ string_of_int (Config.get ctxt Quickcheck.size) ^ "; iterations: " ^ string_of_int (Config.get ctxt Quickcheck.iterations) ^ "\n" ^ "Isabelle environment = ISABELLE_GHC: " ^ getenv "ISABELLE_GHC" ^ "\n"); - map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy mtds) thms; + map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy (num_mutations, max_mutants) mtds) thms; () end
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Feb 14 11:16:07 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Feb 14 12:40:55 2012 +0100 @@ -2711,6 +2711,8 @@ (s, args) | have_head_rolling _ = ("", []) +val max_kbo_weight = 2147483647 + fun atp_problem_kbo_weights problem = let fun add_term_deps head (ATerm (s, args)) = @@ -2735,7 +2737,7 @@ val graph = Graph.empty |> fold (fold (add_line_deps spec_eqN) o snd) problem |> fold (fold (add_line_deps simpN) o snd) problem - fun next_weight w = w + w + fun next_weight w = if w + w <= max_kbo_weight then w + w else w + 1 fun add_weights _ [] = I | add_weights weight syms = fold (AList.update (op =) o rpair weight) syms
--- a/src/HOL/Tools/ATP/atp_proof.ML Tue Feb 14 11:16:07 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Feb 14 12:40:55 2012 +0100 @@ -451,7 +451,7 @@ -- Symbol.scan_id -- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "." -- Scan.option (Scan.this_string "derived from formulae " - |-- Scan.repeat scan_general_id) + |-- Scan.repeat (scan_general_id --| Scan.option ($$ " "))) >> (fn ((((num, rule), deps), u), names) => Inference ((num, resolve_spass_num names spass_names num), u, rule, map (swap o `(resolve_spass_num NONE spass_names)) deps))
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Feb 14 11:16:07 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Feb 14 12:40:55 2012 +0100 @@ -246,12 +246,9 @@ let val method = effective_e_weight_method ctxt in (* FUDGE *) if method = e_smartN then - [(0.333, (true, ((500, FOF, "mono_tags??", combsN, false), - e_fun_weightN))), - (0.334, (true, ((50, FOF, "mono_guards??", combsN, false), - e_fun_weightN))), - (0.333, (true, ((1000, FOF, "mono_tags??", combsN, false), - e_sym_offset_weightN)))] + [(0.333, (true, ((500, FOF, "mono_tags??", combsN, false), e_fun_weightN))), + (0.334, (true, ((50, FOF, "mono_guards??", combsN, false), e_fun_weightN))), + (0.333, (true, ((1000, FOF, "mono_tags??", combsN, false), e_sym_offset_weightN)))] else [(1.0, (true, ((500, FOF, "mono_tags??", combsN, false), method)))] end} @@ -278,10 +275,8 @@ prem_kind = Hypothesis, best_slices = fn ctxt => (* FUDGE *) - [(0.667, (false, ((150, leo2_thf0, "mono_native_higher", liftingN, false), - sosN))), - (0.333, (true, ((50, leo2_thf0, "mono_native_higher", liftingN, false), - no_sosN)))] + [(0.667, (false, ((150, leo2_thf0, "mono_native_higher", liftingN, false), sosN))), + (0.333, (true, ((50, leo2_thf0, "mono_native_higher", liftingN, false), no_sosN)))] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -305,8 +300,7 @@ prem_kind = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, (true, ((100, satallax_thf0, "mono_native_higher", keep_lamsN, - false), "")))]} + K [(1.0, (true, ((100, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))]} val satallax = (satallaxN, satallax_config) @@ -336,23 +330,26 @@ prem_kind = Conjecture, best_slices = fn ctxt => (* FUDGE *) - [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN, false), - sosN))), - (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN, false), - sosN))), - (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false), - no_sosN)))] - |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single - else I)} + [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN, false), sosN))), + (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN, false), sosN))), + (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false), no_sosN)))] + |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} val spass = (spassN, spass_config) +val spass_new_H2 = "-Heuristic=2" +val spass_new_H2SOS = "-Heuristic=2 -SOS" +val spass_new_Red2 = "-RFRew=2 -RBRew=2 -RTaut=2" +val spass_new_Sorts0 = "-Sorts=0" +val spass_new_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0" +val spass_new_H2NuVS0Red2 = + "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2" + (* Experimental *) val spass_new_config : atp_config = {exec = ("SPASS_NEW_HOME", "SPASS"), required_execs = [], arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ => - (* TODO: add: -FPDFGProof -FPFCR *) ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout)) |> extra_options <> "" ? prefix (extra_options ^ " "), proof_delims = #proof_delims spass_config, @@ -361,16 +358,14 @@ prem_kind = #prem_kind spass_config, best_slices = fn _ => (* FUDGE *) - [(0.25, (true, ((150, DFG DFG_Sorted, "mono_native", combsN, true), - "-Heuristic=1"))), - (0.20, (true, ((500, DFG DFG_Sorted, "mono_native", liftingN, true), - "-Heuristic=2 -SOS"))), - (0.20, (true, ((50, DFG DFG_Sorted, "mono_native", liftingN, true), - "-Heuristic=2"))), - (0.20, (true, ((250, DFG DFG_Sorted, "mono_native", combs_and_liftingN, - true), "-Heuristic=2"))), - (0.15, (true, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, - true), "-Heuristic=2")))]} + [(0.1667, (false, ((150, DFG DFG_Sorted, "mono_native", combsN, true), ""))), + (0.1667, (false, ((500, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2SOS))), + (0.1666, (false, ((50, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2))), + (0.1000, (false, ((250, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2NuVS0))), + (0.1000, (false, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2NuVS0))), + (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2SOS))), + (0.1000, (false, ((150, DFG DFG_Sorted, "poly_guards??", liftingN, false), spass_new_H2NuVS0Red2))), + (0.1000, (false, ((400, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2)))]} val spass_new = (spass_newN, spass_new_config) @@ -410,19 +405,13 @@ best_slices = fn ctxt => (* FUDGE *) (if is_old_vampire_version () then - [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN, false), - sosN))), - (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN, false), - sosN))), - (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false), - no_sosN)))] + [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN, false), sosN))), + (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN, false), sosN))), + (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false), no_sosN)))] else - [(0.333, (false, ((150, vampire_tff0, "poly_guards??", - combs_or_liftingN, false), sosN))), - (0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN, - false), sosN))), - (0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN, - false), no_sosN)))]) + [(0.333, (false, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN))), + (0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN))), + (0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN)))]) |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)}