I am to finish a subproof in this
locale sig =
fixes le:: "'a ⇒ 'a ⇒ bool" (infixl "≤" 50)
assumes refl: "x ≤ x"
and antisym: "x ≤ y ⟹ y ≤ x ⟹ x = y"
and trans: "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
and total: "x ≤ y ∨ y ≤ x"
fun min :: "'a ⇒ 'a ⇒ 'a" where
"min a b = (if (a ≤ b) then a else b)"
lemma "min a b = a ∨ min a b = b"
have "m = (if (a ≤ b) then a else b) ⟹ m = a ∨ m = b" by auto
from this show ?thesis by simp
lemma (in sig) case_min:
assumes less: "(x ≤ y ⟹ P x)"
assumes greater: "(y ≤ x ⟹ P y)"
shows "P (min x y)"
have uf: "P (if (x ≤ y) then x else y) ⟹ P (min x y)" unfolding min_def by simp
from less greater have "P (if (x ≤ y) then x else y)"
proof (cases "x ≤ y")
note xlessy = this
from xlessy have "P x" by (rule less)
from this xlessy less greater show "?thesis" by (simp )
note not_xlessy = this
have not_imp_rev: "y ≤ x" using not_xlessy local.total by auto
from not_imp_rev have py: "P y" using greater by simp
have not_imp_y: "¬ x ≤ y ⟹ (if (x ≤ y) then x else y) = y" by simp
from this have "P(if (x ≤ y) then x else y)" using not_xlessy py by simp
from this show "?thesis" by simp
For this last line, I get
Illegal application of proof command in "chain" mode
Do Isabelle say this for the last "show"? In my understanding, "from" shifts the virtual machine into "chain" mode.
When there is more than one error message, you should always look at the first one. In this case, the first error message is
Failed to refine any pending goal Local statement fails to refine any pending goal Failed attempt to solve goal by exported rule: (x ≤ y) ⟹ (¬ x ≤ y) ⟹ P (if x ≤ y then x else y)
Essentially, what you are trying to
show does not correspond to any of your actual goals. Usually, it's quite obvious why that is the case, although there are some cases where one has to look very closely (e.g. when types of polymorphic functions don't match up). In this case, it is simply because you forgot to add a
next after you concluded the
True case. Without a
next, all the fixed variables and assumptions from the
True case are still around.
By the way, your other lemma about
min above can be done with
by simp. I very much doubt that your Isar proof for it actually does anything because that variable
m that you use in it is not fixed anywhere (that's why it is with an orange background). So I'm pretty sure Isabelle will basically ignore that statement in the final step and just prove the goal directly.
Last updated: Sep 25 2021 at 10:20 UTC