1 theory Subgoal

     2 imports Term_pat

     3 begin

     4 

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

     6 

     7 subsection {* Implementation *}

     8 

     9 ML {*

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

    11   let

    12      val thy = Proof_Context.theory_of ctxt

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

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

    15      val ctxt' = ctxt

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

    17 

    18 local

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

    20                            Pretty.markup_chunks Markup.state |> Pretty.writeln

    21 in

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

    23         let 

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

    25             val _ = pr_goal ctxt goal'

    26         in

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

    28         end))

    29 end

    30 

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

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

    33                      in 

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

    35                      end)))

    36 

    37   fun end_focusM x = (     popM 

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

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

    40                                                Subgoal.focus ctxt i goal

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

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

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

    44 *}

    45 

    46 subsection {* Examples *}

    47 

    48 lemma init: "A \<Longrightarrow> A"

    49   by simp

    50 

    51 ML {*

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

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

    54           :|-- goalM 

    55            |-- focusM 1 

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

    57                        val conj = hd prems

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

    59                    in tacM (K r) end )

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

    61 *}

    62 

    63 

    64 ML {*

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

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

    67           :|-- goalM 

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

    69                                   val conj = hd prems

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

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

    72           |> normVal

    73 *}

    74 

    75 end

    76