# HG changeset patch # User nipkow # Date 823869678 -3600 # Node ID 240cc98b94a7d5894a44cd79059b35fba1d29354 # Parent b43cd8a8061f0415f7aee526fccc32ec3d2ca247 Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec' diff -r b43cd8a8061f -r 240cc98b94a7 src/HOL/Arith.ML --- a/src/HOL/Arith.ML Fri Feb 09 12:18:02 1996 +0100 +++ b/src/HOL/Arith.ML Fri Feb 09 13:41:18 1996 +0100 @@ -252,10 +252,7 @@ val prems = goal Arith.thy "m-n = 0 --> n-m = 0 --> m=n"; by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); by (REPEAT(Simp_tac 1 THEN TRY(atac 1))); -qed "diffs0_imp_equal_lemma"; - -(* [| m-n = 0; n-m = 0 |] ==> m=n *) -bind_thm ("diffs0_imp_equal", (diffs0_imp_equal_lemma RS mp RS mp)); +qed_spec_mp "diffs0_imp_equal"; val [prem] = goal Arith.thy "m 0 ? k. n = Suc(m+k)"*) -bind_thm ("less_eq_Suc_add", less_eq_Suc_add_lemma RS mp); - +qed_spec_mp "less_eq_Suc_add"; goal Arith.thy "n <= ((m + n)::nat)"; by (nat_ind_tac "m" 1); @@ -352,8 +345,7 @@ by (nat_ind_tac "k" 1); by (ALLGOALS Asm_simp_tac); by (fast_tac (HOL_cs addDs [Suc_leD]) 1); -val add_leD1_lemma = result(); -bind_thm ("add_leD1", add_leD1_lemma RS mp); +qed_spec_mp "add_leD1"; goal Arith.thy "!!k l::nat. [| k m spec_mpf (specf th a) + | _ $ (Const("op -->",_)$_$_) => spec_mpf (th RS mp) + | _ => th + +in + +fun qed_spec_mp name = bind_thm(name, spec_mpf(result())); + +end; (*** Load simpdata.ML to be able to initialize HOL's simpset ***) diff -r b43cd8a8061f -r 240cc98b94a7 src/HOL/List.ML --- a/src/HOL/List.ML Fri Feb 09 12:18:02 1996 +0100 +++ b/src/HOL/List.ML Fri Feb 09 13:41:18 1996 +0100 @@ -158,7 +158,7 @@ by (rtac allI 1); by (nat_ind_tac "n" 1); by (ALLGOALS Asm_full_simp_tac); -bind_thm("nth_map", result() RS spec RS mp); +qed_spec_mp "nth_map"; Addsimps [nth_map]; goal List.thy "!n. n < length xs --> list_all P xs --> P(nth n xs)"; @@ -169,7 +169,7 @@ by (rtac allI 1); by (nat_ind_tac "n" 1); by (ALLGOALS Asm_full_simp_tac); -bind_thm("list_all_nth", result() RS spec RS mp RS mp); +qed_spec_mp "list_all_nth"; goal List.thy "!n. n < length xs --> (nth n xs) mem xs"; by (list.induct_tac "xs" 1); @@ -182,7 +182,7 @@ by (Asm_full_simp_tac 1); (* case Suc x *) by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1); -bind_thm ("nth_mem",result() RS spec RS mp); +qed_spec_mp "nth_mem"; Addsimps [nth_mem]; (** drop **) diff -r b43cd8a8061f -r 240cc98b94a7 src/HOL/Nat.ML --- a/src/HOL/Nat.ML Fri Feb 09 12:18:02 1996 +0100 +++ b/src/HOL/Nat.ML Fri Feb 09 13:41:18 1996 +0100 @@ -343,7 +343,7 @@ by(nat_ind_tac "k" 1); by(ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq]))); by(fast_tac (HOL_cs addDs [Suc_lessD]) 1); -bind_thm("less_trans_Suc",result() RS mp); +qed_spec_mp "less_trans_Suc"; (*"Less than" is a linear ordering*) goal Nat.thy "m