Re: [isabelle] proof by contradiction



Dear Adamu,

what kind of proof do you need?

An automatic one is easy:

  using axiom1 axiom2 by blast

Just applying proof by contradiction is also easy:

just typing

"proof"

applies the default rule, which in your case is proof-by-contradiction!

Best regards,
René

Am 10.07.2014 um 18:38 schrieb Adamu Sani YAHAYA <adamusaniyahaya at gmail.com>:

> hello,
> please can anyone help me with a hint of our to prove this codes with by
> contradiction.
> ======================================
> theory testing2 imports "~~/src/HOL/Main" begin
> 
> locale geometry =
>  fixes parallel :: "'line ⇒ 'line ⇒ bool"
>  and intersect :: "'line ⇒ 'line ⇒ bool"
>  and angle :: "'line ⇒ 'line ⇒ nat"
>  assumes axiom1: "parallel l1 l2 ⟹ angle l1 l2 = 0"
>  and axiom2: "intersect l1 l2 ⟹ ¬ (angle l1 l2 = 0)"
> begin
> 
> lemma parallel_not_intersect: "parallel l1 l2 ⟹ ¬ intersect l1 l2"
> =================================================
> thanks
> Adamu
> 





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