Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] simp_trace_new

Email Gateway (Aug 19 2022 at 16:44):

From: Walther Neuper <wneuper@ist.tugraz.at>
Following a recent hint (cited at the bottom below) I tried to inspect
(in Isabelle2014), which rewrite rules are used by "auto" for proving
this lemma:

lemma "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
using [[simp_trace_new mode=full]]
using [[simp_break "_ ⟶ _"]]
by auto

With focus on "auto" <Output> indeed shows

lemma (∃x. ∀y. ?P x y) ⟶ (∀y. ∃x. ?P x y)
See <simplifier trace>

but klicking "<simplifier trace>" opens two empty windows.

Now I don't know whether

• "auto" doesn't need the simplifier in the above proof
• there is something I am doing wrong
• the hint below does not yet apply to Isabelle2014.

Thanks a lot in advance,
Walther

PS: "isar-ref" explains "simp_trace_new" and "simp_break", but my
questions above remain; in "jedit" I found no match.

On 14-11-28 03:25 PM, Tobias Nipkow wrote:

:
:
How to find out? Put "using [[simp_trace_new mode=full]]" in front of
your simp/auto command.

Tobias

Email Gateway (Aug 19 2022 at 16:44):

From: Lawrence Paulson <lp15@cam.ac.uk>
Your problem is purely logical and should be proved by the logical part of “auto” before simplification gets invoked.

Larry Paulson

Email Gateway (Aug 19 2022 at 16:47):

From: Walther Neuper <wneuper@ist.tugraz.at>
Hi David,

thanks a lot for your reply to my questions in isabelle-users@ ...

lemma "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
using [[simp_trace_new mode=full]]
using [[simp_break "_ ⟶ _"]]
by auto
With focus on "auto" <Output> indeed shows
lemma (∃x. ∀y. ?P x y) ⟶ (∀y. ∃x. ?P x y)
See <simplifier trace>
but klicking "<simplifier trace>" opens two empty windows.

Now I don't know whether * "auto" doesn't need the simplifier in the above proof * there is something I am doing wrong * "simp_trace_new mode=full" does not yet apply to Isabelle2014.
If the simplifier trace doesn't help you, you might want to look
at Daniel Matichuk's "apply_trace" command, which I have described
at:
http://stackoverflow.com/a/26827242/570879
... this looks great ...

(* attempt 5 to watch *)
lemma "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
apply_trace auto
done
(*used theorems:
allE: ∀x. ?P x ⟹ (?P ?x ⟹ ?R) ⟹ ?R
allI: (⋀x. ?P x) ⟹ ∀x. ?P x
ccontr: (¬ ?P ⟹ False) ⟹ ?P
exE: ∃x. ?P x ⟹ (⋀x. ?P x ⟹ ?Q) ⟹ ?Q
exI: ?P ?x ⟹ ∃x. ?P x
impI: (?P ⟹ ?Q) ⟹ ?P ⟶ ?Q
swap: ¬ ?P ⟹ (¬ ?R ⟹ ?P) ⟹ ?R *)

... and seems to give a negative answer to our ultimate question: Can we
have a "naive mathematician's approach" to simple quantifier reasoning
in Isabelle without delving down to the meta-logic?

Walther

Email Gateway (Aug 19 2022 at 16:47):

From: Lawrence Paulson <lp15@cam.ac.uk>
Isabelle is a logical framework, and that is how quantifier rules are expressed. The declarative representation of quantifier rules in the meta-logic is clearer, I hope, than the common alternative of representing them as computer code.

Larry Paulson

Email Gateway (Aug 19 2022 at 16:47):

From: Makarius <makarius@sketis.net>
The "meta-logic" is just a formal notation for Natural Deduction rules,
and not much delving is required.

Alternatively, it is always possible to print rules as Isar statements,
e.g. as in the 'print_statement' command.

Makarius

http://stop-ttip.org 1,069,976 people so far

Last updated: Nov 21 2024 at 12:39 UTC