--- 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
--- 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)+
--- 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
--- 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
--- 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
--- 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)
--- 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)
--- 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
--- 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
--- 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)
--- 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
--- 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
--- 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