Generate a version of exec-stmt-while
specialized to the loop represented by
(atc-gen-exec-stmt-while-for-loop fn loop-stmt prog-const names-to-avoid wrld) → (mv events exec-stmt-while-for-fn exec-stmt-while-for-fn-thm updated-names-to-avoid)
The correctness theorem for a loop says that
the execution of the loop (via exec-stmt-while)
is suitably equivalent to
the corresponding ACL2 recursive function
What we really need is an induction scheme related to the loop.
Thus we introduce a local function that is like exec-stmt-while
but specialized to the loop generated from
Function:
(defun atc-gen-exec-stmt-while-for-loop (fn loop-stmt prog-const names-to-avoid wrld) (declare (xargs :guard (and (symbolp fn) (stmtp loop-stmt) (symbolp prog-const) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (declare (xargs :guard (and (irecursivep+ fn wrld) (stmt-case loop-stmt :while)))) (let ((__function__ 'atc-gen-exec-stmt-while-for-loop)) (declare (ignorable __function__)) (b* ((loop-test (stmt-while->test loop-stmt)) (loop-body (stmt-while->body loop-stmt)) (exec-stmt-while-for-fn (packn-pos (list 'exec-stmt-while-for- fn) fn)) ((mv exec-stmt-while-for-fn names-to-avoid) (fresh-logical-name-with-$s-suffix exec-stmt-while-for-fn 'function names-to-avoid wrld)) (exec-stmt-while-for-fn-body (cons 'b* (cons (cons (cons 'fenv (cons (cons 'init-fun-env (cons (cons 'preprocess (cons prog-const 'nil)) 'nil)) 'nil)) (cons '((when (zp limit)) (mv (error :limit) (compustate-fix compst))) (cons (cons 'test-eval (cons (cons 'exec-expr-pure (cons (cons 'quote (cons loop-test 'nil)) '(compst))) 'nil)) (cons '((when (errorp test-eval)) (mv test-eval (compustate-fix compst))) (cons '(test-eval (apconvert-expr-value test-eval)) (cons '((when (errorp test-eval)) (mv test-eval (compustate-fix compst))) (cons '(test-val (expr-value->value test-eval)) (cons '(continuep (test-value test-val)) (cons '((when (errorp continuep)) (mv continuep (compustate-fix compst))) (cons '((when (not continuep)) (mv nil (compustate-fix compst))) (cons (cons '(mv val? compst) (cons (cons 'exec-stmt (cons (cons 'quote (cons loop-body 'nil)) '(compst fenv (1- limit)))) 'nil)) '(((when (errorp val?)) (mv val? compst)) ((when (valuep val?)) (mv val? compst)))))))))))))) (cons (cons exec-stmt-while-for-fn '(compst (1- limit))) 'nil)))) (exec-stmt-while-for-fn-hints '(("Goal" :in-theory '(acl2::zp-compound-recognizer nfix natp o-p o-finp o<)))) ((mv exec-stmt-while-for-fn-event &) (evmac-generate-defun exec-stmt-while-for-fn :formals (list 'compst 'limit) :body exec-stmt-while-for-fn-body :measure '(nfix limit) :well-founded-relation 'o< :hints exec-stmt-while-for-fn-hints :verify-guards nil :enable nil)) (exec-stmt-while-for-fn-thm (add-suffix-to-fn exec-stmt-while-for-fn "-TO-EXEC-STMT-WHILE")) ((mv exec-stmt-while-for-fn-thm names-to-avoid) (fresh-logical-name-with-$s-suffix exec-stmt-while-for-fn-thm nil names-to-avoid wrld)) ((mv exec-stmt-while-for-fn-thm-event &) (evmac-generate-defthm exec-stmt-while-for-fn-thm :formula (cons 'equal (cons (cons exec-stmt-while-for-fn '(compst limit)) (cons (cons 'exec-stmt-while (cons (cons 'quote (cons loop-test 'nil)) (cons (cons 'quote (cons loop-body 'nil)) (cons 'compst (cons (cons 'init-fun-env (cons (cons 'preprocess (cons prog-const 'nil)) 'nil)) '(limit)))))) 'nil))) :rule-classes nil :hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons exec-stmt-while-for-fn '(exec-stmt-while)) 'nil)) 'nil))) 'nil)))) (mv (list exec-stmt-while-for-fn-event exec-stmt-while-for-fn-thm-event) exec-stmt-while-for-fn exec-stmt-while-for-fn-thm names-to-avoid))))
Theorem:
(defthm pseudo-event-form-listp-of-atc-gen-exec-stmt-while-for-loop.events (b* (((mv ?events ?exec-stmt-while-for-fn ?exec-stmt-while-for-fn-thm ?updated-names-to-avoid) (atc-gen-exec-stmt-while-for-loop fn loop-stmt prog-const names-to-avoid wrld))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atc-gen-exec-stmt-while-for-loop.exec-stmt-while-for-fn (b* (((mv ?events ?exec-stmt-while-for-fn ?exec-stmt-while-for-fn-thm ?updated-names-to-avoid) (atc-gen-exec-stmt-while-for-loop fn loop-stmt prog-const names-to-avoid wrld))) (symbolp exec-stmt-while-for-fn)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atc-gen-exec-stmt-while-for-loop.exec-stmt-while-for-fn-thm (b* (((mv ?events ?exec-stmt-while-for-fn ?exec-stmt-while-for-fn-thm ?updated-names-to-avoid) (atc-gen-exec-stmt-while-for-loop fn loop-stmt prog-const names-to-avoid wrld))) (symbolp exec-stmt-while-for-fn-thm)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-exec-stmt-while-for-loop.updated-names-to-avoid (implies (symbol-listp names-to-avoid) (b* (((mv ?events ?exec-stmt-while-for-fn ?exec-stmt-while-for-fn-thm ?updated-names-to-avoid) (atc-gen-exec-stmt-while-for-loop fn loop-stmt prog-const names-to-avoid wrld))) (symbol-listp updated-names-to-avoid))) :rule-classes :rewrite)