simprules need names
authorpaulson
Thu Sep 29 17:02:57 2005 +0200 (2005-09-29)
changeset 17724e969fc0a4925
parent 17723 ee5b42e3cbb4
child 17725 d3f55965bdbf
simprules need names
src/HOL/Integ/NatBin.thy
src/HOL/List.thy
src/HOL/Map.thy
     1.1 --- a/src/HOL/Integ/NatBin.thy	Thu Sep 29 15:50:46 2005 +0200
     1.2 +++ b/src/HOL/Integ/NatBin.thy	Thu Sep 29 17:02:57 2005 +0200
     1.3 @@ -268,10 +268,10 @@
     1.4  lemma power2_eq_square: "(a::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = a * a"
     1.5    by (simp add: numeral_2_eq_2 Power.power_Suc)
     1.6  
     1.7 -lemma [simp]: "(0::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 0"
     1.8 +lemma zero_power2 [simp]: "(0::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 0"
     1.9    by (simp add: power2_eq_square)
    1.10  
    1.11 -lemma [simp]: "(1::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 1"
    1.12 +lemma one_power2 [simp]: "(1::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 1"
    1.13    by (simp add: power2_eq_square)
    1.14  
    1.15  lemma power3_eq_cube: "(x::'a::recpower) ^ 3 = x * x * x"
     2.1 --- a/src/HOL/List.thy	Thu Sep 29 15:50:46 2005 +0200
     2.2 +++ b/src/HOL/List.thy	Thu Sep 29 17:02:57 2005 +0200
     2.3 @@ -1774,7 +1774,7 @@
     2.4  apply blast
     2.5  done
     2.6  
     2.7 -lemma [simp]: "distinct xs ==> set(remove1 x xs) = set xs - {x}"
     2.8 +lemma set_remove1_eq [simp]: "distinct xs ==> set(remove1 x xs) = set xs - {x}"
     2.9  apply(induct xs)
    2.10   apply simp
    2.11  apply simp
    2.12 @@ -2180,7 +2180,7 @@
    2.13    set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
    2.14    "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
    2.15  
    2.16 -lemma [simp]: "set_Cons A {[]} = (%x. [x])`A"
    2.17 +lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
    2.18  by (auto simp add: set_Cons_def)
    2.19  
    2.20  text{*Yields the set of lists, all of the same length as the argument and
     3.1 --- a/src/HOL/Map.thy	Thu Sep 29 15:50:46 2005 +0200
     3.2 +++ b/src/HOL/Map.thy	Thu Sep 29 17:02:57 2005 +0200
     3.3 @@ -202,7 +202,7 @@
     3.4   "distinct(map fst xys) \<Longrightarrow> (Some y = map_of xys x) = ((x,y) \<in> set xys)"
     3.5  by(auto simp del:map_of_eq_Some_iff simp add:map_of_eq_Some_iff[symmetric])
     3.6  
     3.7 -lemma [simp]: "\<lbrakk> distinct(map fst xys); (x,y) \<in> set xys \<rbrakk>
     3.8 +lemma map_of_is_SomeI [simp]: "\<lbrakk> distinct(map fst xys); (x,y) \<in> set xys \<rbrakk>
     3.9    \<Longrightarrow> map_of xys x = Some y"
    3.10  apply (induct xys)
    3.11   apply simp
    3.12 @@ -553,13 +553,13 @@
    3.13  lemma map_le_empty [simp]: "empty \<subseteq>\<^sub>m g"
    3.14  by(simp add:map_le_def)
    3.15  
    3.16 -lemma [simp]: "f(x := None) \<subseteq>\<^sub>m f"
    3.17 +lemma upd_None_map_le [simp]: "f(x := None) \<subseteq>\<^sub>m f"
    3.18  by(force simp add:map_le_def)
    3.19  
    3.20  lemma map_le_upd[simp]: "f \<subseteq>\<^sub>m g ==> f(a := b) \<subseteq>\<^sub>m g(a := b)"
    3.21  by(fastsimp simp add:map_le_def)
    3.22  
    3.23 -lemma [simp]: "m1 \<subseteq>\<^sub>m m2 \<Longrightarrow> m1(x := None) \<subseteq>\<^sub>m m2(x \<mapsto> y)"
    3.24 +lemma map_le_imp_upd_le [simp]: "m1 \<subseteq>\<^sub>m m2 \<Longrightarrow> m1(x := None) \<subseteq>\<^sub>m m2(x \<mapsto> y)"
    3.25  by(force simp add:map_le_def)
    3.26  
    3.27  lemma map_le_upds[simp]: