# HG changeset patch # User wenzelm # Date 1238579216 -7200 # Node ID 7c6e1843fda57975a4c57386b9dd4da030c65a18 # Parent 263064c4d0c39040d9591026d1babe1561ecaba6# Parent d64a293f23ba8a923ef4d47450ab7258d0960d9d merged diff -r 263064c4d0c3 -r 7c6e1843fda5 src/HOLCF/Tools/domain/domain_theorems.ML --- a/src/HOLCF/Tools/domain/domain_theorems.ML Tue Mar 31 22:23:40 2009 +0200 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML Wed Apr 01 11:46:56 2009 +0200 @@ -610,7 +610,7 @@ |> (snd o PureThy.add_thmss [ ((Binding.name "iso_rews" , iso_rews ), [Simplifier.simp_add]), ((Binding.name "exhaust" , [exhaust] ), []), - ((Binding.name "casedist" , [casedist]), [Induct.cases_type (Long_Name.base_name dname)]), + ((Binding.name "casedist" , [casedist]), [Induct.cases_type dname]), ((Binding.name "when_rews", when_rews ), [Simplifier.simp_add]), ((Binding.name "compacts", con_compacts), [Simplifier.simp_add]), ((Binding.name "con_rews", con_rews), [Simplifier.simp_add]), @@ -999,6 +999,9 @@ in pg [] goal (K tacs) end; end; (* local *) +val inducts = ProjectRule.projections (ProofContext.init thy) ind; +fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]); + in thy |> Sign.add_path comp_dnam |> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [ ("take_rews" , take_rews ), @@ -1007,6 +1010,7 @@ ("finite_ind", [finite_ind]), ("ind" , [ind ]), ("coind" , [coind ])]))) + |> (snd o (PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))) |> Sign.parent_path |> pair take_rews end; (* let *) end; (* local *) diff -r 263064c4d0c3 -r 7c6e1843fda5 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Tue Mar 31 22:23:40 2009 +0200 +++ b/src/Pure/Tools/find_theorems.ML Wed Apr 01 11:46:56 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 263064c4d0c3 -r 7c6e1843fda5 src/Pure/conjunction.ML --- a/src/Pure/conjunction.ML Tue Mar 31 22:23:40 2009 +0200 +++ b/src/Pure/conjunction.ML Wed Apr 01 11:46:56 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 263064c4d0c3 -r 7c6e1843fda5 src/Tools/auto_solve.ML --- a/src/Tools/auto_solve.ML Tue Mar 31 22:23:40 2009 +0200 +++ b/src/Tools/auto_solve.ML Wed Apr 01 11:46:56 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 263064c4d0c3 -r 7c6e1843fda5 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Tue Mar 31 22:23:40 2009 +0200 +++ b/src/Tools/quickcheck.ML Wed Apr 01 11:46:56 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.