Commit 2bdca923 authored by Raphael Cauderlier's avatar Raphael Cauderlier
Browse files

Add an Emacs Lisp script automating the search for Holide theorem numbers

parent 8f281d7b
......@@ -2,6 +2,20 @@ open "basics";;
open "naturals";;
open "natural_instantiation";;
(* This file is very sensible to the numbering of theorems performed
by Holide.
If the numbering changes for whatever reason, we can use the Emacs
Lisp script update-thm-numbers.el.
In Emacs, this can be done by hitting C-x C-e with point at the end
of the following expression:
(let ((load-path '(".")))
(when (load "update-thm-numbers") (update-all-thm-numbers)))
*)
(* We instantiate the species hierarchy defined in nat.fcl
using the definitions of OpenTheory.
We proceed species by species. *)
......@@ -24,9 +38,8 @@ 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 {* HolNaturals.thm_1238. *};;
(* The statement in HolNaturals.txt:
((p zero) /\ (∀n, (p n) ==> (p (suc n)))) ==> (∀n, p n)
proof = dedukti proof {* HolNaturals.thm_1239. *};;
(* (update-thm-number-on-previous-line "((p zero) /\\ (∀n, (p n) ==> (p (suc n)))) ==> (∀n, p n)")
*)
species HolNatDecl =
......@@ -55,7 +68,7 @@ species HolNatDecl =
prove ~ (succ(m) = zero)
dedukti proof definition of zero, succ
{* HolNaturals.thm_106 m *}
(* ∀n, ~ ((suc n) = zero) *)
(* (update-thm-number-on-previous-line "∀n, ~ ((suc n) = zero)") *)
<1>f conclude;
proof of succ_inj =
......@@ -63,7 +76,7 @@ species HolNatDecl =
prove (succ(m) = succ(n)) <-> (m = n)
dedukti proof definition of succ
{* HolNaturals.thm_107 m n *}
(* ∀m n, ((suc m) = (suc n)) <=> (m = n) *)
(* (update-thm-number-on-previous-line "∀m n, ((suc m) = (suc n)) <=> (m = n)") *)
<1>f conclude;
end;;
......@@ -93,7 +106,7 @@ theorem power_zero : all f : 'a -> 'a,
proof =
dedukti proof
{* HolNaturals.thm_109. *};;
(* ∀f, (f ^ zero) = id *)
(* (update-thm-number-on-previous-line "∀f, (f ^ zero) = id") *)
species HolNatIter =
inherit NatIter, HolNatDecl;
......@@ -120,7 +133,7 @@ species HolNatIter =
assume n : Self,
prove iter(f, z, succ(n)) = f @ iter(f, z, n)
dedukti proof definition of iter, succ {* HolNaturals.thm_6414 abst_T f n z *}
(* ∀f n x, (f ^ (suc n) x) = (f (f ^ n x)) *)
(* (update-thm-number-on-previous-line "∀f n x, (f ^ (suc n) x) = (f (f ^ n x))") *)
<1>f conclude;
end;;
......@@ -142,13 +155,13 @@ species HolPlus =
dedukti proof
definition of plus, zero
{* HolNaturals.thm_144. *};
(* ∀n, (zero + n) = n *)
(* (update-thm-number-on-previous-line "∀n, (zero + n) = n") *)
proof of succ_plus =
dedukti proof
definition of plus, succ
{* HolNaturals.thm_147. *};
(* ∀m n, ((suc m) + n) = (suc (m + n)) *)
(* (update-thm-number-on-previous-line "∀m n, ((suc m) + n) = (suc (m + n))") *)
end;;
collection HolPlusColl = implement HolPlus; end;;
......@@ -162,21 +175,21 @@ let hol_times (p : hnat, q : hnat) : hnat =
theorem hol_times_zero : all n : hnat, hol_times(hzero, n) = hzero
proof = dedukti proof {* HolNaturals.thm_117. *};;
(* ∀n, (zero * n) = zero *)
(* (update-thm-number-on-previous-line "∀n, (zero * n) = zero") *)
theorem hol_times_succ : all m n : hnat, hol_times(hsucc(m), n) = hol_plus(hol_times(m, n), n)
proof = dedukti proof {* HolNaturals.thm_157. *};;
(* ∀m n, ((suc m) * n) = ((m * n) + n) *)
(* (update-thm-number-on-previous-line "∀m n, ((suc m) * n) = ((m * n) + n)") *)
theorem hol_times_commute : all m n : hnat,
hol_times (m, n) = hol_times (n, m)
proof = dedukti proof {* HolNaturals.thm_143. *};;
(* ∀m n, (m * n) = (n * m) *)
(* (update-thm-number-on-previous-line "∀m n, (m * n) = (n * m)") *)
theorem hol_plus_commute : all m n : hnat,
hol_plus (m, n) = hol_plus (n, m)
proof = dedukti proof {* HolNaturals.thm_129. *};;
(* ∀m n, (m + n) = (n + m) *)
(* (update-thm-number-on-previous-line "∀m n, (m + n) = (n + m)") *)
species HolTimes =
inherit NatTimes, HolPlus;
......@@ -204,7 +217,7 @@ let hol_le (m : hnat, n : hnat) =
theorem hol_le_plus : all m n : hnat, hol_le(m, n) <-> ex d : hnat, n = hol_plus(m, d)
proof = dedukti proof {* HolNaturals.thm_132. *};;
(* ∀m n, (m <= n) <=> (∃d, n = (m + d)) *)
(* (update-thm-number-on-previous-line "∀m n, (m <= n) <=> (∃d, n = (m + d))") *)
species HolLe =
inherit NatLe, HolPlus;
......@@ -224,7 +237,7 @@ let hol_divides (p : hnat, q : hnat) : bool =
theorem hol_divides_times1 : all m n : hnat,
hol_divides (m, n) <-> (ex p : hnat, hol_times(p, m) = n)
proof = dedukti proof {* HolNaturals.thm_241. *};;
(* ∀a b, (divides a b) <=> (∃c, (c * a) = b) *)
(* (update-thm-number-on-previous-line "∀a b, (divides a b) <=> (∃c, (c * a) = b)") *)
theorem hol_divides_times2 : all m n : hnat,
hol_divides (m, n) <-> (ex p : hnat, hol_times(m, p) = n)
......@@ -239,26 +252,26 @@ let hol_lt(m : hnat, n : hnat) =
theorem hol_lt_le : all m n : hnat, hol_le(hsucc(m), n) <-> hol_lt(m, n)
proof = dedukti proof {* HolNaturals.thm_189. *};;
(* ∀m n, ((suc m) <= n) <=> (m < n) *)
(* (update-thm-number-on-previous-line "∀m n, ((suc m) <= n) <=> (m < n)") *)
theorem hol_lt_zero : all m : hnat, ~(hol_lt(m, hzero))
proof = dedukti proof {* HolNaturals.thm_104. *};;
(* ∀m, ~ (m < zero) *)
(* (update-thm-number-on-previous-line "∀m, ~ (m < zero)") *)
theorem hol_le_zero : all n : hnat, hol_le(hzero, n)
proof = dedukti proof {* HolNaturals.thm_1348. *};;
(* ∀n, zero <= n *)
(* (update-thm-number-on-previous-line "∀n, zero <= n") *)
theorem hol_le_lt : all m n : hnat, hol_le(m, n) <-> (hol_lt(m, n) \/ m = n)
proof = dedukti proof {* HolNaturals.thm_2162. *};;
(* ∀m n, (m <= n) <=> ((m < n) \/ (m = n)) *)
(* (update-thm-number-on-previous-line "∀m n, (m <= n) <=> ((m < n) \\/ (m = n))") *)
theorem hol_lt_one : all m : hnat, (m = hzero \/ (m = hsucc(hzero) \/ hol_lt(hsucc(hzero), m)))
proof = by property hol_le_zero, hol_le_lt, hol_lt_le;;
theorem hol_lt_irrefl : all n : hnat, ~(hol_lt(n, n))
proof = dedukti proof {* HolNaturals.thm_201. *};;
(* ∀n, ~ (n < n) *)
(* (update-thm-number-on-previous-line "∀n, ~ (n < n)") *)
species HolLt =
inherit NatLt, HolLe;
......@@ -271,7 +284,7 @@ collection HolLtColl = implement HolLt; end;;
theorem hol_divides_le : all m n : hnat, (~(n = hzero) /\ hol_divides(m, n)) -> hol_le(m, n)
proof = dedukti proof {* HolNaturals.thm_232. *};;
(* ∀a b, ((~ (b = zero)) /\ (divides a b)) ==> (a <= b) *)
(* (update-thm-number-on-previous-line "∀a b, ((~ (b = zero)) /\\ (divides a b)) ==> (a <= b)") *)
species HolDiv =
inherit NatDivides, HolTimes, HolLt;
......@@ -320,7 +333,7 @@ let b0 (n : hnat) =
theorem b0_zero : b0(hzero) = hzero
proof = dedukti proof {* HolNaturals.thm_112. *};;
(* (bit0 zero) = zero *)
(* (update-thm-number-on-previous-line "(bit0 zero) = zero") *)
(* Adding a one in binary (n => 2*n + 1) *)
let b1 (n : hnat) = hsucc (b0(n));;
......@@ -337,15 +350,15 @@ theorem hol_prime_def : all p : hnat,
((~(p = hol_one)) /\
all n : hnat, hol_divides(n, p) -> (n = hol_one \/ n = p))
proof = dedukti proof {* HolNaturals.thm_227. *};;
(* ∀p, (prime p) <=> ((~ (p = (bit1 zero))) /\ (∀n, (divides n p) ==> ((n = (bit1 zero)) \/ (n = p)))) *)
(* (update-thm-number-on-previous-line "∀p, (prime p) <=> ((~ (p = (bit1 zero))) /\\ (∀n, (divides n p) ==> ((n = (bit1 zero)) \\/ (n = p))))") *)
theorem hol_prime_zero : ~(hol_prime(hzero))
proof = dedukti proof {* HolNaturals.thm_14422. *};;
(* ~ (prime zero) *)
(* (update-thm-number-on-previous-line "~ (prime zero)") *)
theorem hol_prime_one : ~(hol_prime(hol_one))
proof = dedukti proof {* HolNaturals.thm_14428. *};;
(* ~ (prime (bit1 zero)) *)
(* (update-thm-number-on-previous-line "~ (prime (bit1 zero))") *)
species HolPrime =
inherit NatPrime, HolDiv, HolLt;
......@@ -484,7 +497,7 @@ theorem hol_prime_divisor :
all n : hnat,
(~(n = hol_one)) -> ex p : hnat, hol_prime(p) /\ hol_divides(p, n)
proof = dedukti proof {* HolNaturals.thm_14683. *};;
(* ∀n, (~ (n = (bit1 zero))) ==> (∃p, (prime p) /\ (divides p n)) *)
(* (update-thm-number-on-previous-line "∀n, (~ (n = (bit1 zero))) ==> (∃p, (prime p) /\\ (divides p n))") *)
(* species HolPrimeDiv = *)
(* inherit NatPrimeDiv, HolPrime; *)
......
(defun find-thm-number-in-buffer (statement)
"Find the theorem number corresponding to STATEMENT in the current buffer visiting HolNaturals.txt"
(goto-char (point-min))
(while (not (eolp))
(search-forward (concat ": " statement)))
(beginning-of-line)
(forward-word 3)
(word-at-point))
(defun find-thm-number (statement)
"Find the theorem number corresponding to STATEMENT in file HolNaturals.txt"
(with-temp-buffer
(insert-file-contents "HolNaturals.txt")
(find-thm-number-in-buffer statement) ))
(defun update-thm-number-on-previous-line (statement)
"Update the previous line by replacing any occurence of thm_XXX by thm_YYY where YYY is the number given by find-thm-number"
(let ((thm-number (find-thm-number statement))
(end (point)))
(forward-line (- 1))
(beginning-of-line)
(replace-regexp "thm_[0-9]+" (concat "thm_" thm-number) nil (point) end)
)
)
(defun update-all-thm-numbers ()
(interactive)
(goto-char (point-min))
(while (search-forward "update-thm-number-on-previous-line")
(forward-word (- 6))
(forward-char (- 1))
(forward-sexp 1)
(eval-last-sexp nil)
(forward-line 2))
)
(provide 'update-thm-numbers)
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