Stream: Beginner Questions

Topic: Manual proof using <fname>.cases <fname.elims>

view this post on Zulip waynee95 (Jul 07 2022 at 15:44):

I have the following datatypes and functions

type_synonym variable = string

datatype bexpr =
    Const bool
  | Var variable
  | And bexpr bexpr
  | Or bexpr bexpr
  | Imp bexpr bexpr
  | Neg bexpr

datatype occ =
    Even
  | Odd
  | Both

fun negate :: "occ ⇒ occ" where
"negate Even = Odd" |
"negate Odd = Even" |
"negate Both = Both"

fun merge :: "occ ⇒ occ ⇒ occ" where
"merge x y = (if x = y then x else Both)"

primrec occurrences :: "bexpr ⇒ variable ⇒ occ" where
"occurrences (Const _) _ = Even" |
"occurrences (Var y) x = Even" |
"occurrences (And phi psi) x = (merge (occurrences phi x) (occurrences psi x))" |
"occurrences (Or phi psi) x = (merge (occurrences phi x) (occurrences psi x))" |
"occurrences (Imp phi psi) x = (merge (negate (occurrences phi x)) (occurrences psi x))" |
"occurrences (Neg phi) x = (negate (occurrences phi x))"

and I want to prove that

lemma negateOccEvenIsOdd: "negate (occurrences phi x) = Even ⟶ occurrences phi x = Odd"

I know that Sledgehammer automatically finds proofs for this, e.g. using negate.elims by blast or by (metis negate.cases negate.simps).

However, I want to prove this using Isar manually solely for learning purposes but I am a bit stuck on how to do that.

I managed to do an apply-style proof:

lemma negateOccEvenIsOdd: "negate (occurrences phi x) = Even ⟶ occurrences phi x = Odd"
  apply (rule impI)
  apply (erule negate.elims)
    apply simp
   apply simp
  apply simp
  done

view this post on Zulip Mathias Fleury (Jul 07 2022 at 15:49):

That proof looks like a candidate for apply (cases phi)

view this post on Zulip Mathias Fleury (Jul 07 2022 at 15:49):

And replace ⟶ by ==>

view this post on Zulip waynee95 (Jul 07 2022 at 16:45):

Since I wanted to do it in Isar, I did 

lemma "negate (occurrences phi x) = Even ⟹ occurrences phi x = Odd"
proof (cases phi)
  case (Const b)
...

view this post on Zulip Mathias Fleury (Jul 07 2022 at 16:49):

I would even go for:

lemma
  assumes "negate (occurrences phi x) = Even"
   shows "occurrences phi x = Odd"
proof (cases phi)

view this post on Zulip Mathias Fleury (Jul 07 2022 at 16:56):

I would go for:

lemma negate_Even_iff:
  ‹negate b = Even ⟷ b = Odd›
  by (cases b)
   (simp_all only: negate.simps occ.simps refl)

lemma
  assumes neg: "negate (occurrences phi x) = Even"
  shows "occurrences phi x = Odd"
  using assms
  apply (subst (asm) negate_Even_iff)
  apply assumption
  done

view this post on Zulip Mathias Fleury (Jul 07 2022 at 17:00):

This proof is also showing that my advice for cases phi was wrong, sorry

view this post on Zulip waynee95 (Jul 07 2022 at 17:01):

Mathias Fleury said:

This proof is also showing that my advice for cases phi was wrong, sorry

Yeah I was about to comment that I don't think cases phi is going to work. No worries though! Thanks for the comments.

Last updated: Apr 19 2024 at 01:05 UTC