defmapping-proof-templates

(in-package "ACL2")

(must-succeed* (definputs-guarded-1-1)
  (defthm-alpha-injective :hints (("Goal" :in-theory nil
       :cases ((equal (beta (alpha a)) (beta (alpha aa))))
       :use (beta-of-alpha (:instance beta-of-alpha (a aa))))))
  (defthm-beta-injective :hints (("Goal" :in-theory nil
       :cases ((equal (alpha (beta b)) (alpha (beta bb))))
       :use (alpha-of-beta (:instance alpha-of-beta (b bb))))))
  (defthm-alpha-injective :name alpha-injective-uncond
    :unconditional t
    :hints (("Goal" :in-theory nil
       :cases ((equal (beta (alpha a)) (beta (alpha aa))))
       :use (beta-of-alpha-uncond (:instance beta-of-alpha-uncond (a aa))))))
  (defthm-beta-injective :name beta-injective-uncond
    :unconditional t
    :hints (("Goal" :in-theory nil
       :cases ((equal (alpha (beta b)) (alpha (beta bb))))
       :use (alpha-of-beta-uncond (:instance alpha-of-beta-uncond (b bb))))))
  :with-output-off nil)

(must-succeed* (definputs-guarded-2-1)
  (defthm-alpha-injective :a1...an (a1 a2)
    :aa1...aan (aa1 aa2)
    :hints (("Goal" :in-theory nil
       :cases ((equal (beta (alpha a1 a2)) (beta (alpha aa1 aa2))))
       :use (beta-of-alpha (:instance beta-of-alpha (a1 aa1) (a2 aa2))))))
  (defthm-beta-injective :hints (("Goal" :in-theory nil
       :cases ((equal (alpha (mv-nth 0 (beta b)) (mv-nth 1 (beta b)))
          (alpha (mv-nth 0 (beta bb)) (mv-nth 1 (beta bb)))))
       :use (alpha-of-beta (:instance alpha-of-beta (b bb))))))
  :with-output-off nil)

(must-succeed* (definputs-guarded-1-2)
  (defthm-alpha-injective :hints (("Goal" :in-theory nil
       :cases ((equal (beta (mv-nth 0 (alpha a)) (mv-nth 1 (alpha a)))
          (beta (mv-nth 0 (alpha aa)) (mv-nth 1 (alpha aa)))))
       :use (beta-of-alpha (:instance beta-of-alpha (a aa))))))
  (defthm-beta-injective :b1...bm (b1 b2)
    :bb1...bbm (bb1 bb2)
    :hints (("Goal" :in-theory nil
       :cases ((equal (alpha (beta b1 b2)) (alpha (beta bb1 bb2))))
       :use (alpha-of-beta (:instance alpha-of-beta (b1 bb1) (b2 bb2))))))
  :with-output-off nil)

(must-succeed* (definputs-guarded-2-2)
  (defthm-alpha-injective :a1...an (a1 a2)
    :aa1...aan (aa1 aa2)
    :hints (("Goal" :in-theory nil
       :cases ((equal (beta (mv-nth 0 (alpha a1 a2)) (mv-nth 1 (alpha a1 a2)))
          (beta (mv-nth 0 (alpha aa1 aa2)) (mv-nth 1 (alpha aa1 aa2)))))
       :use (beta-of-alpha (:instance beta-of-alpha (a1 aa1) (a2 aa2))))))
  (defthm-beta-injective :b1...bm (b1 b2)
    :bb1...bbm (bb1 bb2)
    :hints (("Goal" :in-theory nil
       :cases ((equal (alpha (mv-nth 0 (beta b1 b2)) (mv-nth 1 (beta b1 b2)))
          (alpha (mv-nth 0 (beta bb1 bb2)) (mv-nth 1 (beta bb1 bb2)))))
       :use (alpha-of-beta (:instance alpha-of-beta (b1 bb1) (b2 bb2))))))
  (defthm-alpha-injective :name alpha-injective-uncond
    :a1...an (a1 a2)
    :aa1...aan (aa1 aa2)
    :unconditional t
    :hints (("Goal" :in-theory nil
       :cases ((equal (beta (mv-nth 0 (alpha a1 a2)) (mv-nth 1 (alpha a1 a2)))
          (beta (mv-nth 0 (alpha aa1 aa2)) (mv-nth 1 (alpha aa1 aa2)))))
       :use (beta-of-alpha-uncond (:instance beta-of-alpha-uncond (a1 aa1) (a2 aa2))))))
  (defthm-beta-injective :name beta-injective-uncond
    :b1...bm (b1 b2)
    :bb1...bbm (bb1 bb2)
    :unconditional t
    :hints (("Goal" :in-theory nil
       :cases ((equal (alpha (mv-nth 0 (beta b1 b2)) (mv-nth 1 (beta b1 b2)))
          (alpha (mv-nth 0 (beta bb1 bb2)) (mv-nth 1 (beta bb1 bb2)))))
       :use (alpha-of-beta-uncond (:instance alpha-of-beta-uncond (b1 bb1) (b2 bb2))))))
  :with-output-off nil)