Theory "Omega"

Parents integer

Signature

Constant	Type
sumc_tupled	:int list # int list -> int
sumc	:int list -> int list -> int
rshadow_row_tupled	:(num # int) # (num # int) list -> bool
rshadow_row	:num # int -> (num # int) list -> bool
real_shadow	:(num # int) list -> (num # int) list -> bool
nightmare_tupled	:int # num # (num # int) list # (num # int) list # (num # int) list -> bool
nightmare	:int -> num -> (num # int) list -> (num # int) list -> (num # int) list -> bool
modhat	:int -> int -> int
fst_nzero	:num # 'a -> bool
fst1	:num # 'a -> bool
evalupper_tupled	:int # (num # int) list -> bool
evalupper	:int -> (num # int) list -> bool
evallower_tupled	:int # (num # int) list -> bool
evallower	:int -> (num # int) list -> bool
dark_shadow_tupled	:(num # int) list # (num # int) list -> bool
dark_shadow_row_tupled	:num # int # (num # int) list -> bool
dark_shadow_row	:num -> int -> (num # int) list -> bool
dark_shadow_condition_tupled	:(num # int) list # (num # int) list -> bool
dark_shadow_condition	:(num # int) list -> (num # int) list -> bool
dark_shadow_cond_row_tupled	:(num # int) # (num # int) list -> bool
dark_shadow_cond_row	:num # int -> (num # int) list -> bool
dark_shadow	:(num # int) list -> (num # int) list -> bool
calc_nightmare_tupled	:int # num # (num # int) list -> bool
calc_nightmare	:int -> num -> (num # int) list -> bool
MAP2_tupled	:'b # ('b -> 'b -> 'a) # 'b list # 'b list -> 'a list
MAP2	:'b -> ('b -> 'b -> 'a) -> 'b list -> 'b list -> 'a list

Definitions

MAP2_tupled_primitive_def

|- MAP2_tupled =
   WFREC
     (@R.
        WF R /\ (!y ys f pad. R (pad,f,[],ys) (pad,f,[],y::ys)) /\
        (!x xs f pad. R (pad,f,xs,[]) (pad,f,x::xs,[])) /\
        !y x ys xs f pad. R (pad,f,xs,ys) (pad,f,x::xs,y::ys))
     (\MAP2_tupled a.
        case a of
           (pad,f,[],[]) -> I []
        || (pad,f,[],y::ys) -> I (f pad y::MAP2_tupled (pad,f,[],ys))
        || (pad,f,x::xs,[]) -> I (f x pad::MAP2_tupled (pad,f,xs,[]))
        || (pad,f,x::xs,y'::ys') -> I (f x y'::MAP2_tupled (pad,f,xs,ys')))

MAP2_curried_def

|- !x x1 x2 x3. MAP2 x x1 x2 x3 = MAP2_tupled (x,x1,x2,x3)

sumc_tupled_primitive_def

|- sumc_tupled =
   WFREC (@R. WF R /\ !v c vs cs. R (cs,vs) (c::cs,v::vs))
     (\sumc_tupled a.
        case a of
           ([],[]) -> I 0
        || ([],v10::v11) -> I 0
        || (c::cs,[]) -> I 0
        || (c::cs,v::vs) -> I (c * v + sumc_tupled (cs,vs)))

sumc_curried_def

|- !x x1. sumc x x1 = sumc_tupled (x,x1)

modhat_def

|- !x y. modhat x y = x - y * ((2 * x + y) / (2 * y))

evalupper_tupled_primitive_def

|- evalupper_tupled =
   WFREC (@R. WF R /\ !y c cs x. R (x,cs) (x,(c,y)::cs))
     (\evalupper_tupled a.
        case a of
           (x,[]) -> I T
        || (x,(c,y)::cs) -> I (& c * x <= y /\ evalupper_tupled (x,cs)))

evalupper_curried_def

|- !x x1. evalupper x x1 = evalupper_tupled (x,x1)

evallower_tupled_primitive_def

|- evallower_tupled =
   WFREC (@R. WF R /\ !y c cs x. R (x,cs) (x,(c,y)::cs))
     (\evallower_tupled a.
        case a of
           (x,[]) -> I T
        || (x,(c,y)::cs) -> I (y <= & c * x /\ evallower_tupled (x,cs)))

evallower_curried_def

|- !x x1. evallower x x1 = evallower_tupled (x,x1)

fst_nzero_def

|- !x. fst_nzero x = 0 < FST x

fst1_def

|- !x. fst1 x = (FST x = 1)

rshadow_row_tupled_primitive_def

|- rshadow_row_tupled =
   WFREC
     (@R.
        WF R /\
        !lowery lowerc rs uppery upperc.
          R ((upperc,uppery),rs) ((upperc,uppery),(lowerc,lowery)::rs))
     (\rshadow_row_tupled a.
        case a of
           ((upperc,uppery),[]) -> I T
        || ((upperc,uppery),(lowerc,lowery)::rs) ->
             I
               (& upperc * lowery <= & lowerc * uppery /\
                rshadow_row_tupled ((upperc,uppery),rs)))

rshadow_row_curried_def

|- !x x1. rshadow_row x x1 = rshadow_row_tupled (x,x1)

real_shadow_def

|- (!lowers. real_shadow [] lowers = T) /\
   !upper ls lowers.
     real_shadow (upper::ls) lowers =
     rshadow_row upper lowers /\ real_shadow ls lowers

dark_shadow_cond_row_tupled_primitive_def

|- dark_shadow_cond_row_tupled =
   WFREC (@R'. WF R' /\ !R d t L c. R' ((c,L),t) ((c,L),(d,R)::t))
     (\dark_shadow_cond_row_tupled a.
        case a of
           ((c,L),[]) -> I T
        || ((c,L),(d,R)::t) ->
             I
               (~(?i.
                    & c * & d * i < & c * R /\ & c * R <= & d * L /\
                    & d * L < & c * & d * (i + 1)) /\
                dark_shadow_cond_row_tupled ((c,L),t)))

dark_shadow_cond_row_curried_def

|- !x x1. dark_shadow_cond_row x x1 = dark_shadow_cond_row_tupled (x,x1)

dark_shadow_condition_tupled_primitive_def

|- dark_shadow_condition_tupled =
   WFREC
     (@R.
        WF R /\ !L c lowers uppers. R (uppers,lowers) ((c,L)::uppers,lowers))
     (\dark_shadow_condition_tupled a.
        case a of
           ([],lowers) -> I T
        || ((c,L)::uppers,lowers) ->
             I
               (dark_shadow_cond_row (c,L) lowers /\
                dark_shadow_condition_tupled (uppers,lowers)))

dark_shadow_condition_curried_def

|- !x x1. dark_shadow_condition x x1 = dark_shadow_condition_tupled (x,x1)

dark_shadow_row_tupled_primitive_def

|- dark_shadow_row_tupled =
   WFREC (@R'. WF R' /\ !R d rs L c. R' (c,L,rs) (c,L,(d,R)::rs))
     (\dark_shadow_row_tupled a.
        case a of
           (c,L,[]) -> I T
        || (c,L,(d,R)::rs) ->
             I
               (& d * L - & c * R >= (& c - 1) * (& d - 1) /\
                dark_shadow_row_tupled (c,L,rs)))

dark_shadow_row_curried_def

|- !x x1 x2. dark_shadow_row x x1 x2 = dark_shadow_row_tupled (x,x1,x2)

dark_shadow_tupled_primitive_def

|- dark_shadow_tupled =
   WFREC
     (@R.
        WF R /\ !L c lowers uppers. R (uppers,lowers) ((c,L)::uppers,lowers))
     (\dark_shadow_tupled a.
        case a of
           ([],lowers) -> I T
        || ((c,L)::uppers,lowers) ->
             I
               (dark_shadow_row c L lowers /\
                dark_shadow_tupled (uppers,lowers)))

dark_shadow_curried_def

|- !x x1. dark_shadow x x1 = dark_shadow_tupled (x,x1)

nightmare_tupled_primitive_def

|- nightmare_tupled =
   WFREC
     (@R'.
        WF R' /\
        !R d rs lowers uppers c x.
          R' (x,c,uppers,lowers,rs) (x,c,uppers,lowers,(d,R)::rs))
     (\nightmare_tupled a.
        case a of
           (x,c,uppers,lowers,[]) -> I F
        || (x,c,uppers,lowers,(d,R)::rs) ->
             I
               ((?i.
                   (0 <= i /\ i <= (& c * & d - & c - & d) / & c) /\
                   (& d * x = R + i) /\ evalupper x uppers /\
                   evallower x lowers) \/
                nightmare_tupled (x,c,uppers,lowers,rs)))

nightmare_curried_def

|- !x x1 x2 x3 x4. nightmare x x1 x2 x3 x4 = nightmare_tupled (x,x1,x2,x3,x4)

calc_nightmare_tupled_primitive_def

|- calc_nightmare_tupled =
   WFREC (@R'. WF R' /\ !R d rs c x. R' (x,c,rs) (x,c,(d,R)::rs))
     (\calc_nightmare_tupled a.
        case a of
           (x,c,[]) -> I F
        || (x,c,(d,R)::rs) ->
             I
               ((?i.
                   (0 <= i /\ i <= (& c * & d - & c - & d) / & c) /\
                   (& d * x = R + i)) \/ calc_nightmare_tupled (x,c,rs)))

calc_nightmare_curried_def

|- !x x1 x2. calc_nightmare x x1 x2 = calc_nightmare_tupled (x,x1,x2)

Theorems

MAP2_ind

|- !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_def

|- (MAP2 pad f [] [] = []) /\
   (MAP2 pad f [] (y::ys) = f pad y::MAP2 pad f [] ys) /\
   (MAP2 pad f (x::xs) [] = f x pad::MAP2 pad f xs []) /\
   (MAP2 pad f (x::xs) (y::ys) = f x y::MAP2 pad f xs ys)

MAP2_zero_ADD

|- !xs. (MAP2 0 $+ [] xs = xs) /\ (MAP2 0 $+ xs [] = xs)

sumc_ind

|- !P.
     (!v4 v5. P (v4::v5) []) /\ P [] [] /\ (!v8 v9. P [] (v8::v9)) /\
     (!c cs v vs. P cs vs ==> P (c::cs) (v::vs)) ==>
     !v v1. P v v1

sumc_def

|- (sumc (v4::v5) [] = 0) /\ (sumc [] [] = 0) /\ (sumc [] (v8::v9) = 0) /\
   (sumc (c::cs) (v::vs) = c * v + sumc cs vs)

sumc_thm

|- !cs vs c v.
     (sumc [] vs = 0) /\ (sumc cs [] = 0) /\
     (sumc (c::cs) (v::vs) = c * v + sumc cs vs)

sumc_ADD

|- !cs vs ds. sumc cs vs + sumc ds vs = sumc (MAP2 0 $+ cs ds) vs

sumc_MULT

|- !cs vs f. f * sumc cs vs = sumc (MAP (\x. f * x) cs) vs

sumc_singleton

|- !f c. sumc (MAP f [c]) [1] = f c

sumc_nonsingle

|- !f cs c v vs. sumc (MAP f (c::cs)) (v::vs) = f c * v + sumc (MAP f cs) vs

equality_removal

|- !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))

evalupper_ind

|- !P.
     (!x. P x []) /\ (!x c y cs. P x cs ==> P x ((c,y)::cs)) ==> !v v1. P v v1

evalupper_def

|- (evalupper x [] = T) /\
   (evalupper x ((c,y)::cs) = & c * x <= y /\ evalupper x cs)

evallower_ind

|- !P.
     (!x. P x []) /\ (!x c y cs. P x cs ==> P x ((c,y)::cs)) ==> !v v1. P v v1

evallower_def

|- (evallower x [] = T) /\
   (evallower x ((c,y)::cs) = y <= & c * x /\ evallower x cs)

smaller_satisfies_uppers

|- !uppers x y. evalupper x uppers /\ y < x ==> evalupper y uppers

bigger_satisfies_lowers

|- !lowers x y. evallower x lowers /\ x < y ==> evallower y lowers

onlylowers_satisfiable

|- !lowers. EVERY fst_nzero lowers ==> ?x. evallower x lowers

onlyuppers_satisfiable

|- !uppers. EVERY fst_nzero uppers ==> ?x. evalupper x uppers

rshadow_row_ind

|- !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

rshadow_row_def

|- (rshadow_row (upperc,uppery) [] = T) /\
   (rshadow_row (upperc,uppery) ((lowerc,lowery)::rs) =
    & upperc * lowery <= & lowerc * uppery /\ rshadow_row (upperc,uppery) rs)

singleton_real_shadow

|- !c L x.
     & c * x <= L /\ 0 < c ==>
     !lowers.
       EVERY fst_nzero lowers /\ evallower x lowers ==>
       rshadow_row (c,L) lowers

real_shadow_revimp_uppers1

|- !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

real_shadow_revimp_lowers1

|- !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_always_implied

|- !uppers lowers x.
     evalupper x uppers /\ evallower x lowers /\ EVERY fst_nzero uppers /\
     EVERY fst_nzero lowers ==>
     real_shadow uppers lowers

exact_shadow_case

|- !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)

dark_shadow_cond_row_ind

|- !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_cond_row_def

|- (dark_shadow_cond_row (c,L) [] = T) /\
   (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_condition_ind

|- !P.
     (!lowers. P [] lowers) /\
     (!c L uppers lowers. P uppers lowers ==> P ((c,L)::uppers) lowers) ==>
     !v v1. P v v1

dark_shadow_condition_def

|- (dark_shadow_condition [] lowers = T) /\
   (dark_shadow_condition ((c,L)::uppers) lowers =
    dark_shadow_cond_row (c,L) lowers /\ dark_shadow_condition uppers lowers)

basic_shadow_equivalence

|- !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)

dark_shadow_row_ind

|- !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

dark_shadow_row_def

|- (dark_shadow_row c L [] = T) /\
   (dark_shadow_row c L ((d,R)::rs) =
    & d * L - & c * R >= (& c - 1) * (& d - 1) /\ dark_shadow_row c L rs)

dark_shadow_ind

|- !P.
     (!lowers. P [] lowers) /\
     (!c L uppers lowers. P uppers lowers ==> P ((c,L)::uppers) lowers) ==>
     !v v1. P v v1

dark_shadow_def

|- (dark_shadow [] lowers = T) /\
   (dark_shadow ((c,L)::uppers) lowers =
    dark_shadow_row c L lowers /\ dark_shadow uppers lowers)

nightmare_ind

|- !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

nightmare_def

|- (nightmare x c uppers lowers [] = F) /\
   (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

|- !rs x uppers lowers c.
     nightmare x c uppers lowers rs ==>
     evalupper x uppers /\ evallower x lowers

dark_shadow_FORALL

|- !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)

real_shadow_FORALL

|- !uppers lowers.
     real_shadow uppers lowers =
     !c d L R. MEM (c,L) uppers /\ MEM (d,R) lowers ==> & c * R <= & d * L

evalupper_FORALL

|- !uppers x. evalupper x uppers = !c L. MEM (c,L) uppers ==> & c * x <= L

evallower_FORALL

|- !lowers x. evallower x lowers = !d R. MEM (d,R) lowers ==> R <= & d * x

nightmare_EXISTS

|- !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)

final_equivalence

|- !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))

darkrow_implies_realrow

|- !lowers c L.
     0 < c /\ EVERY fst_nzero lowers /\ dark_shadow_row c L lowers ==>
     rshadow_row (c,L) lowers

dark_implies_real

|- !uppers lowers.
     EVERY fst_nzero uppers /\ EVERY fst_nzero lowers /\
     dark_shadow uppers lowers ==>
     real_shadow uppers lowers

alternative_equivalence

|- !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)

eval_base

|- p = ((evalupper x [] /\ evallower x []) /\ T) /\ p

eval_step_upper1

|- ((evalupper x ups /\ evallower x lows) /\ ex) /\ & c * x <= r =
   (evalupper x ((c,r)::ups) /\ evallower x lows) /\ ex

eval_step_upper2

|- ((evalupper x ups /\ evallower x lows) /\ ex) /\ & c * x <= r /\ p =
   ((evalupper x ((c,r)::ups) /\ evallower x lows) /\ ex) /\ p

eval_step_lower1

|- ((evalupper x ups /\ evallower x lows) /\ ex) /\ r <= & c * x =
   (evalupper x ups /\ evallower x ((c,r)::lows)) /\ ex

eval_step_lower2

|- ((evalupper x ups /\ evallower x lows) /\ ex) /\ r <= & c * x /\ p =
   ((evalupper x ups /\ evallower x ((c,r)::lows)) /\ ex) /\ p

eval_step_extra1

|- ((evalupper x ups /\ evallower x lows) /\ T) /\ ex' =
   (evalupper x ups /\ evallower x lows) /\ ex'

eval_step_extra2

|- ((evalupper x ups /\ evallower x lows) /\ ex) /\ ex' =
   (evalupper x ups /\ evallower x lows) /\ ex /\ ex'

eval_step_extra3

|- ((evalupper x ups /\ evallower x lows) /\ T) /\ ex' /\ p =
   ((evalupper x ups /\ evallower x lows) /\ ex') /\ p

eval_step_extra4

|- ((evalupper x ups /\ evallower x lows) /\ ex) /\ ex' /\ p =
   ((evalupper x ups /\ evallower x lows) /\ ex /\ ex') /\ p

calc_nightmare_ind

|- !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

calc_nightmare_def

|- (calc_nightmare x c [] = F) /\
   (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)

calculational_nightmare

|- !rs.
     nightmare x c uppers lowers rs =
     calc_nightmare x c rs /\ evalupper x uppers /\ evallower x lowers