Import all the OpenTheory lemmas

example/arith/natural_hol.fcl

@@ -97,16 +97,62 @@ species HolNatPlus =
     {* HolNaturals.thm_144. *};
     (* (update-thm-number-on-previous-line "∀n, (zero + n) = n") *)
 
+  proof of plus_zero =
+  dedukti proof
+    definition of plus, zero
+    {* HolNaturals.thm_115. *};
+    (* (update-thm-number-on-previous-line "∀m, (m + zero) = m") *)
+
   proof of succ_plus =
   dedukti proof
     definition of plus, succ
     {* HolNaturals.thm_147. *};
     (* (update-thm-number-on-previous-line "∀m n, ((suc m) + n) = (suc (m + n))") *)
 
+  proof of plus_succ =
+  dedukti proof
+    definition of plus, succ
+    {* HolNaturals.thm_116. *};
+    (* (update-thm-number-on-previous-line "∀m n, (m + (suc n)) = (suc (m + n))") *)
+
+  proof of plus_is_zero =
+  dedukti proof
+    definition of plus, zero
+    {* HolNaturals.thm_226. *};
+    (* (update-thm-number-on-previous-line "∀m n, ((m + n) = zero) <=> ((m = zero) /\\ (n = zero))") *)
+
+  proof of plus_eq_right =
+  dedukti proof
+    definition of plus, zero
+    {* HolNaturals.thm_235. *};
+    (* (update-thm-number-on-previous-line "∀m n, ((m + n) = n) <=> (m = zero)") *)
+
+  proof of plus_eq_left =
+  dedukti proof
+    definition of plus, zero
+    {* HolNaturals.thm_177. *};
+    (* (update-thm-number-on-previous-line "∀m n, ((m + n) = m) <=> (n = zero)") *)
+
   proof of plus_commutes =
   dedukti proof definition of plus
     {* HolNaturals.thm_129. *};
     (* (update-thm-number-on-previous-line "∀m n, (m + n) = (n + m)") *)
+
+  proof of plus_regular_left =
+  dedukti proof definition of plus
+    {* HolNaturals.thm_200. *};
+    (* (update-thm-number-on-previous-line "∀m n p, ((m + n) = (m + p)) <=> (n = p)") *)
+
+  proof of plus_regular_right = by property plus_commutes, plus_regular_left;
+
+  theorem hol_plus_assoc : all m n p : Self, plus(m, plus(n, p)) = plus(plus(m, n), p)
+  proof = dedukti proof definition of plus
+    {* HolNaturals.thm_130. *};
+    (* (update-thm-number-on-previous-line "∀m n p, (m + (n + p)) = ((m + n) + p)") *)
+
+  proof of plus_assoc = by property hol_plus_assoc;
+
+
 end;;
 
 species HolNatTimes =
@@ -122,6 +168,28 @@ species HolNatTimes =
     {* HolNaturals.thm_117. *};
     (* (update-thm-number-on-previous-line "∀n, (zero * n) = zero") *)
 
+  proof of times_zero =
+  dedukti proof definition of zero, times
+    {* HolNaturals.thm_113. *};
+    (* (update-thm-number-on-previous-line "∀m, (m * zero) = zero") *)
+
+  proof of times_regular_right =
+  dedukti proof definition of zero, times
+    {* HolNaturals.thm_141. *};
+    (* (update-thm-number-on-previous-line "∀m n p, ((m * p) = (n * p)) <=> ((m = n) \\/ (p = zero))") *)
+
+  theorem hol_times_regular_left : all m n p : Self, times(m, n) = times (m, p) <-> (m = zero \/ n = p)
+  proof = dedukti proof definition of zero, times
+    {* HolNaturals.thm_193. *};
+    (* (update-thm-number-on-previous-line "∀m n p, ((m * n) = (m * p)) <=> ((m = zero) \\/ (n = p))") *)
+
+  proof of times_regular_left = by property hol_times_regular_left;
+
+  proof of times_is_zero =
+  dedukti proof definition of zero, times
+    {* HolNaturals.thm_163. *};
+    (* (update-thm-number-on-previous-line "∀m n, ((m * n) = zero) <=> ((m = zero) \\/ (n = zero))") *)
+
   theorem hol_succ_times : all m n : Self, times(succ(m), n) = plus(times(m, n), n)
   proof = dedukti proof definition of succ, plus, times
   {* HolNaturals.thm_157. *};
@@ -137,6 +205,15 @@ species HolNatTimes =
        <2>f conclude
   <1>f conclude;
 
+  proof of times_succ = by property hol_succ_times, plus_commutes, times_commutes;
+
+  theorem hol_times_assoc : all m n p : Self, times(m, times(n, p)) = times(times(m, n), p)
+  proof = dedukti proof definition of times
+    {* HolNaturals.thm_138. *};
+    (* (update-thm-number-on-previous-line "∀m n p, (m * (n * p)) = ((m * n) * p)") *)
+
+  proof of times_assoc = by property hol_times_assoc;
+
   proof of times_commutes =
   dedukti proof definition of times
     {* HolNaturals.thm_143. *};
@@ -161,6 +238,46 @@ species HolNatLe =
   proof of zero_le = dedukti proof definition of le, zero
     {* HolNaturals.thm_1348. *};
     (* (update-thm-number-on-previous-line "∀n, zero <= n") *)
+
+  proof of le_zero = dedukti proof definition of le, zero
+    {* HolNaturals.thm_101. *};
+    (* (update-thm-number-on-previous-line "∀m, (m <= zero) <=> (m = zero)") *)
+
+  proof of le_succ_succ = dedukti proof definition of le, succ
+    {* HolNaturals.thm_4766. *};
+    (* (update-thm-number-on-previous-line "∀m n, ((suc m) <= (suc n)) <=> (m <= n)") *)
+
+  proof of le_succ = dedukti proof definition of le, succ
+    {* HolNaturals.thm_102. *};
+    (* (update-thm-number-on-previous-line "∀m n, (m <= (suc n)) <=> ((m = (suc n)) \\/ (m <= n))") *)
+
+  proof of le_n_succ_n = dedukti proof definition of le, succ
+    {* HolNaturals.thm_2170. *};
+    (* (update-thm-number-on-previous-line "∀n, n <= (suc n)") *)
+
+  theorem hol_le_trans : all m n p : Self, (le(m, n) /\ le(n, p)) -> le(m, p)
+  proof = dedukti proof definition of le
+    {* HolNaturals.thm_217. *};
+    (* (update-thm-number-on-previous-line "∀m n p, ((m <= n) /\\ (n <= p)) ==> (m <= p)") *)
+
+  proof of le_trans = by property hol_le_trans;
+
+  proof of le_total = dedukti proof definition of le
+    {* HolNaturals.thm_237. *};
+    (* (update-thm-number-on-previous-line "∀m n, (m <= n) \\/ (n <= m)") *)
+
+  proof of le_refl = dedukti proof definition of le
+    {* HolNaturals.thm_216. *};
+    (* (update-thm-number-on-previous-line "∀n, n <= n") *)
+
+  proof of le_refl_eq = by property le_refl;
+
+  theorem hol_le_antisym : all m n p : Self, (le(m, n) /\ le(n, m)) -> m = n
+  proof = dedukti proof definition of le
+    {* HolNaturals.thm_145. *};
+    (* (update-thm-number-on-previous-line "∀m n, ((m <= n) /\\ (n <= m)) <=> (m = n)") *)
+
+  proof of le_antisym = by property hol_le_antisym;
 end;;
 
 species HolNatLt =
@@ -171,6 +288,22 @@ species HolNatLt =
     | dedukti -> {* HolNaturals.Number_2ENatural_2E_3C m n *}
     | coq -> {* *};
 
+  proof of zero_lt_succ = dedukti proof definition of lt, zero, succ
+    {* HolNaturals.thm_2118. *};
+    (* (update-thm-number-on-previous-line "∀n, zero < (suc n)") *)
+
+  proof of zero_lt = dedukti proof definition of lt, zero
+    {* HolNaturals.thm_135. *};
+    (* (update-thm-number-on-previous-line "∀n, (zero < n) <=> (~ (n = zero))") *)
+
+  proof of succ_lt = dedukti proof definition of lt, succ
+    {* HolNaturals.thm_183. *};
+    (* (update-thm-number-on-previous-line "∀m n, ((suc m) < (suc n)) <=> (m < n)") *)
+
+  proof of succ_lt_succ = dedukti proof definition of lt, succ
+    {* HolNaturals.thm_183. *};
+    (* (update-thm-number-on-previous-line "∀m n, ((suc m) < (suc n)) <=> (m < n)") *)
+
   proof of le_succ_is_lt = dedukti proof definition of le, lt, succ
     {* HolNaturals.thm_189. *};
     (* (update-thm-number-on-previous-line "∀m n, ((suc m) <= n) <=> (m < n)") *)
@@ -189,6 +322,85 @@ species HolNatLt =
     {* HolNaturals.thm_201. *};
     (* (update-thm-number-on-previous-line "∀n, ~ (n < n)") *)
 
+  proof of n_lt_succ_n = dedukti proof definition of lt, succ
+    {* HolNaturals.thm_205. *};
+    (* (update-thm-number-on-previous-line "∀n, n < (suc n)") *)
+
+  proof of lt_succ_le = dedukti proof definition of le, lt, succ
+    {* HolNaturals.thm_214. *};
+    (* (update-thm-number-on-previous-line "∀m n, (m < (suc n)) <=> (m <= n)") *)
+
+  proof of lt_succ_is_le = dedukti proof definition of le, lt, succ
+    {* HolNaturals.thm_214. *};
+    (* (update-thm-number-on-previous-line "∀m n, (m < (suc n)) <=> (m <= n)") *)
+
+  proof of lt_succ = dedukti proof definition of lt, succ
+    {* HolNaturals.thm_105. *};
+    (* (update-thm-number-on-previous-line "∀m n, (m < (suc n)) <=> ((m = n) \\/ (m < n))") *)
+
+  proof of not_lt_le = dedukti proof definition of le, lt
+    {* HolNaturals.thm_215. *};
+    (* (update-thm-number-on-previous-line "∀m n, (~ (m < n)) <=> (n <= m)") *)
+
+  proof of not_le_lt = dedukti proof definition of le, lt
+    {* HolNaturals.thm_128. *};
+    (* (update-thm-number-on-previous-line "∀m n, (~ (m <= n)) <=> (n < m)") *)
+
+  proof of not_lt_and_le = dedukti proof definition of le, lt
+    {* HolNaturals.thm_4319. *};
+    (* (update-thm-number-on-previous-line "∀m n, ~ ((m < n) /\\ (n <= m))") *)
+
+  proof of not_le_and_lt = dedukti proof definition of le, lt
+    {* HolNaturals.thm_4311. *};
+    (* (update-thm-number-on-previous-line "∀m n, ~ ((m <= n) /\\ (n < m))") *)
+
+  proof of lt_trichotomy = dedukti proof definition of lt
+    {* HolNaturals.thm_6027. *};
+    (* (update-thm-number-on-previous-line "∀m n, (m < n) \\/ ((n < m) \\/ (m = n))") *)
+
+  theorem hol_lt_trans : all m n p : Self, (lt(m, n) /\ lt(n, p)) -> lt(m, p)
+  proof = dedukti proof definition of lt
+    {* HolNaturals.thm_172. *};
+    (* (update-thm-number-on-previous-line "∀m n p, ((m < n) /\\ (n < p)) ==> (m < p)") *)
+
+  proof of lt_trans = by property hol_lt_trans;
+
+  proof of le_or_lt = dedukti proof definition of le, lt
+    {* HolNaturals.thm_4098. *};
+    (* (update-thm-number-on-previous-line "∀m n, (m <= n) \\/ (n < m)") *)
+
+  proof of lt_or_le = dedukti proof definition of le, lt
+    {* HolNaturals.thm_4101. *};
+    (* (update-thm-number-on-previous-line "∀m n, (m < n) \\/ (n <= m)") *)
+
+  theorem hol_lt_le_lt : all m n p : Self, (lt(m, n) /\ le(n, p)) -> lt(m, p)
+  proof = dedukti proof definition of le, lt
+    {* HolNaturals.thm_211. *};
+    (* (update-thm-number-on-previous-line "∀m n p, ((m < n) /\\ (n <= p)) ==> (m < p)") *)
+
+  theorem hol_le_lt_lt : all m n p : Self, (le(m, n) /\ lt(n, p)) -> lt(m, p)
+  proof = dedukti proof definition of le, lt
+    {* HolNaturals.thm_207. *};
+    (* (update-thm-number-on-previous-line "∀m n p, ((m <= n) /\\ (n < p)) ==> (m < p)") *)
+
+  proof of lt_le_lt = by property hol_lt_le_lt;
+  proof of le_lt_lt = by property hol_le_lt_lt;
+
+  proof of lt_le_diff = dedukti proof definition of le, lt
+    {* HolNaturals.thm_231. *};
+    (* (update-thm-number-on-previous-line "∀m n, (m < n) <=> ((m <= n) /\\ (~ (m = n)))") *)
+
+  proof of lt_le = dedukti proof definition of le, lt
+    {* HolNaturals.thm_195. *};
+    (* (update-thm-number-on-previous-line "∀m n, (m < n) ==> (m <= n)") *)
+
+  proof of lt_irrefl_diff = dedukti proof definition of lt
+    {* HolNaturals.thm_4327. *};
+    (* (update-thm-number-on-previous-line "∀m n, (m < n) ==> (~ (m = n))") *)
+
+  proof of lt_acyclic = dedukti proof definition of lt
+    {* HolNaturals.thm_4281. *};
+    (* (update-thm-number-on-previous-line "∀m n, ~ ((m < n) /\\ (n < m))") *)
 end;;
 
 species HolNatDiv =
@@ -260,6 +472,12 @@ end;;
 species HolNatPrime =
   inherit NatPrime, HolNatOneLt, HolNatDiv, HolNatLt, NatPrimeDiv;
 
+  logical let sd (m, n) = lt(one, m) /\ lt(m, n) /\ divides(m, n);
+  proof of sd_divides = by definition of sd;
+  proof of sd_lt = by definition of sd;
+  proof of sd_1 = by definition of sd;
+  proof of sd_intro = by definition of sd;
+
   logical let prime (p : hnat) = internal bool
   external
   | dedukti -> {* HolNaturals.Number_2ENatural_2Eprime p *}
@@ -414,3 +632,7 @@ species HolNatPrime =
    {* (m : cc.eT abst_T => n : cc.eT abst_T =>
        dk_logic.eqv_refl (abst_primediv_pred m n)). *};
 end;;
+
+collection HolNatPrimeDivColl =
+  implement HolNatPrime;
+end;;

lib/arith/theorems/natthms.fcl

@@ -67,7 +67,6 @@ species NatLeThm =
   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 =
@@ -110,13 +109,6 @@ species NatLtThm =
   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 =