# Re: [isabelle] HELP

```Hi Adamu,

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

On 09/07/14 18:29, Adamu Sani YAHAYA wrote:
```
```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
```