Commit 32f60809 authored by Raphael Cauderlier's avatar Raphael Cauderlier
Browse files

Import HOL arith library

parent bad00f9d
......@@ -3,7 +3,10 @@
INCLUDE_DIRS=
DKTACTICS_DIR=$(shell $(DKTACTICS))
DKCHECK_OPT = $(INCLUDE_DIRS)
FOCALIZEC_OPT = $(INCLUDE_DIRS) -no-stdlib-path -no-ocaml-code -no-coq-code -stop-before-dk -dedukti-code
FOCALIZEC_OPT = $(INCLUDE_DIRS) -no-stdlib-path -dedukti-code -stop-before-zenon -no-ocaml-code
# Bash required for the %.art target in file interop/arith/Makefile
SHELL=/bin/bash
%.dko: %.dk
$(DKCHECK) $(DKCHECK_OPT) -e -nl $<
......@@ -11,9 +14,16 @@ FOCALIZEC_OPT = $(INCLUDE_DIRS) -no-stdlib-path -no-ocaml-code -no-coq-code -sto
%.dko: %.sk
$(SKCHECK) $(DKCHECK_OPT) -e -nl $<
%.sk: %.fcl
%.sk: %.sk.zv
$(ZVTOV) -zenon $(ZENON_MODULO) -new -idedukti $<
mv "$@.v" "$@"
%.sk.zv: %.fcl
$(FOCALIZEC) $(FOCALIZEC_OPT) $<
%.v: %.zv
$(ZVTOV) -zenon $(ZENON) -new -z '-x induct' $<
%.dk: %.art
$(HOLIDE) $< -o $@
......@@ -25,3 +35,4 @@ FOCALIZEC_OPT = $(INCLUDE_DIRS) -no-stdlib-path -no-ocaml-code -no-coq-code -sto
%.vo: %.v
$(COQC) $<
......@@ -124,7 +124,9 @@ these structures. For example, the structure of natural numbers with
addition is defined in the file [[./core/arith/naturals.fcl][core/arith/naturals.fcl]] but it does
not contain proofs for the associativity and commutativity of addition
because these properties are not helpful for proving transfer
theorems. They can however be imported from any arithmetic library so
theorems. It does however contain the theorem statements and proofs
that these properties can be transferred between isomorphic models of
the natural numbers. They can be imported from any arithmetic library so
they are proved in the interoperability library.
*** Logic
......@@ -215,6 +217,8 @@ integers.
=prime= is a predicate over natural numbers defined by the following axiom:
+ =prime(p) <-> lt(succ(zero), p) /\ all d : Self, ~(sd(d, p))=
The file
**** TODO Integers
*** TODO Algebra
......
......@@ -120,12 +120,23 @@ version_eq "${VERSIONS["SKCHECK"]}" "${VERSIONS["DKCHECK"]}" &&
find_binary_and_version "focalizec" "" "FOCALIZEC" "-v |& cut -d ' ' -f 5" &&
version_eq "${VERSIONS["FOCALIZEC"]}" "0.9.2" &&
find_binary_and_version "focalizedep" "" "FOCALIZEDEP" "" &&
## Zvtov is usually installed with FoCaLiZe
find_binary_and_version "zvtov" "" "ZVTOV" "-v |& cut -d ' ' -f 3" &&
version_eq "${VERSIONS["ZVTOV"]}" "0.6.0" &&
## Zenon
find_binary_and_version "zenon" "" "ZENON" "-v |& cut -d ' ' -f 3" &&
version_eq "${VERSIONS["ZENON"]}" "0.8.0" &&
## Zenon Modulo
find_binary_and_version "zenon_modulo" "" "ZENON_MODULO" "-v |& cut -d ' ' -f 3" &&
version_eq "${VERSIONS["ZENON_MODULO"]}" "0.4.3" &&
# Interop
## Coq
find_binary_and_version "coqc" "" "COQC" "-v | grep version | cut -d ' ' -f 6" &&
### Other Coq 8.4 versions probably work too but not >= 8.5
version_eq "${VERSIONS["COQC"]}" "8.4pl6" &&
COQV="${VERSIONS["COQC"]}"
print_to_file "COQ_VERSION=\"$COQV\"" &&
find_binary_and_version "coqtop" "" "COQTOP" "-v | grep version | cut -d ' ' -f 6" &&
version_eq "${VERSIONS["COQTOP"]}" "${VERSIONS["COQC"]}" &&
......
This diff is collapsed.
(* Axiomatic version of OpenTheory Arithmetic library upto product and ordering *)
open "basics";;
open "naturals";;
species NatPlusThm =
inherit NatPlus;
property plus_zero : all m : Self, plus(m, zero) = m;
property plus_succ : all m n : Self, plus(m, succ(n)) = succ(plus(m, n));
property plus_assoc : all m n p : Self, plus(plus(m, n), p) = plus(m, plus(n, p));
property plus_commutes : all m n : Self, plus(m, n) = plus(n, m);
property plus_regular_left : all m n p : Self, (plus(m, n)) = plus(m, p) <-> n = p;
property plus_regular_right : all m n p : Self, plus(m, p) = plus(n, p) <-> m = n;
property plus_is_zero : all m n : Self, plus(m, n) = zero <-> (m = zero /\ n = zero);
property plus_eq_left : all m n : Self, plus(m, n) = m <-> n = zero;
property plus_eq_right : all m n : Self, plus(m, n) = n <-> m = zero;
end;;
species NatPlusOne =
inherit NatPlus, NatOne;
property one_plus : all n : Self, plus(one, n) = succ(n);
property plus_one : all m : Self, plus(m, one) = succ(m);
end;;
species NatTimesThm =
inherit NatTimes;
property times_zero : all m : Self, times(m, zero) = zero;
property times_succ : all m n : Self, times(m, succ(n)) = plus(times(m, n), m);
property times_assoc : all m n p : Self, times(times(m, n), p) = times(m, times(n, p));
property times_commutes : all m n : Self, times(m, n) = times(n, m);
property times_regular_left : all m n p : Self, times(m, n) = times (m, p) <-> (n = p \/ m = zero);
property times_regular_right : all m n p : Self, times(m, p) = times (n, p) <-> (m = n \/ p = zero);
property times_is_zero : all m n : Self, times(m, n) = zero <-> (m = zero \/ n = zero);
end;;
species NatPlusTimes =
inherit NatTimes;
property plus_times : all m n p : Self, times(plus(m, n), p) = plus(times(m, p), times(n, p));
property times_plus : all m n p : Self, times(m, plus(n, p)) = plus(times(m, n), times(m, p));
end;;
species NatTimesOne =
inherit NatTimes, NatOne;
property one_times : all n : Self, times(one, n) = n;
property times_one : all m : Self, times(m, one) = m;
property times_eq_left : all m n : Self, times(m, n) = m <-> (m = zero \/ n = one);
property times_eq_right : all m n : Self, times(m, n) = n <-> (n = zero \/ m = one);
property times_is_1 : all m n : Self, times(m, n) = one <-> (m = one /\ n = one);
end;;
species NatLeThm =
inherit NatLe;
property le_zero : all m : Self, le(m, zero) <-> m = zero;
property le_succ : all m n : Self, le(m, succ(n)) <-> (m = succ(n) \/ le(m, n));
property le_n_succ_n : all n : Self, le(n, succ(n));
property zero_le : all n : Self, le(zero, n);
property le_succ_succ : all m n : Self, le(succ(m), succ(n)) <-> le(m, n);
property le_refl : all n : Self, le(n, n);
property le_refl_eq : all m n : Self, m = n -> le(m, n);
property le_trans : all m n p : Self, le(m, n) -> le(n, p) -> le(m, p);
property le_antisym : all m n : Self, le(m, n) -> le(n, m) -> m = n;
property le_total : all m n : Self, le(m, n) \/ le(n, m);
property le_predmax : all p : Self -> prop, ((ex n : Self, p(n)) /\ (ex m : Self, all n : Self, p(n) -> le(n, m))) <-> (ex m : Self, p(m) /\ all n : Self, p(n) -> le(n, m));
end;;
species NatPlusLe =
inherit NatLe;
property le_n_plus_m_n : all m n : Self, le(n, plus(m, n));
property le_m_plus_m_n : all m n : Self, le(m, plus(m, n));
property le_plus_plus_left : all m n p : Self, le(plus(m, n), plus(m, p)) <-> le(n, p);
property le_plus_plus_right : all m n p : Self, le(plus(n, m), plus(p, m)) <-> le(n, p);
property plus_le_left : all m n : Self, le(plus(m, n), m) <-> n = zero;
property plus_le_right : all m n : Self, le(plus(m, n), n) <-> m = zero;
property plus_increases : all m n p q : Self, le(m, p) -> le(n, q) -> le(plus(m, n), plus(n, q));
end;;
species NatTimesLe =
inherit NatTimes, NatLe;
property le_times_times_left : all m n p : Self, le(times(m, n), times(m, p)) <-> (m = zero \/ le(n, p));
property le_times_times_right : all m n p : Self, le(times(m, p), times(n, p)) <-> (le(m, n) \/ p = zero);
property le_square : all n : Self, le(n, times(n, n));
property times_le_is_zero : all a b : Self,
(all n : Self, le(times(a, n), b)) <-> a = zero;
property times_increases : all m n p q : Self, le(m, p) -> le(n, q) -> le(times(m, n), times(p, q));
end;;
species NatLtThm =
inherit NatLt;
property zero_lt : all n : Self, lt(zero, n) <-> (~ (n = zero));
property succ_lt : all m n : Self, lt(succ(m), succ(n)) <-> lt(m, n);
property zero_lt_succ : all n : Self, lt(zero, succ(n));
property succ_lt_succ : all m n : Self, lt(succ(m), succ(n)) <-> lt(m, n);
property lt_zero : all m : Self, ~ lt(m, zero);
property lt_succ : all m n : Self, lt(m, succ(n)) <-> (m = n \/ lt(m, n));
property lt_irrefl : all n : Self, ~ lt(n, n);
property lt_irrefl_diff : all m n : Self, lt(m, n) -> ~ (m = n);
property n_lt_succ_n : all n : Self, lt(n, succ(n));
property lt_trans : all m n p : Self, lt(m, n) -> lt(n, p) -> lt(m, p);
property lt_acyclic : all m n : Self, ~ (lt(m, n) /\ lt(n, m));
property lt_trichotomy : all m n : Self, lt(m, n) \/ lt(n, m) \/ m = n;
property strong_induction : all p : Self -> prop,
(all n : Self, (all m : Self, lt(m, n) -> p(m)) -> p(n)) ->
all n : Self, p(n);
property lt_predmin : all p : Self -> prop,
(ex n : Self, p(n)) <->
(ex n : Self, p(n) /\ all m : Self, lt(m, n) -> ~ p(m));
end;;
species NatLeLt =
inherit NatLt;
property not_le_lt : all m n : Self, (~ le(m, n)) <-> lt(n, m);
property not_lt_le : all m n : Self, (~ lt(m, n)) <-> le(n, m);
property lt_le_diff : all m n : Self, lt(m, n) <-> (le(m, n) /\ ~ (m = n));
property lt_le : all m n : Self, lt(m, n) -> le(m, n);
property le_lt_lt : all m n p : Self, le(m, n) -> lt(n, p) -> lt(m, p);
property lt_le_lt : all m n p : Self, lt(m, n) -> le(n, p) -> lt(m, p);
property lt_succ_le : all m n : Self, lt(m, succ(n)) <-> le(m, n);
property lt_or_le : all m n : Self, lt(m, n) \/ le(n, m);
property le_or_lt : all m n : Self, le(m, n) \/ lt(n, m);
property not_lt_and_le : all m n : Self, ~ (lt(m, n) /\ le(n, m));
property not_le_and_lt : all m n : Self, ~ (le(m, n) /\ lt(n, m));
property lt_succ_is_le : all m n : Self, lt(m, succ(n)) <-> le(m, n);
property le_succ_is_lt : all m n : Self, le(succ(m), n) <-> lt(m, n);
property le_lt_eq : all m n : Self, le(m, n) <-> (lt(m, n) \/ m = n);
end;;
species NatPlusLt =
inherit NatLt;
property not_plus_lt_left : all m n : Self, ~ lt(plus(m, n), m);
property not_plus_lt_right : all m n : Self, ~ lt(plus(m, n), n);
property lt_plus_left : all m n : Self, lt(m, plus(m, n)) <-> lt(zero, n);
property lt_plus_right : all m n : Self, lt(n, plus(m, n)) <-> lt(zero, m);
property lt_plus_plus_left : all m n p : Self, lt(plus(m, n), plus(m, p)) <-> lt(n, p);
property lt_plus_plus_right : all m n p : Self, lt(plus(n, m), plus(p, m)) <-> lt(n, p);
property lt_exists : all m n : Self, lt(m, n) <-> (ex d : Self, n = plus(m, succ(d)));
property plus_strictly_increases : all m n p q : Self, lt(m, p) -> lt(n, q) -> lt(plus(m, n), plus(p, q));
end;;
species NatPlusLeLt =
inherit NatLt;
property plus_plus_lt_le : all m n p q : Self, lt(m, p) -> le(n, q) -> lt(plus(m, n), plus(p, q));
property plus_plus_le_lt : all m n p q : Self, le(m, p) -> lt(n, q) -> lt(plus(m, n), plus(p, q));
end;;
species NatTimesLt =
inherit NatTimes, NatLt;
property lt_times_times_left : all m n p : Self, lt(times(m, n), times(m, p)) <-> (~ (m = zero) /\ lt(n, p));
property lt_times_times_right : all m n p : Self, lt(times(m, p), times(n, p)) <-> (lt(m, n) /\ ~ (p = zero));
property zero_lt_times : all m n : Self, lt(zero, times(m, n)) <-> (lt(zero, m) /\ lt(zero, n));
property pos_times_strictly_increases : all m n p : Self, ~ (m = zero) -> lt(n, p) -> lt(times(m, n), times(m, p));
property times_strictly_increases : all m n p q : Self, lt(m, p) -> lt(n, q) -> lt(times(m, n), times(p, q));
end;;
species NatFullThm =
inherit NatPlusThm, NatPlusOne, NatTimesThm, NatPlusTimes, NatTimesOne,
NatLeThm, NatPlusLe, NatTimesLe, NatLtThm, NatLeLt, NatPlusLt,
NatPlusLeLt, NatTimesLt;
end;;
......@@ -3,7 +3,7 @@ include ../../../Makefile.rules
FCL_FILES=$(wildcard *.fcl)
INCLUDE_DIRS= -I ../../logic -I ../definitions -I ../morphisms -I ../theorems
FOCALIZEC_OPT += -zvtovopt "-zenon 'zenon_transfer'" -no-coq-code
ZENON_MODULO=zenon_transfer
all: $(FCL_FILES:.fcl=.dko)
depend: .depend
......
(* Transfer theorems for the theorems in natthms.fcl *)
open "basics";;
open "naturals";;
open "natmorph_rev";;
open "natthms";;
(* Warning! All theorems in this file are admitted! *)
(* TODO: move the following false axiom to a separated file which is
not seen by Dedukti *)
let magic_axiom = internal bool
external
| dedukti -> {* dk_bool.true.
list_prop : Type.
nil_prop : list_prop.
cons_prop : dk_logic.Prop -> list_prop -> list_prop.
def proofs : list_prop -> dk_logic.Prop -> Type.
[P] proofs nil_prop P --> dk_logic.eP P
[A,As,P] proofs (cons_prop A As) P --> (dk_logic.eP A -> proofs As P).
def magic : Hyps : list_prop -> P : dk_logic.Prop -> proofs Hyps P *}
| coq -> {* true *}
;;
species NatPlusTransfer (A is NatPlusThm) =
inherit NatPlusMorph(A), NatPlusThm;
proof of plus_zero =
by property morph_zero, morph_plus, morph_injective, morph_surjective, A!plus_zero;
proof of plus_succ =
by property morph_succ, morph_plus, morph_injective, morph_surjective, A!plus_succ;
proof of plus_assoc =
by property morph_plus, morph_injective, morph_surjective, A!plus_assoc;
proof of plus_commutes =
by property morph_plus, morph_injective, morph_surjective, A!plus_commutes;
proof of plus_regular_left =
by property morph_plus, morph_injective, morph_surjective, A!plus_regular_left;
proof of plus_regular_right =
by property morph_plus, morph_injective, morph_surjective, A!plus_regular_right;
proof of plus_is_zero =
by property morph_plus, morph_injective, morph_surjective, A!plus_is_zero;
proof of plus_eq_left =
by property morph_zero, morph_plus, morph_injective, morph_surjective, A!plus_eq_left;
proof of plus_eq_right =
by property morph_zero, morph_plus, morph_injective, morph_surjective, A!plus_eq_right;
end;;
species NatPlusOneTransfer (A is NatPlusOne) =
inherit NatPlusMorph(A), NatOneMorph(A), NatPlusOne;
proof of one_plus =
by property morph_one, morph_plus, morph_injective, morph_surjective, A!one_plus;
proof of plus_one =
by property morph_one, morph_plus, morph_injective, morph_surjective, A!plus_one;
end;;
species NatTimesTransfer (A is NatTimesThm) =
inherit NatTimesMorph(A), NatTimesThm;
proof of times_zero =
by property morph_zero, morph_times, morph_injective, morph_surjective, A!times_zero;
proof of times_succ =
by property morph_succ, morph_times, morph_injective, morph_surjective, A!times_succ;
proof of times_assoc =
by property morph_times, morph_injective, morph_surjective, A!times_assoc;
proof of times_commutes =
by property morph_times, morph_injective, morph_surjective, A!times_commutes;
proof of times_regular_left =
by property morph_zero, morph_times, morph_injective, morph_surjective, A!times_regular_left;
proof of times_is_zero =
by property morph_zero, morph_times, morph_injective, morph_surjective, A!times_is_zero;
end;;
species NatPlusTimesTransfer (A is NatPlusTimes) =
inherit NatPlusMorph(A), NatTimesMorph(A), NatPlusTimes;
proof of plus_times =
by property morph_plus, morph_times, morph_injective, morph_surjective, A!plus_times;
proof of times_plus =
by property morph_plus, morph_times, morph_injective, morph_surjective, A!times_plus;
end;;
species NatTimesOneTransfer (A is NatTimesOne) =
inherit NatTimesMorph(A), NatOneMorph(A), NatTimesOne;
proof of one_times =
by property morph_times, morph_one, morph_injective, morph_surjective, A!one_times;
proof of times_one =
by property morph_times, morph_one, morph_injective, morph_surjective, A!times_one;
proof of times_eq_left =
by property morph_times, morph_one, morph_zero, morph_injective, morph_surjective, A!times_eq_left;
proof of times_eq_right =
by property morph_times, morph_one, morph_zero, morph_injective, morph_surjective, A!times_eq_right;
proof of times_is_1 =
by property morph_times, morph_one, morph_injective, morph_surjective, A!times_eq_right;
end;;
species NatLeTransfer (A is NatLeThm) =
inherit NatLeMorph(A), NatLeThm;
proof of le_zero =
by property morph_le, morph_le_rev, morph_zero, morph_injective, morph_surjective, A!le_zero;
proof of le_succ =
by property morph_le, morph_le_rev, morph_succ, morph_injective, morph_surjective, A!le_succ;
proof of zero_le =
by property morph_le, morph_le_rev, morph_zero, morph_injective, morph_surjective, A!zero_le;
proof of le_n_succ_n =
by property morph_le, morph_le_rev, morph_succ, morph_injective, morph_surjective, A!le_n_succ_n;
proof of le_succ_succ =
by property morph_le, morph_le_rev, morph_succ, morph_injective, morph_surjective, A!le_succ_succ;
proof of le_refl =
by property morph_le, morph_le_rev, morph_injective, morph_surjective, A!le_refl;
proof of le_refl_eq =
by property morph_le, morph_le_rev, morph_injective, morph_surjective, A!le_refl_eq;
proof of le_trans =
by property morph_le, morph_le_rev, morph_injective, morph_surjective, A!le_trans;
proof of le_antisym =
by property morph_le, morph_le_rev, morph_injective, morph_surjective, A!le_antisym;
proof of le_total =
by property morph_le, morph_le_rev, morph_injective, morph_surjective, A!le_total;
(* le_predmax is missing because it is not first-order. *)
end;;
species NatPlusLeTransfer (A is NatPlusLe) =
inherit NatPlusMorph(A), NatLeMorph(A), NatPlusLe;
proof of le_n_plus_m_n =
by property morph_le, morph_le_rev, morph_plus, morph_injective, morph_surjective, A!le_n_plus_m_n;
proof of le_m_plus_m_n =
by property morph_le, morph_le_rev, morph_plus, morph_injective, morph_surjective, A!le_m_plus_m_n;
proof of le_plus_plus_left =
by property morph_le, morph_le_rev, morph_plus, morph_injective, morph_surjective, A!le_plus_plus_left;
proof of le_plus_plus_right =
by property morph_le, morph_le_rev, morph_plus, morph_injective, morph_surjective, A!le_plus_plus_right;
proof of plus_le_left =
by property morph_le, morph_le_rev, morph_plus, morph_zero, morph_injective, morph_surjective, A!plus_le_left;
proof of plus_le_right =
by property morph_le, morph_le_rev, morph_plus, morph_zero, morph_injective, morph_surjective, A!plus_le_right;
proof of plus_increases =
by property morph_le, morph_le_rev, morph_plus, morph_injective, morph_surjective, A!plus_increases;
end;;
species NatTimesLeTransfer (A is NatTimesLe) =
inherit NatTimesMorph(A), NatLeMorph(A), NatTimesLe;
proof of le_times_times_left =
by property morph_le, morph_le_rev, morph_times, morph_zero, morph_injective, morph_surjective, A!le_times_times_left;
proof of le_times_times_right =
by property morph_le, morph_le_rev, morph_times, morph_zero, morph_injective, morph_surjective, A!le_times_times_right;
proof of le_square =
by property morph_le, morph_le_rev, morph_times, morph_injective, morph_surjective, A!le_square;
proof of times_le_is_zero =
by property morph_le, morph_le_rev, morph_times, morph_zero, morph_injective, morph_surjective, A!times_le_is_zero;
proof of times_increases =
by property morph_le, morph_le_rev, morph_times, morph_injective, morph_surjective, A!times_increases;
end;;
species NatLtTransfer (A is NatLtThm) =
inherit NatLtMorph(A), NatLtThm;
proof of zero_lt =
by property morph_lt, morph_lt_rev, morph_zero, morph_injective, morph_surjective, A!zero_lt;
proof of succ_lt =
by property morph_lt, morph_lt_rev, morph_succ, morph_injective, morph_surjective, A!succ_lt;
proof of zero_lt_succ =
by property morph_lt, morph_lt_rev, morph_zero, morph_succ, morph_injective, morph_surjective, A!zero_lt_succ;
proof of lt_irrefl =
by property morph_lt, morph_lt_rev, morph_injective, morph_surjective, A!lt_irrefl;
proof of lt_irrefl_diff =
by property morph_lt, morph_lt_rev, morph_injective, morph_surjective, A!lt_irrefl_diff;
proof of n_lt_succ_n =
by property morph_lt, morph_lt_rev, morph_succ, morph_injective, morph_surjective, A!n_lt_succ_n;
proof of lt_trans =
by property morph_lt, morph_lt_rev, morph_injective, morph_surjective, A!lt_trans;
proof of lt_acyclic =
by property morph_lt, morph_lt_rev, morph_injective, morph_surjective, A!lt_acyclic;
proof of lt_trichotomy =
by property morph_lt, morph_lt_rev, morph_injective, morph_surjective, A!lt_trichotomy;
(* strong_induction and lt_predmin are missing because they are not first-order. *)
end;;
species NatLeLtTransfer (A is NatLeLt) =
inherit NatLeMorph(A), NatLtMorph(A), NatLeLt;
proof of not_le_lt =
by property morph_le, morph_le_rev, morph_lt, morph_lt_rev, morph_injective, morph_surjective, A!not_le_lt;
proof of not_lt_le =
by property morph_le, morph_le_rev, morph_lt, morph_lt_rev, morph_injective, morph_surjective, A!not_lt_le;
proof of lt_le_diff =
by property morph_le, morph_le_rev, morph_lt, morph_lt_rev, morph_injective, morph_surjective, A!lt_le_diff;
proof of lt_le =
by property morph_le, morph_le_rev, morph_lt, morph_lt_rev, morph_injective, morph_surjective, A!lt_le;
proof of le_lt_lt =
by property morph_le, morph_le_rev, morph_lt, morph_lt_rev, morph_injective, morph_surjective, A!le_lt_lt;
proof of lt_le_lt =
by property morph_le, morph_le_rev, morph_lt, morph_lt_rev, morph_injective, morph_surjective, A!lt_le_lt;
proof of lt_succ_le =
by property morph_le, morph_le_rev, morph_lt, morph_lt_rev, morph_succ, morph_injective, morph_surjective, A!lt_succ_le;
proof of lt_or_le =
by property morph_le, morph_le_rev, morph_lt, morph_lt_rev, morph_injective, morph_surjective, A!lt_or_le;
proof of le_or_lt =
by property morph_le, morph_le_rev, morph_lt, morph_lt_rev, morph_injective, morph_surjective, A!le_or_lt;
proof of not_lt_and_le =
by property morph_le, morph_le_rev, morph_lt, morph_lt_rev, morph_injective, morph_surjective, A!not_lt_and_le;
proof of not_le_and_lt =
by property morph_le, morph_le_rev, morph_lt, morph_lt_rev, morph_injective, morph_surjective, A!not_le_and_lt;
proof of lt_succ_is_le =
by property morph_le, morph_le_rev, morph_lt, morph_lt_rev, morph_succ, morph_injective, morph_surjective, A!lt_succ_is_le;
proof of le_succ_is_lt =
by property morph_le, morph_le_rev, morph_lt, morph_lt_rev, morph_succ, morph_injective, morph_surjective, A!le_succ_is_lt;
proof of le_lt_eq =
by property morph_le, morph_le_rev, morph_lt, morph_lt_rev, morph_injective, morph_surjective, A!le_lt_eq;
end;;
species NatPlusLtTransfer (A is NatPlusLt) =
inherit NatPlusMorph(A), NatLtMorph(A), NatPlusLt;
proof of not_plus_lt_left =
by property morph_lt, morph_lt_rev, morph_plus, morph_injective, morph_surjective, A!not_plus_lt_left;
proof of not_plus_lt_right =
by property morph_lt, morph_lt_rev, morph_plus, morph_injective, morph_surjective, A!not_plus_lt_right;
proof of lt_plus_left =
by property morph_lt, morph_lt_rev, morph_plus, morph_zero, morph_injective, morph_surjective, A!lt_plus_left;
proof of lt_plus_right =
by property morph_lt, morph_lt_rev, morph_plus, morph_zero, morph_injective, morph_surjective, A!lt_plus_right;
proof of lt_plus_plus_left =
by property morph_lt, morph_lt_rev, morph_plus, morph_injective, morph_surjective, A!lt_plus_plus_left;
proof of lt_plus_plus_right =
by property morph_lt, morph_lt_rev, morph_plus, morph_injective, morph_surjective, A!lt_plus_plus_right;
proof of lt_exists =
by property morph_lt, morph_lt_rev, morph_plus, morph_succ, morph_injective, morph_surjective, A!lt_exists;
proof of plus_strictly_increases =
by property morph_lt, morph_lt_rev, morph_plus, morph_injective, morph_surjective, A!plus_strictly_increases;
end;;
species NatPlusLeLtTransfer (A is NatPlusLeLt) =
inherit NatPlusMorph(A), NatLeMorph(A), NatLtMorph(A), NatPlusLeLt;
proof of plus_plus_lt_le =
by property morph_le, morph_le_rev, morph_lt, morph_lt_rev, morph_plus, morph_injective, morph_surjective, A!plus_plus_lt_le;
proof of plus_plus_le_lt =
by property morph_le, morph_le_rev, morph_lt, morph_lt_rev, morph_plus, morph_injective, morph_surjective, A!plus_plus_le_lt;
end;;
species NatTimesLtTransfer (A is NatTimesLt) =
inherit NatTimesMorph(A), NatLtMorph(A), NatTimesLt;
proof of lt_times_times_left =
by property morph_lt, morph_lt_rev, morph_times, morph_zero, morph_injective, morph_surjective, A!lt_times_times_left;
proof of lt_times_times_right =
by property morph_lt, morph_lt_rev, morph_times, morph_zero, morph_injective, morph_surjective, A!lt_times_times_right;
proof of zero_lt_times =
by property morph_lt, morph_lt_rev, morph_times, morph_zero, morph_injective, morph_surjective, A!zero_lt_times;
proof of pos_times_strictly_increases =
by property morph_lt, morph_lt_rev, morph_times, morph_zero, morph_injective, morph_surjective, A!pos_times_strictly_increases;
proof of times_strictly_increases =
by property morph_lt, morph_lt_rev, morph_times, morph_injective, morph_surjective, A!times_strictly_increases;
end;;
species NatFullTransfer (A is NatFullThm) =
inherit NatPlusTransfer(A), NatPlusOneTransfer(A), NatTimesTransfer(A),
NatPlusTimesTransfer(A), NatTimesOneTransfer(A), NatLeTransfer(A),
NatPlusLeTransfer(A), NatTimesLeTransfer(A), NatLtTransfer(A),
NatLeLtTransfer(A), NatPlusLtTransfer(A), NatPlusLeLtTransfer(A),
NatTimesLtTransfer(A), NatFullThm;
end;;
include ../../.config_vars
include ../../Makefile.rules
all: basics.dko zen.dko focal.dko
basics.dko: dk_builtins.dko
cc.dko: hol.dko
hol.dko:
dk_bool.dko:
dk_logic.dko: cc.dko dk_bool.dko
focal.dko: dk_logic.dko dk_bool.dko zen.dko
basics.sk: basics.fcl dk_logic.dko dk_bool.dko
$(FOCALIZEC) $(FOCALIZEC_OPT) -no-stdlib-path $<
FCL_FILES=$(wildcard *.fcl)
DK_FILES