Re: [isabelle] simp_trace_new



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.