theory Subgoal

imports Term_pat

begin

section {* Monad for goal and subgoal manipulation, useful for debugging tactics  *}

subsection {* Implementation *}

ML {*

  fun goalM raw_goal = m0M' (fn ((i, _), ctxt) =>

  let

     val thy = Proof_Context.theory_of ctxt

     val goal = raw_goal |> cterm_of thy |> Goal.init

     (* val ctxt' = Variable.auto_fixes raw_goal ctxt *)

     val ctxt' = ctxt

  in (s2M ctxt' |-- (s1M (i, goal)) |-- returnM goal) end)

local

  fun pr_goal ctxt goal = Goal_Display.pretty_goals ctxt goal |> 

                           Pretty.markup_chunks Markup.state |> Pretty.writeln

in

  fun tacM tac = m1M' (fn (i, goal) => m2M (fn ctxt =>

        let 

            val goal' = (Seq.hd (tac ctxt goal)) 

            val _ = pr_goal ctxt goal'

        in

            s1M (i, goal') |-- returnM goal'

        end))

end

  fun focusM i = pushM |-- (liftM (m0M (fn ((_, goal), ctxt) => 

                     let val (focus as {context = ctxt', ...}, goal') = Subgoal.focus ctxt i goal

                     in 

                        setM ((i, goal'), ctxt') |-- returnM focus

                     end)))

  fun end_focusM x = (     popM 

                      :|-- (fn ((i, goal'), _) => topM (fn ((old_i, goal), ctxt) =>

                           let val ({context = ctxt', params, asms, ...}, _) = 

                                               Subgoal.focus ctxt i goal

                               val new_goal = Seq.lifts (Subgoal.retrofit ctxt' ctxt params asms i) 

                                                      (Seq.single goal') goal |> Seq.hd

                               in s1M (old_i, new_goal) |-- returnM new_goal end  ))) x

*}

subsection {* Examples *}

lemma init: "A \<Longrightarrow> A"

  by simp

ML {*

  val r as (result, _)= [((0, @{thm "init"}), @{context})] |> 

          @{fterm "(A \<and> B \<Longrightarrow> A)"} 

          :|-- goalM 

           |-- focusM 1 

          :|--(fn {prems, ...} => let

                       val conj = hd prems

                       val r = rtac (conj RS @{thm HOL.conjunct1}) 1

                   in tacM (K r) end )

           |-- end_focusM >> Drule.export_without_context |> normVal

*}

ML {*

  val r = [((0, @{thm "init"}), @{context})] |> 

          @{fterm "(A \<and> B \<Longrightarrow> A)"} 

          :|-- goalM 

          |-- tacM (fn ctxt => Subgoal.FOCUS (fn {prems, ...} => let

                                  val conj = hd prems

                                  val r = rtac (conj RS @{thm HOL.conjunct1}) 1

                                in r end ) ctxt 1) >> Drule.export_without_context

          |> normVal

*}

end