--- a/Separation_Algebra/Sep_Tactics.thy	Fri Sep 12 00:47:15 2014 +0800
+++ b/Separation_Algebra/Sep_Tactics.thy	Sat Sep 13 10:07:14 2014 +0800
@@ -6,50 +6,78 @@
 header "Separation Logic Tactics"
 
 theory Sep_Tactics
-imports Separation_Algebra
+imports Separation_Algebra 
+uses "sep_tactics.ML"
 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 >> (fn n => fn ctxt => SIMPLE_METHOD' (sep_select_tac ctxt n))
+  Scan.lift Parse.int >> sep_select_method
 *} "Select nth separation conjunct in conclusion"
 
 method_setup sep_select_asm = {*
-  Scan.lift Parse.int >> (fn n => fn ctxt => SIMPLE_METHOD' (sep_select_asm_tac ctxt n))
+  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" = {*
-  Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
-    Attrib.thms >> (fn ((asm, occs), thms) => fn ctxt =>
-      SIMPLE_METHOD' ((if asm then sep_subst_asm_tac else sep_subst_tac) ctxt occs thms))
+  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 >> (fn thms => fn ctxt => SIMPLE_METHOD' (sep_dtac ctxt thms))
+  Attrib.thms >> sep_drule_method
 *} "drule after separating conjunction reordering"
 
 method_setup "sep_frule" = {*
-  Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (sep_ftac ctxt thms))
+  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 >> (fn thms => fn ctxt => SIMPLE_METHOD' (sep_rtac ctxt thms))
+  Attrib.thms >> sep_rule_method
 *} "applies rule after separating conjunction reordering"
 
 
@@ -97,31 +125,37 @@
   fun sep_cancel_smart_tac_rules ctxt etacs =
       sep_cancel_smart_tac ctxt (FIRST' ([atac] @ etacs));
 
-  val sep_cancel_syntax = Method.sections [
-    Args.add -- Args.colon >> K (I, SepCancel_Rules.add)] >> K ();
-*}
-
-method_setup sep_cancel = {*
-  sep_cancel_syntax >> (fn _ => fn ctxt =>
+  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)
+    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. *}
 
-method_setup sep_cancel_blast = {*
-  sep_cancel_syntax >> (fn _ => fn ctxt =>
+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)
+    end;
+*}
+
+method_setup sep_cancel_blast = {*
+  sep_cancel_syntax >> K sep_cancel_blast_method
 *} "Separating conjunction conjunct cancellation using blast"
 
 end