$$$top.pvs top: THEORY BEGIN IMPORTING abstraction END top $$$mutheorems.pvs mutheorems[T : TYPE]: THEORY BEGIN IMPORTING mucalculus[T], connectives[T] f,g,h: VAR pred[T] refl: LEMMA f <= f antisym: LEMMA f <= g AND g <= f IMPLIES f =g trans: LEMMA f <= g AND g <= h IMPLIES f <= h AND_comm: LEMMA (f AND g) = (g AND f) AND_assoc: LEMMA (f AND (g AND h)) = ((f AND g) AND h) OR_comm: LEMMA (f OR g) = (g OR f) OR_assoc: LEMMA (f OR (g OR h)) = ((f OR g) OR h) AND_OR_dist: LEMMA (f AND (g OR h)) = ((f AND g) OR (f AND h)) lem1: LEMMA (f <= (g AND h)) = ((f <= g) AND (f <= h)) lem2: LEMMA (f AND g) <= f lem3: LEMMA f <= (f OR g) lem4: LEMMA (f OR g) <= g IMPLIES f <= g lem5: LEMMA ((f <= h) AND (g <= h)) = ((f OR g) <= h) F: VAR pred[pred[T]] glb_min: THEOREM member(f,F) IMPLIES glb(F) <= f glb_max: THEOREM (FORALL g: member(g,F) IMPLIES f <= g) IMPLIES f <= glb(F) lub_max: THEOREM member(f,F) IMPLIES f <= lub(F) lub_min: THEOREM (FORALL g: member(g,F) IMPLIES g <= f) IMPLIES lub(F) <= f ff: VAR [pred[T]->pred[T]] lfp_lem1: LEMMA (ff(f) = f) IMPLIES (lfp(ff) <= f) lfp_lem2: LEMMA ismono(ff) IMPLIES FORALL f: ff(f) <= f IMPLIES ff(glb(LAMBDA f: ff(f) <= f)) <= f lfp_thm: THEOREM ismono(ff) IMPLIES ff(lfp(ff)) <= lfp(ff) lfp_thm1: THEOREM ismono(ff) IMPLIES lfp(ff) <= ff(lfp(ff)) lfp_thm2: THEOREM ismono(ff) IMPLIES (ff(lfp(ff)) = lfp(ff)) lfp_lem3: LEMMA ismono(ff) IMPLIES FORALL f: ff(f) <= f IMPLIES lfp(ff) <= f lfp_is_lfp: THEOREM ismono(ff) IMPLIES islfp(ff,lfp(ff)) gfp_lem1: LEMMA ff(f) = f IMPLIES f <= gfp(ff) gfp_lem2: LEMMA ismono(ff) IMPLIES (FORALL f: f <= ff(f) IMPLIES f <= ff(lub(LAMBDA f: f <= ff(f) ))) gfp_thm1: THEOREM ismono(ff) IMPLIES gfp(ff) <= ff(gfp(ff)) gfp_thm: THEOREM ismono(ff) IMPLIES ff(gfp(ff)) <= gfp(ff) gfp_thm2: THEOREM ismono(ff) IMPLIES (ff(gfp(ff)) = gfp(ff)) gfp_lem3: LEMMA ismono(ff) IMPLIES FORALL f: f <= ff(f) IMPLIES f <= gfp(ff) gfp_is_gfp: THEOREM ismono(ff) IMPLIES isgfp(ff,gfp(ff)) END mutheorems $$$mutheorems.prf (|mutheorems| (|refl| "" (TCC) NIL) (|antisym| "" (SKOSIMP) (("" (APPLY-EXTENSIONALITY) (("" (TCC) NIL))))) (|trans| "" (TCC) NIL) (|AND_comm| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY) (("" (TCC) NIL))))) (|AND_assoc| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY) (("" (TCC) NIL))))) (|OR_comm| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY) (("" (TCC) NIL))))) (|OR_assoc| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY) (("" (TCC) NIL))))) (|AND_OR_dist| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY) (("" (TCC) NIL))))) (|lem1| "" (TCC) NIL) (|lem2| "" (TCC) NIL) (|lem3| "" (TCC) NIL) (|lem4| "" (TCC) NIL) (|lem5| "" (TCC) NIL) (|glb_min| "" (TCC) NIL) (|glb_max| "" (SKOSIMP) (("" (EXPAND "member") (("" (EXPAND "<=") (("" (EXPAND "glb") (("" (SKOLEM!) (("" (FLATTEN) (("" (SKOLEM!) (("" (EXPAND "member") (("" (INST -1 "p!1") (("" (FLATTEN) (("" (ASSERT) (("" (INST?) (("" (ASSERT) NIL))))))))))))))))))))))))) (|lub_max| "" (TCC) NIL) (|lub_min| "" (SKOSIMP) (("" (AUTO-REWRITE-THEORY "mucalculus[T]") (("" (ASSERT) (("" (SKOSIMP) (("" (SKOLEM!) (("" (INST?) (("" (TCC) NIL))))))))))))) (|lfp_lem1| "" (TCC) NIL) (|lfp_lem2| "" (SKOSIMP) (("" (EXPAND "ismono") (("" (SKOSIMP) (("" (LEMMA "glb_min") (("" (INST -1 "LAMBDA (f: pred[T]): (ff!1(f) <= f)" "f!1") (("" (EXPAND "member") (("" (INST -2 "glb(LAMBDA (f: pred[T]): (ff!1(f) <= f))" "f!1") (("" (BDDSIMP) (("" (LEMMA "trans") (("" (INST -1 "ff!1(glb(LAMBDA (f: pred[T]): (ff!1(f) <= f)))" "ff!1(f!1)" "f!1") (("" (ASSERT) NIL))))))))))))))))))))) (|lfp_thm| "" (SKOSIMP) (("" (EXPAND "lfp") (("" (LEMMA "lfp_lem2") (("" (INST?) (("" (ASSERT) (("" (LEMMA "glb_max") (("" (EXPAND "member") (("" (INST -1 "LAMBDA (f: pred[T]): (ff!1(f) <= f)" "ff!1(glb(LAMBDA (f: pred[T]): (ff!1(f) <= f)))") (("" (BETA) (("" (ASSERT) NIL))))))))))))))))))) (|lfp_thm1| "" (SKOSIMP) (("" (LEMMA "glb_min") (("" (INST -1 "LAMBDA (f: pred[T]): (ff!1(f) <= f)" "ff!1(lfp(ff!1))") (("" (EXPAND "member") (("" (EXPAND "lfp") (("" (LEMMA "lfp_thm") (("" (INST?) (("" (ASSERT) (("" (EXPAND "ismono") (("" (EXPAND "lfp") (("" (INST -2 "ff!1(glb(LAMBDA (p: pred[T]): (ff!1(p) <= p)))" "glb(LAMBDA (p: pred[T]): (ff!1(p) <= p))") (("" (ASSERT) NIL))))))))))))))))))))))) (|lfp_thm2| "" (SKOLEM!) (("" (LEMMA "lfp_thm1") (("" (INST?) (("" (BDDSIMP) (("" (LEMMA "lfp_thm") (("" (INST?) (("" (BDDSIMP) (("" (LEMMA "antisym") (("" (INST -1 "ff!1(lfp(ff!1))" "lfp(ff!1)") (("" (ASSERT) NIL))))))))))))))))))) (|lfp_lem3| "" (SKOSIMP*) (("" (LEMMA "lfp_lem2") (("" (INST?) (("" (PROP) (("" (INST?) (("" (REWRITE "lfp_thm2" :DIR RL) (("" (EXPAND "lfp") (("" (PROP) NIL))))))))))))))) (|lfp_is_lfp| "" (SKOSIMP) (("" (EXPAND "islfp") (("" (EXPAND "isfix") (("" (LEMMA "lfp_thm2") (("" (INST?) (("" (LEMMA "lfp_lem1") (("" (INST?) (("" (BDDSIMP) (("" (SKOLEM!) (("" (LEMMA "lfp_lem1") (("" (INST -1 "p2!1" "ff!1") NIL))))))))))))))))))))) (|gfp_lem1| "" (GRIND) NIL) (|gfp_lem2| "" (SKOSIMP*) (("" (EXPAND "ismono") (("" (LEMMA "lub_max") (("" (INST -1 "LAMBDA (f: pred[T]): f <= ff!1(f)" "f!1") (("" (EXPAND "member") (("" (INST -2 "f!1" "lub(LAMBDA (f: pred[T]): (f <= ff!1(f)))") (("" (PROP) (("" (LEMMA "trans") (("" (INST -1 "f!1" "ff!1(f!1)" "ff!1(lub(LAMBDA (f: pred[T]): (f <= ff!1(f) )))") (("" (PROP) NIL))))))))))))))))))) (|gfp_thm1| "" (SKOSIMP) (("" (EXPAND "gfp") (("" (LEMMA "gfp_lem2") (("" (INST?) (("" (ASSERT) (("" (INST?) (("" (PROP) (("" (LEMMA "lub_min") (("" (INST?) (("" (EXPAND "member") (("" (HIDE 2 3) (("" (SKOSIMP*) (("" (LEMMA "lub_max") (("" (INST?) (("" (INST?) (("" (EXPAND "member") (("" (PROP) (("" (EXPAND "ismono") (("" (INST?) (("" (ASSERT) (("" (HIDE -1) (("" (FORWARD-CHAIN "trans") NIL))))))))))))))))))))))))))))))))))))))))))) (|gfp_thm| "" (SKOSIMP*) (("" (LEMMA "lub_max") (("" (INST -1 "LAMBDA (f: pred[T]): (f <= ff!1(f))" "ff!1(gfp(ff!1))") (("" (EXPAND "member") (("" (EXPAND "gfp") (("" (PROP) (("" (LEMMA "gfp_thm1") (("" (EXPAND "gfp") (("" (INST?) (("" (PROP) (("" (EXPAND "ismono") (("" (INST?) (("" (PROP) NIL))))))))))))))))))))))))) (|gfp_thm2| "" (SKOSIMP*) (("" (LEMMA "gfp_thm") (("" (INST?) (("" (LEMMA "gfp_thm1") (("" (INST?) (("" (LEMMA "antisym") (("" (INST?) (("" (PROP) NIL))))))))))))))) (|gfp_lem3| "" (SKOSIMP*) (("" (LEMMA "gfp_lem2") (("" (INST?) (("" (PROP) (("" (INST?) (("" (REWRITE "gfp_thm2" :DIR RL) (("" (EXPAND "gfp") (("" (PROP) NIL))))))))))))))) (|gfp_is_gfp| "" (SKOSIMP*) (("" (EXPAND "isgfp") (("" (EXPAND "isfix") (("" (USE "gfp_thm2") (("" (USE "gfp_lem1") (("" (PROP) (("" (SKOSIMP*) (("" (USE "gfp_lem1") (("" (PROP) NIL)))))))))))))))))) $$$more_mucalculus_theorems.pvs more_mucalculus_theorems[T:TYPE]: THEORY %Contains definitions of union and intersection continuity along %with proof that the iterated fixpoint of a union-continuous %predicate transformer least BEGIN IMPORTING mucalculus[T], mutheorems[T] q : VAR sequence[PRED[T]] r, s: VAR T Q, P, f, g, p,p1,p2: VAR pred[T] N: VAR [T, T->bool] predtt: TYPE = [pred[T]->pred[T]] pp, qq: VAR predtt setofpred: VAR pred[pred[T]] %ascending/descending sequences of predicates ascends?(q): bool = ascends?(q, <=) descends?(q): bool = descends?(q, <=) %pp(Uq) = U(pp(q)), q ascending U_continuous?(pp): bool = (FORALL (q: (ascends?)) : pp(lub({p | EXISTS (i : nat): p = q(i)})) = lub({p | EXISTS (i : nat) : p = pp(q(i))})) %pp(/\q) = /\pp(q), q descending I_continuous?(pp) : bool = (FORALL (q: (descends?)) : pp(glb({p | EXISTS (i : nat): p = q(i)})) = glb({p | EXISTS (i : nat) : p = pp(q(i))})) U_continuity_implies_monotonicity: LEMMA U_continuous?(pp) IMPLIES ismono(pp) I_continuity_implies_monotonicity: LEMMA I_continuous?(pp) IMPLIES ismono(pp) %pp(pp^{i}(p)) = pp^{i+1}(p) iterate_step: LEMMA (FORALL (i:nat): pp(iterate(pp, i)(p)) = iterate(pp, i+1)(p)) %Mu is iterated fixpoint Mu(pp)(s): bool = lub({p | (EXISTS (j:nat): p = iterate(pp, j)(emptyset[T]))})(s) %For U_continuous pp, iterated fixpoint is the least fixpoint Mu_mu: LEMMA (FORALL (pp: (U_continuous?)): Mu(pp) = mu(pp)) %remaining lemmas are useful but not hard. mu_monot: LEMMA ismono(pp) AND ismono(qq) AND (FORALL p: pp(p) <= qq(p)) IMPLIES mu(pp) <= mu(qq) nu_mu: LEMMA ismono(pp) IMPLIES nu(pp) = NOT mu(LAMBDA p: NOT pp(NOT p)) Pp, Qq : VAR (ismono) mu_induction: LEMMA ismono(pp) AND (FORALL s: pp(Q)(s) IMPLIES Q(s)) IMPLIES (FORALL s: mu(pp)(s) IMPLIES Q(s)) END more_mucalculus_theorems $$$more_mucalculus_theorems.prf (|more_mucalculus_theorems| (|U_continuity_implies_monotonicity| "" (SKOSIMP*) (("" (EXPAND "U_continuous?") (("" (EXPAND "ismono") (("" (SKOSIMP*) (("" (NAME "QQ" "LAMBDA (i:nat): IF i = 0 THEN p1!1 ELSE p2!1 ENDIF") (("" (CASE "lub({p | EXISTS (i : nat) : p = QQ(i)}) = p2!1") (("1" (INST - "QQ") (("1" (REPLACE -1) (("1" (REPLACE -3) (("1" (EXPAND "<=" +) (("1" (SKOSIMP*) (("1" (EXPAND "lub" +) (("1" (INST + "pp!1(p1!1)") (("1" (PROP) (("1" (EXPAND "member") (("1" (INST + 0) (("1" (REPLACE -2 :DIR RL) (("1" (GROUND) NIL))))))))))))))))))))) ("2" (EXPAND "ascends?") (("2" (EXPAND "ascends?") (("2" (EXPAND "preserves") (("2" (SKOSIMP*) (("2" (REPLACE -3 :DIR RL) (("2" (HIDE -2 -3) (("2" (GRIND) NIL))))))))))))))) ("2" (ASSERT) (("2" (GROUND) (("2" (HIDE -2 2) (("2" (EXPAND "lub") (("2" (APPLY-EXTENSIONALITY) (("2" (HIDE 2) (("2" (IFF) (("2" (PROP) (("1" (SKOSIMP) (("1" (EXPAND "<=") (("1" (INST?) (("1" (PROP) (("1" (EXPAND "member") (("1" (SKOSIMP) (("1" (CASE "i!1 = 0") (("1" (REPLACE -4 :DIR RL) (("1" (ASSERT) NIL))) ("2" (REPLACE -3 :DIR RL) (("2" (GROUND) NIL))))))))))))))))) ("2" (INST + "p2!1") (("2" (PROP) (("2" (EXPAND "member") (("2" (INST + 2) (("2" (REPLACE -2 :DIR RL) (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))) (|I_continuity_implies_monotonicity| "" (SKOSIMP*) (("" (EXPAND "I_continuous?") (("" (EXPAND "ismono") (("" (SKOSIMP*) (("" (NAME "QQ" "LAMBDA (i:nat): IF i = 0 THEN p2!1 ELSE p1!1 ENDIF") (("" (CASE "glb({p | EXISTS (i : nat) : p = QQ(i)}) = p1!1") (("1" (INST - "QQ") (("1" (REPLACE -1) (("1" (REPLACE -3) (("1" (HIDE -1 -3) (("1" (EXPAND "glb") (("1" (EXPAND "<=") (("1" (SKOSIMP*) (("1" (INST -3 "pp!1(p2!1)") (("1" (PROP) (("1" (EXPAND "member") (("1" (INST + 0) (("1" (REPLACE -1 :DIR RL) (("1" (BETA) (("1" (ASSERT) NIL))))))))))))))))))))))))) ("2" (EXPAND "descends?") (("2" (EXPAND "descends?") (("2" (EXPAND "inverts") (("2" (SKOSIMP) (("2" (REPLACE -3 :DIR RL) (("2" (BETA) (("2" (LIFT-IF) (("2" (GROUND) (("1" (EXPAND "<=" 1) (("1" (SKOSIMP*) NIL))) ("2" (LIFT-IF) (("2" (GROUND) (("2" (EXPAND "<=" 2) (("2" (SKOSIMP*) NIL))))))))))))))))))))))))) ("2" (HIDE -2 2) (("2" (EXPAND "glb") (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (IFF) (("2" (PROP) (("1" (INST - "p1!1") (("1" (EXPAND "member") (("1" (PROP) (("1" (INST + 1) (("1" (REPLACE -1 :DIR RL) (("1" (ASSERT) NIL))))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "member") (("2" (SKOSIMP*) (("2" (CASE "i!1 = 0") (("1" (REPLACE -4 :DIR RL) (("1" (ASSERT) (("1" (EXPAND "<=") (("1" (INST?) (("1" (ASSERT) NIL))))))))) ("2" (REPLACE -3 :DIR RL) (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))) (|iterate_step| "" (INDUCT-AND-REWRITE! "i") NIL) (|Mu_mu| "" (SKOSIMP*) (("" (CASE "Mu(pp!1) <= mu(pp!1)") (("1" (CASE "mu(pp!1) <= Mu(pp!1)") (("1" (APPLY-EXTENSIONALITY) (("1" (HIDE 2) (("1" (EXPAND "<=") (("1" (INST?) (("1" (INST?) (("1" (IFF) (("1" (PROP) NIL))))))))))))) ("2" (HIDE -1 2) (("2" (TYPEPRED "pp!1") (("2" (FORWARD-CHAIN "U_continuity_implies_monotonicity") (("2" (EXPAND "U_continuous?") (("2" (INST - "(LAMBDA (i:nat): iterate(pp!1, i)(emptyset[T]))") (("1" (CASE-REPLACE "lub({p: pred[T] | EXISTS (i: nat): p = pp!1((LAMBDA (i: nat): iterate(pp!1, i)(emptyset[T]))(i))}) = lub({p: pred[T] | EXISTS (i: nat): p = (LAMBDA (i: nat): iterate(pp!1, i)(emptyset[T]))(i)})") (("1" (HIDE -1) (("1" (FORWARD-CHAIN "lfp_lem1") (("1" (HIDE -3) (("1" (EXPAND "lfp") (("1" (EXPAND "mu") (("1" (EXPAND "Mu") (("1" (CASE-REPLACE "(LAMBDA (s): lub({p: pred[T] | (EXISTS (j: nat): p = iterate(pp!1, j)(emptyset[T]))})(s)) = lub({p: pred[T] | EXISTS (i: nat): p = iterate(pp!1, i)(emptyset[T])})") (("1" (HIDE -1 2) (("1" (EXPAND "lfp") (("1" (PROPAX) NIL))))) ("2" (APPLY-EXTENSIONALITY) NIL))))))))))))))) ("2" (HIDE -2 2) (("2" (EXPAND "lub") (("2" (APPLY-EXTENSIONALITY) (("2" (HIDE 2) (("2" (IFF) (("2" (PROP) (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (SKOSIMP*) (("1" (INST?) (("1" (REWRITE "iterate_step") (("1" (PROP) (("1" (INST + "i!1 + 1") (("1" (ASSERT) NIL))))))))))))))) ("2" (SKOSIMP*) (("2" (EXPAND "member") (("2" (SKOSIMP*) (("2" (INST?) (("2" (PROP) (("2" (CASE "i!1 = 0") (("1" (GRIND) NIL) ("2" (INST + "i!1 - 1") (("1" (REWRITE "iterate_step") NIL) ("2" (ASSERT) NIL))))))))))))))))))))))))))))) ("2" (HIDE 2) (("2" (EXPAND "ascends?") (("2" (EXPAND "ascends?") (("2" (EXPAND "preserves") (("2" (INDUCT "x1") (("1" (GRIND) NIL) ("2" (SKOSIMP*) (("2" (SIMPLIFY-WITH-REWRITES :DEFS T) (("2" (SKOSIMP*) (("2" (INST - "x2!1 - 1") (("2" (INST - "(iterate(pp!1, j!1)(emptyset[T]))" "(iterate(pp!1, x2!1 - 1)(emptyset[T]))") (("2" (GRIND) NIL))))))))))))))))))))))))))))))))) ("2" (HIDE 2) (("2" (EXPAND "Mu") (("2" (TYPEPRED "pp!1") (("2" (FORWARD-CHAIN "U_continuity_implies_monotonicity") (("2" (EXPAND "<=") (("2" (CASE "(FORALL (i:nat), p: p<= mu(pp!1) IMPLIES iterate(pp!1, i)(p) <= mu(pp!1))") (("1" (SKOSIMP*) (("1" (EXPAND "lub") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (SKOSIMP*) (("1" (INST?) (("1" (PROP) (("1" (EXPAND "<=") (("1" (INST?) (("1" (GROUND) NIL))))) ("2" (EXPAND "<=") (("2" (HIDE -1 -2 -3 2) (("2" (GRIND) NIL))))))))))))))))))) ("2" (HIDE 2) (("2" (INDUCT "i") (("1" (GRIND) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "iterate" +) (("2" (INST?) (("2" (PROP) (("2" (FORWARD-CHAIN "lfp_thm2") (("2" (EXPAND "mu") (("2" (EXPAND "lfp") (("2" (REPLACE -1 1 RL) (("2" (EXPAND "ismono") (("2" (INST?) (("2" (PROP) NIL))))))))))))))))))))))))))))))))))))))))) (|mu_monot| "" (SKOSIMP*) (("" (EXPAND "mu") (("" (LEMMA "lfp_lem3") (("" (INST - "pp!1") (("" (PROP) (("" (INST - "lfp(qq!1)") (("" (REWRITE "lfp_thm2" :DIR RL) (("" (INST?) (("" (PROP) (("" (LEMMA "lfp_thm2") (("" (INST?) (("" (GROUND) NIL))))))))))))))))))))))) (|nu_mu| "" (SKOSIMP*) (("" (EXPAND "mu") (("" (EXPAND "nu") (("" (EXPAND "lfp") (("" (APPLY-EXTENSIONALITY) (("" (HIDE 2) (("" (EXPAND "glb") (("" (IFF) (("" (PROP) (("1" (EXPAND "NOT") (("1" (EXPAND "gfp") (("1" (EXPAND "lub") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (INST - "NOT gfp(pp!1)") (("1" (PROP) (("1" (EXPAND "NOT") (("1" (EXPAND "gfp") (("1" (EXPAND "lub") (("1" (INST?) (("1" (HIDE -3) (("1" (GRIND) NIL))))))))))) ("2" (EXPAND "<=" +) (("2" (SKOSIMP*) (("2" (EXPAND "NOT") (("2" (FORWARD-CHAIN "gfp_thm1") (("2" (EXPAND "<=") (("2" (INST?) (("2" (REPLACE-ETA "gfp(pp!1)") (("2" (PROP) NIL))))))))))))))))))))))))))))) ("2" (EXPAND "gfp") (("2" (EXPAND "lub") (("2" (EXPAND "NOT") (("2" (SKOSIMP*) (("2" (INST + "NOT lfp(LAMBDA p: NOT pp!1(NOT p))") (("2" (PROP) (("1" (EXPAND "member") (("1" (LEMMA "lfp_thm") (("1" (INST - "(LAMBDA p: NOT pp!1(NOT p))") (("1" (PROP) (("1" (HIDE -2 -3) (("1" (EXPAND "<=") (("1" (SKOSIMP*) (("1" (INST?) (("1" (EXPAND "NOT") (("1" (PROP) NIL))))))))))) ("2" (HIDE -1 2) (("2" (EXPAND "ismono") (("2" (SKOSIMP*) (("2" (INST - "NOT p2!1" "NOT p1!1") (("2" (PROP) (("1" (EXPAND "<=") (("1" (SKOSIMP*) (("1" (INST?) (("1" (EXPAND "NOT") (("1" (PROP) NIL))))))))) ("2" (EXPAND "NOT") (("2" (EXPAND "<=") (("2" (SKOSIMP*) (("2" (INST?) (("2" (PROP) NIL))))))))))))))))))))))))))) ("2" (EXPAND "member") (("2" (EXPAND "NOT" +) (("2" (EXPAND "lfp") (("2" (EXPAND "glb") (("2" (INST?) (("2" (EXPAND "member") (("2" (PROP) NIL))))))))))))))))))))))))))))))))))))))))))) (|mu_induction| "" (SKOSIMP*) (("" (EXPAND "mu") (("" (LEMMA "lfp_lem3") (("" (EXPAND "<=") (("" (GRIND) NIL)))))))))) $$$connectives.pvs connectives [ T: TYPE ] : THEORY %This theory contains the Boolean connectives lifted to %predicates. BEGIN f, g: VAR pred[T] u,v,w: VAR T AND(f,g)(u):bool = f(u) AND g(u); OR(f,g)(u):bool = f(u) OR g(u) NOT(f)(u):bool = NOT f(u); IMPLIES(f,g)(u):bool = f(u) IMPLIES g(u); IFF(f,g)(u):bool = f(u) IFF g(u); TRUE(u) : bool = TRUE; FALSE(u) : bool = FALSE; END connectives $$$mucalculus.pvs % Defines fixpoints: parent of ctlops theory mucalculus[T:TYPE]: THEORY BEGIN s: VAR T p,p1,p2: VAR pred[T] predtt: TYPE = [pred[T]->pred[T]] pp: VAR predtt setofpred: VAR pred[pred[T]] IMPORTING orders[pred[T]] <=(p1,p2):bool = FORALL s: p1(s) IMPLIES p2(s) ismono(pp):bool = FORALL p1,p2: p1 <= p2 IMPLIES pp(p1) <= pp(p2) isfix (pp,p):bool = (pp(p) = p) glb (setofpred):pred[T] = LAMBDA s: (FORALL p: member(p,setofpred) IMPLIES p(s)) % least fixpoint lfp (pp):pred[T] = glb({p | pp(p) <= p}) mu(pp): pred[T] = lfp(pp) islfp (pp,p1):bool = isfix (pp,p1) AND FORALL p2: isfix (pp,p2) IMPLIES p1 <= p2 lub (setofpred):pred[T] = LAMBDA s: EXISTS p: member(p,setofpred) AND p(s) % greatest fixpoint gfp (pp):pred[T] = lub({p | p <= (pp(p))}) nu (pp):pred[T] = gfp(pp) isgfp (pp,p1):bool = isfix (pp,p1) AND FORALL p2: isfix (pp,p2) IMPLIES p2 <= p1 END mucalculus $$$ctlops.pvs ctlops[state : TYPE]: THEORY %Basic CTL temporal operators (without fairness) %defined in mu-calculus BEGIN IMPORTING mucalculus[state], connectives[state] u,v,w: VAR state f,g,Q,P,p1,p2: VAR pred[state] Z: VAR pred[[state, state]] N: VAR [state, state->bool] EX(N,f)(u):bool = (EXISTS v: (f(v) AND N(u, v))) EG(N,f):pred[state] = nu (LAMBDA Q: (f AND EX(N,Q))) EU(N,f,g):pred[state] = mu (LAMBDA Q: (g OR (f AND EX(N,Q)))) % Other operator definitions EF(N,f):pred[state] = EU(N,(LAMBDA u: TRUE),f) AX(N,f):pred[state] = NOT EX(N, NOT f) AF(N,f):pred[state] = NOT EG(N, NOT f) AG(N,f):pred[state] = NOT EF(N, NOT f) AU(N,f,g):pred[state] = NOT EU(N, NOT g, (NOT f AND NOT g)) AND AF(N,g) END ctlops fairctlops [ state : TYPE ]: THEORY %Fair versions of CTL operators where %fairAG(N, f)(Ff)(s) means f always holds along every N-path %from s along which the fairness predicate Ff holds infinitely %often. This is different from the usual linear-time notion of %fairness where the strong form asserts that if an action A is %enabled infinitely often, it is taken infinitely often, and the %weak form asserts that if any action that is continuously enabled %is taken infinitely often. BEGIN IMPORTING ctlops[state] u,v,w: VAR state f,g,Q,P,p1,p2: VAR pred[state] N: VAR [state, state->bool] Ff: VAR pred[state] % Fair formula fairEG(N, f)(Ff): pred[state] = nu(LAMBDA P: EU(N, f, f AND Ff AND EX(N, P))) fairAF(N,f)(Ff):pred[state] = NOT fairEG(N, NOT f)(Ff) fair?(N,Ff):pred[state] = fairEG(N,LAMBDA u: TRUE)(Ff) fairEX(N,f)(Ff):pred[state] = EX(N,f AND fair?(N,Ff)) fairEU(N,f,g)(Ff):pred[state] = EU(N,f,g AND fair?(N,Ff)) fairEF(N,f)(Ff):pred[state] = EF(N,f AND fair?(N,Ff)) fairAX(N,f)(Ff):pred[state] = NOT fairEX(N, NOT f)(Ff) fairAG(N,f)(Ff):pred[state] = NOT fairEF(N,NOT f)(Ff) fairAU(N,f,g)(Ff):pred[state] = NOT fairEU(N,NOT g,NOT f AND NOT g)(Ff) AND fairAF(N,g)(Ff) END fairctlops Fairctlops [ state : TYPE ]: THEORY %Fair versions of CTL operators with lists of fairness conditions. %FairAG(N,f)(Fflist)(s) means f always holds on every N-path from %s along which each predicate in Fflist holds infinitely often. BEGIN IMPORTING ctlops[state] u,v,w: VAR state f,g,Q,P,p1,p2: VAR pred[state] N: VAR [state, state->bool] Fflist, Gflist: VAR list[pred[state]] % Fair formula CheckFair(Q, N, f, Fflist): RECURSIVE pred[state] = (CASES Fflist OF cons(Ff, Gflist): EU(N, f, f AND Ff AND EX(N, CheckFair(Q, N, f, Gflist))), null : Q ENDCASES) MEASURE length(Fflist) FairEG(N, f)(Fflist): pred[state] = nu(LAMBDA P: CheckFair(P, N, f, Fflist)) FairAF(N,f)(Fflist):pred[state] = NOT FairEG(N, NOT f)(Fflist) Fair?(N,Fflist):pred[state] = FairEG(N,LAMBDA u: TRUE)(Fflist) FairEX(N,f)(Fflist):pred[state] = EX(N,f AND Fair?(N,Fflist)) FairEU(N,f,g)(Fflist):pred[state] = EU(N,f,g AND Fair?(N,Fflist)) FairEF(N,f)(Fflist):pred[state] = EF(N,f AND Fair?(N,Fflist)) FairAX(N,f)(Fflist):pred[state] = NOT FairEX(N, NOT f)(Fflist) FairAG(N,f)(Fflist):pred[state] = NOT FairEF(N,NOT f)(Fflist) FairAU(N,f,g)(Fflist):pred[state] = NOT FairEU(N,NOT g,NOT f AND NOT g)(Fflist) AND FairAF(N,g)(Fflist) END Fairctlops $$$ctlthms.pvs ctlthms [T : TYPE ] : THEORY %This theory contains some useful theorems about CTL %operators. Currently, only the AG operator is considered %but theorems abot other operators will also be included. BEGIN IMPORTING ctlops[T], more_mucalculus_theorems[T] u,v,w: VAR T f,g,Q,P,p1,p2, I: VAR pred[T] F, G, Z: VAR pred[[T, T]] %<= ordering on binary (next-state) predicates <=(F, G): bool = (FORALL u, v: F(u, v) IMPLIES G(u, v)) %de Morgan law for unary predicates. deMorgan: LEMMA ((NOT f) AND (NOT g)) = NOT (f OR g) %Contraposition for unary predicates. contrapose: LEMMA (NOT g) <= (NOT f) = (f <= g) %AG TRUE always holds. AG_true: LEMMA AG(F, (LAMBDA u: TRUE))(v) %AG is contravariant in next-state argument, and covariant %in formula argument. AG_variance: LEMMA G <= F AND f <= g IMPLIES AG(F, f) <= AG(G, g) %Restricts a next-state relation F to pre/post states %satisfying an invariant I (write as F/I). restrict(F, I)(u, v): bool = (I(u) AND I(v) AND F(u, v)) %If AG f holds in F/I and AG I holds in F, then AG f holds in F. AG_invariance: LEMMA (AG(F, I) AND AG(restrict(F, I), f)) <= AG(F, f) END ctlthms $$$ctlthms.prf (|ctlthms| (|deMorgan| "" (GRIND) (("" (EXPAND* "NOT" "AND" "OR") (("" (APPLY-EXTENSIONALITY) (("" (BDDSIMP) (("" (PROPAX) NIL))))))))) (|contrapose| "" (GRIND) NIL) (|AG_true| "" (SKOSIMP*) (("" (GRIND :EXCLUDE ("lfp")) (("" (LEMMA "lfp_lem3") (("" (INST?) (("" (PROP) (("1" (INST - "LAMBDA u: FALSE") (("1" (PROP) (("1" (EXPAND "<=") (("1" (INST?) NIL))) ("2" (BETA) (("2" (EXPAND "<=") (("2" (HIDE -1) (("2" (GRIND) NIL))))))))))) ("2" (HIDE -1) (("2" (GRIND :IF-MATCH NIL) (("2" (INST?) (("2" (INST?) (("2" (PROP) NIL))))))))))))))))))) (|AG_variance| "" (SKOSIMP*) (("" (EXPAND "AG") (("" (EXPAND "EF") (("" (EXPAND "EU") (("" (REWRITE "contrapose") (("" (EXPAND "mu") (("" (LEMMA "lfp_lem3") (("" (INST?) (("" (PROP) (("1" (INST?) (("1" (PROP) (("1" (BETA) (("1" (HIDE 2) (("1" (NAME-REPLACE "foo" "EX(G!1, lfp(LAMBDA (Q: pred[T]): (NOT f!1 OR ((LAMBDA u: TRUE) AND EX(F!1, Q)))))") (("1" (REWRITE "lfp_thm2" :DIR RL) (("1" (REVEAL -1) (("1" (REPLACE -1 :DIR RL :HIDE? T) (("1" (NAME-REPLACE "bar" "lfp(LAMBDA (Q: pred[T]): (NOT f!1 OR ((LAMBDA u: TRUE) AND EX(F!1, Q))))") (("1" (EXPAND "<=") (("1" (SKOSIMP*) (("1" (EXPAND "NOT") (("1" (EXPAND "OR") (("1" (EXPAND "AND") (("1" (PROP) (("1" (INST? -3) (("1" (PROP) NIL))) ("2" (EXPAND "EX") (("2" (SKOSIMP*) (("2" (INST?) (("2" (INST? -4) (("2" (PROP) NIL))))))))))))))))))))))))))) ("2" (HIDE 2) (("2" (EXPAND "ismono") (("2" (GRIND :IF-MATCH NIL) (("2" (INST? +) (("2" (PROP) (("2" (INST? -) (("2" (PROP) NIL))))))))))))))))))))))))) ("2" (HIDE 2) (("2" (GRIND :IF-MATCH NIL) (("2" (INST? +) (("2" (PROP) (("2" (INST? -) (("2" (PROP) NIL))))))))))))))))))))))))))))) (|AG_invariance| "" (GRIND :IF-MATCH NIL :EXCLUDE ("lfp" "<=")) (("" (REWRITE "deMorgan") (("" (REWRITE "contrapose") (("" (NAME-REPLACE "LFP1" "lfp(LAMBDA (Q: pred[T]): (NOT I!1 OR ((LAMBDA u: TRUE) AND EX(F!1, Q))))") (("" (NAME-REPLACE "LFP2" "lfp(LAMBDA (Q: pred[T]): (NOT f!1 OR ((LAMBDA u: TRUE) AND EX(restrict(F!1, I!1), Q))))") (("" (LEMMA "lfp_lem3") (("" (INST?) (("" (PROP) (("1" (INST?) (("1" (PROP) (("1" (HIDE 2) (("1" (BETA) (("1" (NAME-REPLACE "EXF" "EX(F!1, (LFP1 OR LFP2))") (("1" (REVEAL -4 -5) (("1" (REPLACE -1 :DIR RL) (("1" (REPLACE -2 :DIR RL) (("1" (REWRITE "lfp_thm2" :DIR RL :TARGET-FNUMS +) (("1" (REPLACE -1 :HIDE? T) (("1" (REWRITE "lfp_thm2" :DIR RL :TARGET-FNUMS +) (("1" (REPLACE -1 :HIDE? T) (("1" (REVEAL -1) (("1" (REPLACE -1 :DIR RL :HIDE? T) (("1" (GRIND :IF-MATCH NIL) (("1" (INST? +) (("1" (PROP) NIL))) ("2" (INST? 2) (("2" (PROP) (("2" (INST?) (("2" (PROP) (("2" (REVEAL -5) (("2" (REPLACE -1 :DIR RL) (("2" (STOP-REWRITE) (("2" (REWRITE "lfp_thm2" :DIR RL :TARGET-FNUMS +) (("1" (REPLACE -1 :HIDE? T) (("1" (GRIND :IF-MATCH NIL) NIL))) ("2" (HIDE -1 2) (("2" (GRIND :IF-MATCH NIL) (("2" (INST?) (("2" (INST?) (("2" (PROP) NIL))))))))))))))))))))))))))))))))) ("2" (HIDE -1 2) (("2" (GRIND :IF-MATCH NIL) (("2" (INST?) (("2" (INST?) (("2" (PROP) NIL))))))))))))) ("2" (HIDE -1 -2 2) (("2" (GRIND :IF-MATCH NIL) (("2" (INST?) (("2" (INST?) (("2" (PROP) NIL))))))))))))))))))))))))))) ("2" (HIDE 2) (("2" (GRIND :IF-MATCH NIL) (("2" (INST?) (("2" (INST?) (("2" (PROP) NIL)))))))))))))))))))))))))) $$$abstraction.pvs abstraction [cstate, astate : TYPE ] : THEORY %Contains the main results on correct abstractions for AG %properties. good_abstraction? says that abst is a good %abstraction from concrete program(satisfying %invariant I) to an abstract program for the %purpose of proving AG(Cprop) from abstract property AG(Aprop) %if Cinit implies Ainit o abst, C/I implies A o , %and I and Aprop o abst implies Cprop. BEGIN IMPORTING ctlthms abst: VAR [cstate -> astate] C : VAR PRED[[cstate, cstate]] A : VAR PRED[[astate, astate]] Cinit, Cprop : VAR PRED[cstate] Ainit, Aprop : VAR PRED[astate] I : VAR PRED[cstate] good_abstraction?(abst, Cinit, C, Cprop, Ainit, A, Aprop, I): bool = ( (FORALL (u : cstate): Cinit(u) IMPLIES Ainit(abst(u))) AND (FORALL (u, v: cstate): restrict(C, I)(u, v) IMPLIES A(abst(u), abst(v))) AND (FORALL (u: cstate): I(u) AND Aprop(abst(u)) IMPLIES Cprop(u)) ) %If A, abst(a) |= AG(Aprop), %then A o , a |= Aprop o abst abstraction_step: LEMMA (FORALL (v: cstate): AG(A, Aprop)(abst(v)) IMPLIES AG(LAMBDA (u, v: cstate): A(abst(u), abst(v)), LAMBDA (u: cstate): Aprop(abst(u)))(v)) % v |= I and C/I, v |= AG(Cprop), then C/I, v |= AG(I /\ Cprop) %namely v |= I implies C/I, v |= AG(I). It takes some thought %to convince oneself that the I(v) antecedent is needed. restrict_AG: LEMMA (FORALL (v: cstate): I(v) AND AG(restrict(C, I), Cprop)(v) IMPLIES AG(restrict(C, I), (LAMBDA (u: cstate): I(u) AND Cprop(u)))(v)) %This is the main theorem: it asserts that if abst is a good abstraction, %the abstract program satisfies Aprop, the concrete program satisfies %the abstraction invariant I, then the concrete program satisfies Cprop. good_abstraction_works: LEMMA good_abstraction?(abst, Cinit, C, Cprop, Ainit, A, Aprop, I) AND (FORALL (a: astate): Ainit(a) IMPLIES AG(A, Aprop)(a)) AND (FORALL (u: cstate): Cinit(u) IMPLIES AG(C, I)(u)) IMPLIES (FORALL (v: cstate): Cinit(v) IMPLIES AG(C, Cprop)(v)) END abstraction $$$abstraction.prf (|abstraction| (|abstraction_step| "" (SKOSIMP*) (("" (EXPAND "AG") (("" (EXPAND "EF") (("" (EXPAND "EU") (("" (EXPAND "NOT") (("" (EXPAND "mu") (("" (LEMMA "lfp_lem3[cstate]") (("" (INST?) (("" (PROP) (("1" (INST - "LAMBDA (u : cstate): lfp(LAMBDA (Q: pred[astate]): ((LAMBDA (a: astate): NOT Aprop!1(a)) OR ((LAMBDA (a : astate): TRUE) AND EX(A!1, Q))))(abst!1(u))") (("1" (PROP) (("1" (EXPAND "<=") (("1" (INST?) (("1" (PROP) NIL))))) ("2" (HIDE -1 2) (("2" (BETA) (("2" (NAME-REPLACE "EXP" "EX(LAMBDA (u, v: cstate): A!1(abst!1(u), abst!1(v)), LAMBDA (u: cstate): lfp(LAMBDA (Q: pred[astate]): ((LAMBDA (a: astate): NOT Aprop!1(a)) OR ((LAMBDA (a: astate): TRUE) AND EX(A!1, Q))))(abst!1(u)))") (("2" (REWRITE "lfp_thm2" :DIR RL) (("1" (REVEAL -1) (("1" (REPLACE -1 :DIR RL) (("1" (HIDE -1) (("1" (NAME-REPLACE "LFP" "lfp(LAMBDA (Q: pred[astate]): ((LAMBDA (a: astate): NOT Aprop!1(a)) OR ((LAMBDA (a: astate): TRUE) AND EX(A!1, Q))))") (("1" (EXPAND "<=") (("1" (GRIND :IF-MATCH NIL) (("1" (INST?) (("1" (PROP) NIL))))))))))))))) ("2" (HIDE 2) (("2" (GRIND :IF-MATCH NIL) (("2" (INST?) (("2" (INST?) (("2" (PROP) NIL))))))))))))))))))))) ("2" (HIDE -1 2) (("2" (GRIND :IF-MATCH NIL) (("2" (INST?) (("2" (INST?) (("2" (PROP) NIL))))))))))))))))))))))))))) (|restrict_AG| "" (SKOSIMP*) (("" (EXPAND "AG") (("" (EXPAND "EF") (("" (EXPAND "EU") (("" (EXPAND "NOT") (("" (EXPAND "mu") (("" (LEMMA "lfp_lem3[cstate]") (("" (INST? :WHERE -) (("" (PROP) (("1" (NAME-REPLACE "LFP2" "lfp(LAMBDA (Q: pred[cstate]): (LAMBDA (u: cstate): NOT Cprop!1(u)) OR ((LAMBDA (u : cstate): TRUE) AND EX(restrict(C!1, I!1), Q)))") (("1" (INST - "(NOT I!1) OR LFP2") (("1" (BETA) (("1" (PROP) (("1" (EXPAND "<=") (("1" (INST?) (("1" (PROP) (("1" (HIDE -3) (("1" (GRIND) NIL))))))))) ("2" (HIDE -2 2) (("2" (EXPAND "<=") (("2" (SKOSIMP*) (("2" (REVEAL -3) (("2" (REPLACE -1 + :DIR RL) (("2" (REWRITE "lfp_thm2" :TARGET-FNUMS + :DIR RL) (("1" (REPLACE -1 :HIDE? T) (("1" (GRIND :IF-MATCH NIL) (("1" (INST?) (("1" (PROP) NIL))))))) ("2" (HIDE -1 -2 -3 2) (("2" (GRIND :IF-MATCH NIL) (("2" (INST?) (("2" (INST?) (("2" (PROP) NIL))))))))))))))))))))))))))))) ("2" (HIDE -1 -2 2) (("2" (GRIND :IF-MATCH NIL) (("2" (INST?) (("2" (INST?) (("2" (PROP) NIL))))))))))))))))))))))))))) (|good_abstraction_works| "" (SKOSIMP*) (("" (INST? -3) (("" (PROP) (("" (LEMMA "AG_invariance[cstate]") (("" (INST - "C!1" "I!1" "Cprop!1") (("" (EXPAND "<=") (("" (INST?) (("" (PROP) (("" (EXPAND "AND") (("" (PROP) (("" (LEMMA "AG_variance[cstate]") (("" (INST - "restrict(LAMBDA (u, v: cstate): A!1(abst!1(u), abst!1(v)), I!1)" "restrict(C!1, I!1)" "LAMBDA (u: cstate): I!1(u) AND Aprop!1(abst!1(u))" "Cprop!1") (("" (PROP) (("1" (EXPAND "<=") (("1" (INST?) (("1" (PROP) (("1" (REWRITE "restrict_AG") (("1" (HIDE -2 -3 -4 2 3 4) (("1" (GRIND :IF-MATCH NIL :EXCLUDE "lfp") (("1" (REWRITE "lfp_thm2" :DIR RL) (("1" (GRIND :IF-MATCH NIL :EXCLUDE ("lfp" EX)) NIL) ("2" (HIDE 2 3) (("2" (GRIND :IF-MATCH NIL) (("2" (INST?) (("2" (INST?) (("2" (PROP) NIL))))))))))))))) ("2" (LEMMA "AG_variance[cstate]") (("2" (INST - "(LAMBDA (u, v: cstate): A!1(abst!1(u), abst!1(v)))" "restrict(LAMBDA (u, v: cstate): A!1(abst!1(u), abst!1(v)), I!1)" "LAMBDA (u: cstate): Aprop!1(abst!1(u))" "LAMBDA (u: cstate): Aprop!1(abst!1(u))") (("2" (PROP) (("1" (EXPAND "<=") (("1" (INST?) (("1" (PROP) (("1" (REWRITE "abstraction_step") (("1" (INST?) (("1" (PROP) (("1" (EXPAND "good_abstraction?") (("1" (FLATTEN) (("1" (INST? -2) (("1" (PROP) NIL))))))))))))))))))) ("2" (HIDE 2 3 4) (("2" (EXPAND "<=") (("2" (EXPAND "restrict") (("2" (SKOSIMP*) NIL))))))) ("3" (HIDE 2 3 4) (("3" (EXPAND "<=") (("3" (SKOSIMP*) NIL))))))))))))))))))) ("2" (HIDE 2 3) (("2" (EXPAND "good_abstraction?") (("2" (FLATTEN) (("2" (EXPAND "<=") (("2" (SKOSIMP*) (("2" (INST? -4) (("2" (PROP) (("2" (EXPAND "restrict") (("2" (PROP) NIL))))))))))))))))) ("3" (EXPAND "good_abstraction?") (("3" (FLATTEN) (("3" (EXPAND "<=") (("3" (PROPAX) NIL))))))))))))))))))))))))))))))))))