;; shifter
(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)" "")

;; used in proof of lzero_concat1
(defstep lz_tcc ()
  (then (use "logN_is_logN")
                (smash))
  "Strategie for TCCs" "")

;; lzero_exp2_impl_correct
(defstep exp2-strat-neu ()
    (repeat (then (rewrite "expt_inverse")
                                  (rewrite "expt_plus")
                                  (rewrite "expt_div" :dir RL)
                                  (rewrite "expt_x1")
                                  (rewrite "expt_x0")
                                  (assert)))
        "Prove simple ...."
"Rewriting with expt lemmas")

(defstep lz_tcc2 ()
  ( then (skosimp*)
         (smash)) "" "")

(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_0")
  (rewrite "exp2_1")
  (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 rh (fnum &optional (fnums *) (dir LR) (actuals? nil))
 (replace fnum :fnums fnums :dir dir :hide? t :actuals? actuals?)
 "Identical to (replace), with :hide? t set by default."
 "~%Replacing and hiding using formula ~a"
)

(defstep cr (formula &optional (hide? t) (all nil) (actuals? nil))
 (spread
  (case formula)
  ((replace -1 :hide? hide? :actuals? actuals?)
   (if all (hide-all-but 1) (skip))
  )
 )
 "Identical to (case-replace), with further arguments :hide? and :all. The latter will invoke (hide-all-but 1) on the second subgoal."
 "~%Assuming and applying ~a"
)