Theory Refine_Imperative_HOL.Concl_Pres_Clarification

theory Concl_Pres_Clarification
imports Main
begin
  text ‹Clarification and clarsimp that preserve the structure of 
    the subgoal's conclusion, i.e., neither solve it, nor swap it 
    with premises, as, eg, @{thm [source] notE} does.
    ›

  ML ‹
    local 
      fun is_cp_brl (is_elim,thm) = let
        val prems = Thm.prems_of thm
        val nprems = length prems
        val concl = Thm.concl_of thm
      in
        (if is_elim then nprems=2 else nprems=1) andalso let
          val lprem_concl = hd (rev prems)
            |> Logic.strip_assums_concl
        in
          concl aconv lprem_concl
        end
      end

      val not_elim = @{thm notE}
      val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]

      fun eq_contr_tac ctxt i = ematch_tac ctxt [not_elim] i THEN eq_assume_tac i;
      fun eq_assume_contr_tac ctxt = eq_assume_tac ORELSE' eq_contr_tac ctxt;

      fun cp_bimatch_from_nets_tac ctxt =
        Bires.biresolution_from_nets_tac ctxt Bires.tag_ord (SOME is_cp_brl) true;


    in
      fun cp_clarify_step_tac ctxt =
        appSWrappers ctxt
         (FIRST'
           [eq_assume_contr_tac ctxt,
            FIRST' (map (fn tac => tac ctxt) hyp_subst_tacs),
            cp_bimatch_from_nets_tac ctxt (Classical.safep_netpair_of ctxt)
            ]);
      
        fun cp_clarify_tac ctxt = SELECT_GOAL (REPEAT_DETERM (cp_clarify_step_tac ctxt 1));

        fun cp_clarsimp_tac ctxt =
          Simplifier.safe_asm_full_simp_tac ctxt THEN_ALL_NEW
          cp_clarify_tac (addSss ctxt);


    end


  ›

  method_setup cp_clarify = ‹
    (Classical.cla_method' (CHANGED_PROP oo cp_clarify_tac))
    ›

  method_setup cp_clarsimp = ‹let
    fun clasimp_method' tac =
      Method.sections clasimp_modifiers >> K (SIMPLE_METHOD' o tac);
  in
    clasimp_method' (CHANGED_PROP oo cp_clarsimp_tac)
  end›



end