Notes on Isar keywords

Some usage notes on Isar keywords.

`guess`

You have to specify what you get, when you obtain a variable? I guess not.

The canonical form is

have "∃x. f x = 0"
then obtain x where x: "f x = 0" by auto

However you can also do the following:

have "∃x. f x = 0"
then guess x .. note x=this

Instead of ".." you can also write "by(erule exE)" or "apply(erule exE) ."

have "∃x. f x = 0 ∧ f y = 0"
then guess x by(erule exE,erule conjE) note x = this

In many cases, Isabelle is able to prove

obtain x where x:"f x = 0" by auto

directly. If not, you can tell Isabelle to transform the obtain-goal to "∃x. f x = 0" automatically by using the atomize_elim tactic:

obtain x where x:"f x = 0" by atomize_elim auto

Note allows naming a fact:

note new_name = fact

Usually on the right side is an expression involving this:

{ fix something assume "anything"
  hence "something else" by auto }
note P = this

More complicated expressions are also possible:

  note ab=conjunctD2[OF this(1)[unfolded interval_eq_empty not_ex not_less]] this(2-)