Re: [isabelle] HELP



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

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
  Adamu





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.