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