Email Gateway (Aug 19 2022 at 15:17): 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
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: Nov 21 2024 at 12:39 UTC