other
(in-package "FTY")
other
(include-book "centaur/fty/database" :dir :system)
other
(include-book "centaur/fty/fty-parseutils" :dir :system)
other
(include-book "std/lists/list-defuns" :dir :system)
other
(include-book "std/util/defrule" :dir :system)
other
(include-book "xdoc/constructors" :dir :system)
other
(include-book "std/omaps/core" :dir :system)
other
(include-book "kestrel/event-macros/proof-preparation" :dir :system)
other
(defxdoc defomap :parents (fty-extensions fty omaps) :short "Generate a <see topic='@(url fty::fty)'>fixtype</see> of <see topic='@(url omap::omaps)'>omaps</see> whose keys and values have specified fixtypes." :long (topstring (h3 "Include-book Form") (codeblock "(include-book "kestrel/fty/defomap" :dir :system)") (h3 "Introduction") (p "This is analogous to @(tsee fty::deflist), @(tsee fty::defalist), and @(tsee fty::defset). Besides the fixtype itself, this macro also generates some theorems about the fixtype. Future versions of this macro may generate more theorems, as needed.") (p "Aside from the recognizer, fixer, and equivalence for the fixtype, this macro does not generate any operations on the typed omaps. Instead, the " (seetopic "omap::omaps" "generic omap operations") " can be used on typed omaps. This macro generates theorems about the use of these generic operations on typed omaps.") (p "Future versions of this macro may be modularized to provide a ``sub-macro'' that generates only the recognizer and theorems about it, without the fixtype (and without the fixer and equivalence), similarly to @(tsee std::deflist) and @(tsee std::defalist). That sub-macro could be called @('omap::defomap').") (p "This macro differs from @(tsee fty::defmap), which generates an alist.") (h3 "General Form") (codeblock "(defomap type" " :key-type ..." " :val-type ..." " :pred ..." " :fix ..." " :equiv ..." " :parents ..." " :short ..." " :long ...") (h3 "Inputs") (desc "@('type')" (p "The name of the new fixtype.")) (desc "@(':key-type')" (p "The (existing) fixtype of the keys of the new map fixtype.")) (desc "@(':val-type')" (p "The (existing) fixtype of the values of the new map fixtype.")) (desc (list "@(':pred')" "@(':fix')" "@(':equiv')") (p "The name of the recognizer, fixer, and equivalence for the new fixtype.") (p "The defaults are @('type') followed by @('-p'), @('-fix'), and @('-equiv').")) (desc (list "@(':parents')" "@(':short')" "@(':long')") (p "These are used to generate XDOC documentation for the topic @('name').") (p "If any of these is not supplied, the corresponding component is omitted from the generated XDOC topic.")) (p "This macro currently does not perform a thorough validation of its inputs. Erroneous inputs may result in failures of the generated events. Errors should be easy to diagnose, also since this macro has a very simple and readable implementation. Future versions of this macro should perform more thorough input validation.") (h3 "Generated Events") (p "The following are generated, inclusive of XDOC documentation:") (ul (li "The recognizer, the fixer, the equivalence, and the fixtype.") (li "Several theorems about the recognizer, fixer, equivalence, and omap operations applied to this type of omaps."))))
other
(program)
other
(define check-flexomap-already-defined
(pred kwd-alist
our-fixtypes
ctx
state)
(declare (ignorable kwd-alist))
(b* (((when (< 1 (len our-fixtypes))) nil) (existing-formals (fgetprop pred 'formals t (w state)))
(already-defined (not (eq existing-formals t)))
(- (and already-defined
(cw "NOTE: Using existing definition of ~x0.~%"
pred)))
(- (or (not already-defined)
(eql (len existing-formals) 1)
(er hard?
ctx
"~x0 is already defined in an incompatible manner: it ~
should take exactly 1 input, but its formals are ~x1"
pred
existing-formals))))
already-defined))
other
(define check-flexomap-fix-already-defined (fix kwd-alist our-fixtypes ctx state) (declare (ignorable kwd-alist)) (b* (((when (< 1 (len our-fixtypes))) nil) (fix$inline (add-suffix fix *inline-suffix*)) (existing-formals (fgetprop fix$inline 'formals t (w state))) (already-defined (not (eq existing-formals t))) (- (and already-defined (cw "NOTE: Using existing definition of ~x0.~%" fix))) (- (or (not already-defined) (eql (len existing-formals) 1) (er hard? ctx "~x0 is already defined in an incompatible manner: it ~ should take exactly 1 input, but its formals are ~x1" fix existing-formals)))) already-defined))
other
(define flexomap-fns
(x)
(b* (((flexomap x)))
(list x.pred x.fix)))
other
(define flexomap-collect-fix/pred-pairs
(omap)
(b* (((flexomap omap) omap))
(append (and omap.key-type
omap.key-fix
(list (cons omap.key-fix omap.key-type)))
(and omap.val-type
omap.val-fix
(list (cons omap.val-fix omap.val-type))))))
other
(defconst *flexomap-keywords* '(:pred :fix :equiv :count :get :set :key-type :val-type :measure :measure-debug :xvar :parents :short :long))
other
(define parse-flexomap
(x xvar
our-fixtypes
fixtypes
state)
(b* (((cons name args) x) ((unless (symbolp name)) (raise "Malformed flexomap: ~x0: name must be a symbol"
x))
((mv pre-/// post-///) (split-/// name args))
((mv kwd-alist rest) (extract-keywords name
*flexomap-keywords*
pre-///
nil))
(kwd-alist (append kwd-alist
(table-alist 'defomap-defaults
(w state))))
((when rest) (raise "Malformed flexomap: ~x0: after kind should be a keyword/value omap."
name))
(key-type (getarg :key-type nil kwd-alist))
((unless (symbolp key-type)) (raise "Bad flexalist ~x0: Element type must be a symbol"
name))
((mv key-type
key-fix
key-equiv
key-recp) (get-pred/fix/equiv (getarg :key-type nil kwd-alist)
our-fixtypes
fixtypes))
(val-type (getarg :val-type nil kwd-alist))
((unless (symbolp val-type)) (raise "Bad flexalist ~x0: Element type must be a symbol"
name))
((mv val-type
val-fix
val-equiv
val-recp) (get-pred/fix/equiv (getarg :val-type nil kwd-alist)
our-fixtypes
fixtypes))
(pred (getarg! :pred (intern-in-package-of-symbol (cat (symbol-name name) "-P")
name)
kwd-alist))
(fix (getarg! :fix (intern-in-package-of-symbol (cat (symbol-name name) "-FIX")
name)
kwd-alist))
(equiv (getarg! :equiv (intern-in-package-of-symbol (cat (symbol-name name) "-EQUIV")
name)
kwd-alist))
(count (flextype-get-count-fn name kwd-alist))
(xvar (or (getarg :xvar xvar kwd-alist)
(car (find-symbols-named-x (getarg :measure nil kwd-alist)))
(intern-in-package-of-symbol "X" name)))
(measure (getarg! :measure `(acl2-count ,FTY::XVAR)
kwd-alist))
(already-defined (check-flexomap-already-defined pred
kwd-alist
our-fixtypes
'defomap
state))
(fix-already-defined (check-flexomap-fix-already-defined fix
kwd-alist
our-fixtypes
'defomap
state)))
(make-flexomap :name name
:pred pred
:fix fix
:equiv equiv
:count count
:key-type key-type
:key-fix key-fix
:key-equiv key-equiv
:val-type val-type
:val-fix val-fix
:val-equiv val-equiv
:measure measure
:kwd-alist (if post-///
(cons (cons :///-events post-///) kwd-alist)
kwd-alist)
:xvar xvar
:recp (or key-recp val-recp)
:already-definedp already-defined
:fix-already-definedp fix-already-defined)))
other
(define flexomap-predicate-def
(omap)
(b* (((flexomap omap)) (pkg (symbol-package-name omap.pred))
(pkg (if (equal pkg *main-lisp-package-name*)
"ACL2"
pkg))
(pkg-witness (pkg-witness pkg))
(y (intern-in-package-of-symbol "Y" pkg-witness))
(k (intern-in-package-of-symbol "K" pkg-witness))
(v (intern-in-package-of-symbol "V" pkg-witness))
(booleanp-of-pred (packn-pos (list 'booleanp-of- omap.pred)
pkg-witness))
(mapp-when-pred (packn-pos (list 'mapp-when- omap.pred)
pkg-witness))
(pred-of-tail (packn-pos (list omap.pred '-of-tail)
pkg-witness))
(key-pred-of-head-key-when-pred (packn-pos (list omap.key-type
'-of-head-key-when-
omap.pred)
pkg-witness))
(val-pred-of-head-val-when-pred (packn-pos (list omap.val-type
'-of-head-val-when-
omap.pred)
pkg-witness))
(pred-of-update (packn-pos (list omap.pred '-of-update)
pkg-witness))
(pred-of-update* (packn-pos (list omap.pred '-of-update*)
pkg-witness))
(pred-of-delete (packn-pos (list omap.pred '-of-delete)
pkg-witness))
(pred-of-delete* (packn-pos (list omap.pred '-of-delete*)
pkg-witness))
(key-pred-when-assoc-pred (packn-pos (list omap.key-type
'-when-assoc-
omap.pred
'-binds-free-
omap.xvar)
pkg-witness))
(key-pred-of-car-of-assoc-pred (packn-pos (list omap.key-type
'-of-car-of-assoc-
omap.pred)
pkg-witness))
(val-pred-of-cdr-of-assoc-pred (packn-pos (list omap.val-type
'-of-cdr-of-assoc-
omap.pred)
pkg-witness))
(val-pred-of-lookup-when-pred (packn-pos (list omap.val-type
'-of-lookup-when-
omap.pred)
pkg-witness))
(type-ref (concatenate 'string
"@(tsee "
(string-downcase (symbol-package-name omap.name))
"::"
(string-downcase (symbol-name omap.name))
")")))
(if omap.already-definedp
'(progn)
`(define ,FTY::OMAP.PRED
(,FTY::OMAP.XVAR)
:parents (,FTY::OMAP.NAME)
:short ,(CONCATENATE 'STRING "Recognizer for " FTY::TYPE-REF ".")
,@(IF FTY::OMAP.MEASURE
`(:MEASURE ,FTY::OMAP.MEASURE)
NIL)
,@(AND (FTY::GETARG :MEASURE-DEBUG NIL FTY::OMAP.KWD-ALIST) `(:MEASURE-DEBUG T))
(if (atom ,FTY::OMAP.XVAR)
(null ,FTY::OMAP.XVAR)
(and (consp (car ,FTY::OMAP.XVAR))
(,FTY::OMAP.KEY-TYPE (caar ,FTY::OMAP.XVAR))
(,FTY::OMAP.VAL-TYPE (cdar ,FTY::OMAP.XVAR))
(or (null (cdr ,FTY::OMAP.XVAR))
(and (consp (cdr ,FTY::OMAP.XVAR))
(consp (cadr ,FTY::OMAP.XVAR))
(fast-<< (caar ,FTY::OMAP.XVAR) (caadr ,FTY::OMAP.XVAR))
(,FTY::OMAP.PRED (cdr ,FTY::OMAP.XVAR))))))
:no-function t
///
(defrule ,FTY::BOOLEANP-OF-PRED
(booleanp (,FTY::OMAP.PRED ,FTY::OMAP.XVAR)))
(defrule ,FTY::MAPP-WHEN-PRED
(implies (,FTY::OMAP.PRED ,FTY::OMAP.XVAR)
(mapp ,FTY::OMAP.XVAR))
:rule-classes (:rewrite :forward-chaining)
:induct t
:enable mapp)
(defrule ,FTY::PRED-OF-TAIL
(implies (,FTY::OMAP.PRED ,FTY::OMAP.XVAR)
(,FTY::OMAP.PRED (tail ,FTY::OMAP.XVAR)))
:enable tail
:cases ((null (cdr ,FTY::OMAP.XVAR))))
(defrule ,FTY::KEY-PRED-OF-HEAD-KEY-WHEN-PRED
(implies (and (,FTY::OMAP.PRED ,FTY::OMAP.XVAR)
(not (emptyp ,FTY::OMAP.XVAR)))
(,FTY::OMAP.KEY-TYPE (mv-nth 0 (head ,FTY::OMAP.XVAR))))
:enable head)
(defrule ,FTY::VAL-PRED-OF-HEAD-VAL-WHEN-PRED
(implies (and (,FTY::OMAP.PRED ,FTY::OMAP.XVAR)
(not (emptyp ,FTY::OMAP.XVAR)))
(,FTY::OMAP.VAL-TYPE (mv-nth 1 (head ,FTY::OMAP.XVAR))))
:enable head)
(defrule ,FTY::PRED-OF-UPDATE
(implies (and (,FTY::OMAP.PRED ,FTY::OMAP.XVAR)
(,FTY::OMAP.KEY-TYPE ,FTY::K)
(,FTY::OMAP.VAL-TYPE ,FTY::V))
(,FTY::OMAP.PRED (update ,FTY::K ,FTY::V ,FTY::OMAP.XVAR)))
:induct t
:enable (update head tail)
,@(AND (NOT FTY::OMAP.RECP) '(:DISABLE ((:INDUCTION OMAP::UPDATE))))
:expand (,FTY::OMAP.PRED ,FTY::OMAP.XVAR))
(defrule ,FTY::PRED-OF-UPDATE*
(implies (and (,FTY::OMAP.PRED ,FTY::OMAP.XVAR)
(,FTY::OMAP.PRED ,FTY::Y))
(,FTY::OMAP.PRED (update* ,FTY::OMAP.XVAR ,FTY::Y)))
:induct t
:enable update*)
(defrule ,FTY::PRED-OF-DELETE
(implies (,FTY::OMAP.PRED ,FTY::OMAP.XVAR)
(,FTY::OMAP.PRED (delete ,FTY::K ,FTY::OMAP.XVAR)))
:induct t
:enable delete)
(defrule ,FTY::PRED-OF-DELETE*
(implies (,FTY::OMAP.PRED ,FTY::OMAP.XVAR)
(,FTY::OMAP.PRED (delete* ,FTY::K ,FTY::OMAP.XVAR)))
:induct t
:enable delete*)
(defrule ,FTY::KEY-PRED-WHEN-ASSOC-PRED
(implies (and (assoc ,FTY::K ,FTY::OMAP.XVAR)
(,FTY::OMAP.PRED ,FTY::OMAP.XVAR))
(,FTY::OMAP.KEY-TYPE ,FTY::K))
:induct t
:enable assoc)
(defrule ,FTY::KEY-PRED-OF-CAR-OF-ASSOC-PRED
(implies (and (,FTY::OMAP.PRED ,FTY::OMAP.XVAR)
(assoc ,FTY::K ,FTY::OMAP.XVAR))
(,FTY::OMAP.KEY-TYPE (car (assoc ,FTY::K ,FTY::OMAP.XVAR))))
:induct t
:enable assoc)
(defrule ,FTY::VAL-PRED-OF-CDR-OF-ASSOC-PRED
(implies (and (,FTY::OMAP.PRED ,FTY::OMAP.XVAR)
(assoc ,FTY::K ,FTY::OMAP.XVAR))
(,FTY::OMAP.VAL-TYPE (cdr (assoc ,FTY::K ,FTY::OMAP.XVAR))))
:induct t
:enable assoc)
(defrule ,FTY::VAL-PRED-OF-LOOKUP-WHEN-PRED
(implies (and (,FTY::OMAP.PRED ,FTY::OMAP.XVAR)
(assoc ,FTY::K ,FTY::OMAP.XVAR))
(,FTY::OMAP.VAL-TYPE (lookup ,FTY::K ,FTY::OMAP.XVAR)))
:enable lookup)))))
other
(define flexomap-fix-def (omap flagp) (b* (((flexomap omap)) (pred-of-fix (packn-pos (list omap.pred '-of- omap.fix) omap.name)) (fix-when-pred (packn-pos (list omap.fix '-when- omap.pred) omap.name)) (emptyp-fix (packn-pos (list 'emptyp- omap.fix) omap.name)) (emptyp-of-fix (packn-pos (list 'emptyp-of- omap.fix '-to-not- omap.name '-or-emptyp) omap.name))) (if omap.fix-already-definedp '(progn) `(define ,FTY::OMAP.FIX ((,FTY::OMAP.XVAR ,FTY::OMAP.PRED)) :parents (,FTY::OMAP.NAME) :short ,(FTY::CAT "@(call " (XDOC::FULL-ESCAPE-SYMBOL FTY::OMAP.FIX) ") is a usual @(see fty::fty) omap fixing function.") ,@(AND (FTY::GETARG :MEASURE-DEBUG NIL FTY::OMAP.KWD-ALIST) `(:MEASURE-DEBUG T)) ,@(AND FTY::FLAGP `(:FLAG ,FTY::OMAP.NAME)) :progn t (mbe :logic (if (,FTY::OMAP.PRED ,FTY::OMAP.XVAR) ,FTY::OMAP.XVAR nil) :exec ,FTY::OMAP.XVAR) :no-function t /// (defrule ,FTY::PRED-OF-FIX (,FTY::OMAP.PRED (,FTY::OMAP.FIX ,FTY::OMAP.XVAR))) (defrule ,FTY::FIX-WHEN-PRED (implies (,FTY::OMAP.PRED ,FTY::OMAP.XVAR) (equal (,FTY::OMAP.FIX ,FTY::OMAP.XVAR) ,FTY::OMAP.XVAR))) (defrule ,FTY::EMPTYP-FIX (implies (or (emptyp ,FTY::OMAP.XVAR) (not (,FTY::OMAP.PRED ,FTY::OMAP.XVAR))) (emptyp (,FTY::OMAP.FIX ,FTY::OMAP.XVAR)))) (defrule ,FTY::EMPTYP-OF-FIX (equal (emptyp (,FTY::OMAP.FIX ,FTY::OMAP.XVAR)) (or (not (,FTY::OMAP.PRED ,FTY::OMAP.XVAR)) (emptyp ,FTY::OMAP.XVAR))) :enable emptyp)))))
other
(define flexomap-fix-when-pred-thm
(x flagp)
(b* (((flexomap x)) (foo-fix-when-foo-p (intern-in-package-of-symbol (cat (symbol-name x.fix)
"-WHEN-"
(symbol-name x.pred))
x.fix)))
(if flagp
`(defthm ,FTY::FOO-FIX-WHEN-FOO-P
t
:skip t
:flag ,FTY::X.NAME)
'(progn))))
flexomap-countfunction
(defun flexomap-count (omap types) (b* (((flexomap omap)) ((unless omap.count) nil) (keycount (flextypes-find-count-for-pred omap.key-type types)) (keycount (or keycount 'acl2-count)) (valcount (flextypes-find-count-for-pred omap.val-type types)) (valcount (or valcount 'acl2-count))) `((define ,FTY::OMAP.COUNT ((,FTY::OMAP.XVAR ,FTY::OMAP.PRED)) :returns (count natp :rule-classes :type-prescription :hints ('(:expand (,FTY::OMAP.COUNT ,FTY::OMAP.XVAR) :in-theory (disable ,FTY::OMAP.COUNT)))) :measure (let ((,FTY::OMAP.XVAR (,FTY::OMAP.FIX ,FTY::OMAP.XVAR))) ,FTY::OMAP.MEASURE) ,@(AND (FTY::GETARG :MEASURE-DEBUG NIL FTY::OMAP.KWD-ALIST) `(:MEASURE-DEBUG T)) :verify-guards nil :no-function t :progn t (if (or (emptyp ,FTY::OMAP.XVAR) (not (,FTY::OMAP.PRED ,FTY::OMAP.XVAR))) 1 (mv-let (key val) (head ,FTY::OMAP.XVAR) (declare (ignorable key val)) (+ 1 ,@(AND FTY::KEYCOUNT `((,FTY::KEYCOUNT FTY::KEY))) ,@(AND FTY::VALCOUNT `((,FTY::VALCOUNT FTY::VAL))) (,FTY::OMAP.COUNT (tail ,FTY::OMAP.XVAR)))))))))
flexomap-count-post-eventsfunction
(defun flexomap-count-post-events (omap types) (b* (((flexomap omap)) ((unless omap.count) nil) (keycount (flextypes-find-count-for-pred omap.key-type types)) (keycount (or keycount 'acl2-count)) (valcount (flextypes-find-count-for-pred omap.val-type types)) (valcount (or valcount 'acl2-count)) (omap-count-of-update (intern-in-package-of-symbol (cat (symbol-name omap.count) "-OF-UPDATE") omap.count)) (omap-count-of-head (intern-in-package-of-symbol (cat (symbol-name omap.count) "-OF-HEAD") omap.count)) (omap-count-of-head-fix (intern-in-package-of-symbol (cat (symbol-name omap.count) "-OF-HEAD-FIX") omap.count)) (omap-count-of-tail (intern-in-package-of-symbol (cat (symbol-name omap.count) "-OF-TAIL") omap.count)) (omap-count-of-tail-fix (intern-in-package-of-symbol (cat (symbol-name omap.count) "-OF-TAIL-FIX") omap.count)) (omap-count-of-lookup (intern-in-package-of-symbol (cat (symbol-name omap.count) "-OF-LOOKUP") omap.count)) (omap-count-when-emptyp (intern-in-package-of-symbol (cat (symbol-name omap.count) "-WHEN-EMPTYP") omap.count)) (omap-count-when-not-emptyp (intern-in-package-of-symbol (cat (symbol-name omap.count) "-WHEN-NOT-EMPTYP") omap.count))) `((evmac-prepare-proofs) (defthm ,FTY::OMAP-COUNT-WHEN-EMPTYP (implies (emptyp ,FTY::OMAP.XVAR) (equal (,FTY::OMAP.COUNT ,FTY::OMAP.XVAR) 1)) :hints (("Goal" :in-theory (enable ,FTY::OMAP.COUNT)))) (defthm ,FTY::OMAP-COUNT-WHEN-NOT-EMPTYP (implies (and (not (emptyp ,FTY::OMAP.XVAR)) (,FTY::OMAP.PRED ,FTY::OMAP.XVAR)) (equal (,FTY::OMAP.COUNT ,FTY::OMAP.XVAR) (+ 1 ,@(AND FTY::KEYCOUNT `((,FTY::KEYCOUNT (FTY::MV-NTH 0 (OMAP::HEAD ,FTY::OMAP.XVAR))))) ,@(AND FTY::VALCOUNT `((,FTY::VALCOUNT (FTY::MV-NTH 1 (OMAP::HEAD ,FTY::OMAP.XVAR))))) (,FTY::OMAP.COUNT (tail ,FTY::OMAP.XVAR))))) :hints (("Goal" :in-theory (enable ,FTY::OMAP.COUNT)))) ,@(AND FTY::KEYCOUNT FTY::VALCOUNT `((FTY::DEFTHM ,FTY::OMAP-COUNT-OF-HEAD (FTY::IMPLIES (AND (NOT (OMAP::EMPTYP ,FTY::OMAP.XVAR)) (,FTY::OMAP.PRED ,FTY::OMAP.XVAR)) (< (+ (,FTY::KEYCOUNT (FTY::MV-NTH 0 (OMAP::HEAD ,FTY::OMAP.XVAR))) (,FTY::VALCOUNT (FTY::MV-NTH 1 (OMAP::HEAD ,FTY::OMAP.XVAR)))) (,FTY::OMAP.COUNT ,FTY::OMAP.XVAR))) :RULE-CLASSES :LINEAR))) ,@(AND FTY::KEYCOUNT FTY::VALCOUNT `((FTY::DEFTHM ,FTY::OMAP-COUNT-OF-HEAD-FIX (FTY::IMPLIES (CONSP (,FTY::OMAP.FIX ,FTY::OMAP.XVAR)) (< (+ (,FTY::KEYCOUNT (FTY::MV-NTH 0 (OMAP::HEAD (,FTY::OMAP.FIX ,FTY::OMAP.XVAR)))) (,FTY::VALCOUNT (FTY::MV-NTH 1 (OMAP::HEAD (,FTY::OMAP.FIX ,FTY::OMAP.XVAR))))) (,FTY::OMAP.COUNT ,FTY::OMAP.XVAR))) :HINTS (("Goal" :IN-THEORY (FTY::ENABLE ,FTY::OMAP.FIX OMAP::MAPP-NON-NIL-IMPLIES-NOT-EMPTYP))) :RULE-CLASSES :LINEAR))) (defthm ,FTY::OMAP-COUNT-OF-TAIL (implies (and (not (emptyp ,FTY::OMAP.XVAR)) (,FTY::OMAP.PRED ,FTY::OMAP.XVAR)) (< (,FTY::OMAP.COUNT (tail ,FTY::OMAP.XVAR)) (,FTY::OMAP.COUNT ,FTY::OMAP.XVAR))) :rule-classes :linear :hints (("Goal" :in-theory (enable ,FTY::OMAP.COUNT)))) (defthm ,FTY::OMAP-COUNT-OF-TAIL-FIX (implies (consp (,FTY::OMAP.FIX ,FTY::OMAP.XVAR)) (< (,FTY::OMAP.COUNT (tail (,FTY::OMAP.FIX ,FTY::OMAP.XVAR))) (,FTY::OMAP.COUNT ,FTY::OMAP.XVAR))) :rule-classes :linear :hints (("Goal" :in-theory (enable ,FTY::OMAP.COUNT ,FTY::OMAP.FIX mapp-non-nil-implies-not-emptyp)))) (defthm ,FTY::OMAP-COUNT-OF-LOOKUP (implies (and (not (emptyp map)) (,FTY::OMAP.PRED map)) (< (,FTY::VALCOUNT (lookup key map)) (,FTY::OMAP.COUNT map))) :hints (("Goal" :in-theory (enable lookup assoc assoc-when-emptyp ,FTY::VALCOUNT)) ("Goal''" :induct (assoc key map)))) (defthm ,FTY::OMAP-COUNT-OF-UPDATE (implies (and (,FTY::OMAP.PRED ,FTY::OMAP.XVAR) (,FTY::OMAP.KEY-TYPE key) (,FTY::OMAP.VAL-TYPE val) (not (assoc key ,FTY::OMAP.XVAR))) ,(IF (OR FTY::KEYCOUNT FTY::VALCOUNT) `(EQUAL (,FTY::OMAP.COUNT (OMAP::UPDATE FTY::KEY FTY::VAL ,FTY::OMAP.XVAR)) (+ 1 ,@(AND FTY::KEYCOUNT `((,FTY::KEYCOUNT FTY::KEY))) ,@(AND FTY::VALCOUNT `((,FTY::VALCOUNT FTY::VAL))) (,FTY::OMAP.COUNT ,FTY::OMAP.XVAR))) `(> (,FTY::OMAP.COUNT (OMAP::UPDATE FTY::KEY FTY::VAL ,FTY::OMAP.XVAR)) (,FTY::OMAP.COUNT ,FTY::OMAP.XVAR)))) :hints (("Goal" :in-theory (enable head-key emptyp head-key-of-update-of-nil head-value-of-update-when-head-key-equal assoc-when-emptyp assoc-when-assoc-tail mfix-when-mapp tail-of-update-emptyp update-not-emptyp update-when-emptyp (:induction use-weak-update-induction) (:induction weak-update-induction) weak-update-induction-helper-1 weak-update-induction-helper-2 weak-update-induction-helper-3))) :rule-classes :linear))))