Overleg gebruiker:Gereon Vienken

Require Import BenB. Definition T := R. Definition S := R. Variable V: Set. Inductive R: Set := Uit|Normaal|Ultrasnel. Variable rotatieSnelheidAs : T -> S -> B. Variable rotatieSnelheidWieken : T -> S -> B. Variable trekKoord : T -> B. Variable netSpanning : T -> S -> B. Variable spanningAdapterSchakelaar : T -> S -> B. Variable spanningSchakelaarMotor : T -> S -> B. Variable standSnelheidsSchakelaar : T -> R -> B. Definition spanning0 := 0. Definition spanning10 := 10. Definition spanning20 := 20. Definition snelheid0 := 0. Definition snelheid60 := 60. Definition snelheid120 := 120. Definition acceleratie := 10. Definition adapter := forall t:T, netSpanning t 230 -> spanningAdapterSchakelaar t 20. Definition snelheidsSchakelaar := forall t:T, spanningAdapterSchakelaar t 20 -> ( trekKoord t -> (standSnelheidsSchakelaar t Uit -> standSnelheidsSchakelaar (t+1) Normaal) /\ (standSnelheidsSchakelaar t Normaal -> standSnelheidsSchakelaar (t+1) Ultrasnel) /\ (standSnelheidsSchakelaar t Ultrasnel -> standSnelheidsSchakelaar (t+1) Uit) ) /\ ( (standSnelheidsSchakelaar t Uit -> spanningSchakelaarMotor t spanning0) /\ (standSnelheidsSchakelaar t Normaal -> spanningSchakelaarMotor t spanning10) /\ (standSnelheidsSchakelaar t Ultrasnel -> spanningSchakelaarMotor t spanning20) ). Definition motor := forall t:T, (forall s:S, (spanningSchakelaarMotor t 0 /\ (s > snelheid0) -> rotatieSnelheidAs (t+1) (s-acceleratie)) /\ (spanningSchakelaarMotor t 0 /\ (s = snelheid0) -> rotatieSnelheidAs (t+1) s ) /\ (spanningSchakelaarMotor t 10 /\ (s > snelheid60) -> rotatieSnelheidAs (t+1) (s-acceleratie)) /\ (spanningSchakelaarMotor t 10 /\ (s = snelheid60) -> rotatieSnelheidAs (t+1) s ) /\ (spanningSchakelaarMotor t 10 /\ (s < snelheid60) -> rotatieSnelheidAs (t+1) (s+acceleratie)) /\ (spanningSchakelaarMotor t 20 /\ (s = snelheid120) -> rotatieSnelheidAs (t+1) s ) /\ (spanningSchakelaarMotor t 20 /\ (s < snelheid120) -> rotatieSnelheidAs (t+1) (s+acceleratie)) ). Definition wieken := forall t:T, forall s:S, rotatieSnelheidAs t s -> rotatieSnelheidWieken t s. Definition specGeheel := forall t:T, netSpanning t 230 -> ( trekKoord t -> (standSnelheidsSchakelaar t Uit -> standSnelheidsSchakelaar (t+1) Normaal) /\ (standSnelheidsSchakelaar t Normaal -> standSnelheidsSchakelaar (t+1) Ultrasnel) /\ (standSnelheidsSchakelaar t Ultrasnel -> standSnelheidsSchakelaar (t+1) Uit) ) /\ ( ~trekKoord t /\ (forall _t:T, (_t > t /\ _t < (t+12)) -> ~trekKoord _t) -> ( (standSnelheidsSchakelaar t Uit -> rotatieSnelheidWieken (t+12) snelheid0) /\ (standSnelheidsSchakelaar t Normaal -> rotatieSnelheidWieken (t+6) snelheid60) /\ (standSnelheidsSchakelaar t Ultrasnel -> rotatieSnelheidWieken (t+12) snelheid120) ) ). Theorem correctheidsstelling : adapter /\ snelheidsSchakelaar /\ motor /\ wieken -> specGeheel. Proof. imp_i H1. unfold specGeheel. all_i _t. imp_i spanning. con_i. unfold snelheidsSchakelaar in H1. con_e1 ((standSnelheidsSchakelaar _t Uit -> spanningSchakelaarMotor _t spanning0) /\ (standSnelheidsSchakelaar _t Normaal -> spanningSchakelaarMotor _t spanning10) /\ (standSnelheidsSchakelaar _t Ultrasnel -> spanningSchakelaarMotor _t spanning20)). imp_e (spanningAdapterSchakelaar _t 20). all_e (forall t:T, (spanningAdapterSchakelaar t 20 -> (trekKoord t -> (standSnelheidsSchakelaar t Uit -> standSnelheidsSchakelaar (t + 1) Normaal) /\ (standSnelheidsSchakelaar t Normaal -> standSnelheidsSchakelaar (t + 1) Ultrasnel) /\ (standSnelheidsSchakelaar t Ultrasnel -> standSnelheidsSchakelaar (t + 1) Uit)) /\ (standSnelheidsSchakelaar t Uit -> spanningSchakelaarMotor t spanning0) /\ (standSnelheidsSchakelaar t Normaal -> spanningSchakelaarMotor t spanning10) /\ (standSnelheidsSchakelaar t Ultrasnel -> spanningSchakelaarMotor t spanning20)))_t. con_e1 (motor /\ wieken). con_e2 adapter. assumption. unfold adapter in H1. imp_e (netSpanning _t 230). all_e (forall t : T, netSpanning t 230 -> spanningAdapterSchakelaar t 20)_t. con_e1 (snelheidsSchakelaar /\ motor /\ wieken). assumption. assumption. imp_i H2. con_i. imp_i snelheid. unfold wieken in H1. imp_e (rotatieSnelheidAs (_t + 12) snelheid0). all_e (forall s:S, rotatieSnelheidAs (_t + 12) s-> rotatieSnelheidWieken (_t + 12) s) snelheid0. all_e (forall t:T, forall s:S, rotatieSnelheidAs t s-> rotatieSnelheidWieken t s) (_t + 12). con_e2 motor. con_e2 snelheidsSchakelaar. con_e2 adapter. assumption. Focus 2. con_i. unfold wieken in H1. imp_i H3. imp_e (rotatieSnelheidAs (_t + 6) (snelheid60)). all_e (forall s:S, rotatieSnelheidAs (_t + 6) s-> rotatieSnelheidWieken (_t + 6) s) snelheid60. all_e (forall t:T, forall s:S, rotatieSnelheidAs t s-> rotatieSnelheidWieken t s) (_t + 6). con_e2 motor. con_e2 snelheidsSchakelaar. con_e2 adapter. assumption. Focus 2.

imp_i H4. imp_e (rotatieSnelheidAs (_t + 12) (snelheid120)). all_e (forall s:S, rotatieSnelheidAs (_t + 12) s-> rotatieSnelheidWieken (_t + 12) s) snelheid120. all_e (forall t:T, forall s:S, rotatieSnelheidAs t s-> rotatieSnelheidWieken t s) (_t + 12). con_e2 motor. con_e2 snelheidsSchakelaar. con_e2 adapter. assumption.

all_e (forall b, rotatieSnelheidAs (_t + 12) b) snelheid120. all_i y. unfold motor in H1. replace(_t+12) with (_t+11+1). imp_e (spanningSchakelaarMotor (_t+11) 0 /\ y = snelheid0). con_e2 (spanningSchakelaarMotor (_t+11) 0 /\ y > snelheid0 -> rotatieSnelheidAs ((_t+11) + 1) (y - acceleratie)). con_e1 (spanningSchakelaarMotor (_t+11) 10 /\ y > snelheid60 -> rotatieSnelheidAs ((_t+11) + 1) (y - acceleratie)). con_e1 (spanningSchakelaarMotor (_t+11) 10 /\ y = snelheid60 -> rotatieSnelheidAs ((_t+11) + 1) y). con_e1 (spanningSchakelaarMotor (_t+11) 10 /\ y < snelheid60 -> rotatieSnelheidAs ((_t + 11)+ 1) (y + acceleratie)). con_e1 (spanningSchakelaarMotor (_t+11) 20 /\ y = snelheid120 -> rotatieSnelheidAs ((_t+11) + 1) y). con_e1 (spanningSchakelaarMotor (_t+11) 20 /\ y < snelheid120 -> rotatieSnelheidAs ((_t+11) + 1) (y + acceleratie)).

all_e (forall s : S, (((spanningSchakelaarMotor (_t + 11) 0 /\ s > snelheid0 -> rotatieSnelheidAs (_t + 11 + 1) (s - acceleratie)) /\ (spanningSchakelaarMotor (_t + 11) 0 /\ s = snelheid0 -> rotatieSnelheidAs (_t + 11 + 1) s)) /\ (spanningSchakelaarMotor (_t + 11) 10 /\ s > snelheid60 -> rotatieSnelheidAs (_t + 11 + 1) (s - acceleratie) /\ (spanningSchakelaarMotor (_t + 11) 10 /\ s = snelheid60 -> rotatieSnelheidAs (_t + 11 + 1) s) /\ (spanningSchakelaarMotor (_t + 11) 10 /\ s < snelheid60 -> rotatieSnelheidAs (_t + 11 + 1) (s + acceleratie)))) /\ (spanningSchakelaarMotor (_t + 11) 20 /\ s = snelheid120 -> rotatieSnelheidAs (_t + 11 + 1) s /\ (spanningSchakelaarMotor (_t + 11) 20 /\ s < snelheid120 -> rotatieSnelheidAs (_t + 11 + 1) (s + acceleratie)))) y.

all_e (forall t : T, (forall s : S, (((spanningSchakelaarMotor t 0 /\ s > snelheid0 -> rotatieSnelheidAs (t + 1) (s - acceleratie)) /\ (spanningSchakelaarMotor t 0 /\ s = snelheid0 -> rotatieSnelheidAs (t + 1) s)) /\ (spanningSchakelaarMotor t 10 /\ s > snelheid60 -> rotatieSnelheidAs (t + 1) (s - acceleratie) /\ (spanningSchakelaarMotor t 10 /\ s = snelheid60 -> rotatieSnelheidAs (t + 1) s) /\ (spanningSchakelaarMotor t 10 /\ s < snelheid60 -> rotatieSnelheidAs (t + 1) (s + acceleratie)))) /\ (spanningSchakelaarMotor t 20 /\ s = snelheid120 -> rotatieSnelheidAs (t + 1) s /\ (spanningSchakelaarMotor t 20 /\ s < snelheid120 -> rotatieSnelheidAs (t + 1) (s + acceleratie)))))(_t + 11).

con_e1 wieken. con_e2 snelheidsSchakelaar. con_e2 adapter. assumption.