src/HOL/HOL.thy
 changeset 62390 842917225d56 parent 62151 dc4c9748a86e child 62521 6383440f41a8
```     1.1 --- a/src/HOL/HOL.thy	Tue Feb 23 15:37:18 2016 +0100
1.2 +++ b/src/HOL/HOL.thy	Tue Feb 23 16:25:08 2016 +0100
1.3 @@ -988,7 +988,7 @@
1.4
1.5
1.6  lemma cases_simp: "((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q)) = Q"
1.7 -  \<comment> \<open>Avoids duplication of subgoals after \<open>split_if\<close>, when the true and false\<close>
1.8 +  \<comment> \<open>Avoids duplication of subgoals after \<open>if_split\<close>, when the true and false\<close>
1.9    \<comment> \<open>cases boil down to the same thing.\<close>
1.10    by blast
1.11
1.12 @@ -1036,30 +1036,30 @@
1.13  lemma if_not_P: "\<not> P \<Longrightarrow> (if P then x else y) = y"
1.14    by (unfold If_def) blast
1.15
1.16 -lemma split_if: "P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))"
1.17 +lemma if_split: "P (if Q then x else y) = ((Q \<longrightarrow> P x) \<and> (\<not> Q \<longrightarrow> P y))"
1.18    apply (rule case_split [of Q])
1.19     apply (simplesubst if_P)
1.20      prefer 3 apply (simplesubst if_not_P, blast+)
1.21    done
1.22
1.23 -lemma split_if_asm: "P (if Q then x else y) = (\<not> ((Q \<and> \<not> P x) \<or> (\<not> Q \<and> \<not> P y)))"
1.24 -by (simplesubst split_if, blast)
1.25 +lemma if_split_asm: "P (if Q then x else y) = (\<not> ((Q \<and> \<not> P x) \<or> (\<not> Q \<and> \<not> P y)))"
1.26 +by (simplesubst if_split, blast)
1.27
1.28 -lemmas if_splits [no_atp] = split_if split_if_asm
1.29 +lemmas if_splits [no_atp] = if_split if_split_asm
1.30
1.31  lemma if_cancel: "(if c then x else x) = x"
1.32 -by (simplesubst split_if, blast)
1.33 +by (simplesubst if_split, blast)
1.34
1.35  lemma if_eq_cancel: "(if x = y then y else x) = x"
1.36 -by (simplesubst split_if, blast)
1.37 +by (simplesubst if_split, blast)
1.38
1.39  lemma if_bool_eq_conj: "(if P then Q else R) = ((P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R))"
1.40    \<comment> \<open>This form is useful for expanding \<open>if\<close>s on the RIGHT of the \<open>\<Longrightarrow>\<close> symbol.\<close>
1.41 -  by (rule split_if)
1.42 +  by (rule if_split)
1.43
1.44  lemma if_bool_eq_disj: "(if P then Q else R) = ((P \<and> Q) \<or> (\<not> P \<and> R))"
1.45    \<comment> \<open>And this form is useful for expanding \<open>if\<close>s on the LEFT.\<close>
1.46 -  by (simplesubst split_if) blast
1.47 +  by (simplesubst if_split) blast
1.48
1.49  lemma Eq_TrueI: "P \<Longrightarrow> P \<equiv> True" by (unfold atomize_eq) iprover
1.50  lemma Eq_FalseI: "\<not> P \<Longrightarrow> P \<equiv> False" by (unfold atomize_eq) iprover
1.51 @@ -1303,7 +1303,7 @@
1.52    simp_thms
1.53
1.54  lemmas [cong] = imp_cong simp_implies_cong
1.55 -lemmas [split] = split_if
1.56 +lemmas [split] = if_split
1.57
1.58  ML \<open>val HOL_ss = simpset_of @{context}\<close>
1.59
```