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 ML {*

    20   fun sep_select_method n ctxt =

    21         Method.SIMPLE_METHOD' (sep_select_tac ctxt n);

    22   fun sep_select_asm_method n ctxt =

    23         Method.SIMPLE_METHOD' (sep_select_asm_tac ctxt n);

    24 *}

    25 

    26 method_setup sep_select = {*

    27   Scan.lift Parse.int >> sep_select_method

    28 *} "Select nth separation conjunct in conclusion"

    29 

    30 method_setup sep_select_asm = {*

    31   Scan.lift Parse.int >> sep_select_asm_method

    32 *} "Select nth separation conjunct in assumptions"

    33 

    34 

    35 section {* Substitution *}

    36 

    37 ML {*

    38   fun sep_subst_method ctxt occs thms =

    39         SIMPLE_METHOD' (sep_subst_tac ctxt occs thms);

    40   fun sep_subst_asm_method ctxt occs thms =

    41         SIMPLE_METHOD' (sep_subst_asm_tac ctxt occs thms);

    42 

    43   val sep_subst_parser =

    44         Args.mode "asm"

    45         -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0])

    46         -- Attrib.thms;

    47 *}

    48 

    49 method_setup "sep_subst" = {*

    50   sep_subst_parser >>

    51     (fn ((asm, occs), thms) => fn ctxt =>

    52       (if asm then sep_subst_asm_method else sep_subst_method) ctxt occs thms)

    53 *}

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

    55 

    56 

    57 section {* Forward Reasoning *}

    58 

    59 ML {*

    60   fun sep_drule_method thms ctxt = SIMPLE_METHOD' (sep_dtac ctxt thms);

    61   fun sep_frule_method thms ctxt = SIMPLE_METHOD' (sep_ftac ctxt thms);

    62 *}

    63 

    64 method_setup "sep_drule" = {*

    65   Attrib.thms >> sep_drule_method

    66 *} "drule after separating conjunction reordering"

    67 

    68 method_setup "sep_frule" = {*

    69   Attrib.thms >> sep_frule_method

    70 *} "frule after separating conjunction reordering"

    71 

    72 

    73 section {* Backward Reasoning *}

    74 

    75 ML {*

    76   fun sep_rule_method thms ctxt = SIMPLE_METHOD' (sep_rtac ctxt thms)

    77 *}

    78 

    79 method_setup "sep_rule" = {*

    80   Attrib.thms >> sep_rule_method

    81 *} "applies rule after separating conjunction reordering"

    82 

    83 

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

    85 

    86 ML {*

    87   structure SepCancel_Rules = Named_Thms (

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

    89     val description = "sep_cancel rules";

    90   );

    91 *}

    92 setup SepCancel_Rules.setup

    93 

    94 text {*

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

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

    97 

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

    99   follows:

   100   \begin{itemize}

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

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

   103   \item if @{text sep_cancel_tac} succeeds

   104     \begin{itemize}

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

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

   107     \end{itemize}

   108   \end{itemize}

   109   *}

   110 

   111 ML {*

   112   fun sep_cancel_smart_tac ctxt tac =

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

   114     in

   115       tac

   116       ORELSE' (sep_cancel_tac ctxt tac

   117                THEN' TRY' tac

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

   119       ORELSE' (etac @{thm sep_conj_sep_emptyE}

   120                THEN' sep_cancel_tac ctxt tac

   121                THEN' TRY' tac

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

   123     end;

   124 

   125   fun sep_cancel_smart_tac_rules ctxt etacs =

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

   127 

   128   fun sep_cancel_method ctxt =

   129     let

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

   131     in

   132       SIMPLE_METHOD' (sep_cancel_smart_tac_rules ctxt etacs)

   133     end;

   134 

   135   val sep_cancel_syntax = Method.sections [

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

   137 *}

   138 

   139 method_setup sep_cancel = {*

   140   sep_cancel_syntax >> K sep_cancel_method

   141 *} "Separating conjunction conjunct cancellation"

   142 

   143 text {*

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

   145   can be done. *}

   146 

   147 ML {*

   148   fun sep_cancel_blast_method ctxt =

   149     let

   150       val rules = SepCancel_Rules.get ctxt;

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

   152     in

   153       SIMPLE_METHOD' (sep_cancel_smart_tac ctxt tac)

   154     end;

   155 *}

   156 

   157 method_setup sep_cancel_blast = {*

   158   sep_cancel_syntax >> K sep_cancel_blast_method

   159 *} "Separating conjunction conjunct cancellation using blast"

   160 

   161 end