Gergely Buday (Jan 20 2021 at 08:53): Gergely Buday (Jan 20 2021 at 08:53):I got
show add (Suc m) n = add n (Suc m)
Successful attempt to solve goal by exported rule:
(add ?ma2 n = add n ?ma2) ⟹ add (Suc ?ma2) n = add n (Suc ?ma2)
proof (state)
this:
add (Suc m) n = add n (Suc m)
goal:
No subgoals!
Failed to finish proof⌂:
goal (1 subgoal):
So once no subgoals, on the other hand Failed to finish proof.
Does the first relate to to the Suc m case and the failed proof to the top level theorem?
lemma add_commute: "add m n = add n m"
proof (induction m)
case 0
then show ?case by (simp add: add_0_right)
next
case (Suc m)
then show ?case by (simp)
qed
Manuel Eberl (Jan 20 2021 at 08:56):Please use code blocks for readability like this:
```isabelle
lemma "x = x"
by (rule refl)
```
It looks like this:
lemma "x = x"
by (rule refl)
show can fail in two ways: 1. there can be no corresponding to prove (e.g., no such goal generated by induction). 2. discharging the goal can fail because the tactic fails.
Mathias Fleury (Jan 20 2021 at 09:00):To make it easier understand the difference, do not show the state in the output panel (untick the "Proof state"). The state panel refers to the global state and the output panel to the current goal.
Manuel Eberl (Jan 20 2021 at 09:00):If there's read text and a Failed to finished proofs, that is what counts.
The no subgoals is a consequence of the fact that proofs with by are forked in Isabelle, i.e. when Isabelle encounters a by, the theorem is immediately considered as proven and you can carry on doing things. The proof is forked to the background and if it fails at some point, you get an error, but the theorem is still there.
This is to make working easier (and faster) in interactive mode. For the batch mode, there is a phase in the end where it waits for all these forked proofs to complete, and if there are any errors, the build fails.
Gergely Buday (Jan 20 2021 at 09:41):Thanks.
Last updated: Apr 25 2024 at 08:20 UTC