Re: [isabelle] proof by contradiction
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:
applies the default rule, which in your case is proof-by-contradiction!
Am 10.07.2014 um 18:38 schrieb Adamu Sani YAHAYA <adamusaniyahaya at gmail.com>:
> please can anyone help me with a hint of our to prove this codes with by
> 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)"
> lemma parallel_not_intersect: "parallel l1 l2 ⟹ ¬ intersect l1 l2"
This archive was generated by a fusion of
Pipermail (Mailman edition) and