Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step



On 27.02.2013 23:21, Gottfried Barrow wrote:
(A = B) ====> (A seO B) --> (A = B),

where "====>" means I have to convert (A=B) into the form (A seO B)
before anything can be proved, and I can't get the simplifier to convert
(A=B) to something like (A seO B), which I suppose is for good reason,
since "=" is used everywhere. (In a manner of speaking, I manually
convert (A=B) to (A seO B) as the first step in the proof.)

Actually, this kind of thing is good use case for introduction rules. Given a rule X: "A se0 B ==> A = B", you could perform the proof with

  by (rule X) simp

or, for a structured proof:

proof (rule X)
  ...
qed

If declared with [intro?], rule (and hence proof) will automatically pickup this rule.

  -- Lars





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