Structure OmegaTheory

signature OmegaTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val fst1_def : thm
    val fst_nzero_def : thm
    val modhat_def : thm
    val real_shadow_def : thm
  
  (*  Theorems  *)
    val MAP2_def : thm
    val MAP2_ind : thm
    val MAP2_zero_ADD : thm
    val alternative_equivalence : thm
    val basic_shadow_equivalence : thm
    val bigger_satisfies_lowers : thm
    val calc_nightmare_def : thm
    val calc_nightmare_ind : thm
    val calculational_nightmare : thm
    val dark_implies_real : thm
    val dark_shadow_FORALL : thm
    val dark_shadow_cond_row_def : thm
    val dark_shadow_cond_row_ind : thm
    val dark_shadow_condition_def : thm
    val dark_shadow_condition_ind : thm
    val dark_shadow_def : thm
    val dark_shadow_ind : thm
    val dark_shadow_row_def : thm
    val dark_shadow_row_ind : thm
    val darkrow_implies_realrow : thm
    val equality_removal : thm
    val eval_base : thm
    val eval_step_extra1 : thm
    val eval_step_extra2 : thm
    val eval_step_extra3 : thm
    val eval_step_extra4 : thm
    val eval_step_lower1 : thm
    val eval_step_lower2 : thm
    val eval_step_upper1 : thm
    val eval_step_upper2 : thm
    val evallower_FORALL : thm
    val evallower_def : thm
    val evallower_ind : thm
    val evalupper_FORALL : thm
    val evalupper_def : thm
    val evalupper_ind : thm
    val exact_shadow_case : thm
    val final_equivalence : thm
    val nightmare_EXISTS : thm
    val nightmare_def : thm
    val nightmare_implies_LHS : thm
    val nightmare_ind : thm
    val onlylowers_satisfiable : thm
    val onlyuppers_satisfiable : thm
    val real_shadow_FORALL : thm
    val real_shadow_always_implied : thm
    val real_shadow_revimp_lowers1 : thm
    val real_shadow_revimp_uppers1 : thm
    val rshadow_row_def : thm
    val rshadow_row_ind : thm
    val singleton_real_shadow : thm
    val smaller_satisfies_uppers : thm
    val sumc_ADD : thm
    val sumc_MULT : thm
    val sumc_def : thm
    val sumc_ind : thm
    val sumc_nonsingle : thm
    val sumc_singleton : thm
    val sumc_thm : thm
  
  val Omega_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [integer] Parent theory of "Omega"
   
   [fst1_def]  Definition
      
      ⊢ ∀x. fst1 x ⇔ (FST x = 1)
   
   [fst_nzero_def]  Definition
      
      ⊢ ∀x. fst_nzero x ⇔ 0 < FST x
   
   [modhat_def]  Definition
      
      ⊢ ∀x y. modhat x y = x − y * ((2 * x + y) / (2 * y))
   
   [real_shadow_def]  Definition
      
      ⊢ (∀lowers. real_shadow [] lowers ⇔ T) ∧
        ∀upper ls lowers.
            real_shadow (upper::ls) lowers ⇔
            rshadow_row upper lowers ∧ real_shadow ls lowers
   
   [MAP2_def]  Theorem
      
      ⊢ (∀pad f. MAP2 pad f [] [] = []) ∧
        (∀ys y pad f. MAP2 pad f [] (y::ys) = f pad y::MAP2 pad f [] ys) ∧
        (∀xs x pad f. MAP2 pad f (x::xs) [] = f x pad::MAP2 pad f xs []) ∧
        ∀ys y xs x pad f.
            MAP2 pad f (x::xs) (y::ys) = f x y::MAP2 pad f xs ys
   
   [MAP2_ind]  Theorem
      
      ⊢ ∀P.
            (∀pad f. P pad f [] []) ∧
            (∀pad f y ys. P pad f [] ys ⇒ P pad f [] (y::ys)) ∧
            (∀pad f x xs. P pad f xs [] ⇒ P pad f (x::xs) []) ∧
            (∀pad f x xs y ys. P pad f xs ys ⇒ P pad f (x::xs) (y::ys)) ⇒
            ∀v v1 v2 v3. P v v1 v2 v3
   
   [MAP2_zero_ADD]  Theorem
      
      ⊢ ∀xs. (MAP2 0 $+ [] xs = xs) ∧ (MAP2 0 $+ xs [] = xs)
   
   [alternative_equivalence]  Theorem
      
      ⊢ ∀uppers lowers m.
            EVERY fst_nzero uppers ∧ EVERY fst_nzero lowers ∧
            EVERY (λp. FST p ≤ m) uppers ⇒
            ((∃x. evalupper x uppers ∧ evallower x lowers) ⇔
             dark_shadow uppers lowers ∨
             ∃x. nightmare x m uppers lowers lowers)
   
   [basic_shadow_equivalence]  Theorem
      
      ⊢ ∀uppers lowers.
            EVERY fst_nzero uppers ∧ EVERY fst_nzero lowers ⇒
            ((∃x. evalupper x uppers ∧ evallower x lowers) ⇔
             real_shadow uppers lowers ∧
             dark_shadow_condition uppers lowers)
   
   [bigger_satisfies_lowers]  Theorem
      
      ⊢ ∀lowers x y. evallower x lowers ∧ x < y ⇒ evallower y lowers
   
   [calc_nightmare_def]  Theorem
      
      ⊢ (∀x c. calc_nightmare x c [] ⇔ F) ∧
        ∀x rs d c R.
            calc_nightmare x c ((d,R)::rs) ⇔
            (∃i. (0 ≤ i ∧ i ≤ (&c * &d − &c − &d) / &c) ∧ (&d * x = R + i)) ∨
            calc_nightmare x c rs
   
   [calc_nightmare_ind]  Theorem
      
      ⊢ ∀P.
            (∀x c. P x c []) ∧ (∀x c d R rs. P x c rs ⇒ P x c ((d,R)::rs)) ⇒
            ∀v v1 v2. P v v1 v2
   
   [calculational_nightmare]  Theorem
      
      ⊢ ∀rs.
            nightmare x c uppers lowers rs ⇔
            calc_nightmare x c rs ∧ evalupper x uppers ∧ evallower x lowers
   
   [dark_implies_real]  Theorem
      
      ⊢ ∀uppers lowers.
            EVERY fst_nzero uppers ∧ EVERY fst_nzero lowers ∧
            dark_shadow uppers lowers ⇒
            real_shadow uppers lowers
   
   [dark_shadow_FORALL]  Theorem
      
      ⊢ ∀uppers lowers.
            dark_shadow uppers lowers ⇔
            ∀c d L R.
                MEM (c,L) uppers ∧ MEM (d,R) lowers ⇒
                &d * L − &c * R ≥ (&c − 1) * (&d − 1)
   
   [dark_shadow_cond_row_def]  Theorem
      
      ⊢ (∀c L. dark_shadow_cond_row (c,L) [] ⇔ T) ∧
        ∀t d c R L.
            dark_shadow_cond_row (c,L) ((d,R)::t) ⇔
            ¬(∃i.
                 &c * &d * i < &c * R ∧ &c * R ≤ &d * L ∧
                 &d * L < &c * &d * (i + 1)) ∧ dark_shadow_cond_row (c,L) t
   
   [dark_shadow_cond_row_ind]  Theorem
      
      ⊢ ∀P.
            (∀c L. P (c,L) []) ∧
            (∀c L d R t. P (c,L) t ⇒ P (c,L) ((d,R)::t)) ⇒
            ∀v v1 v2. P (v,v1) v2
   
   [dark_shadow_condition_def]  Theorem
      
      ⊢ (∀lowers. dark_shadow_condition [] lowers ⇔ T) ∧
        ∀uppers lowers c L.
            dark_shadow_condition ((c,L)::uppers) lowers ⇔
            dark_shadow_cond_row (c,L) lowers ∧
            dark_shadow_condition uppers lowers
   
   [dark_shadow_condition_ind]  Theorem
      
      ⊢ ∀P.
            (∀lowers. P [] lowers) ∧
            (∀c L uppers lowers. P uppers lowers ⇒ P ((c,L)::uppers) lowers) ⇒
            ∀v v1. P v v1
   
   [dark_shadow_def]  Theorem
      
      ⊢ (∀lowers. dark_shadow [] lowers ⇔ T) ∧
        ∀uppers lowers c L.
            dark_shadow ((c,L)::uppers) lowers ⇔
            dark_shadow_row c L lowers ∧ dark_shadow uppers lowers
   
   [dark_shadow_ind]  Theorem
      
      ⊢ ∀P.
            (∀lowers. P [] lowers) ∧
            (∀c L uppers lowers. P uppers lowers ⇒ P ((c,L)::uppers) lowers) ⇒
            ∀v v1. P v v1
   
   [dark_shadow_row_def]  Theorem
      
      ⊢ (∀c L. dark_shadow_row c L [] ⇔ T) ∧
        ∀rs d c R L.
            dark_shadow_row c L ((d,R)::rs) ⇔
            &d * L − &c * R ≥ (&c − 1) * (&d − 1) ∧ dark_shadow_row c L rs
   
   [dark_shadow_row_ind]  Theorem
      
      ⊢ ∀P.
            (∀c L. P c L []) ∧ (∀c L d R rs. P c L rs ⇒ P c L ((d,R)::rs)) ⇒
            ∀v v1 v2. P v v1 v2
   
   [darkrow_implies_realrow]  Theorem
      
      ⊢ ∀lowers c L.
            0 < c ∧ EVERY fst_nzero lowers ∧ dark_shadow_row c L lowers ⇒
            rshadow_row (c,L) lowers
   
   [equality_removal]  Theorem
      
      ⊢ ∀c x cs vs.
            0 < c ⇒
            ((0 = c * x + sumc cs vs) ⇔
             ∃s.
                 (x =
                  -(c + 1) * s + sumc (MAP (λx. modhat x (c + 1)) cs) vs) ∧
                 (0 = c * x + sumc cs vs))
   
   [eval_base]  Theorem
      
      ⊢ p ⇔ ((evalupper x [] ∧ evallower x []) ∧ T) ∧ p
   
   [eval_step_extra1]  Theorem
      
      ⊢ ((evalupper x ups ∧ evallower x lows) ∧ T) ∧ ex' ⇔
        (evalupper x ups ∧ evallower x lows) ∧ ex'
   
   [eval_step_extra2]  Theorem
      
      ⊢ ((evalupper x ups ∧ evallower x lows) ∧ ex) ∧ ex' ⇔
        (evalupper x ups ∧ evallower x lows) ∧ ex ∧ ex'
   
   [eval_step_extra3]  Theorem
      
      ⊢ ((evalupper x ups ∧ evallower x lows) ∧ T) ∧ ex' ∧ p ⇔
        ((evalupper x ups ∧ evallower x lows) ∧ ex') ∧ p
   
   [eval_step_extra4]  Theorem
      
      ⊢ ((evalupper x ups ∧ evallower x lows) ∧ ex) ∧ ex' ∧ p ⇔
        ((evalupper x ups ∧ evallower x lows) ∧ ex ∧ ex') ∧ p
   
   [eval_step_lower1]  Theorem
      
      ⊢ ((evalupper x ups ∧ evallower x lows) ∧ ex) ∧ r ≤ &c * x ⇔
        (evalupper x ups ∧ evallower x ((c,r)::lows)) ∧ ex
   
   [eval_step_lower2]  Theorem
      
      ⊢ ((evalupper x ups ∧ evallower x lows) ∧ ex) ∧ r ≤ &c * x ∧ p ⇔
        ((evalupper x ups ∧ evallower x ((c,r)::lows)) ∧ ex) ∧ p
   
   [eval_step_upper1]  Theorem
      
      ⊢ ((evalupper x ups ∧ evallower x lows) ∧ ex) ∧ &c * x ≤ r ⇔
        (evalupper x ((c,r)::ups) ∧ evallower x lows) ∧ ex
   
   [eval_step_upper2]  Theorem
      
      ⊢ ((evalupper x ups ∧ evallower x lows) ∧ ex) ∧ &c * x ≤ r ∧ p ⇔
        ((evalupper x ((c,r)::ups) ∧ evallower x lows) ∧ ex) ∧ p
   
   [evallower_FORALL]  Theorem
      
      ⊢ ∀lowers x. evallower x lowers ⇔ ∀d R. MEM (d,R) lowers ⇒ R ≤ &d * x
   
   [evallower_def]  Theorem
      
      ⊢ (∀x. evallower x [] ⇔ T) ∧
        ∀y x cs c. evallower x ((c,y)::cs) ⇔ y ≤ &c * x ∧ evallower x cs
   
   [evallower_ind]  Theorem
      
      ⊢ ∀P.
            (∀x. P x []) ∧ (∀x c y cs. P x cs ⇒ P x ((c,y)::cs)) ⇒
            ∀v v1. P v v1
   
   [evalupper_FORALL]  Theorem
      
      ⊢ ∀uppers x. evalupper x uppers ⇔ ∀c L. MEM (c,L) uppers ⇒ &c * x ≤ L
   
   [evalupper_def]  Theorem
      
      ⊢ (∀x. evalupper x [] ⇔ T) ∧
        ∀y x cs c. evalupper x ((c,y)::cs) ⇔ &c * x ≤ y ∧ evalupper x cs
   
   [evalupper_ind]  Theorem
      
      ⊢ ∀P.
            (∀x. P x []) ∧ (∀x c y cs. P x cs ⇒ P x ((c,y)::cs)) ⇒
            ∀v v1. P v v1
   
   [exact_shadow_case]  Theorem
      
      ⊢ ∀uppers lowers.
            EVERY fst_nzero uppers ∧ EVERY fst_nzero lowers ⇒
            EVERY fst1 uppers ∨ EVERY fst1 lowers ⇒
            ((∃x. evalupper x uppers ∧ evallower x lowers) ⇔
             real_shadow uppers lowers)
   
   [final_equivalence]  Theorem
      
      ⊢ ∀uppers lowers m.
            EVERY fst_nzero uppers ∧ EVERY fst_nzero lowers ∧
            EVERY (λp. FST p ≤ m) uppers ⇒
            ((∃x. evalupper x uppers ∧ evallower x lowers) ⇔
             real_shadow uppers lowers ∧
             (dark_shadow uppers lowers ∨
              ∃x. nightmare x m uppers lowers lowers))
   
   [nightmare_EXISTS]  Theorem
      
      ⊢ ∀rs x c uppers lowers.
            nightmare x c uppers lowers rs ⇔
            ∃i d R.
                0 ≤ i ∧ i ≤ (&d * &c − &c − &d) / &c ∧ MEM (d,R) rs ∧
                evalupper x uppers ∧ evallower x lowers ∧ (&d * x = R + i)
   
   [nightmare_def]  Theorem
      
      ⊢ (∀x uppers lowers c. nightmare x c uppers lowers [] ⇔ F) ∧
        ∀x uppers rs lowers d c R.
            nightmare x c uppers lowers ((d,R)::rs) ⇔
            (∃i.
                 (0 ≤ i ∧ i ≤ (&c * &d − &c − &d) / &c) ∧
                 (&d * x = R + i) ∧ evalupper x uppers ∧ evallower x lowers) ∨
            nightmare x c uppers lowers rs
   
   [nightmare_implies_LHS]  Theorem
      
      ⊢ ∀rs x uppers lowers c.
            nightmare x c uppers lowers rs ⇒
            evalupper x uppers ∧ evallower x lowers
   
   [nightmare_ind]  Theorem
      
      ⊢ ∀P.
            (∀x c uppers lowers. P x c uppers lowers []) ∧
            (∀x c uppers lowers d R rs.
                 P x c uppers lowers rs ⇒ P x c uppers lowers ((d,R)::rs)) ⇒
            ∀v v1 v2 v3 v4. P v v1 v2 v3 v4
   
   [onlylowers_satisfiable]  Theorem
      
      ⊢ ∀lowers. EVERY fst_nzero lowers ⇒ ∃x. evallower x lowers
   
   [onlyuppers_satisfiable]  Theorem
      
      ⊢ ∀uppers. EVERY fst_nzero uppers ⇒ ∃x. evalupper x uppers
   
   [real_shadow_FORALL]  Theorem
      
      ⊢ ∀uppers lowers.
            real_shadow uppers lowers ⇔
            ∀c d L R. MEM (c,L) uppers ∧ MEM (d,R) lowers ⇒ &c * R ≤ &d * L
   
   [real_shadow_always_implied]  Theorem
      
      ⊢ ∀uppers lowers x.
            evalupper x uppers ∧ evallower x lowers ∧
            EVERY fst_nzero uppers ∧ EVERY fst_nzero lowers ⇒
            real_shadow uppers lowers
   
   [real_shadow_revimp_lowers1]  Theorem
      
      ⊢ ∀uppers lowers c L x.
            0 < c ∧ rshadow_row (c,L) lowers ∧ evalupper x uppers ∧
            evallower x lowers ∧ EVERY fst_nzero uppers ∧ EVERY fst1 lowers ⇒
            ∃x. &c * x ≤ L ∧ evalupper x uppers ∧ evallower x lowers
   
   [real_shadow_revimp_uppers1]  Theorem
      
      ⊢ ∀uppers lowers L x.
            rshadow_row (1,L) lowers ∧ evallower x lowers ∧
            evalupper x uppers ∧ EVERY fst_nzero lowers ∧ EVERY fst1 uppers ⇒
            ∃x. x ≤ L ∧ evalupper x uppers ∧ evallower x lowers
   
   [rshadow_row_def]  Theorem
      
      ⊢ (∀uppery upperc. rshadow_row (upperc,uppery) [] ⇔ T) ∧
        ∀uppery upperc rs lowery lowerc.
            rshadow_row (upperc,uppery) ((lowerc,lowery)::rs) ⇔
            &upperc * lowery ≤ &lowerc * uppery ∧
            rshadow_row (upperc,uppery) rs
   
   [rshadow_row_ind]  Theorem
      
      ⊢ ∀P.
            (∀upperc uppery. P (upperc,uppery) []) ∧
            (∀upperc uppery lowerc lowery rs.
                 P (upperc,uppery) rs ⇒
                 P (upperc,uppery) ((lowerc,lowery)::rs)) ⇒
            ∀v v1 v2. P (v,v1) v2
   
   [singleton_real_shadow]  Theorem
      
      ⊢ ∀c L x.
            &c * x ≤ L ∧ 0 < c ⇒
            ∀lowers.
                EVERY fst_nzero lowers ∧ evallower x lowers ⇒
                rshadow_row (c,L) lowers
   
   [smaller_satisfies_uppers]  Theorem
      
      ⊢ ∀uppers x y. evalupper x uppers ∧ y < x ⇒ evalupper y uppers
   
   [sumc_ADD]  Theorem
      
      ⊢ ∀cs vs ds. sumc cs vs + sumc ds vs = sumc (MAP2 0 $+ cs ds) vs
   
   [sumc_MULT]  Theorem
      
      ⊢ ∀cs vs f. f * sumc cs vs = sumc (MAP (λx. f * x) cs) vs
   
   [sumc_def]  Theorem
      
      ⊢ (∀v0. sumc v0 [] = 0) ∧ (∀v5 v4. sumc [] (v4::v5) = 0) ∧
        ∀vs v cs c. sumc (c::cs) (v::vs) = c * v + sumc cs vs
   
   [sumc_ind]  Theorem
      
      ⊢ ∀P.
            (∀v0. P v0 []) ∧ (∀v4 v5. P [] (v4::v5)) ∧
            (∀c cs v vs. P cs vs ⇒ P (c::cs) (v::vs)) ⇒
            ∀v v1. P v v1
   
   [sumc_nonsingle]  Theorem
      
      ⊢ ∀f cs c v vs.
            sumc (MAP f (c::cs)) (v::vs) = f c * v + sumc (MAP f cs) vs
   
   [sumc_singleton]  Theorem
      
      ⊢ ∀f c. sumc (MAP f [c]) [1] = f c
   
   [sumc_thm]  Theorem
      
      ⊢ ∀cs vs c v.
            (sumc [] vs = 0) ∧ (sumc cs [] = 0) ∧
            (sumc (c::cs) (v::vs) = c * v + sumc cs vs)
   
   
*)
end

HOL 4, Kananaskis-13