Email Gateway (Aug 19 2022 at 15:20): Email Gateway (Aug 19 2022 at 15:20):From: Adamu Sani YAHAYA <adamusaniyahaya@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
Email Gateway (Aug 19 2022 at 15:20):From: René Thiemann <rene.thiemann@uibk.ac.at>
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é
Last updated: Apr 25 2024 at 16:19 UTC