--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/Subgoal.thy	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,76 @@
+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
+