# Notes on Isar keywords

Jump to navigation
Jump to search

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

### Using proper "obtain" instead

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`

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