(defstep simp () (then (flatten)(assert)(simplify)(flatten)) " Flatten, assert, simplify" "Flatten, assert, simplify" ) (defstep spsi (&optional (fnum +)) (then (split fnum)(simp)) "split then simp" "split then simp" ) (defstep exptemp (&optional (val? t) (repeat? t) (member? f)) (then ; 29-06-03 expand everything once ; if repeat is t then expand everything repeatedly ; 08 07 03 by default member is not expanded at all ; 10 08 03 Removed sim after expand "is_valid" -- caused infinite loop (expand "OR")(expand "AND")(expand "NOT") (expand "F")(expand "P")(expand "G")(expand "<>")(expand "[]") (expand "\\/") (expand "/\\")(expand "o") (expand "U")(expand "W")(expand "X")(expand "TRUE") (expand "FALSE")(expand "&")(expand "v")(expand "IMPLIES") (expand "assertion_to_TP")(expand "predicate_to_TP")(expand "intersection") (if (eq member? 'f)(skip)(expand "member")) (if (eq val? 't) (then (expand "is_P_valid")(expand "is_P_state_valid") (expand "is_P_run_valid") (expand "is_valid")) (skip) ) (if (eq repeat? 't)(then (repeat* (then (expand "OR")(expand "AND")(expand "NOT") (expand "F")(expand "G")(expand "<>")(expand "[]") (expand "\\/") (expand "/\\")(expand "o") (expand "U")(expand "W")(expand "X")(expand "TRUE") (expand "FALSE")(expand "&")(expand "v")(expand "IMPLIES") (expand "assertion_to_TP")(expand "predicate_to_TP")(expand "intersection") (if (eq member? 't)(expand "member")(skip)) (if (eq val? 't) (then (expand "is_P_valid")(expand "is_P_state_valid") (expand "is_P_run_valid") (expand "is_valid")) (skip) )))) (skip) ) (simp)) "Expands out temporal operators" "Expands out temporal operators" ) (defstep lazygrind (&optional (exclude nil) (defs !)) (then (grind$ :if-match nil :exclude exclude :defs defs)(grind$ :exclude exclude :defs defs)) " Grind with the instantiation postponed to the end" " ") (defstep instbest (&optional (fnum *)) (then (inst? fnum :if-match best)) "Applies inst? :if-match best to the optional line number (num, +, -)" " " ) (defstep lazy-grind (&optional (if-match t) (defs !) rewrites theories exclude (updates? t)) (then (grind$ :if-match nil :defs defs :rewrites rewrites :theories theories :exclude exclude :updates? updates?) (reduce$ :if-match if-match :updates? updates?)) "Equiv. to (grind) with the instantiations postponed until after simplification." "By skolemization, if-lifting, simplification and instantiation") (defstep basic-split-if (&optional (fnum *)) (then (lift-if fnum) (let ((fnums (gather-fnums (s-forms (current-goal *ps*)) fnum nil #'(lambda (sform) (or (branch? (formula sform)) (and (negation? (formula sform)) (branch? (args1 (formula sform)))))))) (fnum (when fnums (car fnums)))) (if fnum (split fnum) (skip-msg "No IF-THEN-ELSE in the sequent.")))) "Applies LIFT-IF and splits only an IF-THEN-ELSE sequent formula in the result." "Lifting IF-THEN-ELSEs and splitting on an IF-THEN-ELSE") (defstep new-split-if (&optional (fnum +)) (then (basic-split-if fnum)(simp)(replace*)(simp)) "Lift-if, split, replace and simplify " "Lift-if, split, replace and simplify " ) (defstep split-if (&optional (fnum +)) (then (basic-split-if fnum)(simp)(replace*)(simp)) "Lift-if, split, replace and simplify " "Lift-if, split, replace and simplify " ) (defstep clean-up () (let ((fnums (gather-fnums (s-forms (current-goal *ps*)) * nil #'(lambda (sform) (or (and (negation? (formula sform)) (and (implication? (args1 (formula sform))) (or (tc-eq (args1 (args1 (formula sform))) *false*) (tc-eq (args2 (args1 (formula sform))) *true*)))) (and (negation? (formula sform)) (and (disjunction? (args1 (formula sform))) (or (tc-eq (args1 (args1 (formula sform))) *true*) (tc-eq (args2 (args1 (formula sform))) *true*)))) (and (conjunction? (formula sform)) (or (tc-eq (args1 (formula sform)) *false*) (tc-eq (args2 (formula sform)) *false*))))))) (fnum (when fnums (car fnums)))) (if fnum (hide fnums)(skip-msg "No formulae to clean-up"))) "Hide all antecedents of the form FALSE IMPLIS X, X IMPLIES TRUE, TRUE OR X and consequents FALSE AND Y " "Hide all antecedents of the form FALSE IMPLIES X, X IMPLIES TRUE, TRUE OR X and consequents FALSE AND Y" ) (defstep reduce-if (&optional (toreplace nil)(exclude nil)) (let ((fnums (gather-fnums (s-forms (current-goal *ps*)) * exclude #'(lambda (sform) (or (and (negation? (formula sform)) (and (branch? (args1 (formula sform))) (or (tc-eq (then-part (args1 (formula sform))) *false*) (tc-eq (else-part (args1 (formula sform))) *false*)))) (and (branch? (formula sform)) (or (tc-eq (then-part (formula sform)) *true*) (tc-eq (else-part (formula sform)) *true*))))))) (fnum (when fnums (car fnums)))) (if fnum (then (split fnum)(flatten)(replace toreplace)) (skip-msg "Nothing to reduce if"))) "Split an antecedent if-formula if either the then-part or the else-part is false" "Reducing void if-formulae" ) (defstep inst-label (fnum value label) (let ((newstring (format nil "~a" label))) (with-labels (inst-cp fnum value) ((newstring))) ) "Instantiate, copy and label" "Instantiates, copies and labels." ) (defstep split-all (&optional (fnum nil)(sko? t)) (then (repeat* (then (basic-split-if$ +)(simp$)(if (eq sko? 't)(skosimp*)(skip))(replace*)(simp$)(reduce-if$) (then (basic-split-if$ fnum)(simp$)(replace*)(simp$))))(clean-up) ) "Lift, splits consequents and those in fnum, if specified. Antecedents with FALSE then or else-parts also split" "Split-all if-then-else consequents" ) (defstep reduce-all (&optional (fnum nil)(sko? t)) (repeat* (then (reduce-if$ +)(simp$)(if (eq sko? 't)(skosimp*)(skip))(replace*)(simp$))) "Split all antecedent if-formulae where either the then-part or the else-part is false. Skolemizes and replaces" "Splitting all if-then antecedents with false" ) (defstep exp-justice() (then (expand "pfs")(expand "justice") (expand "j_1")(expand "j_2")(expand "j_3") (expand "j_4")(expand "j_5")(expand "j_6") (expand "j_7")(expand "j_8")(expand "j_9") (expand "j_10")(expand "j_11")(expand "j_12") (expand "j_13")(expand "j_14")(expand "j_15") (expand "j_16")(expand "j_17")(expand "j_18") (expand "j_19")(expand "j_20")(expand "j_21") ) " Expands justice" " Expands justice" ) (defstep remove-impl () (then (auto-rewrite! "impl_to_if") (auto-rewrite! "iff_to_if") (assert)) "Rewrite implications and iffs to ifs" "Rewrite implications and iffs to ifs" ) (defstep remove-iff (&optional (fnum nil)) (if (eq fnum nil) (then (auto-rewrite! "iff_to_if") (assert)) (then (lemma "iff_to_if") (inst? -1 :where fnum)(replace -1 :hide? t)) ) "Change a iff b to if a then b else not b" "Change a iff b to if a then b else not b" ) (defstep inst-from-upto (&optional min max (fnum +)) (let ((minsucc (+ min 1))) (if (< min max) (then (inst-cp fnum min)(inst-from-upto$ minsucc max fnum)) (then (if (eq min max) (inst fnum min)(skip))))) "instantiate fnum (default +) with all values from min to max" "instantiate fnum (default +) with all values from min to max" ) (defstep inst-upto (&optional max (fnum +)) (inst-from-upto$ 0 max fnum) "instantiate fnum (default +) with all values from 0 to max" "instantiate fnum (default +) with all values from 0 to max" ) (defstep name-replace-l (&optional new old lab (hide? t)) ; 12 12 01 (then (name-replace new old :hide? nil) (if (eq lab 'nil) (then (label new -1) (if (or (eq hide? nil)(eq hide? 'f))(skip)(hide new))) (then (label lab -1) (if (or (eq hide? nil)(eq hide? 'f))(skip)(hide lab))) ) ) "Replaces old with new, labeling formula `old = new' with label lab if given, new otherwise. This formula is hidden if hide? is t" "Replaces old with new and labels" ) (defstep binv (&optional (inv1 nil) (inv2 nil)(inv3 nil)(inv4 nil)) (then (lemma "BINV")(label "binv" -1)(inst? - :where +) (simp)(replace 1)(simp) (hide 2) ; (expand inv1)(expand inv2)(expand inv3)(expand inv4) (skosimp*) (label "computation" -1) (spread (split "binv") ; 01 05 02 : spsi not good if property is anded statement ((then (skosimp*) (save "computation") (expand "computation") (flatten) (label "initial" -1) (hide "computation") (expand "fds")(expand "pfs") (expand "initial") (expand inv1)(expand inv2)(expand inv3)(expand inv4) ; renaming with labeling added 011126 (name-replace "current!1" "seq!1(0)" :hide? nil) (label "current" -1) (hide "current") (try (try (lazygrind) (fail) (skip)) (skip) (comment "The base case of the BINV rule") ) ) (then (skosimp*) (hide "computation") (label "rho" -1) (label "invariant" -2) (if (eq inv1 nil)(skip)(label inv1 -2 :push? t)) (label "rtp" 1) (expand "fds")(expand "pfs")(expand "rho") (try (spread (split-idle)((skip)(fail)))(skip)(skip)) ; 18 05 02 : discharge idling before expanding (expand inv1)(expand inv2)(expand inv3)(expand inv4) (expand "reachable")(simp)(exptemp)(skosimp*) (name-replace "next!1" "seq!1(t!1+1)" :hide? nil) (label "next" -1) (name-replace "current!1" "seq!1(t!1)" :hide? nil) (label "current" -1) (hide "next" "current") ;hidden 011126 (expand inv1)(expand inv2)(expand inv3)(expand inv4) (comment "The inductive step of the BINV rule") ) ) ) ) "lemma BINV. The optional parameters inv1, inv2, inv3 and inv4 are expressions to be expanded." "lemma BINV" ) (defstep inv (&optional weaker stronger (inv1 nil)(inv2 nil)) (then (lemma "INV")(label "inv" -1)(inst? - :where +) (inst - stronger)(simp)(hide-all-but "inv") (skosimp*) (label "initialized_run" -1) (spread (split "inv") ; 01 05 02 : spsi not good if property is anded statement ((then (skosimp*) (hide "initialized_run") (expand* stronger weaker inv1 inv2) (skosimp*) (name-replace "current!1" "seq!1(t!1)" :hide? nil) (label "current" -1) (hide "current") (try (try (lazygrind) (fail) (skip)) (skip) (let ((newstring (format nil "Proving ~a implies ~a" stronger weaker))) (comment newstring)) ) ) (then (skosimp*) (save "initialized_run") (expand "initialized_run") (flatten) (label "initial" -1) (hide "initialized_run") (expand "fds")(expand "pfs") (expand "initial") (expand stronger)(expand weaker) (expand inv1)(expand inv2) ; renaming with labeling added 011126 (name-replace "current!1" "seq!1(0)" :hide? nil) (label "current" -1) (hide "current") (try (try (lazygrind) (fail) (skip)) (skip) (comment "The base case of the INV rule") ) ) (then (skosimp*) (hide "initialized_run") (label "rho" -1) (label "invariant" -2) (if (eq inv1 nil)(skip)(label inv1 -2 :push? t)) (label "rtp" 1) (expand "fds")(expand "pfs")(expand "rho") (try (spread (split-idle)((skip)(fail)))(skip)(skip)) ; 18 05 02 : discharge idling before expanding (expand stronger)(expand weaker) (expand inv1)(expand inv2) (expand "reachable")(simp)(exptemp)(skosimp*) (name-replace "next!1" "seq!1(t!1+1)" :hide? nil) (label "next" -1) (name-replace "current!1" "seq!1(t!1)" :hide? nil) (label "current" -1) (hide "next" "current") ;hidden 011126 (comment "The inductive step of the INV rule") ) ) ) ) "lemma INV. Uses inductive stronger invariant to prove desired, weaker invariant. The optional parameters inv1, inv2, inv3 and inv4 are expressions to be expanded." "lemma INV" ) (defstep bwait (&optional (inv1 nil) (inv2 nil)(inv3 nil)(inv4 nil)(split-rho? f)) (then (skosimp*) (lemma "BWAIT")(label "bwait" -1)(inst? - :where +) (inst? "bwait" :where +) (simp)(replace 1)(simp) (hide 2) (exptemp) (skosimp*) (label "computation" -1) (label "a" -2 :push? t) (label "a_p" 1 :push? t) (label "b_p" 2 :push? t) (save "computation") (expand "computation") (expand "pfs") (expand "run") (flatten) (label "initial" -1) (label "rho" -2) (label "justice" -3) (label "compassion" -4) (hide "initial" "justice" "compassion") (inst "rho" "t!1") (name-replace-l "next!1" "seq!1(t!1+1)" "next") (name-replace-l "current!1" "seq!1(t!1)" "current") (expand "rho") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (if (eq split-rho? 't)(split-rho-all)(skip)) ) "Aplies lemma BWAIT. Splits rho if split-rho? is t. Expressions inv1, .. inv4 are expanded" "lemma BWAIT" ) (defstep moni () (then (lemma "MONI")(label "moni" -1)(inst? "moni" :where +)(inst? "moni")(spsi "moni") (hide-all-but "moni") ) "lemma MONI" "lemma MONI" ) (defstep coni (&optional subst1 subst2 (hide? f)) (let ((sub1 (- subst1 1)) (sub2 (- subst2 1))) (then (lemma "CONI")(label "coni" -1)(inst? :where sub1 )(inst? :where sub2)(simp) (if (eq hide? t)(hide sub1 sub2)(skip))) ) "lemma CONI" "lemma CONI" ) (defstep coni-rec (subst hide?) (let ((subm (- subst 1)) (subp (+ subst 1))) (then (coni subst -1)(hide -2) (if (eq hide? t)(hide subst)(skip)) (if (eq subst -2)(skip)(coni-rec$ subp hide?)))) " " " " ) (defstep coni-m (&optional number (hide? f)) (let ((sub1 (* number -1)) (sub2 (+ 1 (* number -1)))) (if (< number 2) (skip-msg "coni-m must have parameter number set to >= 2") (then (coni sub2 sub1 hide?) (if (eq number 2) (skip) (coni-rec$ sub2 hide?) ) ) ) ) "Applies lemma CONI to multiple formulas. Parameter number gives the number of formulas. If hide? is set to t, these formulas are hidden." "Applies lemma CONI to multiple formulas. Parameter number gives the number of formulas. If hide? is set to t, these formulas are hidden." ) (defstep valid-to-state-valid (&optional (fnum -) (hide? f)) (let ((newnum (if (or (or (eq fnum '-)(eq fnum '+)) (> fnum 0)) fnum (- fnum 1)))) (then (lemma "valid_to_state_valid") (inst? - :where newnum)(simp)(if (and (eq hide? 't) (and (not (or (eq fnum '-) (eq fnum '+)) ) (< fnum 0))) (hide newnum)(skip)))) "rule valid-to-state-valid" "rule valid-to-state-valid" ) (defstep state-valid-to-valid (&optional (fnum -) (hide? f)) (let ((newnum (if (or (or (eq fnum '-)(eq fnum '+)) (> fnum 0)) fnum (- fnum 1)))) (then (lemma "state_valid_to_valid") (inst? - :where newnum)(simp)(if (and (eq hide? 't) (and (not (or (eq fnum '-) (eq fnum '+)) ) (< fnum 0))) (hide newnum)(skip)))) "rule state-valid-to-valid" "rule state-valid-to-valid" ) (defstep use-invariants (&optional (number 1)(hide? t)) (then (if (> number 1)(coni-m$ number)(skip)) (lemma "INTRODUCE_INV")(inst? :where +)(inst? :where -)(simp) (if (eq hide? 't)(hide-all-but 1)(skip))) "lemma use-invaraints" "lemma use-invaraints" ) (defstep use-invariant (&optional inv (where nil)(expand? t)) ; 190602 - inst? to where (try (lemma-l inv) (then (stop-rewrite) ; 10 03 stop-rewrites or strategy fails after grind (exptemp$ :val? t :member? f)(skosimp*) ; 29 06 03 no longer expand member (reveal "computation") (try (reveal "initialized_run") (skip) (then (lemma-l "computation_is_run")(inst? "computation_is_run"))) (expand "predicate_to_TP" inv) ; reveal / replace current 011126 (if (eq expand? 't)(expand inv)(skip)) (simp) (if (eq where nil) (then (with-labels (reveal "current") ("hcurrent") :push? t) (inst? inv :where "current")(simp)(inst? inv :where "current")(replace "current")) (then (with-labels (reveal where) ("where") :push? t) (inst? inv :where where)(simp) (inst? inv :where where)(replace where :hide? t)) ) (hide "computation" "initialized_run" "computation_is_run" "hcurrent") ) (let ((newstring (format nil "Error: Lemma ~a not found." inv))) (comment newstring) )) "Invokes lemma `inv', instantiating in accordance with formula `where'. If a where-value is not provided, instantiate to match current. Expands the formula if expand? is t." "Invokes lemma `inv'" ) (defstep reach () (then (lemma "reachableInv")(label "reachable" -1)(expand "reachable")) "Invokes lemma reachableInv" "lemma reachableInv" ) (defstep try-grind (&optional (if-match nil)) (try (try (grind :if-match if-match)(fail)(skip)) (skip)(skip)) "Does a grind if it completes the proof, else skips" "Does a grind if it completes the proof, else skips" ) (defstep grind-one (&optional (if-match nil)) (try (spread (grind :if-match if-match)((skip)(fail))) (skip)(skip)) ;; 011102 : bad stategy as everything autorewrited, so use-invariants etc no longer work "Does a grind if it completes the proof or leaves only 1 subgoal, else skips" "Does a grind if it completes the proof or leaves only 1 subgoal, else skips" ) (defstep try-lazygrind () (try (try (lazygrind)(fail)(skip)) (skip)(skip)) "Does a grind if it completes the proof, else skips" "Does a grind if it completes the proof, else skips" ) (defstep try-split-all () (try (try (split-all)(then assert :flush? t)(fail)(skip)) (skip)(skip)) "Does a split-all if it completes the proof, else skips" "Does a split-all if it completes the proof, else skips" ) (defstep grind-rho (&optional (if-match nil)) (then (split "rho")(flatten)(replace*)(simp) (try (try (grind :if-match if-match)(fail)(skip)) (skip)(then (lift-if)(reduce-all)))) "Does a grind if it completes the proof, else skips." "Does a grind if it completes the proof, else skips" ) (defstep split-rho (&optional (remove-impl? t)(split-up 0)) (then (if (eq remove-impl? 't)(remove-impl)(skip)) (expand "pfs" "rho")(expand "rho")(spsi "rho")(skosimp*)(then (spsi "rho")(skosimp*)(replace*)(simp)(split-up$ split-up)(assert :flush? t))) "Splits rho, replaces and simps. If remove-impl? is t (the default), then strategy remove-impl is applied." "Splits rho, replaces and simps." ) (defstep split-idle () (then (expand "pfs" "rho")(expand "rho") (spread (split "rho")((then (replace*)(simp)) (skosimp*)))) "Splits rho, replaces and simps. If remove-impl is t (the default), then strategy remove-impl is applied." "Splits rho, replaces and simps." ) (defstep split-up (&optional (fnum 1)) (then (repeat* (then (spsi fnum)))) "Repeatedly splits sequent fnum" "Repeatedly splits sequent fnum" ) (defstep split-rho-all-noinst (&optional (split-up 1)(force? f)(remove-impl? t)(split-all -)) (then (split-rho$ :remove-impl? remove-impl? :split-up split-up) (if (eq force? 't) (split-all split-all) (try (spread (apply (then (split-all split-all)(assert :flush? t))) ((skip)(fail))) (skip) (then (reduce-all)(clean-up)) ) ) ) "Splits the transition relation, and simplifies. Applies split-up to formula fnum, then does split-rho. If force? is true the (split-all -) is applied to every subgoal. Else, (split-all -) is applied only if it completes the subgoal." "Splits the transition relation, and simplifies." ) (defstep inst-set (&optional fnum values (hide? t)) (then (inst-set-p$ fnum values) (if (eq hide? 't)(skip)(then (reveal "_inst_p")(unlabel * "_inst_p"))) ) "Instantiates all values in values set into formula fnum. If hide? is t then fnum is hidden after instatiation." "instantiates all values in values set into formula fnum" ) (defstep inst-set-c (inst-into values) (let ((firstval (car values)) (others (cdr values))) (if others (if firstval (then (with-labels (inst-cp inst-into firstval)("_inst_c") :push? t) (inst-set-c$ inst-into others))(skip)) (if firstval (then (with-labels (inst-cp inst-into firstval)("_inst_c") :push? t)) (skip)) )) "instantiates all values in values set into formula fnum" "instantiates all values in values set into formula fnum" ) (defstep inst-set-p (inst-into values) (let ( (fnums (gather-fnums (s-forms (current-goal *ps*)) inst-into nil #'(lambda (sform) (or (and (negation? (formula sform)) (forall-expr? (args1 (formula sform)))) (exists-expr? (formula sform))))) ) (fnum (car fnums))) (if fnum (then (label "_inst_p" fnum :push? t) (if values (then (inst-set-c$ "_inst_p" values) (unlabel "_inst_c" "_inst_p")(unlabel * "_inst_c")) (skip)) (hide "_inst_p")) (skip) ) ) "instantiates all values in values set into formula fnum" "instantiates all values in values set into formula fnum" ) (defstep expandmany (values &optional (fnum *)) (let ((firstval (car values)) (others (cdr values))) (if others (then (expand firstval fnum)(expandmany$ others fnum)) (if firstval (expand firstval fnum) (skip)))) "Used by expandm" "Used by expandm" ) (defstep expandm (values &optional (fnum *)(repeat? t)) (if (eq repeat? 't)(repeat* (then (expandmany$ values fnum))) (expandmany$ values fnum)) "Repeatedly expands all the expressions in values into line fnum (default *)" "Repeatedly expands all the expressions in values into line fnum (default *)" ) (defstep split-all-inst (values &optional (inst-into -)(split-up 0) (split-all -)(remove-impl? t)(hide? t)) (then (skosimp*)(if (eq remove-impl? 't)(remove-impl)(skip)) (then (split-up$ split-up) (then (repeat* (then (split-all) (if (eq inst-into '*)(then (inst-set$ + values) (inst-set$ - values)) (inst-set$ inst-into values)) (then (split-all split-all) (if (eq inst-into '*)(then (inst-set$ + values) (inst-set$ - values)) (inst-set$ inst-into values)) )) )(assert :flush? t) ) (if (eq hide? t)(skip)(then (reveal "_inst_p")(unlabel * "_inst_p"))) ) ) "Lifts-if, splits ifs, and instantiates with the values given. Parameter values, not optional, is the list of values for instantiation. Instantiates into consequents and formulas inst-into, default -. (To restrict instantiation to consequents, set inst-into to +.) After instantiation formula is labelled _inst_p and hidden if hide? is t (default). Splits up formula split-up, default 0. Splits all if-then-else in consequents and formulas split-all, default -. Rewrites implications and iffs to if-then-else if remove-impl? is t (default t)" "Lift, splits consequents and those in fnum, if specified. Antecedents with FALSE then or else-parts also split. Instantiates with the list of values provided." ) (defstep split-rho-all (&optional (values nil)(split-up 1)(inst-into -)(force? f) (remove-impl? t)(no-sub? f)(split-all -)(hide? t)) (if (eq values 'nil) (split-rho-all-noinst$ :split-up split-up :force? force :remove-impl? remove-impl? :split-all split-all) (then (skosimp*)(if (eq remove-impl? 't)(remove-impl)(skip)) (then (split-rho$ :remove-impl? 'f :split-up split-up) (if (eq force? 't) (split-all-inst$ values :remove-impl? 'f :inst-into inst-into :split-all split-all :hide? t) (try (branch (split-all-inst$ values :remove-impl? 'f :inst-into inst-into :split-all split-all :hide? t) ((if (eq no-sub? 't)(fail)(skip))(fail))) (skip) (then (lift-if)(reduce-all)(clean-up)) ) ) ) (if (eq hide? 't)(skip)(then (reveal "_inst_p")(unlabel * "_inst_p"))) ) ) "Tries to complete a proof using split-rho followed by split-all-inst. Parameter values is the set of values to be instantiated (default nil), Formula split-up is split up using split (default 1), By default, split-all-inst is undone on any branch where it generates more than one subgoal. If force? is set to t (default f) it is not undone. If no-sub? is set to t (default f) it is undone if even one subgoal is generated. Split-all (default -) determines which formulas are to be split up. If remove-impl? is t (default) then implications and iffs are converted to if-then-else. The instantiated formulas are labeled _inst_p and hidden if hide? is t (default)" "Tries to complete a proof using split-rho and then split-all-inst. If this fails does simple simplification and returns goal to user" ) (defstep gen-case-string (variable value) (let ((newstring (format nil "~a = ~a" variable value))) (then (case newstring)(simp))) "try" "tru") (defstep case-split (&optional variable (max 10)) (let ((maxprec (- max 1))) (then (if (> max 0)(then (gen-case-string variable max)(case-split variable maxprec)) (then (gen-case-string variable max)))(simp))) "instantiate variable with all values from 0 to max (default 10) " "instantiate variable with all values from 0 to max " ) (defstep split-impl (&optional (fnum -)) (let ((impls (gather-seq (s-forms (current-goal *ps*)) fnum nil #'(lambda (sform) (and (negation? (formula sform)) (implication? (args1 (formula sform))))))) (icond (when impls (car (arguments (args1 (formula (car impls)))))))) (if icond (let ((newstring (format nil "~a" icond))) (then (case newstring)(reduce-all)(clean-up))) (skip-msg "No implication at specified position"))) "Split an implication antecedent a implies b into two subgoals, a and b, and not a. Takes as parameter the line number of the implication, default -" "Split an implication antecedent a implies b into two subgoals, a and b, and not a" ) (defstep split-or (&optional (fnum -)) (let ((impls (gather-seq (s-forms (current-goal *ps*)) fnum nil #'(lambda (sform) (and (negation? (formula sform)) (disjunction? (args1 (formula sform))))))) (icond (when impls (car (arguments (args1 (formula (car impls)))))))) (if icond (let ((newstring (format nil "~a" icond))) (then (case newstring)(reduce-all)(clean-up))) (skip-msg "No disjunction at specified position"))) "Split a disjunctive antecedent a or b into two subgoals: a ; not a and b. Takes as parameter the line number of the implication, default -" "Split a disjunctive antecedent a or b into two subgoals: a ; not a and b" ) (defstep split-and (&optional (fnum +)(lab nil)) (let ((impls (gather-seq (s-forms (current-goal *ps*)) fnum nil #'(lambda (sform) (conjunction? (formula sform))))) (icond (when impls (args1 (formula (car impls)))))) (if icond (let ((newstring (format nil "not (~a)" icond))) (if (eq lab 'nil) (then (spread (case newstring) ((then (replace 1)(reduce-all)(clean-up)) (then (reduce-all)(clean-up))))) (spread (case newstring) ((then (label lab 1)(replace 1)(reduce-all)(clean-up)) (then (label lab -1)(reduce-all)(clean-up)) ) ) ) ) (skip-msg "No conjuction at specified position"))) "Split a conjunctive antecedent fnum: a and b into two subgoals: antecedent a and consequent b, and consequent a. Labels new a and b with label parameter, if provided." "Split a conjunctive antecedent a and b into two subgoals: antecedent a and consequent b, and consequent a." ) (defstep well (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil)(split-rho? f)) (then (lemma "WELL")(label "well" -1) (skosimp*)(inst? "well") ; 02 01 14 (for goal_id) (expand inv1)(expand inv2)(expand inv3)(expand inv4) (spread (spsi "well") ((then (hide-all-but ("well"))(exptemp)(skosimp*) (label "computation" -1) (reach) (exptemp) ; (lemma-l "computation_is_run") ; (inst? "computation_is_run") (inst? "reachable")(simp) (inst "reachable" "t!1") (hide "computation") ; "computation_is_run") (name-replace-l "current!1" "seq!1(t!1)" "current") (expand "disj_set")(expand "hset")(expand "help") (expand "phi") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (try-grind) (comment "Proving W1 :is_P_state_valid(START_ELT implies (GOAL_ELT or disj_set(hset)), pfs)") ) (then (hide-all-but ("well")) (label "rtp" 1) (exptemp) (skosimp*) ; (inst? "reachable") (simp) (label "computation" -1) ; (label "state_pair" -2) (label "hset" -2) (label "rho" -3) (label "dec" 2 :push? t) (label "same" 3 :push? t) (reach)(exptemp) ; (lemma-l "computation_is_run") ; (inst? "computation_is_run") (inst? "reachable")(simp) (inst "reachable" "t!1") ;(expand "state_pair")(skosimp*) (expand "phi")(expand "hset")(expand "dset") (expand "rank") (expand "help") (expand "restrict") (name-replace-l "current!1" "seq!1(t!1)" "current") (hide "computation") ; "computation_is_run") (expand "pfs") (expand "rho") (expand "justice") ; (hide "reachable") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (if (eq split-rho? 't)(split-rho)(skip)) (comment "Proving W2 : forall d : is_P_state_valid((lambda st: forall next: hset(d)(st) and pfs`rho(st, next) implies GOAL_ELT(next) or (exists e : hset(e)(next) and gt(rank(d)(st), rank(e)(next))) or hset(d)(next) and rank(d)(next) = rank(d)(st) and not jset(d)(next)), pfs)") ) )) ) "lemma WELL. The optional parameters inv1, inv2, inv3 and inv4 are names of expressions to be expanded. If split-rho? is set to t, (default f) then split-rho is applied." "lemma WELL" ) (defstep expand-expected-names () (then (expand "hset")(expand "jset")(expand "dset") (expand "just")(expand "phi") (expand "PHI") (expand "aset")(expand "help")) "" "" ) (defstep lemma-l (lem &optional (lab nonegiven)) (if (eq lab 'nonegiven) (with-labels (lemma lem) lem) (with-labels (lemma lem) lab)) "Applies lemma `lem' labeling it with the given label `lab', if provided, else with `lem'" "Applies a lemma labeling it with the given label" ) (defstep save (fnum &optional (lab nil)) ; fixed 25 2 03 : did not work properly if saved formula was a consequent ; and no label given. ; Try to create "unique" saving labels to ensure that a 2nd save doesn't ; reveal also first saves. (if (eq lab 'nil) (let ((newstring (format nil "saved~a" fnum))) (then (label newstring fnum :push? t)(hide newstring)(reveal newstring)(unlabel * newstring)) ) (then (label lab fnum)(hide lab)(reveal lab))) "Saves formula at line / label fnum by hiding then revealing. If fnum is a line then a 2nd, label, parameter must be given." "Saves a formula by hiding then revealing" ) (defstep DIST_RANK_unbounded (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil) (split-rho? f)) (then (lemma "DIST_RANK_unbounded") (skosimp*)(inst? -) (label "dist_rank" -1) (expand inv1)(expand inv2)(expand inv3)(expand inv4) (spread (spsi "dist_rank") ((then (hide-all-but ("dist_rank"))(exptemp)(skosimp*) (label "computation" -1) (reach) (exptemp) ; (lemma-l "computation_is_run") ; (inst? "computation_is_run") (inst? "reachable")(simp) (inst "reachable" "t!1") (hide "computation") ; "computation_is_run") (name-replace-l "current!1" "seq!1(t!1)" "current") ; added 08 11 01 - label added 12 12 01 (expand "disj_set")(expand "hset")(expand "help") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (try-grind) ;04 05 02 changed from grind-one ; problems of expandign pfs ;081101 -changed from grind (comment "Proving D1: is_P_state_valid(START_ELT implies (GOAL_ELT or disj_set(hset)), pfs)") ) (then (hide-all-but ("dist_rank"))(exptemp)(skosimp*) (label "initialized_run" -1) (lemma-l "finite_support")(exptemp)(skosimp*)(inst? -)(simp) (comment "Proving the support is finite")) (then (hide-all-but ("dist_rank"))(skosimp*) (label "rtp" 1) (exptemp) (skosimp*) (label "computation" -1) (label "hset" -2) (label "rho" -3) (reach)(exptemp) ; (lemma-l "computation_is_run") ; (inst? "computation_is_run") (inst? "reachable")(simp) (inst "reachable" "t!1") (name-replace-l "current!1" "seq!1(t!1)" "current") (HIDE "computation"); "computation_is_run") (expand "rank") (expand-expected-names) (expand "state_help")(expand "helppred") (EXP-JUSTICE) (expand "restrict") (expand "pfs" "rho") (expand "rho") (expand "disj_set") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (spread (split-and "rtp") ((then (try (try (split-rho-all-noinst)(fail)(skip))(skip)(skip)) (comment "proving not ra implies not ra'")) (spread (split-and "rtp") ((then (label "same" 1)(label "dec" 2) (if (eq split-rho? 't)(split-rho)(skip)) (comment "Proving D2 : is_P_state_valid((lambda st: forall next: hset(d)(st) and pfs`rho(st, next) and not GOAL_ELT(next) implies ((hset(d)(next) or disj_set(hset)(next) and exists r : rank(r)(st) > rank(r)(next))))) ") ) (then ; Added label 08 11 01 - labeling nad hiding the assertion that there is some ; h' in the next sequent, and some decreasing rank i.e. D2 (label "hset_p" -1)(hide "hset_p") (if (eq split-rho? 't)(split-rho)(skip)) (comment "Proving D3 : is_P_state_valid((lambda st: forall next: hset(d)(st) and pfs`rho(st, next) and not GOAL_ELT(next) implies forall r : rank(r)(st) >= rank(r)(next), pfs)") )))))) (then (hide-all-but ("dist_rank"))(exptemp)(skosimp*) (label "initialized_run" -1) (label "hset" -2) (label "justice" -3) (reach)(exptemp) (inst? "reachable")(simp)(inst "reachable" "t!1") (expand-expected-names) (hide "initialized_run") (EXPand "pfs")(expand "justice") (name-replace-l "current!1" "seq!1(t!1)" "current") ;added 08 11 01 (expand inv1)(expand inv2)(expand inv3)(expand inv4) (comment "Proving is_valid(IMPLIES(hset(d), not(pfs`justice(d))))") ) ) ) ) "lemma DIST_RANK_infinite. The optional parameters inv1, inv2, inv3 and inv4 are names of expressions to be expanded. If split-rho? is set to t, (default f) then split-rho is applied." "lemma DIST_RANK_infinite" ) (defstep DIST_RANK_old (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil) (split-rho? f)) ; rewritten 2002-04-16 from dist_rank_viable (then (lemma "DIST_RANK_old") (skosimp*)(inst? -) (label "dist_rank" -1) ; (expand inv1)(expand inv2)(expand inv3)(expand inv4) ; 05 02 02 removed as expanding can change line numbers and make ; labeling wrong if expanded term takes > 1 line or moves from - to + ; or vice versa (spread (spsi "dist_rank") ((then (hide-all-but ("dist_rank"))(exptemp)(skosimp*) (label "computation" -1) (reach) (exptemp) ; (lemma-l "computation_is_run") ; (inst? "computation_is_run") (inst? "reachable")(simp) (inst "reachable" "t!1") (hide "computation"); "computation_is_run") (name-replace-l "current!1" "seq!1(t!1)" "current") ; added 08 11 01 - label added 12 12 01 (expand "disj_set")(expand "hset")(expand "help") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (try-grind :if-match nil) ;081101 -changed from grind (comment "Proving D1: is_P_state_valid(START_ELT implies (GOAL_ELT or disj_set(hset)), pfs)") ) (then (hide-all-but ("dist_rank"))(skosimp*) (label "rtp" 1) (exptemp) (skosimp*) (label "computation" -1) (label "hset" -2) (label "rho" -3) (label "tosplit" 2) (reach) (exptemp) ; (lemma-l "computation_is_run") ; (inst? "computation_is_run") (inst? "reachable")(simp) (inst "reachable" "t!1") ; (inst? "reachable")(simp) ; (inst "reachable" "t!1") ; (expand "state_pair")(skosimp*) (name-replace-l "current!1" "seq!1(t!1)" "current") ; (HIDE "computation" "computation_is_run") (hide "computation") (expand "rank") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (expand-expected-names) (expand "state_help")(expand "helppred") ; (EXP-JUSTICE) (expand "restrict") (expand "pfs" "rho") (expand "rho") (expand "disj_set") (spread (split-and "tosplit" "tohide") ((then (label "rtp" "tohide") (label "same" 1)(label "dec" 2) (if (eq split-rho? 't)(split-rho)(skip)) (comment "Proving D2 : is_P_state_valid((lambda st: forall next: hset(d)(st) and pfs`rho(st, next) and not GOAL_ELT(next) implies ((hset(d)(next) or disj_set(hset)(next) and exists r : rank(r)(st) > rank(r)(next))))) ") ) (then ; Added label 08 11 01 - labeling nad hiding the assertion that there is some ; h' in the next sequent, and some decreasing rank i.e. D2 ; (label "hset_p" -1)(hide "hset_p") 05 02 02 ; removed as possibly not at -1 (hide "tohide")(label "rtp" "tosplit") (if (eq split-rho? 't)(split-rho)(skip)) (comment "Proving D3 : is_P_state_valid((lambda st: forall next: hset(d)(st) and pfs`rho(st, next) and not GOAL_ELT(next) implies forall r : rank(r)(st) >= rank(r)(next), pfs)") )))) (then (hide-all-but ("dist_rank"))(exptemp)(skosimp*) (label "initialized_run" -1) (label "hset" -2) (label "justice" -3) (reach)(exptemp) (inst? "reachable")(simp)(inst "reachable" "t!1") (expand-expected-names) (hide "initialized_run") (EXPand "pfs")(expand "justice") (name-replace-l "current!1" "seq!1(t!1)" "current") ;added 08 11 01 (expand inv1)(expand inv2)(expand inv3)(expand inv4) (comment "Proving is_valid(IMPLIES(hset(d), not(pfs`justice(d))))") ) ) ) ) "lemma DIST_RANK. The optional parameters inv1, inv2, inv3 and inv4 are names of expressions to be expanded. If split-rho? is set to t, (default f) then split-rho is applied." "lemma DIST_RANK" ) (defstep DIST_RANK_simple (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil) (split-rho? f)) ; rewritten 2002-04-16 from dist_rank_viable (then (lemma "DIST_RANK_simple") (skosimp*)(inst? -) (label "dist_rank" -1) (spread (spsi "dist_rank") ((then (hide-all-but ("dist_rank"))(exptemp)(skosimp*) (label "computation" -1) (reach) (exptemp) ; (lemma-l "computation_is_run") ; (inst? "computation_is_run") (inst? "reachable")(simp) (inst "reachable" "t!1") (hide "computation") ; "computation_is_run") (name-replace-l "current!1" "seq!1(t!1)" "current") ; added 08 11 01 - label added 12 12 01 (expand "disj_set")(expand "hset")(expand "help") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (try-grind) ;081101 -changed from grind (comment "Proving D1: is_P_state_valid(START_ELT implies (GOAL_ELT or disj_set(hset)), pfs)") ) (then (hide-all-but ("dist_rank"))(skosimp*) (label "rtp" 1) (exptemp) (skosimp*) (label "computation" -1) (label "hset" -2) (label "rho" -3) (label "tosplit" 2) (reach) (exptemp) ; (lemma-l "computation_is_run") ; (inst? "computation_is_run") (inst? "reachable")(simp) (inst "reachable" "t!1") ; (inst? "reachable")(simp) ; (inst "reachable" "t!1") ; (expand "state_pair")(skosimp*) (name-replace-l "current!1" "seq!1(t!1)" "current") (HIDE "computation"); "computation_is_run") (expand "rank") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (expand-expected-names) (expand "state_help")(expand "helppred") ; (EXP-JUSTICE) (expand "restrict") (expand "pfs" "rho") (expand "rho") (expand "disj_set") (spread (split-and "tosplit" "tohide") ((then (label "rtp" "tohide") (label "same" 1)(label "dec" 2) (if (eq split-rho? 't)(split-rho)(skip)) (comment "Proving D2 : is_P_state_valid((lambda st: forall next: hset(d)(st) and pfs`rho(st, next) and not GOAL_ELT(next) implies ((hset(d)(next) or disj_set(hset)(next) and exists r : rank(r)(st) > rank(r)(next))))) ") ) (then (hide "tohide")(label "rtp" "tosplit") (if (eq split-rho? 't)(split-rho)(skip)) (comment "Proving D3 : is_P_state_valid((lambda st: forall next: hset(d)(st) and pfs`rho(st, next) and not GOAL_ELT(next) implies forall r : rank(r)(st) >= rank(r)(next), pfs)") )))) (then (hide-all-but ("dist_rank"))(exptemp)(skosimp*) (label "initialized_run" -1) (label "hset" -2) (label "justice" -3) (reach)(exptemp) (inst? "reachable")(simp)(inst "reachable" "t!1") (expand-expected-names) (hide "initialized_run") (EXPand "pfs")(expand "justice") (name-replace-l "current!1" "seq!1(t!1)" "current") ;added 08 11 01 (expand inv1)(expand inv2)(expand inv3)(expand inv4) (comment "Proving is_valid(IMPLIES(hset(d), not(pfs`justice(d))))") ) ) ) ) "lemma DIST_RANK_simple. The optional parameters inv1, inv2, inv3 and inv4 are names of expressions to be expanded. If split-rho? is set to t, (default f) then split-rho is applied." "lemma DIST_RANK_simple" ) (defstep DIST_RANK_direct (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil) (split-rho? f)) ; written 2002-10-24 from dist_rank_simple (then (lemma "DIST_RANK_direct") (label "dist_rank" -1) (spread (spsi "dist_rank") ((then (hide-all-but ("dist_rank"))(exptemp)(skosimp*) (label "computation" -1) (reach) (exptemp) ; (lemma-l "computation_is_run") ; (inst? "computation_is_run") (inst? "reachable")(simp) (inst "reachable" "t!1") (hide "computation"); "computation_is_run") (name-replace-l "current!1" "seq!1(t!1)" "current") ; added 08 11 01 - label added 12 12 01 (expand "disj_set")(expand "hset")(expand "help") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (try-grind) ;; grind-one removed as autorewrites and causes errors ;; if try to use use-invariant 30 10 02 (comment "Proving D1: is_P_state_valid(START_ELT implies (GOAL_ELT or exists d: hset(d)), pfs)") ) (then (hide-all-but ("dist_rank")) (label "rtp" 1) (exptemp) (skosimp*) (label "computation" -1) (label "hset" -2) (label "rho" -3) (label "tosplit" 2) (reach) (exptemp) ; (lemma-l "computation_is_run") ; (inst? "computation_is_run") (inst? "reachable")(simp) (inst "reachable" "t!1") (name-replace-l "current!1" "seq!1(t!1)" "current") (HIDE "computation"); "computation_is_run") (expand "rank") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (expand-expected-names) (expand "state_help")(expand "helppred") ; (EXP-JUSTICE) (expand "restrict") (expand "pfs" "rho") (expand "rho") (expand "disj_set") (spread (split-and "tosplit" "tohide") ((then (label "rtp" "tohide") (label "same" 1)(label "dec" 2) (try (spread (split "rho") ((then (replace "rho")(hide "dec")(simp)(split-all "hset")(fail)) (skip)))(skosimp*)(skip)) (if (eq split-rho? 't)(split-rho)(skip)) (comment "Proving D2 : is_P_state_valid((lambda st: forall next: hset(d)(st) and pfs`rho(st, next) and not GOAL_ELT(next) implies ((hset(d)(next) or exists e : (hset(e))(next) and rank(d)(st) > rank(d)(next))))) ") ) (then (hide "tohide")(label "rtp" "tosplit") (try (spread (split "rho") ((then (replace "rho")(hide-all-but "rtp")(split-all)(fail)) (skip)))(skosimp*)(skip)) (if (eq split-rho? 't)(split-rho)(skip)) (comment "Proving D3 : is_P_state_valid((lambda st: forall next: hset(d)(st) and pfs`rho(st, next) and not GOAL_ELT(next) implies forall r : rank(r)(st) >= rank(r)(next), pfs)") )))) (then (hide-all-but ("dist_rank"))(exptemp)(skosimp*) (label "initialized_run" -1) (label "hset" -2) (label "justice" -3) (reach)(exptemp) (inst? "reachable")(simp)(inst "reachable" "t!1") (expand-expected-names) (hide "initialized_run") (EXPand "pfs")(expand "justice") (name-replace-l "current!1" "seq!1(t!1)" "current") ;added 08 11 01 (expand inv1)(expand inv2)(expand inv3)(expand inv4) (comment "Proving is_valid(IMPLIES(hset(d), not(pfs`justice(d))))") ) ) ) ) "lemma DIST_RANK_direct. The optional parameters inv1, inv2, inv3 and inv4 are names of expressions to be expanded. If split-rho? is set to t, (default f) then split-rho is applied." "lemma DIST_RANK_direct" ) (defstep DIST_RANK_pend (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil) (split-rho? f)) ; written 2002-10-24 from dist_rank_simple (then (lemma "DIST_RANK_pend") (label "dist_rank" -1) (spread (spsi "dist_rank") ((then (hide-all-but ("dist_rank"))(exptemp)(skosimp*) (label "computation" -1)(reach) (exptemp) ; (lemma-l "computation_is_run") ; (inst? "computation_is_run") (inst? "reachable")(simp) (inst "reachable" "t!1") (hide "computation") ;"computation_is_run") (name-replace-l "current!1" "seq!1(t!1)" "current") (expand "disj_set")(expand "hset")(expand "help") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (try-grind) (comment "Proving D1: is_P_state_valid(START_ELT implies (GOAL_ELT or PEND, pfs)") ) (then (hide-all-but ("dist_rank"))(exptemp)(skosimp*) (label "initialized_run" -1) (label "pend" -2) (label "rtp" +) (reach) (exptemp) (inst? "reachable")(simp) (inst "reachable" "t!1") (hide "initialized_run") (name-replace-l "current!1" "seq!1(t!1)" "current") (expand "disj_set")(expand "hset")(expand "help") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (try-grind) (comment "Proving D2: is_P_reachable_valid(PEND implies (GOAL_ELT or EXISTS d: hset(d), pfs)") ) (then (hide-all-but ("dist_rank")) (label "rtp" 1) (exptemp) (skosimp*) (label "computation" -1) (label "hset" -2) (label "rho" -3) (label "tosplit" 2) (reach) (exptemp) ; (lemma-l "computation_is_run") ; (inst? "computation_is_run") (inst? "reachable")(simp) (inst "reachable" "t!1") (name-replace-l "current!1" "seq!1(t!1)" "current") (HIDE "computation") ; "computation_is_run") (expand "rank") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (expand-expected-names) (expand "state_help")(expand "helppred") ; (EXP-JUSTICE) (expand "restrict") (expand "pfs" "rho") (expand "rho") (expand "disj_set") (spread (split-and "tosplit" "tohide") ((then (label "pend" "tohide") (if (eq split-rho? 't)(split-rho)(skip)) (comment "Proving D : is_P_state_valid((lambda current: forall next: hset(d)(current) and pfs`rho(current, next) and not GOAL_ELT(next) implies hset(d)(next) or rank(current)(d) > rank(next)(d) ") ) (then (label "pend" "tohide")(label "rtp" "tosplit") (try (spread (split "rho") ((then (replace "rho")(hide-all-but "rtp")(split-all)(fail)) (skip)))(skosimp*)(skip)) (if (eq split-rho? 't)(split-rho)(skip)) (comment "Proving D4 : is_P_state_valid((lambda st: forall next: hset(d)(st) and pfs`rho(st, next) and not GOAL_ELT(next) implies hset(d)(next) or (rank(d)(st) > rank(d)(next))), pfs)") )))) (then (hide-all-but ("dist_rank")) (label "rtp" 1) (exptemp) (skosimp*) (label "computation" -1) (label "pend" -2) (label "rho" -3) (reach) (exptemp) ; (lemma-l "computation_is_run") ; (inst? "computation_is_run") (inst? "reachable")(simp) (inst "reachable" "t!1") (name-replace-l "current!1" "seq!1(t!1)" "current") (HIDE "computation"); "computation_is_run") (expand "rank") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (expand-expected-names) (expand "state_help")(expand "helppred") (expand "restrict") (expand "pfs" "rho") (expand "rho") (expand "disj_set") (if (eq split-rho? 't)(split-rho)(skip)) (comment "Proving D5 : is_P_state_valid((lambda current: forall next: pend(current) and pfs`rho(current, next) and not GOAL_ELT(next) implies forall d: rank(current)(d) > rank(next)(d)") ) (then (hide-all-but ("dist_rank"))(exptemp)(skosimp*) (label "initialized_run" -1) (label "hset" -2) (label "justice" -3) (reach)(exptemp) (inst? "reachable")(simp)(inst "reachable" "t!1") (expand-expected-names) (hide "initialized_run") (EXPand "pfs")(expand "justice") (name-replace-l "current!1" "seq!1(t!1)" "current") ;added 08 11 01 (expand inv1)(expand inv2)(expand inv3)(expand inv4) (try-grind) (comment "Proving D6: is_valid(IMPLIES(hset(d), not(pfs`justice(d))))") ) ) ) ) "lemma DIST_RANK_pend. The optional parameters inv1, inv2, inv3 and inv4 are names of expressions to be expanded. If split-rho? is set to t, (default f) then split-rho is applied." "lemma DIST_RANK_pend" ) (defstep well_simple (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil)(split-rho? f)) (then (lemma "WELL_simple")(label "well" -1) (skosimp*) (expand inv1)(expand inv2)(expand inv3)(expand inv4) (spread (spsi "well") ((then (hide-all-but ("well"))(exptemp)(skosimp*) (label "computation" -1) (reach) (exptemp) ; (lemma-l "computation_is_run") ; (inst? "computation_is_run") (inst? "reachable")(simp) (inst "reachable" "t!1") (hide "computation") ; "computation_is_run") (name-replace-l "current!1" "seq!1(t!1)" "current") (expand "disj_set")(expand "hset")(expand "help") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (try-grind) (comment "Proving W1 :is_P_state_valid(START_ELT implies (GOAL_ELT or disj_set(hset)), pfs)") ) (then (hide-all-but ("well")) (label "rtp" 1) (exptemp) (skosimp*) (simp) (label "computation" -1) (label "hset" -2) (label "rho" -3) (label "dec" 2 :push? t) (label "same" 3 :push? t) (reach)(exptemp) ; (lemma-l "computation_is_run") ; (inst? "computation_is_run") (inst? "reachable")(simp) (inst "reachable" "t!1") (expand "phi")(expand "hset")(expand "dset") (expand "rank") (expand "help") (expand "restrict") (name-replace-l "current!1" "seq!1(t!1)" "current") (hide "computation") ; "computation_is_run") (expand "pfs") (expand "rho") (expand "justice") ; (hide "reachable") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (if (eq split-rho? 't)(split-rho)(skip)) (comment "Proving W2 : forall d : is_P_state_valid((lambda st: forall next: hset(d)(st) and pfs`rho(st, next) implies GOAL_ELT(next) or (exists e : hset(e)(next) and gt(rank(d)(st), rank(e)(next))) or hset(d)(next) and rank(d)(next) = rank(d)(st) and not jset(d)(next)), pfs)") ) )) ) "lemma WELL. The optional parameters inv1, inv2, inv3 and inv4 are names of expressions to be expanded. If split-rho? is set to t, (default f) then split-rho is applied." "lemma WELL_simple" ) (defstep PREORDER (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil) (split-rho? f)) (then (lemma "PREORDER")(label "preorder" -1) (expand inv1)(expand inv2)(expand inv3)(expand inv4) (spread (spsi "preorder") ((then (hide-all-but ("preorder"))(exptemp)(skosimp*) (label "computation" -1) (reach) (exptemp) (inst? "reachable")(simp) (inst "reachable" "t!1") (hide "computation") ; "computation_is_run") (name-replace-l "current!1" "seq!1(t!1)" "current") (expand "disj_set")(expand "hset")(expand "help") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (try-grind) (comment "Proving P1 :is_P_state_valid(START_ELT implies (GOAL_ELT or PHI), pfs)")) (then (hide-all-but ("preorder"))(skosimp*) (label "rtp" 1) (exptemp) (skosimp*) (label "computation" -1) (label "hset" -2) (label "rho" -3) (reach)(exptemp) (inst? "reachable")(simp) (inst "reachable" "t!1") (name-replace-l "current!1" "seq!1(t!1)" "current") (HIDE "computation" "current") ; "computation_is_run") (expand "phi")(expand "hset")(expand "dset") (expand "rank") (expand "help")(expand "just") (expand "PHI") (expand "restrict") (expand "pfs" "rho") (expand "rho") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (spread (with-labels (split-and "rtp")(("temp" "rtp"))) ((then (label "same" 1)(label "dec" 2) (if (eq split-rho? 't)(split-rho)(skip)) (comment "Proving is_P_state_valid((lambda st: forall next: forall d: hset(d)(st) and pfs`rho(st, next) and not GOAL_ELT(next) implies ((hset(d)(next) or PHI(next) and exists r : rank(r)(st) > rank(r)(next)))), pfs)") ) (then (label "rtp" "temp" :push? t)(hide "temp")(if (eq split-rho? 't)(split-rho)(skip)) (comment "Proving is_P_state_valid((lambda st: forall next: forall d: hset(d)(st) and pfs`rho(st, next) and not GOAL_ELT(next) implies forall r : rank(r)(st) >= rank(r)(next)), pfs)") ) ) ) ) (then (hide-all-but ("preorder"))(exptemp)(skosimp*) (label "initialized_run" -1) (label "hset" -2) (label "justice" -3) (reach)(exptemp) (inst? "reachable")(simp)(inst "reachable" "t!1") (hide "initialized_run") (expand "phi")(expand "hset")(expand "dset") (expand "rank") (expand "help")(expand "jset")(expand "just") (expand "PHI") (EXP-JUSTICE) (name-replace-l "current!1" "seq!1(t!1)" "current") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (comment "Proving is_P_reachable_valid(G(IMPLIES(hset(d!1) , not(pfs`justice(d!1)))) , pfs)") ) (then (hide-all-but "preorder") (exptemp)(skosimp*) (label "initialized_run" -1) (label "phi" -2)(label "min" -3) (label "hset" 1) (reach)(exptemp) (inst? "reachable")(simp) (inst "reachable" "t!1")(hide "initialized_run") (expand "min")(expand "mind") (expand "preorder")(expand "pre_order")(expand "preord") (expand "phi")(expand "hset")(expand "dset") (expand "rank") (expand "PHI") (expand "reachable") (name-replace-l "current!1" "seq!1(t!1)" "current") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (hide "current") (comment "Proving is_P_reachable_valid(G(IMPLIES(PHI and min(d!1), hset(d!1))), pfs)") ) ) ) ) "lemma PREORDER. The optional parameters inv1, inv2, inv3 and inv4 are names of expressions to be expanded. If split-rho? is set to t, (default f) then split-rho is applied." "lemma PREORDER" ) ;; Strategies not designed for external use (defstep lemLtStrict () (then (lemma "ltIsStrict")(label "ltIsStrict" -1)(inst? -)(simp)(label "linear" -1 :push? t)(label "trans" -2 :push? t)) "introduces ltIsStrict lemma" "introduces ltIsStrict lemma" ) (defstep dist_rank (&optional (inv1 nil)(inv2 nil)(inv3 nil)(inv4 nil) (split-rho? f)) (then (lemma "DIST_RANK") (skosimp*) (label "dist_rank" -1) (expand* inv1 inv2 inv3 inv4) (spread (spsi "dist_rank") ((then (hide-all-but ("dist_rank"))(exptemp)(skosimp*) (label "computation" -1) (reach) (exptemp) (inst? "reachable")(simp) (inst "reachable" "t!1") (hide "computation") ; (name-replace-l "current!1" "seq!1(t!1)" "current") (expand "disj_set")(expand "hset")(expand "help") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (comment "Proving D1: is_P_state_valid(START_ELT implies (GOAL_ELT or disj_set(hset)), pfs)") ) (then (hide-all-but ("dist_rank"))(exptemp)(skosimp*) (label "computation" -1) (lemma-l "finite_support")(exptemp)(skosimp*)(inst? -)(simp) (comment "Proving the support is finite")) (then (hide-all-but ("dist_rank"))(skosimp*) (label "rtp" 1) (exptemp) (skosimp*) (label "computation" -1) (label "hset" -2) (label "rho" -3) (reach)(exptemp) (inst? "reachable")(simp) (inst "reachable" "t!1") (name-replace-l "current!1" "seq!1(t!1)" "current") (hide "computation") ;(expand "rank") (expand-expected-names) (expand "restrict") (expand "pfs" "rho") (expand "rho") (expand "disj_set") (expand inv1)(expand inv2)(expand inv3)(expand inv4) (spread (split-and "rtp") ( (then (label "same" 1)(label "dec" 2) (expand "rank")(expand "restrict") (if (eq split-rho? 't)(split-rho)(skip)) (comment "Proving D3 :is_P_state_valid((lambda st: forall next: forall d: hset(d)(st) and pfs`rho(st, next) and not GOAL_ELT(next) implies (hset(d)(next) or ((exists e : hset(e)(next)) and rank(d)(st) > rank(d)(next)) pfs)") ) (then (label "hset_p" -1)(hide "hset_p") (expand "rank")(expand "restrict") (if (eq split-rho? 't)(split-rho)(skip)) (comment "Proving D3 : is_P_state_valid((lambda st: forall next: hset(d)(st) and pfs`rho(st, next) and not GOAL_ELT(next) implies forall r : rank(r)(st) >= rank(r)(next), pfs)") ) ))) (then (hide-all-but ("dist_rank"))(exptemp)(skosimp*) (label "computation" -1) (label "hset" -2) (label "justice" -3) (reach)(exptemp) (inst? "reachable")(simp)(inst "reachable" "t!1") (expand-expected-names) (hide "computation") (expand "pfs")(expand "justice") (name-replace-l "current!1" "seq!1(t!1)" "current") ;added 08 11 01 (expand inv1)(expand inv2)(expand inv3)(expand inv4) (comment "Proving is_valid(IMPLIES(hset(d), not(pfs`justice(d))))"))))) "The optional parameters inv1, inv2, inv3 and inv4 are names of expressions to be expanded. If split-rho? is set to t, (default f) then split-rho is applied." "lemma DIST_RANK" ) (defstep old_finite_support () (then (label "rtp" 1)(lemma-l "finite_support") (spread (spsi -) ((skip) (fail))) (then (hide-all-but "finite_support")(skosimp*) (spread (spsi) ((try (then (expand "is_finite_type") (then (inst + "2" "lambda (d : FAIRNESS_DOMAIN) : 0") (simp)(lazygrind)(fail))) (skip)(comment "Proving that a finite number of fair domain elements are not dormant in the initial state")) (then (try-lazygrind) (comment "The rank of a dormand fair domain element should be 0")) (try (try (then (typepred "seq!1")(try-lazygrind)) (fail)(skip)) (skip) (comment "Only domain elements of one process can be activated in a single step") ) ) ) ) ) "Invokes lemma finite_support from finite_support_dormant to try to complete the proof" "Invokes lemma finite_support to try to complete the proof" ) (defstep finite_support () (then (label "rtp" 1)(lemma-l "finite_support") (spread (spsi "finite_support") ((skip) (then (comment "Could not apply finite_support lemma")(fail)))) (then (hide-all-but "finite_support")(skosimp*) (spread (spsi) ((try (then (expand "is_finite_type") (then (inst + "2" "lambda (d : FAIRNESS_DOMAIN) : 0") (simp)(lazygrind)(fail))) (skip) (then (label "initial" -1)(expand* "pfs" "initial" "is_finite_type" "injective?" "theta")(comment "Proving that a finite number of fair domain elements are not dormant in the initial state"))) (then (try-lazygrind) (comment "The rank of a dormant fair domain element should be 0")) (try (try (then (typepred "seq!1")(try-lazygrind)) (fail)(skip)) (skip) (then (skosimp*) (try (typepred "seq!1") (then (label "computation" -1) (expand* "computation" "consecution") (flatten "computation") (label "rho" -2) (hide "computation") (expand "pfs" "rho") (expand "rho") (inst "rho" "t!1") (try (spread (then (split-idle)(simp))((skip)(fail))) (skip)(skip))) (skip)) (comment "Only domain elements of one process can be activated in a single step") ) ) ) ) ) ) "Invokes lemma finite_support from finite_support_dormant to try to complete the proof" "Invokes lemma finite_support to try to complete the proof" ) (defstep FAIRNESS_DOMAIN_countable () (then (label "rtp" 1) (LEMMA-L "FAIRNESS_DOMAIN_is_countable") (try-lazygrind) ) "Invokes lemma FAIRNESS_DOMAIN_is_countable from FAIRNESS_DOMAIN_unbounded to prove that the FAIRNESS_DOMAIN is countable" "Invokes lemma FAIRNESS_DOMAIN_is_countable to try to complete the proof" )