Re: [isabelle] simp_trace_new

On Mon, 8 Dec 2014, Walther Neuper wrote:

 (* attempt 5 to watch *)
 lemma "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
 apply_trace auto
 (*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?

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.


           1,069,976 people so far

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