Very simple lemma in Isabelle

Question

I am just starting my first steps with Isabelle but, being new to theorem provers and proof assistants, I am a bit lost. I am mainly interested in applications to Functional Analysis or Algebra I looked at the documentation, and I am trying to get my own example using locales to work, but I ran into some very basic problems. My code is

theory MyTheory
imports Main
begin

locale semigroup_mult =
  fixes f :: "'a ⇒ 'a ⇒ 'a" (infixl "x" 70)
    and e :: 'a ("e")
  assumes assocm : "a x b x c = a x (b x c)"  
    and right_neutralm : "(a x e) = a"  
    and left_neutralm : "(e x a) = a"  
begin

lemma assoc_general: "b x (a x c) = (b x a) x c"  
  apply (rule assocm)
  done

end

end

This is just a one step proof, but I cannot make Isabelle to work... If I remove the apply line, it says it cannot complete the proof, and the apply command gives the error

Illegal application of proof command in "prove" mode

What am I doing wrong? Any help would be appreciated. For instance the difference between using the "show ... by" syntax and the "apply" syntax, "proof ... qed" and "done".

A secondary question is if it is possible for Isabelle to output proofs similar to what one might find in a undergraduate Math textbook.

chris chris · Accepted Answer · 2016-12-01T09:36:33

When I try your code with Isabelle/jEdit (Isabelle2016) I get the error message

Failed to apply proof method⌂:
goal (1 subgoal):
1. b x (a x c) = b x a x c

This tells us that it was not possible to apply the given rule (assocm) to the current subgoal. The reason is that rule tries to unify the conclusion of assocm (which is the whole lemma) with the current subgoal. If it would succeed it would replace the current subgoal by the assumptions of the lemma you applied, but in your example it doesn't succeed.

There are two ways around:

1) You could restate your lemma with swapped left- and right-hand sides. Then your current proof would work (trivially, because it is the same as assocm).

2) Or if you really just wanted to "replace equals by equals", you shouldn't use rule but instead simp or auto. E.g.

apply (simp add: assocm)

or alternatively in two steps

unfolding assocm
by (rule HOL.refl)

which first just replaces the left-hand side of assocm by its right-hand side and finally concludes the proof by reflexivity of equality.

To answer your secondary question: It is not possible to automatically transform some arbitrary proof into something akin to an undergrad textbook. However, it is most definitely possible -- given enough effort and the proper setup of automatic tools like simp, blast, and auto -- to write your proofs in such a style (within the confines of Isar syntax). E.g., the following examples shows some Isar features that make proofs more human readable:

lemma "(b x e) x e x (a x c) = b x a x c"
proof -
  have "b x e = b" by (rule right_neutralm)
  then have "(b x e) x e x (a x c) = b x (a x c)" by simp
  also have "... = b x a x c" by (rule assocm [symmetric])
  finally show ?thesis .
qed

However, it is more common to go for more automatic proofs like:

lemma "(b x e) x e x (a x c) = b x a x c"
  by (simp add: right_neutralm assocm)

Very simple lemma in Isabelle

1 Answers