# HG changeset patch
# User wenzelm
# Date 1329248612 -3600
# Node ID 0632b8e56e46a72031ffbfbee7946e9dcfdbf30c
# Parent  4db76d47b51a19fac0dd38cf0b7d902af025e41c
method setup;

diff -r 4db76d47b51a -r 0632b8e56e46 src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Tue Feb 14 20:09:35 2012 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Tue Feb 14 20:43:32 2012 +0100
@@ -284,7 +284,7 @@
 done
 
 
-(* generalizing the proof above to a tactic *)
+(* generalizing the proof above to a proof method *)
 
 ML {*
 
@@ -296,7 +296,7 @@
 
 fun mkex_induct_tac ctxt sch exA exB =
   let val ss = simpset_of ctxt in
-    EVERY1[Seq_induct_tac ctxt sch defs,
+    EVERY'[Seq_induct_tac ctxt sch defs,
            asm_full_simp_tac ss,
            SELECT_GOAL (safe_tac (Proof_Context.init_global @{theory Fun})),
            Seq_case_simp_tac ctxt exA,
@@ -313,6 +313,11 @@
 end
 *}
 
+method_setup mkex_induct = {*
+  Scan.lift (Args.name -- Args.name -- Args.name)
+    >> (fn ((sch, exA), exB) => fn ctxt => SIMPLE_METHOD' (mkex_induct_tac ctxt sch exA exB))
+*}
+
 
 (*---------------------------------------------------------------------------
                Projection of mkex(sch,exA,exB) onto A stutters on A
@@ -324,10 +329,7 @@
   Filter (%a. a:act A)$sch << filter_act$exA &
   Filter (%a. a:act B)$sch << filter_act$exB
   --> stutter (asig_of A) (s,ProjA2$(snd (mkex A B sch (s,exA) (t,exB))))"
-
-apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
-done
-
+  by (mkex_induct sch exA exB)
 
 lemma stutter_mkex_on_A: "[|
   Forall (%x. x:act (A||B)) sch ;
@@ -354,8 +356,7 @@
   Filter (%a. a:act A)$sch << filter_act$exA &
   Filter (%a. a:act B)$sch << filter_act$exB
   --> stutter (asig_of B) (t,ProjB2$(snd (mkex A B sch (s,exA) (t,exB))))"
-apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
-done
+  by (mkex_induct sch exA exB)
 
 
 lemma stutter_mkex_on_B: "[|
@@ -385,8 +386,7 @@
   Filter (%a. a:act B)$sch << filter_act$exB
   --> Filter_ex2 (asig_of A)$(ProjA2$(snd (mkex A B sch (s,exA) (t,exB)))) =
       Zip$(Filter (%a. a:act A)$sch)$(Map snd$exA)"
-apply (tactic {* mkex_induct_tac @{context} "sch" "exB" "exA" *})
-done
+  by (mkex_induct sch exB exA)
 
 (*---------------------------------------------------------------------------
                       zip$(proj1$y)$(proj2$y) = y   (using the lift operations)
@@ -448,8 +448,7 @@
       Zip$(Filter (%a. a:act B)$sch)$(Map snd$exB)"
 
 (* notice necessary change of arguments exA and exB *)
-apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
-done
+  by (mkex_induct sch exA exB)
 
 
 (*---------------------------------------------------------------------------
@@ -485,8 +484,7 @@
   Filter (%a. a:act B)$sch << filter_act$exB
    --> Forall (%x. fst x : act (A ||B))
          (snd (mkex A B sch (s,exA) (t,exB)))"
-apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
-done
+  by (mkex_induct sch exA exB)
 
 
 (* ------------------------------------------------------------------ *)