--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Separation_Algebra/Sep_Tactics.thy~	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,161 @@
+(* Authors: Gerwin Klein and Rafal Kolanski, 2012
+   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
+                Rafal Kolanski <rafal.kolanski at nicta.com.au>
+*)
+
+header "Separation Logic Tactics"
+
+theory Sep_Tactics
+imports Separation_Algebra
+begin
+
+ML_file "sep_tactics.ML"
+
+text {* A number of proof methods to assist with reasoning about separation logic. *}
+
+
+section {* Selection (move-to-front) tactics *}
+
+ML {*
+  fun sep_select_method n ctxt =
+        Method.SIMPLE_METHOD' (sep_select_tac ctxt n);
+  fun sep_select_asm_method n ctxt =
+        Method.SIMPLE_METHOD' (sep_select_asm_tac ctxt n);
+*}
+
+method_setup sep_select = {*
+  Scan.lift Parse.int >> sep_select_method
+*} "Select nth separation conjunct in conclusion"
+
+method_setup sep_select_asm = {*
+  Scan.lift Parse.int >> sep_select_asm_method
+*} "Select nth separation conjunct in assumptions"
+
+
+section {* Substitution *}
+
+ML {*
+  fun sep_subst_method ctxt occs thms =
+        SIMPLE_METHOD' (sep_subst_tac ctxt occs thms);
+  fun sep_subst_asm_method ctxt occs thms =
+        SIMPLE_METHOD' (sep_subst_asm_tac ctxt occs thms);
+
+  val sep_subst_parser =
+        Args.mode "asm"
+        -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0])
+        -- Attrib.thms;
+*}
+
+method_setup "sep_subst" = {*
+  sep_subst_parser >>
+    (fn ((asm, occs), thms) => fn ctxt =>
+      (if asm then sep_subst_asm_method else sep_subst_method) ctxt occs thms)
+*}
+"single-step substitution after solving one separation logic assumption"
+
+
+section {* Forward Reasoning *}
+
+ML {*
+  fun sep_drule_method thms ctxt = SIMPLE_METHOD' (sep_dtac ctxt thms);
+  fun sep_frule_method thms ctxt = SIMPLE_METHOD' (sep_ftac ctxt thms);
+*}
+
+method_setup "sep_drule" = {*
+  Attrib.thms >> sep_drule_method
+*} "drule after separating conjunction reordering"
+
+method_setup "sep_frule" = {*
+  Attrib.thms >> sep_frule_method
+*} "frule after separating conjunction reordering"
+
+
+section {* Backward Reasoning *}
+
+ML {*
+  fun sep_rule_method thms ctxt = SIMPLE_METHOD' (sep_rtac ctxt thms)
+*}
+
+method_setup "sep_rule" = {*
+  Attrib.thms >> sep_rule_method
+*} "applies rule after separating conjunction reordering"
+
+
+section {* Cancellation of Common Conjuncts via Elimination Rules *}
+
+ML {*
+  structure SepCancel_Rules = Named_Thms (
+    val name = @{binding "sep_cancel"};
+    val description = "sep_cancel rules";
+  );
+*}
+setup SepCancel_Rules.setup
+
+text {*
+  The basic @{text sep_cancel_tac} is minimal. It only eliminates
+  erule-derivable conjuncts between an assumption and the conclusion.
+
+  To have a more useful tactic, we augment it with more logic, to proceed as
+  follows:
+  \begin{itemize}
+  \item try discharge the goal first using @{text tac}
+  \item if that fails, invoke @{text sep_cancel_tac}
+  \item if @{text sep_cancel_tac} succeeds
+    \begin{itemize}
+    \item try to finish off with tac (but ok if that fails)
+    \item try to finish off with @{term sep_true} (but ok if that fails)
+    \end{itemize}
+  \end{itemize}
+  *}
+
+ML {*
+  fun sep_cancel_smart_tac ctxt tac =
+    let fun TRY' tac = tac ORELSE' (K all_tac)
+    in
+      tac
+      ORELSE' (sep_cancel_tac ctxt tac
+               THEN' TRY' tac
+               THEN' TRY' (rtac @{thm TrueI}))
+      ORELSE' (etac @{thm sep_conj_sep_emptyE}
+               THEN' sep_cancel_tac ctxt tac
+               THEN' TRY' tac
+               THEN' TRY' (rtac @{thm TrueI}))
+    end;
+
+  fun sep_cancel_smart_tac_rules ctxt etacs =
+      sep_cancel_smart_tac ctxt (FIRST' ([atac] @ etacs));
+
+  fun sep_cancel_method ctxt =
+    let
+      val etacs = map etac (SepCancel_Rules.get ctxt);
+    in
+      SIMPLE_METHOD' (sep_cancel_smart_tac_rules ctxt etacs)
+    end;
+
+  val sep_cancel_syntax = Method.sections [
+    Args.add -- Args.colon >> K (I, SepCancel_Rules.add)];
+*}
+
+method_setup sep_cancel = {*
+  sep_cancel_syntax >> K sep_cancel_method
+*} "Separating conjunction conjunct cancellation"
+
+text {*
+  As above, but use blast with a depth limit to figure out where cancellation
+  can be done. *}
+
+ML {*
+  fun sep_cancel_blast_method ctxt =
+    let
+      val rules = SepCancel_Rules.get ctxt;
+      val tac = Blast.depth_tac (ctxt addIs rules) 10;
+    in
+      SIMPLE_METHOD' (sep_cancel_smart_tac ctxt tac)
+    end;
+*}
+
+method_setup sep_cancel_blast = {*
+  sep_cancel_syntax >> K sep_cancel_blast_method
+*} "Separating conjunction conjunct cancellation using blast"
+
+end