CODEWITHSUNDEEP
isabellesimplification
IIM
IIM

Reputation: 533

Manually adding an assumption to the simplifier (Isabelle)

I was trying to complete a proof in Isabelle which now works:

lemma axiom1: " x = y ⟹ Δ x y z = 0"
  proof -
    assume 1[simp]: "x = y"
    have 1: "Δ x y z = Δ y z x" by (rule axiom0_a)
    also have "… = Δ y z y" by simp
    also have "… = Δ z y y" by (rule axiom0_a)
    moreover have "Δ y y z  = - Δ z y y" by (rule axiom0_b)
    moreover have "⋀r. ((r::real) = - r ⟹ r = 0)" by simp
    ultimately show "Δ x y z = 0" by simp
  qed

However, I had to manually add the assumption to the simplifier. My question is, will the additional rule in the simplifier x=y remain local to this proof, or will it be used in other proofs (which would cause some problems)? Also, I thought the assumptions were automatically added to the simplifier: is the reason why this assumption wasn't because it would give some danger of looping?

Upvotes: 0

Views: 244

Answers (1)

Peter Zeller
Peter Zeller

Reputation: 2276

  1. The assumption will remain local. It can only be used where the name 1 is also valid
  2. Assumptions are automatically used by the simplifier, but when you start the proof it is no longer an assumption in your current subgoal.

If you do a structured proof, it often works better to also write down the lemma in a structured way with assumes and shows: 

lemma axiom1: 
assumes 1[simp]: "x = y"
shows "Δ x y z = 0"
...

Upvotes: 1

Related Questions