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

[HOL instantiation] fix Zenon proofs

parent 56216cf2
......@@ -143,15 +143,29 @@ species HolNatPlus =
{* 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_regular_right : all p m n : Self, plus(m, p) = plus(n, p) <-> m = n
proof = dedukti proof definition of plus
{* HolNaturals.thm_158. *};
(* (update-thm-number-on-previous-line "∀p m n, ((m + p) = (n + p)) <=> (m = n)") *)
proof of plus_regular_right =
<1>1 assume m n p : Self,
prove plus(m, p) = plus(n, p) <-> m = n
dedukti proof property hol_plus_regular_right {* abst_hol_plus_regular_right p m n *}
<1>f conclude;
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;
proof of plus_assoc =
<1>1 assume m n p : Self,
prove plus(plus(m, n), p) = plus(m, plus(n, p))
<2>1 prove plus(m, plus(n, p)) = plus(plus(m, n), p)
dedukti proof property hol_plus_assoc {* abst_hol_plus_assoc m n p *}
<2>f conclude
<1>f conclude;
end;;
......@@ -183,7 +197,14 @@ species HolNatTimes =
{* 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_regular_left =
<1>1 assume m n p : Self,
prove times(m, n) = times (m, p) <-> (n = p \/ m = zero)
<2>1 prove times(m, n) = times (m, p) <-> (m = zero \/ n = p)
dedukti proof property hol_times_regular_left
{* abst_hol_times_regular_left m n p *}
<2>f conclude
<1>f conclude;
proof of times_is_zero =
dedukti proof definition of zero, times
......@@ -205,14 +226,31 @@ species HolNatTimes =
<2>f conclude
<1>f conclude;
proof of times_succ = by property hol_succ_times, plus_commutes, times_commutes;
theorem hol_times_succ : all m n : Self, times(m, succ(n)) = plus(m, times(m, n))
proof = dedukti proof definition of succ, plus, times
{* HolNaturals.thm_114. *};
(* (update-thm-number-on-previous-line "∀m n, (m * (suc n)) = (m + (m * n))") *)
proof of times_succ =
<1>1 assume m n : Self,
prove times(m, succ(n)) = plus(times(m, n), m)
<2>1 prove times(m, succ(n)) = plus(m, times(m, n))
by property hol_times_succ
<2>f qed by step <2>1 property plus_commutes
<1>f conclude;
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_assoc =
<1>1 assume m n p : Self,
prove times(times(m, n), p) = times(m, times(n, p))
<2>1 prove times(m, times(n, p)) = times(times(m, n), p)
dedukti proof property hol_times_assoc {* abst_hol_times_assoc m n p *}
<2>f conclude
<1>f conclude;
proof of times_commutes =
dedukti proof definition of times
......@@ -272,7 +310,7 @@ species HolNatLe =
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
theorem hol_le_antisym : all m n : 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)") *)
......
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