# HG changeset patch # User wenzelm # Date 1205775425 -3600 # Node ID 02fbd0e7954a503cbb4afb4381d174cfedb97610 # Parent e4f40a0ea2e1273bce4c778c3e2c9f3a0854f19e avoid rebinding of existing facts; diff -r e4f40a0ea2e1 -r 02fbd0e7954a src/HOL/Library/AssocList.thy --- 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 (\p. fst p \ 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 \ fst ` {x \ set ps. fst x \ 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 \ a \ map_of [q\ps . fst q \ 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\ps . fst q \ fst p]) \ length [q\ps . fst q \ fst p]" - by (simp add: delete_def) + by (simp add: delete_eq) also have "\ \ length ps" by simp finally show ?case - by (simp add: delete_def) + by (simp add: delete_eq) qed lemma notin_fst_filter: "a \ fst ` set ps \ [q\ps . fst q \ 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 \ 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 (\p. fst p \ A)" proof fix xs @@ -682,13 +682,13 @@ qed lemma distinct_restr: "distinct (map fst al) \ 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\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 \ A \ 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 \ 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\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 "\ = 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 diff -r e4f40a0ea2e1 -r 02fbd0e7954a src/HOL/Library/Code_Index.thy --- 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 "\n. P (index_of_nat n)" shows "P k" proof - diff -r e4f40a0ea2e1 -r 02fbd0e7954a src/HOL/Library/GCD.thy --- 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 \ nat \ nat" where - "lcm = (\(m, n). m * n div gcd (m, n))" + lcm_prim_def: "lcm = (\(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)" diff -r e4f40a0ea2e1 -r 02fbd0e7954a src/HOL/Matrix/MatrixGeneral.thy --- 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 \ 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 \ nrows (combine_matrix f A B) <= max (nrows A) (nrows B)" +lemma combine_nrows_max: "f 0 0 = 0 \ nrows (combine_matrix f A B) <= max (nrows A) (nrows B)" by (simp add: nrows_le) -lemma combine_ncols: "f 0 0 = 0 \ ncols (combine_matrix f A B) <= max (ncols A) (ncols B)" +lemma combine_ncols_max: "f 0 0 = 0 \ ncols (combine_matrix f A B) <= max (ncols A) (ncols B)" by (simp add: ncols_le) lemma combine_nrows: "f 0 0 = 0 \ nrows A <= q \ nrows B <= q \ nrows(combine_matrix f A B) <= q" diff -r e4f40a0ea2e1 -r 02fbd0e7954a src/HOL/TLA/Init.thy --- 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)" diff -r e4f40a0ea2e1 -r 02fbd0e7954a src/HOL/ZF/Games.thy --- 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) = (\ x. (zin x (right_options G) \ \ ge_game (H, x)) \ (zin x (left_options H) \ \ ge_game (x, G)))" +lemma ge_game_eq: "ge_game (G, H) = (\ x. (zin x (right_options G) \ \ ge_game (H, x)) \ (zin x (left_options H) \ \ 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) \ 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) \ 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) \ option_of" by (auto) with 1 have "ge_game (y, y)" by auto with goal1 have "\ 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) \ option_of" by (auto) with 1 have "ge_game (y, y)" by auto with goal2 have "\ 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 "\ 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 "\ 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 "\ (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 "\ (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 "\ (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 "\ (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: "\ (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: "\ (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 } diff -r e4f40a0ea2e1 -r 02fbd0e7954a src/HOL/ZF/HOLZF.thy --- 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 \ 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 \ Not (Elem b a)" - apply (insert antisym_Elem[of a b]) + apply (insert notsym_Elem[of a b]) apply auto done diff -r e4f40a0ea2e1 -r 02fbd0e7954a src/HOLCF/FOCUS/Buffer_adm.thy --- 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 (\x. x\BufAC_Asm)" +lemma adm_BufAC_Asm': "adm (\x. x\BufAC_Asm)" apply (rule def_gfp_admI) apply (rule BufAC_Asm_def [THEN eq_reflection]) apply (safe)