1 (* Authors: Gerwin Klein and Rafal Kolanski, 2012

     2    Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>

     3                 Rafal Kolanski <rafal.kolanski at nicta.com.au>

     4 *)

     5 

     6 header "Separation Logic Tactics"

     7 

     8 theory Sep_Tactics

     9 imports Separation_Algebra

    10 begin

    11 

    12 ML_file "sep_tactics.ML"

    13 

    14 text {* A number of proof methods to assist with reasoning about separation logic. *}

    15 

    16 

    17 section {* Selection (move-to-front) tactics *}

    18 

    19 method_setup sep_select = {*

    20   Scan.lift Parse.int >> (fn n => fn ctxt => SIMPLE_METHOD' (sep_select_tac ctxt n))

    21 *} "Select nth separation conjunct in conclusion"

    22 

    23 method_setup sep_select_asm = {*

    24   Scan.lift Parse.int >> (fn n => fn ctxt => SIMPLE_METHOD' (sep_select_asm_tac ctxt n))

    25 *} "Select nth separation conjunct in assumptions"

    26 

    27 

    28 section {* Substitution *}

    29 

    30 method_setup "sep_subst" = {*

    31   Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --

    32     Attrib.thms >> (fn ((asm, occs), thms) => fn ctxt =>

    33       SIMPLE_METHOD' ((if asm then sep_subst_asm_tac else sep_subst_tac) ctxt occs thms))

    34 *}

    35 "single-step substitution after solving one separation logic assumption"

    36 

    37 

    38 section {* Forward Reasoning *}

    39 

    40 method_setup "sep_drule" = {*

    41   Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (sep_dtac ctxt thms))

    42 *} "drule after separating conjunction reordering"

    43 

    44 method_setup "sep_frule" = {*

    45   Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (sep_ftac ctxt thms))

    46 *} "frule after separating conjunction reordering"

    47 

    48 

    49 section {* Backward Reasoning *}

    50 

    51 method_setup "sep_rule" = {*

    52   Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (sep_rtac ctxt thms))

    53 *} "applies rule after separating conjunction reordering"

    54 

    55 

    56 section {* Cancellation of Common Conjuncts via Elimination Rules *}

    57 

    58 ML {*

    59   structure SepCancel_Rules = Named_Thms (

    60     val name = @{binding "sep_cancel"};

    61     val description = "sep_cancel rules";

    62   );

    63 *}

    64 setup SepCancel_Rules.setup

    65 

    66 text {*

    67   The basic @{text sep_cancel_tac} is minimal. It only eliminates

    68   erule-derivable conjuncts between an assumption and the conclusion.

    69 

    70   To have a more useful tactic, we augment it with more logic, to proceed as

    71   follows:

    72   \begin{itemize}

    73   \item try discharge the goal first using @{text tac}

    74   \item if that fails, invoke @{text sep_cancel_tac}

    75   \item if @{text sep_cancel_tac} succeeds

    76     \begin{itemize}

    77     \item try to finish off with tac (but ok if that fails)

    78     \item try to finish off with @{term sep_true} (but ok if that fails)

    79     \end{itemize}

    80   \end{itemize}

    81   *}

    82 

    83 ML {*

    84   fun sep_cancel_smart_tac ctxt tac =

    85     let fun TRY' tac = tac ORELSE' (K all_tac)

    86     in

    87       tac

    88       ORELSE' (sep_cancel_tac ctxt tac

    89                THEN' TRY' tac

    90                THEN' TRY' (rtac @{thm TrueI}))

    91       ORELSE' (etac @{thm sep_conj_sep_emptyE}

    92                THEN' sep_cancel_tac ctxt tac

    93                THEN' TRY' tac

    94                THEN' TRY' (rtac @{thm TrueI}))

    95     end;

    96 

    97   fun sep_cancel_smart_tac_rules ctxt etacs =

    98       sep_cancel_smart_tac ctxt (FIRST' ([atac] @ etacs));

    99 

   100   val sep_cancel_syntax = Method.sections [

   101     Args.add -- Args.colon >> K (I, SepCancel_Rules.add)] >> K ();

   102 *}

   103 

   104 method_setup sep_cancel = {*

   105   sep_cancel_syntax >> (fn _ => fn ctxt =>

   106     let

   107       val etacs = map etac (SepCancel_Rules.get ctxt);

   108     in

   109       SIMPLE_METHOD' (sep_cancel_smart_tac_rules ctxt etacs)

   110     end)

   111 *} "Separating conjunction conjunct cancellation"

   112 

   113 text {*

   114   As above, but use blast with a depth limit to figure out where cancellation

   115   can be done. *}

   116 

   117 method_setup sep_cancel_blast = {*

   118   sep_cancel_syntax >> (fn _ => fn ctxt =>

   119     let

   120       val rules = SepCancel_Rules.get ctxt;

   121       val tac = Blast.depth_tac (ctxt addIs rules) 10;

   122     in

   123       SIMPLE_METHOD' (sep_cancel_smart_tac ctxt tac)

   124     end)

   125 *} "Separating conjunction conjunct cancellation using blast"

   126 

   127 end