diff -r a5f5b9336007 -r 1cde7bf45858 Separation_Algebra/Sep_Tactics.thy~
--- a/Separation_Algebra/Sep_Tactics.thy~	Sat Sep 13 10:07:14 2014 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,161 +0,0 @@
-(* 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