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)

lemma

  shows " \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"

apply(tactic {* my_print_tac @{context} *})

apply(rule conjI)

apply(tactic {* my_print_tac @{context} *})

apply(assumption)

apply(tactic {* my_print_tac @{context} *})

apply(assumption)

apply(tactic {* my_print_tac @{context} *})