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