Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] HELP


view this post on Zulip Email Gateway (Aug 19 2022 at 15:17):

From: Adamu Sani YAHAYA <adamusaniyahaya@gmail.com>
Hello,
here is a coq codes
==============================
Variable line: Set.
Variable parallel:line -> line -> bool.

Variable intersect: line -> line -> bool.
Variable angle : line -> line -> nat.

Hypothesis axiom1: forall l1 l2:line,
parallel l1 l2 = true -> angle l1 l2 =0.

Hypothesis axiom2 : forall l1 l2:line,
angle l1 l2 =0 -> intersect l1 l2 = false.

Lemma parrallel_not_intersect: forall l1 l2:line,
parallel l1 l2 = true -> intersect l1 l2 = false.
intros.
assert (parallel l1 l2 = true -> intersect l1 l2 = false).
intro;apply axiom2;apply axiom1;assumption.
apply H0.
auto.
Qed.
===========================================
please can anyone give me a hint how to convert this coq codes to
Isabelle/HOL.
Thanks
Adamu

view this post on Zulip Email Gateway (Aug 19 2022 at 15:18):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Adamu,

How about the following?

theory Geometry 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: "angle l1 l2 = 0 ⟹ ¬ intersect l1 l2"
begin

lemma parallel_not_intersect: "parallel l1 l2 ⟹ ¬ intersect l1 l2"
apply(rule axiom2)
apply(rule axiom1)
apply assumption
done

end

end

Hope this helps,
Andreas


Last updated: Mar 28 2024 at 16:17 UTC