# HG changeset patch
# User wenzelm
# Date 1452986085 -3600
# Node ID 799a5306e2ed4302fb3ac1c4761173c4118554eb
# Parent  0aabc5931361c0e8ea3dd01a262b1e568f739fcc
more method definitions;

diff -r 0aabc5931361 -r 799a5306e2ed src/HOL/HOLCF/IOA/Abstraction.thy
--- a/src/HOL/HOLCF/IOA/Abstraction.thy	Sat Jan 16 23:35:55 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Abstraction.thy	Sun Jan 17 00:14:45 2016 +0100
@@ -88,7 +88,7 @@
   "is_abstraction h C A \<Longrightarrow>
     \<forall>s. reachable C s \<and> is_exec_frag C (s, xs) \<longrightarrow> is_exec_frag A (cex_abs h (s, xs))"
   apply (simp add: cex_abs_def)
-  apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>)
+  apply (pair_induct xs simp: is_exec_frag_def)
   txt \<open>main case\<close>
   apply (auto dest: reachable.reachable_n simp add: is_abstraction_def)
   done
@@ -164,7 +164,7 @@
   "ext C = ext A \<Longrightarrow> mk_trace C $ xs = mk_trace A $ (snd (cex_abs f (s, xs)))"
   apply (unfold cex_abs_def mk_trace_def filter_act_def)
   apply simp
-  apply (tactic \<open>pair_induct_tac @{context} "xs" [] 1\<close>)
+  apply (pair_induct xs)
   done
 
 
@@ -182,13 +182,13 @@
   apply (rule_tac x = "cex_abs h ex" in exI)
   apply auto
   text \<open>Traces coincide\<close>
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (pair ex)
   apply (rule traces_coincide_abs)
   apply (simp (no_asm) add: externals_def)
   apply (auto)[1]
 
   text \<open>\<open>cex_abs\<close> is execution\<close>
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (pair ex)
   apply (simp add: executions_def)
   text \<open>start state\<close>
   apply (rule conjI)
@@ -199,7 +199,7 @@
 
   text \<open>Liveness\<close>
   apply (simp add: temp_weakening_def2)
-   apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+   apply (pair ex)
   done
 
 
@@ -279,23 +279,23 @@
 
 (* FIXME: should be same as nil_is_Conc2 when all nils are turned to right side! *)
 lemma UU_is_Conc: "(UU = x @@ y) = (((x::'a Seq)= UU) | (x = nil \<and> y = UU))"
-  by (tactic \<open>Seq_case_simp_tac @{context} "x" 1\<close>)
+  by (Seq_case_simp x)
 
 lemma ex2seqConc [rule_format]:
   "Finite s1 \<longrightarrow> (\<forall>ex. (s \<noteq> nil \<and> s \<noteq> UU \<and> ex2seq ex = s1 @@ s) \<longrightarrow> (\<exists>ex'. s = ex2seq ex'))"
   apply (rule impI)
-  apply (tactic \<open>Seq_Finite_induct_tac @{context} 1\<close>)
+  apply Seq_Finite_induct
   apply blast
   text \<open>main case\<close>
   apply clarify
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-  apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+  apply (pair ex)
+  apply (Seq_case_simp x2)
   text \<open>\<open>UU\<close> case\<close>
   apply (simp add: nil_is_Conc)
   text \<open>\<open>nil\<close> case\<close>
   apply (simp add: nil_is_Conc)
   text \<open>cons case\<close>
-  apply (tactic \<open>pair_tac @{context} "aa" 1\<close>)
+  apply (pair aa)
   apply auto
   done
 
@@ -337,28 +337,28 @@
   apply (unfold temp_strengthening_def state_strengthening_def
     temp_sat_def satisfies_def Init_def unlift_def)
   apply auto
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-  apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  apply (pair ex)
+  apply (Seq_case_simp x2)
+  apply (pair a)
   done
 
 
 subsubsection \<open>Next\<close>
 
 lemma TL_ex2seq_UU: "TL $ (ex2seq (cex_abs h ex)) = UU \<longleftrightarrow> TL $ (ex2seq ex) = UU"
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-  apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-  apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  apply (pair ex)
+  apply (Seq_case_simp x2)
+  apply (pair a)
+  apply (Seq_case_simp s)
+  apply (pair a)
   done
 
 lemma TL_ex2seq_nil: "TL $ (ex2seq (cex_abs h ex)) = nil \<longleftrightarrow> TL $ (ex2seq ex) = nil"
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-  apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-  apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  apply (pair ex)
+  apply (Seq_case_simp x2)
+  apply (pair a)
+  apply (Seq_case_simp s)
+  apply (pair a)
   done
 
 (*important property of cex_absSeq: As it is a 1to1 correspondence,
@@ -368,18 +368,18 @@
 
 (* important property of ex2seq: can be shiftet, as defined "pointwise" *)
 lemma TLex2seq: "snd ex \<noteq> UU \<Longrightarrow> snd ex \<noteq> nil \<Longrightarrow> \<exists>ex'. TL$(ex2seq ex) = ex2seq ex'"
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-  apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  apply (pair ex)
+  apply (Seq_case_simp x2)
+  apply (pair a)
   apply auto
   done
 
 lemma ex2seqnilTL: "TL $ (ex2seq ex) \<noteq> nil \<longleftrightarrow> snd ex \<noteq> nil \<and> snd ex \<noteq> UU"
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-  apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-  apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  apply (pair ex)
+  apply (Seq_case_simp x2)
+  apply (pair a)
+  apply (Seq_case_simp s)
+  apply (pair a)
   done
 
 lemma strength_Next: "temp_strengthening P Q h \<Longrightarrow> temp_strengthening (Next P) (Next Q) h"
@@ -405,9 +405,9 @@
   apply (simp add: temp_weakening_def2 state_weakening_def2
     temp_sat_def satisfies_def Init_def unlift_def)
   apply auto
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-  apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  apply (pair ex)
+  apply (Seq_case_simp x2)
+  apply (pair a)
   done
 
 
diff -r 0aabc5931361 -r 799a5306e2ed src/HOL/HOLCF/IOA/CompoExecs.thy
--- a/src/HOL/HOLCF/IOA/CompoExecs.thy	Sat Jan 16 23:35:55 2016 +0100
+++ b/src/HOL/HOLCF/IOA/CompoExecs.thy	Sun Jan 17 00:14:45 2016 +0100
@@ -174,7 +174,7 @@
   "\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow>
     is_exec_frag A (fst s, Filter_ex2 (asig_of A) $ (ProjA2 $ xs)) \<and>
     is_exec_frag B (snd s, Filter_ex2 (asig_of B) $ (ProjB2 $ xs))"
-  apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>)
+  apply (pair_induct xs simp: is_exec_frag_def)
   text \<open>main case\<close>
   apply (auto simp add: trans_of_defs2)
   done
@@ -184,7 +184,7 @@
   "\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow>
     stutter (asig_of A) (fst s, ProjA2 $ xs) \<and>
     stutter (asig_of B) (snd s, ProjB2 $ xs)"
-  apply (tactic \<open>pair_induct_tac @{context} "xs" @{thms stutter_def is_exec_frag_def} 1\<close>)
+  apply (pair_induct xs simp: stutter_def is_exec_frag_def)
   text \<open>main case\<close>
   apply (auto simp add: trans_of_defs2)
   done
@@ -192,8 +192,7 @@
 lemma lemma_1_1c:
   \<comment> \<open>Executions of \<open>A \<parallel> B\<close> have only \<open>A\<close>- or \<open>B\<close>-actions\<close>
   "\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow> Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) xs"
-  apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
-    @{thm is_exec_frag_def}] 1\<close>)
+  apply (pair_induct xs simp: Forall_def sforall_def is_exec_frag_def)
   text \<open>main case\<close>
   apply auto
   apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
@@ -208,8 +207,7 @@
     stutter (asig_of B) (snd s, ProjB2 $ xs) \<and>
     Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) xs \<longrightarrow>
     is_exec_frag (A \<parallel> B) (s, xs)"
-  apply (tactic \<open>pair_induct_tac @{context} "xs"
-    @{thms Forall_def sforall_def is_exec_frag_def stutter_def} 1\<close>)
+  apply (pair_induct xs simp: Forall_def sforall_def is_exec_frag_def stutter_def)
   apply (auto simp add: trans_of_defs1 actions_asig_comp asig_of_par)
   done
 
@@ -221,7 +219,7 @@
     stutter (asig_of B) (ProjB ex) \<and>
     Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) (snd ex)"
   apply (simp add: executions_def ProjB_def Filter_ex_def ProjA_def starts_of_par)
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (pair ex)
   apply (rule iffI)
   text \<open>\<open>\<Longrightarrow>\<close>\<close>
   apply (erule conjE)+
diff -r 0aabc5931361 -r 799a5306e2ed src/HOL/HOLCF/IOA/CompoScheds.thy
--- a/src/HOL/HOLCF/IOA/CompoScheds.thy	Sat Jan 16 23:35:55 2016 +0100
+++ b/src/HOL/HOLCF/IOA/CompoScheds.thy	Sun Jan 17 00:14:45 2016 +0100
@@ -200,7 +200,7 @@
   \<comment> \<open>State-projections do not affect \<open>filter_act\<close>\<close>
   "filter_act $ (ProjA2 $ xs) = filter_act $ xs \<and>
     filter_act $ (ProjB2 $ xs) = filter_act $ xs"
-  by (tactic \<open>pair_induct_tac @{context} "xs" [] 1\<close>)
+  by (pair_induct xs)
 
 
 text \<open>
@@ -214,8 +214,7 @@
 
 lemma sch_actions_in_AorB:
   "\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow> Forall (\<lambda>x. x \<in> act (A \<parallel> B)) (filter_act $ xs)"
-  apply (tactic \<open>pair_induct_tac @{context} "xs"
-    @{thms is_exec_frag_def Forall_def sforall_def} 1\<close>)
+  apply (pair_induct xs simp: is_exec_frag_def Forall_def sforall_def)
   text \<open>main case\<close>
   apply auto
   apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
@@ -235,35 +234,34 @@
     Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and>
     Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow>
     filter_act $ (snd (mkex A B sch (s, exA) (t, exB))) = sch"
-  apply (tactic \<open>Seq_induct_tac @{context} "sch" [@{thm Filter_def}, @{thm Forall_def},
-    @{thm sforall_def}, @{thm mkex_def}] 1\<close>)
+  apply (Seq_induct sch simp: Filter_def Forall_def sforall_def mkex_def)
 
   text \<open>main case: splitting into 4 cases according to \<open>a \<in> A\<close>, \<open>a \<in> B\<close>\<close>
   apply auto
 
   text \<open>Case \<open>y \<in> A\<close>, \<open>y \<in> B\<close>\<close>
-  apply (tactic \<open>Seq_case_simp_tac @{context} "exA" 1\<close>)
+  apply (Seq_case_simp exA)
   text \<open>Case \<open>exA = UU\<close>, Case \<open>exA = nil\<close>\<close>
   text \<open>
     These \<open>UU\<close> and \<open>nil\<close> cases are the only places where the assumption
     \<open>filter A sch \<sqsubseteq> f_act exA\<close> is used!
     \<open>\<longrightarrow>\<close> to generate a contradiction using \<open>\<not> a \<leadsto> ss \<sqsubseteq> UU nil\<close>,
     using theorems \<open>Cons_not_less_UU\<close> and \<open>Cons_not_less_nil\<close>.\<close>
-  apply (tactic \<open>Seq_case_simp_tac @{context} "exB" 1\<close>)
+  apply (Seq_case_simp exB)
   text \<open>Case \<open>exA = a \<leadsto> x\<close>, \<open>exB = b \<leadsto> y\<close>\<close>
   text \<open>
-    Here it is important that \<open>Seq_case_simp_tac\<close> uses no \<open>!full!_simp_tac\<close>
+    Here it is important that @{method Seq_case_simp} uses no \<open>!full!_simp_tac\<close>
     for the cons case, as otherwise \<open>mkex_cons_3\<close> would not be rewritten
     without use of \<open>rotate_tac\<close>: then tactic would not be generally
     applicable.\<close>
   apply simp
 
   text \<open>Case \<open>y \<in> A\<close>, \<open>y \<notin> B\<close>\<close>
-  apply (tactic \<open>Seq_case_simp_tac @{context} "exA" 1\<close>)
+  apply (Seq_case_simp exA)
   apply simp
 
   text \<open>Case \<open>y \<notin> A\<close>, \<open>y \<in> B\<close>\<close>
-  apply (tactic \<open>Seq_case_simp_tac @{context} "exB" 1\<close>)
+  apply (Seq_case_simp exB)
   apply simp
 
   text \<open>Case \<open>y \<notin> A\<close>, \<open>y \<notin> B\<close>\<close>
@@ -373,7 +371,7 @@
 \<close>
 
 lemma Zip_Map_fst_snd: "Zip $ (Map fst $ y) $ (Map snd $ y) = y"
-  by (tactic \<open>Seq_induct_tac @{context} "y" [] 1\<close>)
+  by (Seq_induct y)
 
 
 text \<open>
@@ -399,8 +397,8 @@
     Filter (\<lambda>a. a \<in> act B) $ sch = filter_act $ (snd exB) \<Longrightarrow>
   Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA"
   apply (simp add: ProjA_def Filter_ex_def)
-  apply (tactic \<open>pair_tac @{context} "exA" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
+  apply (pair exA)
+  apply (pair exB)
   apply (rule conjI)
   apply (simp (no_asm) add: mkex_def)
   apply (simplesubst trick_against_eq_in_ass)
@@ -436,10 +434,10 @@
     Filter (\<lambda>a. a \<in> act B) $ sch = filter_act $ (snd exB) \<Longrightarrow>
     Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB"
   apply (simp add: ProjB_def Filter_ex_def)
-  apply (tactic \<open>pair_tac @{context} "exA" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
+  apply (pair exA)
+  apply (pair exB)
   apply (rule conjI)
-  apply (simp (no_asm) add: mkex_def)
+  apply (simp add: mkex_def)
   apply (simplesubst trick_against_eq_in_ass)
   back
   apply assumption
@@ -471,9 +469,9 @@
   apply (rule_tac x = "Filter_ex (asig_of B) (ProjB ex)" in bexI)
   prefer 2
   apply (simp add: compositionality_ex)
-  apply (simp (no_asm) add: Filter_ex_def ProjB_def lemma_2_1a lemma_2_1b)
+  apply (simp add: Filter_ex_def ProjB_def lemma_2_1a lemma_2_1b)
   apply (simp add: executions_def)
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (pair ex)
   apply (erule conjE)
   apply (simp add: sch_actions_in_AorB)
   text \<open>\<open>\<Longleftarrow>\<close>\<close>
@@ -482,14 +480,14 @@
   apply (rename_tac exA exB)
   apply (rule_tac x = "mkex A B sch exA exB" in bexI)
   text \<open>\<open>mkex\<close> actions are just the oracle\<close>
-  apply (tactic \<open>pair_tac @{context} "exA" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
+  apply (pair exA)
+  apply (pair exB)
   apply (simp add: Mapfst_mkex_is_sch)
   text \<open>\<open>mkex\<close> is an execution -- use compositionality on ex-level\<close>
   apply (simp add: compositionality_ex)
   apply (simp add: stutter_mkex_on_A stutter_mkex_on_B filter_mkex_is_exB filter_mkex_is_exA)
-  apply (tactic \<open>pair_tac @{context} "exA" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
+  apply (pair exA)
+  apply (pair exB)
   apply (simp add: mkex_actions_in_AorB)
   done
 
diff -r 0aabc5931361 -r 799a5306e2ed src/HOL/HOLCF/IOA/CompoTraces.thy
--- a/src/HOL/HOLCF/IOA/CompoTraces.thy	Sat Jan 16 23:35:55 2016 +0100
+++ b/src/HOL/HOLCF/IOA/CompoTraces.thy	Sun Jan 17 00:14:45 2016 +0100
@@ -170,7 +170,7 @@
   "compatible A B \<Longrightarrow>
     \<forall>schA schB. Forall (\<lambda>x. x \<in> act (A \<parallel> B)) tr \<longrightarrow>
       Forall (\<lambda>x. x \<in> act (A \<parallel> B)) (mksch A B $ tr $ schA $ schB)"
-  apply (tactic \<open>Seq_induct_tac @{context} "tr" @{thms Forall_def sforall_def mksch_def} 1\<close>)
+  apply (Seq_induct tr simp: Forall_def sforall_def mksch_def)
   apply auto
   apply (simp add: actions_of_par)
   apply (case_tac "a \<in> act A")
@@ -198,7 +198,7 @@
   "compatible B A \<Longrightarrow>
     \<forall>schA schB. Forall (\<lambda>x. x \<in> act B \<and> x \<notin> act A) tr \<longrightarrow>
       Forall (\<lambda>x. x \<in> act B \<and> x \<notin> act A) (mksch A B $ tr $ schA $ schB)"
-  apply (tactic \<open>Seq_induct_tac @{context} "tr" @{thms Forall_def sforall_def mksch_def} 1\<close>)
+  apply (Seq_induct tr simp: Forall_def sforall_def mksch_def)
   apply auto
   apply (rule Forall_Conc_impl [THEN mp])
   apply (simp add: intA_is_not_actB int_is_act)
@@ -208,7 +208,7 @@
   "compatible A B \<Longrightarrow>
     \<forall>schA schB. Forall (\<lambda>x. x \<in> act A \<and> x \<notin> act B) tr \<longrightarrow>
       Forall (\<lambda>x. x \<in> act A \<and> x \<notin> act B) (mksch A B $ tr $ schA $ schB)"
-  apply (tactic \<open>Seq_induct_tac @{context} "tr" @{thms Forall_def sforall_def mksch_def} 1\<close>)
+  apply (Seq_induct tr simp: Forall_def sforall_def mksch_def)
   apply auto
   apply (rule Forall_Conc_impl [THEN mp])
   apply (simp add: intA_is_not_actB int_is_act)
@@ -385,7 +385,7 @@
       Filter (\<lambda>a. a \<in> act A) $ tr \<sqsubseteq> Filter (\<lambda>a. a \<in> ext A) $ schA \<and>
       Filter (\<lambda>a. a \<in> act B) $ tr \<sqsubseteq> Filter (\<lambda>a. a \<in> ext B) $ schB
       \<longrightarrow> Filter (\<lambda>a. a \<in> ext (A \<parallel> B)) $ (mksch A B $ tr $ schA $ schB) = tr"
-  apply (tactic \<open>Seq_induct_tac @{context} "tr" @{thms Forall_def sforall_def mksch_def} 1\<close>)
+  apply (Seq_induct tr simp: Forall_def sforall_def mksch_def)
   text \<open>main case\<close>
   text \<open>splitting into 4 cases according to \<open>a \<in> A\<close>, \<open>a \<in> B\<close>\<close>
   apply auto
diff -r 0aabc5931361 -r 799a5306e2ed src/HOL/HOLCF/IOA/Deadlock.thy
--- a/src/HOL/HOLCF/IOA/Deadlock.thy	Sat Jan 16 23:35:55 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Deadlock.thy	Sun Jan 17 00:14:45 2016 +0100
@@ -17,7 +17,7 @@
   apply auto
   apply (frule inp_is_act)
   apply (simp add: executions_def)
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (pair ex)
   apply (rename_tac s ex)
   apply (subgoal_tac "Finite ex")
   prefer 2
diff -r 0aabc5931361 -r 799a5306e2ed src/HOL/HOLCF/IOA/LiveIOA.thy
--- a/src/HOL/HOLCF/IOA/LiveIOA.thy	Sat Jan 16 23:35:55 2016 +0100
+++ b/src/HOL/HOLCF/IOA/LiveIOA.thy	Sun Jan 17 00:14:45 2016 +0100
@@ -54,13 +54,13 @@
   apply (rule_tac x = "corresp_ex A f ex" in exI)
   apply auto
   text \<open>Traces coincide, Lemma 1\<close>
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (pair ex)
   apply (erule lemma_1 [THEN spec, THEN mp])
   apply (simp (no_asm) add: externals_def)
   apply (auto)[1]
   apply (simp add: executions_def reachable.reachable_0)
   text \<open>\<open>corresp_ex\<close> is execution, Lemma 2\<close>
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (pair ex)
   apply (simp add: executions_def)
   text \<open>start state\<close>
   apply (rule conjI)
diff -r 0aabc5931361 -r 799a5306e2ed src/HOL/HOLCF/IOA/RefCorrectness.thy
--- a/src/HOL/HOLCF/IOA/RefCorrectness.thy	Sat Jan 16 23:35:55 2016 +0100
+++ b/src/HOL/HOLCF/IOA/RefCorrectness.thy	Sun Jan 17 00:14:45 2016 +0100
@@ -184,7 +184,7 @@
       mk_trace C $ xs = mk_trace A $ (snd (corresp_ex A f (s, xs)))"
   supply split_if [split del]
   apply (unfold corresp_ex_def)
-  apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>)
+  apply (pair_induct xs simp: is_exec_frag_def)
   text \<open>cons case\<close>
   apply (auto simp add: mk_traceConc)
   apply (frule reachable.reachable_n)
@@ -204,7 +204,7 @@
     (\<forall>s. is_exec_frag A (s, xs) \<and> is_exec_frag A (t, ys) \<and>
       t = laststate (s, xs) \<longrightarrow> is_exec_frag A (s, xs @@ ys))"
   apply (rule impI)
-  apply (tactic \<open>Seq_Finite_induct_tac @{context} 1\<close>)
+  apply Seq_Finite_induct
   text \<open>main case\<close>
   apply (auto simp add: split_paired_all)
   done
@@ -219,7 +219,7 @@
   apply (unfold corresp_ex_def)
 
   apply simp
-  apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>)
+  apply (pair_induct xs simp: is_exec_frag_def)
 
   text \<open>main case\<close>
   apply auto
@@ -263,13 +263,13 @@
   apply (rule_tac x = "corresp_ex A f ex" in bexI)
 
   text \<open>Traces coincide, Lemma 1\<close>
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (pair ex)
   apply (erule lemma_1 [THEN spec, THEN mp])
   apply assumption+
   apply (simp add: executions_def reachable.reachable_0)
 
   text \<open>\<open>corresp_ex\<close> is execution, Lemma 2\<close>
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (pair ex)
   apply (simp add: executions_def)
   text \<open>start state\<close>
   apply (rule conjI)
@@ -311,13 +311,13 @@
   apply auto
 
   text \<open>Traces coincide, Lemma 1\<close>
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (pair ex)
   apply (erule lemma_1 [THEN spec, THEN mp])
   apply assumption+
   apply (simp add: executions_def reachable.reachable_0)
 
   text \<open>\<open>corresp_ex\<close> is execution, Lemma 2\<close>
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (pair ex)
   apply (simp add: executions_def)
   text \<open>start state\<close>
   apply (rule conjI)
@@ -336,14 +336,14 @@
   apply auto
 
   text \<open>Traces coincide, Lemma 1\<close>
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (pair ex)
   apply (erule lemma_1 [THEN spec, THEN mp])
   apply (simp (no_asm) add: externals_def)
   apply (auto)[1]
   apply (simp add: executions_def reachable.reachable_0)
 
   text \<open>\<open>corresp_ex\<close> is execution, Lemma 2\<close>
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (pair ex)
   apply (simp add: executions_def)
   text \<open>start state\<close>
   apply (rule conjI)
diff -r 0aabc5931361 -r 799a5306e2ed src/HOL/HOLCF/IOA/Sequence.thy
--- a/src/HOL/HOLCF/IOA/Sequence.thy	Sat Jan 16 23:35:55 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Sequence.thy	Sun Jan 17 00:14:45 2016 +0100
@@ -990,18 +990,40 @@
 (* induction on a sequence of pairs with pairsplitting and simplification *)
 fun pair_induct_tac ctxt s rws i =
   Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_induct} i
-  THEN pair_tac ctxt "a" (i+3)
-  THEN (REPEAT_DETERM (CHANGED (simp_tac ctxt (i+1))))
+  THEN pair_tac ctxt "a" (i + 3)
+  THEN (REPEAT_DETERM (CHANGED (simp_tac ctxt (i + 1))))
   THEN simp_tac (ctxt addsimps rws) i;
 \<close>
 
+method_setup Seq_case =
+  \<open>Scan.lift Args.name >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_tac ctxt s))\<close>
+
+method_setup Seq_case_simp =
+  \<open>Scan.lift Args.name >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_simp_tac ctxt s))\<close>
+
+method_setup Seq_induct =
+  \<open>Scan.lift Args.name --
+    Scan.optional ((Scan.lift (Args.$$$ "simp" -- Args.colon) |-- Attrib.thms)) []
+    >> (fn (s, rws) => fn ctxt => SIMPLE_METHOD' (Seq_induct_tac ctxt s rws))\<close>
+
+method_setup Seq_Finite_induct =
+  \<open>Scan.succeed (SIMPLE_METHOD' o Seq_Finite_induct_tac)\<close>
+
+method_setup pair =
+  \<open>Scan.lift Args.name >> (fn s => fn ctxt => SIMPLE_METHOD' (pair_tac ctxt s))\<close>
+
+method_setup pair_induct =
+  \<open>Scan.lift Args.name --
+    Scan.optional ((Scan.lift (Args.$$$ "simp" -- Args.colon) |-- Attrib.thms)) []
+    >> (fn (s, rws) => fn ctxt => SIMPLE_METHOD' (pair_induct_tac ctxt s rws))\<close>
+
 lemma Mapnil: "Map f $ s = nil \<longleftrightarrow> s = nil"
-  by (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+  by (Seq_case_simp s)
 
 lemma MapUU: "Map f $ s = UU \<longleftrightarrow> s = UU"
-  by (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+  by (Seq_case_simp s)
 
 lemma MapTL: "Map f $ (TL $ s) = TL $ (Map f $ s)"
-  by (tactic \<open>Seq_induct_tac @{context} "s" [] 1\<close>)
+  by (Seq_induct s)
 
 end
diff -r 0aabc5931361 -r 799a5306e2ed src/HOL/HOLCF/IOA/ShortExecutions.thy
--- a/src/HOL/HOLCF/IOA/ShortExecutions.thy	Sat Jan 16 23:35:55 2016 +0100
+++ b/src/HOL/HOLCF/IOA/ShortExecutions.thy	Sun Jan 17 00:14:45 2016 +0100
@@ -212,7 +212,7 @@
   apply auto
   apply (rule_tac x = "filter_act $ (Cut (\<lambda>a. fst a \<in> ext A) (snd ex))" in exI)
   apply (simp add: executions_def)
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (pair ex)
   apply auto
   apply (rule_tac x = "(x1, Cut (\<lambda>a. fst a \<in> ext A) x2)" in exI)
   apply simp
diff -r 0aabc5931361 -r 799a5306e2ed src/HOL/HOLCF/IOA/SimCorrectness.thy
--- a/src/HOL/HOLCF/IOA/SimCorrectness.thy	Sat Jan 16 23:35:55 2016 +0100
+++ b/src/HOL/HOLCF/IOA/SimCorrectness.thy	Sun Jan 17 00:14:45 2016 +0100
@@ -163,8 +163,8 @@
     \<forall>s s'. reachable C s \<and> is_exec_frag C (s, ex) \<and> (s, s') \<in> R \<longrightarrow>
       mk_trace C $ ex = mk_trace A $ ((corresp_ex_simC A R $ ex) s')"
   supply split_if [split del]
-  apply (tactic \<open>pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1\<close>)
-  (* cons case *)
+  apply (pair_induct ex simp: is_exec_frag_def)
+  text \<open>cons case\<close>
   apply auto
   apply (rename_tac ex a t s s')
   apply (simp add: mk_traceConc)
@@ -182,7 +182,7 @@
   "is_simulation R C A \<Longrightarrow>
     \<forall>s s'. reachable C s \<and> is_exec_frag C (s, ex) \<and> (s, s') \<in> R
       \<longrightarrow> is_exec_frag A (s', (corresp_ex_simC A R $ ex) s')"
-  apply (tactic \<open>pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1\<close>)
+  apply (pair_induct ex simp: is_exec_frag_def)
   text \<open>main case\<close>
   apply auto
   apply (rename_tac ex a t s s')
@@ -250,7 +250,7 @@
   apply (rule_tac x = "corresp_ex_sim A R ex" in bexI)
 
   text \<open>Traces coincide, Lemma 1\<close>
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (pair ex)
   apply (rename_tac s ex)
   apply (simp add: corresp_ex_sim_def)
   apply (rule_tac s = "s" in traces_coincide_sim)
@@ -258,7 +258,7 @@
   apply (simp add: executions_def reachable.reachable_0 sim_starts1)
 
   text \<open>\<open>corresp_ex_sim\<close> is execution, Lemma 2\<close>
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+  apply (pair ex)
   apply (simp add: executions_def)
   apply (rename_tac s ex)
 
diff -r 0aabc5931361 -r 799a5306e2ed src/HOL/HOLCF/IOA/TL.thy
--- a/src/HOL/HOLCF/IOA/TL.thy	Sat Jan 16 23:35:55 2016 +0100
+++ b/src/HOL/HOLCF/IOA/TL.thy	Sun Jan 17 00:14:45 2016 +0100
@@ -113,7 +113,7 @@
 lemma tsuffix_TL [rule_format]: "s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> tsuffix s2 (TL $ s) \<longrightarrow> tsuffix s2 s"
   apply (unfold tsuffix_def suffix_def)
   apply auto
-  apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+  apply (Seq_case_simp s)
   apply (rule_tac x = "a \<leadsto> s1" in exI)
   apply auto
   done
diff -r 0aabc5931361 -r 799a5306e2ed src/HOL/HOLCF/IOA/TLS.thy
--- a/src/HOL/HOLCF/IOA/TLS.thy	Sat Jan 16 23:35:55 2016 +0100
+++ b/src/HOL/HOLCF/IOA/TLS.thy	Sun Jan 17 00:14:45 2016 +0100
@@ -123,9 +123,9 @@
 
 
 lemma ex2seq_nUUnnil: "ex2seq exec \<noteq> UU \<and> ex2seq exec \<noteq> nil"
-  apply (tactic \<open>pair_tac @{context} "exec" 1\<close>)
-  apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  apply (pair exec)
+  apply (Seq_case_simp x2)
+  apply (pair a)
   done
 
 
@@ -143,30 +143,30 @@
   apply (simp split add: split_if)
   text \<open>\<open>TL = UU\<close>\<close>
   apply (rule conjI)
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-  apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-  apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  apply (pair ex)
+  apply (Seq_case_simp x2)
+  apply (pair a)
+  apply (Seq_case_simp s)
+  apply (pair a)
   text \<open>\<open>TL = nil\<close>\<close>
   apply (rule conjI)
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-  apply (tactic \<open>Seq_case_tac @{context} "x2" 1\<close>)
+  apply (pair ex)
+  apply (Seq_case x2)
   apply (simp add: unlift_def)
   apply fast
   apply (simp add: unlift_def)
   apply fast
   apply (simp add: unlift_def)
-  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-  apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  apply (pair a)
+  apply (Seq_case_simp s)
+  apply (pair a)
   text \<open>\<open>TL = cons\<close>\<close>
   apply (simp add: unlift_def)
-  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-  apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-  apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  apply (pair ex)
+  apply (Seq_case_simp x2)
+  apply (pair a)
+  apply (Seq_case_simp s)
+  apply (pair a)
   done
 
 end
diff -r 0aabc5931361 -r 799a5306e2ed src/HOL/HOLCF/IOA/Traces.thy
--- a/src/HOL/HOLCF/IOA/Traces.thy	Sat Jan 16 23:35:55 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Traces.thy	Sun Jan 17 00:14:45 2016 +0100
@@ -272,7 +272,7 @@
 declare laststate_UU [simp] laststate_nil [simp] laststate_cons [simp]
 
 lemma exists_laststate: "Finite ex \<Longrightarrow> \<forall>s. \<exists>u. laststate (s, ex) = u"
-  by (tactic "Seq_Finite_induct_tac @{context} 1")
+  by Seq_Finite_induct
 
 
 subsection \<open>\<open>has_trace\<close> \<open>mk_trace\<close>\<close>
@@ -297,8 +297,7 @@
 
 lemma execfrag_in_sig:
   "is_trans_of A \<Longrightarrow> \<forall>s. is_exec_frag A (s, xs) \<longrightarrow> Forall (\<lambda>a. a \<in> act A) (filter_act $ xs)"
-  apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def},
-    @{thm Forall_def}, @{thm sforall_def}] 1\<close>)
+  apply (pair_induct xs simp: is_exec_frag_def Forall_def sforall_def)
   text \<open>main case\<close>
   apply (auto simp add: is_trans_of_def)
   done
@@ -306,7 +305,7 @@
 lemma exec_in_sig:
   "is_trans_of A \<Longrightarrow> x \<in> executions A \<Longrightarrow> Forall (\<lambda>a. a \<in> act A) (filter_act $ (snd x))"
   apply (simp add: executions_def)
-  apply (tactic \<open>pair_tac @{context} "x" 1\<close>)
+  apply (pair x)
   apply (rule execfrag_in_sig [THEN spec, THEN mp])
   apply auto
   done
@@ -321,10 +320,10 @@
 
 (*only admissible in y, not if done in x!*)
 lemma execfrag_prefixclosed: "\<forall>x s. is_exec_frag A (s, x) \<and> y \<sqsubseteq> x \<longrightarrow> is_exec_frag A (s, y)"
-  apply (tactic \<open>pair_induct_tac @{context} "y" [@{thm is_exec_frag_def}] 1\<close>)
+  apply (pair_induct y simp: is_exec_frag_def)
   apply (intro strip)
-  apply (tactic \<open>Seq_case_simp_tac @{context} "x" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  apply (Seq_case_simp x)
+  apply (pair a)
   apply auto
   done
 
@@ -334,10 +333,10 @@
 (*second prefix notion for Finite x*)
 lemma exec_prefix2closed [rule_format]:
   "\<forall>y s. is_exec_frag A (s, x @@ y) \<longrightarrow> is_exec_frag A (s, x)"
-  apply (tactic \<open>pair_induct_tac @{context} "x" [@{thm is_exec_frag_def}] 1\<close>)
+  apply (pair_induct x simp: is_exec_frag_def)
   apply (intro strip)
-  apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
-  apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+  apply (Seq_case_simp s)
+  apply (pair a)
   apply auto
   done