--- 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 *)
--- 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
--- 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 **)
--- 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)
--- 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.