# HG changeset patch # User nipkow # Date 1456241108 -3600 # Node ID 842917225d56c8133c685a3865a194c23c1d7e98 # Parent 29800666e526518837280719398dbb6cec061f23 more canonical names diff -r 29800666e526 -r 842917225d56 src/HOL/Auth/Guard/Extensions.thy --- a/src/HOL/Auth/Guard/Extensions.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Auth/Guard/Extensions.thy Tue Feb 23 16:25:08 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] diff -r 29800666e526 -r 842917225d56 src/HOL/Auth/Guard/Guard.thy --- a/src/HOL/Auth/Guard/Guard.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Auth/Guard/Guard.thy Tue Feb 23 16:25:08 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 diff -r 29800666e526 -r 842917225d56 src/HOL/Auth/Guard/GuardK.thy --- a/src/HOL/Auth/Guard/GuardK.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Auth/Guard/GuardK.thy Tue Feb 23 16:25:08 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 diff -r 29800666e526 -r 842917225d56 src/HOL/Auth/Guard/Guard_Shared.thy --- a/src/HOL/Auth/Guard/Guard_Shared.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Auth/Guard/Guard_Shared.thy Tue Feb 23 16:25:08 2016 +0100 @@ -198,4 +198,4 @@ with \agt K \ bad\ show False by simp qed -end \ No newline at end of file +end diff -r 29800666e526 -r 842917225d56 src/HOL/Auth/Guard/P1.thy --- a/src/HOL/Auth/Guard/P1.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Auth/Guard/P1.thy Tue Feb 23 16:25:08 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 diff -r 29800666e526 -r 842917225d56 src/HOL/Auth/Guard/P2.thy --- a/src/HOL/Auth/Guard/P2.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Auth/Guard/P2.thy Tue Feb 23 16:25:08 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 diff -r 29800666e526 -r 842917225d56 src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Auth/Message.thy Tue Feb 23 16:25:08 2016 +0100 @@ -468,7 +468,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 \split_if\; apparently +but can cause subgoals to blow up! Use with \if_split\; apparently \split_tac\ does not cope with patterns such as @{term"analz (insert (Crypt K X) H)"}\ lemma analz_Crypt_if [simp]: diff -r 29800666e526 -r 842917225d56 src/HOL/BNF_Cardinal_Order_Relation.thy --- a/src/HOL/BNF_Cardinal_Order_Relation.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Tue Feb 23 16:25:08 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 \ Pow A" "A2 \ 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 diff -r 29800666e526 -r 842917225d56 src/HOL/Bali/AxCompl.thy --- a/src/HOL/Bali/AxCompl.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Bali/AxCompl.thy Tue Feb 23 16:25:08 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: "\nyinitcls G s = {}; is_class G C\ \ 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': "\s\|s';inited C (globs s)\ \ inited C (globs s')" @@ -597,7 +597,7 @@ with abrupt_s' have "G\s' \c\ 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$abupd (absorb (Cont l)) s') \l\ While(e) c\ s'" @@ -1072,7 +1072,7 @@ apply (rule ax_derivs.NewA [where ?Q = "(\Y' s' s. normal s \ G\s \In1r (init_comp_ty T) \\ (Y',s')) \. G\init\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) diff -r 29800666e526 -r 842917225d56 src/HOL/Bali/AxExample.thy --- a/src/HOL/Bali/AxExample.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Bali/AxExample.thy Tue Feb 23 16:25:08 2016 +0100 @@ -37,7 +37,7 @@ done -declare split_if_asm [split del] +declare if_split_asm [split del] declare lvar_def [simp] ML \ @@ -202,7 +202,7 @@ apply (tactic "ax_tac @{context} 2" (* StatRef *)) apply (rule ax_derivs.Done [THEN conseq1]) apply (tactic \inst1_tac @{context} "Q" "\vf. Normal ((\Y s Z. vf=lvar (VName e) (snd s)) \. heap_free four \. initd Base \. initd Ext)" []$ -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) diff -r 29800666e526 -r 842917225d56 src/HOL/Bali/AxSem.thy --- a/src/HOL/Bali/AxSem.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Bali/AxSem.thy Tue Feb 23 16:25:08 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 \map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\ setup \map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\ diff -r 29800666e526 -r 842917225d56 src/HOL/Bali/AxSound.thy --- a/src/HOL/Bali/AxSound.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Bali/AxSound.thy Tue Feb 23 16:25:08 2016 +0100 @@ -1356,12 +1356,12 @@ proof - from s2_no_return s3 have "abrupt s3 \ 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)\\(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 \v\\<^sub>e s4 Z" @@ -1923,7 +1923,7 @@ from wt obtain wt_e: "\prg=G, cls=accC, lcl=L\\e\-PrimT Boolean" and wt_then_else: "\prg=G,cls=accC,lcl=L\\(if the_Bool b then c1 else c2)\\" - by cases (simp split: split_if) + by cases (simp split: if_split) from da obtain E S where da_e: "\prg=G,cls=accC,lcl=L\\ dom (locals (store s0)) \\e\\<^sub>e\ E" and da_then_else: @@ -2587,7 +2587,7 @@ from this wt_super wf have s1_no_ret: "\ j. abrupt s1 \ Some (Jump j)" by - (rule eval_statement_no_jump - [where ?Env="\prg=G,cls=accC,lcl=L\"], auto split: split_if) + [where ?Env="\prg=G,cls=accC,lcl=L\"], auto split: if_split) with conf_s1 show ?thesis by (cases s1) (auto intro: conforms_set_locals) diff -r 29800666e526 -r 842917225d56 src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Bali/Basis.thy Tue Feb 23 16:25:08 2016 +0100 @@ -11,7 +11,7 @@ ML \fun strip_tac ctxt i = REPEAT (resolve_tac ctxt [impI, allI] i)\ -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 \map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\ declare if_weak_cong [cong del] option.case_cong_weak [cong del] declare length_Suc_conv [iff] diff -r 29800666e526 -r 842917225d56 src/HOL/Bali/Eval.thy --- a/src/HOL/Bali/Eval.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Bali/Eval.thy Tue Feb 23 16:25:08 2016 +0100 @@ -753,7 +753,7 @@ \ -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\(Some xc,s) \halloc oi\a\ s'" @@ -819,7 +819,7 @@ declare not_None_eq [simp] (* IntDef.Zero_def [simp] *) declare split_paired_All [simp] split_paired_Ex [simp] declaration \K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac)))\ -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\s \t\\ (w,s') \ (\C. t=In1r (Init C) \ 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\s \halloc oi\a \ s' \ G\s \halloc oi\a' \ s'' \ a' = a \ 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\s \sxalloc\ s' \ G\s \sxalloc\ s'' \ 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\s \sxalloc\ s'}" @@ -1166,12 +1166,12 @@ [strip_tac @{context}, rotate_tac ~1, eresolve_tac @{context} @{thms eval_elim_cases}])\) (* 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 diff -r 29800666e526 -r 842917225d56 src/HOL/Bali/Evaln.thy --- a/src/HOL/Bali/Evaln.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Bali/Evaln.thy Tue Feb 23 16:25:08 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\Norm s \In1l ({accC,statT,mode}e\mn({pT}p)) \\n\ (v, s')" "G\Norm s \In1r (Init C) \\n\ (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}])\) (* 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]] diff -r 29800666e526 -r 842917225d56 src/HOL/Bali/Example.thy --- a/src/HOL/Bali/Example.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Bali/Example.thy Tue Feb 23 16:25:08 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) diff -r 29800666e526 -r 842917225d56 src/HOL/Bali/State.thy --- a/src/HOL/Bali/State.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Bali/State.thy Tue Feb 23 16:25:08 2016 +0100 @@ -501,7 +501,7 @@ "P (abrupt_if c x' x) = ((c \ x = None \ P x') \ (\ (c \ x = None) \ 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 \ 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) \ 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]: "\error_free s; \ (\ err. x=Error err)\ \ 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]: "\error_free (a,s); \ (\ err. x=Error err)\ \ 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 diff -r 29800666e526 -r 842917225d56 src/HOL/Bali/Term.thy --- a/src/HOL/Bali/Term.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Bali/Term.thy Tue Feb 23 16:25:08 2016 +0100 @@ -482,4 +482,4 @@ "\binop\CondAnd; binop\CondOr\ \ need_second_arg binop b" by (cases binop) (simp_all add: need_second_arg_def) -end \ No newline at end of file +end diff -r 29800666e526 -r 842917225d56 src/HOL/Bali/Trans.thy --- a/src/HOL/Bali/Trans.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Bali/Trans.thy Tue Feb 23 16:25:08 2016 +0100 @@ -370,4 +370,4 @@ *) -end \ No newline at end of file +end diff -r 29800666e526 -r 842917225d56 src/HOL/Bali/TypeSafe.thy --- a/src/HOL/Bali/TypeSafe.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Bali/TypeSafe.thy Tue Feb 23 16:25:08 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\Norm s1 \Init C\ s2 \ 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 \map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\ setup \map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\ @@ -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 \map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\ setup \map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\ @@ -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 \map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\ setup \map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\ @@ -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 \map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\ setup \map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\ diff -r 29800666e526 -r 842917225d56 src/HOL/Bali/WellForm.thy --- a/src/HOL/Bali/WellForm.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Bali/WellForm.thy Tue Feb 23 16:25:08 2016 +0100 @@ -2410,7 +2410,7 @@ | Inr Ts \ 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], diff -r 29800666e526 -r 842917225d56 src/HOL/Bali/WellType.thy --- a/src/HOL/Bali/WellType.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Bali/WellType.thy Tue Feb 23 16:25:08 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 \map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\ @@ -492,7 +492,7 @@ "E,dt\In1r (c1 Finally c2) \x" "E,dt\In1r (Init C) \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 \map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\ @@ -655,7 +655,7 @@ G = prg E \ (\T'. E,dt\t\T' \ 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 \ALLGOALS (fn i => @@ -666,7 +666,7 @@ else Rule_Insts.thin_tac @{context} "All P" [(@{binding P}, NONE, NoSyn)] i)\) (*apply (safe del: disjE elim!: wt_elim_cases)*) apply (tactic \ALLGOALS (eresolve_tac @{context} @{thms wt_elim_cases})\) -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 diff -r 29800666e526 -r 842917225d56 src/HOL/Cardinals/Cardinal_Arithmetic.thy --- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Tue Feb 23 16:25:08 2016 +0100 @@ -226,7 +226,7 @@ def f \ "\y a. if y = x \ a \ A then x else undefined" have "Func A {x} \ 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 \ "\(x::'a,y) b. if A = {} then undefined else if b then x else y" have "Func (UNIV :: bool set) A \ f ` (A \ 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 \ 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 \ A| =o |Func (UNIV :: bool set) A|" using card_of_ordIso by blast diff -r 29800666e526 -r 842917225d56 src/HOL/Cardinals/Ordinal_Arithmetic.thy --- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy Tue Feb 23 16:25:08 2016 +0100 @@ -1064,7 +1064,7 @@ lemma FinFunc_singleton: "FinFunc {(z,z)} s = {\x. if x \ 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 \ Field t then r.zero else undefined" from *(4) x(2) the_inv_into_f_eq[OF *(1)] have FLR: "F ` Field ?L \ 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 \ FinFunc r s" "h \ FinFunc r s" "\y. F g y = F h y" diff -r 29800666e526 -r 842917225d56 src/HOL/Complete_Lattices.thy --- a/src/HOL/Complete_Lattices.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Complete_Lattices.thy Tue Feb 23 16:25:08 2016 +0100 @@ -1247,7 +1247,7 @@ by blast lemma Un_eq_UN: "A \ B = (\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: "(\b. A b) = (A True \ A False)" by (fact SUP_UNIV_bool_expand) diff -r 29800666e526 -r 842917225d56 src/HOL/Data_Structures/AA_Set.thy --- a/src/HOL/Data_Structures/AA_Set.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Data_Structures/AA_Set.thy Tue Feb 23 16:25:08 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 diff -r 29800666e526 -r 842917225d56 src/HOL/Data_Structures/Isin2.thy --- a/src/HOL/Data_Structures/Isin2.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Data_Structures/Isin2.thy Tue Feb 23 16:25:08 2016 +0100 @@ -23,4 +23,4 @@ lemma isin_set: "sorted(inorder t) \ isin t x = (x \ elems(inorder t))" by (induction t) (auto simp: elems_simps2) -end \ No newline at end of file +end diff -r 29800666e526 -r 842917225d56 src/HOL/Data_Structures/Lookup2.thy --- a/src/HOL/Data_Structures/Lookup2.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Data_Structures/Lookup2.thy Tue Feb 23 16:25:08 2016 +0100 @@ -18,4 +18,4 @@ "sorted1(inorder t) \ 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 diff -r 29800666e526 -r 842917225d56 src/HOL/Data_Structures/Tree2.thy --- a/src/HOL/Data_Structures/Tree2.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Data_Structures/Tree2.thy Tue Feb 23 16:25:08 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 diff -r 29800666e526 -r 842917225d56 src/HOL/Datatype_Examples/Derivation_Trees/Prelim.thy --- a/src/HOL/Datatype_Examples/Derivation_Trees/Prelim.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Datatype_Examples/Derivation_Trees/Prelim.thy Tue Feb 23 16:25:08 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 diff -r 29800666e526 -r 842917225d56 src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Decision_Procs/Approximation.thy Tue Feb 23 16:25:08 2016 +0100 @@ -182,7 +182,7 @@ "(l1, u1) = float_power_bnds prec n l u \ x \ {l .. u} \ (x::real) ^ n \ {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 \ 0" "\(l1 = 0 \ (u1 = 0 \ l2 \ 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) \ {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' (\ l u. 0 \ l)" and "approx_tse_form' prec t (Add x (Minus lf)) s l u' (\ l u. 0 \ 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) diff -r 29800666e526 -r 842917225d56 src/HOL/Decision_Procs/Polynomial_List.thy --- a/src/HOL/Decision_Procs/Polynomial_List.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy Tue Feb 23 16:25:08 2016 +0100 @@ -908,16 +908,16 @@ unfolding pnormal_def by simp lemma (in semiring_0) pnormal_tail: "p \ [] \ pnormal (c # p) \ 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 \ last p \ 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 \ 0 < length p" unfolding pnormal_def length_greater_0_conv by blast lemma (in semiring_0) pnormal_last_length: "0 < length p \ last p \ 0 \ 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 \ 0 < length p \ last p \ 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 \ 0 \ 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 \ [] \ last (pnormalize p) \ 0" by (induct p) auto diff -r 29800666e526 -r 842917225d56 src/HOL/Decision_Procs/Rat_Pair.thy --- a/src/HOL/Decision_Procs/Rat_Pair.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Decision_Procs/Rat_Pair.thy Tue Feb 23 16:25:08 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 diff -r 29800666e526 -r 842917225d56 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Feb 23 16:25:08 2016 +0100 @@ -2127,4 +2127,4 @@ lemma swap_isweanpoly: "isweaknpoly p \ isweaknpoly (swap n m p)" by (induct p) auto -end \ No newline at end of file +end diff -r 29800666e526 -r 842917225d56 src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Deriv.thy Tue Feb 23 16:25:08 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 diff -r 29800666e526 -r 842917225d56 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Divides.thy Tue Feb 23 16:25:08 2016 +0100 @@ -1002,7 +1002,7 @@ assume "m \ 0" hence "\a b. divmod_nat_rel n q (a, b) \ 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) \ divmod_int_rel a b (q', r') \ 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 diff -r 29800666e526 -r 842917225d56 src/HOL/Enum.thy --- a/src/HOL/Enum.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Enum.thy Tue Feb 23 16:25:08 2016 +0100 @@ -795,13 +795,13 @@ proof(cases a "\B" rule: finite_3.exhaust[case_product finite_3.exhaust]) case a\<^sub>2_a\<^sub>3 then have "\x. x \ B \ 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 \ \B = (\b\B. a \ b)" by (cases a "\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 \ \B = (\b\B. a \ b)" by(cases a "\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 \ \B = (\b\B. a \ b)" by(cases a "\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 *: "\x. x \ A \ z \ x" show "z \ \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 *: "\x. x \ A \ x \ z" show "\A \ 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 diff -r 29800666e526 -r 842917225d56 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Finite_Set.thy Tue Feb 23 16:25:08 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 diff -r 29800666e526 -r 842917225d56 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Fun.thy Tue Feb 23 16:25:08 2016 +0100 @@ -667,7 +667,7 @@ by auto lemma fun_upd_eqD: "f(x := y) = g(x := z) \ y = z" -by(simp add: fun_eq_iff split: split_if_asm) +by(simp add: fun_eq_iff split: if_split_asm) subsection \\override_on\\ diff -r 29800666e526 -r 842917225d56 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/HOL.thy Tue Feb 23 16:25:08 2016 +0100 @@ -988,7 +988,7 @@ lemma cases_simp: "((P \ Q) \ (\ P \ Q)) = Q" - \ \Avoids duplication of subgoals after \split_if\, when the true and false\ + \ \Avoids duplication of subgoals after \if_split\, when the true and false\ \ \cases boil down to the same thing.\ by blast @@ -1036,30 +1036,30 @@ lemma if_not_P: "\ P \ (if P then x else y) = y" by (unfold If_def) blast -lemma split_if: "P (if Q then x else y) = ((Q \ P x) \ (\ Q \ P y))" +lemma if_split: "P (if Q then x else y) = ((Q \ P x) \ (\ Q \ 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) = (\ ((Q \ \ P x) \ (\ Q \ \ P y)))" -by (simplesubst split_if, blast) +lemma if_split_asm: "P (if Q then x else y) = (\ ((Q \ \ P x) \ (\ Q \ \ 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 \ Q) \ (\ P \ R))" \ \This form is useful for expanding \if\s on the RIGHT of the \\\ symbol.\ - by (rule split_if) + by (rule if_split) lemma if_bool_eq_disj: "(if P then Q else R) = ((P \ Q) \ (\ P \ R))" \ \And this form is useful for expanding \if\s on the LEFT.\ - by (simplesubst split_if) blast + by (simplesubst if_split) blast lemma Eq_TrueI: "P \ P \ True" by (unfold atomize_eq) iprover lemma Eq_FalseI: "\ P \ P \ 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 \val HOL_ss = simpset_of @{context}\ diff -r 29800666e526 -r 842917225d56 src/HOL/HOLCF/Bifinite.thy --- a/src/HOL/HOLCF/Bifinite.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/HOLCF/Bifinite.thy Tue Feb 23 16:25:08 2016 +0100 @@ -142,7 +142,7 @@ let ?S = "insert (\::'a discr u) ((\x. up\x) ` undiscr -` to_nat -` {..x = x} \ ?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 diff -r 29800666e526 -r 842917225d56 src/HOL/HOLCF/IOA/ABP/Correctness.thy --- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy Tue Feb 23 16:25:08 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 \\-->\\ 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 \Channel Abstraction\ -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 \ diff -r 29800666e526 -r 842917225d56 src/HOL/HOLCF/IOA/Deadlock.thy --- a/src/HOL/HOLCF/IOA/Deadlock.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/HOLCF/IOA/Deadlock.thy Tue Feb 23 16:25:08 2016 +0100 @@ -64,7 +64,7 @@ and "compatible A B" and "input_enabled B" shows "(sch @@ a \ nil) \ schedules (A \ B)" - supply split_if [split del] + supply if_split [split del] apply (insert assms) apply (simp add: compositionality_sch locals_def) apply (rule conjI) diff -r 29800666e526 -r 842917225d56 src/HOL/HOLCF/IOA/NTP/Correctness.thy --- a/src/HOL/HOLCF/IOA/NTP/Correctness.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/HOLCF/IOA/NTP/Correctness.thy Tue Feb 23 16:25:08 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) diff -r 29800666e526 -r 842917225d56 src/HOL/HOLCF/IOA/NTP/Impl.thy --- a/src/HOL/HOLCF/IOA/NTP/Impl.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy Tue Feb 23 16:25:08 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}) \ @@ -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 \Now the other 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}]") @@ -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 \detour 2\ 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 \Base case\ 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 \10 cases. First 4 are simple, since state doesn't change\ @@ -257,7 +257,7 @@ txt \Base case\ 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 \val tac3 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv3_def}])\ @@ -322,7 +322,7 @@ txt \Base case\ 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 \val tac4 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv4_def}])\ diff -r 29800666e526 -r 842917225d56 src/HOL/HOLCF/IOA/RefCorrectness.thy --- a/src/HOL/HOLCF/IOA/RefCorrectness.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/HOLCF/IOA/RefCorrectness.thy Tue Feb 23 16:25:08 2016 +0100 @@ -182,14 +182,14 @@ "is_ref_map f C A \ ext C = ext A \ \s. reachable C s \ is_exec_frag C (s, xs) \ 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 \cons case\ 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 diff -r 29800666e526 -r 842917225d56 src/HOL/HOLCF/IOA/RefMappings.thy --- a/src/HOL/HOLCF/IOA/RefMappings.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/HOLCF/IOA/RefMappings.thy Tue Feb 23 16:25:08 2016 +0100 @@ -66,7 +66,7 @@ lemma imp_conj_lemma: "(P \ Q \ R) \