Re: [isabelle-dev] Metis: Unused Theorem Reduces Run-Time?
Hi Tjark, Am 18.01.2013 um 16:44 schrieb Tjark Weber: > The new AFP entry on Kleene Algebras contains a metis call > (http://afp.hg.sourceforge.net/hgweb/afp/afp/file/082b389cb3f8/thys/Kleene_Algebra/Kleene_Algebra.thy#l652) > that generates a warning about an unused theorem local.opp_mult_def. > Not passing opp_mult_def as an argument to metis gets rid of the > warning, but increases run-time of this metis call from ~ 1 s to ~ 15 s > on my machine. Sure, these things happen with pretty much any tool that performs a heuristic search. There are even (rare) cases where taking out the unused theorems will lead to an unprovable first-order problem (because of incompletenesses in the translation of HO constructs). What's your concrete suggestion here? Cheers, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Metis: Unused Theorem Reduces Run-Time?
Hi, The new AFP entry on Kleene Algebras contains a metis call (http://afp.hg.sourceforge.net/hgweb/afp/afp/file/082b389cb3f8/thys/Kleene_Algebra/Kleene_Algebra.thy#l652) that generates a warning about an unused theorem local.opp_mult_def. Not passing opp_mult_def as an argument to metis gets rid of the warning, but increases run-time of this metis call from ~ 1 s to ~ 15 s on my machine. Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Resolve with premises
Hi all,
as the question currently arose on the users list, I remembered that I
have the following method laying around since several month. I'm using
it frequently in apply-style scripts (Mainly to apply induction
hypotheses).
We discussed here in Munich whether we should add it to Isabelle. Should
we? Opinions?
Peter
---
ML {*
(* Resolve with premises. Copied and adjusted from
Goal.assume_rule_tac. *)
fun rprems_tac ctxt = Goal.norm_hhf_tac THEN' CSUBGOAL (fn (goal, i)
=>
let
fun non_atomic (Const ("==>", _) $ _ $ _) = true
| non_atomic (Const ("all", _) $ _) = true
| non_atomic _ = false;
val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
val goal'' = Drule.cterm_rule
(singleton (Variable.export ctxt' ctxt)) goal';
val Rs = filter (non_atomic o Thm.term_of)
(Drule.strip_imp_prems goal'');
val ethms = Rs |> map (fn R =>
(Raw_Simplifier.norm_hhf (Thm.trivial R)));
in eresolve_tac ethms i end
);
(* Resolve with premise. Copied and adjusted from
Goal.assume_rule_tac. *)
fun rprem_tac n ctxt = Goal.norm_hhf_tac THEN' CSUBGOAL (fn (goal,
i) =>
let
val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
val goal'' = Drule.cterm_rule
(singleton (Variable.export ctxt' ctxt)) goal';
val R = nth (Drule.strip_imp_prems goal'') (n - 1)
val rl = Raw_Simplifier.norm_hhf (Thm.trivial R)
in
etac rl i
end
);
val setup =
Method.setup @{binding rprems}
(Scan.lift (Scan.option Parse.nat) >> (fn i => fn ctxt =>
SIMPLE_METHOD' (
case i of
NONE => rprems_tac ctxt
| SOME i => rprem_tac i ctxt
))
)
"Resolve with premises"
*}
setup "setup"
(* EXAMPLES: *)
lemma "\ A\B; B\C; A \
\ C"
apply (rprems 2) -- "Explicitely specify number of premise"
apply (rprems 1)
.
lemma "\ A\B; B\C; A \
\ C"
apply (rprems) -- "Resolve with any matching premise,
first to last, backtracking"
apply (rprems)
.
--
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] key bindings
I have updated, see below: ~/isabelle/Repos/src/HOL: hg id 00d87ade2294 tip ~/isabelle/Repos/src/HOL: isabelle components -l Available components: /Users/lp15/isabelle/Repos /Users/lp15/isabelle/Repos/src/Tools/Code /Users/lp15/isabelle/Repos/src/Tools/jEdit /Users/lp15/isabelle/Repos/src/Tools/Graphview /Users/lp15/isabelle/Repos/src/Tools/WWW_Find /Users/lp15/isabelle/Repos/src/HOL/Mirabelle /Users/lp15/isabelle/Repos/src/HOL/Mutabelle /Users/lp15/isabelle/Repos/src/HOL/Library/Sum_of_Squares /Users/lp15/isabelle/Repos/src/HOL/Tools/ATP /Users/lp15/isabelle/Repos/src/HOL/Tools/Predicate_Compile /Users/lp15/isabelle/Repos/src/HOL/Tools/Sledgehammer/MaSh /Users/lp15/isabelle/Repos/src/HOL/Tools/SMT /Users/lp15/isabelle/Repos/src/HOL/TPTP /Users/lp15/isabelle/Repos/Admin /Users/lp15/.isabelle /Users/lp15/.isabelle/contrib/cvc3-2.4.1 /Users/lp15/.isabelle/contrib/e-1.6-2 /Users/lp15/.isabelle/contrib/exec_process-1.0.3 /Users/lp15/.isabelle/contrib/Haskabelle-2013 /Users/lp15/.isabelle/contrib/jdk-7u11 /Users/lp15/.isabelle/contrib/jedit_build-20130104 /Users/lp15/.isabelle/contrib/jfreechart-1.0.14 /Users/lp15/.isabelle/contrib/kodkodi-1.5.2 /Users/lp15/.isabelle/contrib/polyml-5.5.0 /Users/lp15/.isabelle/contrib/scala-2.10.0 /Users/lp15/.isabelle/contrib/spass-3.8ds /Users/lp15/.isabelle/contrib/z3-3.2 Missing components: ~/isabelle/Repos/src/HOL: And I have to say, it looks very much better! The difference from just last week's version is remarkable. I'm afraid that the crash is still there. By crash, I mean everything dies. I've attached a core dump. To do this, I select Utilities > Global Options > Shortcuts. In the filter, I type "select code block", choose the key binding CMD-[, and when it asks whether to overwrite an existing binding, click YES. Larry hs_err_pid2302.log Description: Binary data On 17 Jan 2013, at 12:59, Makarius wrote: > On Thu, 17 Jan 2013, Lawrence Paulson wrote: > > Depending what you mean by "crash", this hyperreactive popup might cause > problems on Mac OS X. > > >> ~/isabelle/Repos/src/HOL: hg id >> cbc7002cc273 tip >> ~/isabelle/Repos/src/HOL: isabelle component -l >> >> Available components: >> /Users/lp15/.isabelle/contrib/jdk-7u9 > > This is already 1 week old. In the meantime Oracle puslished jdk-7u11 and I > updated to it. This might or might not improve the Java-on-Mac situation > again a tiny little bit. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
