(in-package "RTL")

(include-book "calendar")

;;-----------------------------------------------------------------------------------------------------------
;; Moments
;;-----------------------------------------------------------------------------------------------------------

;; A moment is determined by its three components:

(defun day (x) (ag 'day x))
(defun hour (x) (ag 'hour x))
(defun part (x) (ag 'part x))

(defund momentp (x)
  (and (natp (day x))
       (natp (hour x)) (< (hour x) 24)
       (natp (part x)) (< (part x) 1080)))

(defund momentp= (x y)
  (and (= (day x) (day y)) (= (hour x) (hour y)) (= (part x) (part y))))

;; momentp is closed under timaplus and multime:

(defthm momentp+
  (implies (and (momentp x) (momentp y))
           (momentp (addtime x y)))
  :hints (("Goal" :in-theory (enable fl momentp day hour part addtime))))

(defthm momentp*
  (implies (and (natp n) (momentp x))
           (momentp (multime n x)))
  :hints (("Goal" :in-theory (enable fl momentp multime))))

;; Every molad or delayed-molad is a moment:

(defthm momentp-beharad
  (momentp (beharad))
  :hints (("Goal" :in-theory (enable momentp beharad))))

(defthm momentp-lunation
  (momentp (lunation))
  :hints (("Goal" :in-theory (enable momentp lunation))))

(defthm natp-priormonths
  (implies (natp n)
           (natp (molad-loop-0 y year n)))
  :rule-classes (:type-prescription :rewrite)
  :hints (("Goal" :in-theory (enable molad-loop-0))))

(defthm momentp-molad
  (implies (posp year)
           (momentp (molad year)))
  :hints (("Goal" :in-theory (enable molad))))

(defthmd momentp-delayedmolad
  (implies (posp year)
           (momentp (delayedmolad year)))
  :hints (("Goal" :in-theory (enable delayedmolad))))

;; Total number of parts in a moment:

(defund expand (x)
  (+ (* 1080
        (+ (* 24 (day x))
           (hour x)))        
     (part x)))

(defthm expand=
  (implies (and (momentp x) (momentp y) (= (expand x) (expand y)))
           (momentp= x y))
  :rule-classes ()
  :hints (("Goal" :in-theory (e/d (momentp expand momentp=) (ACL2::|(equal (mod (+ x y) z) x)|))
                  :use ((:instance mod-mult (m (part x)) (n 1080) (a (+ (hour x) (* 24 (day x)))))
			(:instance mod-mult (m (part y)) (n 1080) (a (+ (hour y) (* 24 (day y)))))
		        (:instance mod-mult (m (hour x)) (n 24) (a (day x)))
		        (:instance mod-mult (m (hour y)) (n 24) (a (day y)))))))

(defthmd expand+
  (implies (and (momentp x) (momentp y))
           (equal (expand (addtime x y))
	          (+ (expand x) (expand y))))
  :hints (("Goal" :in-theory (enable momentp addtime expand)
                  :use ((:instance mod-def (x (+ (part x) (part y))) (y 1080))
		        (:instance mod-def (x (+ (hour x) (hour y) (fl (/ (+ (part x) (part y)) 1080)))) (y 24))))))

(defthmd expand*
  (implies (and (natp m) (momentp x))
           (equal (expand (multime m x))
	          (* m (expand x))))
  :hints (("Goal" :in-theory (enable momentp multime expand)
                  :use ((:instance mod-def (x (* m (part x))) (y 1080))
		        (:instance mod-def (x (+ (* m (hour x)) (fl (/ (* m (part x)) 1080)))) (y 24))))))


;;-----------------------------------------------------------------------------------------------------------
;; Admissibility of year lengths: 353, 354, or 355 for a common year; 383, 384, or 385 for a leap year
;;-----------------------------------------------------------------------------------------------------------

;; Complement of a time of day:

(defund comp-time (hour part)
  (if (zp part)
      (mv (- 24 hour) 0)
    (mv (- 23 hour) (- 1080 part))))

;; Number of days between one delayed molad and the next:

(defthm next-molad
  (implies (and (momentp molad)
		(momentp delta))
           (let ((next (addtime molad delta)))
	     (mv-let (comp-hour comp-part) (comp-time (hour delta) (part delta))
	       (if1 (earlier molad comp-hour comp-part)
	            (and (= (day next) (+ (day molad) (day delta)))
		         (= (earlier next (hour delta) (part delta)) 0))
	         (and (= (day next) (+ 1 (day molad) (day delta)))
		      (= (earlier next (hour delta) (part delta)) 1))))))
  :hints (("Goal" :nonlinearp t
                  :in-theory (enable addtime momentp comp-time expand earlier)
		  :use ((:instance expand+ (x molad) (y delta))
		        (:instance momentp+ (x molad) (y delta))))))

;; Difference between successive delayed molodot:

(defthmd molad-loop-0-plus
  (implies (and (natp n)
		(posp y)
		(posp k)
		(posp year)
		(<= y k)
		(<= k year))
	   (equal (molad-loop-0 y year n)
		  (molad-loop-0 k year (molad-loop-0 y k n))))
  :hints (("Goal" :in-theory (enable molad-loop-0))))

(defthm molad-loop-0-plus-1
  (implies (posp year)
	   (equal (molad-loop-0 1 (+ 1 year) 0)
		  (+ (molad-loop-0 1 year 0)
		     (monthsinyear year))))
  :hints (("Goal" :in-theory (enable molad-loop-0)
	          :use ((:instance molad-loop-0-plus (n 0) (y 1) (year (1+ year)) (k year))))))

(defthmd delayed-molad-next
  (implies (posp year)
           (momentp= (delayedmolad (1+ year))
	             (addtime (delayedmolad year)
		               (multime (if1 (common year) 12 13) (lunation)))))
  :hints (("Goal" :in-theory (enable common monthsinyear delayedmolad molad expand+ expand*)
                  :use ((:instance expand= (x (delayedmolad (1+ year)))
		                           (y (addtime (delayedmolad year)
		                                        (multime (if1 (common year) 12 13) (lunation)))))))))

(defthmd next-molad-common
  (implies (and (posp year) (= (common year) 1))
           (let ((molad (delayedmolad year))
	         (next (delayedmolad (1+ year))))
	     (if1 (earlier molad 15 204)
                  (and (= (day next) (+ (day molad) 354))
		       (= (earlier next 8 876) 0))
	        (and (= (day next) (+ (day molad) 355))
		     (= (earlier next 8 876) 1)))))
  :hints (("Goal" :in-theory (enable earlier momentp momentp= lunation)
                  :use (momentp-delayedmolad delayed-molad-next
		        (:instance next-molad (molad (delayedmolad year)) (delta (multime 12 (lunation))))))))

(defthm next-molad-leap
  (implies (and (posp year) (= (leap year) 1))
           (let ((molad (delayedmolad year))
	         (next (delayedmolad (1+ year))))
	     (if1 (earlier molad 2 491)
                  (and (= (day next) (+ (day molad) 383))
		       (= (earlier next 21 589) 0))
	        (and (= (day next) (+ (day molad) 384))
		     (= (earlier next 21 589) 1)))))
  :hints (("Goal" :in-theory (enable common earlier momentp momentp= lunation)
                  :use (momentp-delayedmolad delayed-molad-next
		        (:instance next-molad (molad (delayedmolad year)) (delta (multime 13 (lunation))))))))

;; Enumeration of the days of the week (used to force a case split):

(defthmd days-of-week
  (implies (natp d)
           (member (dayofweek d)
	           '(0 1 2 3 4 5 6)))
  :hints (("Goal" :in-theory (enable dayofweek))))

;; The day of the week that occurs k days after a given day of the week:

(defthmd dayofweek-plus
  (implies (and (natp d) (natp k))
           (equal (dayofweek (+ k d))
	          (dayofweek (+ k (dayofweek d)))))
  :hints (("Goal" :in-theory (enable dayofweek))))

;; The following is proved by a case analysis based on next-molad-common and next-molad-leap:

(defthm legal-year-lengths
  (implies (posp year)
           (member (yearlength year)
		   (if1 (leap year)
		        '(383 384 385)
		      '(353 354 355))))
  :hints (("Goal" :in-theory (enable common momentp yearlength earlier)
                  :expand ((roshhashanah year) (roshhashanah (+ 1 year)))
                  :use (momentp-delayedmolad next-molad-common next-molad-leap
			(:instance momentp-delayedmolad (year (1+ year)))
			(:instance dayofweek-plus (d (day (delayedmolad year))) (k (if1 (leap year) 383 354)))
			(:instance dayofweek-plus (d (day (delayedmolad year))) (k (if1 (leap year) 384 355)))
			(:instance days-of-week (d (day (delayedmolad year))))))))


;;-----------------------------------------------------------------------------------------------------------
;; 20 possible keviyot
;;-----------------------------------------------------------------------------------------------------------

(defthmd dayofweek-roshhashanah
  (implies (posp year)
           (member (dayofweek (roshhashanah year))
	           '(0 2 3 5)))
  :hints (("Goal" :in-theory (enable dayofweek-plus momentp common roshhashanah)
	   :use (momentp-delayedmolad (:instance days-of-week (d (day (delayedmolad year))))))))

(defthmd keviyot
  (implies (posp year)
           (let ((dw (dayofweek (roshhashanah year)))
	         (len (yearlength year)))
	     (or (and (= dw 3)
	              (member len '(354 384)))
		 (and (member dw '(0 2))
		      (member len '(353 355 383 385)))
		 (and (= dw 5)
		      (member len '(354 355 383 385))))))
  :hints (("Goal" :in-theory (enable momentp roshhashanah dayofweek-plus common yearlength)
                  :use (legal-year-lengths dayofweek-roshhashanah momentp-delayedmolad next-molad-leap
					   (:instance dayofweek-roshhashanah (year (1+ year)))))))


;;-----------------------------------------------------------------------------------------------------------
;; Landau's theorem: The molad of every month occurs before the end of the 1st day of the month.
;;-----------------------------------------------------------------------------------------------------------

(defthm natp-roshhashanah
  (implies (natp year) (natp (roshhashanah year)))
  :hints (("Goal" :in-theory (enable momentp roshhashanah)
                  :use (momentp-delayedmolad)))
  :rule-classes (:rewrite :type-prescription))

;; Difference between successive molodot:

(defthmd molad-next
  (implies (posp year)
           (momentp= (molad (1+ year))
	             (addtime (molad year)
		              (multime (if1 (common year) 12 13) (lunation)))))
  :hints (("Goal" :in-theory (enable common monthsinyear molad expand+ expand*)
                  :use ((:instance expand= (x (molad (1+ year)))
		                           (y (addtime (molad year)
						       (multime (if1 (common year) 12 13) (lunation)))))))))

;; This bound is sufficient for year lengths 355, 384, and 385:

(defthmd molad-roshhashanah
  (implies (natp year)
            (< (expand (molad year))
	       (* 1080 (+ 18 (* 24 (roshhashanah year))))))
  :hints (("Goal" :in-theory (enable earlier addtime momentp expand roshhashanah delayedmolad)
		  :nonlinearp t
		  :cases ((= (earlier (molad year) 18 0) 0))
                  :use (momentp-molad
		        (:instance fl-unique (x (/ (part (molad year)) 1080)) (n 0))
		        (:instance fl-unique (x (/ (+ (hour (molad year)) 6) 24)) (n 1))
		        (:instance fl-unique (x (/ (+ (hour (molad year)) 6) 24)) (n 0))))))

;; This bound is required for year lengths 353, 354, and 383:

(defthmd molad-roshhashanah-next
  (implies (posp year)
            (< (expand (molad year))
	       (- (* 1080 (+ 18 (* 24 (+ (roshhashanah year) (yearlength year)))))
		  (* (if1 (leap year) 13 12) (expand (lunation))))))
  :hints (("Goal" :in-theory (enable common momentp= momentp expand yearlength)
                  :use (momentp-molad molad-next
		        (:instance expand+ (x (molad year)) (y (multime (if1 (common year) 12 13) (lunation))))
			(:instance molad-roshhashanah (year (1+ year)))))))

;; First day of month:

(defun firstofmonth (month year) (as 'day 1 (as 'month month (as 'year year ()))))

;; This splits into the 6 cases of year length and applies one of the above 2 bounds in each case:

(defthmd expand-monthlymolad
  (implies (and (posp year)
                (posp month)
		(<= month (if1 (leap year) 13 12)))
	   (< (expand (monthlymolad month year))
	      (* 1080 24 (1+ (h2a (firstofmonth month year))))))
  :hints (("Goal" :in-theory (enable monthlymolad monthlength h2a expand+ expand*)
                  :use (legal-year-lengths molad-roshhashanah molad-roshhashanah-next)
	          :expand ((:free (x y z) (h2a-loop-0 x y z))))))

(defthmd expand-day
  (implies (and (momentp x)
                (natp d)
		(< (expand x) (* 1080 24 (1+ d))))
	   (<= (day x) d))
  :hints (("Goal" :in-theory (enable momentp expand))))

(defthmd natp-h2a
  (implies (and (posp (ag 'year date))
                (posp (ag 'day date))
                (posp (ag 'month date))
		(<= (ag 'month date) 13))
           (natp (h2a date)))
  :hints (("Goal" :in-theory (enable monthlength h2a h2a-loop-0)
	          :expand ((:free (x y z) (h2a-loop-0 x y z))))))

(defthm landau-thm
  (implies (and (posp year)
		(posp month)
		(<= month (monthsinyear year)))
	   (<= (day (monthlymolad month year))
	       (h2a (firstofmonth month year))))
  :hints (("Goal" :in-theory (enable monthsinyear monthlymolad)
                  :use (expand-monthlymolad
		        (:instance natp-h2a (date (firstofmonth month year)))
                        (:instance expand-day (x (monthlymolad month year))
				              (d (h2a (firstofmonth month year))))))))