Re: [isabelle] Natural property




Hello Gabriele,

Amine wrote:
Now from
a * 1 < b * (a + 1)
I would demonstrate the thesis but I don't know how to do that.

You just need to use the Ex-Introduction rule, i.e. append

thus ?thesis
  apply(rule_tac x="1" in exI) apply (rule_tac x="a+1" in exI)
    by simp

to your proof.

Nicer still, and more in the Isar spirit:

- Replace "proof -" by "proof (intro exI)". This applies exI in backward style,
leaving you a schematic goal.

- Replace the last "have" by "show", since this is already an instance of the goal.

- add "qed" in the end :-)

If you had only one existential quantifier instead of two, you could even drop the "(intro exI)", but in your case, this would only eliminate one of the quantifications... The "intro" method applies the supplied introduction rules repeatedly.

Alex





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.