1.1 --- a/src/Pure/Tools/find_theorems.ML Tue Mar 31 21:39:56 2009 +0200
1.2 +++ b/src/Pure/Tools/find_theorems.ML Tue Mar 31 22:25:46 2009 +0200
1.3 @@ -271,15 +271,17 @@
1.4 prod_ord int_ord int_ord ((p1, s1), (p0, s0));
1.5 in map_filter eval_filters thms |> sort thm_ord |> map #2 end;
1.6
1.7 -fun lazy_filter filters = let
1.8 +fun lazy_filter filters =
1.9 + let
1.10 fun lazy_match thms = Seq.make (fn () => first_match thms)
1.11
1.12 and first_match [] = NONE
1.13 - | first_match (thm::thms) =
1.14 - case app_filters thm (SOME (0, 0), NONE, filters) of
1.15 + | first_match (thm :: thms) =
1.16 + (case app_filters thm (SOME (0, 0), NONE, filters) of
1.17 NONE => first_match thms
1.18 - | SOME (_, t) => SOME (t, lazy_match thms);
1.19 + | SOME (_, t) => SOME (t, lazy_match thms));
1.20 in lazy_match end;
1.21 +
1.22 end;
1.23
1.24
1.25 @@ -304,9 +306,9 @@
1.26 fun rem_c rev_seen [] = rev rev_seen
1.27 | rem_c rev_seen [x] = rem_c (x :: rev_seen) []
1.28 | rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) =
1.29 - if Thm.eq_thm_prop (t, t')
1.30 - then rem_c rev_seen ((if nicer n n' then x else y) :: xs)
1.31 - else rem_c (x :: rev_seen) (y :: xs)
1.32 + if Thm.eq_thm_prop (t, t')
1.33 + then rem_c rev_seen ((if nicer n n' then x else y) :: xs)
1.34 + else rem_c (x :: rev_seen) (y :: xs)
1.35 in rem_c [] xs end;
1.36
1.37 in
1.38 @@ -346,9 +348,10 @@
1.39
1.40 fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
1.41 let
1.42 - val assms = ProofContext.get_fact ctxt (Facts.named "local.assms")
1.43 - handle ERROR _ => [];
1.44 - val add_prems = Seq.hd o (TRY (Method.insert_tac assms 1));
1.45 + val assms =
1.46 + ProofContext.get_fact ctxt (Facts.named "local.assms")
1.47 + handle ERROR _ => [];
1.48 + val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
1.49 val opt_goal' = Option.map add_prems opt_goal;
1.50
1.51 val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
1.52 @@ -370,7 +373,7 @@
1.53 val find =
1.54 if rem_dups orelse is_none opt_limit
1.55 then find_all
1.56 - else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters
1.57 + else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters;
1.58
1.59 in find (all_facts_of ctxt) end;
1.60
1.61 @@ -388,12 +391,13 @@
1.62 val returned = length thms;
1.63
1.64 val tally_msg =
1.65 - case foundo of
1.66 + (case foundo of
1.67 NONE => "displaying " ^ string_of_int returned ^ " theorems"
1.68 - | SOME found => "found " ^ string_of_int found ^ " theorems" ^
1.69 - (if returned < found
1.70 - then " (" ^ string_of_int returned ^ " displayed)"
1.71 - else "");
1.72 + | SOME found =>
1.73 + "found " ^ string_of_int found ^ " theorems" ^
1.74 + (if returned < found
1.75 + then " (" ^ string_of_int returned ^ " displayed)"
1.76 + else ""));
1.77
1.78 val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
1.79 in
1.80 @@ -411,11 +415,11 @@
1.81
1.82 fun find_theorems_cmd ((opt_lim, rem_dups), spec) =
1.83 Toplevel.unknown_theory o Toplevel.keep (fn state =>
1.84 - let
1.85 - val proof_state = Toplevel.enter_proof_body state;
1.86 - val ctxt = Proof.context_of proof_state;
1.87 - val opt_goal = try Proof.get_goal proof_state |> Option.map (#2 o #2);
1.88 - in print_theorems ctxt opt_goal opt_lim rem_dups spec end);
1.89 + let
1.90 + val proof_state = Toplevel.enter_proof_body state;
1.91 + val ctxt = Proof.context_of proof_state;
1.92 + val opt_goal = try Proof.get_goal proof_state |> Option.map (#2 o #2);
1.93 + in print_theorems ctxt opt_goal opt_lim rem_dups spec end);
1.94
1.95 local
1.96
2.1 --- a/src/Pure/conjunction.ML Tue Mar 31 21:39:56 2009 +0200
2.2 +++ b/src/Pure/conjunction.ML Tue Mar 31 22:25:46 2009 +0200
2.3 @@ -10,6 +10,7 @@
2.4 val mk_conjunction: cterm * cterm -> cterm
2.5 val mk_conjunction_balanced: cterm list -> cterm
2.6 val dest_conjunction: cterm -> cterm * cterm
2.7 + val dest_conjunctions: cterm -> cterm list
2.8 val cong: thm -> thm -> thm
2.9 val convs: (cterm -> thm) -> cterm -> thm
2.10 val conjunctionD1: thm
2.11 @@ -44,6 +45,11 @@
2.12 (Const ("Pure.conjunction", _) $ _ $ _) => Thm.dest_binop ct
2.13 | _ => raise TERM ("dest_conjunction", [Thm.term_of ct]));
2.14
2.15 +fun dest_conjunctions ct =
2.16 + (case try dest_conjunction ct of
2.17 + NONE => [ct]
2.18 + | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B);
2.19 +
2.20
2.21
2.22 (** derived rules **)
3.1 --- a/src/Tools/auto_solve.ML Tue Mar 31 21:39:56 2009 +0200
3.2 +++ b/src/Tools/auto_solve.ML Tue Mar 31 22:25:46 2009 +0200
3.3 @@ -1,11 +1,11 @@
3.4 -(* Title: Pure/Tools/auto_solve.ML
3.5 +(* Title: Tools/auto_solve.ML
3.6 Author: Timothy Bourke and Gerwin Klein, NICTA
3.7
3.8 Check whether a newly stated theorem can be solved directly by an
3.9 -existing theorem. Duplicate lemmas can be detected in this way.
3.10 +existing theorem. Duplicate lemmas can be detected in this way.
3.11
3.12 -The implemenation is based in part on Berghofer and Haftmann's
3.13 -Pure/codegen.ML. It relies critically on the FindTheorems solves
3.14 +The implementation is based in part on Berghofer and Haftmann's
3.15 +quickcheck.ML. It relies critically on the FindTheorems solves
3.16 feature.
3.17 *)
3.18
3.19 @@ -29,58 +29,48 @@
3.20 let
3.21 val ctxt = Proof.context_of state;
3.22
3.23 - fun conj_to_list [] = []
3.24 - | conj_to_list (t::ts) =
3.25 - (Conjunction.dest_conjunction t
3.26 - |> (fn (t1, t2) => conj_to_list (t1::t2::ts)))
3.27 - handle TERM _ => t::conj_to_list ts;
3.28 -
3.29 val crits = [(true, FindTheorems.Solves)];
3.30 - fun find g = (NONE, snd (FindTheorems.find_theorems ctxt g (SOME (!limit)) false crits));
3.31 - fun find_cterm g = (SOME g, snd (FindTheorems.find_theorems ctxt
3.32 - (SOME (Goal.init g)) (SOME (!limit)) false crits));
3.33 + fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
3.34
3.35 fun prt_result (goal, results) =
3.36 let
3.37 - val msg = case goal of
3.38 - NONE => "The current goal"
3.39 - | SOME g => Syntax.string_of_term ctxt (term_of g);
3.40 + val msg =
3.41 + (case goal of
3.42 + NONE => "The current goal"
3.43 + | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
3.44 in
3.45 - Pretty.big_list (msg ^ " could be solved directly with:")
3.46 - (map (FindTheorems.pretty_thm ctxt) results)
3.47 + Pretty.big_list
3.48 + (msg ^ " could be solved directly with:")
3.49 + (map (FindTheorems.pretty_thm ctxt) results)
3.50 end;
3.51
3.52 fun seek_against_goal () =
3.53 - let
3.54 - val goal = try Proof.get_goal state
3.55 - |> Option.map (#2 o #2);
3.56 -
3.57 - val goals = goal
3.58 - |> Option.map (fn g => cprem_of g 1)
3.59 - |> the_list
3.60 - |> conj_to_list;
3.61 -
3.62 - val rs = if length goals = 1
3.63 - then [find goal]
3.64 - else map find_cterm goals;
3.65 - val frs = filter_out (null o snd) rs;
3.66 -
3.67 - in if null frs then NONE else SOME frs end;
3.68 + (case try Proof.get_goal state of
3.69 + NONE => NONE
3.70 + | SOME (_, (_, goal)) =>
3.71 + let
3.72 + val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1);
3.73 + val rs =
3.74 + if length subgoals = 1
3.75 + then [(NONE, find goal)]
3.76 + else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
3.77 + val results = filter_out (null o snd) rs;
3.78 + in if null results then NONE else SOME results end);
3.79
3.80 fun go () =
3.81 let
3.82 - val res = TimeLimit.timeLimit
3.83 - (Time.fromMilliseconds (! auto_time_limit))
3.84 - (try seek_against_goal) ();
3.85 + val res =
3.86 + TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit))
3.87 + (try seek_against_goal) ();
3.88 in
3.89 - case Option.join res of
3.90 - NONE => state
3.91 - | SOME results => (Proof.goal_message
3.92 - (fn () => Pretty.chunks [Pretty.str "",
3.93 - Pretty.markup Markup.hilite
3.94 - (Library.separate (Pretty.brk 0)
3.95 - (map prt_result results))])
3.96 - state)
3.97 + (case res of
3.98 + SOME (SOME results) =>
3.99 + state |> Proof.goal_message
3.100 + (fn () => Pretty.chunks
3.101 + [Pretty.str "",
3.102 + Pretty.markup Markup.hilite
3.103 + (separate (Pretty.brk 0) (map prt_result results))])
3.104 + | _ => state)
3.105 end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
3.106 in
3.107 if int andalso ! auto andalso not (! Toplevel.quiet)
4.1 --- a/src/Tools/quickcheck.ML Tue Mar 31 21:39:56 2009 +0200
4.2 +++ b/src/Tools/quickcheck.ML Tue Mar 31 22:25:46 2009 +0200
4.3 @@ -1,4 +1,4 @@
4.4 -(* Title: Pure/Tools/quickcheck.ML
4.5 +(* Title: Tools/quickcheck.ML
4.6 Author: Stefan Berghofer, Florian Haftmann, TU Muenchen
4.7
4.8 Generic counterexample search engine.