--- a/src/Doc/Tutorial/Inductive/AB.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/Doc/Tutorial/Inductive/AB.thy Wed Aug 10 09:33:54 2016 +0200
@@ -264,7 +264,7 @@
*}
apply(force simp add: min_less_iff_disj)
- apply(force split add: nat_diff_split)
+ apply(force split: nat_diff_split)
txt{*
The case @{prop"w = b#v"} is proved analogously:
@@ -278,7 +278,7 @@
apply(rule_tac n1=i and t=v in subst[OF append_take_drop_id])
apply(rule S_A_B.intros)
apply(force simp add: min_less_iff_disj)
-by(force simp add: min_less_iff_disj split add: nat_diff_split)
+by(force simp add: min_less_iff_disj split: nat_diff_split)
text{*
We conclude this section with a comparison of our proof with
--- a/src/Doc/Tutorial/Protocol/Event.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/Doc/Tutorial/Protocol/Event.thy Wed Aug 10 09:33:54 2016 +0200
@@ -125,13 +125,13 @@
lemma Says_imp_knows_Spy [rule_format]:
"Says A B X \<in> set evs --> X \<in> knows Spy evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
done
lemma Notes_imp_knows_Spy [rule_format]:
"Notes A X \<in> set evs --> A: bad --> X \<in> knows Spy evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
done
@@ -174,14 +174,14 @@
text{*Agents know what they say*}
lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs --> X \<in> knows A evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
apply blast
done
text{*Agents know what they note*}
lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs --> X \<in> knows A evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
apply blast
done
@@ -189,7 +189,7 @@
lemma Gets_imp_knows_agents [rule_format]:
"A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
done
@@ -200,7 +200,7 @@
Says A B X \<in> set evs | Gets A X \<in> set evs | Notes A X \<in> set evs | X \<in> initState A"
apply (erule rev_mp)
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
apply blast
done
@@ -211,7 +211,7 @@
Says A B X \<in> set evs | Notes A X \<in> set evs | X \<in> initState Spy"
apply (erule rev_mp)
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
apply blast
done
@@ -224,7 +224,7 @@
lemma initState_into_used: "X \<in> parts (initState B) ==> X \<in> used evs"
apply (induct_tac "evs")
-apply (simp_all add: parts_insert_knows_A split add: event.split, blast)
+apply (simp_all add: parts_insert_knows_A split: event.split, blast)
done
lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs"
--- a/src/Doc/Tutorial/Protocol/Public.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/Doc/Tutorial/Protocol/Public.thy Wed Aug 10 09:33:54 2016 +0200
@@ -130,7 +130,7 @@
lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs"
apply (induct_tac "evs")
apply (rule_tac x = 0 in exI)
-apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
+apply (simp_all (no_asm_simp) add: used_Cons split: event.split)
apply safe
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
done
--- a/src/HOL/Auth/Event.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Auth/Event.thy Wed Aug 10 09:33:54 2016 +0200
@@ -124,13 +124,13 @@
lemma Says_imp_knows_Spy [rule_format]:
"Says A B X \<in> set evs --> X \<in> knows Spy evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
done
lemma Notes_imp_knows_Spy [rule_format]:
"Notes A X \<in> set evs --> A: bad --> X \<in> knows Spy evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
done
@@ -164,14 +164,14 @@
text\<open>Agents know what they say\<close>
lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs --> X \<in> knows A evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
apply blast
done
text\<open>Agents know what they note\<close>
lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs --> X \<in> knows A evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
apply blast
done
@@ -179,7 +179,7 @@
lemma Gets_imp_knows_agents [rule_format]:
"A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
done
@@ -190,7 +190,7 @@
Says A B X \<in> set evs | Gets A X \<in> set evs | Notes A X \<in> set evs | X \<in> initState A"
apply (erule rev_mp)
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
apply blast
done
@@ -201,7 +201,7 @@
Says A B X \<in> set evs | Notes A X \<in> set evs | X \<in> initState Spy"
apply (erule rev_mp)
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
apply blast
done
@@ -214,7 +214,7 @@
lemma initState_into_used: "X \<in> parts (initState B) ==> X \<in> used evs"
apply (induct_tac "evs")
-apply (simp_all add: parts_insert_knows_A split add: event.split, blast)
+apply (simp_all add: parts_insert_knows_A split: event.split, blast)
done
lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs"
--- a/src/HOL/Auth/Public.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Auth/Public.thy Wed Aug 10 09:33:54 2016 +0200
@@ -309,7 +309,7 @@
text\<open>All public keys are visible\<close>
lemma spies_pubK [iff]: "Key (publicKey b A) \<in> spies evs"
apply (induct_tac "evs")
-apply (auto simp add: imageI knows_Cons split add: event.split)
+apply (auto simp add: imageI knows_Cons split: event.split)
done
lemmas analz_spies_pubK = spies_pubK [THEN analz.Inj]
@@ -319,14 +319,14 @@
lemma Spy_spies_bad_privateKey [intro!]:
"A \<in> bad ==> Key (privateKey b A) \<in> spies evs"
apply (induct_tac "evs")
-apply (auto simp add: imageI knows_Cons split add: event.split)
+apply (auto simp add: imageI knows_Cons split: event.split)
done
text\<open>Spy sees long-term shared keys of bad agents!\<close>
lemma Spy_spies_bad_shrK [intro!]:
"A \<in> bad ==> Key (shrK A) \<in> spies evs"
apply (induct_tac "evs")
-apply (simp_all add: imageI knows_Cons split add: event.split)
+apply (simp_all add: imageI knows_Cons split: event.split)
done
lemma publicKey_into_used [iff] :"Key (publicKey b A) \<in> used evs"
@@ -361,7 +361,7 @@
lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs"
apply (induct_tac "evs")
apply (rule_tac x = 0 in exI)
-apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
+apply (simp_all (no_asm_simp) add: used_Cons split: event.split)
apply safe
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
done
--- a/src/HOL/Auth/Shared.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Auth/Shared.thy Wed Aug 10 09:33:54 2016 +0200
@@ -78,7 +78,7 @@
(*Spy sees shared keys of agents!*)
lemma Spy_knows_Spy_bad [intro!]: "A: bad ==> Key (shrK A) \<in> knows Spy evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
+apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
done
(*For case analysis on whether or not an agent is compromised*)
@@ -123,7 +123,7 @@
lemma Nonce_supply_lemma: "\<exists>N. ALL n. N<=n --> Nonce n \<notin> used evs"
apply (induct_tac "evs")
apply (rule_tac x = 0 in exI)
-apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
+apply (simp_all (no_asm_simp) add: used_Cons split: event.split)
apply (metis le_sup_iff msg_Nonce_supply)
done
--- a/src/HOL/Auth/Smartcard/EventSC.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Auth/Smartcard/EventSC.thy Wed Aug 10 09:33:54 2016 +0200
@@ -196,13 +196,13 @@
lemma Says_imp_knows_Spy [rule_format]:
"Says A B X \<in> set evs \<longrightarrow> X \<in> knows Spy evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
done
lemma Notes_imp_knows_Spy [rule_format]:
"Notes A X \<in> set evs \<longrightarrow> A\<in> bad \<longrightarrow> X \<in> knows Spy evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
done
(*Nothing can be stated on a Gets event*)
@@ -210,13 +210,13 @@
lemma Inputs_imp_knows_Spy_secureM [rule_format (no_asm)]:
"Inputs Spy C X \<in> set evs \<longrightarrow> secureM \<longrightarrow> X \<in> knows Spy evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
done
lemma Inputs_imp_knows_Spy_insecureM [rule_format (no_asm)]:
"Inputs A C X \<in> set evs \<longrightarrow> insecureM \<longrightarrow> X \<in> knows Spy evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
done
(*Nothing can be stated on a C_Gets event*)
@@ -224,13 +224,13 @@
lemma Outpts_imp_knows_Spy_secureM [rule_format (no_asm)]:
"Outpts C Spy X \<in> set evs \<longrightarrow> secureM \<longrightarrow> X \<in> knows Spy evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
done
lemma Outpts_imp_knows_Spy_insecureM [rule_format (no_asm)]:
"Outpts C A X \<in> set evs \<longrightarrow> insecureM \<longrightarrow> X \<in> knows Spy evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
done
(*Nothing can be stated on an A_Gets event*)
@@ -290,14 +290,14 @@
text\<open>Agents know what they say\<close>
lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs \<longrightarrow> X \<in> knows A evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
apply blast
done
text\<open>Agents know what they note\<close>
lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs \<longrightarrow> X \<in> knows A evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
apply blast
done
@@ -305,14 +305,14 @@
lemma Gets_imp_knows_agents [rule_format]:
"A \<noteq> Spy \<longrightarrow> Gets A X \<in> set evs \<longrightarrow> X \<in> knows A evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
done
(*Agents know what they input to their smart card*)
lemma Inputs_imp_knows_agents [rule_format (no_asm)]:
"Inputs A (Card A) X \<in> set evs \<longrightarrow> X \<in> knows A evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
apply blast
done
@@ -323,14 +323,14 @@
lemma Outpts_imp_knows_agents_secureM [rule_format (no_asm)]:
"secureM \<longrightarrow> Outpts (Card A) A X \<in> set evs \<longrightarrow> X \<in> knows A evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
done
(*otherwise only the spy knows the outputs*)
lemma Outpts_imp_knows_agents_insecureM [rule_format (no_asm)]:
"insecureM \<longrightarrow> Outpts (Card A) A X \<in> set evs \<longrightarrow> X \<in> knows Spy evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
done
(*end lemmas about agents' knowledge*)
@@ -346,7 +346,7 @@
lemma initState_into_used: "X \<in> parts (initState B) \<Longrightarrow> X \<in> used evs"
apply (induct_tac "evs")
-apply (simp_all add: parts_insert_knows_A split add: event.split, blast)
+apply (simp_all add: parts_insert_knows_A split: event.split, blast)
done
simps_of_case used_Cons_simps[simp]: used_Cons
@@ -362,28 +362,28 @@
lemma Says_parts_used [rule_format (no_asm)]:
"Says A B X \<in> set evs \<longrightarrow> (parts {X}) \<subseteq> used evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
apply blast
done
lemma Notes_parts_used [rule_format (no_asm)]:
"Notes A X \<in> set evs \<longrightarrow> (parts {X}) \<subseteq> used evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
apply blast
done
lemma Outpts_parts_used [rule_format (no_asm)]:
"Outpts C A X \<in> set evs \<longrightarrow> (parts {X}) \<subseteq> used evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
apply blast
done
lemma Inputs_parts_used [rule_format (no_asm)]:
"Inputs A C X \<in> set evs \<longrightarrow> (parts {X}) \<subseteq> used evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) split add: event.split)
+apply (simp_all (no_asm_simp) split: event.split)
apply blast
done
--- a/src/HOL/Auth/Smartcard/Smartcard.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy Wed Aug 10 09:33:54 2016 +0200
@@ -137,7 +137,7 @@
(*Spy knows the pins of bad agents!*)
lemma Spy_knows_bad [intro!]: "A \<in> bad \<Longrightarrow> Key (pin A) \<in> knows Spy evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
+apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
done
(*Spy knows the long-term keys of cloned cards!*)
@@ -147,24 +147,24 @@
Key (pin A) \<in> knows Spy evs &
(\<forall> B. Key (pairK(B,A)) \<in> knows Spy evs)"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
+apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
done
lemma Spy_knows_cloned1 [intro!]: "C \<in> cloned \<Longrightarrow> Key (crdK C) \<in> knows Spy evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
+apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
done
lemma Spy_knows_cloned2 [intro!]: "\<lbrakk> Card A \<in> cloned; Card B \<in> cloned \<rbrakk>
\<Longrightarrow> Nonce (Pairkey(A,B))\<in> knows Spy evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
+apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
done
(*Spy only knows pins of bad agents!*)
lemma Spy_knows_Spy_bad [intro!]: "A\<in> bad \<Longrightarrow> Key (pin A) \<in> knows Spy evs"
apply (induct_tac "evs")
-apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split)
+apply (simp_all (no_asm_simp) add: imageI knows_Cons split: event.split)
done
--- a/src/HOL/Bali/AxCompl.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Bali/AxCompl.thy Wed Aug 10 09:33:54 2016 +0200
@@ -56,7 +56,7 @@
lemma nyinitcls_init_lvars [simp]:
"nyinitcls G ((init_lvars G C sig mode a' pvs) s) = nyinitcls G s"
- by (induct s) (simp add: init_lvars_def2 split add: if_split)
+ by (induct s) (simp add: init_lvars_def2 split: if_split)
lemma nyinitcls_emptyD: "\<lbrakk>nyinitcls G s = {}; is_class G C\<rbrakk> \<Longrightarrow> initd C s"
unfolding nyinitcls_def by fast
@@ -74,7 +74,7 @@
apply (erule_tac V="nyinitcls G (x, s) = rhs" for rhs in thin_rl)
apply (rule card_Suc_lemma [OF _ _ finite_nyinitcls])
apply (auto dest!: not_initedD elim!:
- simp add: nyinitcls_def inited_def split add: if_split_asm)
+ simp add: nyinitcls_def inited_def split: if_split_asm)
done
lemma inited_gext': "\<lbrakk>s\<le>|s';inited C (globs s)\<rbrakk> \<Longrightarrow> inited C (globs s')"
@@ -1072,7 +1072,7 @@
apply (rule ax_derivs.NewA
[where ?Q = "(\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>In1r (init_comp_ty T)
\<succ>\<rightarrow> (Y',s')) \<and>. G\<turnstile>init\<le>n"])
- apply (simp add: init_comp_ty_def split add: if_split)
+ apply (simp add: init_comp_ty_def split: if_split)
apply (rule conjI, clarsimp)
apply (rule MGFn_InitD [OF hyp, THEN conseq2])
apply (clarsimp intro: eval.Init)
--- a/src/HOL/Bali/Conform.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Bali/Conform.thy Wed Aug 10 09:33:54 2016 +0200
@@ -207,7 +207,7 @@
apply (unfold lconf_def)
apply safe
apply (case_tac [3] "n")
-apply (force split add: sum.split)+
+apply (force split: sum.split)+
done
lemma lconf_ext_list [rule_format (no_asm)]: "
@@ -288,7 +288,7 @@
apply (unfold wlconf_def)
apply safe
apply (case_tac [3] "n")
-apply (force split add: sum.split)+
+apply (force split: sum.split)+
done
lemma wlconf_ext_list [rule_format (no_asm)]: "
@@ -370,7 +370,7 @@
apply (drule_tac var_tys_Some_eq [THEN iffD1])
defer
apply (subst obj_ty_cong)
-apply (auto dest!: fields_table_SomeD split add: sum.split_asm obj_tag.split_asm)
+apply (auto dest!: fields_table_SomeD split: sum.split_asm obj_tag.split_asm)
done
subsubsection "state conformance"
--- a/src/HOL/Bali/Decl.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Bali/Decl.thy Wed Aug 10 09:33:54 2016 +0200
@@ -69,22 +69,22 @@
proof
fix x y z::acc_modi
show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
- by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split)
+ by (auto simp add: le_acc_def less_acc_def split: acc_modi.split)
show "x \<le> x" \<comment> reflexivity
by (auto simp add: le_acc_def)
{
assume "x \<le> y" "y \<le> z" \<comment> transitivity
then show "x \<le> z"
- by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split)
+ by (auto simp add: le_acc_def less_acc_def split: acc_modi.split)
next
assume "x \<le> y" "y \<le> x" \<comment> antisymmetry
moreover have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
- by (auto simp add: less_acc_def split add: acc_modi.split)
+ by (auto simp add: less_acc_def split: acc_modi.split)
ultimately show "x = y" by (unfold le_acc_def) iprover
next
fix x y:: acc_modi
show "x \<le> y \<or> y \<le> x"
- by (auto simp add: less_acc_def le_acc_def split add: acc_modi.split)
+ by (auto simp add: less_acc_def le_acc_def split: acc_modi.split)
}
qed
--- a/src/HOL/Bali/Eval.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Bali/Eval.thy Wed Aug 10 09:33:54 2016 +0200
@@ -1166,12 +1166,12 @@
[strip_tac @{context}, rotate_tac ~1, eresolve_tac @{context} @{thms eval_elim_cases}])\<close>)
(* 31 subgoals *)
prefer 28 (* Try *)
-apply (simp (no_asm_use) only: split add: if_split_asm)
+apply (simp (no_asm_use) only: split: if_split_asm)
(* 34 subgoals *)
prefer 30 (* Init *)
apply (case_tac "inited C (globs s0)", (simp only: if_True if_False simp_thms)+)
prefer 26 (* While *)
-apply (simp (no_asm_use) only: split add: if_split_asm, blast)
+apply (simp (no_asm_use) only: split: if_split_asm, blast)
(* 36 subgoals *)
apply (blast dest: unique_sxalloc unique_halloc split_pairD)+
done
--- a/src/HOL/Bali/State.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Bali/State.thy Wed Aug 10 09:33:54 2016 +0200
@@ -97,7 +97,7 @@
lemma obj_ty_widenD:
"G\<turnstile>obj_ty obj\<preceq>RefT t \<Longrightarrow> (\<exists>C. tag obj = CInst C) \<or> (\<exists>T k. tag obj = Arr T k)"
apply (unfold obj_ty_def)
-apply (auto split add: obj_tag.split_asm)
+apply (auto split: obj_tag.split_asm)
done
definition
@@ -207,7 +207,7 @@
fields_table G C (\<lambda>fn f. declclassf fn = C \<and> static f) nt
= Some T))"
apply (unfold var_tys_def arr_comps_def)
-apply (force split add: sum.split_asm sum.split obj_tag.split)
+apply (force split: sum.split_asm sum.split obj_tag.split)
done
@@ -704,7 +704,7 @@
lemma inited_gupdate [simp]: "inited C (g(r\<mapsto>obj)) = (inited C g \<or> r = Stat C)"
apply (unfold inited_def)
-apply (auto split add: st.split)
+apply (auto split: st.split)
done
lemma inited_init_class_obj [intro!]: "inited C (globs (init_class_obj G C s))"
--- a/src/HOL/Bali/TypeSafe.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Wed Aug 10 09:33:54 2016 +0200
@@ -213,7 +213,7 @@
apply (auto del: conjI dest!: not_initedD gext_new sxalloc_gext halloc_gext
simp add: lvar_def fvar_def2 avar_def2 init_lvars_def2
check_field_access_def check_method_access_def Let_def
- split del: if_split_asm split add: sum3.split)
+ split del: if_split_asm split: sum3.split)
(* 6 subgoals *)
apply force+
done
@@ -632,7 +632,7 @@
apply (case_tac "mode = IntVir")
apply (drule conf_RefTD)
apply (force intro!: conf_AddrI
- simp add: obj_class_def split add: obj_tag.split_asm)
+ simp add: obj_class_def split: obj_tag.split_asm)
apply clarsimp
apply safe
apply (erule (1) widen.subcls [THEN conf_widen])
@@ -655,7 +655,7 @@
lemma Throw_lemma: "\<lbrakk>G\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable; wf_prog G; (x1,s1)\<Colon>\<preceq>(G, L);
x1 = None \<longrightarrow> G,s1\<turnstile>a'\<Colon>\<preceq> Class tn\<rbrakk> \<Longrightarrow> (throw a' x1, s1)\<Colon>\<preceq>(G, L)"
-apply (auto split add: split_abrupt_if simp add: throw_def2)
+apply (auto split: split_abrupt_if simp add: throw_def2)
apply (erule conforms_xconf)
apply (frule conf_RefTD)
apply (auto elim: widen.subcls [THEN conf_widen])
@@ -674,7 +674,7 @@
"\<lbrakk>G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> (x2,s2); wf_prog G; (Some a, s1)\<Colon>\<preceq>(G, L); (x2,s2)\<Colon>\<preceq>(G, L);
dom (locals s1) \<subseteq> dom (locals s2)\<rbrakk>
\<Longrightarrow> (abrupt_if True (Some a) x2, s2)\<Colon>\<preceq>(G, L)"
-apply (auto elim: eval_gext' conforms_xgext split add: split_abrupt_if)
+apply (auto elim: eval_gext' conforms_xgext split: split_abrupt_if)
done
lemma FVar_lemma1:
@@ -700,7 +700,7 @@
apply (erule fields_table_SomeI, simp (no_asm))
apply clarsimp
apply (drule conf_RefTD, clarsimp, rule var_tys_Some_eq [THEN iffD2])
-apply (auto dest!: widen_Array split add: obj_tag.split)
+apply (auto dest!: widen_Array split: obj_tag.split)
apply (rule fields_table_SomeI)
apply (auto elim!: fields_mono subcls_is_class2)
done
@@ -829,7 +829,7 @@
=
(G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
apply (unfold lconf_def)
-apply (auto split add: lname.splits)
+apply (auto split: lname.splits)
done
lemma wlconf_map_lname [simp]:
@@ -837,7 +837,7 @@
=
(G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))"
apply (unfold wlconf_def)
-apply (auto split add: lname.splits)
+apply (auto split: lname.splits)
done
lemma lconf_map_ename [simp]:
@@ -845,7 +845,7 @@
=
(G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
apply (unfold lconf_def)
-apply (auto split add: ename.splits)
+apply (auto split: ename.splits)
done
lemma wlconf_map_ename [simp]:
@@ -853,7 +853,7 @@
=
(G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))"
apply (unfold wlconf_def)
-apply (auto split add: ename.splits)
+apply (auto split: ename.splits)
done
@@ -902,7 +902,7 @@
then None else Some (Class declC)))"
apply (simp add: init_lvars_def2)
apply (rule conforms_set_locals)
-apply (simp (no_asm_simp) split add: if_split)
+apply (simp (no_asm_simp) split: if_split)
apply (drule (4) DynT_conf)
apply clarsimp
(* apply intro *)
--- a/src/HOL/Binomial.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Binomial.thy Wed Aug 10 09:33:54 2016 +0200
@@ -317,7 +317,7 @@
text \<open>Another version of absorption, with \<open>-1\<close> instead of \<open>Suc\<close>.\<close>
lemma times_binomial_minus1_eq: "0 < k \<Longrightarrow> k * (n choose k) = n * ((n - 1) choose (k - 1))"
using Suc_times_binomial_eq [where n = "n - 1" and k = "k - 1"]
- by (auto split add: nat_diff_split)
+ by (auto split: nat_diff_split)
subsection \<open>The binomial theorem (courtesy of Tobias Nipkow):\<close>
--- a/src/HOL/Deriv.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Deriv.thy Wed Aug 10 09:33:54 2016 +0200
@@ -1095,7 +1095,7 @@
fix h :: real
assume "0 < h" "h < s" "x - h \<in> S"
with all [of "x - h"] show "f x < f (x-h)"
- proof (simp add: abs_if pos_less_divide_eq dist_real_def split add: if_split_asm)
+ proof (simp add: abs_if pos_less_divide_eq dist_real_def split: if_split_asm)
assume "- ((f (x-h) - f x) / h) < l" and h: "0 < h"
with l have "0 < (f (x-h) - f x) / h"
by arith
--- a/src/HOL/Finite_Set.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Finite_Set.thy Wed Aug 10 09:33:54 2016 +0200
@@ -1405,7 +1405,7 @@
apply (subgoal_tac "finite A \<and> A - {x} \<subseteq> F")
prefer 2 apply (blast intro: finite_subset, atomize)
apply (drule_tac x = "A - {x}" in spec)
- apply (simp add: card_Diff_singleton_if split add: if_split_asm)
+ apply (simp add: card_Diff_singleton_if split: if_split_asm)
apply (case_tac "card A", auto)
done
--- a/src/HOL/HOLCF/IOA/NTP/Impl.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy Wed Aug 10 09:33:54 2016 +0200
@@ -155,14 +155,14 @@
apply (rule impI)
apply (erule conjE)+
apply (simp (no_asm_simp) add: hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def
- split add: if_split)
+ split: if_split)
txt \<open>detour 2\<close>
apply (tactic "tac @{context} 1")
apply (tactic "tac_ren @{context} 1")
apply (rule impI)
apply (erule conjE)+
apply (simp add: Impl.hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def
- Multiset.delm_nonempty_def split add: if_split)
+ Multiset.delm_nonempty_def split: if_split)
apply (rule allI)
apply (rule conjI)
apply (rule impI)
--- a/src/HOL/HOLCF/IOA/NTP/Lemmas.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Lemmas.thy Wed Aug 10 09:33:54 2016 +0200
@@ -25,7 +25,7 @@
subsection \<open>Arithmetic\<close>
lemma pred_suc: "0<x ==> (x - 1 = y) = (x = Suc(y))"
- by (simp add: diff_Suc split add: nat.split)
+ by (simp add: diff_Suc split: nat.split)
lemmas [simp] = hd_append set_lemmas
--- a/src/HOL/HOLCF/IOA/RefCorrectness.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/HOLCF/IOA/RefCorrectness.thy Wed Aug 10 09:33:54 2016 +0200
@@ -189,7 +189,7 @@
apply (auto simp add: mk_traceConc)
apply (frule reachable.reachable_n)
apply assumption
- apply (auto simp add: move_subprop4 split add: if_split)
+ apply (auto simp add: move_subprop4 split: if_split)
done
--- a/src/HOL/HOLCF/IOA/Seq.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/HOLCF/IOA/Seq.thy Wed Aug 10 09:33:54 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Partial, Finite and Infinite Sequences (lazy lists), modeled as domain\<close>
theory Seq
-imports "../../HOLCF"
+imports "../HOLCF"
begin
default_sort pcpo
--- a/src/HOL/HOLCF/IOA/SimCorrectness.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/HOLCF/IOA/SimCorrectness.thy Wed Aug 10 09:33:54 2016 +0200
@@ -173,7 +173,7 @@
apply (erule_tac x = "t" in allE)
apply (erule_tac x = "SOME t'. \<exists>ex1. (t, t') \<in> R \<and> move A ex1 s' a t'" in allE)
apply (simp add: move_subprop5_sim [unfolded Let_def]
- move_subprop4_sim [unfolded Let_def] split add: if_split)
+ move_subprop4_sim [unfolded Let_def] split: if_split)
done
text \<open>Lemma 2: \<open>corresp_ex_sim\<close> is execution\<close>
--- a/src/HOL/HOLCF/IOA/TL.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/HOLCF/IOA/TL.thy Wed Aug 10 09:33:54 2016 +0200
@@ -128,7 +128,7 @@
apply (erule_tac x = "s" in allE)
apply (simp add: tsuffix_def suffix_refl)
text \<open>\<open>\<box>F \<^bold>\<longrightarrow> \<circle>\<box>F\<close>\<close>
- apply (simp split add: if_split)
+ apply (simp split: if_split)
apply auto
apply (drule tsuffix_TL2)
apply assumption+
--- a/src/HOL/HOLCF/IOA/TLS.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/HOLCF/IOA/TLS.thy Wed Aug 10 09:33:54 2016 +0200
@@ -140,7 +140,7 @@
\<^bold>\<longrightarrow> (\<circle>(Init (\<lambda>(s, a, t). Q s))))"
apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def)
apply clarify
- apply (simp split add: if_split)
+ apply (simp split: if_split)
text \<open>\<open>TL = UU\<close>\<close>
apply (rule conjI)
apply (pair ex)
--- a/src/HOL/IOA/Solve.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/IOA/Solve.thy Wed Aug 10 09:33:54 2016 +0200
@@ -86,7 +86,7 @@
apply (simp cong del: if_weak_cong
add: executions_def is_execution_fragment_def par_def starts_of_def
trans_of_def filter_oseq_def
- split add: option.split)
+ split: option.split)
done
@@ -103,7 +103,7 @@
apply (simp cong del: if_weak_cong
add: executions_def is_execution_fragment_def par_def starts_of_def
trans_of_def filter_oseq_def
- split add: option.split)
+ split: option.split)
done
declare if_split [split del] if_weak_cong [cong del]
@@ -143,7 +143,7 @@
(* delete auxiliary subgoal *)
prefer 2
apply force
- apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: if_split)
+ apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split: if_split)
apply (tactic \<open>
REPEAT((resolve_tac @{context} [conjI, impI] 1 ORELSE eresolve_tac @{context} [conjE] 1) THEN
asm_full_simp_tac(@{context} addsimps [@{thm comp1_reachable}, @{thm comp2_reachable}]) 1)\<close>)
@@ -157,7 +157,7 @@
apply (simp (no_asm))
(* execution is indeed an execution of C *)
apply (simp add: executions_def is_execution_fragment_def par_def
- starts_of_def trans_of_def rename_def split add: option.split)
+ starts_of_def trans_of_def rename_def split: option.split)
apply force
done
@@ -197,7 +197,7 @@
apply assumption
apply simp
(* x is internal *)
- apply (simp (no_asm) add: de_Morgan_disj de_Morgan_conj not_ex cong add: conj_cong)
+ apply (simp (no_asm) cong add: conj_cong)
apply (rule impI)
apply (erule conjE)
apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa)
--- a/src/HOL/Int.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Int.thy Wed Aug 10 09:33:54 2016 +0200
@@ -1190,7 +1190,7 @@
apply (case_tac "k = f (Suc n)")
apply force
apply (erule impE)
- apply (simp add: abs_if split add: if_split_asm)
+ apply (simp add: abs_if split: if_split_asm)
apply (blast intro: le_SucI)
done
--- a/src/HOL/Library/positivstellensatz.ML Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Wed Aug 10 09:33:54 2016 +0200
@@ -266,7 +266,7 @@
by auto};
val abs_split' = @{lemma "P \<bar>x::'a::linordered_idom\<bar> == (x >= 0 & P x | x < 0 & P (-x))"
- by (atomize (full)) (auto split add: abs_split)};
+ by (atomize (full)) (auto split: abs_split)};
val max_split = @{lemma "P (max x y) == ((x::'a::linorder) <= y & P y | x > y & P x)"
by (atomize (full)) (cases "x <= y", auto simp add: max_def)};
--- a/src/HOL/Map.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Map.thy Wed Aug 10 09:33:54 2016 +0200
@@ -312,7 +312,7 @@
apply (induct xs)
apply simp
apply (rule ext)
-apply (simp split add: option.split)
+apply (simp split: option.split)
done
lemma finite_range_map_of_map_add:
--- a/src/HOL/MicroJava/J/Example.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/MicroJava/J/Example.thy Wed Aug 10 09:33:54 2016 +0200
@@ -191,7 +191,7 @@
lemma class_tprgD:
"class tprg C = Some z ==> C=Object \<or> C=Base \<or> C=Ext \<or> C=Xcpt NP \<or> C=Xcpt ClassCast \<or> C=Xcpt OutOfMemory"
apply (unfold ObjectC_def ClassCastC_def NullPointerC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
-apply (auto split add: if_split_asm simp add: map_of_Cons)
+apply (auto split: if_split_asm simp add: map_of_Cons)
done
lemma not_class_subcls_class [elim!]: "(C, C) \<in> (subcls1 tprg)^+ ==> R"
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Wed Aug 10 09:33:54 2016 +0200
@@ -234,7 +234,7 @@
apply( erule conjI)
apply( clarsimp)
apply( drule eval_no_xcpt)
-apply( simp split add: binop.split)
+apply( simp split: binop.split)
\<comment> "12 LAcc"
apply simp
--- a/src/HOL/MicroJava/J/WellForm.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy Wed Aug 10 09:33:54 2016 +0200
@@ -146,7 +146,7 @@
lemma wf_cdecl_supD:
"!!r. \<lbrakk>ws_cdecl G (C,D,r); C \<noteq> Object\<rbrakk> \<Longrightarrow> is_class G D"
apply (unfold ws_cdecl_def)
-apply (auto split add: option.split_asm)
+apply (auto split: option.split_asm)
done
lemma subcls_asym: "[|ws_prog G; (C, D) \<in> (subcls1 G)^+|] ==> (D, C) \<notin> (subcls1 G)^+"
@@ -534,7 +534,7 @@
apply (simp add: map_of_map)
apply (clarify)
apply (subst method_rec, assumption+)
- apply (simp add: map_add_def map_of_map split add: option.split)
+ apply (simp add: map_add_def map_of_map split: option.split)
done
@@ -554,7 +554,7 @@
apply (simp add: map_of_map)
apply (clarify)
apply (subst method_rec, assumption+)
- apply (simp add: map_add_def map_of_map split add: option.split)
+ apply (simp add: map_add_def map_of_map split: option.split)
done
lemma fields_in_fd [rule_format (no_asm)]: "\<lbrakk> wf_prog wf_mb G; is_class G C\<rbrakk>
--- a/src/HOL/MicroJava/J/WellType.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy Wed Aug 10 09:33:54 2016 +0200
@@ -215,7 +215,7 @@
apply (rule ty_expr_ty_exprs_wt_stmt.induct)
apply auto
apply ( erule typeof_empty_is_type)
-apply ( simp split add: if_split_asm)
+apply ( simp split: if_split_asm)
apply ( drule field_fields)
apply ( drule (1) fields_is_type)
apply ( simp (no_asm_simp))
--- a/src/HOL/NanoJava/Example.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/NanoJava/Example.thy Wed Aug 10 09:33:54 2016 +0200
@@ -184,7 +184,7 @@
apply rule
apply (rule hoare_ehoare.Asm) (* 20 *)
apply (rule_tac a = "((case n of 0 \<Rightarrow> 0 | Suc m \<Rightarrow> m),m+1)" in UN_I, rule+)
-apply (clarsimp split add: nat.split_asm dest!: Nat_atleast_mono)
+apply (clarsimp split: nat.split_asm dest!: Nat_atleast_mono)
apply rule
apply (rule hoare_ehoare.Call) (* 21 *)
apply (rule hoare_ehoare.LAcc)
--- a/src/HOL/Nat.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Nat.thy Wed Aug 10 09:33:54 2016 +0200
@@ -1940,19 +1940,19 @@
lemma diff_le_mono: "m \<le> n \<Longrightarrow> m - l \<le> n - l"
for m n l :: nat
- by (auto dest: less_imp_le less_imp_Suc_add split add: nat_diff_split)
+ by (auto dest: less_imp_le less_imp_Suc_add split: nat_diff_split)
lemma diff_le_mono2: "m \<le> n \<Longrightarrow> l - n \<le> l - m"
for m n l :: nat
- by (auto dest: less_imp_le le_Suc_ex less_imp_Suc_add less_le_trans split add: nat_diff_split)
+ by (auto dest: less_imp_le le_Suc_ex less_imp_Suc_add less_le_trans split: nat_diff_split)
lemma diff_less_mono2: "m < n \<Longrightarrow> m < l \<Longrightarrow> l - n < l - m"
for m n l :: nat
- by (auto dest: less_imp_Suc_add split add: nat_diff_split)
+ by (auto dest: less_imp_Suc_add split: nat_diff_split)
lemma diffs0_imp_equal: "m - n = 0 \<Longrightarrow> n - m = 0 \<Longrightarrow> m = n"
for m n :: nat
- by (simp split add: nat_diff_split)
+ by (simp split: nat_diff_split)
lemma min_diff: "min (m - i) (n - i) = min m n - i"
for m n i :: nat
--- a/src/HOL/Nat_Transfer.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Nat_Transfer.thy Wed Aug 10 09:33:54 2016 +0200
@@ -1,4 +1,3 @@
-
(* Authors: Jeremy Avigad and Amine Chaieb *)
section \<open>Generic transfer machinery; specific transfer from nats to ints and back.\<close>
@@ -82,7 +81,7 @@
text \<open>first-order quantifiers\<close>
lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
- by (simp split add: split_nat)
+ by (simp split: split_nat)
lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
proof
--- a/src/HOL/Nonstandard_Analysis/HyperDef.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/HyperDef.thy Wed Aug 10 09:33:54 2016 +0200
@@ -285,7 +285,7 @@
by (simp add: abs_if)
lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = \<bar>x + - z\<bar> ==> y = z | x = y"
-by (simp add: abs_if split add: if_split_asm)
+by (simp add: abs_if split: if_split_asm)
subsection\<open>Embedding the Naturals into the Hyperreals\<close>
--- a/src/HOL/Numeral_Simprocs.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Numeral_Simprocs.thy Wed Aug 10 09:33:54 2016 +0200
@@ -32,35 +32,35 @@
lemma nat_diff_add_eq1:
"j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
-by (simp split add: nat_diff_split add: add_mult_distrib)
+by (simp split: nat_diff_split add: add_mult_distrib)
lemma nat_diff_add_eq2:
"i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"
-by (simp split add: nat_diff_split add: add_mult_distrib)
+by (simp split: nat_diff_split add: add_mult_distrib)
lemma nat_eq_add_iff1:
"j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
+by (auto split: nat_diff_split simp add: add_mult_distrib)
lemma nat_eq_add_iff2:
"i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
+by (auto split: nat_diff_split simp add: add_mult_distrib)
lemma nat_less_add_iff1:
"j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
+by (auto split: nat_diff_split simp add: add_mult_distrib)
lemma nat_less_add_iff2:
"i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
+by (auto split: nat_diff_split simp add: add_mult_distrib)
lemma nat_le_add_iff1:
"j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
+by (auto split: nat_diff_split simp add: add_mult_distrib)
lemma nat_le_add_iff2:
"i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
-by (auto split add: nat_diff_split simp add: add_mult_distrib)
+by (auto split: nat_diff_split simp add: add_mult_distrib)
text \<open>For \<open>cancel_numeral_factors\<close>\<close>
--- a/src/HOL/Option.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Option.thy Wed Aug 10 09:33:54 2016 +0200
@@ -100,13 +100,13 @@
by (auto split: option.split)
lemma map_option_is_None [iff]: "(map_option f opt = None) = (opt = None)"
- by (simp add: map_option_case split add: option.split)
+ by (simp add: map_option_case split: option.split)
lemma None_eq_map_option_iff [iff]: "None = map_option f x \<longleftrightarrow> x = None"
by(cases x) simp_all
lemma map_option_eq_Some [iff]: "(map_option f xo = Some y) = (\<exists>z. xo = Some z \<and> f z = y)"
- by (simp add: map_option_case split add: option.split)
+ by (simp add: map_option_case split: option.split)
lemma map_option_o_case_sum [simp]:
"map_option f o case_sum g h = case_sum (map_option f o g) (map_option f o h)"
--- a/src/HOL/Power.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Power.thy Wed Aug 10 09:33:54 2016 +0200
@@ -112,7 +112,7 @@
lemma power_minus_mult:
"0 < n \<Longrightarrow> a ^ (n - 1) * a = a ^ n"
- by (simp add: power_commutes split add: nat_diff_split)
+ by (simp add: power_commutes split: nat_diff_split)
end
--- a/src/HOL/SET_Protocol/Cardholder_Registration.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy Wed Aug 10 09:33:54 2016 +0200
@@ -493,7 +493,7 @@
lemma K_fresh_not_KeyCryptKey:
"[|\<forall>C. DK \<noteq> priEK C; Key K \<notin> used evs|] ==> ~ KeyCryptKey DK K evs"
apply (induct evs)
-apply (auto simp add: parts_insert2 split add: event.split)
+apply (auto simp add: parts_insert2 split: event.split)
done
@@ -513,7 +513,7 @@
text\<open>Lemma for message 5: pubSK C is never used to encrypt Keys.\<close>
lemma pubSK_not_KeyCryptKey [simp]: "~ KeyCryptKey (pubSK C) K evs"
apply (induct_tac "evs")
-apply (auto simp add: parts_insert2 split add: event.split)
+apply (auto simp add: parts_insert2 split: event.split)
done
text\<open>Lemma for message 6: either cardSK is compromised (when we don't care)
@@ -690,7 +690,7 @@
text\<open>Lemma for message 5: pubSK C is never used to encrypt Nonces.\<close>
lemma pubSK_not_KeyCryptNonce [simp]: "~ KeyCryptNonce (pubSK C) N evs"
apply (induct_tac "evs")
-apply (auto simp add: parts_insert2 split add: event.split)
+apply (auto simp add: parts_insert2 split: event.split)
done
text\<open>Lemma for message 6: either cardSK is compromised (when we don't care)
--- a/src/HOL/SET_Protocol/Public_SET.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/SET_Protocol/Public_SET.thy Wed Aug 10 09:33:54 2016 +0200
@@ -300,7 +300,7 @@
text\<open>Spy knows all public keys\<close>
lemma knows_Spy_pubEK_i [iff]: "Key (publicKey b A) \<in> knows Spy evs"
apply (induct_tac "evs")
-apply (simp_all add: imageI knows_Cons split add: event.split)
+apply (simp_all add: imageI knows_Cons split: event.split)
done
declare knows_Spy_pubEK_i [THEN analz.Inj, iff]
@@ -324,7 +324,7 @@
lemma Nonce_supply_lemma: "\<exists>N. \<forall>n. N<=n --> Nonce n \<notin> used evs"
apply (induct_tac "evs")
apply (rule_tac x = 0 in exI)
-apply (simp_all add: used_Cons split add: event.split, safe)
+apply (simp_all add: used_Cons split: event.split, safe)
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
done
--- a/src/HOL/UNITY/Lift_prog.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/UNITY/Lift_prog.thy Wed Aug 10 09:33:54 2016 +0200
@@ -41,7 +41,7 @@
lemma insert_map_delete_map_eq: "(insert_map i x (delete_map i g)) = g(i:=x)"
apply (rule ext)
-apply (auto split add: nat_diff_split)
+apply (auto split: nat_diff_split)
done
subsection\<open>Injectiveness proof\<close>
@@ -120,7 +120,7 @@
else if i<j then insert_map j t (f(i:=s))
else insert_map j t (f(i - Suc 0 := s)))"
apply (rule ext)
-apply (simp split add: nat_diff_split)
+apply (simp split: nat_diff_split)
txt\<open>This simplification is VERY slow\<close>
done
--- a/src/HOL/UNITY/Simple/Reachability.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/UNITY/Simple/Reachability.thy Wed Aug 10 09:33:54 2016 +0200
@@ -94,7 +94,7 @@
lemma Detects_part1: "F \<in> {s. (root,v) \<in> REACHABLE} LeadsTo reachable v"
apply (rule single_LeadsTo_I)
-apply (simp split add: if_split_asm)
+apply (simp split: if_split_asm)
apply (rule MA1 [THEN Always_LeadsToI])
apply (erule REACHABLE_LeadsTo_reachable [THEN LeadsTo_weaken_L], auto)
done
@@ -147,7 +147,7 @@
==> (\<Inter>v \<in> V. \<Inter>e \<in> E. {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))}
\<inter> nmsg_eq 0 e) \<subseteq> final"
apply (unfold final_def Equality_def)
-apply (auto split add: if_split_asm)
+apply (auto split!: if_split)
apply (frule E_imp_in_V_L, blast)
done
@@ -197,7 +197,7 @@
(-{s. (v,w) \<in> E} \<union> (nmsg_eq 0 (v,w))))"
apply (unfold final_def)
apply (rule subset_antisym, blast)
-apply (auto split add: if_split_asm)
+apply (auto split: if_split_asm)
apply (blast dest: E_imp_in_V_L E_imp_in_V_R)+
done
--- a/src/HOL/UNITY/Simple/Token.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/UNITY/Simple/Token.thy Wed Aug 10 09:33:54 2016 +0200
@@ -82,7 +82,7 @@
"[| i<N; j<N |] ==> ((next i, i) \<in> nodeOrder j) = (i \<noteq> j)"
apply (unfold nodeOrder_def next_def)
apply (auto simp add: mod_Suc mod_geq)
-apply (auto split add: nat_diff_split simp add: linorder_neq_iff mod_geq)
+apply (auto split: nat_diff_split simp add: linorder_neq_iff mod_geq)
done
text\<open>From "A Logic for Concurrent Programming", but not used in Chapter 4.
--- a/src/HOL/Word/Bool_List_Representation.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy Wed Aug 10 09:33:54 2016 +0200
@@ -300,7 +300,7 @@
"n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n)"
apply (induct xs)
apply simp
- apply (clarsimp simp add : nth_append nth.simps split add : nat.split)
+ apply (clarsimp simp add : nth_append nth.simps split: nat.split)
apply (rule_tac f = "\<lambda>n. xs ! n" in arg_cong)
apply arith
done
@@ -577,11 +577,11 @@
lemma take_takefill':
"!!w n. n = k + m ==> take k (takefill fill n w) = takefill fill k w"
- by (induct k) (auto split add : list.split)
+ by (induct k) (auto split: list.split)
lemma drop_takefill:
"!!w. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
- by (induct k) (auto split add : list.split)
+ by (induct k) (auto split: list.split)
lemma takefill_le [simp]:
"m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
--- a/src/ZF/ArithSimp.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/ZF/ArithSimp.thy Wed Aug 10 09:33:54 2016 +0200
@@ -542,7 +542,7 @@
lemma diff_lt_imp_lt: "[|(k#-i) < (k#-j); i\<in>nat; j\<in>nat; k\<in>nat|] ==> j<i"
apply (erule rev_mp)
-apply (simp split add: nat_diff_split, auto)
+apply (simp split: nat_diff_split, auto)
apply (blast intro: add_le_self lt_trans1)
apply (rule not_le_iff_lt [THEN iffD1], auto)
apply (subgoal_tac "i #+ da < j #+ d", force)
@@ -552,7 +552,7 @@
lemma lt_imp_diff_lt: "[|j<i; i\<le>k; k\<in>nat|] ==> (k#-i) < (k#-j)"
apply (frule le_in_nat, assumption)
apply (frule lt_nat_in_nat, assumption)
-apply (simp split add: nat_diff_split, auto)
+apply (simp split: nat_diff_split, auto)
apply (blast intro: lt_asym lt_trans2)
apply (blast intro: lt_irrefl lt_trans2)
apply (rule not_le_iff_lt [THEN iffD1], auto)
--- a/src/ZF/IntDiv_ZF.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/ZF/IntDiv_ZF.thy Wed Aug 10 09:33:54 2016 +0200
@@ -531,7 +531,7 @@
apply assumption+
apply (case_tac "#0 $< ba")
apply (simp add: posDivAlg_eqn adjust_def integ_of_type
- split add: split_if_asm)
+ split: split_if_asm)
apply clarify
apply (simp add: int_0_less_mult_iff not_zle_iff_zless)
apply (simp add: not_zless_iff_zle)
@@ -625,7 +625,7 @@
apply assumption+
apply (case_tac "#0 $< ba")
apply (simp add: negDivAlg_eqn adjust_def integ_of_type
- split add: split_if_asm)
+ split: split_if_asm)
apply clarify
apply (simp add: int_0_less_mult_iff not_zle_iff_zless)
apply (simp add: not_zless_iff_zle)
--- a/src/ZF/Int_ZF.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/ZF/Int_ZF.thy Wed Aug 10 09:33:54 2016 +0200
@@ -283,7 +283,7 @@
by (simp add: nat_of_def)
lemma nat_of_congruent: "(\<lambda>x. (\<lambda>\<langle>x,y\<rangle>. x #- y)(x)) respects intrel"
-by (auto simp add: congruent_def split add: nat_diff_split)
+by (auto simp add: congruent_def split: nat_diff_split)
lemma raw_nat_of:
"[| x\<in>nat; y\<in>nat |] ==> raw_nat_of(intrel``{<x,y>}) = x#-y"
@@ -367,7 +367,7 @@
apply (subgoal_tac "intify(z) \<in> int")
apply (simp add: int_def)
apply (auto simp add: znegative nat_of_def raw_nat_of
- split add: nat_diff_split)
+ split: nat_diff_split)
done
--- a/src/ZF/OrderType.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/ZF/OrderType.thy Wed Aug 10 09:33:54 2016 +0200
@@ -517,7 +517,7 @@
done
lemma oadd_lt_cancel2: "[| i++j < i++k; Ord(j) |] ==> j<k"
-apply (simp (asm_lr) add: oadd_eq_if_raw_oadd split add: split_if_asm)
+apply (simp (asm_lr) add: oadd_eq_if_raw_oadd split: split_if_asm)
prefer 2
apply (frule_tac i = i and j = j in oadd_le_self)
apply (simp (asm_lr) add: oadd_def ordify_def lt_Ord not_lt_iff_le [THEN iff_sym])
@@ -530,7 +530,7 @@
by (blast intro!: oadd_lt_mono2 dest!: oadd_lt_cancel2)
lemma oadd_inject: "[| i++j = i++k; Ord(j); Ord(k) |] ==> j=k"
-apply (simp add: oadd_eq_if_raw_oadd split add: split_if_asm)
+apply (simp add: oadd_eq_if_raw_oadd split: split_if_asm)
apply (simp add: raw_oadd_eq_oadd)
apply (rule Ord_linear_lt, auto)
apply (force dest: oadd_lt_mono2 [of concl: i] simp add: lt_not_refl)+
@@ -538,7 +538,7 @@
lemma lt_oadd_disj: "k < i++j ==> k<i | (\<exists>l\<in>j. k = i++l )"
apply (simp add: Ord_in_Ord' [of _ j] oadd_eq_if_raw_oadd
- split add: split_if_asm)
+ split: split_if_asm)
prefer 2
apply (simp add: Ord_in_Ord' [of _ j] lt_def)
apply (simp add: ordertype_pred_unfold well_ord_radd well_ord_Memrel raw_oadd_def)
--- a/src/ZF/UNITY/AllocImpl.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/ZF/UNITY/AllocImpl.thy Wed Aug 10 09:33:54 2016 +0200
@@ -314,7 +314,7 @@
apply (rule LeadsTo_weaken)
apply (rule_tac n = "s0`NbR" in alloc_prog_NbR_LeadsTo_lemma2, safe)
prefer 3 apply assumption
-apply (auto split add: nat_diff_split simp add: greater_than_def not_lt_imp_le not_le_iff_lt)
+apply (auto split: nat_diff_split simp add: greater_than_def not_lt_imp_le not_le_iff_lt)
apply (blast dest: lt_asym)
apply (force dest: add_lt_elim2)
done
@@ -416,7 +416,7 @@
apply (subgoal_tac "x`available_tok =
NbT #+ (tokens(take(x`NbR,x`rel)) #- tokens(x`giv))")
apply (simp add: )
-apply (auto split add: nat_diff_split dest: lt_trans2)
+apply (auto split: nat_diff_split dest: lt_trans2)
done
--- a/src/ZF/UNITY/GenPrefix.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/ZF/UNITY/GenPrefix.thy Wed Aug 10 09:33:54 2016 +0200
@@ -489,7 +489,7 @@
apply (force simp add: le_subset_iff, safe)
apply (subgoal_tac "length (xs) #+ (i #- length (xs)) = i")
apply (subst nth_drop)
-apply (simp_all (no_asm_simp) add: leI split add: nat_diff_split)
+apply (simp_all (no_asm_simp) add: leI split: nat_diff_split)
done
lemma prefix_snoc: