|
|
|---|
|
|
|
|---|
Generate a theorem for the transformation of a pure expression.
(simpadd0-gen-expr-pure-thm old
new vartys const-new thm-index hints)
→
(mv thm-event thm-name updated-thm-index)This function takes the old and new expressions as inputs, which must satisfy expr-pure-formalp. If the two expressions are syntactically equal, the generated theorem just says that if the execution of the expression does not yield an error, then the resulting value has the type of the expression. If the two expressions are not syntactically equal, the theorem also says that if the result of executing the old expression is not an error then neither is the result of executing the new expression, and the values of the two results are equal.
Note that the calls of ldm-expr in the theorem are known to succeed (i.e. not return any error), given that expr-pure-formalp holds.
This function also takes as input a map from identifiers to types, which are the variables in scope with their types. The theorem includes a hypothesis for each of these variables, saying that they are in the computation state and that they contain values of the appropriate types.
The hints to prove the theorem are passed as input too, since the proof varies depending on the kind of expression.
Function:
(defun simpadd0-gen-expr-pure-thm (old new vartys const-new thm-index hints) (declare (xargs :guard (and (exprp old) (exprp new) (ident-type-mapp vartys) (symbolp const-new) (posp thm-index) (true-listp hints)))) (declare (xargs :guard (and (expr-unambp old) (expr-unambp new)))) (let ((__function__ 'simpadd0-gen-expr-pure-thm)) (declare (ignorable __function__)) (b* ((old (expr-fix old)) (new (expr-fix new)) ((unless (expr-pure-formalp old)) (raise "Internal error: ~x0 is not in the formalized subset." old) (mv '(_) nil 1)) (equalp (equal old new)) ((unless (or equalp (expr-pure-formalp new))) (raise "Internal error: ~x0 is not in the formalized subset." new) (mv '(_) nil 1)) (type (expr-type old)) ((unless (or equalp (equal (expr-type new) type))) (raise "Internal error: ~ the type ~x0 of the new expression ~x1 differs from ~ the type ~x2 of the old expression ~x3." (expr-type new) new type old) (mv '(_) nil 1)) (hyps (simpadd0-gen-var-hyps vartys)) ((unless (type-formalp type)) (raise "Internal error: expression ~x0 has type ~x1." old type) (mv '(_) nil 1)) ((mv & ctype) (ldm-type type)) (formula (if equalp (cons 'b* (cons (cons (cons 'expr (cons (cons 'mv-nth (cons '1 (cons (cons 'ldm-expr (cons (cons 'quote (cons old 'nil)) 'nil)) 'nil))) 'nil)) '((result (c::exec-expr-pure expr compst)) (value (c::expr-value->value result)))) (cons (cons 'implies (cons (cons 'and (append hyps '((not (c::errorp result))))) (cons (cons 'equal (cons '(c::type-of-value value) (cons (cons 'quote (cons ctype 'nil)) 'nil))) 'nil))) 'nil))) (cons 'b* (cons (cons (cons 'old-expr (cons (cons 'mv-nth (cons '1 (cons (cons 'ldm-expr (cons (cons 'quote (cons old 'nil)) 'nil)) 'nil))) 'nil)) (cons (cons 'new-expr (cons (cons 'mv-nth (cons '1 (cons (cons 'ldm-expr (cons (cons 'quote (cons new 'nil)) 'nil)) 'nil))) 'nil)) '((old-result (c::exec-expr-pure old-expr compst)) (new-result (c::exec-expr-pure new-expr compst)) (old-value (c::expr-value->value old-result)) (new-value (c::expr-value->value new-result))))) (cons (cons 'implies (cons (cons 'and (append hyps '((not (c::errorp old-result))))) (cons (cons 'and (cons '(not (c::errorp new-result)) (cons '(equal old-value new-value) (cons (cons 'equal (cons '(c::type-of-value old-value) (cons (cons 'quote (cons ctype 'nil)) 'nil))) 'nil)))) 'nil))) 'nil))))) (thm-name (packn-pos (list const-new '-thm- thm-index) const-new)) (thm-index (1+ (pos-fix thm-index))) (thm-event (cons 'defthmd (cons thm-name (cons formula (cons ':hints (cons hints 'nil))))))) (mv thm-event thm-name thm-index))))
Theorem:
(defthm pseudo-event-formp-of-simpadd0-gen-expr-pure-thm.thm-event (b* (((mv ?thm-event ?thm-name ?updated-thm-index) (simpadd0-gen-expr-pure-thm old new vartys const-new thm-index hints))) (pseudo-event-formp thm-event)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-simpadd0-gen-expr-pure-thm.thm-name (b* (((mv ?thm-event ?thm-name ?updated-thm-index) (simpadd0-gen-expr-pure-thm old new vartys const-new thm-index hints))) (symbolp thm-name)) :rule-classes :rewrite)
Theorem:
(defthm posp-of-simpadd0-gen-expr-pure-thm.updated-thm-index (b* (((mv ?thm-event ?thm-name ?updated-thm-index) (simpadd0-gen-expr-pure-thm old new vartys const-new thm-index hints))) (posp updated-thm-index)) :rule-classes :rewrite)
Theorem:
(defthm simpadd0-gen-expr-pure-thm-of-expr-fix-old (equal (simpadd0-gen-expr-pure-thm (expr-fix old) new vartys const-new thm-index hints) (simpadd0-gen-expr-pure-thm old new vartys const-new thm-index hints)))
Theorem:
(defthm simpadd0-gen-expr-pure-thm-expr-equiv-congruence-on-old (implies (c$::expr-equiv old old-equiv) (equal (simpadd0-gen-expr-pure-thm old new vartys const-new thm-index hints) (simpadd0-gen-expr-pure-thm old-equiv new vartys const-new thm-index hints))) :rule-classes :congruence)
Theorem:
(defthm simpadd0-gen-expr-pure-thm-of-expr-fix-new (equal (simpadd0-gen-expr-pure-thm old (expr-fix new) vartys const-new thm-index hints) (simpadd0-gen-expr-pure-thm old new vartys const-new thm-index hints)))
Theorem:
(defthm simpadd0-gen-expr-pure-thm-expr-equiv-congruence-on-new (implies (c$::expr-equiv new new-equiv) (equal (simpadd0-gen-expr-pure-thm old new vartys const-new thm-index hints) (simpadd0-gen-expr-pure-thm old new-equiv vartys const-new thm-index hints))) :rule-classes :congruence)