# 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`

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