# HG changeset patch # User wenzelm # Date 1238531146 -7200 # Node ID 50c8f55cde7ff9f2a3df6ec65ef02665e2c7ee3c # Parent fe4331fb3806a8d7f79d139c0e61773d5480235a# Parent 14d24e1fe594b061b05ed1160882a3ffd2e1558f merged diff -r fe4331fb3806 -r 50c8f55cde7f src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Tue Mar 31 21:39:56 2009 +0200 +++ b/src/Pure/Tools/find_theorems.ML Tue Mar 31 22:25:46 2009 +0200 @@ -271,15 +271,17 @@ prod_ord int_ord int_ord ((p1, s1), (p0, s0)); in map_filter eval_filters thms |> sort thm_ord |> map #2 end; -fun lazy_filter filters = let +fun lazy_filter filters = + let fun lazy_match thms = Seq.make (fn () => first_match thms) and first_match [] = NONE - | first_match (thm::thms) = - case app_filters thm (SOME (0, 0), NONE, filters) of + | first_match (thm :: thms) = + (case app_filters thm (SOME (0, 0), NONE, filters) of NONE => first_match thms - | SOME (_, t) => SOME (t, lazy_match thms); + | SOME (_, t) => SOME (t, lazy_match thms)); in lazy_match end; + end; @@ -304,9 +306,9 @@ fun rem_c rev_seen [] = rev rev_seen | rem_c rev_seen [x] = rem_c (x :: rev_seen) [] | rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) = - if Thm.eq_thm_prop (t, t') - then rem_c rev_seen ((if nicer n n' then x else y) :: xs) - else rem_c (x :: rev_seen) (y :: xs) + if Thm.eq_thm_prop (t, t') + then rem_c rev_seen ((if nicer n n' then x else y) :: xs) + else rem_c (x :: rev_seen) (y :: xs) in rem_c [] xs end; in @@ -346,9 +348,10 @@ fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = let - val assms = ProofContext.get_fact ctxt (Facts.named "local.assms") - handle ERROR _ => []; - val add_prems = Seq.hd o (TRY (Method.insert_tac assms 1)); + val assms = + ProofContext.get_fact ctxt (Facts.named "local.assms") + handle ERROR _ => []; + val add_prems = Seq.hd o TRY (Method.insert_tac assms 1); val opt_goal' = Option.map add_prems opt_goal; val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; @@ -370,7 +373,7 @@ val find = if rem_dups orelse is_none opt_limit then find_all - else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters + else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters; in find (all_facts_of ctxt) end; @@ -388,12 +391,13 @@ val returned = length thms; val tally_msg = - case foundo of + (case foundo of NONE => "displaying " ^ string_of_int returned ^ " theorems" - | SOME found => "found " ^ string_of_int found ^ " theorems" ^ - (if returned < found - then " (" ^ string_of_int returned ^ " displayed)" - else ""); + | SOME found => + "found " ^ string_of_int found ^ " theorems" ^ + (if returned < found + then " (" ^ string_of_int returned ^ " displayed)" + else "")); val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs"; in @@ -411,11 +415,11 @@ fun find_theorems_cmd ((opt_lim, rem_dups), spec) = Toplevel.unknown_theory o Toplevel.keep (fn state => - let - val proof_state = Toplevel.enter_proof_body state; - val ctxt = Proof.context_of proof_state; - val opt_goal = try Proof.get_goal proof_state |> Option.map (#2 o #2); - in print_theorems ctxt opt_goal opt_lim rem_dups spec end); + let + val proof_state = Toplevel.enter_proof_body state; + val ctxt = Proof.context_of proof_state; + val opt_goal = try Proof.get_goal proof_state |> Option.map (#2 o #2); + in print_theorems ctxt opt_goal opt_lim rem_dups spec end); local diff -r fe4331fb3806 -r 50c8f55cde7f src/Pure/conjunction.ML --- a/src/Pure/conjunction.ML Tue Mar 31 21:39:56 2009 +0200 +++ b/src/Pure/conjunction.ML Tue Mar 31 22:25:46 2009 +0200 @@ -10,6 +10,7 @@ val mk_conjunction: cterm * cterm -> cterm val mk_conjunction_balanced: cterm list -> cterm val dest_conjunction: cterm -> cterm * cterm + val dest_conjunctions: cterm -> cterm list val cong: thm -> thm -> thm val convs: (cterm -> thm) -> cterm -> thm val conjunctionD1: thm @@ -44,6 +45,11 @@ (Const ("Pure.conjunction", _) $ _ $ _) => Thm.dest_binop ct | _ => raise TERM ("dest_conjunction", [Thm.term_of ct])); +fun dest_conjunctions ct = + (case try dest_conjunction ct of + NONE => [ct] + | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B); + (** derived rules **) diff -r fe4331fb3806 -r 50c8f55cde7f src/Tools/auto_solve.ML --- a/src/Tools/auto_solve.ML Tue Mar 31 21:39:56 2009 +0200 +++ b/src/Tools/auto_solve.ML Tue Mar 31 22:25:46 2009 +0200 @@ -1,11 +1,11 @@ -(* Title: Pure/Tools/auto_solve.ML +(* Title: Tools/auto_solve.ML Author: Timothy Bourke and Gerwin Klein, NICTA Check whether a newly stated theorem can be solved directly by an -existing theorem. Duplicate lemmas can be detected in this way. +existing theorem. Duplicate lemmas can be detected in this way. -The implemenation is based in part on Berghofer and Haftmann's -Pure/codegen.ML. It relies critically on the FindTheorems solves +The implementation is based in part on Berghofer and Haftmann's +quickcheck.ML. It relies critically on the FindTheorems solves feature. *) @@ -29,58 +29,48 @@ let val ctxt = Proof.context_of state; - fun conj_to_list [] = [] - | conj_to_list (t::ts) = - (Conjunction.dest_conjunction t - |> (fn (t1, t2) => conj_to_list (t1::t2::ts))) - handle TERM _ => t::conj_to_list ts; - val crits = [(true, FindTheorems.Solves)]; - fun find g = (NONE, snd (FindTheorems.find_theorems ctxt g (SOME (!limit)) false crits)); - fun find_cterm g = (SOME g, snd (FindTheorems.find_theorems ctxt - (SOME (Goal.init g)) (SOME (!limit)) false crits)); + fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits); fun prt_result (goal, results) = let - val msg = case goal of - NONE => "The current goal" - | SOME g => Syntax.string_of_term ctxt (term_of g); + val msg = + (case goal of + NONE => "The current goal" + | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg)); in - Pretty.big_list (msg ^ " could be solved directly with:") - (map (FindTheorems.pretty_thm ctxt) results) + Pretty.big_list + (msg ^ " could be solved directly with:") + (map (FindTheorems.pretty_thm ctxt) results) end; fun seek_against_goal () = - let - val goal = try Proof.get_goal state - |> Option.map (#2 o #2); - - val goals = goal - |> Option.map (fn g => cprem_of g 1) - |> the_list - |> conj_to_list; - - val rs = if length goals = 1 - then [find goal] - else map find_cterm goals; - val frs = filter_out (null o snd) rs; - - in if null frs then NONE else SOME frs end; + (case try Proof.get_goal state of + NONE => NONE + | SOME (_, (_, goal)) => + let + val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1); + val rs = + if length subgoals = 1 + then [(NONE, find goal)] + else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals; + val results = filter_out (null o snd) rs; + in if null results then NONE else SOME results end); fun go () = let - val res = TimeLimit.timeLimit - (Time.fromMilliseconds (! auto_time_limit)) - (try seek_against_goal) (); + val res = + TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit)) + (try seek_against_goal) (); in - case Option.join res of - NONE => state - | SOME results => (Proof.goal_message - (fn () => Pretty.chunks [Pretty.str "", - Pretty.markup Markup.hilite - (Library.separate (Pretty.brk 0) - (map prt_result results))]) - state) + (case res of + SOME (SOME results) => + state |> Proof.goal_message + (fn () => Pretty.chunks + [Pretty.str "", + Pretty.markup Markup.hilite + (separate (Pretty.brk 0) (map prt_result results))]) + | _ => state) end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state); in if int andalso ! auto andalso not (! Toplevel.quiet) diff -r fe4331fb3806 -r 50c8f55cde7f src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Tue Mar 31 21:39:56 2009 +0200 +++ b/src/Tools/quickcheck.ML Tue Mar 31 22:25:46 2009 +0200 @@ -1,4 +1,4 @@ -(* Title: Pure/Tools/quickcheck.ML +(* Title: Tools/quickcheck.ML Author: Stefan Berghofer, Florian Haftmann, TU Muenchen Generic counterexample search engine.