--- a/src/HOL/Library/AssocList.thy Mon Mar 17 18:37:04 2008 +0100
+++ b/src/HOL/Library/AssocList.thy Mon Mar 17 18:37:05 2008 +0100
@@ -95,7 +95,7 @@
subsection {* @{const delete} *}
-lemma delete_def:
+lemma delete_eq:
"delete k xs = filter (\<lambda>p. fst p \<noteq> k) xs"
by (induct xs) auto
@@ -163,14 +163,14 @@
by (induct ps) auto
lemma dom_clearjunk: "fst ` set (clearjunk al) = fst ` set al"
- by (induct al rule: clearjunk.induct) (simp_all add: insert_fst_filter delete_def)
+ by (induct al rule: clearjunk.induct) (simp_all add: insert_fst_filter delete_eq)
lemma notin_filter_fst: "a \<notin> fst ` {x \<in> set ps. fst x \<noteq> a}"
by (induct ps) auto
lemma distinct_clearjunk [simp]: "distinct (map fst (clearjunk al))"
by (induct al rule: clearjunk.induct)
- (simp_all add: dom_clearjunk notin_filter_fst delete_def)
+ (simp_all add: dom_clearjunk notin_filter_fst delete_eq)
lemma map_of_filter: "k \<noteq> a \<Longrightarrow> map_of [q\<leftarrow>ps . fst q \<noteq> a] k = map_of ps k"
by (induct ps) auto
@@ -188,11 +188,11 @@
next
case (Cons p ps)
from Cons have "length (clearjunk [q\<leftarrow>ps . fst q \<noteq> fst p]) \<le> length [q\<leftarrow>ps . fst q \<noteq> fst p]"
- by (simp add: delete_def)
+ by (simp add: delete_eq)
also have "\<dots> \<le> length ps"
by simp
finally show ?case
- by (simp add: delete_def)
+ by (simp add: delete_eq)
qed
lemma notin_fst_filter: "a \<notin> fst ` set ps \<Longrightarrow> [q\<leftarrow>ps . fst q \<noteq> a] = ps"
@@ -319,7 +319,7 @@
by (induct ps) auto
lemma clearjunk_update: "clearjunk (update k v al) = update k v (clearjunk al)"
- by (induct al rule: clearjunk.induct) (auto simp add: update_filter delete_def)
+ by (induct al rule: clearjunk.induct) (auto simp add: update_filter delete_eq)
lemma update_triv: "map_of al k = Some v \<Longrightarrow> update k v al = al"
by (induct al) auto
@@ -442,7 +442,7 @@
by (induct ps) auto
lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
- by (induct al rule: clearjunk.induct) (auto simp add: delete_def map_ran_filter)
+ by (induct al rule: clearjunk.induct) (auto simp add: delete_eq map_ran_filter)
subsection {* @{const merge} *}
@@ -673,7 +673,7 @@
subsection {* @{const restrict} *}
-lemma restrict_def:
+lemma restrict_eq:
"restrict A = filter (\<lambda>p. fst p \<in> A)"
proof
fix xs
@@ -682,13 +682,13 @@
qed
lemma distinct_restr: "distinct (map fst al) \<Longrightarrow> distinct (map fst (restrict A al))"
- by (induct al) (auto simp add: restrict_def)
+ by (induct al) (auto simp add: restrict_eq)
lemma restr_conv: "map_of (restrict A al) k = ((map_of al)|` A) k"
apply (induct al)
- apply (simp add: restrict_def)
+ apply (simp add: restrict_eq)
apply (cases "k\<in>A")
- apply (auto simp add: restrict_def)
+ apply (auto simp add: restrict_eq)
done
lemma restr_conv': "map_of (restrict A al) = ((map_of al)|` A)"
@@ -697,7 +697,7 @@
lemma restr_empty [simp]:
"restrict {} al = []"
"restrict A [] = []"
- by (induct al) (auto simp add: restrict_def)
+ by (induct al) (auto simp add: restrict_eq)
lemma restr_in [simp]: "x \<in> A \<Longrightarrow> map_of (restrict A al) x = map_of al x"
by (simp add: restr_conv')
@@ -706,13 +706,13 @@
by (simp add: restr_conv')
lemma dom_restr [simp]: "fst ` set (restrict A al) = fst ` set al \<inter> A"
- by (induct al) (auto simp add: restrict_def)
+ by (induct al) (auto simp add: restrict_eq)
lemma restr_upd_same [simp]: "restrict (-{x}) (update x y al) = restrict (-{x}) al"
- by (induct al) (auto simp add: restrict_def)
+ by (induct al) (auto simp add: restrict_eq)
lemma restr_restr [simp]: "restrict A (restrict B al) = restrict (A\<inter>B) al"
- by (induct al) (auto simp add: restrict_def)
+ by (induct al) (auto simp add: restrict_eq)
lemma restr_update[simp]:
"map_of (restrict D (update x y al)) =
@@ -747,18 +747,18 @@
case True
with not_fst_a_x
have "delete x (restrict D (a#al)) = a#(delete x (restrict D al))"
- by (cases a) (simp add: restrict_def)
+ by (cases a) (simp add: restrict_eq)
also from not_fst_a_x True hyp have "\<dots> = restrict (D - {x}) (a # al)"
- by (cases a) (simp add: restrict_def)
+ by (cases a) (simp add: restrict_eq)
finally show ?thesis
using x_D by simp
next
case False
hence "delete x (restrict D (a#al)) = delete x (restrict D al)"
- by (cases a) (simp add: restrict_def)
+ by (cases a) (simp add: restrict_eq)
moreover from False not_fst_a_x
have "restrict (D - {x}) (a # al) = restrict (D - {x}) al"
- by (cases a) (simp add: restrict_def)
+ by (cases a) (simp add: restrict_eq)
ultimately
show ?thesis using x_D hyp by simp
qed
--- a/src/HOL/Library/Code_Index.thy Mon Mar 17 18:37:04 2008 +0100
+++ b/src/HOL/Library/Code_Index.thy Mon Mar 17 18:37:05 2008 +0100
@@ -45,7 +45,7 @@
shows P
by (rule assms [of "nat_of_index k"]) simp
-lemma index_induct:
+lemma index_induct_raw:
assumes "\<And>n. P (index_of_nat n)"
shows "P k"
proof -
--- a/src/HOL/Library/GCD.thy Mon Mar 17 18:37:04 2008 +0100
+++ b/src/HOL/Library/GCD.thy Mon Mar 17 18:37:05 2008 +0100
@@ -224,11 +224,11 @@
definition
lcm :: "nat \<times> nat \<Rightarrow> nat"
where
- "lcm = (\<lambda>(m, n). m * n div gcd (m, n))"
+ lcm_prim_def: "lcm = (\<lambda>(m, n). m * n div gcd (m, n))"
lemma lcm_def:
"lcm (m, n) = m * n div gcd (m, n)"
- unfolding lcm_def by simp
+ unfolding lcm_prim_def by simp
lemma prod_gcd_lcm:
"m * n = gcd (m, n) * lcm (m, n)"
--- a/src/HOL/Matrix/MatrixGeneral.thy Mon Mar 17 18:37:04 2008 +0100
+++ b/src/HOL/Matrix/MatrixGeneral.thy Mon Mar 17 18:37:05 2008 +0100
@@ -342,10 +342,10 @@
lemma Rep_combine_matrix[simp]: "f 0 0 = 0 \<Longrightarrow> Rep_matrix (combine_matrix f A B) j i = f (Rep_matrix A j i) (Rep_matrix B j i)"
by(simp add: combine_matrix_def)
-lemma combine_nrows: "f 0 0 = 0 \<Longrightarrow> nrows (combine_matrix f A B) <= max (nrows A) (nrows B)"
+lemma combine_nrows_max: "f 0 0 = 0 \<Longrightarrow> nrows (combine_matrix f A B) <= max (nrows A) (nrows B)"
by (simp add: nrows_le)
-lemma combine_ncols: "f 0 0 = 0 \<Longrightarrow> ncols (combine_matrix f A B) <= max (ncols A) (ncols B)"
+lemma combine_ncols_max: "f 0 0 = 0 \<Longrightarrow> ncols (combine_matrix f A B) <= max (ncols A) (ncols B)"
by (simp add: ncols_le)
lemma combine_nrows: "f 0 0 = 0 \<Longrightarrow> nrows A <= q \<Longrightarrow> nrows B <= q \<Longrightarrow> nrows(combine_matrix f A B) <= q"
--- a/src/HOL/TLA/Init.thy Mon Mar 17 18:37:04 2008 +0100
+++ b/src/HOL/TLA/Init.thy Mon Mar 17 18:37:05 2008 +0100
@@ -45,7 +45,7 @@
"|- (Init #False) = #False"
by (auto simp: Init_def)
-lemma Init_simps [int_rewrite]:
+lemma Init_simps1 [int_rewrite]:
"!!F. |- (Init ~F) = (~ Init F)"
"|- (Init (P --> Q)) = (Init P --> Init Q)"
"|- (Init (P & Q)) = (Init P & Init Q)"
@@ -59,13 +59,13 @@
lemma Init_stp_act: "|- (Init $P) = (Init P)"
by (auto simp add: Init_def fw_act_def fw_stp_def)
-lemmas Init_simps = Init_stp_act [int_rewrite] Init_simps
+lemmas Init_simps2 = Init_stp_act [int_rewrite] Init_simps1
lemmas Init_stp_act_rev = Init_stp_act [int_rewrite, symmetric]
lemma Init_temp: "|- (Init F) = F"
by (auto simp add: Init_def fw_temp_def)
-lemmas Init_simps = Init_temp [int_rewrite] Init_simps
+lemmas Init_simps = Init_temp [int_rewrite] Init_simps2
(* Trivial instances of the definitions that avoid introducing lambda expressions. *)
lemma Init_stp: "(sigma |= Init P) = P (st1 sigma)"
--- a/src/HOL/ZF/Games.thy Mon Mar 17 18:37:04 2008 +0100
+++ b/src/HOL/ZF/Games.thy Mon Mar 17 18:37:05 2008 +0100
@@ -375,7 +375,7 @@
declare ge_game.simps [simp del]
-lemma ge_game_def: "ge_game (G, H) = (\<forall> x. (zin x (right_options G) \<longrightarrow> \<not> ge_game (H, x)) \<and> (zin x (left_options H) \<longrightarrow> \<not> ge_game (x, G)))"
+lemma ge_game_eq: "ge_game (G, H) = (\<forall> x. (zin x (right_options G) \<longrightarrow> \<not> ge_game (H, x)) \<and> (zin x (left_options H) \<longrightarrow> \<not> ge_game (x, G)))"
apply (subst ge_game.simps[where G=G and H=H])
apply (auto)
done
@@ -391,7 +391,7 @@
proof -
have "(y, g) \<in> option_of" by (auto intro: y)
with 1 have "ge_game (y, y)" by auto
- with y show ?thesis by (subst ge_game_def, auto)
+ with y show ?thesis by (subst ge_game_eq, auto)
qed
}
note right = this
@@ -402,12 +402,12 @@
proof -
have "(y, g) \<in> option_of" by (auto intro: y)
with 1 have "ge_game (y, y)" by auto
- with y show ?thesis by (subst ge_game_def, auto)
+ with y show ?thesis by (subst ge_game_eq, auto)
qed
}
note left = this
from left right show ?case
- by (auto, subst ge_game_def, auto)
+ by (auto, subst ge_game_eq, auto)
qed
lemma ge_game_refl: "ge_game (x,x)" by (simp add: ge_game_leftright_refl)
@@ -421,19 +421,19 @@
from goal1 have "(y, g) \<in> option_of" by (auto)
with 1 have "ge_game (y, y)" by auto
with goal1 have "\<not> ge_game (g, y)"
- by (subst ge_game_def, auto)
+ by (subst ge_game_eq, auto)
with goal1 show ?case by auto}
note right = this
{case (goal2 y)
from goal2 have "(y, g) \<in> option_of" by (auto)
with 1 have "ge_game (y, y)" by auto
with goal2 have "\<not> ge_game (y, g)"
- by (subst ge_game_def, auto)
+ by (subst ge_game_eq, auto)
with goal2 show ?case by auto}
note left = this
{case goal3
from left right show ?case
- by (subst ge_game_def, auto)
+ by (subst ge_game_eq, auto)
}
qed
qed
@@ -473,7 +473,7 @@
apply (auto intro: xr lprod_3_1 simp add: prems)
done
moreover from xr have "\<not> ge_game (y, xr)"
- by (simp add: goal1(2)[simplified ge_game_def[of x y], rule_format, of xr, simplified xr])
+ by (simp add: goal1(2)[simplified ge_game_eq[of x y], rule_format, of xr, simplified xr])
ultimately have "False" by auto
}
note xr = this
@@ -485,12 +485,12 @@
apply (auto intro: zl lprod_3_2 simp add: prems)
done
moreover from zl have "\<not> ge_game (zl, y)"
- by (simp add: goal1(3)[simplified ge_game_def[of y z], rule_format, of zl, simplified zl])
+ by (simp add: goal1(3)[simplified ge_game_eq[of y z], rule_format, of zl, simplified zl])
ultimately have "False" by auto
}
note zl = this
show ?thesis
- by (auto simp add: ge_game_def[of x z] intro: xr zl)
+ by (auto simp add: ge_game_eq[of x z] intro: xr zl)
qed
qed
qed
@@ -708,7 +708,7 @@
{ fix yr
assume yr: "zin yr (right_options y)"
from hyp have "\<not> (ge_game (plus_game (x, z), plus_game (x, yr)))"
- by (auto simp add: ge_game_def[of "plus_game (x,y)" "plus_game(x,z)"]
+ by (auto simp add: ge_game_eq[of "plus_game (x,y)" "plus_game(x,z)"]
right_options_plus zunion zimage_iff intro: yr)
then have "\<not> (ge_game (z, yr))"
apply (subst induct_hyp[where y="[x, z, yr]", of "x" "z" "yr"])
@@ -719,7 +719,7 @@
{ fix zl
assume zl: "zin zl (left_options z)"
from hyp have "\<not> (ge_game (plus_game (x, zl), plus_game (x, y)))"
- by (auto simp add: ge_game_def[of "plus_game (x,y)" "plus_game(x,z)"]
+ by (auto simp add: ge_game_eq[of "plus_game (x,y)" "plus_game(x,z)"]
left_options_plus zunion zimage_iff intro: zl)
then have "\<not> (ge_game (zl, y))"
apply (subst goal1(1)[rule_format, where y="[x, zl, y]", of "x" "zl" "y"])
@@ -728,7 +728,7 @@
}
note zl = this
show "ge_game (y, z)"
- apply (subst ge_game_def)
+ apply (subst ge_game_eq)
apply (auto simp add: yr zl)
done
qed
@@ -741,7 +741,7 @@
assume x': "zin x' (right_options x)"
assume hyp: "ge_game (plus_game (x, z), plus_game (x', y))"
then have n: "\<not> (ge_game (plus_game (x', y), plus_game (x', z)))"
- by (auto simp add: ge_game_def[of "plus_game (x,z)" "plus_game (x', y)"]
+ by (auto simp add: ge_game_eq[of "plus_game (x,z)" "plus_game (x', y)"]
right_options_plus zunion zimage_iff intro: x')
have t: "ge_game (plus_game (x', y), plus_game (x', z))"
apply (subst induct_hyp[symmetric])
@@ -755,7 +755,7 @@
assume x': "zin x' (left_options x)"
assume hyp: "ge_game (plus_game (x', z), plus_game (x, y))"
then have n: "\<not> (ge_game (plus_game (x', y), plus_game (x', z)))"
- by (auto simp add: ge_game_def[of "plus_game (x',z)" "plus_game (x, y)"]
+ by (auto simp add: ge_game_eq[of "plus_game (x',z)" "plus_game (x, y)"]
left_options_plus zunion zimage_iff intro: x')
have t: "ge_game (plus_game (x', y), plus_game (x', z))"
apply (subst induct_hyp[symmetric])
@@ -791,7 +791,7 @@
}
note case4 = this
have "ge_game(plus_game (x, y), plus_game (x, z))"
- apply (subst ge_game_def)
+ apply (subst ge_game_eq)
apply (auto simp add: right_options_plus left_options_plus zunion zimage_iff)
apply (auto intro: case1 case2 case3 case4)
done
@@ -831,7 +831,7 @@
}
note yr = this
show ?case
- by (auto simp add: ge_game_def[of "neg_game x" "neg_game y"] ge_game_def[of "y" "x"]
+ by (auto simp add: ge_game_eq[of "neg_game x" "neg_game y"] ge_game_eq[of "y" "x"]
right_options_neg left_options_neg zimage_iff xl yr)
qed
}
--- a/src/HOL/ZF/HOLZF.thy Mon Mar 17 18:37:04 2008 +0100
+++ b/src/HOL/ZF/HOLZF.thy Mon Mar 17 18:37:05 2008 +0100
@@ -481,7 +481,7 @@
lemma Singleton_nonEmpty: "Singleton x \<noteq> Empty"
by (auto simp add: Singleton_def Upair_nonEmpty)
-lemma antisym_Elem: "Not(Elem a b & Elem b a)"
+lemma notsym_Elem: "Not(Elem a b & Elem b a)"
proof -
{
fix a b
@@ -504,10 +504,10 @@
qed
lemma irreflexiv_Elem: "Not(Elem a a)"
- by (simp add: antisym_Elem[of a a, simplified])
+ by (simp add: notsym_Elem[of a a, simplified])
lemma antisym_Elem: "Elem a b \<Longrightarrow> Not (Elem b a)"
- apply (insert antisym_Elem[of a b])
+ apply (insert notsym_Elem[of a b])
apply auto
done
--- a/src/HOLCF/FOCUS/Buffer_adm.thy Mon Mar 17 18:37:04 2008 +0100
+++ b/src/HOLCF/FOCUS/Buffer_adm.thy Mon Mar 17 18:37:05 2008 +0100
@@ -233,7 +233,7 @@
(**** new approach for admissibility, reduces itself to absurdity *************)
-lemma adm_BufAC_Asm: "adm (\<lambda>x. x\<in>BufAC_Asm)"
+lemma adm_BufAC_Asm': "adm (\<lambda>x. x\<in>BufAC_Asm)"
apply (rule def_gfp_admI)
apply (rule BufAC_Asm_def [THEN eq_reflection])
apply (safe)