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"

begin

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"

proof -

have "m = (if (a ≤ b) then a else b) ⟹ m = a ∨ m = b" by auto

from this show ?thesis by simp

qed

lemma (in sig) case_min:

assumes less: "(x ≤ y ⟹ P x)"

assumes greater: "(y ≤ x ⟹ P y)"

shows "P (min x y)"

proof -

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")

case True

note xlessy = this

from xlessy have "P x" by (rule less)

from this xlessy less greater show "?thesis" by (simp )

case False

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.

Thanks.

Last updated: Jun 20 2024 at 12:31 UTC