(defstep do-with-tcc (str1 str2)
  (try (quote str1)
	   (try (then (quote str2) (fail)) (fail) (assert)) 
	   (postpone)) 
  "Tries (str2) on all subgoals generated by (str1)" "")

(defstep exp2 ()
 (repeat (then 
	  (rewrite "exp2_def")
	  (rewrite "expt_inverse")
	  (rewrite "expt_plus")
	  (rewrite "expt_div" :dir RL)
	  (rewrite "expt_x1")
	  (rewrite "expt_x0")
	  (assert)))
 "exp2-catch-all-strategy, includes exp2_def expt_inverse expt_plus
 expt_div :dir RL expt_x1 expt_x0 and assert"
 "Rewriting with expt lemmas")

(defstep exp2-const ()
 (then 
  (repeat (rewrite "exp2_def"))
  (rewrite "exp2_2")
  (rewrite "exp2_3")
  (rewrite "exp2_4")
  (rewrite "exp2_5")
  (rewrite "exp2_6")
  (rewrite "exp2_7")
  (rewrite "exp2_8")
  (rewrite "exp2_9")
  (rewrite "exp2_10")
  (rewrite "exp2_13")
  (rewrite "exp2_23")
  (rewrite "exp2_28")
  (rewrite "exp2_29")
  (rewrite "exp2_52")
  (rewrite "exp2_53")
  (rewrite "exp2_54")
  (rewrite "exp2_55")
  (rewrite "exp2_56")
  (rewrite "exp2_57")
  (rewrite "exp2_63")
  (rewrite "exp2_64")
  (rewrite "exp2_71")
  (rewrite "exp2_127")
  (rewrite "exp2_128")
  (assert))
 "Resolves 2^i for various values of i" "Using exp2 lemmas")

(defstep exp2-const-inverse ()
 (then
  (repeat (rewrite "exp2_def"))
  (repeat (rewrite "expt_inverse"))
  (exp2-const)
 )
 "(exp2-const) plus (rewrite \"expt_inverse\")"
 "Using exp2 lemmas"
)

(defstep case-replace-hide (step)
 (spread
  (case-replace step)
  ((hide -1))
 )
 "do (case-replace <step> :hide? t)"
 "case-replacing ~a"
)

(defstep case-replace-hide-all (step)
 (else
  (spread!
   (case-replace step)
   ((hide -1) (hide-all-but 1))
  )
  (spread!
   (case-replace step)
   ((hide-all-but 1))
  )
 )
 "do (case-replace <step> :hide? t) and (hide-all-but 1) on the second subgoal"
 "case-replacing ~a"
)

(defstep case-replace-assert (step)
 (spread!
  (case-replace step)
  ((hide -1) (assert))
 )
 "do (case-replace <step> :hide? t) and (assert) the second subgoal"
 "case-replacing ~a"
)

(defstep case-replace-grind (step)
 (spread!
  (case-replace step)
  ((hide -1)
   (then
    (hide-all-but 1)
    (grind)
   )
  )
 )
 "do (case-replace <step> :hide? t) and (grind) the case"
 "case-replacing ~a"
)

(defstep first (command first)
 (spread!
  (quote command)
  ((quote first) (skip))
 )
 ""
 "Using ~a and resolving this with ~a"
)

(defstep second (command second)
 (spread!
  (quote command)
  ((skip) (quote second))
 )
 ""
 "Using ~a and resolving the other case with ~a"
)

(defstep bv-const ()
 (then
  (repeat (rewrite "b2n_fill_caret"))
  (rewrite "b2n_F")
  (rewrite "b2n_T")
  (rewrite "b2sign_F")
  (rewrite "b2sign_T")
  (repeat (rewrite "bv2int_fill_F"))
  (repeat (rewrite "bv2int_fill_T"))
  (assert)
 )
 ""
 "Replacing various instances of bv2int(fill()), b2n() and b2sign()"
)


(defstep fa ()
 (repeat (then (assert) (flatten)))
 ""
 "Repeating assert/flatten"
)

(defstep md-pushstep ()
 (then (REWRITE-MSG-OFF)
	   (AUTO-REWRITE-THEORY "md_def")
       (AUTO-REWRITE-THEORY "md_ctl")
       (AUTO-REWRITE-THEORY "md_tomcirc")
       (AUTO-REWRITE-THEORY "md_types")
	   (AUTO-REWRITE "stall_in")
	   (SMASH) )
 "" 
 "Push instruction one stage")


(defstep mddivstep ()
 (then
       (USE "TOMmd_md2_live")
       (SMASH)
       (SKOSIMP*)
       (REPLACE*)
	   (ASSERT)
       (HIDE-ALL-BUT (-3 -4 -5 -6))
       (USE "TOMmd_md2to1_live")
       (APPLY (BRANCH (SMASH) ((SKIP) (then (replace*) (hide-all-but 1) (GRIND)))))
       (REPLACE*)
	   (ASSERT)
       (HIDE-ALL-BUT (-2 -3 -4 -5))
	  )
 "Expand definitions for MD"
 "Expanding definitins of MD")

(defstep add-pushstep ()
 (then (REWRITE-MSG-OFF)
	   (AUTO-REWRITE-THEORY "add_def")
       (AUTO-REWRITE-THEORY "add_ctl")
       (AUTO-REWRITE-THEORY "add_tomcirc")
       (AUTO-REWRITE-THEORY "add_types")
	   (AUTO-REWRITE "stall_in")
	   (SMASH) )
 "" 
 "Push instruction one stage")