(defstep bksim-act-start ()
	(then
	   (with-labels (skosimp) (("action" "goal")))
	   (expand "bkwd_sim_step_act")
	   (with-labels (skosimp) (("reach" "postsim" "conctrans" "goal")))
	   (hide "reach")
	   (inst 1 "bk_sim_prestate(alpha!1,c0!1,c!1,a!1,action_corr(alpha!1,c0!1,c!1,a!1))" "action_corr(alpha!1,c0!1,c!1,a!1)")
	   (split)
	)
	"" ""
)

(defstep bksim-step-corr-holds-in-prestate ()
        (then
	   (expand "back_sim_rel_step_corr")
	   (skosimp)
	   (inst "p!1")
	   (branch
	     (case "p!1 = proc(alpha!1)")
	     ((grind))
	   )
	)
	"" ""
)

(defstep bksim-holds-in-prestate (data-strat)
        (then
	   (expand "back_sim_rel")
	   (branch
	      (split)
	      ((data-strat)     ;; Leave data subgoal to user, most will just need grind
	       (bksim-step-corr-holds-in-prestate)
	      )
	   )
	)
	"" ""
)

(defstep bksim-precond-holds ()
        (grind)
	"" ""
)

(defstep bksim-simple-precond-holds ()
        (grind)
	"" ""
)


(defstep bksim-correct-poststate ()
        (then
	   (inst?)
	   (grind)
           (inst?)   ;; only state of right type is a!1, which is what we want
	   (expand "transition")
	   (decompose-equality)
	   (grind)
         )
 	 "" ""
)

  
(defstep bksim-valid-transition ()
        (then
	  (flatten)
	  (branch
	    (split)
	    ((bksim-simple-precond-holds)
	     (bksim-correct-poststate)
	    )
	  )
	)
	"" ""
)


;; I suspect this one is working "by fluke" on steps with null action list


(defstep bksim-valid-transition-list-1 ()  ;; if list has one action
        (then
	   (expand "transition" "goal")
	   (lift-if "goal")
	   (branch
	     (split)
	     ((grind)   ;; list is not null so this one is easy
	      (bksim-valid-transition)
	     )
	   )
	 )
	"" ""
)

(defstep traces-equal ()
        (grind)
	"" ""
)

(defstep bksim-act (data-strat valid-transition-strat)
        (branch
	   (bksim-act-start)
	   ((bksim-holds-in-prestate data-strat)
	    (valid-transition-strat)
	    (traces-equal)
	   )
	)
	"" ""
)



;; Construct the fssa_lemma name from the current value of alpha.
;; Assumes [-1] is of the form action-name?(alpha),
;; returns fssa_action-name
(defun get-fssa_lemma-name ()
	(string-trim "?" (format nil "fssa_~A" (get-op-name -1))) 
)




(defstep replace-alpha ()
    (then
        (let ( (ca_name (format nil "(~A)" (get-op-name -1)) ) )
            (eta ca_name)
        )
        (inst -1 alpha)
        (label alpha= -1)
        (name-replace "ppp" "proc(alpha)" :hide? nil)
        (label ppp-name -1)
        (hide ppp-name)
        (replace alpha= :dir rl)
        (hide alpha)
    )
    "Turns term 'alpha' into an instance of the particular action,
    eg, 'eff(alpha)' becomes 'eff(addResp)', if addResp happens to be
    alpha"
    ""
)


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Victor's strategies



(defstep victor-pfwd ()
  (then
   (expand "fwd_sim")
   (spread (split)
       ((grind)
        (then (expand* "fwd_sim_step" "fwd_sim_step_act")
          (skolem 1 ("alpha"))
          (skolem 1 ("c0" "c" "a0"))
          (with-labels (name "beta" "action_corr(alpha, c0, c, a0)") ("name-beta"))
          (with-labels (flatten) (("reachable" "induct-hyp" "conc-transition" "main")))
          (hide "reachable")
          (expand* "fwd_sim_rel" "fwd_sim_rel_data")
          (with-labels (flatten) (("pre-keys" "pre-seenout" "pre-step")) T)
          (expand transition -)
          (with-labels (flatten) (("conc-pre" "conc-eff")))
          (inst main "fun_transition(a0, int_ioa_inst, beta)" "beta")
          (expand "fun_transition")
          (with-labels (typepred "alpha") ("cc-alpha"))
          (expand* "ext" "conc")
          (branch (split "cc-alpha")
              ((query*))
              )
          )
        ))
   )
  "" ""
  )

(defstep victor-single-alpha ()
  (then (replace "name-beta" :dir rl :hide? T)
	(expand "action_corr")
	(assert)
	(spread (with-labels (case "pre(alpha)(a0)") (("abs-pre") ("prove-abs-pre")))
		((then (replace "abs-pre")
		       (spread (split "main")
			       ((grind)
				(grind)
				(then (expand "fwd_sim_rel_step_corr" -)
				      (with-labels (inst? :copy? T) ("ppp-pc"))
				      (expand "fwd_sim_rel_step_corr" +)
				      (skolem "main" "q")
				      (spread (with-labels (case "q = proc(alpha)") (("q-is-ppp") ("q-is-not-ppp")))
					      ((then (hide "pre-step")
						     (auto-rewrite-theory "fwd_sim_rel")
						     (expand* "eff" "main_eff" "pcout")
						     (assert))
					       (then (inst - "q")
						     (spread (with-labels (case "eff(alpha)(a0)`pc(q) = a0`pc(q) AND c`pc(q) = c0`pc(q)")
									  (("q-pc-nochange") ("prove-q-pc-nochange")))
							     ((then (flatten "q-pc-nochange")
								    (hide "ppp-pc" "induct-hyp")
								    (grind) ;; make this faster
								    )
							      (then (hide "main")
								    (spread (split)
									    ((then (hide -)
										  (grind))
									     (then (hide-all-but "conc-eff" -)
										   (grind)))))
							      (propax)))))))
				(then (expand "transition")
				      (expand "transition")
				      (replace "abs-pre")
				      (inst "main" "eff(alpha)(a0)")))))
		 (then (hide "main" "conc-eff")
		       (expand "fwd_sim_rel_step_corr")
		       (inst?)
		       (grind)))))
  "" ""
  )


(defstep prove-fssa ()
  (then (skolem 1 "alpha")
	(with-labels (flatten) (("alpha" "main")))
	(prove-step$))
  "" "")

(defstep prove-fwd ()
  (then (rewrite-msg-off)
	(label "main" 1)
	(expand "fwd_sim")
        (spread (split)
		( (grind)
		  (then (expand "fwd_sim_step")
			(skolem 1 "alpha") ;; skolem-typepred does not allow naming
			(with-labels (typepred "alpha") (("alpha"))) 
			(expand* "ext" "conc")
			(with-labels (use "fssa_nontrivial") (("fssa_nontrivial")))
			(spread (split "fssa_nontrivial")
				( (propax)
				  (then (flatten "fssa_nontrivial")
					(assert)
					(hide "fssa_nontrivial")
					(branch (split "alpha")
						((prove-step$))))))))))
  "" "")

(defstep prove-step ()
  (then (hide "alpha")
	(expand "fwd_sim_step_act")
	(skolem 1 ("c0" "c" "a0"))
	(with-labels (flatten) (("reachable" "induct-hyp" "conc-transition" "main")))
	(hide "reachable")
	(expand* "fwd_sim_rel" "fwd_sim_rel_data")
	(with-labels (flatten -1) (("pre-keys-data" "pre-seen_out-data" "pre-steps")))
	(hide "pre-keys-data" "pre-seen_out-data" "pre-steps")
	(expand "transition" "conc-transition")
	(with-labels (flatten "conc-transition") (("pre" "eff")))
	(inst main _ "action_corr(alpha, c0, c, a0)")
	(inst main "fun_transition(a0, int_ioa_inst, action_corr(alpha, c0, c, a0))")
	(reveal "alpha")
	(simplify-single-alpha$)
	(prove-pc$))
  "" "")

(defstep simplify-single-alpha ()
  (then (eta-alpha)  ;; change act?(alpha) to act(..) = alpha
        (name-replace "ppp" "proc(alpha)" :hide? nil)
        (label ppp-name -1)
        (hide ppp-name)
        (replace alpha :dir rl)
        (hide alpha)
	(auto-rewrite-theory "ConcreteAut")
        (assert "pre")
        (flatten "pre")
        (get-abstract-pre-pc$)
	(simplify)
        (assert "eff")
        (replace "eff")
        (hide "eff")
        (install-rewrites :theories ("simulation" "fwd_sim_rel" "IntAut")
			  :exclude ("fwd_sim_rel_step_corr"))
        (assert)
	;; transition does not expand because it is recursive
	;; so we expand it explicitly
        (expand transition)
        (assert :quant-simp? t)
        (expand transition)

        ;; Get rid of data information (if we can)
        (reveal pre-keys-data pre-seen_out-data)
        (assert)
        (hide (pre-keys-data pre-seen_out-data))

        (reveal alpha)
    )
    "" ""
)

(defstep eta-alpha ()
    (then (let ( (ca_name (format nil "(~A)" (get-op-name -1)) ) )
            (with-labels (eta ca_name) (("alpha"))))
        (inst "alpha" "alpha")
    )
    "Turns term 'alpha' into an instance of the particular action,
    eg, 'eff(alpha)' becomes 'eff(addResp)', if addResp happens to be
    alpha"
    ""
)

(defstep get-abstract-pre-pc ()
  (then (reveal pre-steps)
        (expand fwd_sim_rel_step_corr pre-steps)
        (with-labels (inst pre-steps ppp) (("a0pc")))
        (replace pre a0pc)
        (auto-rewrite-theory fwd_sim_rel)
        (assert a0pc)
        (expand member a0pc)
        (stop-rewrite-theory fwd_sim_rel)
    )
    "Calculate the pc value in the initial abstract state, and label
    it 'a0pc'"
    ""
)   

(defstep prove-pc ()
  (then (expand "fwd_sim_rel_step_corr")
        (skolem "main" "q")
        (spread 
	 (with-labels (case "q = ppp") (("q-is-ppp") ("q-not-ppp")))
	 ( (then (assert) (replace "q-is-ppp"))
	   (then (reveal "pre-steps")
		 (inst "pre-steps" "q")
                 ;;(assert :cases-rewrite? T)
		 ;; Using assert above take 4.77 secs vs 2.33 secs run time
		 ;; to prove fssa_cont.
                 (record "q-not-ppp")
		 (simplify :cases-rewrite? T)
		 ))))
  "" "")

(defstep start-trans-lemma (extra-vars)
  (then (let ((varlist (append '("alpha" "c0" "c1") extra-vars)))
	  (skolem 1 varlist))
	(with-labels (flatten) (("reachable" "transition" "main")))
	(hide "reachable")
	(with-labels (typepred "alpha") (("alpha")))
	(expand* "ext" "conc"))
  "" "")

(defstep split-alpha-trans-lemma (strat)
  (branch (split "alpha")
	  ((then (expand "transition")
		 (with-labels (flatten "transition") (("pre" "eff")))
		 (expand* "conc_ioa_inst" "pre" "eff" "pcin" "pre_con" "pcout" "main_eff")
		 (assert)
		 (strat))))
  "" "")

(defstep flatten-and-assert ()
  (repeat (then (flatten) (assert)))
  "" "")

(defstep public-stable ()
  (then (skolem "main" "n")
	(expand "public")
	(flatten-and-assert)
	(skolem + "q")
	(inst - "q")
	(flatten-and-assert)
	(spread (with-labels (case "q = proc(alpha)") ("q-is-p" "q-not-p"))
		((flatten-and-assert)
		 (then (record "q-not-p")
		       (flatten-and-assert)))))
  "" "")

(defstep two-processes (q p)
  ;;; this doesn't work--I haven't tried to figure out how to fix it yet
  (spread (with-labels (case (format nil "~A = ~A" q p)) ("q-is-p" "q-not-p"))
	  ((flatten-and-assert)
	   (then (record "q-not-p")
		 (flatten-and-assert))))
  "" "")
	

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Rob's invariant-related strategies  

(defun get-op-name (label)
	(let ( (f (formula (car (select-seq (s-forms *goal*) label)))) )
	(if (negation? f)
		(id (operator (args1 f)))
		(id (operator f))
	)
	)
)

(defstep ret_addr ()
	(then
		(typepred "c0`ret_addr(ppp)")
		(grind)
	)
	"" ""
)


(defstep rp (eq exp)
	(try
		(replace eq exp)
		(skip)
		(replace eq exp rl)
	)
	"Small strategy for replacement - try rl direction if it fails"
	""
)

;; Combining some steps
(defstep siri2 (invname)
	(then
   		(start-invariant-reach-induct)
    	(expand invname)
      	(skolem "goal" "p")
        (instantiate "pre" "p")
        (case "p=proc(alpha)")
	)
"" ""
)


(defstep intro-inv (name)
	(let ((inv-name (intern (format nil "inv_~A" name))))
	(then
		(lemma inv-name)
		(expand invariant) 
		(inst -1 "c0") 
		(reveal reachable)
		(replace reachable -2)
		(hide reachable)
		(expand name -1)
		(inst -1 "ppp")
		(label name -1)
		(assert -1)
	)
	)
	"Introduce invariant as antecedent"
	""
)

; -------------- Mark's strategies below ----------------

(defun get-invariant-name (propname)
	(string-trim "?" (format nil "inv_~A" propname)) 
)

(defstep apply-invariant (propname state &optional instargs)
        (let ((x (get-invariant-name propname)))
	  (then 
            (with-labels (use x)((propname)))
 	    (expand "invariant" propname)
	    (instantiate propname state)
	    (assert)
	    (expand propname propname)
	    (instantiate propname instargs)
	  )
	)
	"" ""
)

(defun get-lemma-name (propname)
	(string-trim "?" (format nil "lemma_~A" propname)) 
)

(defstep apply-lemma (propname args &optional instargs)
        (let ((x (get-lemma-name propname)))
	  (then 
            (with-labels (lemma x)((propname)))
	    (instantiate propname args)
	    (assert)
	    (instantiate propname instargs)
	    (assert)
	  )
	)
	"" ""
)

(defstep start-invariant-induct (indvar indmeas invname)
  (then
    (stop-rewrite)          ;; remove this later when unnecessary auto_rewrites are all gone?
    (expand "invariant")
    (with-labels (skosimp) (("reach" "goal")))
    (with-labels (measure-induct+ indvar indmeas) (("indhyp" "goal")))
    (expand invname "goal"))
    "" ""
)

(defstep start-invariant-reach-induct ()
   (then
      (stop-rewrite)        ;; remove this later when unnecessary auto_rewrites are all gone?
      (expand "invariant")
      (rule-induct reachable? + reachable?_induction)
      (skolem 1 ("c1")) 
      (with-labels (flatten) (("indrule" "goal")))
      (branch 
         (with-labels (split) (("init") ("indstep")))
	 (
	   (grind)   ;; almost always deals to initial state
	   (then
	     (skolem "indstep" ("c0" "alpha"))
             (with-labels (flatten "indstep") (("reach" "pre" "trans")))
	   )
	 )
       )
    )
   "" ""
 )




; Introduces definition of alpha in form needed for open-trans

(defun get-case-string-for-alphadef (alpha actdef)
	(string-trim "?" (format nil "~A = ~A" alpha actdef)) 
)

(defstep intro-alpha-def (alpha actdef)
  (let ((x (get-case-string-for-alphadef alpha actdef)))
    (branch
      (with-labels (case x) (("alphadef")))
      (
       (skip)
       (decompose-equality "alphadef"))))
  "" ""
)

(defstep open-trans-a-bit ()
  (then
    (with-labels (copy "trans") (("trans-cp")))
    (expand "transition" "trans-cp")
    (with-labels (flatten "trans-cp") (("precon" "effect")))
    (expand "conc_ioa_inst" ("precon" "effect"))
    (expand "pre" "precon")
    (with-labels (flatten "precon") (("precon-pc" "precon-rest"))))
  "" ""
)

; The following takes an action name and a value known to be equivalent, in a form that will
; allow beta to figure out that things like cont1(alpha) is false if actdef says alpha = cont2(p).
; For example, if we invoke (open-trans "alpha" "cont1(proc(alpha)"), it extracts the specific details
; for that action from a sequent like
; [-6,(trans)]
;      transition(c0, conc_ioa_inst, alpha, c1)

(defstep open-trans (alpha actdef)
  (then
    (intro-alpha-def alpha actdef)
    (assert)
    (open-trans-a-bit)

    (expand "pcin" "precon-pc")
    (lift-if "precon-pc")
    (replace "alphadef" ("precon-pc"))
    (beta "precon-pc")
    (with-labels (bddsimp "precon-pc") (("precon-pc")))
    
    (expand "pre_con" "precon-rest")
    (lift-if "precon-rest")
    (replace "alphadef" ("precon-rest"))
    (beta "precon-rest")
    (with-labels (bddsimp "precon-rest") (("precon-rest")))
    
    (expand "eff" "effect")
    (expand "pcout" "effect")
    (lift-if "effect")
    (replace "alphadef" ("effect"))
    (beta "effect")
    (with-labels (bddsimp "effect") (("effect")))
    
    (expand "main_eff" "effect")
    (lift-if "effect")
    (replace "alphadef" ("effect"))
    (beta "effect")
    (with-labels (bddsimp "effect") (("effect")))
  )
  "" ""
)


; A simpler version of the above, which does not require the action name to be given.
; It just assumes that a formula such as cont?(alpha) is available to show what the
; action is.

(defstep open-trans-simple ()
  (then
   (open-trans-a-bit)
   (hide "trans" "reach")
   (expand "pcin")
   (assert)
   (expand "pre_con")
   (assert)
   (expand "eff" "effect")
   (assert)
   (expand "pcout")
   (assert)
   (expand "main_eff")
   (assert))
  "" ""
)




(defstep get-pc-change ()
  (then
    (open-trans-a-bit)
    (hide "precon-rest")
  )
  "" ""
)


  
(defstep easy-dnm ()
  (then
    (stop-rewrite)
    (install-rewrites ("ext" "conc"))
    (skosimp)
    (typepred "alpha!1")
    (assert)
    (branch (split) ((grind)))
  )
  "" ""
)


(defun get-typepred-string-for-easy-grind (state)
	(string-trim "?" (format nil "~A`ret_addr(proc(alpha))" state)) 
)

(defstep easy-grind-over-actions (state)
  (let ((x (get-typepred-string-for-easy-grind state)))
  (then
     (typepred x)
     (typepred "alpha")
     (expand "ext")
     (expand "conc")
     (apply (branch (split -1) ((grind))))))
  "" ""
)

;; Another version that assumes the prestate is c0 and calls open-trans-simple
;; to get transition details.

(defstep easy-grind-over-actions-2 ()
  (then
     (typepred "c0`ret_addr(proc(alpha))")
     (typepred "alpha")
     (expand "ext")
     (expand "conc")
     (apply (branch (split -1) ((then (open-trans-simple)(grind))))))
  "" ""
)
    
;-------------- Mark's strategies above ----------------