--- a/src/Doc/Isar_Ref/Generic.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy Tue Feb 23 18:04:31 2016 +0100
@@ -1086,9 +1086,9 @@
For technical reasons, there is a distinction between case splitting
in the conclusion and in the premises of a subgoal. The former is
done by @{ML Splitter.split_tac} with rules like @{thm [source]
- split_if} or @{thm [source] option.split}, which do not split the
+ if_split} or @{thm [source] option.split}, which do not split the
subgoal, while the latter is done by @{ML Splitter.split_asm_tac}
- with rules like @{thm [source] split_if_asm} or @{thm [source]
+ with rules like @{thm [source] if_split_asm} or @{thm [source]
option.split_asm}, which split the subgoal. The function @{ML
Splitter.add_split} automatically takes care of which tactic to
call, analyzing the form of the rules given as argument; it is the
--- a/src/Doc/Tutorial/Fun/fun0.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/Doc/Tutorial/Fun/fun0.thy Tue Feb 23 18:04:31 2016 +0100
@@ -137,7 +137,7 @@
different ways.
The most radical solution is to disable the offending theorem
-@{thm[source]split_if},
+@{thm[source]if_split},
as shown in \S\ref{sec:AutoCaseSplits}. However, we do not recommend this
approach: you will often have to invoke the rule explicitly when
@{text "if"} is involved.
--- a/src/Doc/Tutorial/Misc/simp.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/Doc/Tutorial/Misc/simp.thy Tue Feb 23 18:04:31 2016 +0100
@@ -268,11 +268,11 @@
The goal can be split by a special method, \methdx{split}:
*}
-apply(split split_if)
+apply(split if_split)
txt{*\noindent
@{subgoals[display,indent=0]}
-where \tdx{split_if} is a theorem that expresses splitting of
+where \tdx{if_split} is a theorem that expresses splitting of
@{text"if"}s. Because
splitting the @{text"if"}s is usually the right proof strategy, the
simplifier does it automatically. Try \isacommand{apply}@{text"(simp)"}
@@ -316,7 +316,7 @@
(*<*)
lemma "dummy=dummy"
(*>*)
-apply(simp split del: split_if)
+apply(simp split del: if_split)
(*<*)
oops
(*>*)
@@ -334,11 +334,11 @@
The split rules shown above are intended to affect only the subgoal's
conclusion. If you want to split an @{text"if"} or @{text"case"}-expression
-in the assumptions, you have to apply \tdx{split_if_asm} or
+in the assumptions, you have to apply \tdx{if_split_asm} or
$t$@{text".split_asm"}: *}
lemma "if xs = [] then ys \<noteq> [] else ys = [] \<Longrightarrow> xs @ ys \<noteq> []"
-apply(split split_if_asm)
+apply(split if_split_asm)
txt{*\noindent
Unlike splitting the conclusion, this step creates two
--- a/src/Doc/Tutorial/Protocol/Event.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/Doc/Tutorial/Protocol/Event.thy Tue Feb 23 18:04:31 2016 +0100
@@ -383,4 +383,4 @@
(*<*)
end
-(*>*)
\ No newline at end of file
+(*>*)
--- a/src/Doc/Tutorial/Protocol/Message.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy Tue Feb 23 18:04:31 2016 +0100
@@ -483,7 +483,7 @@
by (intro equalityI lemma1 lemma2)
text{*Case analysis: either the message is secure, or it is not! Effective,
-but can cause subgoals to blow up! Use with @{text "split_if"}; apparently
+but can cause subgoals to blow up! Use with @{text "if_split"}; apparently
@{text "split_tac"} does not cope with patterns such as @{term"analz (insert
(Crypt K X) H)"} *}
lemma analz_Crypt_if [simp]:
@@ -918,4 +918,4 @@
end
-(*>*)
\ No newline at end of file
+(*>*)
--- a/src/Doc/Tutorial/Protocol/Public.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/Doc/Tutorial/Protocol/Public.thy Tue Feb 23 18:04:31 2016 +0100
@@ -169,4 +169,4 @@
"for proving possibility theorems"
end
-(*>*)
\ No newline at end of file
+(*>*)
--- a/src/Doc/Tutorial/Recdef/simplification.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/Doc/Tutorial/Recdef/simplification.thy Tue Feb 23 18:04:31 2016 +0100
@@ -40,7 +40,7 @@
different ways.
The most radical solution is to disable the offending theorem
-@{thm[source]split_if},
+@{thm[source]if_split},
as shown in \S\ref{sec:AutoCaseSplits}. However, we do not recommend this
approach: you will often have to invoke the rule explicitly when
@{text "if"} is involved.
--- a/src/Doc/Tutorial/Types/Setup.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/Doc/Tutorial/Types/Setup.thy Tue Feb 23 18:04:31 2016 +0100
@@ -5,4 +5,4 @@
ML_file "../../antiquote_setup.ML"
ML_file "../../more_antiquote.ML"
-end
\ No newline at end of file
+end
--- a/src/HOL/Auth/Guard/Extensions.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy Tue Feb 23 18:04:31 2016 +0100
@@ -39,7 +39,7 @@
declare analz_subset_parts [THEN subsetD, dest]
declare parts_insert2 [simp]
declare analz_cut [dest]
-declare split_if_asm [split]
+declare if_split_asm [split]
declare analz_insertI [intro]
declare Un_Diff [simp]
--- a/src/HOL/Auth/Guard/Guard.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Auth/Guard/Guard.thy Tue Feb 23 18:04:31 2016 +0100
@@ -304,4 +304,4 @@
apply (drule_tac G="G Un (H Int keysfor G)" in Guard_invKey_finite)
by (auto simp: Guard_def intro: analz_sub)
-end
\ No newline at end of file
+end
--- a/src/HOL/Auth/Guard/GuardK.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Auth/Guard/GuardK.thy Tue Feb 23 18:04:31 2016 +0100
@@ -299,4 +299,4 @@
apply (auto simp: GuardK_def intro: analz_sub)
by (drule keyset_in, auto)
-end
\ No newline at end of file
+end
--- a/src/HOL/Auth/Guard/Guard_Shared.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Auth/Guard/Guard_Shared.thy Tue Feb 23 18:04:31 2016 +0100
@@ -198,4 +198,4 @@
with \<open>agt K \<notin> bad\<close> show False by simp
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/Auth/Guard/P1.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Auth/Guard/P1.thy Tue Feb 23 18:04:31 2016 +0100
@@ -634,4 +634,4 @@
apply (blast dest: Crypt_Hash_imp_sign [unfolded sign_def])
done
-end
\ No newline at end of file
+end
--- a/src/HOL/Auth/Guard/P2.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Auth/Guard/P2.thy Tue Feb 23 18:04:31 2016 +0100
@@ -558,4 +558,4 @@
apply (blast dest: Crypt_Hash_imp_sign [unfolded sign_def])
done
-end
\ No newline at end of file
+end
--- a/src/HOL/Auth/Message.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Auth/Message.thy Tue Feb 23 18:04:31 2016 +0100
@@ -468,7 +468,7 @@
by (intro equalityI lemma1 lemma2)
text\<open>Case analysis: either the message is secure, or it is not! Effective,
-but can cause subgoals to blow up! Use with \<open>split_if\<close>; apparently
+but can cause subgoals to blow up! Use with \<open>if_split\<close>; apparently
\<open>split_tac\<close> does not cope with patterns such as @{term"analz (insert
(Crypt K X) H)"}\<close>
lemma analz_Crypt_if [simp]:
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Tue Feb 23 18:04:31 2016 +0100
@@ -1631,7 +1631,7 @@
have "bij_betw F (Pow A) (Func A (UNIV::bool set))"
unfolding bij_betw_def inj_on_def proof (intro ballI impI conjI)
fix A1 A2 assume "A1 \<in> Pow A" "A2 \<in> Pow A" "F A1 = F A2"
- thus "A1 = A2" unfolding F_def Pow_def fun_eq_iff by (auto split: split_if_asm)
+ thus "A1 = A2" unfolding F_def Pow_def fun_eq_iff by (auto split: if_split_asm)
next
show "F ` Pow A = Func A UNIV"
proof safe
--- a/src/HOL/Bali/AxCompl.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Bali/AxCompl.thy Tue Feb 23 18:04:31 2016 +0100
@@ -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: split_if)
+ by (induct s) (simp add: init_lvars_def2 split add: 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: split_if_asm)
+ simp add: nyinitcls_def inited_def split add: if_split_asm)
done
lemma inited_gext': "\<lbrakk>s\<le>|s';inited C (globs s)\<rbrakk> \<Longrightarrow> inited C (globs s')"
@@ -597,7 +597,7 @@
with abrupt_s' have "G\<turnstile>s' \<midarrow>c\<rightarrow> s'" by auto
moreover from abrupt_s' no_cont
have no_absorb: "(abupd (absorb (Cont l)) s')=s'"
- by (cases s') (simp add: absorb_def split: split_if)
+ by (cases s') (simp add: absorb_def split: if_split)
moreover
from no_absorb abrupt_s'
have "G\<turnstile>(abupd (absorb (Cont l)) s') \<midarrow>l\<bullet> While(e) c\<rightarrow> 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: split_if)
+ apply (simp add: init_comp_ty_def split add: if_split)
apply (rule conjI, clarsimp)
apply (rule MGFn_InitD [OF hyp, THEN conseq2])
apply (clarsimp intro: eval.Init)
--- a/src/HOL/Bali/AxExample.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Bali/AxExample.thy Tue Feb 23 18:04:31 2016 +0100
@@ -37,7 +37,7 @@
done
-declare split_if_asm [split del]
+declare if_split_asm [split del]
declare lvar_def [simp]
ML \<open>
@@ -202,7 +202,7 @@
apply (tactic "ax_tac @{context} 2" (* StatRef *))
apply (rule ax_derivs.Done [THEN conseq1])
apply (tactic \<open>inst1_tac @{context} "Q" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" []\<close>)
-apply (clarsimp split del: split_if)
+apply (clarsimp split del: if_split)
apply (frule atleast_free_weaken [THEN atleast_free_weaken])
apply (drule initedD)
apply (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def)
--- a/src/HOL/Bali/AxSem.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Bali/AxSem.thy Tue Feb 23 18:04:31 2016 +0100
@@ -462,7 +462,7 @@
declare split_paired_All [simp del] split_paired_Ex [simp del]
-declare split_if [split del] split_if_asm [split del]
+declare if_split [split del] if_split_asm [split del]
option.split [split del] option.split_asm [split del]
setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
--- a/src/HOL/Bali/AxSound.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Bali/AxSound.thy Tue Feb 23 18:04:31 2016 +0100
@@ -1356,12 +1356,12 @@
proof -
from s2_no_return s3
have "abrupt s3 \<noteq> Some (Jump Ret)"
- by (cases s2) (auto simp add: init_lvars_def2 split: split_if_asm)
+ by (cases s2) (auto simp add: init_lvars_def2 split: if_split_asm)
moreover
obtain abr2 str2 where s2: "s2=(abr2,str2)"
by (cases s2)
from s3 s2 conf_s2 have "(abrupt s3,str2)\<Colon>\<preceq>(G, L)"
- by (auto simp add: init_lvars_def2 split: split_if_asm)
+ by (auto simp add: init_lvars_def2 split: if_split_asm)
ultimately show ?thesis
using s3 s2 eq_s3'_s3
apply (simp add: init_lvars_def2)
@@ -1661,7 +1661,7 @@
by (rule jumpNestingOk_evalE) (auto intro: jmpOk simp add: s1_no_jmp)
moreover note s3
ultimately show ?thesis
- by (force split: split_if)
+ by (force split: if_split)
qed
with R v s4
have "R \<lfloor>v\<rfloor>\<^sub>e s4 Z"
@@ -1923,7 +1923,7 @@
from wt obtain
wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
wt_then_else: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
- by cases (simp split: split_if)
+ by cases (simp split: if_split)
from da obtain E S where
da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E" and
da_then_else:
@@ -2587,7 +2587,7 @@
from this wt_super wf
have s1_no_ret: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
by - (rule eval_statement_no_jump
- [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>"], auto split: split_if)
+ [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>"], auto split: if_split)
with conf_s1
show ?thesis
by (cases s1) (auto intro: conforms_set_locals)
--- a/src/HOL/Bali/Basis.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Bali/Basis.thy Tue Feb 23 18:04:31 2016 +0100
@@ -11,7 +11,7 @@
ML \<open>fun strip_tac ctxt i = REPEAT (resolve_tac ctxt [impI, allI] i)\<close>
-declare split_if_asm [split] option.split [split] option.split_asm [split]
+declare if_split_asm [split] option.split [split] option.split_asm [split]
setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
declare if_weak_cong [cong del] option.case_cong_weak [cong del]
declare length_Suc_conv [iff]
--- a/src/HOL/Bali/Eval.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Bali/Eval.thy Tue Feb 23 18:04:31 2016 +0100
@@ -753,7 +753,7 @@
\<close>
-declare split_if [split del] split_if_asm [split del]
+declare if_split [split del] if_split_asm [split del]
option.split [split del] option.split_asm [split del]
inductive_cases halloc_elim_cases:
"G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
@@ -819,7 +819,7 @@
declare not_None_eq [simp] (* IntDef.Zero_def [simp] *)
declare split_paired_All [simp] split_paired_Ex [simp]
declaration \<open>K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac)))\<close>
-declare split_if [split] split_if_asm [split]
+declare if_split [split] if_split_asm [split]
option.split [split] option.split_asm [split]
lemma eval_Inj_elim:
@@ -1062,7 +1062,7 @@
lemma init_retains_locals [rule_format (no_asm)]: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow>
(\<forall>C. t=In1r (Init C) \<longrightarrow> locals (store s) = locals (store s'))"
apply (erule eval.induct)
-apply (simp (no_asm_use) split del: split_if_asm option.split_asm)+
+apply (simp (no_asm_use) split del: if_split_asm option.split_asm)+
apply auto
done
@@ -1128,7 +1128,7 @@
lemma unique_halloc [rule_format (no_asm)]:
"G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>halloc oi\<succ>a' \<rightarrow> s'' \<longrightarrow> a' = a \<and> s'' = s'"
apply (erule halloc.induct)
-apply (auto elim!: halloc_elim_cases split del: split_if split_if_asm)
+apply (auto elim!: halloc_elim_cases split del: if_split if_split_asm)
apply (drule trans [THEN sym], erule sym)
defer
apply (drule trans [THEN sym], erule sym)
@@ -1146,7 +1146,7 @@
"G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'' \<longrightarrow> s'' = s'"
apply (erule sxalloc.induct)
apply (auto dest: unique_halloc elim!: sxalloc_elim_cases
- split del: split_if split_if_asm)
+ split del: if_split if_split_asm)
done
lemma single_valued_sxalloc: "single_valued {(s,s'). G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'}"
@@ -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: split_if_asm)
+apply (simp (no_asm_use) only: split add: 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: split_if_asm, blast)
+apply (simp (no_asm_use) only: split add: if_split_asm, blast)
(* 36 subgoals *)
apply (blast dest: unique_sxalloc unique_halloc split_pairD)+
done
--- a/src/HOL/Bali/Evaln.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Bali/Evaln.thy Tue Feb 23 18:04:31 2016 +0100
@@ -193,7 +193,7 @@
if_bool_eq_conj
-declare split_if [split del] split_if_asm [split del]
+declare if_split [split del] if_split_asm [split del]
option.split [split del] option.split_asm [split del]
not_None_eq [simp del]
split_paired_All [simp del] split_paired_Ex [simp del]
@@ -234,7 +234,7 @@
"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> (v, s')"
"G\<turnstile>Norm s \<midarrow>In1r (Init C) \<succ>\<midarrow>n\<rightarrow> (x, s')"
-declare split_if [split] split_if_asm [split]
+declare if_split [split] if_split_asm [split]
option.split [split] option.split_asm [split]
not_None_eq [simp]
split_paired_All [simp] split_paired_Ex [simp]
@@ -453,7 +453,7 @@
REPEAT o smp_tac @{context} 1,
resolve_tac @{context} @{thms evaln.intros} THEN_ALL_NEW TRY o assume_tac @{context}])\<close>)
(* 3 subgoals *)
-apply (auto split del: split_if)
+apply (auto split del: if_split)
done
lemmas evaln_nonstrict_Suc = evaln_nonstrict [OF _ le_refl [THEN le_SucI]]
--- a/src/HOL/Bali/Example.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Bali/Example.thy Tue Feb 23 18:04:31 2016 +0100
@@ -1347,7 +1347,7 @@
apply (rule eval_Is (* Acc *))
apply (rule eval_Is (* LVar *))
apply (simp)
-apply (simp split del: split_if)
+apply (simp split del: if_split)
apply (simp add: check_field_access_def Let_def)
apply (rule eval_Is (* XcptE *))
apply (simp)
@@ -1362,7 +1362,7 @@
apply (erule alloc_one [THEN conjunct1])
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
-apply (simp add: gupd_def lupd_def obj_ty_def split del: split_if)
+apply (simp add: gupd_def lupd_def obj_ty_def split del: if_split)
apply (drule alloc_one [THEN conjunct1])
apply (simp (no_asm_simp))
apply (erule_tac V = "atleast_free _ two" in thin_rl)
--- a/src/HOL/Bali/State.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Bali/State.thy Tue Feb 23 18:04:31 2016 +0100
@@ -501,7 +501,7 @@
"P (abrupt_if c x' x) =
((c \<and> x = None \<longrightarrow> P x') \<and> (\<not> (c \<and> x = None) \<longrightarrow> P x))"
apply (unfold abrupt_if_def)
-apply (split split_if)
+apply (split if_split)
apply auto
done
@@ -756,25 +756,25 @@
"error_free s \<Longrightarrow> error_free (abupd (absorb j) s)"
by (cases s)
(auto simp add: error_free_def absorb_def
- split: split_if_asm)
+ split: if_split_asm)
lemma error_free_absorb [simp,intro]:
"error_free (a,s) \<Longrightarrow> error_free (absorb j a, s)"
by (auto simp add: error_free_def absorb_def
- split: split_if_asm)
+ split: if_split_asm)
lemma error_free_abrupt_if [simp,intro]:
"\<lbrakk>error_free s; \<not> (\<exists> err. x=Error err)\<rbrakk>
\<Longrightarrow> error_free (abupd (abrupt_if p (Some x)) s)"
by (cases s)
(auto simp add: abrupt_if_def
- split: split_if)
+ split: if_split)
lemma error_free_abrupt_if1 [simp,intro]:
"\<lbrakk>error_free (a,s); \<not> (\<exists> err. x=Error err)\<rbrakk>
\<Longrightarrow> error_free (abrupt_if p (Some x) a, s)"
by (auto simp add: abrupt_if_def
- split: split_if)
+ split: if_split)
lemma error_free_abrupt_if_Xcpt [simp,intro]:
"error_free s
--- a/src/HOL/Bali/Term.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Bali/Term.thy Tue Feb 23 18:04:31 2016 +0100
@@ -482,4 +482,4 @@
"\<lbrakk>binop\<noteq>CondAnd; binop\<noteq>CondOr\<rbrakk> \<Longrightarrow> need_second_arg binop b"
by (cases binop)
(simp_all add: need_second_arg_def)
-end
\ No newline at end of file
+end
--- a/src/HOL/Bali/Trans.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Bali/Trans.thy Tue Feb 23 18:04:31 2016 +0100
@@ -370,4 +370,4 @@
*)
-end
\ No newline at end of file
+end
--- a/src/HOL/Bali/TypeSafe.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Bali/TypeSafe.thy Tue Feb 23 18:04:31 2016 +0100
@@ -60,7 +60,7 @@
apply (cases s)
apply (auto simp add: check_field_access_def Let_def error_free_def
abrupt_if_def
- split: split_if_asm)
+ split: if_split_asm)
done
lemma error_free_check_method_access_eq:
@@ -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: split_if_asm split add: sum3.split)
+ split del: if_split_asm split add: sum3.split)
(* 6 subgoals *)
apply force+
done
@@ -232,9 +232,9 @@
done
lemma init_yields_initd: "G\<turnstile>Norm s1 \<midarrow>Init C\<rightarrow> s2 \<Longrightarrow> initd C s2"
-apply (erule eval_cases , auto split del: split_if_asm)
+apply (erule eval_cases , auto split del: if_split_asm)
apply (case_tac "inited C (globs s1)")
-apply (clarsimp split del: split_if_asm)+
+apply (clarsimp split del: if_split_asm)+
apply (drule eval_gext')+
apply (drule init_class_obj_inited)
apply (erule inited_gext)
@@ -724,7 +724,7 @@
qed
declare split_paired_All [simp del] split_paired_Ex [simp del]
-declare split_if [split del] split_if_asm [split del]
+declare if_split [split del] if_split_asm [split del]
option.split [split del] option.split_asm [split del]
setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
@@ -753,7 +753,7 @@
apply (blast intro: FVar_lemma2)
done
declare split_paired_All [simp] split_paired_Ex [simp]
-declare split_if [split] split_if_asm [split]
+declare if_split [split] if_split_asm [split]
option.split [split] option.split_asm [split]
setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\<close>
setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
@@ -869,7 +869,7 @@
by (auto simp add: abrupt_if_def)
declare split_paired_All [simp del] split_paired_Ex [simp del]
-declare split_if [split del] split_if_asm [split del]
+declare if_split [split del] if_split_asm [split del]
option.split [split del] option.split_asm [split del]
setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
@@ -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: split_if)
+apply (simp (no_asm_simp) split add: if_split)
apply (drule (4) DynT_conf)
apply clarsimp
(* apply intro *)
@@ -922,7 +922,7 @@
apply (simp add: np_no_jump)
done
declare split_paired_All [simp] split_paired_Ex [simp]
-declare split_if [split] split_if_asm [split]
+declare if_split [split] if_split_asm [split]
option.split [split] option.split_asm [split]
setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\<close>
setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
--- a/src/HOL/Bali/WellForm.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Bali/WellForm.thy Tue Feb 23 18:04:31 2016 +0100
@@ -2410,7 +2410,7 @@
| Inr Ts \<Rightarrow> Ball (set Ts) (is_type (prg E)))"
apply (unfold empty_dt_def)
apply (erule wt.induct)
-apply (auto split del: split_if_asm simp del: snd_conv
+apply (auto split del: if_split_asm simp del: snd_conv
simp add: is_acc_class_def is_acc_type_def)
apply (erule typeof_empty_is_type)
apply (frule (1) wf_prog_cdecl [THEN wf_cdecl_supD],
--- a/src/HOL/Bali/WellType.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Bali/WellType.thy Tue Feb 23 18:04:31 2016 +0100
@@ -456,7 +456,7 @@
ty_exprs_syntax ("_|-_:#_" [51,51,51] 50)
declare not_None_eq [simp del]
-declare split_if [split del] split_if_asm [split del]
+declare if_split [split del] if_split_asm [split del]
declare split_paired_All [simp del] split_paired_Ex [simp del]
setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
@@ -492,7 +492,7 @@
"E,dt\<Turnstile>In1r (c1 Finally c2) \<Colon>x"
"E,dt\<Turnstile>In1r (Init C) \<Colon>x"
declare not_None_eq [simp]
-declare split_if [split] split_if_asm [split]
+declare if_split [split] if_split_asm [split]
declare split_paired_All [simp] split_paired_Ex [simp]
setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
@@ -655,7 +655,7 @@
G = prg E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T = T')"
apply (cases "E", erule wt.induct)
apply (safe del: disjE)
-apply (simp_all (no_asm_use) split del: split_if_asm)
+apply (simp_all (no_asm_use) split del: if_split_asm)
apply (safe del: disjE)
(* 17 subgoals *)
apply (tactic \<open>ALLGOALS (fn i =>
@@ -666,7 +666,7 @@
else Rule_Insts.thin_tac @{context} "All P" [(@{binding P}, NONE, NoSyn)] i)\<close>)
(*apply (safe del: disjE elim!: wt_elim_cases)*)
apply (tactic \<open>ALLGOALS (eresolve_tac @{context} @{thms wt_elim_cases})\<close>)
-apply (simp_all (no_asm_use) split del: split_if_asm)
+apply (simp_all (no_asm_use) split del: if_split_asm)
apply (erule_tac [12] V = "All P" for P in thin_rl) (* Call *)
apply (blast del: equalityCE dest: sym [THEN trans])+
done
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Tue Feb 23 18:04:31 2016 +0100
@@ -226,7 +226,7 @@
def f \<equiv> "\<lambda>y a. if y = x \<and> a \<in> A then x else undefined"
have "Func A {x} \<subseteq> f ` {x}" unfolding f_def Func_def by (force simp: fun_eq_iff)
hence "bij_betw f {x} (Func A {x})" unfolding bij_betw_def inj_on_def f_def Func_def
- by (auto split: split_if_asm)
+ by (auto split: if_split_asm)
thus "|{x}| =o |Func A {x}|" using card_of_ordIso by blast
qed
@@ -239,7 +239,7 @@
proof (rule ordIso_symmetric)
def f \<equiv> "\<lambda>(x::'a,y) b. if A = {} then undefined else if b then x else y"
have "Func (UNIV :: bool set) A \<subseteq> f ` (A \<times> A)" unfolding f_def Func_def
- by (auto simp: image_iff fun_eq_iff split: option.splits split_if_asm) blast
+ by (auto simp: image_iff fun_eq_iff split: option.splits if_split_asm) blast
hence "bij_betw f (A \<times> A) (Func (UNIV :: bool set) A)"
unfolding bij_betw_def inj_on_def f_def Func_def by (auto simp: fun_eq_iff)
thus "|A \<times> A| =o |Func (UNIV :: bool set) A|" using card_of_ordIso by blast
--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy Tue Feb 23 18:04:31 2016 +0100
@@ -1064,7 +1064,7 @@
lemma FinFunc_singleton: "FinFunc {(z,z)} s = {\<lambda>x. if x \<in> Field s then z else undefined}"
unfolding FinFunc_def Func_def fin_support_def support_def
- by (auto simp: fun_eq_iff split: split_if_asm intro!: finite_subset[of _ "{}"])
+ by (auto simp: fun_eq_iff split: if_split_asm intro!: finite_subset[of _ "{}"])
lemma oone_ordIso_oexp:
assumes "r =o oone" and s: "Well_order s"
@@ -1301,7 +1301,7 @@
if z \<in> Field t then r.zero else undefined"
from *(4) x(2) the_inv_into_f_eq[OF *(1)] have FLR: "F ` Field ?L \<subseteq> Field ?R"
unfolding rt.Field_oexp rs.Field_oexp FinFunc_def Func_def fin_support_def support_def F_def
- by (fastforce split: option.splits split_if_asm elim!: finite_surj[of _ _ f])
+ by (fastforce split: option.splits if_split_asm elim!: finite_surj[of _ _ f])
have "inj_on F (Field ?L)" unfolding rs.Field_oexp inj_on_def fun_eq_iff
proof safe
fix g h x assume "g \<in> FinFunc r s" "h \<in> FinFunc r s" "\<forall>y. F g y = F h y"
--- a/src/HOL/Complete_Lattices.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Complete_Lattices.thy Tue Feb 23 18:04:31 2016 +0100
@@ -1247,7 +1247,7 @@
by blast
lemma Un_eq_UN: "A \<union> B = (\<Union>b. if b then A else B)"
- by safe (auto simp add: split_if_mem2)
+ by safe (auto simp add: if_split_mem2)
lemma UN_bool_eq: "(\<Union>b. A b) = (A True \<union> A False)"
by (fact SUP_UNIV_bool_expand)
--- a/src/HOL/Data_Structures/AA_Set.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Data_Structures/AA_Set.thy Tue Feb 23 18:04:31 2016 +0100
@@ -135,4 +135,4 @@
case 4 thus ?case by(simp add: inorder_delete)
qed auto
-end
\ No newline at end of file
+end
--- a/src/HOL/Data_Structures/Isin2.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Data_Structures/Isin2.thy Tue Feb 23 18:04:31 2016 +0100
@@ -23,4 +23,4 @@
lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
by (induction t) (auto simp: elems_simps2)
-end
\ No newline at end of file
+end
--- a/src/HOL/Data_Structures/Lookup2.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Data_Structures/Lookup2.thy Tue Feb 23 18:04:31 2016 +0100
@@ -18,4 +18,4 @@
"sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
by(induction t) (auto simp: map_of_simps split: option.split)
-end
\ No newline at end of file
+end
--- a/src/HOL/Data_Structures/Tree2.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Data_Structures/Tree2.thy Tue Feb 23 18:04:31 2016 +0100
@@ -14,4 +14,4 @@
"height Leaf = 0" |
"height (Node _ l a r) = max (height l) (height r) + 1"
-end
\ No newline at end of file
+end
--- a/src/HOL/Datatype_Examples/Derivation_Trees/Prelim.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Datatype_Examples/Derivation_Trees/Prelim.thy Tue Feb 23 18:04:31 2016 +0100
@@ -61,4 +61,4 @@
shows "A = B"
apply safe using assms apply(case_tac x, auto) by(case_tac x, auto)
-end
\ No newline at end of file
+end
--- a/src/HOL/Decision_Procs/Approximation.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Tue Feb 23 18:04:31 2016 +0100
@@ -182,7 +182,7 @@
"(l1, u1) = float_power_bnds prec n l u \<Longrightarrow> x \<in> {l .. u} \<Longrightarrow> (x::real) ^ n \<in> {l1..u1}"
by (auto
simp: float_power_bnds_def max_def real_power_up_fl real_power_down_fl minus_le_iff
- split: split_if_asm
+ split: if_split_asm
intro!: power_up_le power_down_le le_minus_power_downI
intro: power_mono_odd power_mono power_mono_even zero_le_even_power)
@@ -2771,14 +2771,14 @@
del: lb_ln.simps ub_ln.simps)
next
assume "l1 \<le> 0" "\<not>(l1 = 0 \<and> (u1 = 0 \<or> l2 \<ge> 1))"
- with lu show ?thesis by (simp add: bnds_powr_def split: split_if_asm)
+ with lu show ?thesis by (simp add: bnds_powr_def split: if_split_asm)
next
assume l1: "l1 > 0"
obtain lm um where lmum:
"(lm, um) = bnds_mult prec (the (lb_ln prec l1)) (the (ub_ln prec u1)) l2 u2"
by (cases "bnds_mult prec (the (lb_ln prec l1)) (the (ub_ln prec u1)) l2 u2") simp
with l1 have "(l, u) = map_bnds lb_exp ub_exp prec (lm, um)"
- using lu by (simp add: bnds_powr_def del: lb_ln.simps ub_ln.simps split: split_if_asm)
+ using lu by (simp add: bnds_powr_def del: lb_ln.simps ub_ln.simps split: if_split_asm)
hence "exp (ln x * y) \<in> {real_of_float l..real_of_float u}"
proof (rule map_bnds[OF _ mono_exp_real], goal_cases)
case 1
@@ -4229,7 +4229,7 @@
with f_def a b assms
have "approx_tse_form' prec t (Add rt (Minus x)) s l u' (\<lambda> l u. 0 \<le> l)"
and "approx_tse_form' prec t (Add x (Minus lf)) s l u' (\<lambda> l u. 0 \<le> l)"
- unfolding approx_tse_form_def lazy_conj by (auto split: split_if_asm)
+ unfolding approx_tse_form_def lazy_conj by (auto split: if_split_asm)
from approx_tse_form'_le[OF this(1) bnd] approx_tse_form'_le[OF this(2) bnd]
show ?case using AtLeastAtMost by auto
qed (auto simp: f_def approx_tse_form_def elim!: case_optionE)
--- a/src/HOL/Decision_Procs/Polynomial_List.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy Tue Feb 23 18:04:31 2016 +0100
@@ -908,16 +908,16 @@
unfolding pnormal_def by simp
lemma (in semiring_0) pnormal_tail: "p \<noteq> [] \<Longrightarrow> pnormal (c # p) \<Longrightarrow> pnormal p"
- unfolding pnormal_def by (auto split: split_if_asm)
+ unfolding pnormal_def by (auto split: if_split_asm)
lemma (in semiring_0) pnormal_last_nonzero: "pnormal p \<Longrightarrow> last p \<noteq> 0"
- by (induct p) (simp_all add: pnormal_def split: split_if_asm)
+ by (induct p) (simp_all add: pnormal_def split: if_split_asm)
lemma (in semiring_0) pnormal_length: "pnormal p \<Longrightarrow> 0 < length p"
unfolding pnormal_def length_greater_0_conv by blast
lemma (in semiring_0) pnormal_last_length: "0 < length p \<Longrightarrow> last p \<noteq> 0 \<Longrightarrow> pnormal p"
- by (induct p) (auto simp: pnormal_def split: split_if_asm)
+ by (induct p) (auto simp: pnormal_def split: if_split_asm)
lemma (in semiring_0) pnormal_id: "pnormal p \<longleftrightarrow> 0 < length p \<and> last p \<noteq> 0"
using pnormal_last_length pnormal_length pnormal_last_nonzero by blast
@@ -1010,7 +1010,7 @@
qed
lemma (in semiring_0) pnormalize_eq: "last p \<noteq> 0 \<Longrightarrow> pnormalize p = p"
- by (induct p) (auto split: split_if_asm)
+ by (induct p) (auto split: if_split_asm)
lemma (in semiring_0) last_pnormalize: "pnormalize p \<noteq> [] \<Longrightarrow> last (pnormalize p) \<noteq> 0"
by (induct p) auto
--- a/src/HOL/Decision_Procs/Rat_Pair.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Decision_Procs/Rat_Pair.thy Tue Feb 23 18:04:31 2016 +0100
@@ -188,7 +188,7 @@
proof cases
case 1
then show ?thesis
- using na nb H by (simp add: x y INum_def split_def isnormNum_def split: split_if_asm)
+ using na nb H by (simp add: x y INum_def split_def isnormNum_def split: if_split_asm)
next
case 2
with na nb have pos: "b > 0" "b' > 0"
@@ -599,7 +599,7 @@
show ?thesis using nx ny
apply (simp only: isnormNum_unique[where ?'a = 'a, OF Nmul_normN[OF nx ny] n0, symmetric]
Nmul[where ?'a = 'a])
- apply (simp add: x y INum_def split_def isnormNum_def split: split_if_asm)
+ apply (simp add: x y INum_def split_def isnormNum_def split: if_split_asm)
done
qed
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Feb 23 18:04:31 2016 +0100
@@ -2127,4 +2127,4 @@
lemma swap_isweanpoly: "isweaknpoly p \<Longrightarrow> isweaknpoly (swap n m p)"
by (induct p) auto
-end
\ No newline at end of file
+end
--- a/src/HOL/Decision_Procs/approximation.ML Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Decision_Procs/approximation.ML Tue Feb 23 18:04:31 2016 +0100
@@ -261,4 +261,4 @@
THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
THEN gen_eval_tac (approximation_conv ctxt) ctxt i
-end;
\ No newline at end of file
+end;
--- a/src/HOL/Decision_Procs/langford.ML Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Decision_Procs/langford.ML Tue Feb 23 18:04:31 2016 +0100
@@ -260,4 +260,4 @@
THEN Object_Logic.full_atomize_tac ctxt i
THEN CONVERSION (Object_Logic.judgment_conv ctxt (raw_dlo_conv ctxt ss instance)) i
THEN (simp_tac (put_simpset ss ctxt) i)));
-end;
\ No newline at end of file
+end;
--- a/src/HOL/Deriv.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Deriv.thy Tue Feb 23 18:04:31 2016 +0100
@@ -962,7 +962,7 @@
fix h::real
assume "0 < h" "h < s"
with all [of h] show "f x < f (x+h)"
- proof (simp add: abs_if pos_less_divide_eq split add: split_if_asm)
+ proof (simp add: abs_if pos_less_divide_eq split add: 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
@@ -991,7 +991,7 @@
fix h::real
assume "0 < h" "h < s"
with all [of "-h"] show "f x < f (x-h)"
- proof (simp add: abs_if pos_less_divide_eq split add: split_if_asm)
+ proof (simp add: abs_if pos_less_divide_eq split add: 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/Divides.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Divides.thy Tue Feb 23 18:04:31 2016 +0100
@@ -1002,7 +1002,7 @@
assume "m \<noteq> 0"
hence "\<And>a b. divmod_nat_rel n q (a, b) \<Longrightarrow> divmod_nat_rel (m * n) (m * q) (a, m * b)"
unfolding divmod_nat_rel_def
- by (auto split: split_if_asm, simp_all add: algebra_simps)
+ by (auto split: if_split_asm, simp_all add: algebra_simps)
moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" .
ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" .
thus "(m * n) div (m * q) = n div q" by (rule div_nat_unique)
@@ -1660,7 +1660,7 @@
lemma unique_quotient:
"divmod_int_rel a b (q, r) \<Longrightarrow> divmod_int_rel a b (q', r') \<Longrightarrow> q = q'"
-apply (simp add: divmod_int_rel_def linorder_neq_iff split: split_if_asm)
+apply (simp add: divmod_int_rel_def linorder_neq_iff split: if_split_asm)
apply (blast intro: order_antisym
dest: order_eq_refl [THEN unique_quotient_lemma]
order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
@@ -2072,7 +2072,7 @@
==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
by (auto simp add: mult.assoc divmod_int_rel_def linorder_neq_iff
zero_less_mult_iff distrib_left [symmetric]
- zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)
+ zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: if_split_asm)
lemma zdiv_zmult2_eq:
fixes a b c :: int
--- a/src/HOL/Enum.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Enum.thy Tue Feb 23 18:04:31 2016 +0100
@@ -795,13 +795,13 @@
proof(cases a "\<Sqinter>B" rule: finite_3.exhaust[case_product finite_3.exhaust])
case a\<^sub>2_a\<^sub>3
then have "\<And>x. x \<in> B \<Longrightarrow> x = a\<^sub>3"
- by(case_tac x)(auto simp add: Inf_finite_3_def split: split_if_asm)
+ by(case_tac x)(auto simp add: Inf_finite_3_def split: if_split_asm)
then show ?thesis using a\<^sub>2_a\<^sub>3
- by(auto simp add: Inf_finite_3_def max_def less_eq_finite_3_def less_finite_3_def split: split_if_asm)
- qed (auto simp add: Inf_finite_3_def max_def less_finite_3_def less_eq_finite_3_def split: split_if_asm)
+ by(auto simp add: Inf_finite_3_def max_def less_eq_finite_3_def less_finite_3_def split: if_split_asm)
+ qed (auto simp add: Inf_finite_3_def max_def less_finite_3_def less_eq_finite_3_def split: if_split_asm)
show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
by (cases a "\<Squnion>B" rule: finite_3.exhaust[case_product finite_3.exhaust])
- (auto simp add: Sup_finite_3_def min_def less_finite_3_def less_eq_finite_3_def split: split_if_asm)
+ (auto simp add: Sup_finite_3_def min_def less_finite_3_def less_eq_finite_3_def split: if_split_asm)
qed
instance finite_3 :: complete_linorder ..
@@ -920,10 +920,10 @@
fix a :: finite_4 and B
show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
by(cases a "\<Sqinter>B" rule: finite_4.exhaust[case_product finite_4.exhaust])
- (auto simp add: sup_finite_4_def Inf_finite_4_def split: finite_4.splits split_if_asm)
+ (auto simp add: sup_finite_4_def Inf_finite_4_def split: finite_4.splits if_split_asm)
show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
by(cases a "\<Squnion>B" rule: finite_4.exhaust[case_product finite_4.exhaust])
- (auto simp add: inf_finite_4_def Sup_finite_4_def split: finite_4.splits split_if_asm)
+ (auto simp add: inf_finite_4_def Sup_finite_4_def split: finite_4.splits if_split_asm)
qed
instantiation finite_4 :: complete_boolean_algebra begin
@@ -1022,13 +1022,13 @@
fix A and z :: finite_5
assume *: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
show "z \<le> \<Sqinter>A"
- by(auto simp add: less_eq_finite_5_def Inf_finite_5_def split: finite_5.splits split_if_asm dest!: *)
+ by(auto simp add: less_eq_finite_5_def Inf_finite_5_def split: finite_5.splits if_split_asm dest!: *)
next
fix A and z :: finite_5
assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
show "\<Squnion>A \<le> z"
- by(auto simp add: less_eq_finite_5_def Sup_finite_5_def split: finite_5.splits split_if_asm dest!: *)
-qed(auto simp add: less_eq_finite_5_def less_finite_5_def inf_finite_5_def sup_finite_5_def Inf_finite_5_def Sup_finite_5_def split: finite_5.splits split_if_asm)
+ by(auto simp add: less_eq_finite_5_def Sup_finite_5_def split: finite_5.splits if_split_asm dest!: *)
+qed(auto simp add: less_eq_finite_5_def less_finite_5_def inf_finite_5_def sup_finite_5_def Inf_finite_5_def Sup_finite_5_def split: finite_5.splits if_split_asm)
end
--- a/src/HOL/Finite_Set.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Finite_Set.thy Tue Feb 23 18:04:31 2016 +0100
@@ -1312,7 +1312,7 @@
apply (subgoal_tac "finite A & A - {x} <= 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: split_if_asm)
+apply (simp add: card_Diff_singleton_if split add: if_split_asm)
apply (case_tac "card A", auto)
done
--- a/src/HOL/Fun.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Fun.thy Tue Feb 23 18:04:31 2016 +0100
@@ -667,7 +667,7 @@
by auto
lemma fun_upd_eqD: "f(x := y) = g(x := z) \<Longrightarrow> y = z"
-by(simp add: fun_eq_iff split: split_if_asm)
+by(simp add: fun_eq_iff split: if_split_asm)
subsection \<open>\<open>override_on\<close>\<close>
--- a/src/HOL/HOL.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/HOL.thy Tue Feb 23 18:04:31 2016 +0100
@@ -988,7 +988,7 @@
lemma cases_simp: "((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q)) = Q"
- \<comment> \<open>Avoids duplication of subgoals after \<open>split_if\<close>, when the true and false\<close>
+ \<comment> \<open>Avoids duplication of subgoals after \<open>if_split\<close>, when the true and false\<close>
\<comment> \<open>cases boil down to the same thing.\<close>
by blast
@@ -1036,30 +1036,30 @@
lemma if_not_P: "\<not> P \<Longrightarrow> (if P then x else y) = y"
by (unfold If_def) blast
-lemma split_if: "P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))"
+lemma if_split: "P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))"
apply (rule case_split [of Q])
apply (simplesubst if_P)
prefer 3 apply (simplesubst if_not_P, blast+)
done
-lemma split_if_asm: "P (if Q then x else y) = (\<not> ((Q \<and> \<not> P x) \<or> (\<not> Q \<and> \<not> P y)))"
-by (simplesubst split_if, blast)
+lemma if_split_asm: "P (if Q then x else y) = (\<not> ((Q \<and> \<not> P x) \<or> (\<not> Q \<and> \<not> P y)))"
+by (simplesubst if_split, blast)
-lemmas if_splits [no_atp] = split_if split_if_asm
+lemmas if_splits [no_atp] = if_split if_split_asm
lemma if_cancel: "(if c then x else x) = x"
-by (simplesubst split_if, blast)
+by (simplesubst if_split, blast)
lemma if_eq_cancel: "(if x = y then y else x) = x"
-by (simplesubst split_if, blast)
+by (simplesubst if_split, blast)
lemma if_bool_eq_conj: "(if P then Q else R) = ((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R))"
\<comment> \<open>This form is useful for expanding \<open>if\<close>s on the RIGHT of the \<open>\<Longrightarrow>\<close> symbol.\<close>
- by (rule split_if)
+ by (rule if_split)
lemma if_bool_eq_disj: "(if P then Q else R) = ((P \<and> Q) \<or> (\<not> P \<and> R))"
\<comment> \<open>And this form is useful for expanding \<open>if\<close>s on the LEFT.\<close>
- by (simplesubst split_if) blast
+ by (simplesubst if_split) blast
lemma Eq_TrueI: "P \<Longrightarrow> P \<equiv> True" by (unfold atomize_eq) iprover
lemma Eq_FalseI: "\<not> P \<Longrightarrow> P \<equiv> False" by (unfold atomize_eq) iprover
@@ -1303,7 +1303,7 @@
simp_thms
lemmas [cong] = imp_cong simp_implies_cong
-lemmas [split] = split_if
+lemmas [split] = if_split
ML \<open>val HOL_ss = simpset_of @{context}\<close>
--- a/src/HOL/HOLCF/Bifinite.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/HOLCF/Bifinite.thy Tue Feb 23 18:04:31 2016 +0100
@@ -142,7 +142,7 @@
let ?S = "insert (\<bottom>::'a discr u) ((\<lambda>x. up\<cdot>x) ` undiscr -` to_nat -` {..<i})"
show "{x::'a discr u. discr_approx i\<cdot>x = x} \<subseteq> ?S"
unfolding discr_approx_def
- by (rule subsetI, case_tac x, simp, simp split: split_if_asm)
+ by (rule subsetI, case_tac x, simp, simp split: if_split_asm)
show "finite ?S"
by (simp add: finite_vimageI)
qed
--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy Tue Feb 23 18:04:31 2016 +0100
@@ -94,7 +94,7 @@
"if x=hd(reverse(reduce(l))) & reduce(l)~=[] then
reduce(l@[x])=reduce(l) else
reduce(l@[x])=reduce(l)@[x]"
-apply (simplesubst split_if)
+apply (simplesubst if_split)
apply (rule conjI)
txt \<open>\<open>-->\<close>\<close>
apply (induct_tac "l")
@@ -115,7 +115,7 @@
apply (case_tac "list=[]")
apply (cut_tac [2] l = "list" in cons_not_nil)
apply simp
-apply (auto simp del: reduce_Cons simp add: last_ind_on_first l_iff_red_nil split: split_if)
+apply (auto simp del: reduce_Cons simp add: last_ind_on_first l_iff_red_nil split: if_split)
apply simp
done
@@ -134,7 +134,7 @@
subsection \<open>Channel Abstraction\<close>
-declare split_if [split del]
+declare if_split [split del]
lemma channel_abstraction: "is_weak_ref_map reduce ch_ioa ch_fin_ioa"
apply (simp (no_asm) add: is_weak_ref_map_def)
@@ -161,7 +161,7 @@
apply (erule reduce_tl)
done
-declare split_if [split]
+declare if_split [split]
lemma sender_abstraction: "is_weak_ref_map reduce srch_ioa srch_fin_ioa"
apply (tactic \<open>
--- a/src/HOL/HOLCF/IOA/Deadlock.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Deadlock.thy Tue Feb 23 18:04:31 2016 +0100
@@ -64,7 +64,7 @@
and "compatible A B"
and "input_enabled B"
shows "(sch @@ a \<leadsto> nil) \<in> schedules (A \<parallel> B)"
- supply split_if [split del]
+ supply if_split [split del]
apply (insert assms)
apply (simp add: compositionality_sch locals_def)
apply (rule conjI)
--- a/src/HOL/HOLCF/IOA/NTP/Correctness.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Correctness.thy Tue Feb 23 18:04:31 2016 +0100
@@ -61,7 +61,7 @@
lemma ntp_correct:
"is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig)) spec_ioa"
apply (unfold Spec.ioa_def is_weak_ref_map_def)
-apply (simp (no_asm) cong del: if_weak_cong split del: split_if add: Correctness.hom_def
+apply (simp (no_asm) cong del: if_weak_cong split del: if_split add: Correctness.hom_def
cancel_restrict externals_lemma)
apply (rule conjI)
apply (simp (no_asm) add: hom_ioas)
--- a/src/HOL/HOLCF/IOA/NTP/Impl.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy Tue Feb 23 18:04:31 2016 +0100
@@ -107,10 +107,10 @@
fun tac ctxt =
asm_simp_tac (put_simpset ss ctxt
- |> Simplifier.add_cong @{thm conj_cong} |> Splitter.add_split @{thm split_if})
+ |> Simplifier.add_cong @{thm conj_cong} |> Splitter.add_split @{thm if_split})
fun tac_ren ctxt =
asm_simp_tac (put_simpset rename_ss ctxt
- |> Simplifier.add_cong @{thm conj_cong} |> Splitter.add_split @{thm split_if})
+ |> Simplifier.add_cong @{thm conj_cong} |> Splitter.add_split @{thm if_split})
\<close>
@@ -128,7 +128,7 @@
apply (rule conjI)
(* First half *)
-apply (simp add: Impl.inv1_def split del: split_if)
+apply (simp add: Impl.inv1_def split del: if_split)
apply (induct_tac a)
apply (tactic "EVERY1[tac @{context}, tac @{context}, tac @{context}, tac @{context}]")
@@ -145,7 +145,7 @@
txt \<open>Now the other half\<close>
-apply (simp add: Impl.inv1_def split del: split_if)
+apply (simp add: Impl.inv1_def split del: if_split)
apply (induct_tac a)
apply (tactic "EVERY1 [tac @{context}, tac @{context}]")
@@ -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: split_if)
+ split add: 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: split_if)
+ Multiset.delm_nonempty_def split add: if_split)
apply (rule allI)
apply (rule conjI)
apply (rule impI)
@@ -198,7 +198,7 @@
txt \<open>Base case\<close>
apply (simp add: inv2_def receiver_projections sender_projections impl_ioas)
- apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
+ apply (simp (no_asm_simp) add: impl_ioas split del: if_split)
apply (induct_tac "a")
txt \<open>10 cases. First 4 are simple, since state doesn't change\<close>
@@ -257,7 +257,7 @@
txt \<open>Base case\<close>
apply (simp add: Impl.inv3_def receiver_projections sender_projections impl_ioas)
- apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
+ apply (simp (no_asm_simp) add: impl_ioas split del: if_split)
apply (induct_tac "a")
ML_prf \<open>val tac3 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv3_def}])\<close>
@@ -322,7 +322,7 @@
txt \<open>Base case\<close>
apply (simp add: Impl.inv4_def receiver_projections sender_projections impl_ioas)
- apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
+ apply (simp (no_asm_simp) add: impl_ioas split del: if_split)
apply (induct_tac "a")
ML_prf \<open>val tac4 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv4_def}])\<close>
--- a/src/HOL/HOLCF/IOA/RefCorrectness.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/HOLCF/IOA/RefCorrectness.thy Tue Feb 23 18:04:31 2016 +0100
@@ -182,14 +182,14 @@
"is_ref_map f C A \<Longrightarrow> ext C = ext A \<Longrightarrow>
\<forall>s. reachable C s \<and> is_exec_frag C (s, xs) \<longrightarrow>
mk_trace C $ xs = mk_trace A $ (snd (corresp_ex A f (s, xs)))"
- supply split_if [split del]
+ supply if_split [split del]
apply (unfold corresp_ex_def)
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)
apply assumption
- apply (auto simp add: move_subprop4 split add: split_if)
+ apply (auto simp add: move_subprop4 split add: if_split)
done
--- a/src/HOL/HOLCF/IOA/RefMappings.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/HOLCF/IOA/RefMappings.thy Tue Feb 23 18:04:31 2016 +0100
@@ -66,7 +66,7 @@
lemma imp_conj_lemma: "(P \<Longrightarrow> Q \<longrightarrow> R) \<Longrightarrow> P \<and> Q \<longrightarrow> R"
by blast
-declare split_if [split del]
+declare if_split [split del]
declare if_weak_cong [cong del]
lemma rename_through_pmap:
@@ -81,7 +81,7 @@
apply (simp (no_asm) add: rename_def rename_set_def)
apply (simp add: externals_def asig_inputs_def asig_outputs_def asig_of_def trans_of_def)
apply safe
- apply (simplesubst split_if)
+ apply (simplesubst if_split)
apply (rule conjI)
apply (rule impI)
apply (erule disjE)
@@ -108,7 +108,7 @@
apply auto
done
-declare split_if [split]
+declare if_split [split]
declare if_weak_cong [cong]
end
--- a/src/HOL/HOLCF/IOA/SimCorrectness.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/HOLCF/IOA/SimCorrectness.thy Tue Feb 23 18:04:31 2016 +0100
@@ -162,7 +162,7 @@
"is_simulation R C A \<Longrightarrow> ext C = ext A \<Longrightarrow>
\<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]
+ supply if_split [split del]
apply (pair_induct ex simp: is_exec_frag_def)
text \<open>cons case\<close>
apply auto
@@ -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: split_if)
+ move_subprop4_sim [unfolded Let_def] split add: if_split)
done
text \<open>Lemma 2: \<open>corresp_ex_sim\<close> is execution\<close>
--- a/src/HOL/HOLCF/IOA/TL.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/HOLCF/IOA/TL.thy Tue Feb 23 18:04:31 2016 +0100
@@ -121,14 +121,14 @@
lemmas tsuffix_TL2 = conjI [THEN tsuffix_TL]
lemma LTL1: "s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> (F \<^bold>\<and> (Next (\<box>F))))"
- supply split_if [split del]
+ supply if_split [split del]
apply (unfold Next_def satisfies_def NOT_def IMPLIES_def AND_def Box_def)
apply auto
text \<open>\<open>\<box>F \<^bold>\<longrightarrow> F\<close>\<close>
apply (erule_tac x = "s" in allE)
apply (simp add: tsuffix_def suffix_refl)
text \<open>\<open>\<box>F \<^bold>\<longrightarrow> Next \<box>F\<close>\<close>
- apply (simp split add: split_if)
+ apply (simp split add: if_split)
apply auto
apply (drule tsuffix_TL2)
apply assumption+
--- a/src/HOL/HOLCF/IOA/TLS.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/HOLCF/IOA/TLS.thy Tue Feb 23 18:04:31 2016 +0100
@@ -140,7 +140,7 @@
\<^bold>\<longrightarrow> (Next (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: split_if)
+ apply (simp split add: if_split)
text \<open>\<open>TL = UU\<close>\<close>
apply (rule conjI)
apply (pair ex)
--- a/src/HOL/HOLCF/Universal.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/HOLCF/Universal.thy Tue Feb 23 18:04:31 2016 +0100
@@ -377,7 +377,7 @@
apply (rule inj_onI)
apply (drule_tac x="A - {choose A}" in meta_spec, simp)
apply (simp add: choose_pos.simps)
- apply (simp split: split_if_asm)
+ apply (simp split: if_split_asm)
apply (erule (1) inj_onD, simp, simp)
done
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Lemmas.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Lemmas.thy Tue Feb 23 18:04:31 2016 +0100
@@ -1,4 +1,4 @@
(*<*)
theory Hahn_Banach_Lemmas imports Hahn_Banach_Sup_Lemmas Hahn_Banach_Ext_Lemmas begin
end
-(*>*)
\ No newline at end of file
+(*>*)
--- a/src/HOL/Hoare/Examples.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Hoare/Examples.thy Tue Feb 23 18:04:31 2016 +0100
@@ -233,4 +233,4 @@
apply (force simp: nth_list_update)
done
-end
\ No newline at end of file
+end
--- a/src/HOL/Hoare_Parallel/OG_Com.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Com.thy Tue Feb 23 18:04:31 2016 +0100
@@ -47,4 +47,4 @@
| "atom_com (Cond b c1 c2) = (atom_com c1 \<and> atom_com c2)"
| "atom_com (While b i c) = atom_com c"
-end
\ No newline at end of file
+end
--- a/src/HOL/Hoare_Parallel/OG_Hoare.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy Tue Feb 23 18:04:31 2016 +0100
@@ -408,13 +408,13 @@
apply(rule conjI)
apply clarify
apply(case_tac "i=j")
- apply(simp split del:split_if)
+ apply(simp split del:if_split)
apply(erule Strong_Soundness_aux_aux,simp+)
apply force
apply force
- apply(simp split del: split_if)
+ apply(simp split del: if_split)
apply(erule Parallel_Strong_Soundness_aux_aux)
- apply(simp_all add: split del:split_if)
+ apply(simp_all add: split del:if_split)
apply force
apply(rule interfree_lemma)
apply simp_all
--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Tue Feb 23 18:04:31 2016 +0100
@@ -125,4 +125,4 @@
end;
\<close>
-end
\ No newline at end of file
+end
--- a/src/HOL/Hoare_Parallel/OG_Tran.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Tran.thy Tue Feb 23 18:04:31 2016 +0100
@@ -300,4 +300,4 @@
definition ann_com_validity :: "'a ann_com \<Rightarrow> 'a assn \<Rightarrow> bool" ("\<Turnstile> _ _" [60,90] 45) where
"\<Turnstile> c q \<equiv> ann_SEM c (pre c) \<subseteq> q"
-end
\ No newline at end of file
+end
--- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Tue Feb 23 18:04:31 2016 +0100
@@ -17,4 +17,4 @@
in [(@{syntax_const "_quote"}, K quote_tr)] end
\<close>
-end
\ No newline at end of file
+end
--- a/src/HOL/Hoare_Parallel/RG_Com.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Com.thy Tue Feb 23 18:04:31 2016 +0100
@@ -19,4 +19,4 @@
type_synonym 'a par_com = "'a com option list"
-end
\ No newline at end of file
+end
--- a/src/HOL/Hoare_Parallel/RG_Syntax.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy Tue Feb 23 18:04:31 2016 +0100
@@ -79,4 +79,4 @@
end
\<close>
-end
\ No newline at end of file
+end
--- a/src/HOL/Hoare_Parallel/RG_Tran.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Tran.thy Tue Feb 23 18:04:31 2016 +0100
@@ -320,7 +320,7 @@
apply(drule_tac P=P1 in lift_is_cptn)
apply(simp add:lift_def)
apply simp
-apply(simp split: split_if_asm)
+apply(simp split: if_split_asm)
apply(frule_tac P=P1 in last_lift)
apply(rule last_fst_esp)
apply (simp add:last_length)
@@ -337,7 +337,7 @@
apply(drule_tac P="While b P" in lift_is_cptn)
apply(simp add:lift_def)
apply simp
-apply(simp split: split_if_asm)
+apply(simp split: if_split_asm)
apply(frule_tac P="While b P" in last_lift)
apply(rule last_fst_esp,simp add:last_length)
apply(simp add:Cons_lift lift_def split_def last_conv_nth)
--- a/src/HOL/IMP/Compiler2.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/IMP/Compiler2.thy Tue Feb 23 18:04:31 2016 +0100
@@ -465,7 +465,7 @@
s' = s \<and> stk' = stk"
using assms proof (induction b arbitrary: f j i n s' stk')
case Bc thus ?case
- by (simp split: split_if_asm add: exec_n_simps exec1_def)
+ by (simp split: if_split_asm add: exec_n_simps exec1_def)
next
case (Not b)
from Not.prems show ?case
@@ -490,7 +490,7 @@
by (auto dest!: And.IH)
with b2 j
show ?case
- by (fastforce dest!: And.IH simp: exec_n_end split: split_if_asm)
+ by (fastforce dest!: And.IH simp: exec_n_end split: if_split_asm)
next
case Less
thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps exec1_def) (* takes time *)
@@ -547,7 +547,7 @@
show ?thesis
by simp
(fastforce dest: exec_n_drop_right
- split: split_if_asm
+ split: if_split_asm
simp: exec_n_simps exec1_def)
next
case False with cs'
--- a/src/HOL/IMP/Finite_Reachable.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/IMP/Finite_Reachable.thy Tue Feb 23 18:04:31 2016 +0100
@@ -158,4 +158,4 @@
done
-end
\ No newline at end of file
+end
--- a/src/HOL/IOA/Solve.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/IOA/Solve.thy Tue Feb 23 18:04:31 2016 +0100
@@ -106,7 +106,7 @@
split add: option.split)
done
-declare split_if [split del] if_weak_cong [cong del]
+declare if_split [split del] if_weak_cong [cong del]
(*Composition of possibility-mappings *)
lemma fxg_is_weak_pmap_of_product_IOA:
@@ -126,7 +126,7 @@
apply (simp (no_asm) add: externals_of_par_extra)
apply (simp (no_asm) add: par_def)
apply (simp add: trans_of_def)
- apply (simplesubst split_if)
+ apply (simplesubst if_split)
apply (rule conjI)
apply (rule impI)
apply (erule disjE)
@@ -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: split_if)
+ apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: if_split)
apply (tactic {*
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) *})
@@ -172,7 +172,7 @@
apply (simp (no_asm) add: rename_def)
apply (simp add: externals_def asig_inputs_def asig_outputs_def asig_of_def trans_of_def)
apply safe
- apply (simplesubst split_if)
+ apply (simplesubst if_split)
apply (rule conjI)
apply (rule impI)
apply (erule disjE)
@@ -204,6 +204,6 @@
apply auto
done
-declare split_if [split] if_weak_cong [cong]
+declare if_split [split] if_weak_cong [cong]
end
--- a/src/HOL/Imperative_HOL/Overview.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Imperative_HOL/Overview.thy Tue Feb 23 18:04:31 2016 +0100
@@ -240,4 +240,4 @@
\end{itemize}
*}
-end
\ No newline at end of file
+end
--- a/src/HOL/Imperative_HOL/ex/Sorted_List.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Imperative_HOL/ex/Sorted_List.thy Tue Feb 23 18:04:31 2016 +0100
@@ -95,4 +95,4 @@
lemma "sorted xs \<Longrightarrow> smember xs x \<longleftrightarrow> (x \<in> set xs)"
by (induct xs) (auto simp add: sorted_Cons)
-end
\ No newline at end of file
+end
--- a/src/HOL/Imperative_HOL/ex/Subarray.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Imperative_HOL/ex/Subarray.thy Tue Feb 23 18:04:31 2016 +0100
@@ -68,4 +68,4 @@
lemma ball_in_set_subarray_conv: "(\<forall>j \<in> set (subarray l r a h). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Array.length h a \<longrightarrow> P (Array.get h a ! k))"
unfolding subarray_def Array.length_def by (rule ball_in_set_sublist'_conv)
-end
\ No newline at end of file
+end
--- a/src/HOL/Induct/Common_Patterns.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Induct/Common_Patterns.thy Tue Feb 23 18:04:31 2016 +0100
@@ -402,4 +402,4 @@
with step.r show ?case by (rule star.step)
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/Int.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Int.thy Tue Feb 23 18:04:31 2016 +0100
@@ -1190,7 +1190,7 @@
apply (case_tac "k = f (Suc n)")
apply force
apply (erule impE)
- apply (simp add: abs_if split add: split_if_asm)
+ apply (simp add: abs_if split add: if_split_asm)
apply (blast intro: le_SucI)
done
--- a/src/HOL/Isar_Examples/Group.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Isar_Examples/Group.thy Tue Feb 23 18:04:31 2016 +0100
@@ -254,4 +254,4 @@
finally show ?thesis .
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/AList.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/AList.thy Tue Feb 23 18:04:31 2016 +0100
@@ -58,11 +58,11 @@
proof (induct al arbitrary: al')
case Nil
then show ?case
- by (cases al') (auto split: split_if_asm)
+ by (cases al') (auto split: if_split_asm)
next
case Cons
then show ?case
- by (cases al') (auto split: split_if_asm)
+ by (cases al') (auto split: if_split_asm)
qed
lemma update_last [simp]: "update k v (update k v' al) = update k v al"
@@ -293,7 +293,7 @@
by(simp add: map_of_delete_aux')
lemma delete_aux_eq_Nil_conv: "delete_aux k ts = [] \<longleftrightarrow> ts = [] \<or> (\<exists>v. ts = [(k, v)])"
-by(cases ts)(auto split: split_if_asm)
+by(cases ts)(auto split: if_split_asm)
subsection \<open>\<open>restrict\<close>\<close>
@@ -574,7 +574,7 @@
lemma compose_first_None [simp]:
assumes "map_of xs k = None"
shows "map_of (compose xs ys) k = None"
- using assms by (induct xs ys rule: compose.induct) (auto split: option.splits split_if_asm)
+ using assms by (induct xs ys rule: compose.induct) (auto split: option.splits if_split_asm)
lemma compose_conv: "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
proof (induct xs ys rule: compose.induct)
--- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy Tue Feb 23 18:04:31 2016 +0100
@@ -253,4 +253,4 @@
end
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Cardinality.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/Cardinality.thy Tue Feb 23 18:04:31 2016 +0100
@@ -495,7 +495,7 @@
with that show ?thesis
by (auto simp add: rhs_def Let_def List.card_set[symmetric]
card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"]
- dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm)
+ dest: card_eq_UNIV_imp_eq_UNIV split: if_split_asm)
qed
qed
}
--- a/src/HOL/Library/Countable_Complete_Lattices.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/Countable_Complete_Lattices.thy Tue Feb 23 18:04:31 2016 +0100
@@ -274,4 +274,4 @@
subclass (in complete_distrib_lattice) countable_complete_distrib_lattice
by standard (auto intro: sup_Inf inf_Sup)
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Countable_Set.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/Countable_Set.thy Tue Feb 23 18:04:31 2016 +0100
@@ -94,7 +94,7 @@
unfolding from_nat_into_def[abs_def]
using to_nat_on_finite[of S]
apply (subst bij_betw_cong)
- apply (split split_if)
+ apply (split if_split)
apply (simp add: bij_betw_def)
apply (auto cong: bij_betw_cong
intro: bij_betw_inv_into to_nat_on_finite)
@@ -303,7 +303,7 @@
assumes "countable X" obtains F where "\<And>i. F i \<subseteq> X" "\<And>i. F i \<subseteq> F (Suc i)" "\<And>i. finite (F i)" "(\<Union>i. F i) = X"
proof - show thesis
apply (rule that[of "\<lambda>i. if X = {} then {} else from_nat_into X ` {..i}"])
- apply (auto simp: image_iff Ball_def intro: from_nat_into split: split_if_asm)
+ apply (auto simp: image_iff Ball_def intro: from_nat_into split: if_split_asm)
proof -
fix x n assume "x \<in> X" "\<forall>i m. m \<le> i \<longrightarrow> x \<noteq> from_nat_into X m"
with from_nat_into_surj[OF \<open>countable X\<close> \<open>x \<in> X\<close>]
--- a/src/HOL/Library/Countable_Set_Type.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy Tue Feb 23 18:04:31 2016 +0100
@@ -219,8 +219,8 @@
lemmas cimage_csubset_iff[no_atp] = image_subset_iff[Transfer.transferred]
lemmas cimage_csubsetI = image_subsetI[Transfer.transferred]
lemmas cimage_ident[simp] = image_ident[Transfer.transferred]
-lemmas split_if_cin1 = split_if_mem1[Transfer.transferred]
-lemmas split_if_cin2 = split_if_mem2[Transfer.transferred]
+lemmas if_split_cin1 = if_split_mem1[Transfer.transferred]
+lemmas if_split_cin2 = if_split_mem2[Transfer.transferred]
lemmas cpsubsetI[intro!,no_atp] = psubsetI[Transfer.transferred]
lemmas cpsubsetE[elim!,no_atp] = psubsetE[Transfer.transferred]
lemmas cpsubset_finsert_iff = psubset_insert_iff[Transfer.transferred]
--- a/src/HOL/Library/Discrete.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/Discrete.thy Tue Feb 23 18:04:31 2016 +0100
@@ -219,4 +219,4 @@
end
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Disjoint_Sets.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/Disjoint_Sets.thy Tue Feb 23 18:04:31 2016 +0100
@@ -153,4 +153,4 @@
lemma disjointed_mono: "mono A \<Longrightarrow> disjointed A (Suc n) = A (Suc n) - A n"
using mono_Un[of A] by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Dlist.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/Dlist.thy Tue Feb 23 18:04:31 2016 +0100
@@ -241,7 +241,7 @@
proof(induction xs ys rule: wpull.induct)
case 1 thus ?case by(simp add: Nil)
next
- case 2 thus ?case by(simp split: split_if_asm)
+ case 2 thus ?case by(simp split: if_split_asm)
next
case Cons: (3 a b xs b' c ys)
let ?xs = "(a, b) # xs" and ?ys = "(b', c) # ys"
@@ -254,7 +254,7 @@
from xs eq have "b \<in> fst ` set ?ys" by (metis list.set_map set_remdups)
hence "map_of (rev ?ys) b \<noteq> None" unfolding map_of_eq_None_iff by auto
then obtain c' where "map_of (rev ?ys) b = Some c'" by blast
- then have "(b, the (map_of (rev ?ys) b)) \<in> set ?ys" by(auto dest: map_of_SomeD split: split_if_asm)
+ then have "(b, the (map_of (rev ?ys) b)) \<in> set ?ys" by(auto dest: map_of_SomeD split: if_split_asm)
from xs eq this Cons.IH(1)[OF xs eq] show ?thesis by(rule left)
next
case ys
@@ -264,7 +264,7 @@
unfolding map_of_eq_None_iff by(auto simp add: image_image)
then obtain a' where "map_of (map prod.swap (rev ?xs)) b' = Some a'" by blast
then have "(the (map_of (map prod.swap (rev ?xs)) b'), b') \<in> set ?xs"
- by(auto dest: map_of_SomeD split: split_if_asm)
+ by(auto dest: map_of_SomeD split: if_split_asm)
from ys eq this Cons.IH(2)[OF ys eq] show ?thesis by(rule right)
next
case *: step
@@ -334,4 +334,4 @@
end
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Extended_Real.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/Extended_Real.thy Tue Feb 23 18:04:31 2016 +0100
@@ -1592,7 +1592,7 @@
shows "b < c"
using assms
by (cases rule: ereal3_cases[of a b c])
- (auto split: split_if_asm simp: zero_less_mult_iff zero_le_mult_iff)
+ (auto split: if_split_asm simp: zero_less_mult_iff zero_le_mult_iff)
lemma ereal_mult_divide: fixes a b :: ereal shows "0 < b \<Longrightarrow> b < \<infinity> \<Longrightarrow> b * (a / b) = a"
by (cases a b rule: ereal2_cases) auto
@@ -1646,7 +1646,7 @@
shows "z / x \<le> z / y"
using assms
by (cases x y z rule: ereal3_cases)
- (auto intro: divide_left_mono simp: field_simps zero_less_mult_iff mult_less_0_iff split: split_if_asm)
+ (auto intro: divide_left_mono simp: field_simps zero_less_mult_iff mult_less_0_iff split: if_split_asm)
lemma ereal_divide_zero_left[simp]:
fixes a :: ereal
@@ -2852,7 +2852,7 @@
by (auto simp: dist_real_def abs_diff_less_iff field_simps)
from dist[OF this] show "u N \<in> S"
using \<open>u N \<notin> {\<infinity>, -\<infinity>}\<close>
- by (auto simp: ereal_real split: split_if_asm)
+ by (auto simp: ereal_real split: if_split_asm)
qed
qed
--- a/src/HOL/Library/FSet.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/FSet.thy Tue Feb 23 18:04:31 2016 +0100
@@ -300,8 +300,8 @@
lemmas fimage_fsubset_iff[no_atp] = image_subset_iff[Transfer.transferred]
lemmas fimage_fsubsetI = image_subsetI[Transfer.transferred]
lemmas fimage_ident[simp] = image_ident[Transfer.transferred]
-lemmas split_if_fmem1 = split_if_mem1[Transfer.transferred]
-lemmas split_if_fmem2 = split_if_mem2[Transfer.transferred]
+lemmas if_split_fmem1 = if_split_mem1[Transfer.transferred]
+lemmas if_split_fmem2 = if_split_mem2[Transfer.transferred]
lemmas pfsubsetI[intro!,no_atp] = psubsetI[Transfer.transferred]
lemmas pfsubsetE[elim!,no_atp] = psubsetE[Transfer.transferred]
lemmas pfsubset_finsert_iff = psubset_insert_iff[Transfer.transferred]
--- a/src/HOL/Library/FinFun.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/FinFun.thy Tue Feb 23 18:04:31 2016 +0100
@@ -578,7 +578,7 @@
have gg: "g = ?g" unfolding g
proof(rule the_equality)
from f y bfin show "?the f ?g"
- by(auto)(simp add: restrict_map_def ran_def split: split_if_asm)
+ by(auto)(simp add: restrict_map_def ran_def split: if_split_asm)
next
fix g'
assume "?the f g'"
@@ -1308,7 +1308,7 @@
case (update f a b)
have "{x. finfun_dom f(a $:= b) $ x} =
(if b = finfun_default f then {x. finfun_dom f $ x} - {a} else insert a {x. finfun_dom f $ x})"
- by (auto simp add: finfun_upd_apply split: split_if_asm)
+ by (auto simp add: finfun_upd_apply split: if_split_asm)
thus ?case using update by simp
qed
@@ -1372,7 +1372,7 @@
have "set (insort_insert a xs) = insert a (set xs)" by(simp add: set_insort_insert)
also note eq also
have "insert a {x. finfun_dom f(a $:= b) $ x} = {x. finfun_dom f $ x}" using True
- by(auto simp add: finfun_upd_apply split: split_if_asm)
+ by(auto simp add: finfun_upd_apply split: if_split_asm)
finally show 1: "set (insort_insert a xs) = {x. finfun_dom f $ x} \<and> sorted (insort_insert a xs) \<and> distinct (insort_insert a xs)"
by(simp add: sorted_insort_insert distinct_insort_insert)
@@ -1415,7 +1415,7 @@
have "set (remove1 a xs) = set xs - {a}" by simp
also note eq also
have "{x. finfun_dom f(a $:= b) $ x} - {a} = {x. finfun_dom f $ x}" using False
- by(auto simp add: finfun_upd_apply split: split_if_asm)
+ by(auto simp add: finfun_upd_apply split: if_split_asm)
finally show 1: "set (remove1 a xs) = {x. finfun_dom f $ x} \<and> sorted (remove1 a xs) \<and> distinct (remove1 a xs)"
by(simp add: sorted_remove1)
@@ -1427,7 +1427,7 @@
by (simp add: insort_insert_insort insort_remove1)
qed
qed
-qed (auto simp add: distinct_finfun_to_list sorted_finfun_to_list sorted_remove1 set_insort_insert sorted_insort_insert distinct_insort_insert finfun_upd_apply split: split_if_asm)
+qed (auto simp add: distinct_finfun_to_list sorted_finfun_to_list sorted_remove1 set_insort_insert sorted_insort_insert distinct_insort_insert finfun_upd_apply split: if_split_asm)
lemma finfun_to_list_update_code [code]:
"finfun_to_list (finfun_update_code f a b) =
@@ -1489,7 +1489,7 @@
hence "finite (range ?f)"
by(rule finite_subset[rotated 1])(auto simp add: F_def finfun_def \<open>b1 \<noteq> b2\<close> intro!: exI[where x=b2])
thus "finite (UNIV :: 'a set)"
- by(rule finite_imageD)(auto intro: inj_onI simp add: fun_eq_iff \<open>b1 \<noteq> b2\<close> split: split_if_asm)
+ by(rule finite_imageD)(auto intro: inj_onI simp add: fun_eq_iff \<open>b1 \<noteq> b2\<close> split: if_split_asm)
from finite have "finite (range (\<lambda>b. ((K$ b) :: 'a \<Rightarrow>f 'b)))"
by(rule finite_subset[rotated 1]) simp
--- a/src/HOL/Library/FinFun_Syntax.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/FinFun_Syntax.thy Tue Feb 23 18:04:31 2016 +0100
@@ -21,4 +21,4 @@
finfun_comp (infixr "o$" 55) and
finfun_comp2 (infixr "$o" 55)
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Float.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/Float.thy Tue Feb 23 18:04:31 2016 +0100
@@ -1612,7 +1612,7 @@
then have floor_eq: "\<lfloor>b * 2 powr (real_of_int p + 1)\<rfloor> = -1"
using b_le_1
by (auto simp: floor_eq_iff algebra_simps pos_divide_le_eq[symmetric] abs_if divide_powr_uminus
- intro!: mult_neg_pos split: split_if_asm)
+ intro!: mult_neg_pos split: if_split_asm)
have "\<lfloor>(a + b) * 2 powr q\<rfloor> = \<lfloor>(2*a + 2*b) * 2 powr p * 2 powr (q - p - 1)\<rfloor>"
by (simp add: algebra_simps powr_realpow[symmetric] powr_add[symmetric] powr_mult_base)
also have "\<dots> = \<lfloor>(2 * (a * 2 powr p) + 2 * b * 2 powr p) * 2 powr (q - p - 1)\<rfloor>"
@@ -1667,10 +1667,10 @@
have pos: "\<bar>b\<bar> < 1 \<Longrightarrow> 0 < 2 powr k + (r + b)" for b :: real
using \<open>0 \<le> k\<close> \<open>ai \<noteq> 0\<close>
by (auto simp add: r_def powr_realpow[symmetric] abs_if sgn_if algebra_simps
- split: split_if_asm)
+ split: if_split_asm)
have less: "\<bar>sgn ai * b\<bar> < 1"
and less': "\<bar>sgn (sgn ai * b) / 2\<bar> < 1"
- using \<open>\<bar>b\<bar> \<le> _\<close> by (auto simp: abs_if sgn_if split: split_if_asm)
+ using \<open>\<bar>b\<bar> \<le> _\<close> by (auto simp: abs_if sgn_if split: if_split_asm)
have floor_eq: "\<And>b::real. \<bar>b\<bar> \<le> 1 / 2 \<Longrightarrow>
\<lfloor>log 2 (1 + (r + b) / 2 powr k)\<rfloor> = (if r = 0 \<and> b < 0 then -1 else 0)"
@@ -1751,7 +1751,7 @@
finally have b_less_half_a: "\<bar>?b\<bar> < 1/2 * \<bar>?a\<bar>"
by (simp add: algebra_simps powr_mult_base abs_mult)
then have a_half_less_sum: "\<bar>?a\<bar> / 2 < \<bar>?sum\<bar>"
- by (auto simp: field_simps abs_if split: split_if_asm)
+ by (auto simp: field_simps abs_if split: if_split_asm)
from b_less_half_a have "\<bar>?b\<bar> < \<bar>?a\<bar>" "\<bar>?b\<bar> \<le> \<bar>?a\<bar>"
by simp_all
--- a/src/HOL/Library/Formal_Power_Series.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Tue Feb 23 18:04:31 2016 +0100
@@ -472,7 +472,7 @@
proof
assume "(X :: 'a fps) ^ m = X ^ n"
hence "(X :: 'a fps) ^ m $ m = X ^ n $ m" by (simp only:)
- thus "m = n" by (simp split: split_if_asm)
+ thus "m = n" by (simp split: if_split_asm)
qed simp_all
@@ -767,7 +767,7 @@
proof (cases "f = 0")
assume "f \<noteq> 0"
with A have "n \<le> subdegree f"
- by (intro subdegree_geI) (auto simp: fps_eq_iff split: split_if_asm)
+ by (intro subdegree_geI) (auto simp: fps_eq_iff split: if_split_asm)
thus ?thesis ..
qed simp
qed (auto simp: fps_eq_iff intro: nth_less_subdegree_zero)
@@ -824,7 +824,7 @@
instance
proof
show th: "dist a b = 0 \<longleftrightarrow> a = b" for a b :: "'a fps"
- by (simp add: dist_fps_def split: split_if_asm)
+ by (simp add: dist_fps_def split: if_split_asm)
then have th'[simp]: "dist a a = 0" for a :: "'a fps" by simp
fix a b c :: "'a fps"
@@ -4376,7 +4376,7 @@
assume "f $ j \<noteq> g $ j"
hence "f \<noteq> g" by auto
with assms have "i < subdegree (f - g)"
- by (simp add: split_if_asm dist_fps_def)
+ by (simp add: if_split_asm dist_fps_def)
also have "\<dots> \<le> j"
using \<open>f $ j \<noteq> g $ j\<close> by (intro subdegree_leI) simp_all
finally show False using \<open>j \<le> i\<close> by simp
@@ -4391,7 +4391,7 @@
next
case False
with assms have "dist f g = inverse (2 ^ subdegree (f - g))"
- by (simp add: split_if_asm dist_fps_def)
+ by (simp add: if_split_asm dist_fps_def)
moreover
from assms and False have "i < subdegree (f - g)"
by (intro subdegree_greaterI) simp_all
--- a/src/HOL/Library/FuncSet.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/FuncSet.thy Tue Feb 23 18:04:31 2016 +0100
@@ -151,7 +151,7 @@
lemma Pi_fupd_iff: "i \<in> I \<Longrightarrow> f \<in> Pi I (B(i := A)) \<longleftrightarrow> f \<in> Pi (I - {i}) B \<and> f i \<in> A"
apply auto
apply (drule_tac x=x in Pi_mem)
- apply (simp_all split: split_if_asm)
+ apply (simp_all split: if_split_asm)
apply (drule_tac x=i in Pi_mem)
apply (auto dest!: Pi_mem)
done
@@ -527,7 +527,7 @@
apply (auto intro: PiE_mem del: PiE_I PiE_E)
apply (rule_tac x="xa(x := undefined)" in exI)
apply (auto intro!: extensional_funcset_fun_upd_restricts_rangeI)
- apply (auto dest!: PiE_mem split: split_if_asm)
+ apply (auto dest!: PiE_mem split: if_split_asm)
done
lemma extensional_funcset_extend_domain_inj_onI:
@@ -555,7 +555,7 @@
unfolding fun_eq_iff by auto
from this[of x] show "y = z" by simp
fix i from *[of i] \<open>x \<notin> S\<close> fg show "f i = g i"
- by (auto split: split_if_asm simp: PiE_def extensional_def)
+ by (auto split: if_split_asm simp: PiE_def extensional_def)
qed
lemma card_PiE: "finite S \<Longrightarrow> card (\<Pi>\<^sub>E i \<in> S. T i) = (\<Prod> i\<in>S. card (T i))"
--- a/src/HOL/Library/Indicator_Function.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/Indicator_Function.thy Tue Feb 23 18:04:31 2016 +0100
@@ -68,7 +68,7 @@
shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)"
and setsum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator B x * f x) = (\<Sum>x \<in> A \<inter> B. f x)"
unfolding indicator_def
- using assms by (auto intro!: setsum.mono_neutral_cong_right split: split_if_asm)
+ using assms by (auto intro!: setsum.mono_neutral_cong_right split: if_split_asm)
lemma setsum_indicator_eq_card:
assumes "finite A"
@@ -79,7 +79,7 @@
lemma setsum_indicator_scaleR[simp]:
"finite A \<Longrightarrow>
(\<Sum>x \<in> A. indicator (B x) (g x) *\<^sub>R f x) = (\<Sum>x \<in> {x\<in>A. g x \<in> B x}. f x::'a::real_vector)"
- using assms by (auto intro!: setsum.mono_neutral_cong_right split: split_if_asm simp: indicator_def)
+ using assms by (auto intro!: setsum.mono_neutral_cong_right split: if_split_asm simp: indicator_def)
lemma LIMSEQ_indicator_incseq:
assumes "incseq A"
--- a/src/HOL/Library/Lattice_Constructions.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/Lattice_Constructions.thy Tue Feb 23 18:04:31 2016 +0100
@@ -485,4 +485,4 @@
end
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Tue Feb 23 18:04:31 2016 +0100
@@ -767,4 +767,4 @@
lemma hld_smap': "HLD x (smap f s) = HLD (f -` x) s"
by (simp add: HLD_def)
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Multiset.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/Multiset.thy Tue Feb 23 18:04:31 2016 +0100
@@ -357,13 +357,13 @@
apply (clarsimp simp: subset_mset_def subseteq_mset_def)
apply safe
apply (erule_tac x = a in allE)
- apply (auto split: split_if_asm)
+ apply (auto split: if_split_asm)
done
lemma mset_le_insertD: "(A + {#x#} \<le># B) \<Longrightarrow> (x \<in># B \<and> A \<le># B)"
apply (rule conjI)
apply (simp add: mset_leD)
-apply (force simp: subset_mset_def subseteq_mset_def split: split_if_asm)
+apply (force simp: subset_mset_def subseteq_mset_def split: if_split_asm)
done
lemma mset_less_of_empty[simp]: "A <# {#} \<longleftrightarrow> False"
--- a/src/HOL/Library/Nonpos_Ints.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/Nonpos_Ints.thy Tue Feb 23 18:04:31 2016 +0100
@@ -301,4 +301,4 @@
lemma ii_not_nonpos_Reals [iff]: "\<i> \<notin> \<real>\<^sub>\<le>\<^sub>0"
by (simp add: complex_nonpos_Reals_iff)
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Periodic_Fun.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/Periodic_Fun.thy Tue Feb 23 18:04:31 2016 +0100
@@ -129,4 +129,4 @@
interpretation cot: periodic_fun_simple cot "2 * of_real pi :: 'a :: {real_normed_field,banach}"
by standard (simp only: cot_def [abs_def] sin.plus_1 cos.plus_1)
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Permutations.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/Permutations.thy Tue Feb 23 18:04:31 2016 +0100
@@ -1033,7 +1033,7 @@
by simp
then have bc: "b = c"
by (simp add: permutes_def pa qa o_def fun_upd_def Fun.swap_def id_def
- cong del: if_weak_cong split: split_if_asm)
+ cong del: if_weak_cong split: if_split_asm)
from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> p) =
(\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> q)" by simp
then have "p = q"
--- a/src/HOL/Library/RBT_Impl.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/RBT_Impl.thy Tue Feb 23 18:04:31 2016 +0100
@@ -155,7 +155,7 @@
next
case (Branch color t1 a b t2)
let ?A = "Set.insert a (dom (rbt_lookup t1) \<union> dom (rbt_lookup t2))"
- have "dom (rbt_lookup (Branch color t1 a b t2)) \<subseteq> ?A" by (auto split: split_if_asm)
+ have "dom (rbt_lookup (Branch color t1 a b t2)) \<subseteq> ?A" by (auto split: if_split_asm)
moreover from Branch have "finite (insert a (dom (rbt_lookup t1) \<union> dom (rbt_lookup t2)))" by simp
ultimately show ?case by (rule finite_subset)
qed
--- a/src/HOL/Library/RBT_Mapping.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/RBT_Mapping.thy Tue Feb 23 18:04:31 2016 +0100
@@ -206,4 +206,4 @@
\vspace{1ex}
\<close>
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Transitive_Closure_Table.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Library/Transitive_Closure_Table.thy Tue Feb 23 18:04:31 2016 +0100
@@ -226,4 +226,4 @@
"\<lbrakk> rtrancl_path R x p y; \<And>x y. R x y \<Longrightarrow> S x y \<rbrakk> \<Longrightarrow> rtrancl_path S x p y"
by(induction rule: rtrancl_path.induct)(auto intro: rtrancl_path.intros)
-end
\ No newline at end of file
+end
--- a/src/HOL/Limits.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Limits.thy Tue Feb 23 18:04:31 2016 +0100
@@ -1354,7 +1354,7 @@
fix Z :: real assume "0 < Z"
from f \<open>0 < c\<close> have "eventually (\<lambda>x. c / 2 < f x) F"
by (auto dest!: tendstoD[where e="c / 2"] elim!: eventually_mono
- simp: dist_real_def abs_real_def split: split_if_asm)
+ simp: dist_real_def abs_real_def split: if_split_asm)
moreover from g have "eventually (\<lambda>x. (Z / c * 2) \<le> g x) F"
unfolding filterlim_at_top by auto
ultimately show "eventually (\<lambda>x. Z \<le> f x * g x) F"
--- a/src/HOL/List.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/List.thy Tue Feb 23 18:04:31 2016 +0100
@@ -620,7 +620,7 @@
resolve_tac ctxt [set_singleton] 1 ORELSE
resolve_tac ctxt [inst_Collect_mem_eq] 1
| tac ctxt (If :: cont) =
- Splitter.split_tac ctxt @{thms split_if} 1
+ Splitter.split_tac ctxt @{thms if_split} 1
THEN resolve_tac ctxt @{thms conjI} 1
THEN resolve_tac ctxt @{thms impI} 1
THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
@@ -1469,7 +1469,7 @@
case Nil thus ?case by simp
next
case (Cons x xs) thus ?case
- apply (auto split:split_if_asm)
+ apply (auto split:if_split_asm)
using length_filter_le[of P xs] apply arith
done
qed
@@ -1918,7 +1918,7 @@
by (induct xs) auto
lemma in_set_butlastD: "x : set (butlast xs) ==> x : set xs"
-by (induct xs) (auto split: split_if_asm)
+by (induct xs) (auto split: if_split_asm)
lemma in_set_butlast_appendI:
"x : set (butlast xs) | x : set (butlast ys) ==> x : set (butlast (xs @ ys))"
@@ -2261,10 +2261,10 @@
by (auto simp add: dropWhile_append3 in_set_conv_decomp)
lemma set_dropWhileD: "x \<in> set (dropWhile P xs) \<Longrightarrow> x \<in> set xs"
-by (induct xs) (auto split: split_if_asm)
+by (induct xs) (auto split: if_split_asm)
lemma set_takeWhileD: "x : set (takeWhile P xs) ==> x : set xs \<and> P x"
-by (induct xs) (auto split: split_if_asm)
+by (induct xs) (auto split: if_split_asm)
lemma takeWhile_eq_all_conv[simp]:
"(takeWhile P xs = xs) = (\<forall>x \<in> set xs. P x)"
@@ -3322,7 +3322,7 @@
next
case True with Cons.prems
have "card (set xs) = Suc (length xs)"
- by (simp add: card_insert_if split: split_if_asm)
+ by (simp add: card_insert_if split: if_split_asm)
moreover have "card (set xs) \<le> length xs" by (rule card_length)
ultimately have False by simp
thus ?thesis ..
@@ -3335,7 +3335,7 @@
lemma not_distinct_decomp: "~ distinct ws ==> EX xs ys zs y. ws = xs@[y]@ys@[y]@zs"
apply (induct n == "length ws" arbitrary:ws) apply simp
apply(case_tac ws) apply simp
-apply (simp split:split_if_asm)
+apply (simp split:if_split_asm)
apply (metis Cons_eq_appendI eq_Nil_appendI split_list)
done
@@ -3657,7 +3657,7 @@
lemma remdups_adj_singleton:
"remdups_adj xs = [x] \<Longrightarrow> xs = replicate (length xs) x"
-by (induct xs rule: remdups_adj.induct, auto split: split_if_asm)
+by (induct xs rule: remdups_adj.induct, auto split: if_split_asm)
lemma remdups_adj_map_injective:
assumes "inj f"
@@ -4814,7 +4814,7 @@
lemma sorted_remdups_adj[simp]:
"sorted xs \<Longrightarrow> sorted (remdups_adj xs)"
-by (induct xs rule: remdups_adj.induct, simp_all split: split_if_asm add: sorted_Cons)
+by (induct xs rule: remdups_adj.induct, simp_all split: if_split_asm add: sorted_Cons)
lemma sorted_distinct_set_unique:
assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys" "set xs = set ys"
@@ -6766,7 +6766,7 @@
lemma [code]:
"R `` S = List.map_project (%(x, y). if x : S then Some y else None) R"
-unfolding map_project_def by (auto split: prod.split split_if_asm)
+unfolding map_project_def by (auto split: prod.split if_split_asm)
lemma trancl_set_ntrancl [code]:
"trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
--- a/src/HOL/Map.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Map.thy Tue Feb 23 18:04:31 2016 +0100
@@ -358,10 +358,10 @@
by (simp add: restrict_map_def)
lemma ran_restrictD: "y \<in> ran (m|`A) \<Longrightarrow> \<exists>x\<in>A. m x = Some y"
-by (auto simp: restrict_map_def ran_def split: split_if_asm)
+by (auto simp: restrict_map_def ran_def split: if_split_asm)
lemma dom_restrict [simp]: "dom (m|`A) = dom m \<inter> A"
-by (auto simp: restrict_map_def dom_def split: split_if_asm)
+by (auto simp: restrict_map_def dom_def split: if_split_asm)
lemma restrict_upd_same [simp]: "m(x\<mapsto>y)|`(-{x}) = m|`(-{x})"
by (rule ext) (auto simp: restrict_map_def)
@@ -429,7 +429,7 @@
apply (induct xs arbitrary: x y ys f)
apply simp
apply (case_tac ys)
- apply (auto split: split_if simp: fun_upd_twist)
+ apply (auto split: if_split simp: fun_upd_twist)
done
lemma map_upds_twist [simp]:
@@ -691,7 +691,7 @@
lemma dom_eq_singleton_conv: "dom f = {x} \<longleftrightarrow> (\<exists>v. f = [x \<mapsto> v])"
proof(rule iffI)
assume "\<exists>v. f = [x \<mapsto> v]"
- thus "dom f = {x}" by(auto split: split_if_asm)
+ thus "dom f = {x}" by(auto split: if_split_asm)
next
assume "dom f = {x}"
then obtain v where "f x = Some v" by auto
--- a/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy Tue Feb 23 18:04:31 2016 +0100
@@ -16,4 +16,4 @@
ML_file "compute.ML"
ML_file "linker.ML"
-end
\ No newline at end of file
+end
--- a/src/HOL/Matrix_LP/Compute_Oracle/report.ML Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Matrix_LP/Compute_Oracle/report.ML Tue Feb 23 18:04:31 2016 +0100
@@ -30,4 +30,4 @@
end
end
-end
\ No newline at end of file
+end
--- a/src/HOL/Matrix_LP/LP.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Matrix_LP/LP.thy Tue Feb 23 18:04:31 2016 +0100
@@ -160,4 +160,4 @@
by(simp only:)
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/Matrix_LP/Matrix.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Matrix_LP/Matrix.thy Tue Feb 23 18:04:31 2016 +0100
@@ -1653,8 +1653,8 @@
lemma Rep_one_matrix[simp]: "Rep_matrix (one_matrix n) j i = (if (j = i & j < n) then 1 else 0)"
apply (simp add: one_matrix_def)
apply (simplesubst RepAbs_matrix)
-apply (rule exI[of _ n], simp add: split_if)+
-by (simp add: split_if)
+apply (rule exI[of _ n], simp add: if_split)+
+by (simp add: if_split)
lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _")
proof -
--- a/src/HOL/Metis_Examples/Message.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Metis_Examples/Message.thy Tue Feb 23 18:04:31 2016 +0100
@@ -460,7 +460,7 @@
by (intro equalityI lemma1 lemma2)
text{*Case analysis: either the message is secure, or it is not! Effective,
-but can cause subgoals to blow up! Use with @{text "split_if"}; apparently
+but can cause subgoals to blow up! Use with @{text "if_split"}; apparently
@{text "split_tac"} does not cope with patterns such as @{term"analz (insert
(Crypt K X) H)"} *}
lemma analz_Crypt_if [simp]:
--- a/src/HOL/Metis_Examples/Tarski.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy Tue Feb 23 18:04:31 2016 +0100
@@ -711,7 +711,7 @@
apply (erule exE)
-- {* define the lub for the interval as *}
apply (rule_tac x = "if S = {} then a else L" in exI)
-apply (simp (no_asm_simp) add: isLub_def split del: split_if)
+apply (simp (no_asm_simp) add: isLub_def split del: if_split)
apply (intro impI conjI)
-- {* @{text "(if S = {} then a else L) \<in> interval r a b"} *}
apply (simp add: CL_imp_PO L_in_interval)
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Feb 23 18:04:31 2016 +0100
@@ -50,7 +50,7 @@
"(fst (exec_instr i G hp stk vars Cl sig pc frs) = Some xcp)
= (\<exists>stk'. exec_instr i G hp stk vars Cl sig pc frs =
(Some xcp, hp, (stk', vars, Cl, sig, pc)#frs))"
- by (cases i, auto simp add: split_beta split: split_if_asm)
+ by (cases i, auto simp add: split_beta split: if_split_asm)
text \<open>
@@ -120,7 +120,7 @@
\<Longrightarrow> match G X pc et = [Xcpt X]"
apply (simp add: match_some_entry)
apply (induct et)
- apply (auto split: split_if_asm)
+ apply (auto split: if_split_asm)
done
text \<open>
@@ -257,7 +257,7 @@
(is "\<lbrakk> ?xcpt; ?wt; ?correct \<rbrakk> \<Longrightarrow> ?thesis")
proof -
note [simp] = split_beta raise_system_xcpt_def
- note [split] = split_if_asm option.split_asm
+ note [split] = if_split_asm option.split_asm
assume wt: ?wt ?correct
hence pre: "preallocated hp" by (simp add: correct_state_def)
@@ -348,7 +348,7 @@
have state':
"state' = (None, hp, ([xcp], loc, C, sig, handler)#frs)"
by (cases "ins!pc") (auto simp add: raise_system_xcpt_def split_beta
- split: split_if_asm) (* takes long! *)
+ split: if_split_asm) (* takes long! *)
let ?f' = "([xcp], loc, C, sig, handler)"
from eff
@@ -357,7 +357,7 @@
frame': "correct_frame G hp (ST',LT') maxl ins ?f'"
proof (cases "ins!pc")
case Return \<comment> "can't generate exceptions:"
- with xp' have False by (simp add: split_beta split: split_if_asm)
+ with xp' have False by (simp add: split_beta split: if_split_asm)
thus ?thesis ..
next
case New
@@ -393,7 +393,7 @@
case Getfield
with some_handler xp'
have xcp: "xcp = Addr (XcptRef NullPointer)"
- by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
+ by (simp add: raise_system_xcpt_def split_beta split: if_split_asm)
with prehp have "cname_of hp xcp = Xcpt NullPointer" ..
with Getfield some_handler phi_pc eff
obtain ST' LT' where
@@ -423,7 +423,7 @@
case Putfield
with some_handler xp'
have xcp: "xcp = Addr (XcptRef NullPointer)"
- by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
+ by (simp add: raise_system_xcpt_def split_beta split: if_split_asm)
with prehp have "cname_of hp xcp = Xcpt NullPointer" ..
with Putfield some_handler phi_pc eff
obtain ST' LT' where
@@ -453,7 +453,7 @@
case Checkcast
with some_handler xp'
have xcp: "xcp = Addr (XcptRef ClassCast)"
- by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
+ by (simp add: raise_system_xcpt_def split_beta split: if_split_asm)
with prehp have "cname_of hp xcp = Xcpt ClassCast" ..
with Checkcast some_handler phi_pc eff
obtain ST' LT' where
@@ -655,7 +655,7 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs2 wt_jvm_prog_def split: split_if_asm)
+apply (clarsimp simp add: defs2 wt_jvm_prog_def split: if_split_asm)
apply (blast intro: Cast_conf2)
done
@@ -670,7 +670,7 @@
fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs2 wt_jvm_prog_def split_beta
- split: option.split split_if_asm)
+ split: option.split if_split_asm)
apply (frule conf_widen)
apply assumption+
apply (drule conf_RefTD)
@@ -702,7 +702,7 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs2 split_beta split: option.split list.split split_if_asm)
+apply (clarsimp simp add: defs2 split_beta split: option.split list.split if_split_asm)
apply (frule conf_widen)
prefer 2
apply assumption
@@ -1328,7 +1328,7 @@
assumes wf: "wf_prog wf_mb \<Gamma>"
shows hconf_start: "\<Gamma> \<turnstile>h (start_heap \<Gamma>) \<surd>"
apply (unfold hconf_def start_heap_def)
- apply (auto simp add: fun_upd_apply blank_def oconf_def split: split_if_asm)
+ apply (auto simp add: fun_upd_apply blank_def oconf_def split: if_split_asm)
apply (simp add: fields_is_type
[OF _ wf [THEN wf_prog_ws_prog]
is_class_xcpt [OF wf [THEN wf_prog_ws_prog]]])+
--- a/src/HOL/MicroJava/BV/Effect.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy Tue Feb 23 18:04:31 2016 +0100
@@ -181,7 +181,7 @@
apply simp
apply simp
apply clarify
- apply (simp split: split_if_asm)
+ apply (simp split: if_split_asm)
apply (auto simp add: match_exception_entry_def)
done
@@ -189,7 +189,7 @@
"C \<in> set (match G X pc et) \<Longrightarrow> match_exception_table G C pc et \<noteq> None"
apply (induct et)
apply simp
- apply (simp split: split_if_asm)
+ apply (simp split: if_split_asm)
done
lemma xcpt_names_in_et:
--- a/src/HOL/MicroJava/BV/JType.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy Tue Feb 23 18:04:31 2016 +0100
@@ -202,7 +202,7 @@
thus ?thesis
apply (unfold sup_def subtype_def)
apply (cases s)
- apply (auto split: ty.split_asm ref_ty.split_asm split_if_asm)
+ apply (auto split: ty.split_asm ref_ty.split_asm if_split_asm)
done
qed
@@ -248,7 +248,7 @@
"subtype G a c" "subtype G b c" "sup G a b = OK d"
thus ?thesis
by (auto simp add: subtype_def sup_def
- split: ty.split_asm ref_ty.split_asm split_if_asm)
+ split: ty.split_asm ref_ty.split_asm if_split_asm)
qed
lemma sup_exists:
--- a/src/HOL/MicroJava/Comp/AuxLemmas.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy Tue Feb 23 18:04:31 2016 +0100
@@ -108,7 +108,7 @@
lemma map_of_map_prop:
"\<lbrakk>map_of (map f xs) k = Some v; \<forall>x \<in> set xs. P1 x; \<forall>x. P1 x \<longrightarrow> P2 (f x)\<rbrakk> \<Longrightarrow> P2 (k, v)"
- by (induct xs) (auto split: split_if_asm)
+ by (induct xs) (auto split: if_split_asm)
lemma map_of_map2: "\<forall>x \<in> set xs. (fst (f x)) = (fst x) \<Longrightarrow>
map_of (map f xs) a = map_option (\<lambda> b. (snd (f (a, b)))) (map_of xs a)"
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Tue Feb 23 18:04:31 2016 +0100
@@ -115,7 +115,7 @@
apply (drule_tac x=kr in spec)
apply (simp only: rev.simps)
apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = empty (rev kr[\<mapsto>]rev xs)([k'][\<mapsto>][a])")
- apply (simp split:split_if_asm)
+ apply (simp split:if_split_asm)
apply (simp add: map_upds_append [symmetric])
apply (case_tac ks)
apply auto
--- a/src/HOL/MicroJava/DFA/Abstract_BV.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/DFA/Abstract_BV.thy Tue Feb 23 18:04:31 2016 +0100
@@ -11,4 +11,4 @@
begin
end
-(*>*)
\ No newline at end of file
+(*>*)
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/DFA/LBVComplete.thy Tue Feb 23 18:04:31 2016 +0100
@@ -88,7 +88,7 @@
(is "?app ss1") and
sum: "(map snd [(p',t') \<leftarrow> ss1 . p' = pc+1] ++_f x) = ?s1"
(is "?map ss1 ++_f x = _" is "?sum ss1 = _")
- by (simp split: split_if_asm)
+ by (simp split: if_split_asm)
from app less
have "?app ss2" by (blast dest: trans_r lesub_step_typeD)
moreover {
@@ -159,7 +159,7 @@
have "?s1' = \<top> \<Longrightarrow> ?thesis" by simp
moreover {
assume "?s1' \<noteq> \<top>"
- with False have c: "s1 <=_r c!pc" by (simp add: wtc split: split_if_asm)
+ with False have c: "s1 <=_r c!pc" by (simp add: wtc split: if_split_asm)
with less have "s2 <=_r c!pc" ..
with False c have ?thesis by (simp add: wtc)
}
@@ -310,7 +310,7 @@
from suc_pc have pc: "pc < length \<phi>" by simp
with stable have "?wtc \<noteq> \<top>" by (rule stable_wtc)
with False have "?wtc = wti c pc (c!pc)"
- by (unfold wtc) (simp split: split_if_asm)
+ by (unfold wtc) (simp split: if_split_asm)
also from pc False have "c!pc = \<phi>!pc" ..
finally have "?wtc = wti c pc (\<phi>!pc)" .
also from stable suc_pc have "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" by (rule wti_less)
--- a/src/HOL/MicroJava/DFA/LBVCorrect.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/DFA/LBVCorrect.thy Tue Feb 23 18:04:31 2016 +0100
@@ -42,7 +42,7 @@
proof -
from all pc
have "wtc c (pc+1) (wtl (take (pc+1) ins) c 0 s0) \<noteq> T" by (rule wtl_all)
- with pc show ?thesis by (simp add: phi_def wtc split: split_if_asm)
+ with pc show ?thesis by (simp add: phi_def wtc split: if_split_asm)
qed
@@ -68,7 +68,7 @@
from wt_s1 pc c_None c_Some
have inst: "wtc c pc ?s1 = wti c pc (\<phi>!pc)"
- by (simp add: wtc split: split_if_asm)
+ by (simp add: wtc split: if_split_asm)
from pres cert s0 wtl pc have "?s1 \<in> A" by (rule wtl_pres)
with pc c_Some cert c_None
@@ -175,7 +175,7 @@
moreover
from wtl have "wtl (take 1 ins) c 0 s0 \<noteq> \<top>" by (rule wtl_take)
with 0 False
- have "s0 <=_r c!0" by (auto simp add: neq_Nil_conv wtc split: split_if_asm)
+ have "s0 <=_r c!0" by (auto simp add: neq_Nil_conv wtc split: if_split_asm)
ultimately
show ?thesis by simp
qed
--- a/src/HOL/MicroJava/DFA/LBVSpec.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/DFA/LBVSpec.thy Tue Feb 23 18:04:31 2016 +0100
@@ -161,7 +161,7 @@
assume "\<And>x. ?set ls \<Longrightarrow> ?merge ls x \<Longrightarrow> ?P ls" hence "?P ls" using set merge' .
moreover
from merge set
- have "pc' \<noteq> pc+1 \<longrightarrow> s' <=_r (c!pc')" by (simp add: l split: split_if_asm)
+ have "pc' \<noteq> pc+1 \<longrightarrow> s' <=_r (c!pc')" by (simp add: l split: if_split_asm)
ultimately
show "?P (l#ls)" by (simp add: l)
qed
@@ -223,7 +223,7 @@
proof -
from ss m have "\<forall>(pc',s') \<in> set ss. (pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc')"
by (rule merge_not_top)
- with x ss m show ?thesis by - (drule merge_def, auto split: split_if_asm)
+ with x ss m show ?thesis by - (drule merge_def, auto split: if_split_asm)
qed
subsection "wtl-inst-list"
--- a/src/HOL/MicroJava/DFA/Semilattices.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/DFA/Semilattices.thy Tue Feb 23 18:04:31 2016 +0100
@@ -11,4 +11,4 @@
begin
end
-(*>*)
\ No newline at end of file
+(*>*)
--- a/src/HOL/MicroJava/DFA/Typing_Framework_err.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/DFA/Typing_Framework_err.thy Tue Feb 23 18:04:31 2016 +0100
@@ -70,7 +70,7 @@
apply clarify
apply (erule allE, erule impE, assumption)
apply (case_tac s)
- apply (auto simp add: map_snd_def split: split_if_asm)
+ apply (auto simp add: map_snd_def split: if_split_asm)
done
@@ -150,7 +150,7 @@
apply simp
apply (drule in_errorD)
apply simp
-apply (simp add: map_snd_def split: split_if_asm)
+apply (simp add: map_snd_def split: if_split_asm)
apply fast
apply (drule in_errorD)
apply simp
--- a/src/HOL/MicroJava/J/Example.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/J/Example.thy Tue Feb 23 18:04:31 2016 +0100
@@ -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: split_if_asm simp add: map_of_Cons)
+apply (auto split add: if_split_asm simp add: map_of_Cons)
done
lemma not_class_subcls_class [elim!]: "(C, C) \<in> (subcls1 tprg)^+ ==> R"
@@ -402,7 +402,7 @@
lemmas e = NewCI eval_evals_exec.intros
-declare split_if [split del]
+declare if_split [split del]
declare init_vars_def [simp] c_hupd_def [simp] cast_ok_def [simp]
schematic_goal exec_test:
" [|new_Addr (heap (snd s0)) = (a, None)|] ==>
--- a/src/HOL/MicroJava/J/Exceptions.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/J/Exceptions.thy Tue Feb 23 18:04:31 2016 +0100
@@ -37,7 +37,7 @@
proof -
assume "raise_if b x None = Some xcp"
hence "xcp = Addr (XcptRef x)"
- by (simp add: raise_if_def split: split_if_asm)
+ by (simp add: raise_if_def split: if_split_asm)
moreover
assume "preallocated hp"
then obtain fs where "hp (XcptRef x) = Some (Xcpt x, fs)" ..
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Tue Feb 23 18:04:31 2016 +0100
@@ -171,7 +171,7 @@
-declare split_if [split del]
+declare if_split [split del]
declare fun_upd_apply [simp del]
declare fun_upd_same [simp]
declare wf_prog_ws_prog [simp]
--- a/src/HOL/MicroJava/J/State.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/J/State.thy Tue Feb 23 18:04:31 2016 +0100
@@ -84,7 +84,7 @@
hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))"
apply (drule sym)
apply (unfold new_Addr_def)
-apply (simp split: split_if_asm)
+apply (simp split: if_split_asm)
apply (erule LeastI)
done
@@ -164,7 +164,7 @@
lemma new_Addr_code_code [code]:
"new_Addr h = gen_new_Addr h 0"
-by(simp only: new_Addr_def gen_new_Addr_def split: split_if) simp
+by(simp only: new_Addr_def gen_new_Addr_def split: if_split) simp
lemma gen_new_Addr_code [code]:
"gen_new_Addr h n = (if h (Loc (nat_to_loc' n)) = None then (Loc (nat_to_loc' n), None) else gen_new_Addr h (Suc n))"
--- a/src/HOL/MicroJava/J/TypeRel.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy Tue Feb 23 18:04:31 2016 +0100
@@ -193,7 +193,7 @@
method (G,C) = (if C = Object then empty else method (G,D)) ++
map_of (map (\<lambda>(s,m). (s,(C,m))) ms)"
apply (unfold method_def)
-apply (simp split del: split_if)
+apply (simp split del: if_split)
apply (erule (1) class_rec_lemma [THEN trans])
apply auto
done
@@ -202,7 +202,7 @@
fields (G,C) =
map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))"
apply (unfold fields_def)
-apply (simp split del: split_if)
+apply (simp split del: if_split)
apply (erule (1) class_rec_lemma [THEN trans])
apply auto
done
--- a/src/HOL/MicroJava/J/WellForm.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy Tue Feb 23 18:04:31 2016 +0100
@@ -319,7 +319,7 @@
apply( subst fields_rec)
apply( assumption)
apply( assumption)
-apply( simp (no_asm) split del: split_if)
+apply( simp (no_asm) split del: if_split)
apply( rule ballI)
apply( simp (no_asm_simp) only: split_tupled_all)
apply( simp (no_asm))
--- a/src/HOL/MicroJava/J/WellType.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy Tue Feb 23 18:04:31 2016 +0100
@@ -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: split_if_asm)
+apply ( simp split add: if_split_asm)
apply ( drule field_fields)
apply ( drule (1) fields_is_type)
apply ( simp (no_asm_simp))
--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy Tue Feb 23 18:04:31 2016 +0100
@@ -155,7 +155,7 @@
apply (erule disjE, simp)
apply (elim exE conjE)
apply (erule allE, erule impE, assumption)
- apply (simp add: exec_all_def exec_d_def split: type_error.splits split_if_asm)
+ apply (simp add: exec_all_def exec_d_def split: type_error.splits if_split_asm)
apply (rule rtrancl_trans, assumption)
apply blast
done
@@ -165,4 +165,4 @@
show "G \<turnstile> s \<midarrow>jvm\<rightarrow> t" by blast
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy Tue Feb 23 18:04:31 2016 +0100
@@ -52,7 +52,7 @@
\<close>
lemma match_exception_table_in_et:
"match_exception_table G C pc et = Some pc' \<Longrightarrow> \<exists>e \<in> set et. pc' = fst (snd (snd e))"
- by (induct et) (auto split: split_if_asm)
+ by (induct et) (auto split: if_split_asm)
end
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy Tue Feb 23 18:04:31 2016 +0100
@@ -122,4 +122,4 @@
in
(xcpt', hp, (stk, vars, Cl, sig, pc)#frs))"
-end
\ No newline at end of file
+end
--- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy Tue Feb 23 18:04:31 2016 +0100
@@ -387,7 +387,7 @@
have "(\<Sum>j\<in>Basis. \<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j)) *\<^sub>R j) \<bullet> b
= (\<Sum>j\<in>Basis. if j = b then (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j))) else 0)"
using b
- by (auto simp add: algebra_simps inner_setsum_left inner_Basis split: split_if intro!: setsum.cong)
+ by (auto simp add: algebra_simps inner_setsum_left inner_Basis split: if_split intro!: setsum.cong)
also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> b)))"
using b by (simp add: setsum.delta)
also have "\<dots> = f x \<bullet> b"
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Feb 23 18:04:31 2016 +0100
@@ -222,7 +222,7 @@
proof cases
assume *: "{..n} \<subseteq> rl ` s"
with rl rl_bd[OF s] have rl_s: "rl ` s = {..n}"
- by (auto simp add: atMost_Suc subset_insert_iff split: split_if_asm)
+ by (auto simp add: atMost_Suc subset_insert_iff split: if_split_asm)
then have "\<not> inj_on rl s"
by (intro pigeonhole) simp
then obtain a b where ab: "a \<in> s" "b \<in> s" "rl a = rl b" "a \<noteq> b"
@@ -320,7 +320,7 @@
then have "\<And>i. i \<le> n \<Longrightarrow> enum i j = p'"
unfolding s_eq by auto
from this[of 0] this[of n] have "j \<notin> upd ` {..< n}"
- by (auto simp: enum_def fun_eq_iff split: split_if_asm)
+ by (auto simp: enum_def fun_eq_iff split: if_split_asm)
with upd \<open>j < n\<close> show False
by (auto simp: bij_betw_def)
qed
@@ -479,7 +479,7 @@
with enum_eq[of "Suc j"] enum_eq[of "Suc (Suc j)"]
have "u_s (Suc j) = u_t (Suc j)"
using s.enum_Suc[of "Suc j"] t.enum_Suc[of "Suc j"]
- by (auto simp: fun_eq_iff split: split_if_asm) }
+ by (auto simp: fun_eq_iff split: if_split_asm) }
then have "\<And>j. 0 < j \<Longrightarrow> j < n \<Longrightarrow> u_s j = u_t j"
by (auto simp: gr0_conv_Suc)
with \<open>n \<noteq> 0\<close> have "u_t 0 = u_s 0"
@@ -518,7 +518,7 @@
with enum_eq[of j] enum_eq[of "Suc j"]
have "u_s j = u_t j"
using s.enum_Suc[of j] t.enum_Suc[of j]
- by (auto simp: Suc fun_eq_iff split: split_if_asm) }
+ by (auto simp: Suc fun_eq_iff split: if_split_asm) }
then have "\<And>j. j < n' \<Longrightarrow> u_s j = u_t j"
by (auto simp: gr0_conv_Suc)
then have "u_t n' = u_s n'"
@@ -541,7 +541,7 @@
then interpret kuhn_simplex p n b u s .
from s_space \<open>a \<in> s\<close> out_eq_p[OF \<open>a \<in> s\<close>]
have "a \<in> (\<lambda>f x. if n \<le> x then p else f x) ` ({..< n} \<rightarrow>\<^sub>E {.. p})"
- by (auto simp: image_iff subset_eq Pi_iff split: split_if_asm
+ by (auto simp: image_iff subset_eq Pi_iff split: if_split_asm
intro!: bexI[of _ "restrict a {..< n}"]) }
then show "{s. ksimplex p n s} \<subseteq> Pow ((\<lambda>f x. if n \<le> x then p else f x) ` ({..< n} \<rightarrow>\<^sub>E {.. p}))"
by auto
@@ -577,7 +577,7 @@
by auto
then have "upd 0 = n"
using \<open>a n < p\<close> \<open>a = enum 0\<close> na[rule_format, of "enum 1"]
- by (auto simp: fun_eq_iff enum_Suc split: split_if_asm)
+ by (auto simp: fun_eq_iff enum_Suc split: if_split_asm)
then have "bij_betw upd (Suc ` {..< n}) {..< n}"
using upd
by (subst notIn_Un_bij_betw3[where b=0])
@@ -1006,7 +1006,7 @@
using i by (simp add: k \<open>Suc l = k\<close> i'_def)
then have False
using \<open>l < k\<close> \<open>k \<le> n\<close> \<open>Suc i' < n\<close>
- by (auto simp: t.enum_Suc enum_Suc l upd_inj fun_eq_iff split: split_if_asm)
+ by (auto simp: t.enum_Suc enum_Suc l upd_inj fun_eq_iff split: if_split_asm)
(metis Suc_lessD n_not_Suc_n upd_inj) }
with \<open>l < k\<close> have "Suc l < k"
by arith
@@ -1042,7 +1042,7 @@
using \<open>Suc l < k\<close> \<open>k \<le> n\<close> by (simp add: t.enum_Suc l t.upd_inj)
finally have "(u l = upd i' \<and> u (Suc l) = upd (Suc i')) \<or>
(u l = upd (Suc i') \<and> u (Suc l) = upd i')"
- using \<open>Suc i' < n\<close> by (auto simp: enum_Suc fun_eq_iff split: split_if_asm)
+ using \<open>Suc i' < n\<close> by (auto simp: enum_Suc fun_eq_iff split: if_split_asm)
then have "t = s \<or> t = b.enum ` {..n}"
proof (elim disjE conjE)
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Tue Feb 23 18:04:31 2016 +0100
@@ -188,7 +188,7 @@
apply (intro ballI)
apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>x. (x+1)/2)"
in differentiable_transform_within)
- apply (auto simp: dist_real_def joinpaths_def abs_if field_simps split: split_if_asm)
+ apply (auto simp: dist_real_def joinpaths_def abs_if field_simps split: if_split_asm)
apply (rule differentiable_chain_within derivative_intros | simp)+
apply (rule differentiable_subset)
apply (force simp: divide_simps)+
@@ -765,7 +765,7 @@
vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at z) =
2 *\<^sub>R vector_derivative g1 (at (z*2))" for z
apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g1(2*x))" and d = "\<bar>z - 1/2\<bar>"]])
- apply (simp_all add: dist_real_def abs_if split: split_if_asm)
+ apply (simp_all add: dist_real_def abs_if split: if_split_asm)
apply (rule vector_diff_chain_at [of "\<lambda>x. 2*x" 2 _ g1, simplified o_def])
apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
using s1
@@ -775,7 +775,7 @@
vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at z) =
2 *\<^sub>R vector_derivative g2 (at (z*2 - 1))" for z
apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g2 (2*x - 1))" and d = "\<bar>z - 1/2\<bar>"]])
- apply (simp_all add: dist_real_def abs_if split: split_if_asm)
+ apply (simp_all add: dist_real_def abs_if split: if_split_asm)
apply (rule vector_diff_chain_at [of "\<lambda>x. 2*x - 1" 2 _ g2, simplified o_def])
apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
using s2
@@ -826,7 +826,7 @@
vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2)) =
2 *\<^sub>R vector_derivative g1 (at z)" for z
apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g1(2*x))" and d = "\<bar>(z-1)/2\<bar>"]])
- apply (simp_all add: field_simps dist_real_def abs_if split: split_if_asm)
+ apply (simp_all add: field_simps dist_real_def abs_if split: if_split_asm)
apply (rule vector_diff_chain_at [of "\<lambda>x. x*2" 2 _ g1, simplified o_def])
using s1
apply (auto simp: vector_derivative_works has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
@@ -860,7 +860,7 @@
vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2+1/2)) =
2 *\<^sub>R vector_derivative g2 (at z)" for z
apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g2(2*x-1))" and d = "\<bar>z/2\<bar>"]])
- apply (simp_all add: field_simps dist_real_def abs_if split: split_if_asm)
+ apply (simp_all add: field_simps dist_real_def abs_if split: if_split_asm)
apply (rule vector_diff_chain_at [of "\<lambda>x. x*2-1" 2 _ g2, simplified o_def])
using s2
apply (auto simp: has_vector_derivative_def has_derivative_def bounded_linear_mult_left
@@ -926,7 +926,7 @@
vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a))"
unfolding shiftpath_def
apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g(a+x))" and d = "dist(1-a) x"]])
- apply (auto simp: field_simps dist_real_def abs_if split: split_if_asm)
+ apply (auto simp: field_simps dist_real_def abs_if split: if_split_asm)
apply (rule vector_diff_chain_at [of "\<lambda>x. x+a" 1 _ g, simplified o_def scaleR_one])
apply (intro derivative_eq_intros | simp)+
using g
@@ -939,7 +939,7 @@
vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a - 1))"
unfolding shiftpath_def
apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g(a+x-1))" and d = "dist (1-a) x"]])
- apply (auto simp: field_simps dist_real_def abs_if split: split_if_asm)
+ apply (auto simp: field_simps dist_real_def abs_if split: if_split_asm)
apply (rule vector_diff_chain_at [of "\<lambda>x. x+a-1" 1 _ g, simplified o_def scaleR_one])
apply (intro derivative_eq_intros | simp)+
using g
@@ -1000,7 +1000,7 @@
apply (auto simp: finite_imp_closed open_Diff shiftpath_shiftpath
vector_derivative_within_interior vector_derivative_works [symmetric])
apply (rule differentiable_transform_within [OF gx, of "min x (1-x)"])
- apply (auto simp: dist_real_def shiftpath_shiftpath abs_if split: split_if_asm)
+ apply (auto simp: dist_real_def shiftpath_shiftpath abs_if split: if_split_asm)
done
} note vd = this
have fi: "(f has_contour_integral i) (shiftpath (1 - a) (shiftpath a g))"
@@ -3071,7 +3071,7 @@
} note ind = this
have "contour_integral h f = contour_integral g f"
using ind [OF order_refl] N joins
- by (simp add: linked_paths_def pathstart_def pathfinish_def split: split_if_asm)
+ by (simp add: linked_paths_def pathstart_def pathfinish_def split: if_split_asm)
}
ultimately
have "path_image g \<subseteq> s \<and> path_image h \<subseteq> s \<and> (\<forall>f. f holomorphic_on s \<longrightarrow> contour_integral h f = contour_integral g f)"
@@ -3889,7 +3889,7 @@
}
then show ?thesis
using assms
- by (simp add: Groups.abs_if_class.abs_if winding_number_pos_meets split: split_if_asm)
+ by (simp add: Groups.abs_if_class.abs_if winding_number_pos_meets split: if_split_asm)
qed
lemma winding_number_less_1:
@@ -4455,7 +4455,7 @@
and ks: "k ` ({0..1} \<times> {0..1}) \<subseteq> s"
and k [simp]: "\<forall>x. k (0, x) = g x" "\<forall>x. k (1, x) = h x"
and ksf: "\<forall>t\<in>{0..1}. linked_paths atends g (\<lambda>x. k (t, x))"
- using hom pathsf by (auto simp: linked_paths_def homotopic_paths_def homotopic_loops_def homotopic_with_def split: split_if_asm)
+ using hom pathsf by (auto simp: linked_paths_def homotopic_paths_def homotopic_loops_def homotopic_with_def split: if_split_asm)
have ucontk: "uniformly_continuous_on ({0..1} \<times> {0..1}) k"
by (blast intro: compact_Times compact_uniformly_continuous [OF contk])
{ fix t::real assume t: "t \<in> {0..1}"
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Tue Feb 23 18:04:31 2016 +0100
@@ -608,7 +608,7 @@
lemma e_less_3: "exp 1 < (3::real)"
using e_approx_32
- by (simp add: abs_if split: split_if_asm)
+ by (simp add: abs_if split: if_split_asm)
lemma ln3_gt_1: "ln 3 > (1::real)"
by (metis e_less_3 exp_less_cancel_iff exp_ln_iff less_trans ln_exp)
@@ -1088,7 +1088,7 @@
then have "\<bar>Im w\<bar> < pi/2 \<longleftrightarrow> 0 < Re(exp w)"
apply (auto simp: Re_exp zero_less_mult_iff cos_gt_zero_pi)
using cos_lt_zero_pi [of "-(Im w)"] cos_lt_zero_pi [of "(Im w)"]
- apply (simp add: abs_if split: split_if_asm)
+ apply (simp add: abs_if split: if_split_asm)
apply (metis (no_types) cos_minus cos_pi_half eq_divide_eq_numeral1(1) eq_numeral_simps(4)
less_numeral_extra(3) linorder_neqE_linordered_idom minus_mult_minus minus_mult_right
mult_numeral_1_right)
@@ -1110,7 +1110,7 @@
then have "\<bar>Im w\<bar> \<le> pi/2 \<longleftrightarrow> 0 \<le> Re(exp w)"
apply (auto simp: Re_exp zero_le_mult_iff cos_ge_zero)
using cos_lt_zero_pi [of "- (Im w)"] cos_lt_zero_pi [of "(Im w)"] not_le
- apply (auto simp: abs_if split: split_if_asm)
+ apply (auto simp: abs_if split: if_split_asm)
done
}
then show ?thesis using assms
@@ -1176,7 +1176,7 @@
lemma cnj_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> cnj(Ln z) = Ln(cnj z)"
apply (cases "z=0", auto)
apply (rule exp_complex_eqI)
- apply (auto simp: abs_if split: split_if_asm)
+ apply (auto simp: abs_if split: if_split_asm)
using Im_Ln_less_pi Im_Ln_le_pi apply force
apply (metis complex_cnj_zero_iff diff_minus_eq_add diff_strict_mono minus_less_iff
mpi_less_Im_Ln mult.commute mult_2_right)
@@ -1186,7 +1186,7 @@
apply (cases "z=0", auto)
apply (rule exp_complex_eqI)
using mpi_less_Im_Ln [of z] mpi_less_Im_Ln [of "inverse z"]
- apply (auto simp: abs_if exp_minus split: split_if_asm)
+ apply (auto simp: abs_if exp_minus split: if_split_asm)
apply (metis Im_Ln_less_pi Im_Ln_le_pi add.commute add_mono_thms_linordered_field(3) inverse_nonzero_iff_nonzero mult_2)
done
@@ -1990,7 +1990,7 @@
using nz1 nz2 by auto
have "Im ((1 - \<i>*z) / (1 + \<i>*z)) = 0 \<Longrightarrow> 0 < Re ((1 - \<i>*z) / (1 + \<i>*z))"
apply (simp add: divide_complex_def)
- apply (simp add: divide_simps split: split_if_asm)
+ apply (simp add: divide_simps split: if_split_asm)
using assms
apply (auto simp: algebra_simps abs_square_less_1 [unfolded power2_eq_square])
done
@@ -2400,7 +2400,7 @@
also have "... = z"
apply (subst Complex_Transcendental.Ln_exp)
using assms
- apply (auto simp: abs_if simp del: eq_divide_eq_numeral1 split: split_if_asm)
+ apply (auto simp: abs_if simp del: eq_divide_eq_numeral1 split: if_split_asm)
done
finally show ?thesis .
qed
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Feb 23 18:04:31 2016 +0100
@@ -3481,7 +3481,7 @@
by (auto intro!: exI[of _ "(a + b) / 2"] simp: box_def)
then show ?thesis
using interior_rel_interior_gen[of "cbox a b", symmetric]
- by (simp split: split_if_asm del: box_real add: box_real[symmetric] interior_cbox)
+ by (simp split: if_split_asm del: box_real add: box_real[symmetric] interior_cbox)
qed
lemma rel_interior_real_semiline:
@@ -3491,7 +3491,7 @@
have *: "{a<..} \<noteq> {}"
unfolding set_eq_iff by (auto intro!: exI[of _ "a + 1"])
then show ?thesis using interior_real_semiline interior_rel_interior_gen[of "{a..}"]
- by (auto split: split_if_asm)
+ by (auto split: if_split_asm)
qed
subsubsection \<open>Relative open sets\<close>
@@ -6583,7 +6583,7 @@
shows "norm (x - a) < norm (b - a)"
proof -
obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 < u" "u < 1" "a \<noteq> b"
- using assms by (auto simp add: open_segment_eq split: split_if_asm)
+ using assms by (auto simp add: open_segment_eq split: if_split_asm)
then show "norm (x - a) < norm (b - a)"
apply clarify
apply (auto simp: algebra_simps)
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Feb 23 18:04:31 2016 +0100
@@ -903,7 +903,7 @@
unfolding y_def
by (rule cSup_upper) simp
thus False using \<open>d > 0\<close> \<open>y < b\<close>
- by (simp add: d'_def min_def split: split_if_asm)
+ by (simp add: d'_def min_def split: if_split_asm)
qed
} moreover {
assume "a = y"
@@ -2691,7 +2691,7 @@
from fx[OF \<open>x \<in> X\<close> \<open>y \<in> Y\<close>, unfolded has_derivative_within, THEN conjunct2, THEN tendstoD, OF \<open>0 < e\<close>]
have "\<forall>\<^sub>F x' in at x within X. ?le x'"
by eventually_elim
- (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps split: split_if_asm)
+ (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps split: if_split_asm)
then have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. ?le x'"
by (rule eventually_at_Pair_within_TimesI1)
(simp add: blinfun.bilinear_simps)
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Feb 23 18:04:31 2016 +0100
@@ -155,7 +155,7 @@
"Basis = {1, ii}"
instance
- by standard (auto simp add: Basis_complex_def intro: complex_eqI split: split_if_asm)
+ by standard (auto simp add: Basis_complex_def intro: complex_eqI split: if_split_asm)
end
@@ -192,7 +192,7 @@
assume "u \<in> Basis" and "v \<in> Basis"
thus "inner u v = (if u = v then 1 else 0)"
unfolding Basis_prod_def inner_prod_def
- by (auto simp add: inner_Basis split: split_if_asm)
+ by (auto simp add: inner_Basis split: if_split_asm)
next
fix x :: "'a \<times> 'b"
show "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> x = 0"
--- a/src/HOL/Multivariate_Analysis/Gamma.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Gamma.thy Tue Feb 23 18:04:31 2016 +0100
@@ -2218,7 +2218,7 @@
lemma rGamma_reflection_complex:
"rGamma z * rGamma (1 - z :: complex) = sin (of_real pi * z) / of_real pi"
using Gamma_reflection_complex[of z]
- by (simp add: Gamma_def divide_simps split: split_if_asm)
+ by (simp add: Gamma_def divide_simps split: if_split_asm)
lemma rGamma_reflection_complex':
"rGamma z * rGamma (- z :: complex) = -z * sin (of_real pi * z) / of_real pi"
--- a/src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy Tue Feb 23 18:04:31 2016 +0100
@@ -167,7 +167,7 @@
note A[OF this]
also have "complex_of_real (-x + -y) = - complex_of_real (x + y)" by simp
also from xy assms have "... powr a = (-1) powr -a * of_real (x + y) powr a"
- by (subst powr_neg_real_complex) (simp add: abs_real_def split: split_if_asm)
+ by (subst powr_neg_real_complex) (simp add: abs_real_def split: if_split_asm)
also {
fix n :: nat
from y have "(a gchoose n) * of_real (-x) ^ n * of_real (-y) powr (a - of_nat n) =
@@ -251,4 +251,4 @@
"\<bar>z\<bar> < 1 \<Longrightarrow> (\<lambda>n. ((1/2) gchoose n) * z ^ n) sums sqrt (1 + z)"
using gen_binomial_real[of z "1/2"] by (simp add: powr_half_sqrt)
-end
\ No newline at end of file
+end
--- a/src/HOL/Multivariate_Analysis/Integral_Test.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Integral_Test.thy Tue Feb 23 18:04:31 2016 +0100
@@ -110,4 +110,4 @@
end
-end
\ No newline at end of file
+end
--- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Feb 23 18:04:31 2016 +0100
@@ -640,7 +640,7 @@
shows "content s = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. \<exists>v. \<forall>x \<in> s. x \<bullet> i = v)" (is "_ = ?rhs")
proof safe
assume "content s = 0" then show ?rhs
- apply (clarsimp simp: ex_in_conv content_def split: split_if_asm)
+ apply (clarsimp simp: ex_in_conv content_def split: if_split_asm)
apply (rule_tac x=a in bexI)
apply (rule_tac x="interval_lowerbound s \<bullet> a" in exI)
apply (clarsimp simp: interval_upperbound_def interval_lowerbound_def)
@@ -3213,7 +3213,7 @@
by (rule setsum.mono_neutral_left) auto
let ?M1 = "{(x, kk \<inter> {x. x\<bullet>k \<le> c}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}"
have d1_fine: "d1 fine ?M1"
- by (force intro: fineI dest: fineD[OF p(2)] simp add: split: split_if_asm)
+ by (force intro: fineI dest: fineD[OF p(2)] simp add: split: if_split_asm)
have "norm ((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) < e/2"
proof (rule d1norm [OF tagged_division_ofI d1_fine])
show "finite ?M1"
@@ -3252,7 +3252,7 @@
moreover
let ?M2 = "{(x,kk \<inter> {x. x\<bullet>k \<ge> c}) |x kk. (x,kk) \<in> p \<and> kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}"
have d2_fine: "d2 fine ?M2"
- by (force intro: fineI dest: fineD[OF p(2)] simp add: split: split_if_asm)
+ by (force intro: fineI dest: fineD[OF p(2)] simp add: split: if_split_asm)
have "norm ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j) < e/2"
proof (rule d2norm [OF tagged_division_ofI d2_fine])
show "finite ?M2"
@@ -3749,10 +3749,10 @@
apply (rule bexI[OF _ \<open>l \<in> d\<close>])
using as(1-3,5) fstx
unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as
- apply (auto split: split_if_asm)
+ apply (auto split: if_split_asm)
done
show "snd x < b \<bullet> fst x"
- using as(2) \<open>c < b\<bullet>k\<close> by (auto split: split_if_asm)
+ using as(2) \<open>c < b\<bullet>k\<close> by (auto split: if_split_asm)
qed
show ?t2
unfolding division_points_def interval_split[OF k, of a b]
@@ -3780,10 +3780,10 @@
apply (rule bexI[OF _ \<open>l \<in> d\<close>])
using as(1-3,5) fstx
unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as
- apply (auto split: split_if_asm)
+ apply (auto split: if_split_asm)
done
show "a \<bullet> fst x < snd x"
- using as(1) \<open>a\<bullet>k < c\<close> by (auto split: split_if_asm)
+ using as(1) \<open>a\<bullet>k < c\<close> by (auto split: if_split_asm)
qed
qed
@@ -4368,7 +4368,7 @@
then show False
unfolding inner_simps
using rsum_component_le[OF p(1) le]
- by (simp add: abs_real_def split: split_if_asm)
+ by (simp add: abs_real_def split: if_split_asm)
qed
show ?thesis
proof (cases "\<exists>a b. s = cbox a b")
@@ -4391,7 +4391,7 @@
guess w1 using B(2)[OF ab(1)] .. note w1=conjunctD2[OF this]
guess w2 using B(4)[OF ab(2)] .. note w2=conjunctD2[OF this]
have *: "\<And>w1 w2 j i::real .\<bar>w1 - i\<bar> < (i - j) / 3 \<Longrightarrow> \<bar>w2 - j\<bar> < (i - j) / 3 \<Longrightarrow> w1 \<le> w2 \<Longrightarrow> False"
- by (simp add: abs_real_def split: split_if_asm)
+ by (simp add: abs_real_def split: if_split_asm)
note le_less_trans[OF Basis_le_norm[OF k]]
note this[OF w1(2)] this[OF w2(2)]
moreover
@@ -6086,7 +6086,7 @@
def Dg \<equiv> "\<lambda>n s. if n < p then (-1)^n * (b - s)^(p - 1 - n) / fact (p - 1 - n) else 0"
have g0: "Dg 0 = g"
using \<open>p > 0\<close>
- by (auto simp add: Dg_def divide_simps g_def split: split_if_asm)
+ by (auto simp add: Dg_def divide_simps g_def split: if_split_asm)
{
fix m
assume "p > Suc m"
@@ -8476,7 +8476,7 @@
shows "(f has_integral y) s \<longleftrightarrow> (f has_integral y) t"
unfolding has_integral_restrict_univ[symmetric,of f]
apply (rule has_integral_spike_eq[OF assms])
- by (auto split: split_if_asm)
+ by (auto split: if_split_asm)
lemma has_integral_spike_set[dest]:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
@@ -8998,7 +8998,7 @@
\<bar>ga - i\<bar> < e / 3 \<and> \<bar>gc - i\<bar> < e / 3 \<and> \<bar>ha - j\<bar> < e / 3 \<and>
\<bar>hc - j\<bar> < e / 3 \<and> \<bar>i - j\<bar> < e / 3 \<and> ga \<le> fa \<and> fa \<le> ha \<and> gc \<le> fc \<and> fc \<le> hc \<Longrightarrow>
\<bar>fa - fc\<bar> < e"
- by (simp add: abs_real_def split: split_if_asm)
+ by (simp add: abs_real_def split: if_split_asm)
show "norm (integral (cbox a b) (\<lambda>x. if x \<in> s then f x else 0) - integral (cbox c d)
(\<lambda>x. if x \<in> s then f x else 0)) < e"
unfolding real_norm_def
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Tue Feb 23 18:04:31 2016 +0100
@@ -504,7 +504,7 @@
show ?thesis
using assms
apply (simp add: arc_def simple_path_def path_join, clarify)
- apply (simp add: joinpaths_def split: split_if_asm)
+ apply (simp add: joinpaths_def split: if_split_asm)
apply (force dest: inj_onD [OF injg1])
apply (metis *)
apply (metis **)
@@ -542,7 +542,7 @@
show ?thesis
apply (simp add: arc_def inj_on_def)
apply (clarsimp simp add: arc_imp_path assms path_join)
- apply (simp add: joinpaths_def split: split_if_asm)
+ apply (simp add: joinpaths_def split: if_split_asm)
apply (force dest: inj_onD [OF injg1])
apply (metis *)
apply (metis *)
@@ -642,7 +642,7 @@
then have "x = y \<or> x = u \<and> y = v \<or> x = v \<and> y = u"
using sim [of "(x-u)/(v-u)" "(y-u)/(v-u)"] p
by (auto simp: closed_segment_real_eq image_affinity_atLeastAtMost divide_simps
- split: split_if_asm)
+ split: if_split_asm)
} moreover
have "path(subpath u v g) \<and> u\<noteq>v"
using sim [of "1/3" "2/3"] p
@@ -678,7 +678,7 @@
then have "x = y"
using sim [of "(x-u)/(v-u)" "(y-u)/(v-u)"] p
by (force simp add: inj_on_def closed_segment_real_eq image_affinity_atLeastAtMost divide_simps
- split: split_if_asm)
+ split: if_split_asm)
} moreover
have "path(subpath u v g) \<and> u\<noteq>v"
using sim [of "1/3" "2/3"] p
@@ -807,7 +807,7 @@
apply (auto simp: closed_segment_eq_real_ivl pathstart_def pathfinish_def subpath_def)
apply (rename_tac y)
apply (drule_tac x="y/u" in spec)
- apply (auto split: split_if_asm)
+ apply (auto split: if_split_asm)
done
qed
@@ -1530,7 +1530,7 @@
unfolding image_iff
apply (rule_tac x=x in bexI)
unfolding mem_Collect_eq
- apply (auto split: split_if_asm)
+ apply (auto split: if_split_asm)
done
have "continuous_on (- {0}) (\<lambda>x::'a. 1 / norm x)"
by (auto intro!: continuous_intros)
--- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Tue Feb 23 18:04:31 2016 +0100
@@ -512,6 +512,7 @@
unfolding uniformly_convergent_on_def
by (blast dest: bounded_linear_uniform_limit_intros(13))
+
subsection\<open>Power series and uniform convergence\<close>
proposition powser_uniformly_convergent:
@@ -554,4 +555,5 @@
apply (rule continuous_on_cong [THEN iffD1, OF refl _ powser_continuous_suminf [OF r]])
using sm sums_unique by fastforce
-end
\ No newline at end of file
+end
+
--- a/src/HOL/Multivariate_Analysis/ex/Approximations.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/ex/Approximations.thy Tue Feb 23 18:04:31 2016 +0100
@@ -333,7 +333,7 @@
by (subst (asm) hsum_63) simp
have "ln (64::real) = real (6::nat) * ln 2" by (subst ln_realpow[symmetric]) simp_all
hence "ln (real_of_nat (Suc 63)) \<in> {4.158883083293<..<4.158883083367}" using ln_2_64
- by (simp add: abs_real_def split: split_if_asm)
+ by (simp add: abs_real_def split: if_split_asm)
from euler_mascheroni_bounds'[OF _ this]
have "(euler_mascheroni :: real) \<in> {l<..<u}"
by (simp add: hsum_63 del: greaterThanLessThan_iff) (simp only: l_def u_def)
--- a/src/HOL/NSA/HyperDef.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/NSA/HyperDef.thy Tue Feb 23 18:04:31 2016 +0100
@@ -276,7 +276,7 @@
subsection\<open>Absolute Value Function for the Hyperreals\<close>
lemma hrabs_add_less: "[| \<bar>x\<bar> < r; \<bar>y\<bar> < s |] ==> \<bar>x + y\<bar> < r + (s::hypreal)"
-by (simp add: abs_if split: split_if_asm)
+by (simp add: abs_if split: if_split_asm)
lemma hrabs_less_gt_zero: "\<bar>x\<bar> < r ==> (0::hypreal) < r"
by (blast intro!: order_le_less_trans abs_ge_zero)
@@ -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: split_if_asm)
+by (simp add: abs_if split add: if_split_asm)
subsection\<open>Embedding the Naturals into the Hyperreals\<close>
--- a/src/HOL/NanoJava/OpSem.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/NanoJava/OpSem.thy Tue Feb 23 18:04:31 2016 +0100
@@ -109,4 +109,4 @@
apply (fast elim: exec_elim_cases intro: exec_eval.Impl)
done
-end
\ No newline at end of file
+end
--- a/src/HOL/NanoJava/TypeRel.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy Tue Feb 23 18:04:31 2016 +0100
@@ -47,7 +47,7 @@
"subcls1 =
(SIGMA C: {C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})"
apply (unfold subcls1_def is_class_def)
-apply (auto split:split_if_asm)
+apply (auto split:if_split_asm)
done
lemma finite_subcls1: "finite subcls1"
--- a/src/HOL/Nominal/Examples/Compile.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Nominal/Examples/Compile.thy Tue Feb 23 18:04:31 2016 +0100
@@ -253,4 +253,4 @@
| "trans_type (\<tau>1\<rightarrow>\<tau>2) = (trans_type \<tau>1)\<rightarrow>(trans_type \<tau>2)"
by (rule TrueI)+
-end
\ No newline at end of file
+end
--- a/src/HOL/Nominal/Examples/Pattern.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Nominal/Examples/Pattern.thy Tue Feb 23 18:04:31 2016 +0100
@@ -640,7 +640,7 @@
apply simp
apply (simp add: split_paired_all supp_eqvt)
apply (drule perm_mem_left)
- apply (simp add: calc_atm split: split_if_asm)
+ apply (simp add: calc_atm split: if_split_asm)
apply (auto dest: perm_mem_right)
done
qed
--- a/src/HOL/Nominal/Examples/SN.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Nominal/Examples/SN.thy Tue Feb 23 18:04:31 2016 +0100
@@ -578,4 +578,4 @@
ultimately show "SN(t)" by (simp add: CR1_def)
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/Nominal/Examples/Standardization.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Nominal/Examples/Standardization.thy Tue Feb 23 18:04:31 2016 +0100
@@ -370,7 +370,7 @@
(\<exists>t u us. x \<sharp> r \<longrightarrow> r = (Lam [x].t) \<and> rs = u # us \<and> s = t[x::=u] \<degree>\<degree> us)"
apply (nominal_induct u \<equiv> "r \<degree>\<degree> rs" s avoiding: x r rs rule: beta.strong_induct)
apply (simp add: App_eq_foldl_conv)
- apply (split split_if_asm)
+ apply (split if_split_asm)
apply simp
apply blast
apply simp
@@ -391,12 +391,12 @@
apply (rule refl)
apply (simp add: abs_fresh fresh_atm fresh_left calc_atm subst_rename)
apply (drule App_eq_foldl_conv [THEN iffD1])
- apply (split split_if_asm)
+ apply (split if_split_asm)
apply simp
apply blast
apply (force intro!: disjI1 [THEN append_step1I] simp add: fresh_list_append)
apply (drule App_eq_foldl_conv [THEN iffD1])
- apply (split split_if_asm)
+ apply (split if_split_asm)
apply simp
apply blast
apply (clarify, auto 0 3 intro!: exI intro: append_step1I)
--- a/src/HOL/Nominal/Examples/Support.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Nominal/Examples/Support.thy Tue Feb 23 18:04:31 2016 +0100
@@ -143,4 +143,4 @@
text {* Moral: support is a sublte notion. *}
-end
\ No newline at end of file
+end
--- a/src/HOL/Nominal/Examples/VC_Condition.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Nominal/Examples/VC_Condition.thy Tue Feb 23 18:04:31 2016 +0100
@@ -207,4 +207,4 @@
is in general an unsound reasoning principle.
*}
-end
\ No newline at end of file
+end
--- a/src/HOL/Nominal/Examples/Weakening.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Nominal/Examples/Weakening.thy Tue Feb 23 18:04:31 2016 +0100
@@ -204,4 +204,4 @@
and weakening_version2, and imagine you are proving something more substantial
than the weakening lemma. *}
-end
\ No newline at end of file
+end
--- a/src/HOL/NthRoot.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/NthRoot.thy Tue Feb 23 18:04:31 2016 +0100
@@ -101,7 +101,7 @@
have x: "\<And>a b :: real. (0 < b \<and> a < 0) \<Longrightarrow> \<not> a > b" by auto
fix a b :: real assume "0 < n" "sgn a * \<bar>a\<bar> ^ n < sgn b * \<bar>b\<bar> ^ n" then show "a < b"
using power_less_imp_less_base[of a n b] power_less_imp_less_base[of "-b" n "-a"]
- by (simp add: sgn_real_def x [of "a ^ n" "- ((- b) ^ n)"] split: split_if_asm)
+ by (simp add: sgn_real_def x [of "a ^ n" "- ((- b) ^ n)"] split: if_split_asm)
qed
lemma real_root_gt_zero: "\<lbrakk>0 < n; 0 < x\<rbrakk> \<Longrightarrow> 0 < root n x"
@@ -122,13 +122,13 @@
by (auto split: split_root simp: sgn_real_def)
lemma odd_real_root_pow: "odd n \<Longrightarrow> root n x ^ n = x"
- using sgn_power_root[of n x] by (simp add: odd_pos sgn_real_def split: split_if_asm)
+ using sgn_power_root[of n x] by (simp add: odd_pos sgn_real_def split: if_split_asm)
lemma real_root_power_cancel: "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> root n (x ^ n) = x"
using root_sgn_power[of n x] by (auto simp add: le_less power_0_left)
lemma odd_real_root_power_cancel: "odd n \<Longrightarrow> root n (x ^ n) = x"
- using root_sgn_power[of n x] by (simp add: odd_pos sgn_real_def power_0_left split: split_if_asm)
+ using root_sgn_power[of n x] by (simp add: odd_pos sgn_real_def power_0_left split: if_split_asm)
lemma real_root_pos_unique: "\<lbrakk>0 < n; 0 \<le> y; y ^ n = x\<rbrakk> \<Longrightarrow> root n x = y"
using root_sgn_power[of n y] by (auto simp add: le_less power_0_left)
--- a/src/HOL/Partial_Function.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Partial_Function.thy Tue Feb 23 18:04:31 2016 +0100
@@ -304,7 +304,7 @@
and P [rule_format]: "\<forall>f\<in>A. \<forall>x. f x \<noteq> c \<longrightarrow> P x (f x)"
and defined: "fun_lub (flat_lub c) A x \<noteq> c"
from defined obtain f where f: "f \<in> A" "f x \<noteq> c"
- by(auto simp add: fun_lub_def flat_lub_def split: split_if_asm)
+ by(auto simp add: fun_lub_def flat_lub_def split: if_split_asm)
hence "P x (f x)" by(rule P)
moreover from chain f have "\<forall>f' \<in> A. f' x = c \<or> f' x = f x"
by(auto 4 4 simp add: Complete_Partial_Order.chain_def flat_ord_def fun_ord_def)
--- a/src/HOL/Predicate.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Predicate.thy Tue Feb 23 18:04:31 2016 +0100
@@ -346,11 +346,11 @@
lemma not_predE: "eval (not_pred (Pred (\<lambda>u. P))) x \<Longrightarrow> (\<not> P \<Longrightarrow> thesis) \<Longrightarrow> thesis"
unfolding not_pred_eq
- by (auto split: split_if_asm elim: botE)
+ by (auto split: if_split_asm elim: botE)
lemma not_predE': "eval (not_pred P) x \<Longrightarrow> (\<not> eval P x \<Longrightarrow> thesis) \<Longrightarrow> thesis"
unfolding not_pred_eq
- by (auto split: split_if_asm elim: botE)
+ by (auto split: if_split_asm elim: botE)
lemma "f () = False \<or> f () = True"
by simp
--- a/src/HOL/Predicate_Compile.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Predicate_Compile.thy Tue Feb 23 18:04:31 2016 +0100
@@ -59,7 +59,7 @@
lemma contains_predE:
assumes "Predicate.eval (contains_pred A x) y"
obtains "contains A x"
-using assms by(simp add: contains_pred_def contains_def split: split_if_asm)
+using assms by(simp add: contains_pred_def contains_def split: if_split_asm)
lemma contains_pred_eq: "contains_pred \<equiv> \<lambda>A x. Predicate.Pred (\<lambda>y. contains A x)"
by(rule eq_reflection)(auto simp add: contains_pred_def fun_eq_iff contains_def intro: pred_eqI)
--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Tue Feb 23 18:04:31 2016 +0100
@@ -171,4 +171,4 @@
hide_const a b
-end
\ No newline at end of file
+end
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Tue Feb 23 18:04:31 2016 +0100
@@ -88,4 +88,4 @@
lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2)
-end
\ No newline at end of file
+end
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Tue Feb 23 18:04:31 2016 +0100
@@ -154,4 +154,4 @@
quickcheck[tester = prolog, iterations = 1, expect = counterexample]
oops
-end
\ No newline at end of file
+end
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy Tue Feb 23 18:04:31 2016 +0100
@@ -63,4 +63,4 @@
oops
-end
\ No newline at end of file
+end
--- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy Tue Feb 23 18:04:31 2016 +0100
@@ -27,4 +27,4 @@
quickcheck[tester = prolog, expect = counterexample]
oops
-end
\ No newline at end of file
+end
--- a/src/HOL/Probability/Binary_Product_Measure.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Tue Feb 23 18:04:31 2016 +0100
@@ -169,7 +169,7 @@
have "Pair x -` A = (if x \<in> space M1 then Pair x -` A \<inter> space M2 else {})"
using A[THEN sets.sets_into_space] by (auto simp: space_pair_measure)
also have "\<dots> \<in> sets M2"
- using A by (auto simp add: measurable_Pair1' intro!: measurable_sets split: split_if_asm)
+ using A by (auto simp add: measurable_Pair1' intro!: measurable_sets split: if_split_asm)
finally show ?thesis .
qed
@@ -181,7 +181,7 @@
have "(\<lambda>x. (x, y)) -` A = (if y \<in> space M2 then (\<lambda>x. (x, y)) -` A \<inter> space M1 else {})"
using A[THEN sets.sets_into_space] by (auto simp: space_pair_measure)
also have "\<dots> \<in> sets M1"
- using A by (auto simp add: measurable_Pair2' intro!: measurable_sets split: split_if_asm)
+ using A by (auto simp add: measurable_Pair2' intro!: measurable_sets split: if_split_asm)
finally show ?thesis .
qed
--- a/src/HOL/Probability/Bochner_Integration.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy Tue Feb 23 18:04:31 2016 +0100
@@ -165,7 +165,7 @@
shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator (B x) (g x)) = (\<Sum>x\<in>{x\<in>A. g x \<in> B x}. f x)"
and setsum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator (B x) (g x) * f x) = (\<Sum>x\<in>{x\<in>A. g x \<in> B x}. f x)"
unfolding indicator_def
- using assms by (auto intro!: setsum.mono_neutral_cong_right split: split_if_asm)
+ using assms by (auto intro!: setsum.mono_neutral_cong_right split: if_split_asm)
lemma borel_measurable_induct_real[consumes 2, case_names set mult add seq]:
fixes P :: "('a \<Rightarrow> real) \<Rightarrow> bool"
--- a/src/HOL/Probability/Borel_Space.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Tue Feb 23 18:04:31 2016 +0100
@@ -970,7 +970,7 @@
fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis"
then have "i \<in> Basis" by auto
then have *: "{x::'a. x\<bullet>i \<le> a} = (\<Union>k::nat. {.. (\<Sum>n\<in>Basis. (if n = i then a else real k)*\<^sub>R n)})"
- proof (safe, simp_all add: eucl_le[where 'a='a] split: split_if_asm)
+ proof (safe, simp_all add: eucl_le[where 'a='a] split: if_split_asm)
fix x :: 'a
from real_arch_simple[of "Max ((\<lambda>i. x\<bullet>i)`Basis)"] guess k::nat ..
then have "\<And>i. i \<in> Basis \<Longrightarrow> x\<bullet>i \<le> real k"
@@ -991,7 +991,7 @@
have "{x::'a. x\<bullet>i \<le> a} = UNIV - {x::'a. a < x\<bullet>i}" by auto
also have *: "{x::'a. a < x\<bullet>i} =
(\<Union>k::nat. {x. (\<Sum>n\<in>Basis. (if n = i then a else -real k) *\<^sub>R n) <e x})" using i
- proof (safe, simp_all add: eucl_less_def split: split_if_asm)
+ proof (safe, simp_all add: eucl_less_def split: if_split_asm)
fix x :: 'a
from reals_Archimedean2[of "Max ((\<lambda>i. -x\<bullet>i)`Basis)"]
guess k::nat .. note k = this
@@ -1017,7 +1017,7 @@
then have i: "i \<in> Basis" by auto
have "{x::'a. a \<le> x\<bullet>i} = UNIV - {x::'a. x\<bullet>i < a}" by auto
also have *: "{x::'a. x\<bullet>i < a} = (\<Union>k::nat. {x. x <e (\<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n)})" using \<open>i\<in> Basis\<close>
- proof (safe, simp_all add: eucl_less_def split: split_if_asm)
+ proof (safe, simp_all add: eucl_less_def split: if_split_asm)
fix x :: 'a
from reals_Archimedean2[of "Max ((\<lambda>i. x\<bullet>i)`Basis)"]
guess k::nat .. note k = this
@@ -1454,7 +1454,7 @@
{ fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule: ereal2_cases) auto }
note * = this
from assms show ?thesis
- by (subst *) (simp del: space_borel split del: split_if)
+ by (subst *) (simp del: space_borel split del: if_split)
qed
lemma borel_measurable_ereal_iff:
--- a/src/HOL/Probability/Caratheodory.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Caratheodory.thy Tue Feb 23 18:04:31 2016 +0100
@@ -713,7 +713,7 @@
then have "disjoint_family F"
using F'_disj by (auto simp: disjoint_family_on_def)
moreover from F' have "(\<Union>i. F i) = \<Union>C"
- by (auto simp add: F_def split: split_if_asm) blast
+ by (auto simp add: F_def split: if_split_asm) blast
moreover have sets_F: "\<And>i. F i \<in> M"
using F' sets_C by (auto simp: F_def)
moreover note sets_C
--- a/src/HOL/Probability/Complete_Measure.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Complete_Measure.thy Tue Feb 23 18:04:31 2016 +0100
@@ -113,15 +113,15 @@
and main_part_null_part_Un[simp]: "main_part M S \<union> null_part M S = S"
and main_part_null_part_Int[simp]: "main_part M S \<inter> null_part M S = {}"
using split_completion[OF assms]
- by (auto simp: split_completion_def split: split_if_asm)
+ by (auto simp: split_completion_def split: if_split_asm)
lemma main_part[simp]: "S \<in> sets M \<Longrightarrow> main_part M S = S"
using split_completion[of S M]
- by (auto simp: split_completion_def split: split_if_asm)
+ by (auto simp: split_completion_def split: if_split_asm)
lemma null_part:
assumes "S \<in> sets (completion M)" shows "\<exists>N. N\<in>null_sets M \<and> null_part M S \<subseteq> N"
- using split_completion[OF assms] by (auto simp: split_completion_def split: split_if_asm)
+ using split_completion[OF assms] by (auto simp: split_completion_def split: if_split_asm)
lemma null_part_sets[intro, simp]:
assumes "S \<in> sets M" shows "null_part M S \<in> sets M" "emeasure M (null_part M S) = 0"
@@ -202,7 +202,7 @@
shows "emeasure (completion M) (S \<union> T) = emeasure M (main_part M S \<union> main_part M T)"
proof (subst emeasure_completion)
have UN: "(\<Union>i. binary (main_part M S) (main_part M T) i) = (\<Union>i. main_part M (binary S T i))"
- unfolding binary_def by (auto split: split_if_asm)
+ unfolding binary_def by (auto split: if_split_asm)
show "emeasure M (main_part M (S \<union> T)) = emeasure M (main_part M S \<union> main_part M T)"
using emeasure_main_part_UN[of "binary S T" M] assms
by (simp add: range_binary_eq, simp add: Un_range_binary UN)
@@ -238,7 +238,7 @@
(if x \<in> ?N then ?F undefined \<union> ?N
else if f x = undefined then ?F (f x) \<union> ?N
else ?F (f x) - ?N)"
- using N(2) sets.sets_into_space by (auto split: split_if_asm simp: null_sets_def)
+ using N(2) sets.sets_into_space by (auto split: if_split_asm simp: null_sets_def)
moreover { fix y have "?F y \<union> ?N \<in> sets M"
proof cases
assume y: "y \<in> f`space M"
--- a/src/HOL/Probability/Discrete_Topology.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Discrete_Topology.thy Tue Feb 23 18:04:31 2016 +0100
@@ -34,7 +34,7 @@
proof
fix X::"nat\<Rightarrow>'a discrete" assume "Cauchy X"
hence "\<exists>n. \<forall>m\<ge>n. X n = X m"
- by (force simp: dist_discrete_def Cauchy_def split: split_if_asm dest:spec[where x=1])
+ by (force simp: dist_discrete_def Cauchy_def split: if_split_asm dest:spec[where x=1])
then guess n ..
thus "convergent X"
by (intro convergentI[where L="X n"] tendstoI eventually_sequentiallyI[of n])
--- a/src/HOL/Probability/Distributions.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Distributions.thy Tue Feb 23 18:04:31 2016 +0100
@@ -354,7 +354,7 @@
then have "AE x in lborel. x \<le> (0::real)"
apply eventually_elim
using \<open>l < 0\<close>
- apply (auto simp: exponential_density_def zero_le_mult_iff split: split_if_asm)
+ apply (auto simp: exponential_density_def zero_le_mult_iff split: if_split_asm)
done
then show "emeasure lborel {x :: real \<in> space lborel. 0 < x} = 0"
by (subst (asm) AE_iff_measurable[OF _ refl]) (auto simp: not_le greaterThan_def[symmetric])
@@ -543,7 +543,7 @@
have 3: "1 = integral\<^sup>N lborel (\<lambda>xa. ?LHS xa * indicator {0<..} xa)"
by (subst 2[symmetric])
(auto intro!: nn_integral_cong_AE AE_I[where N="{0}"]
- simp: erlang_density_def nn_integral_multc[symmetric] indicator_def split: split_if_asm)
+ simp: erlang_density_def nn_integral_multc[symmetric] indicator_def split: if_split_asm)
also have "... = integral\<^sup>N lborel (\<lambda>x. (ereal (?C) * ?I) * ((erlang_density ?s l x) * indicator {0<..} x))"
by (auto intro!: nn_integral_cong simp: * split: split_indicator)
also have "... = ereal (?C) * ?I"
--- a/src/HOL/Probability/Fin_Map.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Fin_Map.thy Tue Feb 23 18:04:31 2016 +0100
@@ -194,7 +194,7 @@
moreover assume "\<forall>S. open S \<longrightarrow> a \<in> S \<longrightarrow> eventually (\<lambda>x. x \<in> S) F" "a i \<in> S"
ultimately have "eventually (\<lambda>x. x \<in> ?S) F" by auto
thus "eventually (\<lambda>x. (x)\<^sub>F i \<in> S) F"
- by eventually_elim (insert \<open>a i \<in> S\<close>, force simp: Pi'_iff split: split_if_asm)
+ by eventually_elim (insert \<open>a i \<in> S\<close>, force simp: Pi'_iff split: if_split_asm)
qed
lemma continuous_proj:
@@ -298,7 +298,7 @@
lemma dist_le_1_imp_domain_eq:
shows "dist P Q < 1 \<Longrightarrow> domain P = domain Q"
- by (simp add: dist_finmap_def finite_proj_diag split: split_if_asm)
+ by (simp add: dist_finmap_def finite_proj_diag split: if_split_asm)
lemma dist_proj:
shows "dist ((x)\<^sub>F i) ((y)\<^sub>F i) \<le> dist x y"
@@ -724,7 +724,7 @@
by (auto intro!: exI[where x="to_nat l"])
next
fix x n assume "x \<in> (let s = set (from_nat n) in if P s then f s else {})"
- thus "x \<in> \<Union>{f s|s. P s}" using assms by (auto simp: Let_def split: split_if_asm)
+ thus "x \<in> \<Union>{f s|s. P s}" using assms by (auto simp: Let_def split: if_split_asm)
qed
hence "\<Union>{f s|s. P s} = (\<Union>n. let s = set (from_nat n) in if P s then f s else {})" by simp
also have "\<dots> \<in> sets M" using assms by (auto simp: Let_def)
@@ -975,7 +975,7 @@
by auto
then have "A = (\<Pi>' j \<in> I. if j = i then B else space (M j))"
using sets.sets_into_space[OF A(3)]
- apply (auto simp: Pi'_iff split: split_if_asm)
+ apply (auto simp: Pi'_iff split: if_split_asm)
apply blast
done
also have "\<dots> \<in> sigma_sets ?\<Omega> {Pi' I X |X. X \<in> (\<Pi> j\<in>I. sets (M j))}"
@@ -1050,7 +1050,7 @@
proof
fix A assume A: "A \<in> E i"
then have "(\<lambda>x. (x)\<^sub>F i) -` A \<inter> space ?P = (\<Pi>' j\<in>I. if i = j then A else space (M j))"
- using E_closed \<open>i \<in> I\<close> by (auto simp: space_P Pi_iff subset_eq split: split_if_asm)
+ using E_closed \<open>i \<in> I\<close> by (auto simp: space_P Pi_iff subset_eq split: if_split_asm)
also have "\<dots> = (\<Pi>' j\<in>I. \<Union>n. if i = j then A else S j n)"
by (intro Pi'_cong) (simp_all add: S_union)
also have "\<dots> = (\<Union>xs\<in>{xs. length xs = card I}. \<Pi>' j\<in>I. if i = j then A else S j (xs ! T j))"
--- a/src/HOL/Probability/Finite_Product_Measure.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Tue Feb 23 18:04:31 2016 +0100
@@ -131,7 +131,7 @@
lemma prod_emb_PiE: "J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow>
prod_emb I M J (\<Pi>\<^sub>E i\<in>J. E i) = (\<Pi>\<^sub>E i\<in>I. if i \<in> J then E i else space (M i))"
- by (force simp: prod_emb_def PiE_iff split_if_mem2)
+ by (force simp: prod_emb_def PiE_iff if_split_mem2)
lemma prod_emb_PiE_same_index[simp]:
"(\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow> prod_emb I M I (Pi\<^sub>E I E) = Pi\<^sub>E I E"
@@ -145,7 +145,7 @@
assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K"
shows "prod_emb K M J (Pi\<^sub>E J X) = (\<Pi>\<^sub>E i\<in>K. if i \<in> J then X i else space (M i))"
using assms sets.space_closed
- by (auto simp: prod_emb_def PiE_iff split: split_if_asm) blast+
+ by (auto simp: prod_emb_def PiE_iff split: if_split_asm) blast+
lemma prod_emb_id:
"B \<subseteq> (\<Pi>\<^sub>E i\<in>L. space (M i)) \<Longrightarrow> prod_emb L M L B = B"
@@ -202,7 +202,7 @@
next
case (4 x)
thus ?case using assms
- by (auto intro!: setprod.cong split: split_if_asm)
+ by (auto intro!: setprod.cong split: if_split_asm)
qed
@@ -581,7 +581,7 @@
fix A assume "A \<in> sets (M i)"
then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M I M) = prod_emb I M {i} (\<Pi>\<^sub>E j\<in>{i}. A)"
using sets.sets_into_space \<open>i \<in> I\<close>
- by (fastforce dest: Pi_mem simp: prod_emb_def space_PiM split: split_if_asm)
+ by (fastforce dest: Pi_mem simp: prod_emb_def space_PiM split: if_split_asm)
then show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M I M) \<in> sets (Pi\<^sub>M I M)"
using \<open>A \<in> sets (M i)\<close> \<open>i \<in> I\<close> by (auto intro!: sets_PiM_I)
qed (insert \<open>i \<in> I\<close>, auto simp: space_PiM)
@@ -911,13 +911,13 @@
by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+
also have "?h -` ?p \<inter> space (Pi\<^sub>M I M \<Otimes>\<^sub>M M i) = ?p' \<times> (if i \<in> J then E i else space (M i))"
using J E[rule_format, THEN sets.sets_into_space]
- by (force simp: space_pair_measure space_PiM prod_emb_iff PiE_def Pi_iff split: split_if_asm)
+ by (force simp: space_pair_measure space_PiM prod_emb_iff PiE_def Pi_iff split: if_split_asm)
also have "emeasure (Pi\<^sub>M I M \<Otimes>\<^sub>M (M i)) (?p' \<times> (if i \<in> J then E i else space (M i))) =
emeasure (Pi\<^sub>M I M) ?p' * emeasure (M i) (if i \<in> J then (E i) else space (M i))"
using J E by (intro M.emeasure_pair_measure_Times sets_PiM_I) auto
also have "?p' = (\<Pi>\<^sub>E j\<in>I. if j \<in> J-{i} then E j else space (M j))"
using J E[rule_format, THEN sets.sets_into_space]
- by (auto simp: prod_emb_iff PiE_def Pi_iff split: split_if_asm) blast+
+ by (auto simp: prod_emb_iff PiE_def Pi_iff split: if_split_asm) blast+
also have "emeasure (Pi\<^sub>M I M) (\<Pi>\<^sub>E j\<in>I. if j \<in> J-{i} then E j else space (M j)) =
(\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))"
using E by (subst insert) (auto intro!: setprod.cong)
--- a/src/HOL/Probability/Independent_Family.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Independent_Family.thy Tue Feb 23 18:04:31 2016 +0100
@@ -155,7 +155,7 @@
next
assume "J \<noteq> {j}"
have "prob (\<Inter>i\<in>J. A i) = prob ((\<Inter>i\<in>J-{j}. A i) \<inter> X)"
- using \<open>j \<in> J\<close> \<open>A j = X\<close> by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
+ using \<open>j \<in> J\<close> \<open>A j = X\<close> by (auto intro!: arg_cong[where f=prob] split: if_split_asm)
also have "\<dots> = prob X * (\<Prod>i\<in>J-{j}. prob (A i))"
proof (rule indep)
show "J - {j} \<noteq> {}" "J - {j} \<subseteq> K" "finite (J - {j})" "j \<notin> J - {j}"
@@ -172,7 +172,7 @@
qed
next
assume "j \<notin> J"
- with J have "\<forall>i\<in>J. A i \<in> G i" by (auto split: split_if_asm)
+ with J have "\<forall>i\<in>J. A i \<in> G i" by (auto split: if_split_asm)
with J show ?thesis
by (intro indep_setsD[OF G(1)]) auto
qed
@@ -192,10 +192,10 @@
have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) =
prob ((\<Inter>j\<in>J. A j) - (\<Inter>i\<in>insert j J. (A(j := X)) i))"
using A_sets sets.sets_into_space[of _ M] X \<open>J \<noteq> {}\<close>
- by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
+ by (auto intro!: arg_cong[where f=prob] split: if_split_asm)
also have "\<dots> = prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)"
using J \<open>J \<noteq> {}\<close> \<open>j \<notin> J\<close> A_sets X sets.sets_into_space
- by (auto intro!: finite_measure_Diff sets.finite_INT split: split_if_asm)
+ by (auto intro!: finite_measure_Diff sets.finite_INT split: if_split_asm)
finally have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) =
prob (\<Inter>j\<in>J. A j) - prob (\<Inter>i\<in>insert j J. (A(j := X)) i)" .
moreover {
@@ -223,7 +223,7 @@
then have A_sets: "\<And>i. i\<in>J \<Longrightarrow> A i \<in> events"
using G by auto
have "prob ((\<Inter>j\<in>J. A j) \<inter> (\<Union>k. F k)) = prob (\<Union>k. (\<Inter>i\<in>insert j J. (A(j := F k)) i))"
- using \<open>J \<noteq> {}\<close> \<open>j \<notin> J\<close> \<open>j \<in> K\<close> by (auto intro!: arg_cong[where f=prob] split: split_if_asm)
+ using \<open>J \<noteq> {}\<close> \<open>j \<notin> J\<close> \<open>j \<in> K\<close> by (auto intro!: arg_cong[where f=prob] split: if_split_asm)
moreover have "(\<lambda>k. prob (\<Inter>i\<in>insert j J. (A(j := F k)) i)) sums prob (\<Union>k. (\<Inter>i\<in>insert j J. (A(j := F k)) i))"
proof (rule finite_measure_UNION)
show "disjoint_family (\<lambda>k. \<Inter>i\<in>insert j J. (A(j := F k)) i)"
@@ -233,7 +233,7 @@
qed
moreover { fix k
from J A \<open>j \<in> K\<close> have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * (\<Prod>i\<in>J. prob (A i))"
- by (subst indep_setsD[OF F(2)]) (auto intro!: setprod.cong split: split_if_asm)
+ by (subst indep_setsD[OF F(2)]) (auto intro!: setprod.cong split: if_split_asm)
also have "\<dots> = prob (F k) * prob (\<Inter>i\<in>J. A i)"
using J A \<open>j \<in> K\<close> by (subst indep_setsD[OF G(1)]) auto
finally have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * prob (\<Inter>i\<in>J. A i)" . }
@@ -271,7 +271,7 @@
by (intro indep_setsD[OF indep]) auto
next
assume "j \<notin> J"
- with J A have "\<forall>i\<in>J. A i \<in> G i" by (auto split: split_if_asm)
+ with J A have "\<forall>i\<in>J. A i \<in> G i" by (auto split: if_split_asm)
with J show ?thesis
by (intro indep_setsD[OF G(1)]) auto
qed
@@ -842,10 +842,10 @@
let ?A = "\<lambda>j. if j \<in> J then A j else space M"
have "prob (\<Inter>j\<in>I. ?A j) = prob (\<Inter>j\<in>J. A j)"
using subset_trans[OF F(1) sets.space_closed] J A
- by (auto intro!: arg_cong[where f=prob] split: split_if_asm) blast
+ by (auto intro!: arg_cong[where f=prob] split: if_split_asm) blast
also
from A F have "(\<lambda>j. if j \<in> J then A j else space M) \<in> Pi I F" (is "?A \<in> _")
- by (auto split: split_if_asm)
+ by (auto split: if_split_asm)
with indep have "prob (\<Inter>j\<in>I. ?A j) = (\<Prod>j\<in>I. prob (?A j))"
by auto
also have "\<dots> = (\<Prod>j\<in>J. prob (A j))"
@@ -1089,7 +1089,7 @@
then have "emeasure ?D E = emeasure M (?X -` E \<inter> space M)"
by (simp add: emeasure_distr X)
also have "?X -` E \<inter> space M = (\<Inter>i\<in>J. X i -` Y i \<inter> space M)"
- using J \<open>I \<noteq> {}\<close> measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm)
+ using J \<open>I \<noteq> {}\<close> measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: if_split_asm)
also have "emeasure M (\<Inter>i\<in>J. X i -` Y i \<inter> space M) = (\<Prod> i\<in>J. emeasure M (X i -` Y i \<inter> space M))"
using \<open>indep_vars M' X I\<close> J \<open>I \<noteq> {}\<close> using indep_varsD[of M' X I J]
by (auto simp: emeasure_eq_measure setprod_ereal)
@@ -1120,7 +1120,7 @@
Y: "\<And>j. j \<in> J \<Longrightarrow> Y' j = X j -` Y j \<inter> space M" "\<And>j. j \<in> J \<Longrightarrow> Y j \<in> sets (M' j)" by auto
let ?E = "prod_emb I M' J (Pi\<^sub>E J Y)"
from Y have "(\<Inter>j\<in>J. Y' j) = ?X -` ?E \<inter> space M"
- using J \<open>I \<noteq> {}\<close> measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: split_if_asm)
+ using J \<open>I \<noteq> {}\<close> measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: if_split_asm)
then have "emeasure M (\<Inter>j\<in>J. Y' j) = emeasure M (?X -` ?E \<inter> space M)"
by simp
also have "\<dots> = emeasure ?D ?E"
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Tue Feb 23 18:04:31 2016 +0100
@@ -271,4 +271,4 @@
end
-end
\ No newline at end of file
+end
--- a/src/HOL/Probability/Information.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Information.thy Tue Feb 23 18:04:31 2016 +0100
@@ -1105,7 +1105,7 @@
by (intro nn_integral_0_iff_AE[THEN iffD1]) auto
then have "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. Pxyz x = 0"
using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
- by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
+ by eventually_elim (auto split: if_split_asm simp: mult_le_0_iff divide_le_0_iff)
then have "(\<integral>\<^sup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) = 0"
by (subst nn_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
with P.emeasure_space_1 show False
@@ -1362,7 +1362,7 @@
by (intro nn_integral_0_iff_AE[THEN iffD1]) (auto intro!: borel_measurable_ereal measurable_If)
then have "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. Pxyz x = 0"
using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
- by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
+ by eventually_elim (auto split: if_split_asm simp: mult_le_0_iff divide_le_0_iff)
then have "(\<integral>\<^sup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) = 0"
by (subst nn_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
with P.emeasure_space_1 show False
--- a/src/HOL/Probability/Interval_Integral.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Interval_Integral.thy Tue Feb 23 18:04:31 2016 +0100
@@ -302,7 +302,7 @@
proof (induct a b rule: linorder_wlog)
case (sym a b) then show ?case
by (auto simp add: interval_lebesgue_integral_def interval_integrable_endpoints_reverse
- split: split_if_asm)
+ split: if_split_asm)
next
case (le a b) then show ?case
unfolding interval_lebesgue_integral_def
--- a/src/HOL/Probability/Lebesgue_Measure.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Tue Feb 23 18:04:31 2016 +0100
@@ -871,7 +871,7 @@
then have "ereal c * (\<integral>\<^sup>+ x. g x \<partial>lborel) = ereal r"
by (subst nn_integral_cmult[symmetric]) auto
then obtain r' where "(c = 0 \<and> r = 0) \<or> ((\<integral>\<^sup>+ x. ereal (g x) \<partial>lborel) = ereal r' \<and> r = c * r')"
- by (cases "\<integral>\<^sup>+ x. ereal (g x) \<partial>lborel") (auto split: split_if_asm)
+ by (cases "\<integral>\<^sup>+ x. ereal (g x) \<partial>lborel") (auto split: if_split_asm)
with mult show ?case
by (auto intro!: has_integral_cmult_real)
next
@@ -966,7 +966,7 @@
{ fix i x have "real_of_ereal (F i x) \<le> f x"
using F(3,5) F(4)[of x, symmetric] nonneg
unfolding real_le_ereal_iff
- by (auto simp: image_iff eq_commute[of \<infinity>] max_def intro: SUP_upper split: split_if_asm) }
+ by (auto simp: image_iff eq_commute[of \<infinity>] max_def intro: SUP_upper split: if_split_asm) }
note F_le_f = this
let ?F = "\<lambda>i x. F i x * indicator (?B i) x"
have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>lborel) = (SUP i. integral\<^sup>N lborel (\<lambda>x. ?F i x))"
--- a/src/HOL/Probability/Measurable.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Measurable.thy Tue Feb 23 18:04:31 2016 +0100
@@ -581,7 +581,7 @@
shows "Measurable.pred M (\<lambda>x. \<exists>!i\<in>I. P i x)"
unfolding bex1_def by measurable
-lemma measurable_split_if[measurable (raw)]:
+lemma measurable_if_split[measurable (raw)]:
"(c \<Longrightarrow> Measurable.pred M f) \<Longrightarrow> (\<not> c \<Longrightarrow> Measurable.pred M g) \<Longrightarrow>
Measurable.pred M (if c then f else g)"
by simp
--- a/src/HOL/Probability/Measure_Space.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Measure_Space.thy Tue Feb 23 18:04:31 2016 +0100
@@ -1897,7 +1897,7 @@
proof (intro iffI impI)
assume "emeasure (count_space A) X = 0"
with X show "X = {}"
- by (subst (asm) emeasure_count_space) (auto split: split_if_asm)
+ by (subst (asm) emeasure_count_space) (auto split: if_split_asm)
qed simp
qed (simp add: emeasure_notin_sets)
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Tue Feb 23 18:04:31 2016 +0100
@@ -55,7 +55,7 @@
then have "(\<Union>x\<in>f ` space M. if x \<in> A then f -` {x} \<inter> space M else {}) \<in> sets M"
by (intro sets.finite_UN) auto
also have "(\<Union>x\<in>f ` space M. if x \<in> A then f -` {x} \<inter> space M else {}) = f -` A \<inter> space M"
- by (auto split: split_if_asm)
+ by (auto split: if_split_asm)
finally show "f -` A \<inter> space M \<in> sets M" .
qed simp
@@ -222,7 +222,7 @@
proof -
def f \<equiv> "\<lambda>x i. if real i \<le> u x then i * 2 ^ i else nat \<lfloor>real_of_ereal (u x) * 2 ^ i\<rfloor>"
{ fix x j have "f x j \<le> j * 2 ^ j" unfolding f_def
- proof (split split_if, intro conjI impI)
+ proof (split if_split, intro conjI impI)
assume "\<not> real j \<le> u x"
then have "nat \<lfloor>real_of_ereal (u x) * 2 ^ j\<rfloor> \<le> nat \<lfloor>j * 2 ^ j\<rfloor>"
by (cases "u x") (auto intro!: nat_mono floor_mono)
@@ -258,7 +258,7 @@
proof (intro incseq_ereal incseq_SucI le_funI)
fix x and i :: nat
have "f x i * 2 \<le> f x (Suc i)" unfolding f_def
- proof ((split split_if)+, intro conjI impI)
+ proof ((split if_split)+, intro conjI impI)
assume "ereal (real i) \<le> u x" "\<not> ereal (real (Suc i)) \<le> u x"
then show "i * 2 ^ i * 2 \<le> nat \<lfloor>real_of_ereal (u x) * 2 ^ Suc i\<rfloor>"
by (cases "u x") (auto intro!: le_nat_floor)
@@ -311,7 +311,7 @@
moreover
have "real (nat \<lfloor>p * 2 ^ max N m\<rfloor>) \<le> r * 2 ^ max N m"
using *[of "max N m"] m unfolding real_f using ux
- by (cases "0 \<le> u x") (simp_all add: max_def split: split_if_asm)
+ by (cases "0 \<le> u x") (simp_all add: max_def split: if_split_asm)
then have "p * 2 ^ max N m - 1 < r * 2 ^ max N m"
by linarith
ultimately show False by auto
@@ -467,7 +467,7 @@
then have *: "?IF -` {?IF x} \<inter> space M = (if x \<in> A
then ((F (f x) \<inter> (A \<inter> space M)) \<union> (G (f x) - (G (f x) \<inter> (A \<inter> space M))))
else ((F (g x) \<inter> (A \<inter> space M)) \<union> (G (g x) - (G (g x) \<inter> (A \<inter> space M)))))"
- using sets.sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def)
+ using sets.sets_into_space[OF A] by (auto split: if_split_asm simp: G_def F_def)
have [intro]: "\<And>x. F x \<in> sets M" "\<And>x. G x \<in> sets M"
unfolding F_def G_def using sf[THEN simple_functionD(2)] by auto
show "?IF -` {?IF x} \<inter> space M \<in> sets M" unfolding * using A by auto
@@ -685,7 +685,7 @@
(\<Sum>x \<in> f ` space M. x * emeasure M (f -` {x} \<inter> space M \<inter> A))"
proof -
have eq: "(\<lambda>x. (f x, indicator A x)) ` space M \<inter> {x. snd x = 1} = (\<lambda>x. (f x, 1::ereal))`A"
- using A[THEN sets.sets_into_space] by (auto simp: indicator_def image_iff split: split_if_asm)
+ using A[THEN sets.sets_into_space] by (auto simp: indicator_def image_iff split: if_split_asm)
have eq2: "\<And>x. f x \<notin> f ` A \<Longrightarrow> f -` {f x} \<inter> space M \<inter> A = {}"
by (auto simp: image_iff)
@@ -694,7 +694,7 @@
using assms by (intro simple_function_partition) auto
also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, indicator A x::ereal))`space M.
if snd y = 1 then fst y * emeasure M (f -` {fst y} \<inter> space M \<inter> A) else 0)"
- by (auto simp: indicator_def split: split_if_asm intro!: arg_cong2[where f="op *"] arg_cong2[where f=emeasure] setsum.cong)
+ by (auto simp: indicator_def split: if_split_asm intro!: arg_cong2[where f="op *"] arg_cong2[where f=emeasure] setsum.cong)
also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, 1::ereal))`A. fst y * emeasure M (f -` {fst y} \<inter> space M \<inter> A))"
using assms by (subst setsum.If_cases) (auto intro!: simple_functionD(1) simp: eq)
also have "\<dots> = (\<Sum>y\<in>fst`(\<lambda>x. (f x, 1::ereal))`A. y * emeasure M (f -` {y} \<inter> space M \<inter> A))"
@@ -709,7 +709,7 @@
assumes "A \<in> sets M"
shows "integral\<^sup>S M (indicator A) = emeasure M A"
using simple_integral_indicator[OF assms, of "\<lambda>x. 1"] sets.sets_into_space[OF assms]
- by (simp_all add: image_constant_conv Int_absorb1 split: split_if_asm)
+ by (simp_all add: image_constant_conv Int_absorb1 split: if_split_asm)
lemma simple_integral_null_set:
assumes "simple_function M u" "\<And>x. 0 \<le> u x" and "N \<in> null_sets M"
@@ -777,7 +777,7 @@
let ?g = "\<lambda>y x. if g x = \<infinity> then y else max 0 (g x)"
from g gM have g_in_A: "\<And>y. 0 \<le> y \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> ?g y \<in> ?A"
apply (safe intro!: simple_function_max simple_function_If)
- apply (force simp: max_def le_fun_def split: split_if_asm)+
+ apply (force simp: max_def le_fun_def split: if_split_asm)+
done
show "integral\<^sup>S M g \<le> SUPREMUM ?A ?f"
proof cases
@@ -826,7 +826,7 @@
assume x: "x \<in> space M - N"
with N have "u x \<le> v x" by auto
with n(2)[THEN le_funD, of x] x show ?thesis
- by (auto simp: max_def split: split_if_asm)
+ by (auto simp: max_def split: if_split_asm)
qed simp }
then have "?n \<le> max 0 \<circ> v" by (auto simp: le_funI)
moreover have "integral\<^sup>S M n \<le> integral\<^sup>S M ?n"
@@ -1086,7 +1086,7 @@
by (subst nn_integral_eq_simple_integral) auto
lemma nn_integral_const_nonpos: "c \<le> 0 \<Longrightarrow> nn_integral M (\<lambda>x. c) = 0"
- using nn_integral_max_0[of M "\<lambda>x. c"] by (simp add: max_def split: split_if_asm)
+ using nn_integral_max_0[of M "\<lambda>x. c"] by (simp add: max_def split: if_split_asm)
lemma nn_integral_linear:
assumes f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" and "0 \<le> a"
@@ -1111,7 +1111,7 @@
have pos: "\<And>i. 0 \<le> integral\<^sup>S M (u i)" "\<And>i. 0 \<le> integral\<^sup>S M (v i)" "\<And>i. 0 \<le> a * integral\<^sup>S M (u i)"
using u v \<open>0 \<le> a\<close> by (auto simp: simple_integral_nonneg)
{ fix i from pos[of i] have "a * integral\<^sup>S M (u i) \<noteq> -\<infinity>" "integral\<^sup>S M (v i) \<noteq> -\<infinity>"
- by (auto split: split_if_asm) }
+ by (auto split: if_split_asm) }
note not_MInf = this
have l': "(SUP i. integral\<^sup>S M (l i)) = (SUP i. integral\<^sup>S M (?L' i))"
@@ -1316,7 +1316,7 @@
moreover have "0 \<le> (emeasure M) (f -` {\<infinity>} \<inter> space M)"
by (rule emeasure_nonneg)
ultimately show ?thesis
- using assms by (auto split: split_if_asm)
+ using assms by (auto split: if_split_asm)
qed
lemma nn_integral_PInf_AE:
@@ -1620,7 +1620,7 @@
show "integral\<^sup>N M u = 0" by (simp add: u_eq null_sets_def)
next
{ fix r :: ereal and n :: nat assume gt_1: "1 \<le> real n * r"
- then have "0 < real n * r" by (cases r) (auto split: split_if_asm simp: one_ereal_def)
+ then have "0 < real n * r" by (cases r) (auto split: if_split_asm simp: one_ereal_def)
then have "0 \<le> r" by (auto simp add: ereal_zero_less_0_iff) }
note gt_1 = this
assume *: "integral\<^sup>N M u = 0"
@@ -2377,7 +2377,7 @@
using f \<open>A \<in> sets M\<close>
by (intro AE_iff_measurable[OF _ refl, symmetric]) auto
also have "(AE x in M. max 0 (f x) * indicator A x = 0) \<longleftrightarrow> (AE x in M. x \<in> A \<longrightarrow> f x \<le> 0)"
- by (auto simp add: indicator_def max_def split: split_if_asm)
+ by (auto simp add: indicator_def max_def split: if_split_asm)
finally have "(\<integral>\<^sup>+x. f x * indicator A x \<partial>M) = 0 \<longleftrightarrow> (AE x in M. x \<in> A \<longrightarrow> f x \<le> 0)" . }
with f show ?thesis
by (simp add: null_sets_def emeasure_density cong: conj_cong)
--- a/src/HOL/Probability/Probability_Mass_Function.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Tue Feb 23 18:04:31 2016 +0100
@@ -876,7 +876,7 @@
by transfer (simp add: emeasure_measure_pmf_not_zero pmf.rep_eq)
lemma set_cond_pmf[simp]: "set_pmf cond_pmf = set_pmf p \<inter> s"
- by (auto simp add: set_pmf_iff pmf_cond measure_measure_pmf_not_zero split: split_if_asm)
+ by (auto simp add: set_pmf_iff pmf_cond measure_measure_pmf_not_zero split: if_split_asm)
end
--- a/src/HOL/Probability/Probability_Measure.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy Tue Feb 23 18:04:31 2016 +0100
@@ -195,7 +195,7 @@
lemma (in prob_space) nn_integral_ge_const:
"(AE x in M. c \<le> f x) \<Longrightarrow> c \<le> (\<integral>\<^sup>+x. f x \<partial>M)"
using nn_integral_mono_AE[of "\<lambda>x. c" f M] emeasure_space_1
- by (simp add: nn_integral_const_If split: split_if_asm)
+ by (simp add: nn_integral_const_If split: if_split_asm)
lemma (in prob_space) expectation_less:
fixes X :: "_ \<Rightarrow> real"
--- a/src/HOL/Probability/Radon_Nikodym.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy Tue Feb 23 18:04:31 2016 +0100
@@ -155,7 +155,7 @@
{ fix n have "A n \<in> sets M"
proof (induct n)
case (Suc n) thus "A (Suc n) \<in> sets M"
- using A'_in_sets[of "A n"] by (auto split: split_if_asm)
+ using A'_in_sets[of "A n"] by (auto split: if_split_asm)
qed (simp add: A_def) }
note A_in_sets = this
hence "range A \<subseteq> sets M" by auto
@@ -870,7 +870,7 @@
by (auto simp: indicator_def Q0)
ultimately have "AE x in M. ?f (space M) x = ?f' (space M) x"
unfolding AE_all_countable[symmetric]
- by eventually_elim (auto intro!: AE_I2 split: split_if_asm simp: indicator_def)
+ by eventually_elim (auto intro!: AE_I2 split: if_split_asm simp: indicator_def)
then show "AE x in M. f x = f' x" by auto
qed
--- a/src/HOL/Probability/Sigma_Algebra.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Tue Feb 23 18:04:31 2016 +0100
@@ -280,7 +280,7 @@
from assms have "range ?A \<subseteq> M" by auto
with countable_nat_UN[of "?A \<circ> from_nat"] countable_UN_eq[of ?A M]
have "(\<Union>x. ?A x) \<in> M" by auto
- moreover have "(\<Union>x. ?A x) = (\<Union>x\<in>X. A x)" by (auto split: split_if_asm)
+ moreover have "(\<Union>x. ?A x) = (\<Union>x\<in>X. A x)" by (auto split: if_split_asm)
ultimately show ?thesis by simp
qed
@@ -1194,7 +1194,7 @@
have "range ?f = {D, \<Omega> - E, {}}"
by (auto simp: image_iff)
moreover have "D \<union> (\<Omega> - E) = (\<Union>i. ?f i)"
- by (auto simp: image_iff split: split_if_asm)
+ by (auto simp: image_iff split: if_split_asm)
moreover
have "disjoint_family ?f" unfolding disjoint_family_on_def
using \<open>D \<in> M\<close>[THEN sets_into_space] \<open>D \<subseteq> E\<close> by auto
--- a/src/HOL/Probability/Sinc_Integral.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/Sinc_Integral.thy Tue Feb 23 18:04:31 2016 +0100
@@ -196,7 +196,7 @@
using interval_integral_FTC2[of "min 0 (x - 1)" 0 "max 0 (x + 1)" sinc x]
by (auto simp: continuous_at_imp_continuous_on isCont_sinc Si_alt_def[abs_def] zero_ereal_def
has_field_derivative_iff_has_vector_derivative
- split del: split_if)
+ split del: if_split)
qed
lemma isCont_Si: "isCont Si x"
@@ -389,7 +389,7 @@
hence "LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x =
- (LBINT x. indicator {0<..<- (T * \<theta>)} x * sin x / x)"
using assms `0 > \<theta>` unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def
- by (auto simp add: field_simps mult_le_0_iff split: split_if_asm)
+ by (auto simp add: field_simps mult_le_0_iff split: if_split_asm)
} note aux2 = this
show ?thesis
using assms unfolding Si_def interval_lebesgue_integral_def sgn_real_def einterval_eq zero_ereal_def
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Tue Feb 23 18:04:31 2016 +0100
@@ -43,7 +43,7 @@
shows "extensionalD d (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensionalD d A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)"
apply (rule funset_eq_UN_fun_upd_I)
using assms
- by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensionalD_def)
+ by (auto intro!: inj_onI dest: inj_onD split: if_split_asm simp: extensionalD_def)
lemma finite_extensionalD_funcset[simp, intro]:
assumes "finite A" "finite B"
--- a/src/HOL/Probability/ex/Measure_Not_CCC.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Probability/ex/Measure_Not_CCC.thy Tue Feb 23 18:04:31 2016 +0100
@@ -110,7 +110,7 @@
show "(\<Union>i. X i) \<in> sets M" "countable (\<Union>i. J i)" "G \<in> (\<Union>i. J i) \<rightarrow> sets M"
using XFJ by (auto simp: G_def Pi_iff)
show "UNION UNIV A = (UNIV - (\<Union>i. J i)) \<times> (\<Union>i. X i) \<union> (SIGMA j:\<Union>i. J i. \<Union>i. if j \<in> J i then F i j else X i)"
- unfolding A_eq by (auto split: split_if_asm)
+ unfolding A_eq by (auto split: if_split_asm)
qed
qed
--- a/src/HOL/Proofs/Lambda/ListBeta.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Proofs/Lambda/ListBeta.thy Tue Feb 23 18:04:31 2016 +0100
@@ -42,21 +42,21 @@
apply (case_tac r)
apply simp
apply (simp add: App_eq_foldl_conv)
- apply (split split_if_asm)
+ apply (split if_split_asm)
apply simp
apply blast
apply simp
apply (simp add: App_eq_foldl_conv)
- apply (split split_if_asm)
+ apply (split if_split_asm)
apply simp
apply simp
apply (drule App_eq_foldl_conv [THEN iffD1])
- apply (split split_if_asm)
+ apply (split if_split_asm)
apply simp
apply blast
apply (force intro!: disjI1 [THEN append_step1I])
apply (drule App_eq_foldl_conv [THEN iffD1])
- apply (split split_if_asm)
+ apply (split if_split_asm)
apply simp
apply blast
apply (clarify, auto 0 3 intro!: exI intro: append_step1I)
--- a/src/HOL/Rat.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Rat.thy Tue Feb 23 18:04:31 2016 +0100
@@ -280,15 +280,15 @@
lemma normalize_eq: "normalize (a, b) = (p, q) \<Longrightarrow> Fract p q = Fract a b"
by (auto simp add: normalize_def Let_def Fract_coprime dvd_div_neg rat_number_collapse
- split:split_if_asm)
+ split:if_split_asm)
lemma normalize_denom_pos: "normalize r = (p, q) \<Longrightarrow> q > 0"
by (auto simp add: normalize_def Let_def dvd_div_neg pos_imp_zdiv_neg_iff nonneg1_imp_zdiv_pos_iff
- split:split_if_asm)
+ split:if_split_asm)
lemma normalize_coprime: "normalize r = (p, q) \<Longrightarrow> coprime p q"
by (auto simp add: normalize_def Let_def dvd_div_neg div_gcd_coprime
- split:split_if_asm)
+ split:if_split_asm)
lemma normalize_stable [simp]:
"q > 0 \<Longrightarrow> coprime p q \<Longrightarrow> normalize (p, q) = (p, q)"
--- a/src/HOL/Real.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Real.thy Tue Feb 23 18:04:31 2016 +0100
@@ -476,7 +476,7 @@
shows "inverse (Real X) =
(if vanishes X then 0 else Real (\<lambda>n. inverse (X n)))"
using assms inverse_real.transfer zero_real.transfer
- unfolding cr_real_eq rel_fun_def by (simp split: split_if_asm, metis)
+ unfolding cr_real_eq rel_fun_def by (simp split: if_split_asm, metis)
instance proof
fix a b c :: real
--- a/src/HOL/Rings.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Rings.thy Tue Feb 23 18:04:31 2016 +0100
@@ -1578,7 +1578,7 @@
by (simp add: not_less)
proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y"
- by (auto simp add: abs_if split: split_if_asm)
+ by (auto simp add: abs_if split: if_split_asm)
lemma sum_squares_ge_zero:
"0 \<le> x * x + y * y"
--- a/src/HOL/SET_Protocol/Message_SET.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy Tue Feb 23 18:04:31 2016 +0100
@@ -539,7 +539,7 @@
(*Case analysis: either the message is secure, or it is not!
Effective, but can cause subgoals to blow up!
- Use with split_if; apparently split_tac does not cope with patterns
+ Use with if_split; apparently split_tac does not cope with patterns
such as "analz (insert (Crypt K X) H)" *)
lemma analz_Crypt_if [simp]:
"analz (insert (Crypt K X) H) =
--- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy Tue Feb 23 18:04:31 2016 +0100
@@ -177,4 +177,4 @@
where
"rmd X len = rounds X h_0 len"
-end
\ No newline at end of file
+end
--- a/src/HOL/SPARK/Examples/RIPEMD-160/S_L.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/S_L.thy Tue Feb 23 18:04:31 2016 +0100
@@ -27,4 +27,4 @@
spark_end
-end
\ No newline at end of file
+end
--- a/src/HOL/SPARK/Examples/RIPEMD-160/S_R.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/S_R.thy Tue Feb 23 18:04:31 2016 +0100
@@ -27,4 +27,4 @@
spark_end
-end
\ No newline at end of file
+end
--- a/src/HOL/Set.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Set.thy Tue Feb 23 18:04:31 2016 +0100
@@ -1046,26 +1046,26 @@
by auto
text \<open>
- Rewrite rules for boolean case-splitting: faster than \<open>split_if [split]\<close>.
+ Rewrite rules for boolean case-splitting: faster than \<open>if_split [split]\<close>.
\<close>
-lemma split_if_eq1: "((if Q then x else y) = b) = ((Q --> x = b) & (~ Q --> y = b))"
- by (rule split_if)
-
-lemma split_if_eq2: "(a = (if Q then x else y)) = ((Q --> a = x) & (~ Q --> a = y))"
- by (rule split_if)
+lemma if_split_eq1: "((if Q then x else y) = b) = ((Q --> x = b) & (~ Q --> y = b))"
+ by (rule if_split)
+
+lemma if_split_eq2: "(a = (if Q then x else y)) = ((Q --> a = x) & (~ Q --> a = y))"
+ by (rule if_split)
text \<open>
Split ifs on either side of the membership relation. Not for \<open>[simp]\<close> -- can cause goals to blow up!
\<close>
-lemma split_if_mem1: "((if Q then x else y) : b) = ((Q --> x : b) & (~ Q --> y : b))"
- by (rule split_if)
-
-lemma split_if_mem2: "(a : (if Q then x else y)) = ((Q --> a : x) & (~ Q --> a : y))"
- by (rule split_if [where P="%S. a : S"])
-
-lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
+lemma if_split_mem1: "((if Q then x else y) : b) = ((Q --> x : b) & (~ Q --> y : b))"
+ by (rule if_split)
+
+lemma if_split_mem2: "(a : (if Q then x else y)) = ((Q --> a : x) & (~ Q --> a : y))"
+ by (rule if_split [where P="%S. a : S"])
+
+lemmas split_ifs = if_bool_eq_conj if_split_eq1 if_split_eq2 if_split_mem1 if_split_mem2
(*Would like to add these, but the existing code only searches for the
outer-level constant, which in this case is just Set.member; we instead need
--- a/src/HOL/Set_Interval.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Set_Interval.thy Tue Feb 23 18:04:31 2016 +0100
@@ -929,7 +929,7 @@
by (auto intro!: image_eqI[of _ _ "a + c"])
next
assume "\<not> c < y" with a show ?thesis
- by (auto intro!: image_eqI[of _ _ x] split: split_if_asm)
+ by (auto intro!: image_eqI[of _ _ x] split: if_split_asm)
qed
qed auto
--- a/src/HOL/Statespace/DistinctTreeProver.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Tue Feb 23 18:04:31 2016 +0100
@@ -134,12 +134,12 @@
by simp
with l'_l Some x_l_Some del
show ?thesis
- by (auto split: split_if_asm)
+ by (auto split: if_split_asm)
next
case None
with l'_l Some x_l_Some del
show ?thesis
- by (fastforce split: split_if_asm)
+ by (fastforce split: if_split_asm)
qed
next
case None
@@ -152,12 +152,12 @@
by simp
with Some x_l_None del
show ?thesis
- by (fastforce split: split_if_asm)
+ by (fastforce split: if_split_asm)
next
case None
with x_l_None del
show ?thesis
- by (fastforce split: split_if_asm)
+ by (fastforce split: if_split_asm)
qed
qed
qed
@@ -221,7 +221,7 @@
case None
with x_l_None del dist_l dist_r d dist_l_r
show ?thesis
- by (fastforce split: split_if_asm)
+ by (fastforce split: if_split_asm)
qed
qed
qed
@@ -257,14 +257,14 @@
by simp
from x_r x_l Some x_l_Some del
show ?thesis
- by (clarsimp split: split_if_asm)
+ by (clarsimp split: if_split_asm)
next
case None
then have "x \<notin> set_of r"
by (simp add: delete_None_set_of_conv)
with x_l None x_l_Some del
show ?thesis
- by (clarsimp split: split_if_asm)
+ by (clarsimp split: if_split_asm)
qed
next
case None
@@ -279,14 +279,14 @@
by simp
from x_r x_notin_l Some x_l_None del
show ?thesis
- by (clarsimp split: split_if_asm)
+ by (clarsimp split: if_split_asm)
next
case None
then have "x \<notin> set_of r"
by (simp add: delete_None_set_of_conv)
with None x_l_None x_notin_l del
show ?thesis
- by (clarsimp split: split_if_asm)
+ by (clarsimp split: if_split_asm)
qed
qed
qed
--- a/src/HOL/Statespace/StateFun.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Statespace/StateFun.thy Tue Feb 23 18:04:31 2016 +0100
@@ -106,4 +106,4 @@
apply simp
oops
-end
\ No newline at end of file
+end
--- a/src/HOL/Statespace/StateSpaceLocale.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Statespace/StateSpaceLocale.thy Tue Feb 23 18:04:31 2016 +0100
@@ -36,4 +36,4 @@
end
-end
\ No newline at end of file
+end
--- a/src/HOL/Statespace/distinct_tree_prover.ML Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Tue Feb 23 18:04:31 2016 +0100
@@ -365,4 +365,4 @@
end;
-end;
\ No newline at end of file
+end;
--- a/src/HOL/TPTP/TPTP_Interpret.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Interpret.thy Tue Feb 23 18:04:31 2016 +0100
@@ -14,4 +14,4 @@
ML_file "TPTP_Parser/tptp_interpret.ML"
-end
\ No newline at end of file
+end
--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy Tue Feb 23 18:04:31 2016 +0100
@@ -158,4 +158,4 @@
else ()
*}
-end
\ No newline at end of file
+end
--- a/src/HOL/TPTP/TPTP_Parser.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Parser.thy Tue Feb 23 18:04:31 2016 +0100
@@ -44,4 +44,4 @@
performance of this software.
*}
-end
\ No newline at end of file
+end
--- a/src/HOL/TPTP/TPTP_Parser_Test.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Parser_Test.thy Tue Feb 23 18:04:31 2016 +0100
@@ -125,4 +125,4 @@
else ()
*}
-end
\ No newline at end of file
+end
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Tue Feb 23 18:04:31 2016 +0100
@@ -822,4 +822,4 @@
Use this to find the smallest failure, then debug that.
*)
-end
\ No newline at end of file
+end
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy Tue Feb 23 18:04:31 2016 +0100
@@ -2290,4 +2290,4 @@
apply (tactic {*standard_cnf_tac @{context} 1*})
done
-end
\ No newline at end of file
+end
--- a/src/HOL/TPTP/TPTP_Test.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Test.thy Tue Feb 23 18:04:31 2016 +0100
@@ -105,4 +105,4 @@
Timing.timing TPTP_Parser.parse_file (Path.implode file)
*}
-end
\ No newline at end of file
+end
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Tue Feb 23 18:04:31 2016 +0100
@@ -32,8 +32,8 @@
val atomize_conjL = @{thm atomize_conjL};
val falseEs = @{thms not_TrueE FalseE};
val neq_eq_eq_contradict = @{thm neq_eq_eq_contradict};
-val split_if = @{thm split_if};
-val split_if_asm = @{thm split_if_asm};
+val if_split = @{thm if_split};
+val if_split_asm = @{thm if_split_asm};
val split_connectI = @{thms allI impI conjI};
val unfold_lets = @{thms Let_def[abs_def] split_beta}
@@ -136,8 +136,8 @@
HEADGOAL (REPEAT_DETERM o (rtac ctxt refl ORELSE'
eresolve_tac ctxt falseEs ORELSE'
resolve_tac ctxt split_connectI ORELSE'
- Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE'
- Splitter.split_tac ctxt (split_if :: splits) ORELSE'
+ Splitter.split_asm_tac ctxt (if_split_asm :: split_asms) ORELSE'
+ Splitter.split_tac ctxt (if_split :: splits) ORELSE'
eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN'
assume_tac ctxt ORELSE'
etac ctxt notE THEN' assume_tac ctxt ORELSE'
@@ -169,7 +169,7 @@
fun raw_code_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
let
val splits' =
- map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits);
+ map (fn th => th RS iffD2) (@{thm if_split_eq2} :: map (inst_split_eq ctxt) splits);
in
HEADGOAL (REPEAT o (resolve_tac ctxt (splits' @ split_connectI))) THEN
prelude_tac ctxt [] (fun_ctr RS trans) THEN
@@ -177,8 +177,8 @@
SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
(rtac ctxt refl ORELSE' assume_tac ctxt ORELSE'
resolve_tac ctxt (@{thm Code.abort_def} :: split_connectI) ORELSE'
- Splitter.split_tac ctxt (split_if :: splits) ORELSE'
- Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE'
+ Splitter.split_tac ctxt (if_split :: splits) ORELSE'
+ Splitter.split_asm_tac ctxt (if_split_asm :: split_asms) ORELSE'
mk_primcorec_assumption_tac ctxt discIs ORELSE'
distinct_in_prems_tac ctxt distincts ORELSE'
(TRY o dresolve_tac ctxt discIs) THEN' etac ctxt notE THEN' assume_tac ctxt)))))
@@ -210,7 +210,7 @@
SELECT_GOAL (unfold_thms_tac ctxt unfold_lets) THEN' REPEAT_DETERM o
(rtac ctxt refl ORELSE' assume_tac ctxt ORELSE'
resolve_tac ctxt split_connectI ORELSE'
- Splitter.split_tac ctxt (split_if :: splits) ORELSE'
+ Splitter.split_tac ctxt (if_split :: splits) ORELSE'
distinct_in_prems_tac ctxt distincts ORELSE'
rtac ctxt sym THEN' assume_tac ctxt ORELSE'
etac ctxt notE THEN' assume_tac ctxt));
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Tue Feb 23 18:04:31 2016 +0100
@@ -477,4 +477,4 @@
(map (fn (mode, (fun_name, random)) => (mode, (functional_compilation fun_name mode, random)))
fun_names)
-end
\ No newline at end of file
+end
--- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML Tue Feb 23 18:04:31 2016 +0100
@@ -544,4 +544,4 @@
((moded_clauses, need_random), errors)
end;
-end;
\ No newline at end of file
+end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Tue Feb 23 18:04:31 2016 +0100
@@ -320,7 +320,7 @@
else all_tac
in
split_term_tac (HOLogic.mk_tuple out_ts)
- THEN (DETERM (TRY ((Splitter.split_asm_tac ctxt @{thms split_if_asm} 1)
+ THEN (DETERM (TRY ((Splitter.split_asm_tac ctxt @{thms if_split_asm} 1)
THEN (eresolve_tac ctxt @{thms botE} 2))))
end
@@ -505,4 +505,4 @@
else (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt)))
end
-end
\ No newline at end of file
+end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Tue Feb 23 18:04:31 2016 +0100
@@ -209,4 +209,4 @@
fold_map specialise' specs thy
end
-end
\ No newline at end of file
+end
--- a/src/HOL/Tools/Quickcheck/abstract_generators.ML Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML Tue Feb 23 18:04:31 2016 +0100
@@ -75,4 +75,4 @@
>> (fn ((tyco, opt_pred), constrs) =>
Toplevel.theory (quickcheck_generator_cmd tyco opt_pred constrs)))
-end;
\ No newline at end of file
+end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Feb 23 18:04:31 2016 +0100
@@ -412,4 +412,4 @@
preferred_methss = preferred_methss, run_time = run_time, message = message}
end
-end;
\ No newline at end of file
+end;
--- a/src/HOL/Tools/boolean_algebra_cancel.ML Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Tools/boolean_algebra_cancel.ML Tue Feb 23 18:04:31 2016 +0100
@@ -78,4 +78,4 @@
val cancel_sup_conv = cancel_conv true (fn pos => if pos then mk_meta_eq @{thm sup_cancel_left1} else mk_meta_eq @{thm sup_cancel_left2})
val cancel_inf_conv = cancel_conv false (fn pos => if pos then mk_meta_eq @{thm inf_cancel_left1} else mk_meta_eq @{thm inf_cancel_left2})
-end
\ No newline at end of file
+end
--- a/src/HOL/Transcendental.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Transcendental.thy Tue Feb 23 18:04:31 2016 +0100
@@ -4265,11 +4265,11 @@
lemma cos_tan: "\<bar>x\<bar> < pi/2 \<Longrightarrow> cos(x) = 1 / sqrt(1 + tan(x) ^ 2)"
using cos_gt_zero_pi [of x]
- by (simp add: divide_simps tan_def real_sqrt_divide abs_if split: split_if_asm)
+ by (simp add: divide_simps tan_def real_sqrt_divide abs_if split: if_split_asm)
lemma sin_tan: "\<bar>x\<bar> < pi/2 \<Longrightarrow> sin(x) = tan(x) / sqrt(1 + tan(x) ^ 2)"
using cos_gt_zero [of "x"] cos_gt_zero [of "-x"]
- by (force simp add: divide_simps tan_def real_sqrt_divide abs_if split: split_if_asm)
+ by (force simp add: divide_simps tan_def real_sqrt_divide abs_if split: if_split_asm)
lemma tan_mono_le: "-(pi/2) < x ==> x \<le> y ==> y < pi/2 \<Longrightarrow> tan(x) \<le> tan(y)"
using less_eq_real_def tan_monotone by auto
@@ -4284,7 +4284,7 @@
lemma tan_bound_pi2: "\<bar>x\<bar> < pi/4 \<Longrightarrow> \<bar>tan x\<bar> < 1"
using tan_45 tan_monotone [of x "pi/4"] tan_monotone [of "-x" "pi/4"]
- by (auto simp: abs_if split: split_if_asm)
+ by (auto simp: abs_if split: if_split_asm)
lemma tan_cot: "tan(pi/2 - x) = inverse(tan x)"
by (simp add: tan_def sin_diff cos_diff)
--- a/src/HOL/UNITY/Lift_prog.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy Tue Feb 23 18:04:31 2016 +0100
@@ -129,7 +129,7 @@
==> \<exists>g'. insert_map i s' f = insert_map j t g'"
apply (subst insert_map_upd_same [symmetric])
apply (erule ssubst)
-apply (simp only: insert_map_upd if_False split: split_if, blast)
+apply (simp only: insert_map_upd if_False split: if_split, blast)
done
lemma lift_map_eq_diff:
--- a/src/HOL/UNITY/Simple/Channel.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/UNITY/Simple/Channel.thy Tue Feb 23 18:04:31 2016 +0100
@@ -29,7 +29,7 @@
(*None represents "infinity" while Some represents proper integers*)
lemma minSet_eq_SomeD: "minSet A = Some x ==> x \<in> A"
apply (unfold minSet_def)
-apply (simp split: split_if_asm)
+apply (simp split: if_split_asm)
apply (fast intro: LeastI)
done
--- a/src/HOL/UNITY/Simple/Lift.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/UNITY/Simple/Lift.thy Tue Feb 23 18:04:31 2016 +0100
@@ -336,7 +336,7 @@
(** Towards lift_4 ***)
-declare split_if_asm [split]
+declare if_split_asm [split]
(*lem_lift_4_1 *)
--- a/src/HOL/UNITY/Simple/Reach.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/UNITY/Simple/Reach.thy Tue Feb 23 18:04:31 2016 +0100
@@ -45,7 +45,7 @@
"[| if P then Q else R;
[| P; Q |] ==> S;
[| ~ P; R |] ==> S |] ==> S"
-by (simp split: split_if_asm)
+by (simp split: if_split_asm)
declare Rprg_def [THEN def_prg_Init, simp]
--- a/src/HOL/UNITY/Simple/Reachability.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/UNITY/Simple/Reachability.thy Tue Feb 23 18:04:31 2016 +0100
@@ -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: split_if_asm)
+apply (simp split add: 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: split_if_asm)
+apply (auto split add: if_split_asm)
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: split_if_asm)
+apply (auto split add: if_split_asm)
apply (blast dest: E_imp_in_V_L E_imp_in_V_R)+
done
--- a/src/HOL/Word/Bool_List_Representation.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy Tue Feb 23 18:04:31 2016 +0100
@@ -922,8 +922,8 @@
lemmas bin_rsplit_aux_simps = bin_rsplit_aux.simps bin_rsplitl_aux.simps
lemmas rsplit_aux_simps = bin_rsplit_aux_simps
-lemmas th_if_simp1 = split_if [where P = "op = l", THEN iffD1, THEN conjunct1, THEN mp] for l
-lemmas th_if_simp2 = split_if [where P = "op = l", THEN iffD1, THEN conjunct2, THEN mp] for l
+lemmas th_if_simp1 = if_split [where P = "op = l", THEN iffD1, THEN conjunct1, THEN mp] for l
+lemmas th_if_simp2 = if_split [where P = "op = l", THEN iffD1, THEN conjunct2, THEN mp] for l
lemmas rsplit_aux_simp1s = rsplit_aux_simps [THEN th_if_simp1]
@@ -995,7 +995,7 @@
apply clarsimp
apply clarsimp
apply (drule bthrs)
- apply (simp (no_asm_use) add: Let_def split: prod.split_asm split_if_asm)
+ apply (simp (no_asm_use) add: Let_def split: prod.split_asm if_split_asm)
apply clarify
apply (drule split_bintrunc)
apply simp
@@ -1011,7 +1011,7 @@
apply clarsimp
apply clarsimp
apply (drule bthrs)
- apply (simp (no_asm_use) add: Let_def split: prod.split_asm split_if_asm)
+ apply (simp (no_asm_use) add: Let_def split: prod.split_asm if_split_asm)
apply clarify
apply (erule allE, erule impE, erule exI)
apply (case_tac k)
--- a/src/HOL/Word/Word.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Word/Word.thy Tue Feb 23 18:04:31 2016 +0100
@@ -1545,7 +1545,7 @@
fun uint_arith_simpset ctxt =
ctxt addsimps @{thms uint_arith_simps}
delsimps @{thms word_uint.Rep_inject}
- |> fold Splitter.add_split @{thms split_if_asm}
+ |> fold Splitter.add_split @{thms if_split_asm}
|> fold Simplifier.add_cong @{thms power_False_cong}
fun uint_arith_tacs ctxt =
@@ -1748,7 +1748,7 @@
using [[simproc del: linordered_ring_less_cancel_factor]]
apply (unfold udvd_def)
apply clarify
- apply (simp add: uint_arith_simps split: split_if_asm)
+ apply (simp add: uint_arith_simps split: if_split_asm)
prefer 2
apply (insert uint_range' [of s])[1]
apply arith
@@ -2047,7 +2047,7 @@
fun unat_arith_simpset ctxt =
ctxt addsimps @{thms unat_arith_simps}
delsimps @{thms word_unat.Rep_inject}
- |> fold Splitter.add_split @{thms split_if_asm}
+ |> fold Splitter.add_split @{thms if_split_asm}
|> fold Simplifier.add_cong @{thms power_False_cong}
fun unat_arith_tacs ctxt =
@@ -4217,7 +4217,7 @@
show ?thesis
apply (unfold word_rot_defs)
- apply (simp only: split: split_if)
+ apply (simp only: split: if_split)
apply (safe intro!: abl_cong)
apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse']
to_bl_rotl
--- a/src/HOL/Word/WordBitwise.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Word/WordBitwise.thy Tue Feb 23 18:04:31 2016 +0100
@@ -572,7 +572,7 @@
val no_split_ss =
simpset_of (put_simpset HOL_ss @{context}
- |> Splitter.del_split @{thm split_if});
+ |> Splitter.del_split @{thm if_split});
val expand_word_eq_sss =
(simpset_of (put_simpset HOL_basic_ss @{context} addsimps
--- a/src/HOL/Word/Word_Miscellaneous.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Word/Word_Miscellaneous.thy Tue Feb 23 18:04:31 2016 +0100
@@ -54,7 +54,7 @@
"y = xa # list ==> size y = Suc k ==> size list = k"
by auto
-lemmas ls_splits = prod.split prod.split_asm split_if_asm
+lemmas ls_splits = prod.split prod.split_asm if_split_asm
lemma not_B1_is_B0: "y \<noteq> (1::bit) \<Longrightarrow> y = (0::bit)"
by (cases y) auto
--- a/src/HOL/ex/Cubic_Quartic.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/ex/Cubic_Quartic.thy Tue Feb 23 18:04:31 2016 +0100
@@ -142,4 +142,4 @@
apply algebra
done
-end
\ No newline at end of file
+end
--- a/src/HOL/ex/Erdoes_Szekeres.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/ex/Erdoes_Szekeres.thy Tue Feb 23 18:04:31 2016 +0100
@@ -161,4 +161,4 @@
from card_le card_eq show False by simp
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/ex/FinFunPred.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/ex/FinFunPred.thy Tue Feb 23 18:04:31 2016 +0100
@@ -142,7 +142,7 @@
lemma finfun_Ball_except_update:
"finfun_Ball_except xs (A(a $:= b)) P = ((a \<in> set xs \<or> (b \<longrightarrow> P a)) \<and> finfun_Ball_except (a # xs) A P)"
-by(fastforce simp add: finfun_Ball_except_def finfun_upd_apply split: split_if_asm)
+by(fastforce simp add: finfun_Ball_except_def finfun_upd_apply split: if_split_asm)
lemma finfun_Ball_except_update_code [code]:
fixes a :: "'a :: card_UNIV"
@@ -169,7 +169,7 @@
lemma finfun_Bex_except_update:
"finfun_Bex_except xs (A(a $:= b)) P \<longleftrightarrow> (a \<notin> set xs \<and> b \<and> P a) \<or> finfun_Bex_except (a # xs) A P"
-by(fastforce simp add: finfun_Bex_except_def finfun_upd_apply dest: bspec split: split_if_asm)
+by(fastforce simp add: finfun_Bex_except_def finfun_upd_apply dest: bspec split: if_split_asm)
lemma finfun_Bex_except_update_code [code]:
fixes a :: "'a :: card_UNIV"
@@ -265,4 +265,4 @@
end
declare iso_finfun_Ball_Ball[code_unfold del]
-end
\ No newline at end of file
+end
--- a/src/HOL/ex/Induction_Schema.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/ex/Induction_Schema.thy Tue Feb 23 18:04:31 2016 +0100
@@ -45,4 +45,4 @@
using assms
by induction_schema (pat_completeness+, lexicographic_order)
-end
\ No newline at end of file
+end
--- a/src/HOL/ex/Pythagoras.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/ex/Pythagoras.thy Tue Feb 23 18:04:31 2016 +0100
@@ -29,4 +29,4 @@
shows "vecsqnorm(vector C A) = vecsqnorm(vector B A) + vecsqnorm(vector C B)"
using o unfolding ort vc vcn by (algebra add: fst_conv snd_conv)
- end
\ No newline at end of file
+ end
--- a/src/HOL/ex/Tarski.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/ex/Tarski.thy Tue Feb 23 18:04:31 2016 +0100
@@ -659,7 +659,7 @@
apply (erule exE)
\<comment> \<open>define the lub for the interval as\<close>
apply (rule_tac x = "if S = {} then a else L" in exI)
-apply (simp (no_asm_simp) add: isLub_def split del: split_if)
+apply (simp (no_asm_simp) add: isLub_def split del: if_split)
apply (intro impI conjI)
\<comment> \<open>\<open>(if S = {} then a else L) \<in> interval r a b\<close>\<close>
apply (simp add: CL_imp_PO L_in_interval)
--- a/src/HOL/ex/Unification.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/ex/Unification.thy Tue Feb 23 18:04:31 2016 +0100
@@ -285,7 +285,7 @@
thus ?thesis by auto
qed auto
qed
-qed (auto split: split_if_asm)
+qed (auto split: if_split_asm)
text \<open>The result of a unification is either the identity
@@ -458,7 +458,7 @@
by (rule subst_eq_intro, auto simp:subst_eq_dest[OF eqv] subst_eq_dest[OF eqv2])
thus "\<exists>\<gamma>. \<sigma>' \<doteq> \<sigma> \<lozenge> \<gamma>" ..
qed
-qed (auto simp: MGU_Const intro: MGU_Var MGU_Var[symmetric] split: split_if_asm)
+qed (auto simp: MGU_Const intro: MGU_Var MGU_Var[symmetric] split: if_split_asm)
subsection \<open>Unification returns Idempotent Substitution\<close>
--- a/src/HOL/ex/While_Combinator_Example.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/ex/While_Combinator_Example.thy Tue Feb 23 18:04:31 2016 +0100
@@ -57,4 +57,4 @@
done
qed
-end
\ No newline at end of file
+end