Nuprl Theory zeno

(only non hidden objects are presented)

 COM zeno_com This theory formalizes famous Zeno paradox COM zeno_author Pavel Naumov COM zeno_date January - February 1996 COM zeno_local ~pavel/Nuprl/zeno.thy COM zeno_web http://www.cs.cornell.edu/Info/People/pavel/Nuprl/lib/zeno COM zeno_req Requires only Nuprl4.2 standard libraries COM zeno_end_com ---------------------------------- THM phole_aux n:{1...}. f:(n + 1) n. i:(n + 1). j:{(i + 1)..(n + 1)}. f i = f j THM phole_aux_ez n:{1...}. f:(n + 1) n. i:(n + 1). j:{(i + 1)..(n + 1)}. f i = f j DISP signature_df Signature{}()== Signature() Signature()== Signature() ABS signature Signature(E;T;L) == e_rel:(E E ) t_rel:(T T ) l_rel:(L L ) inst_e:(E ) time:(E T) d:(T L) t0:T t1:T def_t:(T ) (L ) THM signature_wf E,T,L:. Signature(E;T;L) ' DISP sign_e_rel_df .e_rel== < < == < ABS sign_e_rel < == s.1 THM sign_e_rel_wf E,T,L:. s:Signature(E;T;L). < E E DISP sign_t_rel_df .t_rel== < <== < ABS sign_t_rel < == s.2.1 THM sign_t_rel_wf E,T,L:. s:Signature(E;T;L). < T T DISP sign_l_rel_df .l_rel== < <== < ABS sign_l_rel < == s.2.2.1 THM sign_l_rel_wf E,T,L:. s:Signature(E;T;L). < L L DISP sign_inst_e_df .inst_e== I I== I ABS sign_inst_e I == s.2.2.2.1 THM sign_inst_e_wf E,T,L:. s:Signature(E;T;L). I E DISP sign_time_df .time== time time== time ABS sign_time time == s.2.2.2.2.1 THM sign_time_wf E,T,L:. s:Signature(E;T;L). time E T DISP sign_d_df .d== .d ABS sign_d s.d == s.2.2.2.2.2.1 THM sign_d_wf E,T,L:. s:Signature(E;T;L). s.d T L DISP sign_t0_df .t0== t0 t0== t0 ABS sign_t0 t0 == s.2.2.2.2.2.2.1 THM sign_t0_wf E,T,L:. s:Signature(E;T;L). t0 T DISP sign_t1_df .t1== .t1 ABS sign_t1 s.t1 == s.2.2.2.2.2.2.2.1 THM sign_t1_wf E,T,L:. s:Signature(E;T;L). s.t1 T DISP sign_def_t_df .def_t== Def Def== Def ABS sign_def_t Def == s.2.2.2.2.2.2.2.2.1 THM sign_def_t_wf E,T,L:. s:Signature(E;T;L). Def T DISP sign_def_l_df .def_l== Def Def== Def ABS sign_def_l Def == s.2.2.2.2.2.2.2.2.2 THM sign_def_l_wf E,T,L:. s:Signature(E;T;L). Def L ML create_signature Class Declaration for: s Signature(E;T;L) Long Name: signature Short Name: sign Parameters: E : T : L : Fields: (< ) e_rel : E E (<) t_rel : T T (sign_x_rel(s)) l_rel : L L (I) inst_e : E (time) time : E T (s.d) d : T L (t0) t0 : T (s.t1) t1 : T (Def) def_t : T (Def) def_l : L Universe: ' DISP sign_t_ref_rel_df sign_t_ref_rel()== == ABS sign_t_ref_rel == x,y.x < y x = y THM sign_t_ref_rel_wf E,T,X:. S:Signature(E;T;X). T T DISP sign_l_ref_rel_df sign_l_ref_rel()== == ABS sign_l_ref_rel == x,y.x < y x = y THM sign_l_ref_rel_wf E,T,L:. S:Signature(E;T;L). L L COM zeno_vs_jackson === stuff that Paul Jackson forgot to put into theory gen_algebra_1 == = DISP ir_connex_df IrConnex(,.)== IrConnex(,.) ABS ir_connex IrConnex(T;x,y.R[x; y]) == x,y:T. R[x; y] x = y R[x; y] THM ir_connex_wf T:. R:T T . IrConnex(T;x,y.R[x;y]) DISP ir_order_df IrOrder(,.)== IrOrder(,.) ABS ir_order IrOrder(T;x,y.R[x; y]) == Irrefl(T;x,y.R[x; y]) Trans(T;x,y.R[x; y]) THM ir_order_wf T:. R:T T . IrOrder(T;x,y.R[x;y]) DISP ir_linorder_df IrLinorder(,.) == IrLinorder(,.) ABS ir_linorder IrLinorder(T;x,y.R[x; y]) == IrConnex(T;x,y.R[x; y]) IrOrder(T;x,y.R[x; y]) THM ir_linorder_wf T:. R:T T . IrLinorder(T;x,y.R[x;y]) COM back2zeno === now back to zeno === DISP run_df Run()== Run() ABS run Run(E;T;L;S) == Order(E;e,f.e < f) IrLinorder(T;t,u.t < u) IrLinorder(L;x,y.x < y) t0 < S.t1 (r,u:T. t0 r r < u u S.t1 (S.d r) < (S.d u)) (e,f:E. I e I f (e < f (time e) < (time f))) (e:E. n:. w:{f:E| f < e} n. Inj({f:E| f < e} ;n;w)) Def t0 (r:T. t0 r r S.t1 Def r Def (S.d r)) THM run_wf E,T,X:. S:Signature(E;T;X). Run(E;T;X;S) DISP concurrent_df concurrent{}() == || || == || ABS concurrent S1 || S2 == < = < < = < < = < I = I time = time Def = Def Def = Def THM concurrent_wf E,T,L:. S1,S2:Signature(E;T;L). S1 || S2 ' DISP race_df race{}() == == ABS race Ach Tor == Ach || Tor t0 = t0 (Tor.t1 < Ach.t1 (t:T (t0 < t t Ach.t1 Ach.d t = Tor.d t (s:T. t0 s s < t (Ach.d s) < (Tor.d s))) Def t)) THM race_wf E,T,X:. Ach,Tor:Signature(E;T;X). Ach Tor ' DISP ivp_df IVP()== IVP() IVP()== IVP() ABS ivp IVP(S) == b,e:T. a:L. t0 b b < e e S.t1 (S.d b) < a a < (S.d e) Def b Def a Def e (t:T. b < t t < e S.d t = a Def t) THM ivp_wf E,T,L:. S:Signature(E;T;L). IVP(S) THM successor E,T,L:. Ach,Tor:Signature(E;T;L). u,w:T. Run(E;T;L;Ach) Run(E;T;L;Tor) Ach Tor IVP(Ach) Ach.d w = Tor.d w t0 u u < w (w Ach.t1 w Tor.t1) (Ach.d u) < (Tor.d u) Def u Def w (v:T. u < v v < w Def v) THM successor_ez E,T,L:. Ach,Tor:Signature(E;T;L). u,w:T. Run(E;T;L;Ach) Run(E;T;L;Tor) Ach Tor IVP(Ach) Ach.d w = Tor.d w t0 u u < w (w Ach.t1 w Tor.t1) (Ach.d u) < (Tor.d u) Def u Def w (v:T. u < v v < w Def v) THM sequence E,T,L:. Ach,Tor:Signature(E;T;L). w:T. Run(E;T;L;Ach) Run(E;T;L;Tor) Ach Tor IVP(Ach) Ach.d w = Tor.d w t0 < w (w Ach.t1 w Tor.t1) (s:T. t0 s s < w (Ach.d s) < (Tor.d s)) Def w (n: v:n T t0 = v 0 (i:(n - 1). (v i) < (v (i + 1))) (i:n. (v i) < w Def (v i) t0 (v i))) THM sequence_ez E,T,L:. Ach,Tor:Signature(E;T;L). w:T. Run(E;T;L;Ach) Run(E;T;L;Tor) Ach Tor IVP(Ach) Ach.d w = Tor.d w t0 < w (w Ach.t1 w Tor.t1) (s:T. t0 s s < w (Ach.d s) < (Tor.d s)) Def w (n: v:n T t0 = v 0 (i:(n - 1). (v i) < (v (i + 1))) (i:n. (v i) < w Def (v i) t0 (v i))) THM mult_trans T:. R:T T . n:{2...}. v:n T. Trans(T;x,y.x R y) (i:(n - 1). (v i) R (v (i + 1))) (v 0) R (v (n - 1)) THM mult_trans_ez T:. R:T T . n:{2...}. v:n T. Trans(T;x,y.x R y) (i:(n - 1). (v i) R (v (i + 1))) (v 0) R (v (n - 1)) DISP tep_df TEP()== TEP TEP== TEP ABS tep TEP == t:T. e:E. Def t I e t = time e THM tep_wf E,T,L:. S:Signature(E;T;L). TEP THM sign_t_ref_rel_trans E,T,L:. S:Signature(E;T;L). u,v,w:T. Run(E;T;L;S) u v v w u w THM sign_t_ref_rel_trans_ez E,T,L:. S:Signature(E;T;L). u,v,w:T. Run(E;T;L;S) u v v w u w THM paradox E,T,L:. Ach,Tor:Signature(E;T;L). (Run(E;T;L;Ach) Run(E;T;L;Tor)) Ach Tor Ach.t1 Tor.t1 IVP(Ach) TEP THM paradox_ez E,T,L:. Ach,Tor:Signature(E;T;L). (Run(E;T;L;Ach) Run(E;T;L;Tor)) Ach Tor Ach.t1 Tor.t1 IVP(Ach) TEP