Commit fedcd127 authored by Raphael Cauderlier's avatar Raphael Cauderlier
Browse files

Hol naturals instantiation but holide files still missing

parent e6432f53
......@@ -2,10 +2,6 @@
open "basics";;
(* Explicit application to help Zenon accept applied variables *)
let ( @ ) (f, x) = f(x);;
(* The basic block: Peano axiomatization of natural numbers *)
species NatDecl =
......@@ -13,10 +9,12 @@ species NatDecl =
signature succ : Self -> Self;
property zero_succ : all n : Self, ~(zero = succ(n));
property succ_inj : all m n : Self, succ(m) = succ(n) -> m = n;
(* Highr-order axiom, cannot be given to Zenon *)
property ind : all p : Self -> prop,
p @ zero ->
(all n : Self, p @ n -> p @ (succ(n))) ->
all n : Self, p @ n;
p (zero) ->
(all n : Self, p(n) -> p(succ(n))) ->
all n : Self, p(n);
end;;
species NatCase =
......@@ -32,7 +30,8 @@ species NatCase =
<1>2 prove casep(zero) ->
(all n : Self, casep(n) -> casep(succ(n))) ->
all n : Self, casep(n)
dedukti proof property ind {* abst_ind abst_casep *}
dedukti proof property ind
{* abst_ind abst_casep *}
<1>3 prove casep(zero) by step <1>1
<1>4 assume n : Self, prove casep(succ(n)) by step <1>1
<1>f conclude;
......
......@@ -21,10 +21,10 @@ let hsucc (n : hnat) = internal hnat
| dedukti -> {* natural__div__full.Number_2ENatural_2Esuc n *};;
theorem hol_induction :
all p : hnat -> bool,
(p(hzero) /\ (all n : hnat, p(n) -> p(hsucc(n)))) ->
(all n : hnat, p(n))
proof = dedukti proof {* natural__div__full.thm_3723. *};;
all p : hnat -> prop,
(p(hzero) /\ (all n : hnat, p(n) -> p(hsucc(n)))) ->
(all n : hnat, p(n))
proof = dedukti proof {* natural__div__full.thm_3723. *};;
species HolNatDecl =
inherit NatDecl;
......@@ -162,10 +162,10 @@ species HolPlus =
definition of plus, succ
{* natural__div__full.thm_10450. *};
proof of plus_zero =
dedukti proof
definition of plus, zero
{* natural__div__full.thm_10569. *};
(* proof of plus_zero = *)
(* dedukti proof *)
(* definition of plus, zero *)
(* {* natural__div__full.thm_10569. *}; *)
end;;
collection HolPlusColl = implement HolPlus; end;;
......@@ -283,7 +283,8 @@ species HolDiv =
logical let divides (p, q) = hol_divides(p, q);
proof of divides_times = by definition of divides, times property hol_divides_times2;
proof of divides_le =
theorem divides_le : all m n : Self, divides(m, n) -> le(succ(succ(zero)), n) -> le(m, n)
proof =
<1>1 assume m n : Self,
hypothesis H1 : divides(m, n),
hypothesis H2 : le(succ(succ(zero)), n),
......@@ -485,22 +486,22 @@ theorem hol_prime_divisor :
(~(n = hol_one)) -> ex p : hnat, hol_prime(p) /\ hol_divides(p, n)
proof = dedukti proof {* natural__div__full.thm_33959. *};;
species HolPrimeDiv =
inherit NatPrimeDiv, HolPrime;
proof of prime_divisor =
by property hol_prime_divisor, hol_one_succ
definition of prime, divides, succ, zero;
let primediv_pred (n : hnat, p : hnat) = internal bool
external | dedukti -> {* hol.and (hol_prime p) (hol_divides p n) *};
proof of primediv_pred_spec =
<1>1 assume n p : Self,
prove (primediv_pred(n, p) <-> (prime(p) /\ divides(p, n)))
dedukti proof definition of primediv_pred, prime, divides
{* hol.REFL hol.bool (abst_primediv_pred n p) *}
<1>f conclude;
end;;
collection HolPrimeDivColl =
implement HolPrimeDiv;
end;;
(* species HolPrimeDiv = *)
(* inherit NatPrimeDiv, HolPrime; *)
(* proof of prime_divisor = *)
(* by property hol_prime_divisor, hol_one_succ *)
(* definition of prime, divides, succ, zero; *)
(* let primediv_pred (n : hnat, p : hnat) = internal bool *)
(* external | dedukti -> {* hol.and (hol_prime p) (hol_divides p n) *}; *)
(* proof of primediv_pred_spec = *)
(* <1>1 assume n p : Self, *)
(* prove (primediv_pred(n, p) <-> (prime(p) /\ divides(p, n))) *)
(* dedukti proof definition of primediv_pred, prime, divides *)
(* {* hol.REFL hol.bool (abst_primediv_pred n p) *} *)
(* <1>f conclude; *)
(* end;; *)
(* collection HolPrimeDivColl = *)
(* implement HolPrimeDiv; *)
(* end;; *)
......@@ -48,6 +48,7 @@ end;;
(* We lack polymorphism here as it is often convenient to
iterate a function over an other type than natural numbers,
in particular to define morphisms *)
let ( @ )(f, x) = f(x);;
species NatIter =
inherit NatCase;
signature iter : (Self -> Self) -> Self -> Self -> Self;
......
......@@ -140,7 +140,7 @@ species NatDividesZenon =
external | dedukti -> {* dk_logic.select abst_T p *};
theorem choice : all p : Self -> bool,
all x : Self, p @ x -> p @ select(p)
all x : Self, p(x) -> p(select(p))
proof = dedukti proof definition of select
{* dk_logic.choice abst_T. *};
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment