# HG changeset patch
# User matichuk <daniel.matichuk@nicta.com.au>
# Date 1464659134 -36000
# Node ID dc221b8945f20a3948177338e22b456c783985f6
# Parent  08369e33c1851c804c66c21bcea991acbc5e0961
allow multiple recursive methods to co-exist in order to support mutual recursion;

diff -r 08369e33c185 -r dc221b8945f2 src/HOL/Eisbach/Tests.thy
--- a/src/HOL/Eisbach/Tests.thy	Mon May 30 16:11:53 2016 +1000
+++ b/src/HOL/Eisbach/Tests.thy	Tue May 31 11:45:34 2016 +1000
@@ -591,4 +591,17 @@
 
 end
 
+subsection \<open>Mutual recursion via higher-order methods\<close>
+
+experiment begin
+
+method inner_method methods passed_method = (rule conjI; passed_method)
+
+method outer_method = (inner_method \<open>outer_method\<close> | assumption)
+
+lemma "Q \<Longrightarrow> R \<Longrightarrow> P \<Longrightarrow> (Q \<and> R) \<and> P"
+  by outer_method
+
 end
+
+end
diff -r 08369e33c185 -r dc221b8945f2 src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Mon May 30 16:11:53 2016 +1000
+++ b/src/HOL/Eisbach/method_closure.ML	Tue May 31 11:45:34 2016 +1000
@@ -32,8 +32,8 @@
 (
   type T =
     (Proof.context -> Method.method) Symtab.table *  (*dynamic methods*)
-    (term list -> Proof.context -> Method.method)  (*recursive method*);
-  fun init _ : T = (Symtab.empty, fn _ => fn _ => Method.fail);
+    (term list -> Proof.context -> Method.method) Symtab.table  (*recursive methods*);
+  fun init _ : T = (Symtab.empty, Symtab.empty);
 );
 
 fun lookup_dynamic_method ctxt full_name =
@@ -43,8 +43,12 @@
 
 val update_dynamic_method = Method_Definition.map o apfst o Symtab.update;
 
-fun get_recursive_method ts ctxt = #2 (Method_Definition.get ctxt) ts ctxt;
-val put_recursive_method = Method_Definition.map o apsnd o K;
+fun get_recursive_method full_name ts ctxt =
+  (case Symtab.lookup (#2 (Method_Definition.get ctxt)) full_name of
+    SOME m => m ts ctxt
+  | NONE => error ("Illegal use of internal Eisbach method: " ^ quote full_name));
+
+val put_recursive_method = Method_Definition.map o apsnd o Symtab.update;
 
 
 (* stored method closures *)
@@ -136,9 +140,9 @@
 
 (** apply method closure **)
 
-fun recursive_method vars body ts =
+fun recursive_method full_name vars body ts =
   let val m = method_instantiate vars body
-  in put_recursive_method m #> m ts end;
+  in put_recursive_method (full_name, m) #> m ts end;
 
 fun apply_method ctxt method_name terms facts methods =
   let
@@ -151,7 +155,7 @@
   in
     declare_facts named_thms facts
     #> fold update_dynamic_method (method_args ~~ methods)
-    #> recursive_method vars body terms
+    #> recursive_method method_name vars body terms
   end;
 
 
@@ -244,9 +248,12 @@
           Scan.succeed (fold Named_Theorems.clear uses_internal context, ())) --
          Method.sections modifiers)) >> (fn (ts, decl) => meth ts o decl);
 
+    val full_name = Local_Theory.full_name lthy name;
+
     val lthy3 = lthy2
       |> Method.local_setup (Binding.make (Binding.name_of name, Position.none))
-        (parser term_args get_recursive_method) "(internal)";
+        (parser term_args (get_recursive_method full_name)) "(internal)"
+      |> put_recursive_method (full_name, fn _ => fn _ => Method.fail);
 
     val (text, src) =
       read_closure (Config.put Proof_Context.dynamic_facts_dummy true lthy3) source;
@@ -260,7 +267,6 @@
 
     val text' = (Method.map_source o map) (Token.transform morphism) text;
     val term_args' = map (Morphism.term morphism) term_args;
-    val full_name = Local_Theory.full_name lthy name;
   in
     lthy3
     |> Local_Theory.close_target
@@ -270,7 +276,7 @@
     |> Method.local_setup name 
         (Args.context :|-- (fn ctxt =>
           let val {body, vars, ...} = get_closure ctxt full_name in
-            parser vars (recursive_method vars body) end)) ""
+            parser vars (recursive_method full_name vars body) end)) ""
     |> pair full_name
   end;