theory Tactical
imports Advanced
begin

ML {*
fun my_print_tac ctxt thm =
let
   val _ = tracing (Pretty.string_of (pretty_thm_no_vars ctxt thm))
in
   Seq.single thm
end
*}

ML {*
let
   val ctxt = @{context}
   val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}
in
   Goal.prove ctxt ["x", "y", "u", "v", "P", "Q"] [@{prop "x = y"}, @{prop "u = v"}] goal
    (fn {prems = pms, context = ctxt} =>  
              (my_print_tac ctxt)
              THEN etac @{thm disjE} 1 THEN
               (my_print_tac ctxt) 
              THEN rtac @{thm disjI2} 1
              THEN  (my_print_tac ctxt) 
              THEN atac 1
              THEN rtac @{thm disjI1} 1
              THEN atac 1)
end
*}

ML {*
  Goal.prove
*}

ML {*
fun pretty_cterms ctxt ctrms =
  Pretty.block (Pretty.commas (map (pretty_cterm ctxt) ctrms))
*}

ML {*
fun foc_tac {prems, params, asms, concl, context, schematics} =
let
  fun assgn1 f1 f2 xs =
    let
       val out = map (fn (x, y) => Pretty.enum ":=" "" "" [f1 x, f2 y]) xs
    in
       Pretty.list "" "" out
    end
  fun assgn2 f xs = assgn1 f f xs
  val pps = map (fn (s, pp) => Pretty.block [Pretty.str s, pp])
    [("params: ", assgn1 Pretty.str (pretty_cterm context) params),
     ("assumptions: ", pretty_cterms context asms),
     ("conclusion: ", pretty_cterm context concl),
     ("premises: ", pretty_thms_no_vars context prems),
     ("schematics: ", assgn2 (pretty_cterm context) (snd schematics))]
in
  tracing (Pretty.string_of (Pretty.chunks pps)); all_tac
end
*}

notation (output) "prop"   ("#_" [1000] 1000)

end