# HG changeset patch # User clasohm # Date 812808734 -3600 # Node ID 3ae9fe3c0f68e30c74e6069432e859e096ac9195 # Parent 6ef9a9893fd6270b7d443bb678b22b08666382e7 added local simpsets diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/AxClasses/Group/GroupDefs.ML --- a/src/HOL/AxClasses/Group/GroupDefs.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/AxClasses/Group/GroupDefs.ML Wed Oct 04 13:12:14 1995 +0100 @@ -29,6 +29,8 @@ (* cartesian products *) +val prod_ss = simpset_of "Prod"; + goalw thy [times_prod_def] "(x * y) * z = x * (y * (z::'a::semigroup*'b::semigroup))"; by (simp_tac (prod_ss addsimps [assoc]) 1); qed "prod_assoc"; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/AxClasses/Tutorial/ProdGroupInsts.thy --- a/src/HOL/AxClasses/Tutorial/ProdGroupInsts.thy Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/AxClasses/Tutorial/ProdGroupInsts.thy Wed Oct 04 13:12:14 1995 +0100 @@ -15,6 +15,6 @@ instance "*" :: (semigroup, semigroup) semigroup - {| simp_tac (prod_ss addsimps [assoc]) 1 |} + {| simp_tac (!simpset addsimps [assoc]) 1 |} end diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/IMP/Denotation.ML --- a/src/HOL/IMP/Denotation.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/IMP/Denotation.ML Wed Oct 04 13:12:14 1995 +0100 @@ -8,9 +8,6 @@ (**** Rewrite Rules for A,B,C ****) -val A_simps = - [A_nat,A_loc,A_op1,A_op2]; - val B_simps = map (fn t => t RS eq_reflection) [B_true,B_false,B_op,B_not,B_and,B_or] diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/IMP/Equiv.ML --- a/src/HOL/IMP/Equiv.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/IMP/Equiv.ML Wed Oct 04 13:12:14 1995 +0100 @@ -6,19 +6,19 @@ goal Equiv.thy "!n. ( -a-> n) = (n = A a s)"; by (aexp.induct_tac "a" 1); (* struct. ind. *) -by (ALLGOALS(simp_tac (HOL_ss addsimps A_simps))); (* rewr. Den. *) +by (ALLGOALS Simp_tac); (* rewr. Den. *) by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems) addSEs evala_elim_cases))); bind_thm("aexp_iff", result() RS spec); goal Equiv.thy "!w. ( -b-> w) = (w = B b s)"; by (bexp.induct_tac "b" 1); -by (ALLGOALS(asm_simp_tac (HOL_ss addcongs [conj_cong] - addsimps (aexp_iff::B_simps@evalb_simps)))); +by (ALLGOALS(asm_simp_tac (!simpset addcongs [conj_cong] + addsimps (aexp_iff::evalb_simps)))); bind_thm("bexp_iff", result() RS spec); -val equiv_cs = comp_cs addss - (prod_ss addsimps (aexp_iff::bexp_iff::evalc.intrs)); +val equiv_cs = + comp_cs addss (simpset_of "Prod" addsimps (aexp_iff::bexp_iff::evalc.intrs)); goal Equiv.thy "!!c. -c-> t ==> (s,t) : C(c)"; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/IMP/Hoare.ML --- a/src/HOL/IMP/Hoare.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/IMP/Hoare.ML Wed Oct 04 13:12:14 1995 +0100 @@ -23,7 +23,7 @@ goalw Hoare.thy (spec_def::C_simps) "!!P. [| !s. P s --> Q(s[A a s/x]) |] ==> {{P}} x := a {{Q}}"; -by(asm_full_simp_tac prod_ss 1); +by(Asm_full_simp_tac 1); qed"hoare_assign"; goalw Hoare.thy (spec_def::C_simps) @@ -34,7 +34,7 @@ goalw Hoare.thy (spec_def::C_simps) "!!P. [| {{%s. P s & B b s}} c {{Q}}; {{%s. P s & ~B b s}} d {{Q}} |] ==> \ \ {{P}} ifc b then c else d {{Q}}"; -by(simp_tac prod_ss 1); +by(Simp_tac 1); by(fast_tac comp_cs 1); qed"hoare_if"; @@ -49,7 +49,7 @@ by (rewrite_goals_tac [Gamma_def]); by(eres_inst_tac [("x","a")] allE 1); by (safe_tac comp_cs); -by(ALLGOALS(asm_full_simp_tac prod_ss)); +by(ALLGOALS Asm_full_simp_tac); qed"hoare_while"; fun while_tac inv ss i = @@ -70,7 +70,7 @@ \ while noti(ROp op = (X u) (X y)) \ \ do (u := Op1 Suc (X u); z := Op1 Suc (X z))) \ \ {{%s. s(z)=i+j}}"; -val ss = arith_ss addsimps (eq_sym_conv::assign_def::prems@A_simps@B_simps); +val ss = !simpset addsimps (eq_sym_conv::assign_def::prems); by(hoare_tac ss); by(while_tac "%s.s z = i + s u & s y = j" ss 3); by(hoare_tac ss); diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/IOA/ABP/Action.ML --- a/src/HOL/IOA/ABP/Action.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/IOA/ABP/Action.ML Wed Oct 04 13:12:14 1995 +0100 @@ -8,6 +8,6 @@ goal Action.thy "!!x. x = y ==> action_case a b c d e f g x = \ \ action_case a b c d e f g y"; -by (asm_simp_tac HOL_ss 1); +by (Asm_simp_tac 1); -val action_ss = arith_ss addcongs [result()] addsimps Action.action.simps; +Addcongs [result()]; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/IOA/ABP/Correctness.ML --- a/src/HOL/IOA/ABP/Correctness.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/IOA/ABP/Correctness.ML Wed Oct 04 13:12:14 1995 +0100 @@ -12,33 +12,29 @@ by (fast_tac HOL_cs 1); qed"exis_elim"; -val abschannel_ss = action_ss addsimps +Addsimps ([srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def, ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, asig_of_def, actions_def, exis_elim, srch_trans_def, rsch_trans_def, ch_trans_def, - trans_of_def] - @ Option.option.simps @ act.simps @ asig_projections @ set_lemmas); + trans_of_def] @ asig_projections @ set_lemmas); val abschannel_fin = [srch_fin_asig_def, rsch_fin_asig_def, rsch_fin_ioa_def, srch_fin_ioa_def, ch_fin_ioa_def,ch_fin_trans_def,ch_fin_asig_def]; -val abschannel_fin_ss = abschannel_ss addsimps abschannel_fin; +Addsimps abschannel_fin; val impl_ioas = [Sender.sender_ioa_def,Receiver.receiver_ioa_def]; val impl_trans = [Sender.sender_trans_def,Receiver.receiver_trans_def]; val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def]; -val impl_ss = merge_ss(action_ss,list_ss) - addcongs [let_weak_cong] - addsimps [Let_def, ioa_triple_proj, starts_of_par]; +Addcongs [let_weak_cong]; +Addsimps [Let_def, ioa_triple_proj, starts_of_par]; val env_ioas = [Env.env_ioa_def,Env.env_asig_def,Env.env_trans_def]; val hom_ioas = env_ioas @ impl_ioas @ impl_trans @ impl_asigs @ asig_projections @ set_lemmas; -val hom_ss = (impl_ss addsimps hom_ioas); +Addsimps hom_ioas; -val red_ss = impl_ss addsimps [reduce_Nil,reduce_Cons]; -val red_ss_ch = merge_ss(abschannel_fin_ss,red_ss); - +Addsimps [reduce_Nil,reduce_Cons]; @@ -52,27 +48,27 @@ by (subgoal_tac "(l~=[]) --> (reduce(l)~=[])" 1); by (fast_tac HOL_cs 1); by (List.list.induct_tac "l" 1); - by (simp_tac red_ss 1); - by (simp_tac red_ss 1); + by (Simp_tac 1); + by (Simp_tac 1); by (rtac (expand_list_case RS iffD2) 1); - by (asm_full_simp_tac list_ss 1); + by (Asm_full_simp_tac 1); by (REPEAT (rtac allI 1)); by (rtac impI 1); by (hyp_subst_tac 1); by (rtac (expand_if RS ssubst) 1); - by (asm_full_simp_tac list_ss 1); - by (asm_full_simp_tac red_ss 1); + by (Asm_full_simp_tac 1); + by (Asm_full_simp_tac 1); val l_iff_red_nil = result(); goal Correctness.thy "s~=[] --> hd(s)=hd(reduce(s))"; by (List.list.induct_tac "s" 1); -by (simp_tac red_ss 1); +by (Simp_tac 1); by (case_tac "list =[]" 1); -by (asm_full_simp_tac red_ss 1); +by (Asm_full_simp_tac 1); (* main case *) by (rotate 1 1); by (asm_full_simp_tac list_ss 1); -by (simp_tac red_ss 1); +by (Simp_tac 1); by (rtac (expand_list_case RS iffD2) 1); by (asm_full_simp_tac list_ss 1); by (REPEAT (rtac allI 1)); @@ -80,31 +76,31 @@ by (rtac (expand_if RS ssubst) 1); by (REPEAT(hyp_subst_tac 1)); by (etac subst 1); -by (simp_tac list_ss 1); +by (Simp_tac 1); qed"hd_is_reduce_hd"; (* to be used in the following Lemma *) goal Correctness.thy "l~=[] --> reverse(reduce(l))~=[]"; by (List.list.induct_tac "l" 1); -by (simp_tac red_ss 1); +by (Simp_tac 1); by (case_tac "list =[]" 1); -by (asm_full_simp_tac (red_ss addsimps [reverse_Cons]) 1); +by (asm_full_simp_tac (!simpset addsimps [reverse_Cons]) 1); (* main case *) by (rotate 1 1); -by (asm_full_simp_tac red_ss 1); +by (Asm_full_simp_tac 1); by (cut_inst_tac [("l","list")] cons_not_nil 1); -by (asm_full_simp_tac list_ss 1); +by (Asm_full_simp_tac 1); by (REPEAT (etac exE 1)); -by (asm_simp_tac list_ss 1); +by (Asm_simp_tac 1); by (rtac (expand_if RS ssubst) 1); by (hyp_subst_tac 1); -by (asm_full_simp_tac (list_ss addsimps [reverse_Cons]) 1); +by (asm_full_simp_tac (!simpset addsimps [reverse_Cons]) 1); qed"rev_red_not_nil"; (* shows applicability of the induction hypothesis of the following Lemma 1 *) goal Correctness.thy "!!l.[| l~=[] |] ==> \ \ hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))"; - by (simp_tac red_ss 1); + by (Simp_tac 1); by (rtac (expand_list_case RS iffD2) 1); by (asm_full_simp_tac list_ss 1); by (REPEAT (rtac allI 1)); @@ -114,6 +110,7 @@ (rev_red_not_nil RS mp)]) 1); qed"last_ind_on_first"; +val impl_ss = !simpset delsimps [reduce_Cons]; (* Main Lemma 1 for S_pkt in showing that reduce is refinement *) goal Correctness.thy @@ -124,26 +121,26 @@ by (rtac conjI 1); (* --> *) by (List.list.induct_tac "l" 1); -by (simp_tac red_ss 1); +by (Simp_tac 1); by (case_tac "list=[]" 1); - by (asm_full_simp_tac (red_ss addsimps [reverse_Nil,reverse_Cons]) 1); + by (asm_full_simp_tac (!simpset addsimps [reverse_Nil,reverse_Cons]) 1); by (rtac impI 1); -by (simp_tac red_ss 1); +by (Simp_tac 1); by (cut_inst_tac [("l","list")] cons_not_nil 1); by (asm_full_simp_tac impl_ss 1); by (REPEAT (etac exE 1)); by (hyp_subst_tac 1); by (asm_full_simp_tac (impl_ss addsimps [last_ind_on_first,l_iff_red_nil]) 1); (* <-- *) -by (simp_tac (red_ss addsimps [and_de_morgan_and_absorbe,l_iff_red_nil]) 1); +by (simp_tac (!simpset addsimps [and_de_morgan_and_absorbe,l_iff_red_nil]) 1); by (List.list.induct_tac "l" 1); -by (simp_tac red_ss 1); +by (Simp_tac 1); by (case_tac "list=[]" 1); - by (asm_full_simp_tac (red_ss addsimps [reverse_Nil,reverse_Cons]) 1); + by (asm_full_simp_tac (!simpset addsimps [reverse_Nil,reverse_Cons]) 1); by (rtac (expand_if RS ssubst) 1); by (fast_tac HOL_cs 1); by (rtac impI 1); -by (simp_tac red_ss 1); +by (Simp_tac 1); by (cut_inst_tac [("l","list")] cons_not_nil 1); by (asm_full_simp_tac impl_ss 1); by (REPEAT (etac exE 1)); @@ -162,17 +159,17 @@ \ reduce(tl(s))=reduce(s) else \ \ reduce(tl(s))=tl(reduce(s))"; by (cut_inst_tac [("l","s")] cons_not_nil 1); -by (asm_full_simp_tac red_ss 1); +by (Asm_full_simp_tac 1); by (REPEAT (etac exE 1)); -by (asm_full_simp_tac red_ss 1); +by (Asm_full_simp_tac 1); by (rtac (expand_if RS ssubst) 1); by (rtac conjI 1); -by (simp_tac (red_ss addsimps [and_de_morgan_and_absorbe]) 2); -by (ALLGOALS (EVERY'[rtac impI,etac conjE,cut_inst_tac [("l","xs")] cons_not_nil,asm_full_simp_tac red_ss])); +by (simp_tac (!simpset addsimps [and_de_morgan_and_absorbe]) 2); +by (ALLGOALS (EVERY'[rtac impI,etac conjE,cut_inst_tac [("l","xs")] cons_not_nil,Asm_full_simp_tac])); by (REPEAT (etac exE 1)); by (REPEAT (etac exE 2)); by (REPEAT(hyp_subst_tac 2)); -by (ALLGOALS (asm_full_simp_tac red_ss)); +by (ALLGOALS (Asm_full_simp_tac)); val reduce_tl =result(); @@ -182,18 +179,18 @@ goal Correctness.thy "is_weak_pmap reduce ch_ioa ch_fin_ioa"; -by (simp_tac (red_ss addsimps [Solve.is_weak_pmap_def]) 1); +by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); by (rtac conjI 1); (* -------------- start states ----------------- *) -by (simp_tac red_ss_ch 1); +by (Simp_tac 1); br ballI 1; -by (asm_full_simp_tac red_ss_ch 1); +by (Asm_full_simp_tac 1); (* ---------------- main-part ------------------- *) by (REPEAT (rtac allI 1)); by (rtac imp_conj_lemma 1); by (act.induct_tac "a" 1); (* ----------------- 2 cases ---------------------*) -by (ALLGOALS (simp_tac (red_ss_ch addsimps [externals_def]))); +by (ALLGOALS (simp_tac (!simpset addsimps [externals_def]))); (* fst case --------------------------------------*) by (rtac impI 1); by (rtac disjI2 1); @@ -202,9 +199,9 @@ by (rtac impI 1); by (REPEAT (etac conjE 1)); by (etac disjE 1); -by (asm_full_simp_tac (red_ss addsimps [l_iff_red_nil]) 1); +by (asm_full_simp_tac (!simpset addsimps [l_iff_red_nil]) 1); by (etac (hd_is_reduce_hd RS mp) 1); -by (asm_full_simp_tac (red_ss addsimps [l_iff_red_nil]) 1); +by (asm_full_simp_tac (!simpset addsimps [l_iff_red_nil]) 1); by (rtac conjI 1); by (etac (hd_is_reduce_hd RS mp) 1); by (rtac (bool_if_impl_or RS mp) 1); @@ -228,129 +225,138 @@ the absence of internal actions. *) goal Correctness.thy "is_weak_pmap (%id.id) sender_ioa sender_ioa"; -by (simp_tac (red_ss addsimps [Solve.is_weak_pmap_def]) 1); +by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); by (rtac conjI 1); (* start states *) br ballI 1; -by (simp_tac red_ss_ch 1); +by (Simp_tac 1); (* main-part *) by (REPEAT (rtac allI 1)); by (rtac imp_conj_lemma 1); by (Action.action.induct_tac "a" 1); (* 7 cases *) -by (ALLGOALS (simp_tac ((hom_ss addsimps [externals_def]) setloop (split_tac [expand_if])))); +by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if])))); qed"sender_unchanged"; (* 2 copies of before *) goal Correctness.thy "is_weak_pmap (%id.id) receiver_ioa receiver_ioa"; -by (simp_tac (red_ss addsimps [Solve.is_weak_pmap_def]) 1); +by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); by (rtac conjI 1); (* start states *) br ballI 1; -by (simp_tac red_ss_ch 1); +by (Simp_tac 1); (* main-part *) by (REPEAT (rtac allI 1)); by (rtac imp_conj_lemma 1); by (Action.action.induct_tac "a" 1); (* 7 cases *) -by (ALLGOALS (simp_tac ((hom_ss addsimps [externals_def]) setloop (split_tac [expand_if])))); +by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if])))); qed"receiver_unchanged"; goal Correctness.thy "is_weak_pmap (%id.id) env_ioa env_ioa"; -by (simp_tac (red_ss addsimps [Solve.is_weak_pmap_def]) 1); +by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1); by (rtac conjI 1); (* start states *) br ballI 1; -by (simp_tac red_ss_ch 1); +by (Simp_tac 1); (* main-part *) by (REPEAT (rtac allI 1)); by (rtac imp_conj_lemma 1); by (Action.action.induct_tac "a" 1); (* 7 cases *) -by (ALLGOALS (simp_tac ((hom_ss addsimps [externals_def]) setloop (split_tac [expand_if])))); +by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if])))); qed"env_unchanged"; goal Correctness.thy "compat_ioas srch_ioa rsch_ioa"; -by (simp_tac (red_ss_ch addsimps [compat_ioas_def,compat_asigs_def,Int_def,empty_def]) 1); +by (simp_tac (!simpset addsimps [compat_ioas_def,compat_asigs_def,Int_def,empty_def]) 1); by (rtac set_ext 1); by (Action.action.induct_tac "x" 1); -by (ALLGOALS(simp_tac red_ss_ch)); +by (ALLGOALS(Simp_tac)); val compat_single_ch = result(); (* totally the same as before *) goal Correctness.thy "compat_ioas srch_fin_ioa rsch_fin_ioa"; -by (simp_tac (red_ss_ch addsimps [compat_ioas_def,compat_asigs_def,Int_def,empty_def]) 1); +by (simp_tac (!simpset addsimps [compat_ioas_def,compat_asigs_def,Int_def,empty_def]) 1); by (rtac set_ext 1); by (Action.action.induct_tac "x" 1); -by (ALLGOALS(simp_tac red_ss_ch)); +by (ALLGOALS(Simp_tac)); val compat_single_fin_ch = result(); +val ss = + !simpset delsimps ([trans_of_def, srch_asig_def,rsch_asig_def, + asig_of_def, actions_def, srch_trans_def, rsch_trans_def, + srch_ioa_def, srch_fin_ioa_def, rsch_fin_ioa_def, + rsch_ioa_def, Sender.sender_trans_def, + Receiver.receiver_trans_def] @ set_lemmas); + goal Correctness.thy "compat_ioas receiver_ioa (srch_ioa || rsch_ioa)"; -by (simp_tac (hom_ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); -by (simp_tac red_ss_ch 1); +by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def, + asig_of_par,asig_comp_def,actions_def, + Int_def]) 1); +by (Simp_tac 1); by (rtac set_ext 1); by (Action.action.induct_tac "x" 1); -by (ALLGOALS(simp_tac red_ss_ch)); -by (ALLGOALS(simp_tac (red_ss addsimps [insert_def,Un_def]))); -by (ALLGOALS(simp_tac (red_ss_ch addsimps [de_morgan,singleton_set]))); -val compat_rec =result(); +by (ALLGOALS Simp_tac); +by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def]))); +by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set]))); +val compat_rec = result(); (* 5 proofs totally the same as before *) goal Correctness.thy "compat_ioas receiver_ioa (srch_fin_ioa || rsch_fin_ioa)"; -by (simp_tac (hom_ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); -by (simp_tac red_ss_ch 1); +by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); +by (Simp_tac 1); by (rtac set_ext 1); by (Action.action.induct_tac "x" 1); -by (ALLGOALS(simp_tac red_ss_ch)); -by (ALLGOALS(simp_tac (red_ss addsimps [insert_def,Un_def]))); -by (ALLGOALS(simp_tac (red_ss_ch addsimps [de_morgan,singleton_set]))); +by (ALLGOALS Simp_tac); +by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def]))); +by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set]))); val compat_rec_fin =result(); goal Correctness.thy "compat_ioas sender_ioa \ \ (receiver_ioa || srch_ioa || rsch_ioa)"; -by (simp_tac (hom_ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); -by (simp_tac red_ss_ch 1); +by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); +by (Simp_tac 1); by (rtac set_ext 1); by (Action.action.induct_tac "x" 1); -by (ALLGOALS(simp_tac red_ss_ch)); -by (ALLGOALS(simp_tac (red_ss addsimps [insert_def,Un_def]))); -by (ALLGOALS(simp_tac (red_ss_ch addsimps [de_morgan,singleton_set]))); +by (ALLGOALS(Simp_tac)); +by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def]))); +by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set]))); val compat_sen=result(); goal Correctness.thy "compat_ioas sender_ioa\ \ (receiver_ioa || srch_fin_ioa || rsch_fin_ioa)"; -by (simp_tac (hom_ss addsimps [empty_def, compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); -by (simp_tac red_ss_ch 1); +by (simp_tac (ss addsimps [empty_def, compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); +by (Simp_tac 1); by (rtac set_ext 1); by (Action.action.induct_tac "x" 1); -by (ALLGOALS(simp_tac red_ss_ch)); -by (ALLGOALS(simp_tac (red_ss addsimps [insert_def,Un_def]))); -by (ALLGOALS(simp_tac (red_ss_ch addsimps [de_morgan,singleton_set]))); +by (ALLGOALS(Simp_tac)); +by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def]))); +by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set]))); val compat_sen_fin =result(); goal Correctness.thy "compat_ioas env_ioa\ \ (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"; -by (simp_tac (hom_ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); -by (simp_tac red_ss_ch 1); +by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); +by (Simp_tac 1); by (rtac set_ext 1); by (Action.action.induct_tac "x" 1); -by (ALLGOALS(simp_tac red_ss_ch)); -by (ALLGOALS(simp_tac (red_ss addsimps [insert_def,Un_def]))); -by (ALLGOALS(simp_tac (red_ss_ch addsimps [de_morgan,singleton_set]))); +by (ALLGOALS(Simp_tac)); +by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def]))); +by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set]))); val compat_env=result(); goal Correctness.thy "compat_ioas env_ioa\ \ (sender_ioa || receiver_ioa || srch_fin_ioa || rsch_fin_ioa)"; -by (simp_tac (hom_ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); -by (simp_tac red_ss_ch 1); +by (simp_tac (ss addsimps [empty_def,compat_ioas_def,compat_asigs_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1); +by (Simp_tac 1); by (rtac set_ext 1); by (Action.action.induct_tac "x" 1); -by (ALLGOALS(simp_tac red_ss_ch)); -by (ALLGOALS(simp_tac (red_ss addsimps [insert_def,Un_def]))); -by (ALLGOALS(simp_tac (red_ss_ch addsimps [de_morgan,singleton_set]))); +by (ALLGOALS Simp_tac); +by (ALLGOALS(simp_tac (!simpset addsimps [insert_def,Un_def]))); +by (ALLGOALS(simp_tac (!simpset addsimps [de_morgan,singleton_set]))); val compat_env_fin=result(); @@ -358,7 +364,7 @@ goal Correctness.thy "externals(asig_of(srch_fin_ioa)) = externals(asig_of(srch_ioa)) & \ \ externals(asig_of(rsch_fin_ioa)) = externals(asig_of(rsch_ioa))"; -by (simp_tac (red_ss_ch addsimps [externals_def]) 1); +by (simp_tac (!simpset addsimps [externals_def]) 1); val ext_single_ch = result(); @@ -370,27 +376,28 @@ compat_rec_fin,compat_sen,compat_sen_fin,compat_env,compat_env_fin]; val abstractions = [env_unchanged,sender_unchanged, receiver_unchanged,sender_abstraction,receiver_abstraction]; -val impl_ss = impl_ss addsimps [impl_def,impl_fin_def,sys_IOA, sys_fin_IOA]; -val sys_ss = impl_ss addsimps [system_def, system_fin_def, abs_def]; - (************************************************************************ S o u n d n e s s o f A b s t r a c t i o n *************************************************************************) +val ss = !simpset delsimps ([asig_of_def, srch_ioa_def, rsch_ioa_def, + srch_fin_ioa_def, rsch_fin_ioa_def] @ + impl_ioas @ env_ioas); goal Correctness.thy "is_weak_pmap abs system_ioa system_fin_ioa"; -by (simp_tac sys_ss 1); +by (simp_tac (impl_ss delsimps ([srch_ioa_def, rsch_ioa_def, srch_fin_ioa_def, + rsch_fin_ioa_def] @ env_ioas @ impl_ioas) + addsimps [system_def, system_fin_def, abs_def, impl_def, + impl_fin_def, sys_IOA, sys_fin_IOA]) 1); by (REPEAT (EVERY[rtac fxg_is_weak_pmap_of_product_IOA 1, - simp_tac (red_ss addsimps abstractions) 1, + simp_tac (ss addsimps abstractions) 1, rtac conjI 1])); -by (ALLGOALS (simp_tac (red_ss addsimps ext_ss @ compat_ss))); +by (ALLGOALS (simp_tac (ss addsimps ext_ss @ compat_ss))); qed "system_refinement"; - - diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/IOA/ABP/Lemmas.ML --- a/src/HOL/IOA/ABP/Lemmas.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/IOA/ABP/Lemmas.ML Wed Oct 04 13:12:14 1995 +0100 @@ -42,6 +42,8 @@ (* Lists *) +val list_ss = simpset_of "List"; + goal List.thy "hd(l@m) = (if l~=[] then hd(l) else hd(m))"; by (List.list.induct_tac "l" 1); by (simp_tac list_ss 1); diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/IOA/NTP/Abschannel.ML --- a/src/HOL/IOA/NTP/Abschannel.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/IOA/NTP/Abschannel.ML Wed Oct 04 13:12:14 1995 +0100 @@ -8,12 +8,11 @@ open Abschannel; -val abschannel_ss = action_ss addsimps +Addsimps ([srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def, ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, asig_of_def, actions_def, srch_trans_def, rsch_trans_def, ch_trans_def,starts_of_def, - trans_of_def] - @ Option.option.simps @ act.simps @ asig_projections @ set_lemmas); + trans_of_def] @ asig_projections @ set_lemmas); goal Abschannel.thy "S_msg(m) ~: actions(srch_asig) & \ @@ -26,7 +25,7 @@ \ C_m_r ~: actions(srch_asig) & \ \ C_r_s ~: actions(srch_asig) & C_r_r(m) ~: actions(srch_asig)"; -by(simp_tac abschannel_ss 1); +by(Simp_tac 1); qed"in_srch_asig"; goal Abschannel.thy @@ -41,14 +40,14 @@ \ C_r_s ~: actions(rsch_asig) & \ \ C_r_r(m) ~: actions(rsch_asig)"; -by(simp_tac abschannel_ss 1); +by(Simp_tac 1); qed"in_rsch_asig"; goal Abschannel.thy "srch_ioa = (srch_asig, {{|}}, srch_trans)"; -by (simp_tac (abschannel_ss addsimps [starts_of_def]) 1); +by (Simp_tac 1); qed"srch_ioa_thm"; goal Abschannel.thy "rsch_ioa = (rsch_asig, {{|}}, rsch_trans)"; -by (simp_tac (abschannel_ss addsimps [starts_of_def]) 1); +by (Simp_tac 1); qed"rsch_ioa_thm"; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/IOA/NTP/Action.ML --- a/src/HOL/IOA/NTP/Action.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/IOA/NTP/Action.ML Wed Oct 04 13:12:14 1995 +0100 @@ -8,6 +8,6 @@ goal Action.thy "!!x. x = y ==> action_case a b c d e f g h i j x = \ \ action_case a b c d e f g h i j y"; -by (asm_simp_tac HOL_ss 1); +by (Asm_simp_tac 1); -val action_ss = arith_ss addcongs [result()] addsimps Action.action.simps; +Addcongs [result()]; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/IOA/NTP/Correctness.ML --- a/src/HOL/IOA/NTP/Correctness.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/IOA/NTP/Correctness.ML Wed Oct 04 13:12:14 1995 +0100 @@ -9,16 +9,27 @@ open Impl; open Spec; -val hom_ss = impl_ss; val hom_ioas = [Spec.ioa_def, Spec.trans_def, Sender.sender_trans_def,Receiver.receiver_trans_def] @ impl_ioas; -val hom_ss' = hom_ss addsimps hom_ioas; +Addsimps hom_ioas; val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def, Abschannel.srch_asig_def,Abschannel.rsch_asig_def]; +val ss = + !simpset delsimps ([trans_of_def, starts_of_def, srch_asig_def,rsch_asig_def, + asig_of_def, actions_def, srch_trans_def, rsch_trans_def, + impl_def, srch_ioa_thm, rsch_ioa_thm, srch_ioa_def, + rsch_ioa_def, Sender.sender_trans_def, + Receiver.receiver_trans_def] @ set_lemmas); + +val ss' = !simpset delsimps [trans_of_def, srch_asig_def, rsch_asig_def, + srch_trans_def, rsch_trans_def, asig_of_def, + actions_def] + addcongs [let_weak_cong]; + (* A lemma about restricting the action signature of the implementation * to that of the specification. @@ -36,25 +47,22 @@ \ | C_m_r => False \ \ | C_r_s => False \ \ | C_r_r(m) => False)"; - by(simp_tac (hom_ss addcongs [if_weak_cong] - addsimps ([externals_def, restrict_def, restrict_asig_def, - Spec.sig_def] @ asig_projections)) 1); + by(simp_tac (ss addcongs [if_weak_cong] + addsimps ([externals_def, restrict_def, + restrict_asig_def, Spec.sig_def])) 1); by(Action.action.induct_tac "a" 1); - by(ALLGOALS(simp_tac (action_ss addsimps - (actions_def :: asig_projections @ set_lemmas)))); + by(ALLGOALS(simp_tac (ss addsimps (actions_def :: set_lemmas)))); (* 2 *) - by (simp_tac (hom_ss addsimps impl_ioas) 1); - by (simp_tac (hom_ss addsimps impl_asigs) 1); - by(simp_tac (hom_ss addsimps ([asig_of_par, asig_comp_def] - @ asig_projections)) 1); - by (simp_tac abschannel_ss 1); + by (simp_tac (ss addsimps impl_ioas) 1); + by (simp_tac (ss addsimps impl_asigs) 1); + by (simp_tac (ss addsimps ([asig_of_par, asig_comp_def])) 1); + by (simp_tac (!simpset delsimps [srch_ioa_thm, rsch_ioa_thm, Let_def]) 1); (* 1 *) - by (simp_tac (hom_ss addsimps impl_ioas) 1); - by (simp_tac (hom_ss addsimps impl_asigs) 1); - by(simp_tac (hom_ss addsimps ([asig_of_par, asig_comp_def] - @ asig_projections)) 1); - by (simp_tac abschannel_ss 1); + by (simp_tac (ss addsimps impl_ioas) 1); + by (simp_tac (ss addsimps impl_asigs) 1); + by (simp_tac (ss addsimps ([asig_of_par, asig_comp_def])) 1); + by (simp_tac (!simpset delsimps [srch_ioa_thm, rsch_ioa_thm, Let_def]) 1); qed "externals_lemma"; @@ -64,53 +72,51 @@ (* Proof of correctness *) goalw Correctness.thy [Spec.ioa_def, Solve.is_weak_pmap_def] "is_weak_pmap hom (restrict impl_ioa (externals spec_sig)) spec_ioa"; -by(simp_tac (hom_ss addsimps +by(simp_tac (ss delsimps [trans_def] addsimps (Correctness.hom_def::[cancel_restrict,externals_lemma])) 1); br conjI 1; -by(simp_tac (hom_ss addsimps impl_ioas) 1); +by(simp_tac (ss addsimps impl_ioas) 1); br ballI 1; bd CollectD 1; -by(asm_simp_tac (hom_ss addsimps sels) 1); +by(asm_simp_tac (!simpset addsimps sels) 1); by(REPEAT(rtac allI 1)); br imp_conj_lemma 1; (* from lemmas.ML *) by(Action.action.induct_tac "a" 1); -by(asm_simp_tac (hom_ss' setloop (split_tac [expand_if])) 1); +by(asm_simp_tac (ss' setloop (split_tac [expand_if])) 1); by(forward_tac [inv4] 1); -by(asm_full_simp_tac (hom_ss addsimps - [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1); -by(simp_tac hom_ss' 1); -by(simp_tac hom_ss' 1); -by(simp_tac hom_ss' 1); -by(simp_tac hom_ss' 1); -by(simp_tac hom_ss' 1); -by(simp_tac hom_ss' 1); -by(simp_tac hom_ss' 1); +by(asm_full_simp_tac (ss addsimps [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1); +by(simp_tac ss' 1); +by(simp_tac ss' 1); +by(simp_tac ss' 1); +by(simp_tac ss' 1); +by(simp_tac ss' 1); +by(simp_tac ss' 1); +by(simp_tac ss' 1); -by(asm_simp_tac hom_ss' 1); +by(asm_simp_tac ss' 1); by(forward_tac [inv4] 1); by(forward_tac [inv2] 1); be disjE 1; -by(asm_simp_tac hom_ss 1); -by(asm_full_simp_tac (hom_ss addsimps - [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1); +by(asm_simp_tac ss 1); +by(asm_full_simp_tac (ss addsimps [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1); -by(asm_simp_tac hom_ss' 1); +by(asm_simp_tac ss' 1); by(forward_tac [inv2] 1); be disjE 1; by(forward_tac [inv3] 1); by(case_tac "sq(sen(s))=[]" 1); -by(asm_full_simp_tac hom_ss' 1); +by(asm_full_simp_tac ss' 1); by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1); by(case_tac "m = hd(sq(sen(s)))" 1); -by(asm_full_simp_tac (hom_ss addsimps +by(asm_full_simp_tac (ss addsimps [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1); -by(asm_full_simp_tac hom_ss 1); +by(asm_full_simp_tac ss 1); by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1); -by(asm_full_simp_tac hom_ss 1); +by(asm_full_simp_tac ss 1); result(); diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/IOA/NTP/Impl.ML --- a/src/HOL/IOA/NTP/Impl.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/IOA/NTP/Impl.ML Wed Oct 04 13:12:14 1995 +0100 @@ -19,74 +19,78 @@ Abschannel.srch_trans_def, Abschannel.rsch_trans_def]; -val impl_ss = merge_ss(action_ss,list_ss) - addcongs [let_weak_cong] - addsimps [Let_def, ioa_triple_proj, starts_of_par, trans_of_par4, - in_sender_asig, in_receiver_asig, in_srch_asig, - in_rsch_asig, count_addm_simp, count_delm_simp, - Multiset.countm_empty_def, Multiset.delm_empty_def, - (* Multiset.count_def, *) count_empty, - Packet.hdr_def, Packet.msg_def]; +Addsimps [ioa_triple_proj, starts_of_par, trans_of_par4, + in_sender_asig, in_receiver_asig, in_srch_asig, + in_rsch_asig, count_addm_simp, count_delm_simp, + Multiset.countm_empty_def, Multiset.delm_empty_def, + (* Multiset.count_def, *) count_empty, + Packet.hdr_def, Packet.msg_def]; goal Impl.thy "fst(x) = sen(x) & \ \ fst(snd(x)) = rec(x) & \ \ fst(snd(snd(x))) = srch(x) & \ \ snd(snd(snd(x))) = rsch(x)"; -by(simp_tac (HOL_ss addsimps - [Impl.sen_def,Impl.rec_def,Impl.srch_def,Impl.rsch_def]) 1); -val impl_ss = impl_ss addsimps [result()]; +by(simp_tac (!simpset addsimps + [Impl.sen_def,Impl.rec_def,Impl.srch_def,Impl.rsch_def]) 1); +Addsimps [result()]; goal Impl.thy "a:actions(sender_asig) \ \ | a:actions(receiver_asig) \ \ | a:actions(srch_asig) \ \ | a:actions(rsch_asig)"; by(Action.action.induct_tac "a" 1); - by(ALLGOALS(simp_tac impl_ss)); -val impl_ss = impl_ss addsimps [result()]; + by(ALLGOALS (simp_tac (!simpset + delsimps [actions_def,srch_asig_def,rsch_asig_def]))); +Addsimps [result()]; (* INVARIANT 1 *) -val ss = impl_ss addcongs [if_weak_cong] addsimps transitions; -val abs_ss= merge_ss(ss,abschannel_ss); +val ss = !simpset addcongs [let_weak_cong] delsimps + [trans_of_def, starts_of_def, srch_asig_def, rsch_asig_def, + asig_of_def, actions_def, srch_trans_def, rsch_trans_def]; goalw Impl.thy impl_ioas "invariant impl_ioa inv1"; br invariantI 1; -by(asm_full_simp_tac (impl_ss addsimps - [Impl.inv1_def, Impl.hdr_sum_def, - Sender.srcvd_def, Sender.ssent_def, - Receiver.rsent_def,Receiver.rrcvd_def]) 1); +by(asm_full_simp_tac (ss + addsimps [Impl.inv1_def, Impl.hdr_sum_def, Sender.srcvd_def, + Sender.ssent_def, Receiver.rsent_def,Receiver.rrcvd_def]) 1); -by(simp_tac (HOL_ss addsimps [fork_lemma,Impl.inv1_def]) 1); +by(simp_tac (ss delsimps [trans_of_par4] + addsimps [fork_lemma,Impl.inv1_def]) 1); (* Split proof in two *) by (rtac conjI 1); (* First half *) -by(asm_full_simp_tac (impl_ss addsimps [Impl.inv1_def]) 1); +by(asm_full_simp_tac (ss addsimps [Impl.inv1_def]) 1); br Action.action.induct 1; -val tac = asm_simp_tac (ss addcongs [conj_cong] - addsimps [Suc_pred_lemma] - setloop (split_tac [expand_if])); -val tac_abs = asm_simp_tac (abs_ss addcongs [conj_cong] - addsimps [Suc_pred_lemma] +val tac = asm_simp_tac (ss delsimps [srch_ioa_def, rsch_ioa_def] + addcongs [if_weak_cong, conj_cong] + addsimps (Suc_pred_lemma :: transitions) setloop (split_tac [expand_if])); +val tac_abs = asm_simp_tac (!simpset + delsimps [srch_asig_def, rsch_asig_def, actions_def, + srch_trans_def, rsch_trans_def] + addcongs [if_weak_cong, conj_cong] + addsimps (Suc_pred_lemma :: transitions) + setloop (split_tac [expand_if])); by (EVERY1[tac, tac, tac, tac]); by (tac 1); by (tac_abs 1); (* 5 + 1 *) - + by (tac 1); by (tac_abs 1); - + (* 4 + 1 *) by(EVERY1[tac, tac, tac, tac]); (* Now the other half *) -by(asm_full_simp_tac (impl_ss addsimps [Impl.inv1_def]) 1); +by(asm_full_simp_tac (ss addsimps [Impl.inv1_def]) 1); br Action.action.induct 1; by(EVERY1[tac, tac]); @@ -95,7 +99,7 @@ by (tac_abs 1); by (rtac impI 1); by (REPEAT (etac conjE 1)); -by (asm_simp_tac (impl_ss addsimps [Impl.hdr_sum_def, Multiset.count_def, +by (asm_simp_tac (ss addsimps [Impl.hdr_sum_def, Multiset.count_def, Multiset.countm_nonempty_def] setloop (split_tac [expand_if])) 1); (* detour 2 *) @@ -103,19 +107,18 @@ by (tac_abs 1); by (rtac impI 1); by (REPEAT (etac conjE 1)); -by (asm_full_simp_tac (impl_ss addsimps - [Impl.hdr_sum_def, - Multiset.count_def, - Multiset.countm_nonempty_def, - Multiset.delm_nonempty_def, - left_plus_cancel,left_plus_cancel_inside_succ, - unzero_less] - setloop (split_tac [expand_if])) 1); +by (asm_full_simp_tac (ss addsimps [Impl.hdr_sum_def, + Multiset.count_def, + Multiset.countm_nonempty_def, + Multiset.delm_nonempty_def, + left_plus_cancel, + left_plus_cancel_inside_succ, + unzero_less] + setloop (split_tac [expand_if])) 1); by (rtac allI 1); by (rtac conjI 1); by (rtac impI 1); by (hyp_subst_tac 1); - by (rtac (pred_suc RS mp RS sym RS iffD2) 1); by (dtac less_le_trans 1); by (cut_facts_tac [rewrite_rule[Packet.hdr_def] @@ -125,13 +128,13 @@ by (rtac (countm_done_delm RS mp RS sym) 1); by (rtac refl 1); -by (asm_simp_tac (HOL_ss addsimps [Multiset.count_def]) 1); +by (asm_simp_tac (ss addsimps [Multiset.count_def]) 1); by (rtac impI 1); -by (asm_full_simp_tac (HOL_ss addsimps [neg_flip]) 1); +by (asm_full_simp_tac (ss addsimps [neg_flip]) 1); by (hyp_subst_tac 1); by (rtac countm_spurious_delm 1); -by (simp_tac HOL_ss 1); +by (Simp_tac 1); by (EVERY1[tac, tac, tac, tac, tac, tac]); @@ -145,48 +148,55 @@ by (rtac invariantI1 1); (* Base case *) - by (asm_full_simp_tac (impl_ss addsimps - (Impl.inv2_def :: (receiver_projections - @ sender_projections @ impl_ioas))) 1); + by (asm_full_simp_tac (ss addsimps (Impl.inv2_def :: + (receiver_projections + @ sender_projections @ impl_ioas))) + 1); - by (asm_simp_tac (impl_ss addsimps impl_ioas) 1); + by (asm_simp_tac (ss addsimps impl_ioas) 1); by (Action.action.induct_tac "a" 1); (* 10 cases. First 4 are simple, since state doesn't change wrt. invariant *) (* 10 *) - by (asm_simp_tac (impl_ss addsimps (Impl.inv2_def::transitions)) 1); + by (asm_simp_tac (ss delsimps [srch_ioa_def, rsch_ioa_def] + addsimps (Impl.inv2_def::transitions)) 1); (* 9 *) - by (asm_simp_tac (impl_ss addsimps (Impl.inv2_def::transitions)) 1); + by (asm_simp_tac (ss delsimps [srch_ioa_def, rsch_ioa_def] + addsimps (Impl.inv2_def::transitions)) 1); (* 8 *) - by (asm_simp_tac (impl_ss addsimps (Impl.inv2_def::transitions)) 2); + by (asm_simp_tac (ss delsimps [srch_ioa_def, rsch_ioa_def] + addsimps (Impl.inv2_def::transitions)) 2); (* 7 *) - by (asm_simp_tac (impl_ss addsimps (Impl.inv2_def::transitions)) 3); + by (asm_simp_tac (ss delsimps [srch_ioa_def, rsch_ioa_def] + addsimps (Impl.inv2_def::transitions)) 3); (* 6 *) by(forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE) RS conjunct1] 1); - by (asm_full_simp_tac (impl_ss addsimps [leq_imp_leq_suc,Impl.inv2_def] - addsimps transitions) 1); + by (asm_full_simp_tac (ss delsimps [srch_ioa_def, rsch_ioa_def] + addsimps ([leq_imp_leq_suc,Impl.inv2_def] + @ transitions)) 1); (* 5 *) - by (asm_full_simp_tac (impl_ss addsimps [leq_imp_leq_suc,Impl.inv2_def] - addsimps transitions) 1); + by (asm_full_simp_tac (ss delsimps [srch_ioa_def, rsch_ioa_def] + addsimps ([leq_imp_leq_suc,Impl.inv2_def] + @ transitions)) 1); (* 4 *) by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE) RS conjunct1] 1); - by (asm_full_simp_tac (impl_ss addsimps [Impl.inv2_def] - addsimps transitions) 1); + by (asm_full_simp_tac (ss delsimps [srch_ioa_def, rsch_ioa_def] + addsimps (Impl.inv2_def :: transitions)) 1); by (fast_tac (HOL_cs addDs [add_leD1,leD]) 1); (* 3 *) by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1); - by (asm_full_simp_tac (impl_ss addsimps - (Impl.inv2_def::transitions)) 1); + by (asm_full_simp_tac (ss delsimps [srch_ioa_def, rsch_ioa_def] + addsimps (Impl.inv2_def :: transitions)) 1); by (fold_tac [rewrite_rule [Packet.hdr_def]Impl.hdr_sum_def]); by (fast_tac (HOL_cs addDs [add_leD1,leD]) 1); (* 2 *) - by (asm_full_simp_tac (impl_ss addsimps - (Impl.inv2_def::transitions)) 1); + by (asm_full_simp_tac (ss delsimps [srch_ioa_def, rsch_ioa_def] + addsimps (Impl.inv2_def :: transitions)) 1); by(forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE) RS conjunct1] 1); by (rtac impI 1); @@ -194,11 +204,11 @@ by (REPEAT (etac conjE 1)); by (dres_inst_tac [("k","count (rsch s) (~sbit(sen s))")] (standard(leq_add_leq RS mp)) 1); - by (asm_full_simp_tac HOL_ss 1); + by (asm_full_simp_tac ss 1); (* 1 *) - by (asm_full_simp_tac (impl_ss addsimps - (Impl.inv2_def::transitions)) 1); + by (asm_full_simp_tac (ss delsimps [srch_ioa_def, rsch_ioa_def] + addsimps (Impl.inv2_def :: transitions)) 1); by(forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE) RS conjunct2] 1); by (rtac impI 1); @@ -207,103 +217,103 @@ by (fold_tac [rewrite_rule[Packet.hdr_def]Impl.hdr_sum_def]); by (dres_inst_tac [("k","hdr_sum (srch s) (sbit(sen s))")] (standard(leq_add_leq RS mp)) 1); - by (asm_full_simp_tac HOL_ss 1); + by (asm_full_simp_tac ss 1); qed "inv2"; (* INVARIANT 3 *) + +val ss = ss delsimps [srch_ioa_def, rsch_ioa_def, Packet.hdr_def]; + goal Impl.thy "invariant impl_ioa inv3"; by (rtac invariantI 1); (* Base case *) - by (asm_full_simp_tac (impl_ss addsimps + by (asm_full_simp_tac (ss addsimps (Impl.inv3_def :: (receiver_projections @ sender_projections @ impl_ioas))) 1); - by (asm_simp_tac (impl_ss addsimps impl_ioas) 1); + by (asm_simp_tac (ss addsimps impl_ioas) 1); by (Action.action.induct_tac "a" 1); (* 10 *) - by (asm_full_simp_tac (impl_ss addsimps - (append_cons::not_hd_append::Impl.inv3_def::transitions) - setloop (split_tac [expand_if])) 1); + by (asm_full_simp_tac (ss + addsimps (append_cons::not_hd_append::Impl.inv3_def::transitions) + setloop (split_tac [expand_if])) 1); (* 9 *) - by (asm_full_simp_tac (impl_ss addsimps - (append_cons::not_hd_append::Impl.inv3_def::transitions) - setloop (split_tac [expand_if])) 1); + by (asm_full_simp_tac (ss + addsimps (append_cons::not_hd_append::Impl.inv3_def::transitions) + setloop (split_tac [expand_if])) 1); (* 8 *) - by (asm_full_simp_tac (impl_ss addsimps - (append_cons::not_hd_append::Impl.inv3_def::transitions) - setloop (split_tac [expand_if])) 1); + by (asm_full_simp_tac (ss + addsimps (append_cons::not_hd_append::Impl.inv3_def::transitions) + setloop (split_tac [expand_if])) 1); by (tac_abs 1); by (strip_tac 1 THEN REPEAT (etac conjE 1)); - by (asm_full_simp_tac (HOL_ss addsimps [cons_imp_not_null]) 1); - + by (asm_full_simp_tac (ss addsimps [cons_imp_not_null]) 1); by (hyp_subst_tac 1); by (etac exE 1); - by (asm_full_simp_tac list_ss 1); + by (Asm_full_simp_tac 1); (* 7 *) - by (asm_full_simp_tac (impl_ss addsimps + by (asm_full_simp_tac (ss addsimps (Suc_pred_lemma::append_cons::not_hd_append::Impl.inv3_def::transitions) setloop (split_tac [expand_if])) 1); by (tac_abs 1); by (fast_tac HOL_cs 1); (* 6 *) - by (asm_full_simp_tac (impl_ss addsimps + by (asm_full_simp_tac (ss addsimps (append_cons::not_hd_append::Impl.inv3_def::transitions) setloop (split_tac [expand_if])) 1); (* 5 *) - by (asm_full_simp_tac (impl_ss addsimps + by (asm_full_simp_tac (ss addsimps (append_cons::not_hd_append::Impl.inv3_def::transitions) setloop (split_tac [expand_if])) 1); - (* 4 *) - by (asm_full_simp_tac (impl_ss addsimps + by (asm_full_simp_tac (ss addsimps (append_cons::not_hd_append::Impl.inv3_def::transitions) setloop (split_tac [expand_if])) 1); (* 3 *) - by (asm_full_simp_tac (impl_ss addsimps + by (asm_full_simp_tac (ss addsimps (append_cons::not_hd_append::Impl.inv3_def::transitions) setloop (split_tac [expand_if])) 1); (* 2 *) - by (asm_full_simp_tac (impl_ss addsimps transitions) 1); - by (simp_tac (HOL_ss addsimps [Impl.inv3_def]) 1); + by (asm_full_simp_tac (ss addsimps transitions) 1); + by (simp_tac (ss addsimps [Impl.inv3_def]) 1); by (strip_tac 1 THEN REPEAT (etac conjE 1)); by (rtac (imp_or_lem RS iffD2) 1); by (rtac impI 1); by (forward_tac [rewrite_rule [Impl.inv2_def] (inv2 RS invariantE)] 1); - by (asm_full_simp_tac list_ss 1); + by (asm_full_simp_tac ss 1); by (REPEAT (etac conjE 1)); by (res_inst_tac [("j","count (ssent(sen s)) (~sbit(sen s))"), ("k","count (rsent(rec s)) (sbit(sen s))")] le_trans 1); by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE) RS conjunct2] 1); - by (asm_full_simp_tac (list_ss addsimps + by (asm_full_simp_tac (ss addsimps [Impl.hdr_sum_def, Multiset.count_def]) 1); by (rtac (less_eq_add_cong RS mp RS mp) 1); by (rtac countm_props 1); - by (simp_tac (list_ss addsimps [Packet.hdr_def]) 1); + by (simp_tac (ss addsimps [Packet.hdr_def]) 1); by (rtac countm_props 1); - by (simp_tac (list_ss addsimps [Packet.hdr_def]) 1); + by (simp_tac (ss addsimps [Packet.hdr_def]) 1); by (assume_tac 1); - (* 1 *) - by (asm_full_simp_tac (impl_ss addsimps + by (asm_full_simp_tac (ss addsimps (append_cons::not_hd_append::Impl.inv3_def::transitions) setloop (split_tac [expand_if])) 1); by (strip_tac 1 THEN REPEAT (etac conjE 1)); by (rtac (imp_or_lem RS iffD2) 1); by (rtac impI 1); by (forward_tac [rewrite_rule [Impl.inv2_def] (inv2 RS invariantE)] 1); - by (asm_full_simp_tac list_ss 1); + by (asm_full_simp_tac ss 1); by (REPEAT (etac conjE 1)); by (dtac mp 1); by (assume_tac 1); @@ -315,73 +325,62 @@ qed "inv3"; - (* INVARIANT 4 *) goal Impl.thy "invariant impl_ioa inv4"; by (rtac invariantI 1); (* Base case *) - by (asm_full_simp_tac (impl_ss addsimps + by (asm_full_simp_tac (ss addsimps (Impl.inv4_def :: (receiver_projections @ sender_projections @ impl_ioas))) 1); - by (asm_simp_tac (impl_ss addsimps impl_ioas) 1); + by (asm_simp_tac (ss addsimps impl_ioas) 1); by (Action.action.induct_tac "a" 1); (* 10 *) - by (asm_full_simp_tac (impl_ss addsimps - (append_cons::Impl.inv4_def::transitions) + by (asm_full_simp_tac (ss addsimps (append_cons::Impl.inv4_def::transitions) setloop (split_tac [expand_if])) 1); (* 9 *) - by (asm_full_simp_tac (impl_ss addsimps - (append_cons::Impl.inv4_def::transitions) + by (asm_full_simp_tac (ss addsimps (append_cons::Impl.inv4_def::transitions) setloop (split_tac [expand_if])) 1); (* 8 *) - by (asm_full_simp_tac (impl_ss addsimps - (append_cons::Impl.inv4_def::transitions) + by (asm_full_simp_tac (ss addsimps (append_cons::Impl.inv4_def::transitions) setloop (split_tac [expand_if])) 1); (* 7 *) - by (asm_full_simp_tac (impl_ss addsimps - (append_cons::Impl.inv4_def::transitions) + by (asm_full_simp_tac (ss addsimps (append_cons::Impl.inv4_def::transitions) setloop (split_tac [expand_if])) 1); (* 6 *) - by (asm_full_simp_tac (impl_ss addsimps - (append_cons::Impl.inv4_def::transitions) + by (asm_full_simp_tac (ss addsimps (append_cons::Impl.inv4_def::transitions) setloop (split_tac [expand_if])) 1); (* 5 *) - by (asm_full_simp_tac (impl_ss addsimps - (append_cons::Impl.inv4_def::transitions) + by (asm_full_simp_tac (ss addsimps (append_cons::Impl.inv4_def::transitions) setloop (split_tac [expand_if])) 1); (* 4 *) - by (asm_full_simp_tac (impl_ss addsimps - (append_cons::Impl.inv4_def::transitions) + by (asm_full_simp_tac (ss addsimps (append_cons::Impl.inv4_def::transitions) setloop (split_tac [expand_if])) 1); (* 3 *) - by (asm_full_simp_tac (impl_ss addsimps - (append_cons::Impl.inv4_def::transitions) + by (asm_full_simp_tac (ss addsimps (append_cons::Impl.inv4_def::transitions) setloop (split_tac [expand_if])) 1); (* 2 *) - by (asm_full_simp_tac (impl_ss addsimps - (append_cons::Impl.inv4_def::transitions) + by (asm_full_simp_tac (ss addsimps (append_cons::Impl.inv4_def::transitions) setloop (split_tac [expand_if])) 1); by (strip_tac 1 THEN REPEAT (etac conjE 1)); by(forward_tac [rewrite_rule [Impl.inv2_def] (inv2 RS invariantE)] 1); - by (asm_full_simp_tac list_ss 1); + by (Asm_full_simp_tac 1); (* 1 *) - by (asm_full_simp_tac (impl_ss addsimps - (append_cons::Impl.inv4_def::transitions) + by (asm_full_simp_tac (ss addsimps (append_cons::Impl.inv4_def::transitions) setloop (split_tac [expand_if])) 1); by (strip_tac 1 THEN REPEAT (etac conjE 1)); by (rtac ccontr 1); @@ -389,20 +388,18 @@ (inv2 RS invariantE)] 1); by(forward_tac [rewrite_rule [Impl.inv3_def] (inv3 RS invariantE)] 1); - by (asm_full_simp_tac list_ss 1); + by (Asm_full_simp_tac 1); by (eres_inst_tac [("x","m")] allE 1); by (dtac less_le_trans 1); by (dtac (left_add_leq RS mp) 1); - by (asm_full_simp_tac list_ss 1); - by (asm_full_simp_tac arith_ss 1); + by (Asm_full_simp_tac 1); + by (Asm_full_simp_tac 1); qed "inv4"; - (* rebind them *) val inv1 = rewrite_rule [Impl.inv1_def] (inv1 RS invariantE); val inv2 = rewrite_rule [Impl.inv2_def] (inv2 RS invariantE); val inv3 = rewrite_rule [Impl.inv3_def] (inv3 RS invariantE); val inv4 = rewrite_rule [Impl.inv4_def] (inv4 RS invariantE); - diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/IOA/NTP/Lemmas.ML --- a/src/HOL/IOA/NTP/Lemmas.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/IOA/NTP/Lemmas.ML Wed Oct 04 13:12:14 1995 +0100 @@ -56,7 +56,7 @@ (* Arithmetic *) goal Arith.thy "n ~= 0 --> Suc(m+pred(n)) = m+n"; by (nat_ind_tac "n" 1); - by (REPEAT(simp_tac arith_ss 1)); + by (REPEAT(Simp_tac 1)); val Suc_pred_lemma = store_thm("Suc_pred_lemma", result() RS mp); goal Arith.thy "x <= y --> x <= Suc(y)"; @@ -66,49 +66,49 @@ by (dtac (le_eq_less_or_eq RS iffD1) 1); by (etac disjE 1); by (etac less_SucI 1); - by (asm_simp_tac nat_ss 1); + by (Asm_simp_tac 1); val leq_imp_leq_suc = store_thm("leq_imp_leq_suc", result() RS mp); (* Same as previous! *) goal Arith.thy "(x::nat)<=y --> x<=Suc(y)"; - by (simp_tac (arith_ss addsimps [le_eq_less_or_eq]) 1); + by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); qed "leq_suc"; goal Arith.thy "((m::nat) + n = m + p) = (n = p)"; by (nat_ind_tac "m" 1); - by (simp_tac arith_ss 1); - by (asm_simp_tac arith_ss 1); + by (Simp_tac 1); + by (Asm_simp_tac 1); qed "left_plus_cancel"; goal Arith.thy "((x::nat) + y = Suc(x + z)) = (y = Suc(z))"; by (nat_ind_tac "x" 1); - by (simp_tac arith_ss 1); - by (asm_simp_tac arith_ss 1); + by (Simp_tac 1); + by (Asm_simp_tac 1); qed "left_plus_cancel_inside_succ"; goal Arith.thy "(x ~= 0) = (? y. x = Suc(y))"; by (nat_ind_tac "x" 1); - by (simp_tac arith_ss 1); - by (asm_simp_tac arith_ss 1); + by (Simp_tac 1); + by (Asm_simp_tac 1); by (fast_tac HOL_cs 1); qed "nonzero_is_succ"; goal Arith.thy "(m::nat) < n --> m + p < n + p"; by (nat_ind_tac "p" 1); - by (simp_tac arith_ss 1); - by (asm_simp_tac arith_ss 1); + by (Simp_tac 1); + by (Asm_simp_tac 1); qed "less_add_same_less"; goal Arith.thy "(x::nat)<= y --> x<=y+k"; by (nat_ind_tac "k" 1); - by (simp_tac arith_ss 1); - by (asm_full_simp_tac (arith_ss addsimps [leq_suc]) 1); + by (Simp_tac 1); + by (asm_full_simp_tac (!simpset addsimps [leq_suc]) 1); qed "leq_add_leq"; goal Arith.thy "(x::nat) + y <= z --> x <= z"; by (nat_ind_tac "y" 1); - by (simp_tac arith_ss 1); - by (asm_simp_tac arith_ss 1); + by (Simp_tac 1); + by (Asm_simp_tac 1); by (rtac impI 1); by (dtac Suc_leD 1); by (fast_tac HOL_cs 1); @@ -129,7 +129,7 @@ goal Arith.thy "(A::nat) <= B --> C <= D --> A + C <= B + D"; by (rtac impI 1); by (rtac impI 1); - by (asm_full_simp_tac (arith_ss addsimps [le_eq_less_or_eq]) 1); + by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); by (safe_tac HOL_cs); by (rtac (less_add_cong RS mp RS mp) 1); by (assume_tac 1); @@ -147,7 +147,7 @@ by (dtac (less_eq_add_cong RS mp) 1); by (cut_facts_tac [le_refl] 1); by (dres_inst_tac [("P","x<=x")] mp 1);by (assume_tac 1); - by (asm_full_simp_tac (HOL_ss addsimps [add_commute]) 1); + by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1); by (rtac impI 1); by (etac le_trans 1); by (assume_tac 1); @@ -155,67 +155,68 @@ goal Arith.thy "(? x. y = Suc(x)) = (~(y = 0))"; by (nat_ind_tac "y" 1); - by (simp_tac arith_ss 1); + by (Simp_tac 1); by (rtac iffI 1); - by (asm_full_simp_tac arith_ss 1); + by (Asm_full_simp_tac 1); by (fast_tac HOL_cs 1); qed "suc_not_zero"; goal Arith.thy "Suc(x) <= y --> (? z. y = Suc(z))"; by (rtac impI 1); - by (asm_full_simp_tac (arith_ss addsimps [le_eq_less_or_eq]) 1); + by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); by (safe_tac HOL_cs); by (fast_tac HOL_cs 2); - by (asm_simp_tac (arith_ss addsimps [suc_not_zero]) 1); + by (asm_simp_tac (!simpset addsimps [suc_not_zero]) 1); by (rtac ccontr 1); - by (asm_full_simp_tac (arith_ss addsimps [suc_not_zero]) 1); + by (asm_full_simp_tac (!simpset addsimps [suc_not_zero]) 1); by (hyp_subst_tac 1); - by (asm_full_simp_tac arith_ss 1); + by (Asm_full_simp_tac 1); qed "suc_leq_suc"; goal Arith.thy "~0 n = 0"; by (nat_ind_tac "n" 1); - by (asm_simp_tac arith_ss 1); + by (Asm_simp_tac 1); by (safe_tac HOL_cs); - by (asm_full_simp_tac arith_ss 1); - by (asm_full_simp_tac arith_ss 1); + by (Asm_full_simp_tac 1); + by (Asm_full_simp_tac 1); qed "zero_eq"; goal Arith.thy "x < Suc(y) --> x<=y"; by (nat_ind_tac "n" 1); - by (asm_simp_tac arith_ss 1); + by (Asm_simp_tac 1); by (safe_tac HOL_cs); by (etac less_imp_le 1); qed "less_suc_imp_leq"; goal Arith.thy "0 Suc(pred(x)) = x"; by (nat_ind_tac "x" 1); - by (simp_tac arith_ss 1); - by (asm_simp_tac arith_ss 1); + by (Simp_tac 1); + by (Asm_simp_tac 1); qed "suc_pred_id"; goal Arith.thy "0 (pred(x) = y) = (x = Suc(y))"; by (nat_ind_tac "x" 1); - by (simp_tac arith_ss 1); - by (asm_simp_tac arith_ss 1); + by (Simp_tac 1); + by (Asm_simp_tac 1); qed "pred_suc"; goal Arith.thy "(x ~= 0) = (0 (y <= x)"; by (nat_ind_tac "y" 1); - by (simp_tac arith_ss 1); - by (simp_tac (arith_ss addsimps - [Suc_le_mono, le_refl RS (leq_add_leq RS mp)]) 1); + by (Simp_tac 1); + by (simp_tac (!simpset addsimps [le_refl RS (leq_add_leq RS mp)]) 1); qed "plus_leq_lem"; (* Lists *) +val list_ss = simpset_of "List"; + goal List.thy "(xs @ (y#ys)) ~= []"; by (list.induct_tac "xs" 1); by (simp_tac list_ss 1); diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/IOA/NTP/Multiset.ML --- a/src/HOL/IOA/NTP/Multiset.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/IOA/NTP/Multiset.ML Wed Oct 04 13:12:14 1995 +0100 @@ -14,13 +14,13 @@ goal Multiset.thy "count (addm M x) y = (if y=x then Suc(count M y) else count M y)"; - by (asm_simp_tac (arith_ss addsimps + by (asm_simp_tac (!simpset addsimps [Multiset.count_def,Multiset.countm_nonempty_def] setloop (split_tac [expand_if])) 1); qed "count_addm_simp"; goal Multiset.thy "count M y <= count (addm M x) y"; - by (simp_tac (arith_ss addsimps [count_addm_simp] + by (simp_tac (!simpset addsimps [count_addm_simp] setloop (split_tac [expand_if])) 1); by (rtac impI 1); by (rtac (le_refl RS (leq_suc RS mp)) 1); @@ -29,31 +29,31 @@ goalw Multiset.thy [Multiset.count_def] "count (delm M x) y = (if y=x then pred(count M y) else count M y)"; by (res_inst_tac [("M","M")] Multiset.induction 1); - by (asm_simp_tac (arith_ss + by (asm_simp_tac (!simpset addsimps [Multiset.delm_empty_def,Multiset.countm_empty_def] setloop (split_tac [expand_if])) 1); - by (asm_full_simp_tac (arith_ss + by (asm_full_simp_tac (!simpset addsimps [Multiset.delm_nonempty_def, Multiset.countm_nonempty_def] setloop (split_tac [expand_if])) 1); by (safe_tac HOL_cs); - by (asm_full_simp_tac HOL_ss 1); + by (Asm_full_simp_tac 1); qed "count_delm_simp"; goal Multiset.thy "!!M. (!x. P(x) --> Q(x)) ==> (countm M P <= countm M Q)"; by (res_inst_tac [("M","M")] Multiset.induction 1); - by (simp_tac (arith_ss addsimps [Multiset.countm_empty_def]) 1); - by (simp_tac (arith_ss addsimps[Multiset.countm_nonempty_def]) 1); + by (simp_tac (!simpset addsimps [Multiset.countm_empty_def]) 1); + by (simp_tac (!simpset addsimps[Multiset.countm_nonempty_def]) 1); by (etac (less_eq_add_cong RS mp RS mp) 1); - by (asm_full_simp_tac (arith_ss addsimps [le_eq_less_or_eq] + by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq] setloop (split_tac [expand_if])) 1); qed "countm_props"; goal Multiset.thy "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P"; by (res_inst_tac [("M","M")] Multiset.induction 1); - by (simp_tac (arith_ss addsimps [Multiset.delm_empty_def, + by (simp_tac (!simpset addsimps [Multiset.delm_empty_def, Multiset.countm_empty_def]) 1); - by (asm_simp_tac (arith_ss addsimps[Multiset.countm_nonempty_def, + by (asm_simp_tac (!simpset addsimps[Multiset.countm_nonempty_def, Multiset.delm_nonempty_def] setloop (split_tac [expand_if])) 1); qed "countm_spurious_delm"; @@ -61,10 +61,10 @@ goal Multiset.thy "!!P. P(x) ==> 0 0 0 countm (delm M x) P = pred (countm M P)"; by (res_inst_tac [("M","M")] Multiset.induction 1); - by (simp_tac (arith_ss addsimps + by (simp_tac (!simpset addsimps [Multiset.delm_empty_def, Multiset.countm_empty_def]) 1); - by (asm_simp_tac (arith_ss addsimps + by (asm_simp_tac (!simpset addsimps [eq_sym_conv,count_addm_simp,Multiset.delm_nonempty_def, Multiset.countm_nonempty_def,pos_count_imp_pos_countm, suc_pred_id] diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/IOA/NTP/Packet.ML --- a/src/HOL/IOA/NTP/Packet.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/IOA/NTP/Packet.ML Wed Oct 04 13:12:14 1995 +0100 @@ -9,5 +9,5 @@ (* Instantiation of a tautology? *) goal Packet.thy "!x. x = packet --> hdr(x) = hdr(packet)"; - by (simp_tac (HOL_ss addsimps [Packet.hdr_def]) 1); + by (simp_tac (!simpset addsimps [Packet.hdr_def]) 1); qed "eq_packet_imp_eq_hdr"; \ No newline at end of file diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/IOA/NTP/Receiver.ML --- a/src/HOL/IOA/NTP/Receiver.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/IOA/NTP/Receiver.ML Wed Oct 04 13:12:14 1995 +0100 @@ -15,9 +15,8 @@ \ C_m_r : actions(receiver_asig) & \ \ C_r_s ~: actions(receiver_asig) & \ \ C_r_r(m) : actions(receiver_asig)"; - by(simp_tac (action_ss addsimps - (Receiver.receiver_asig_def :: actions_def :: - asig_projections @ set_lemmas)) 1); + by(simp_tac (!simpset addsimps (Receiver.receiver_asig_def :: actions_def :: + asig_projections @ set_lemmas)) 1); qed "in_receiver_asig"; val receiver_projections = diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/IOA/NTP/Sender.ML --- a/src/HOL/IOA/NTP/Sender.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/IOA/NTP/Sender.ML Wed Oct 04 13:12:14 1995 +0100 @@ -15,7 +15,7 @@ \ C_m_r ~: actions(sender_asig) & \ \ C_r_s : actions(sender_asig) & \ \ C_r_r(m) ~: actions(sender_asig)"; -by(simp_tac (action_ss addsimps +by(simp_tac (!simpset addsimps (Sender.sender_asig_def :: actions_def :: asig_projections @ set_lemmas)) 1); qed "in_sender_asig"; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/IOA/meta_theory/Asig.ML --- a/src/HOL/IOA/meta_theory/Asig.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/IOA/meta_theory/Asig.ML Wed Oct 04 13:12:14 1995 +0100 @@ -11,9 +11,9 @@ val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def]; goal Asig.thy "!!a.[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)"; -by (asm_full_simp_tac (list_ss addsimps [externals_def,actions_def]) 1); +by (asm_full_simp_tac (!simpset addsimps [externals_def,actions_def]) 1); qed"int_and_ext_is_act"; goal Asig.thy "!!a.[|a:externals(S)|] ==> a:actions(S)"; -by (asm_full_simp_tac (list_ss addsimps [externals_def,actions_def]) 1); +by (asm_full_simp_tac (!simpset addsimps [externals_def,actions_def]) 1); qed"ext_is_act"; \ No newline at end of file diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/IOA/meta_theory/IOA.ML --- a/src/HOL/IOA/meta_theory/IOA.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/IOA/meta_theory/IOA.ML Wed Oct 04 13:12:14 1995 +0100 @@ -14,23 +14,23 @@ goal IOA.thy "asig_of((x,y,z)) = x & starts_of((x,y,z)) = y & trans_of((x,y,z)) = z"; - by (simp_tac (SS addsimps ioa_projections) 1); + by (simp_tac (!simpset addsimps ioa_projections) 1); qed "ioa_triple_proj"; goalw IOA.thy [ioa_def,state_trans_def,actions_def, is_asig_def] "!!A. [| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:actions(asig_of(A))"; by (REPEAT(etac conjE 1)); by (EVERY1[etac allE, etac impE, atac]); - by (asm_full_simp_tac SS 1); + by (Asm_full_simp_tac 1); qed "trans_in_actions"; goal IOA.thy "filter_oseq p (filter_oseq p s) = filter_oseq p s"; - by (simp_tac (SS addsimps [filter_oseq_def]) 1); + by (simp_tac (!simpset addsimps [filter_oseq_def]) 1); by (rtac ext 1); by (Option.option.induct_tac "s(i)" 1); - by (simp_tac SS 1); - by (simp_tac (SS setloop (split_tac [expand_if])) 1); + by (Simp_tac 1); + by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); qed "filter_oseq_idemp"; goalw IOA.thy [mk_trace_def,filter_oseq_def] @@ -40,35 +40,35 @@ \ (mk_trace A s n = Some(a)) = \ \ (s(n)=Some(a) & a : externals(asig_of(A)))"; by (Option.option.induct_tac "s(n)" 1); - by (ALLGOALS (simp_tac (SS setloop (split_tac [expand_if])))); + by (ALLGOALS (simp_tac (!simpset setloop (split_tac [expand_if])))); by (fast_tac HOL_cs 1); qed "mk_trace_thm"; goalw IOA.thy [reachable_def] "!!A. s:starts_of(A) ==> reachable A s"; by (res_inst_tac [("x","(%i.None,%i.s)")] bexI 1); - by (simp_tac SS 1); - by (asm_simp_tac (SS addsimps exec_rws) 1); + by (Simp_tac 1); + by (asm_simp_tac (!simpset addsimps exec_rws) 1); qed "reachable_0"; goalw IOA.thy (reachable_def::exec_rws) "!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t"; - by(asm_full_simp_tac SS 1); + by(Asm_full_simp_tac 1); by(safe_tac set_cs); by(res_inst_tac [("x","(%i.if i a~:internals(asig_of(A2))"; -by (asm_full_simp_tac SS 1); +by (Asm_full_simp_tac 1); by (best_tac (set_cs addEs [equalityCE]) 1); qed"ext1_is_not_int2"; goalw IOA.thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def] "!! a. [| compat_ioas A2 A1 ; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))"; -by (asm_full_simp_tac SS 1); +by (Asm_full_simp_tac 1); by (best_tac (set_cs addEs [equalityCE]) 1); qed"ext2_is_not_int1"; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/IOA/meta_theory/Option.ML --- a/src/HOL/IOA/meta_theory/Option.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/IOA/meta_theory/Option.ML Wed Oct 04 13:12:14 1995 +0100 @@ -6,8 +6,7 @@ Derived rules *) -val option_rws = Let_def :: Option.option.simps; -val SS = arith_ss addsimps option_rws; +Addsimps [Let_def]; val [prem] = goal Option.thy "P(opt) ==> P(None) | (? x. P(Some(x)))"; br (prem RS rev_mp) 1; @@ -17,8 +16,8 @@ goal Option.thy "x=None | (? y.x=Some(y))"; by (Option.option.induct_tac "x" 1); -by (asm_full_simp_tac list_ss 1); +by (Asm_full_simp_tac 1); by (rtac disjI2 1); by (rtac exI 1); -by (asm_full_simp_tac list_ss 1); -qed"opt_cases"; \ No newline at end of file +by (Asm_full_simp_tac 1); +qed"opt_cases"; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/IOA/meta_theory/Solve.ML --- a/src/HOL/IOA/meta_theory/Solve.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/IOA/meta_theory/Solve.ML Wed Oct 04 13:12:14 1995 +0100 @@ -8,30 +8,30 @@ open Solve; -val SS = SS addsimps [mk_trace_thm,trans_in_actions]; +Addsimps [mk_trace_thm,trans_in_actions]; goalw Solve.thy [is_weak_pmap_def,traces_def] "!!f. [| IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A)); \ \ is_weak_pmap f C A |] ==> traces(C) <= traces(A)"; - by (simp_tac(SS addsimps [has_trace_def])1); + by (simp_tac(!simpset addsimps [has_trace_def])1); by (safe_tac set_cs); (* choose same trace, therefore same NF *) by (res_inst_tac[("x","mk_trace C (fst ex)")] exI 1); - by (asm_full_simp_tac set_ss 1); + by (Asm_full_simp_tac 1); (* give execution of abstract automata *) by (res_inst_tac[("x","(mk_trace A (fst ex),%i.f(snd ex i))")] bexI 1); (* Traces coincide *) - by (asm_simp_tac (SS addsimps [mk_trace_def,filter_oseq_idemp])1); + by (asm_simp_tac (!simpset addsimps [mk_trace_def,filter_oseq_idemp])1); (* Use lemma *) by (forward_tac [states_of_exec_reachable] 1); (* Now show that it's an execution *) - by (asm_full_simp_tac(SS addsimps [executions_def]) 1); + by (asm_full_simp_tac(!simpset addsimps [executions_def]) 1); by (safe_tac set_cs); (* Start states map to start states *) @@ -39,13 +39,13 @@ by (atac 1); (* Show that it's an execution fragment *) - by (asm_full_simp_tac (SS addsimps [is_execution_fragment_def])1); + by (asm_full_simp_tac (!simpset addsimps [is_execution_fragment_def])1); by (safe_tac HOL_cs); by (eres_inst_tac [("x","snd ex n")] allE 1); by (eres_inst_tac [("x","snd ex (Suc n)")] allE 1); by (eres_inst_tac [("x","a")] allE 1); - by (asm_full_simp_tac SS 1); + by (Asm_full_simp_tac 1); qed "trace_inclusion"; (* Lemmata *) @@ -60,70 +60,70 @@ \ (a:externals(asig_of(A1)) & a:externals(asig_of(A2)) | \ \ a:externals(asig_of(A1)) & a~:externals(asig_of(A2)) | \ \ a~:externals(asig_of(A1)) & a:externals(asig_of(A2)))"; -by (asm_full_simp_tac (SS addsimps [externals_def,asig_of_par,asig_comp_def,asig_inputs_def,asig_outputs_def]) 1); +by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_of_par,asig_comp_def,asig_inputs_def,asig_outputs_def]) 1); by (fast_tac set_cs 1); val externals_of_par_extra = result(); goal Solve.thy "!!s.[| reachable (C1||C2) s |] ==> reachable C1 (fst s)"; -by (asm_full_simp_tac (SS addsimps [reachable_def]) 1); +by (asm_full_simp_tac (!simpset addsimps [reachable_def]) 1); by (etac bexE 1); by (res_inst_tac [("x", "(filter_oseq (%a.a:actions(asig_of(C1))) \ \ (fst ex), \ \ %i.fst (snd ex i))")] bexI 1); (* fst(s) is in projected execution *) - by (simp_tac SS 1); + by (Simp_tac 1); by (fast_tac HOL_cs 1); (* projected execution is indeed an execution *) -by (asm_full_simp_tac (SS addsimps [executions_def,is_execution_fragment_def, +by (asm_full_simp_tac (!simpset addsimps [executions_def,is_execution_fragment_def, par_def, starts_of_def,trans_of_def]) 1); -by (simp_tac (SS addsimps [filter_oseq_def]) 1); +by (simp_tac (!simpset addsimps [filter_oseq_def]) 1); by (REPEAT(rtac allI 1)); by (cut_inst_tac [("x","fst ex n")] opt_cases 1); by (etac disjE 1); (* case 1: action sequence of || had already a None *) -by (asm_full_simp_tac SS 1); +by (Asm_full_simp_tac 1); by (REPEAT(etac exE 1)); by (case_tac "y:actions(asig_of(C1))" 1); (* case 2: action sequence of || had Some(a) and filtered sequence also *) -by (asm_full_simp_tac SS 1); +by (Asm_full_simp_tac 1); by (rtac impI 1); by (REPEAT(hyp_subst_tac 1)); - by (asm_full_simp_tac SS 1); + by (Asm_full_simp_tac 1); (* case 3: action sequence pf || had Some(a) but filtered sequence has None *) - by (asm_full_simp_tac SS 1); + by (Asm_full_simp_tac 1); qed"comp1_reachable"; (* Exact copy of proof of comp1_reachable for the second component of a parallel composition. *) goal Solve.thy "!!s.[| reachable (C1||C2) s|] ==> reachable C2 (snd s)"; -by (asm_full_simp_tac (SS addsimps [reachable_def]) 1); +by (asm_full_simp_tac (!simpset addsimps [reachable_def]) 1); by (etac bexE 1); by (res_inst_tac [("x", "(filter_oseq (%a.a:actions(asig_of(C2)))\ \ (fst ex), \ \ %i.snd (snd ex i))")] bexI 1); (* fst(s) is in projected execution *) - by (simp_tac list_ss 1); + by (Simp_tac 1); by (fast_tac HOL_cs 1); (* projected execution is indeed an execution *) - by (asm_full_simp_tac (SS addsimps [executions_def,is_execution_fragment_def, + by (asm_full_simp_tac (!simpset addsimps [executions_def,is_execution_fragment_def, par_def, starts_of_def,trans_of_def]) 1); - by (simp_tac (SS addsimps [filter_oseq_def]) 1); + by (simp_tac (!simpset addsimps [filter_oseq_def]) 1); by (REPEAT(rtac allI 1)); by (cut_inst_tac [("x","fst ex n")] opt_cases 1); by (etac disjE 1); - by (asm_full_simp_tac SS 1); + by (Asm_full_simp_tac 1); by (REPEAT(etac exE 1)); by (case_tac "y:actions(asig_of(C2))" 1); - by (asm_full_simp_tac SS 1); + by (Asm_full_simp_tac 1); by (rtac impI 1); by (REPEAT(hyp_subst_tac 1)); - by (asm_full_simp_tac SS 1); - by (asm_full_simp_tac SS 1); + by (Asm_full_simp_tac 1); + by (Asm_full_simp_tac 1); qed"comp2_reachable"; @@ -137,71 +137,71 @@ \ ==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1||C2) (A1||A2)"; by (rtac conjI 1); (* start_states *) - by (asm_full_simp_tac (SS addsimps [par_def, starts_of_def]) 1); + by (asm_full_simp_tac (!simpset addsimps [par_def, starts_of_def]) 1); by (fast_tac set_cs 1); (* transitions *) by (REPEAT (rtac allI 1)); by (rtac imp_conj_lemma 1); by (REPEAT(etac conjE 1)); -by (simp_tac (SS addsimps [externals_of_par_extra]) 1); -by (simp_tac (SS addsimps [par_def]) 1); -by (asm_full_simp_tac (SS addsimps [trans_of_def]) 1); +by (simp_tac (!simpset addsimps [externals_of_par_extra]) 1); +by (simp_tac (!simpset addsimps [par_def]) 1); +by (asm_full_simp_tac (!simpset addsimps [trans_of_def]) 1); by (rtac (expand_if RS ssubst) 1); by (rtac conjI 1); by (rtac impI 1); by (etac disjE 1); (* case 1 a:e(A1) | a:e(A2) *) -by (asm_full_simp_tac (SS addsimps [comp1_reachable,comp2_reachable, +by (asm_full_simp_tac (!simpset addsimps [comp1_reachable,comp2_reachable, ext_is_act]) 1); by (etac disjE 1); (* case 2 a:e(A1) | a~:e(A2) *) -by (asm_full_simp_tac (SS addsimps [comp1_reachable,comp2_reachable, +by (asm_full_simp_tac (!simpset addsimps [comp1_reachable,comp2_reachable, ext_is_act,ext1_ext2_is_not_act2]) 1); (* case 3 a:~e(A1) | a:e(A2) *) -by (asm_full_simp_tac (SS addsimps [comp1_reachable,comp2_reachable, +by (asm_full_simp_tac (!simpset addsimps [comp1_reachable,comp2_reachable, ext_is_act,ext1_ext2_is_not_act1]) 1); (* case 4 a:~e(A1) | a~:e(A2) *) by (rtac impI 1); by (subgoal_tac "a~:externals(asig_of(A1)) & a~:externals(asig_of(A2))" 1); (* delete auxiliary subgoal *) -by (asm_full_simp_tac SS 2); +by (Asm_full_simp_tac 2); by (fast_tac HOL_cs 2); -by (simp_tac (SS addsimps [conj_disj_distribR] addcongs [conj_cong] +by (simp_tac (!simpset addsimps [conj_disj_distribR] addcongs [conj_cong] setloop (split_tac [expand_if])) 1); by(REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN - asm_full_simp_tac(SS addsimps[comp1_reachable, + asm_full_simp_tac(!simpset addsimps[comp1_reachable, comp2_reachable])1)); qed"fxg_is_weak_pmap_of_product_IOA"; goal Solve.thy "!!s.[| reachable (rename C g) s |] ==> reachable C s"; -by (asm_full_simp_tac (SS addsimps [reachable_def]) 1); +by (asm_full_simp_tac (!simpset addsimps [reachable_def]) 1); by (etac bexE 1); by (res_inst_tac [("x", "((%i. case (fst ex i) \ \ of None => None\ \ | Some(x) => g x) ,snd ex)")] bexI 1); -by (simp_tac SS 1); +by (Simp_tac 1); (* execution is indeed an execution of C *) -by (asm_full_simp_tac (SS addsimps [executions_def,is_execution_fragment_def, +by (asm_full_simp_tac (!simpset addsimps [executions_def,is_execution_fragment_def, par_def, starts_of_def,trans_of_def,rename_def]) 1); by (REPEAT(rtac allI 1)); by (cut_inst_tac [("x","fst ex n")] opt_cases 1); by (etac disjE 1); (* case 1: action sequence of rename C had already a None *) -by (asm_full_simp_tac SS 1); +by (Asm_full_simp_tac 1); (* case 2 *) by (REPEAT(etac exE 1)); by (etac conjE 1); by (eres_inst_tac [("x","n")] allE 1); by (eres_inst_tac [("x","y")] allE 1); -by (asm_full_simp_tac SS 1); +by (Asm_full_simp_tac 1); by (etac exE 1); by (etac conjE 1); by (dtac sym 1); by (dtac sym 1); by (dtac sym 1); -by (asm_full_simp_tac SS 1); +by (Asm_full_simp_tac 1); by (safe_tac HOL_cs); qed"reachable_rename_ioa"; @@ -220,14 +220,14 @@ goal Solve.thy "!!f.[| is_weak_pmap f C A |]\ \ ==> (is_weak_pmap f (rename C g) (rename A g))"; -by (asm_full_simp_tac (SS addsimps [is_weak_pmap_def]) 1); +by (asm_full_simp_tac (!simpset addsimps [is_weak_pmap_def]) 1); by (rtac conjI 1); -by (asm_full_simp_tac (SS addsimps [rename_def,starts_of_def]) 1); +by (asm_full_simp_tac (!simpset addsimps [rename_def,starts_of_def]) 1); by (fast_tac set_cs 1); by (REPEAT (rtac allI 1)); by (rtac imp_conj_lemma 1); -by (simp_tac (SS addsimps [rename_def]) 1); -by (asm_full_simp_tac (SS addsimps [externals_def,asig_inputs_def,asig_outputs_def,asig_of_def,trans_of_def]) 1); +by (simp_tac (!simpset addsimps [rename_def]) 1); +by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_inputs_def,asig_outputs_def,asig_of_def,trans_of_def]) 1); by (safe_tac set_cs); by (rtac (expand_if RS ssubst) 1); by (rtac conjI 1); @@ -238,23 +238,23 @@ (* x is input *) by (dtac sym 1); by (dtac sym 1); -by (asm_full_simp_tac SS 1); +by (Asm_full_simp_tac 1); by (REPEAT (hyp_subst_tac 1)); by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1); by (assume_tac 1); -by (asm_full_simp_tac SS 1); +by (Asm_full_simp_tac 1); (* x is output *) by (etac exE 1); by (etac conjE 1); by (dtac sym 1); by (dtac sym 1); -by (asm_full_simp_tac SS 1); +by (Asm_full_simp_tac 1); by (REPEAT (hyp_subst_tac 1)); by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1); by (assume_tac 1); -by (asm_full_simp_tac SS 1); +by (Asm_full_simp_tac 1); (* x is internal *) -by (simp_tac (SS addsimps [disj_demorgan,neg_ex,conj_demorgan] addcongs [conj_cong]) 1); +by (simp_tac (!simpset addsimps [disj_demorgan,neg_ex,conj_demorgan] addcongs [conj_cong]) 1); by (rtac impI 1); by (etac conjE 1); by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1); @@ -263,7 +263,7 @@ by (eres_inst_tac [("x","t")] allE 1); by (eres_inst_tac [("x","x")] allE 1); by (eres_inst_tac [("x","x")] allE 1); -by (asm_full_simp_tac SS 1); +by (Asm_full_simp_tac 1); qed"rename_through_pmap"; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/Integ/Equiv.ML --- a/src/HOL/Integ/Equiv.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/Integ/Equiv.ML Wed Oct 04 13:12:14 1995 +0100 @@ -214,8 +214,8 @@ by (safe_tac rel_cs); by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1); by (assume_tac 1); -by (asm_simp_tac (prod_ss addsimps [equivA RS UN_equiv_class, - congruent2_implies_congruent]) 1); +by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class, + congruent2_implies_congruent]) 1); by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]); by (fast_tac rel_cs 1); qed "congruent2_implies_congruent_UN"; @@ -224,9 +224,9 @@ "[| equiv A r; congruent2 r b; a1: A; a2: A |] \ \ ==> (UN x1:r^^{a1}. UN x2:r^^{a2}. b x1 x2) = b a1 a2"; by (cut_facts_tac prems 1); -by (asm_simp_tac (prod_ss addsimps [equivA RS UN_equiv_class, - congruent2_implies_congruent, - congruent2_implies_congruent_UN]) 1); +by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class, + congruent2_implies_congruent, + congruent2_implies_congruent_UN]) 1); qed "UN_equiv_class2"; (*type checking*) diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/Integ/Integ.ML --- a/src/HOL/Integ/Integ.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/Integ/Integ.ML Wed Oct 04 13:12:14 1995 +0100 @@ -83,9 +83,8 @@ by (etac Abs_Integ_inverse 1); qed "inj_onto_Abs_Integ"; -val intrel_ss = - arith_ss addsimps [equiv_intrel_iff, inj_onto_Abs_Integ RS inj_onto_iff, - intrel_iff, intrel_in_integ, Abs_Integ_inverse]; +Addsimps [equiv_intrel_iff, inj_onto_Abs_Integ RS inj_onto_iff, + intrel_iff, intrel_in_integ, Abs_Integ_inverse]; goal Integ.thy "inj(Rep_Integ)"; by (rtac inj_inverseI 1); @@ -106,7 +105,7 @@ by (rtac equiv_intrel 1); by (fast_tac set_cs 1); by (safe_tac intrel_cs); -by (asm_full_simp_tac arith_ss 1); +by (Asm_full_simp_tac 1); qed "inj_znat"; @@ -115,7 +114,7 @@ goalw Integ.thy [congruent_def] "congruent intrel (%p. split (%x y. intrel^^{(y,x)}) p)"; by (safe_tac intrel_cs); -by (asm_simp_tac (intrel_ss addsimps add_ac) 1); +by (asm_simp_tac (!simpset addsimps add_ac) 1); qed "zminus_congruent"; @@ -125,10 +124,8 @@ goalw Integ.thy [zminus_def] "$~ Abs_Integ(intrel^^{(x,y)}) = Abs_Integ(intrel ^^ {(y,x)})"; by (res_inst_tac [("f","Abs_Integ")] arg_cong 1); -by (simp_tac (set_ss addsimps +by (simp_tac (!simpset addsimps [intrel_in_integ RS Abs_Integ_inverse,zminus_ize UN_equiv_class]) 1); -by (rewtac split_def); -by (simp_tac prod_ss 1); qed "zminus"; (*by lcp*) @@ -139,22 +136,22 @@ by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1); by (res_inst_tac [("p","x")] PairE 1); by (rtac prem 1); -by (asm_full_simp_tac (HOL_ss addsimps [Rep_Integ_inverse]) 1); +by (asm_full_simp_tac (!simpset addsimps [Rep_Integ_inverse]) 1); qed "eq_Abs_Integ"; goal Integ.thy "$~ ($~ z) = z"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); -by (asm_simp_tac (HOL_ss addsimps [zminus]) 1); +by (asm_simp_tac (!simpset addsimps [zminus]) 1); qed "zminus_zminus"; goal Integ.thy "inj(zminus)"; by (rtac injI 1); by (dres_inst_tac [("f","zminus")] arg_cong 1); -by (asm_full_simp_tac (HOL_ss addsimps [zminus_zminus]) 1); +by (asm_full_simp_tac (!simpset addsimps [zminus_zminus]) 1); qed "inj_zminus"; goalw Integ.thy [znat_def] "$~ ($#0) = $#0"; -by (simp_tac (arith_ss addsimps [zminus]) 1); +by (simp_tac (!simpset addsimps [zminus]) 1); qed "zminus_0"; @@ -162,7 +159,7 @@ goal Arith.thy "!!m x n::nat. n+m=x ==> m<=x"; by (dtac (disjI2 RS less_or_eq_imp_le) 1); -by (asm_full_simp_tac (arith_ss addsimps add_ac) 1); +by (asm_full_simp_tac (!simpset addsimps add_ac) 1); by (dtac add_leD1 1); by (assume_tac 1); qed "not_znegative_znat_lemma"; @@ -170,21 +167,21 @@ goalw Integ.thy [znegative_def, znat_def] "~ znegative($# n)"; -by (simp_tac intrel_ss 1); +by (Simp_tac 1); by (safe_tac intrel_cs); by (rtac ccontr 1); by (etac notE 1); -by (asm_full_simp_tac arith_ss 1); +by (Asm_full_simp_tac 1); by (dtac not_znegative_znat_lemma 1); by (fast_tac (HOL_cs addDs [leD]) 1); qed "not_znegative_znat"; goalw Integ.thy [znegative_def, znat_def] "znegative($~ $# Suc(n))"; -by (simp_tac (intrel_ss addsimps [zminus]) 1); +by (simp_tac (!simpset addsimps [zminus]) 1); by (REPEAT (ares_tac [exI, conjI] 1)); by (rtac (intrelI RS ImageI) 2); by (rtac singletonI 3); -by (simp_tac arith_ss 2); +by (Simp_tac 2); by (rtac less_add_Suc1 1); qed "znegative_zminus_znat"; @@ -193,29 +190,29 @@ goal Arith.thy "!!n::nat. n - Suc(n+m)=0"; by (nat_ind_tac "n" 1); -by (ALLGOALS(asm_simp_tac arith_ss)); +by (ALLGOALS Asm_simp_tac); qed "diff_Suc_add_0"; goal Arith.thy "Suc((n::nat)+m)-n=Suc(m)"; by (nat_ind_tac "n" 1); -by (ALLGOALS(asm_simp_tac arith_ss)); +by (ALLGOALS Asm_simp_tac); qed "diff_Suc_add_inverse"; goalw Integ.thy [congruent_def] "congruent intrel (split (%x y. intrel^^{((y-x) + (x-(y::nat)),0)}))"; by (safe_tac intrel_cs); -by (asm_simp_tac intrel_ss 1); +by (Asm_simp_tac 1); by (etac rev_mp 1); by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1); -by (asm_simp_tac (arith_ss addsimps [inj_Suc RS inj_eq]) 3); -by (asm_simp_tac (arith_ss addsimps [diff_add_inverse,diff_add_0]) 2); -by (asm_simp_tac arith_ss 1); +by (asm_simp_tac (!simpset addsimps [inj_Suc RS inj_eq]) 3); +by (asm_simp_tac (!simpset addsimps [diff_add_inverse,diff_add_0]) 2); +by (Asm_simp_tac 1); by (rtac impI 1); by (etac subst 1); by (res_inst_tac [("m1","x")] (add_commute RS ssubst) 1); -by (asm_simp_tac (arith_ss addsimps [diff_add_inverse,diff_add_0]) 1); +by (asm_simp_tac (!simpset addsimps [diff_add_inverse,diff_add_0]) 1); by (rtac impI 1); -by (asm_simp_tac (arith_ss addsimps +by (asm_simp_tac (!simpset addsimps [diff_add_inverse, diff_add_0, diff_Suc_add_0, diff_Suc_add_inverse]) 1); qed "zmagnitude_congruent"; @@ -228,15 +225,15 @@ "zmagnitude (Abs_Integ(intrel^^{(x,y)})) = \ \ Abs_Integ(intrel^^{((y - x) + (x - y),0)})"; by (res_inst_tac [("f","Abs_Integ")] arg_cong 1); -by (asm_simp_tac (intrel_ss addsimps [zmagnitude_ize UN_equiv_class]) 1); +by (asm_simp_tac (!simpset addsimps [zmagnitude_ize UN_equiv_class]) 1); qed "zmagnitude"; goalw Integ.thy [znat_def] "zmagnitude($# n) = $#n"; -by (asm_simp_tac (intrel_ss addsimps [zmagnitude]) 1); +by (asm_simp_tac (!simpset addsimps [zmagnitude]) 1); qed "zmagnitude_znat"; goalw Integ.thy [znat_def] "zmagnitude($~ $# n) = $#n"; -by (asm_simp_tac (intrel_ss addsimps [zmagnitude, zminus]) 1); +by (asm_simp_tac (!simpset addsimps [zmagnitude, zminus]) 1); qed "zmagnitude_zminus_znat"; @@ -249,11 +246,11 @@ \ split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)"; (*Proof via congruent2_commuteI seems longer*) by (safe_tac intrel_cs); -by (asm_simp_tac (intrel_ss addsimps [add_assoc]) 1); +by (asm_simp_tac (!simpset addsimps [add_assoc]) 1); (*The rest should be trivial, but rearranging terms is hard*) by (res_inst_tac [("x1","x1a")] (add_left_commute RS ssubst) 1); -by (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]) 1); -by (asm_simp_tac (arith_ss addsimps add_ac) 1); +by (asm_simp_tac (!simpset addsimps [add_assoc RS sym]) 1); +by (asm_simp_tac (!simpset addsimps add_ac) 1); qed "zadd_congruent2"; (*Resolve th against the corresponding facts for zadd*) @@ -263,31 +260,31 @@ "Abs_Integ(intrel^^{(x1,y1)}) + Abs_Integ(intrel^^{(x2,y2)}) = \ \ Abs_Integ(intrel^^{(x1+x2, y1+y2)})"; by (asm_simp_tac - (intrel_ss addsimps [zadd_ize UN_equiv_class2]) 1); + (!simpset addsimps [zadd_ize UN_equiv_class2]) 1); qed "zadd"; goalw Integ.thy [znat_def] "$#0 + z = z"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); -by (asm_simp_tac (arith_ss addsimps [zadd]) 1); +by (asm_simp_tac (!simpset addsimps [zadd]) 1); qed "zadd_0"; goal Integ.thy "$~ (z + w) = $~ z + $~ w"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (res_inst_tac [("z","w")] eq_Abs_Integ 1); -by (asm_simp_tac (arith_ss addsimps [zminus,zadd]) 1); +by (asm_simp_tac (!simpset addsimps [zminus,zadd]) 1); qed "zminus_zadd_distrib"; goal Integ.thy "(z::int) + w = w + z"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (res_inst_tac [("z","w")] eq_Abs_Integ 1); -by (asm_simp_tac (intrel_ss addsimps (add_ac @ [zadd])) 1); +by (asm_simp_tac (!simpset addsimps (add_ac @ [zadd])) 1); qed "zadd_commute"; goal Integ.thy "((z1::int) + z2) + z3 = z1 + (z2 + z3)"; by (res_inst_tac [("z","z1")] eq_Abs_Integ 1); by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); by (res_inst_tac [("z","z3")] eq_Abs_Integ 1); -by (asm_simp_tac (arith_ss addsimps [zadd, add_assoc]) 1); +by (asm_simp_tac (!simpset addsimps [zadd, add_assoc]) 1); qed "zadd_assoc"; (*For AC rewriting*) @@ -301,12 +298,12 @@ val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute]; goalw Integ.thy [znat_def] "$# (m + n) = ($#m) + ($#n)"; -by (asm_simp_tac (arith_ss addsimps [zadd]) 1); +by (asm_simp_tac (!simpset addsimps [zadd]) 1); qed "znat_add"; goalw Integ.thy [znat_def] "z + ($~ z) = $#0"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); -by (asm_simp_tac (intrel_ss addsimps [zminus, zadd, add_commute]) 1); +by (asm_simp_tac (!simpset addsimps [zminus, zadd, add_commute]) 1); qed "zadd_zminus_inverse"; goal Integ.thy "($~ z) + z = $#0"; @@ -327,7 +324,7 @@ (** Congruence property for multiplication **) goal Integ.thy "((k::nat) + l) + (m + n) = (k + m) + (n + l)"; -by (simp_tac (arith_ss addsimps add_ac) 1); +by (simp_tac (!simpset addsimps add_ac) 1); qed "zmult_congruent_lemma"; goal Integ.thy @@ -337,15 +334,17 @@ by (rtac (equiv_intrel RS congruent2_commuteI) 1); by (safe_tac intrel_cs); by (rewtac split_def); -by (simp_tac (arith_ss addsimps add_ac@mult_ac) 1); -by (asm_simp_tac (arith_ss addsimps add_ac@mult_ac) 1); +by (simp_tac (!simpset addsimps add_ac@mult_ac) 1); +by (asm_simp_tac (!simpset delsimps [equiv_intrel_iff] + addsimps add_ac@mult_ac) 1); by (rtac (intrelI RS(equiv_intrel RS equiv_class_eq)) 1); by (rtac (zmult_congruent_lemma RS trans) 1); by (rtac (zmult_congruent_lemma RS trans RS sym) 1); by (rtac (zmult_congruent_lemma RS trans RS sym) 1); by (rtac (zmult_congruent_lemma RS trans RS sym) 1); -by (asm_simp_tac (HOL_ss addsimps [add_mult_distrib RS sym]) 1); -by (asm_simp_tac (arith_ss addsimps add_ac@mult_ac) 1); +by (asm_simp_tac (!simpset delsimps [add_mult_distrib] + addsimps [add_mult_distrib RS sym]) 1); +by (asm_simp_tac (!simpset addsimps add_ac@mult_ac) 1); qed "zmult_congruent2"; (*Resolve th against the corresponding facts for zmult*) @@ -354,36 +353,36 @@ goalw Integ.thy [zmult_def] "Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) = \ \ Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})"; -by (simp_tac (intrel_ss addsimps [zmult_ize UN_equiv_class2]) 1); +by (simp_tac (!simpset addsimps [zmult_ize UN_equiv_class2]) 1); qed "zmult"; goalw Integ.thy [znat_def] "$#0 * z = $#0"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); -by (asm_simp_tac (arith_ss addsimps [zmult]) 1); +by (asm_simp_tac (!simpset addsimps [zmult]) 1); qed "zmult_0"; goalw Integ.thy [znat_def] "$#Suc(0) * z = z"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); -by (asm_simp_tac (arith_ss addsimps [zmult, add_0_right]) 1); +by (asm_simp_tac (!simpset addsimps [zmult]) 1); qed "zmult_1"; goal Integ.thy "($~ z) * w = $~ (z * w)"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (res_inst_tac [("z","w")] eq_Abs_Integ 1); -by (asm_simp_tac (intrel_ss addsimps ([zminus, zmult] @ add_ac)) 1); +by (asm_simp_tac (!simpset addsimps ([zminus, zmult] @ add_ac)) 1); qed "zmult_zminus"; goal Integ.thy "($~ z) * ($~ w) = (z * w)"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (res_inst_tac [("z","w")] eq_Abs_Integ 1); -by (asm_simp_tac (intrel_ss addsimps ([zminus, zmult] @ add_ac)) 1); +by (asm_simp_tac (!simpset addsimps ([zminus, zmult] @ add_ac)) 1); qed "zmult_zminus_zminus"; goal Integ.thy "(z::int) * w = w * z"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (res_inst_tac [("z","w")] eq_Abs_Integ 1); -by (asm_simp_tac (intrel_ss addsimps ([zmult] @ add_ac @ mult_ac)) 1); +by (asm_simp_tac (!simpset addsimps ([zmult] @ add_ac @ mult_ac)) 1); qed "zmult_commute"; goal Integ.thy "z * $# 0 = $#0"; @@ -398,7 +397,7 @@ by (res_inst_tac [("z","z1")] eq_Abs_Integ 1); by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); by (res_inst_tac [("z","z3")] eq_Abs_Integ 1); -by (asm_simp_tac (intrel_ss addsimps ([zmult] @ add_ac @ mult_ac)) 1); +by (asm_simp_tac (!simpset addsimps ([zmult] @ add_ac @ mult_ac)) 1); qed "zmult_assoc"; (*For AC rewriting*) @@ -415,18 +414,17 @@ by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); by (res_inst_tac [("z","w")] eq_Abs_Integ 1); by (asm_simp_tac - (intrel_ss addsimps ([zadd, zmult, add_mult_distrib] @ - add_ac @ mult_ac)) 1); + (!simpset addsimps ([zadd, zmult] @ add_ac @ mult_ac)) 1); qed "zadd_zmult_distrib"; val zmult_commute'= read_instantiate [("z","w")] zmult_commute; goal Integ.thy "w * ($~ z) = $~ (w * z)"; -by (simp_tac (HOL_ss addsimps [zmult_commute', zmult_zminus]) 1); +by (simp_tac (!simpset addsimps [zmult_commute', zmult_zminus]) 1); qed "zmult_zminus_right"; goal Integ.thy "(w::int) * (z1 + z2) = (w * z1) + (w * z2)"; -by (simp_tac (HOL_ss addsimps [zmult_commute',zadd_zmult_distrib]) 1); +by (simp_tac (!simpset addsimps [zmult_commute',zadd_zmult_distrib]) 1); qed "zadd_zmult_distrib2"; val zadd_simps = @@ -437,34 +435,33 @@ val zmult_simps = [zmult_0, zmult_1, zmult_0_right, zmult_1_right, zmult_zminus, zmult_zminus_right]; -val integ_ss = - arith_ss addsimps (zadd_simps @ zminus_simps @ zmult_simps @ - [zmagnitude_znat, zmagnitude_zminus_znat]); +Addsimps (zadd_simps @ zminus_simps @ zmult_simps @ + [zmagnitude_znat, zmagnitude_zminus_znat]); (**** Additional Theorems (by Mattolini; proofs mainly by lcp) ****) (* Some Theorems about zsuc and zpred *) goalw Integ.thy [zsuc_def] "$#(Suc(n)) = zsuc($# n)"; -by (simp_tac (arith_ss addsimps [znat_add RS sym]) 1); +by (simp_tac (!simpset addsimps [znat_add RS sym]) 1); qed "znat_Suc"; goalw Integ.thy [zpred_def,zsuc_def,zdiff_def] "$~ zsuc(z) = zpred($~ z)"; -by (simp_tac integ_ss 1); +by (Simp_tac 1); qed "zminus_zsuc"; goalw Integ.thy [zpred_def,zsuc_def,zdiff_def] "$~ zpred(z) = zsuc($~ z)"; -by (simp_tac integ_ss 1); +by (Simp_tac 1); qed "zminus_zpred"; goalw Integ.thy [zsuc_def,zpred_def,zdiff_def] "zpred(zsuc(z)) = z"; -by (simp_tac (integ_ss addsimps [zadd_assoc]) 1); +by (simp_tac (!simpset addsimps [zadd_assoc]) 1); qed "zpred_zsuc"; goalw Integ.thy [zsuc_def,zpred_def,zdiff_def] "zsuc(zpred(z)) = z"; -by (simp_tac (integ_ss addsimps [zadd_assoc]) 1); +by (simp_tac (!simpset addsimps [zadd_assoc]) 1); qed "zsuc_zpred"; goal Integ.thy "(zpred(z)=w) = (z=zsuc(w))"; @@ -488,56 +485,56 @@ goal Integ.thy"(zsuc(z)=zsuc(w)) = (z=w)"; by (safe_tac intrel_cs); by (dres_inst_tac [("f","zpred")] arg_cong 1); -by (asm_full_simp_tac (HOL_ss addsimps [zpred_zsuc]) 1); +by (asm_full_simp_tac (!simpset addsimps [zpred_zsuc]) 1); qed "bijective_zsuc"; goal Integ.thy"(zpred(z)=zpred(w)) = (z=w)"; by (safe_tac intrel_cs); by (dres_inst_tac [("f","zsuc")] arg_cong 1); -by (asm_full_simp_tac (HOL_ss addsimps [zsuc_zpred]) 1); +by (asm_full_simp_tac (!simpset addsimps [zsuc_zpred]) 1); qed "bijective_zpred"; (* Additional Theorems about zadd *) goalw Integ.thy [zsuc_def] "zsuc(z) + w = zsuc(z+w)"; -by (simp_tac (arith_ss addsimps zadd_ac) 1); +by (simp_tac (!simpset addsimps zadd_ac) 1); qed "zadd_zsuc"; goalw Integ.thy [zsuc_def] "w + zsuc(z) = zsuc(w+z)"; -by (simp_tac (arith_ss addsimps zadd_ac) 1); +by (simp_tac (!simpset addsimps zadd_ac) 1); qed "zadd_zsuc_right"; goalw Integ.thy [zpred_def,zdiff_def] "zpred(z) + w = zpred(z+w)"; -by (simp_tac (arith_ss addsimps zadd_ac) 1); +by (simp_tac (!simpset addsimps zadd_ac) 1); qed "zadd_zpred"; goalw Integ.thy [zpred_def,zdiff_def] "w + zpred(z) = zpred(w+z)"; -by (simp_tac (arith_ss addsimps zadd_ac) 1); +by (simp_tac (!simpset addsimps zadd_ac) 1); qed "zadd_zpred_right"; (* Additional Theorems about zmult *) goalw Integ.thy [zsuc_def] "zsuc(w) * z = z + w * z"; -by (simp_tac (integ_ss addsimps [zadd_zmult_distrib, zadd_commute]) 1); +by (simp_tac (!simpset addsimps [zadd_zmult_distrib, zadd_commute]) 1); qed "zmult_zsuc"; goalw Integ.thy [zsuc_def] "z * zsuc(w) = z + w * z"; by (simp_tac - (integ_ss addsimps [zadd_zmult_distrib2, zadd_commute, zmult_commute]) 1); + (!simpset addsimps [zadd_zmult_distrib2, zadd_commute, zmult_commute]) 1); qed "zmult_zsuc_right"; goalw Integ.thy [zpred_def, zdiff_def] "zpred(w) * z = w * z - z"; -by (simp_tac (integ_ss addsimps [zadd_zmult_distrib]) 1); +by (simp_tac (!simpset addsimps [zadd_zmult_distrib]) 1); qed "zmult_zpred"; goalw Integ.thy [zpred_def, zdiff_def] "z * zpred(w) = w * z - z"; -by (simp_tac (integ_ss addsimps [zadd_zmult_distrib2, zmult_commute]) 1); +by (simp_tac (!simpset addsimps [zadd_zmult_distrib2, zmult_commute]) 1); qed "zmult_zpred_right"; (* Further Theorems about zsuc and zpred *) goal Integ.thy "$#Suc(m) ~= $#0"; -by (simp_tac (integ_ss addsimps [inj_znat RS inj_eq]) 1); +by (simp_tac (!simpset addsimps [inj_znat RS inj_eq]) 1); qed "znat_Suc_not_znat_Zero"; bind_thm ("znat_Zero_not_znat_Suc", (znat_Suc_not_znat_Zero RS not_sym)); @@ -545,7 +542,7 @@ goalw Integ.thy [zsuc_def,znat_def] "w ~= zsuc(w)"; by (res_inst_tac [("z","w")] eq_Abs_Integ 1); -by (asm_full_simp_tac (intrel_ss addsimps [zadd]) 1); +by (asm_full_simp_tac (!simpset addsimps [zadd]) 1); qed "n_not_zsuc_n"; val zsuc_n_not_n = n_not_zsuc_n RS not_sym; @@ -553,7 +550,7 @@ goal Integ.thy "w ~= zpred(w)"; by (safe_tac HOL_cs); by (dres_inst_tac [("x","w"),("f","zsuc")] arg_cong 1); -by (asm_full_simp_tac (HOL_ss addsimps [zsuc_zpred,zsuc_n_not_n]) 1); +by (asm_full_simp_tac (!simpset addsimps [zsuc_zpred,zsuc_n_not_n]) 1); qed "n_not_zpred_n"; val zpred_n_not_n = n_not_zpred_n RS not_sym; @@ -566,30 +563,32 @@ by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (res_inst_tac [("z","w")] eq_Abs_Integ 1); by (safe_tac intrel_cs); -by (asm_full_simp_tac (intrel_ss addsimps [zadd, zminus]) 1); +by (asm_full_simp_tac (!simpset addsimps [zadd, zminus]) 1); by (safe_tac (intrel_cs addSDs [less_eq_Suc_add])); by (res_inst_tac [("x","k")] exI 1); -by (asm_full_simp_tac (HOL_ss addsimps ([add_Suc RS sym] @ add_ac)) 1); +by (asm_full_simp_tac (!simpset delsimps [add_Suc, add_Suc_right] + addsimps ([add_Suc RS sym] @ add_ac)) 1); (*To cancel x2, rename it to be first!*) by (rename_tac "a b c" 1); -by (asm_full_simp_tac (HOL_ss addsimps (add_left_cancel::add_ac)) 1); +by (asm_full_simp_tac (!simpset delsimps [add_Suc_right] + addsimps (add_left_cancel::add_ac)) 1); qed "zless_eq_zadd_Suc"; goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] "z < z + $#(Suc(n))"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (safe_tac intrel_cs); -by (simp_tac (intrel_ss addsimps [zadd, zminus]) 1); +by (simp_tac (!simpset addsimps [zadd, zminus]) 1); by (REPEAT_SOME (ares_tac [refl, exI, singletonI, ImageI, conjI, intrelI])); by (rtac le_less_trans 1); by (rtac lessI 2); -by (asm_simp_tac (arith_ss addsimps ([le_add1,add_left_cancel_le]@add_ac)) 1); +by (asm_simp_tac (!simpset addsimps ([le_add1,add_left_cancel_le]@add_ac)) 1); qed "zless_zadd_Suc"; goal Integ.thy "!!z1 z2 z3. [| z1 z1 < (z3::int)"; by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc])); by (simp_tac - (arith_ss addsimps [zadd_assoc, zless_zadd_Suc, znat_add RS sym]) 1); + (!simpset addsimps [zadd_assoc, zless_zadd_Suc, znat_add RS sym]) 1); qed "zless_trans"; goalw Integ.thy [zsuc_def] "z z<=(w::int)"; @@ -691,7 +690,7 @@ qed "zle_eq_zless_or_eq"; goal Integ.thy "w <= (w::int)"; -by (simp_tac (HOL_ss addsimps [zle_eq_zless_or_eq]) 1); +by (simp_tac (!simpset addsimps [zle_eq_zless_or_eq]) 1); qed "zle_refl"; val prems = goal Integ.thy "!!i. [| i <= j; j < k |] ==> i < (k::int)"; @@ -712,7 +711,7 @@ goal Integ.thy "!!w w' z::int. z + w' = z + w ==> w' = w"; by (dres_inst_tac [("f", "%x. x + $~z")] arg_cong 1); -by (asm_full_simp_tac (integ_ss addsimps zadd_ac) 1); +by (asm_full_simp_tac (!simpset addsimps zadd_ac) 1); qed "zadd_left_cancel"; @@ -720,19 +719,19 @@ goal Integ.thy "!!v w z::int. v < w ==> v + z < w + z"; by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc])); -by (simp_tac (HOL_ss addsimps zadd_ac) 1); -by (simp_tac (HOL_ss addsimps [zadd_assoc RS sym, zless_zadd_Suc]) 1); +by (simp_tac (!simpset addsimps zadd_ac) 1); +by (simp_tac (!simpset addsimps [zadd_assoc RS sym, zless_zadd_Suc]) 1); qed "zadd_zless_mono1"; goal Integ.thy "!!v w z::int. (v+z < w+z) = (v < w)"; by (safe_tac (HOL_cs addSEs [zadd_zless_mono1])); by (dres_inst_tac [("z", "$~z")] zadd_zless_mono1 1); -by (asm_full_simp_tac (integ_ss addsimps [zadd_assoc]) 1); +by (asm_full_simp_tac (!simpset addsimps [zadd_assoc]) 1); qed "zadd_left_cancel_zless"; goal Integ.thy "!!v w z::int. (v+z <= w+z) = (v <= w)"; by (asm_full_simp_tac - (integ_ss addsimps [zle_def, zadd_left_cancel_zless]) 1); + (!simpset addsimps [zle_def, zadd_left_cancel_zless]) 1); qed "zadd_left_cancel_zle"; (*"v<=w ==> v+z <= w+z"*) @@ -741,12 +740,12 @@ goal Integ.thy "!!z' z::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z"; by (etac (zadd_zle_mono1 RS zle_trans) 1); -by (simp_tac (HOL_ss addsimps [zadd_commute]) 1); +by (simp_tac (!simpset addsimps [zadd_commute]) 1); (*w moves to the end because it is free while z', z are bound*) by (etac zadd_zle_mono1 1); qed "zadd_zle_mono"; goal Integ.thy "!!w z::int. z<=$#0 ==> w+z <= w"; by (dres_inst_tac [("z", "w")] zadd_zle_mono1 1); -by (asm_full_simp_tac (integ_ss addsimps [zadd_commute]) 1); +by (asm_full_simp_tac (!simpset addsimps [zadd_commute]) 1); qed "zadd_zle_self"; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/Lambda/Confluence.ML --- a/src/HOL/Lambda/Confluence.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/Lambda/Confluence.ML Wed Oct 04 13:12:14 1995 +0100 @@ -31,7 +31,7 @@ bd rtrancl_mono 1; by(fast_tac (HOL_cs addIs [diamond_diamond_rtrancl] addDs [subset_antisym] - addss (HOL_ss addsimps [rtrancl_idemp])) 1); + addss (!simpset addsimps [rtrancl_idemp])) 1); qed "diamond_to_confluence"; goalw Confluence.thy [confluent_def,diamond_def,Church_Rosser_def] diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/Lambda/Lambda.ML --- a/src/HOL/Lambda/Lambda.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/Lambda/Lambda.ML Wed Oct 04 13:12:14 1995 +0100 @@ -15,36 +15,36 @@ goal Nat.thy "!!i. [| i < Suc j; j < k |] ==> i < k"; br le_less_trans 1; ba 2; -by(asm_full_simp_tac (nat_ss addsimps [le_def]) 1); +by(asm_full_simp_tac (!simpset addsimps [le_def]) 1); by(fast_tac (HOL_cs addEs [less_asym,less_anti_refl]) 1); qed "lt_trans1"; goal Nat.thy "!!i. [| i < j; j < Suc(k) |] ==> i < k"; be less_le_trans 1; -by(asm_full_simp_tac (nat_ss addsimps [le_def]) 1); +by(asm_full_simp_tac (!simpset addsimps [le_def]) 1); by(fast_tac (HOL_cs addEs [less_asym,less_anti_refl]) 1); qed "lt_trans2"; val major::prems = goal Nat.thy "[| i < Suc j; i < j ==> P; i = j ==> P |] ==> P"; br (major RS lessE) 1; -by(ALLGOALS(asm_full_simp_tac nat_ss)); +by(ALLGOALS Asm_full_simp_tac); by(resolve_tac prems 1 THEN etac sym 1); by(fast_tac (HOL_cs addIs prems) 1); qed "leqE"; goal Arith.thy "!!i. i < j ==> Suc(pred j) = j"; -by(fast_tac (HOL_cs addEs [lessE] addss arith_ss) 1); +by(fast_tac (HOL_cs addEs [lessE] addss !simpset) 1); qed "Suc_pred"; goal Arith.thy "!!i. Suc i < j ==> i < pred j "; by (resolve_tac [Suc_less_SucD] 1); -by (asm_simp_tac (arith_ss addsimps [Suc_pred]) 1); +by (asm_simp_tac (!simpset addsimps [Suc_pred]) 1); qed "lt_pred"; goal Arith.thy "!!i. [| i < Suc j; k < i |] ==> pred i < j "; by (resolve_tac [Suc_less_SucD] 1); -by (asm_simp_tac (arith_ss addsimps [Suc_pred]) 1); +by (asm_simp_tac (!simpset addsimps [Suc_pred]) 1); qed "gt_pred"; @@ -52,11 +52,7 @@ open Lambda; -val lambda_ss = arith_ss delsimps [less_Suc_eq] addsimps - db.simps @ beta.intrs @ - [if_not_P, not_less_eq, - subst_App,subst_Fun, - lift_Var,lift_App,lift_Fun]; +Addsimps [if_not_P, not_less_eq]; val lambda_cs = HOL_cs addSIs beta.intrs; @@ -84,127 +80,127 @@ (*** subst and lift ***) -fun addsplit ss = ss addsimps [subst_Var] setloop (split_tac [expand_if]); +val split_ss = !simpset delsimps [less_Suc_eq,subst_Var] + addsimps [subst_Var] + setloop (split_tac [expand_if]); goal Lambda.thy "(Var k)[u/k] = u"; -by (asm_full_simp_tac (addsplit lambda_ss) 1); +by (asm_full_simp_tac split_ss 1); qed "subst_eq"; goal Lambda.thy "!!s. i (Var j)[u/i] = Var(pred j)"; -by (asm_full_simp_tac (addsplit lambda_ss) 1); +by (asm_full_simp_tac split_ss 1); qed "subst_gt"; goal Lambda.thy "!!s. j (Var j)[u/i] = Var(j)"; -by (asm_full_simp_tac (addsplit lambda_ss addsimps +by (asm_full_simp_tac (split_ss addsimps [less_not_refl2 RS not_sym,less_SucI]) 1); qed "subst_lt"; -val lambda_ss = lambda_ss addsimps [subst_eq,subst_gt,subst_lt]; +Addsimps [subst_eq,subst_gt,subst_lt]; +val ss = !simpset delsimps [less_Suc_eq, subst_Var]; goal Lambda.thy "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i"; by(db.induct_tac "t" 1); -by(ALLGOALS(asm_simp_tac lambda_ss)); +by(ALLGOALS (asm_simp_tac ss)); by(strip_tac 1); by (excluded_middle_tac "nat < i" 1); by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2)); -by (ALLGOALS(asm_full_simp_tac ((addsplit lambda_ss) addsimps [less_SucI]))); +by (ALLGOALS(asm_full_simp_tac (split_ss addsimps [less_SucI]))); qed"lift_lift"; goal Lambda.thy "!i j s. j < Suc i --> \ \ lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]"; by(db.induct_tac "t" 1); -by(ALLGOALS(asm_simp_tac (lambda_ss addsimps [lift_lift]))); +by(ALLGOALS(asm_simp_tac (ss addsimps [lift_lift]))); by(strip_tac 1); by (excluded_middle_tac "nat < j" 1); -by (asm_full_simp_tac lambda_ss 1); +by (asm_full_simp_tac ss 1); by (eres_inst_tac [("j","nat")] leqE 1); -by (asm_full_simp_tac ((addsplit lambda_ss) - addsimps [less_SucI,gt_pred,Suc_pred]) 1); +by (asm_full_simp_tac (split_ss addsimps [less_SucI,gt_pred,Suc_pred]) 1); by (hyp_subst_tac 1); -by (asm_simp_tac lambda_ss 1); +by (Asm_simp_tac 1); by (forw_inst_tac [("j","j")] lt_trans2 1); by (assume_tac 1); -by (asm_full_simp_tac (addsplit lambda_ss addsimps [less_SucI]) 1); +by (asm_full_simp_tac (split_ss addsimps [less_SucI]) 1); qed "lift_subst"; -val lambda_ss = lambda_ss addsimps [lift_subst]; +Addsimps [lift_subst]; goal Lambda.thy "!i j s. i < Suc j -->\ \ lift (t[s/j]) i = (lift t i) [lift s i / Suc j]"; by(db.induct_tac "t" 1); -by(ALLGOALS(asm_simp_tac (lambda_ss addsimps [lift_lift]))); +by(ALLGOALS(asm_simp_tac (ss addsimps [lift_lift]))); by(strip_tac 1); by (excluded_middle_tac "nat < j" 1); -by (asm_full_simp_tac lambda_ss 1); +by (asm_full_simp_tac ss 1); by (eres_inst_tac [("i","j")] leqE 1); by (forward_tac [lt_trans1] 1 THEN assume_tac 1); -by (ALLGOALS(asm_full_simp_tac - (lambda_ss addsimps [Suc_pred,less_SucI,gt_pred]))); +by (ALLGOALS(asm_full_simp_tac (ss addsimps [Suc_pred,less_SucI,gt_pred]))); by (hyp_subst_tac 1); -by (asm_full_simp_tac (lambda_ss addsimps [less_SucI]) 1); +by (asm_full_simp_tac (ss addsimps [less_SucI]) 1); by(split_tac [expand_if] 1); -by (asm_full_simp_tac (lambda_ss addsimps [less_SucI]) 1); +by (asm_full_simp_tac (!simpset addsimps [less_SucI]) 1); qed "lift_subst_lt"; goal Lambda.thy "!k s. (lift t k)[s/k] = t"; by(db.induct_tac "t" 1); -by(ALLGOALS(asm_simp_tac lambda_ss)); +by(ALLGOALS Asm_simp_tac); by(split_tac [expand_if] 1); -by(ALLGOALS(asm_full_simp_tac lambda_ss)); +by(ALLGOALS Asm_full_simp_tac); qed "subst_lift"; -val lambda_ss = lambda_ss addsimps [subst_lift]; +Addsimps [subst_lift]; goal Lambda.thy "!i j u v. i < Suc j --> \ \ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"; by(db.induct_tac "t" 1); -by (ALLGOALS(asm_simp_tac (lambda_ss addsimps +by (ALLGOALS(asm_simp_tac (ss addsimps [lift_lift RS spec RS spec RS mp RS sym,lift_subst_lt]))); by(strip_tac 1); by (excluded_middle_tac "nat < Suc(Suc j)" 1); -by(asm_full_simp_tac lambda_ss 1); +by(asm_full_simp_tac ss 1); by (forward_tac [lessI RS less_trans] 1); by (eresolve_tac [leqE] 1); -by (asm_simp_tac (lambda_ss addsimps [Suc_pred,lt_pred]) 2); +by (asm_simp_tac (ss addsimps [Suc_pred,lt_pred]) 2); by (forward_tac [Suc_mono RS less_trans] 1 THEN assume_tac 1); by (forw_inst_tac [("i","i")] (lessI RS less_trans) 1); -by (asm_simp_tac (lambda_ss addsimps [Suc_pred,lt_pred]) 1); +by (asm_simp_tac (ss addsimps [Suc_pred,lt_pred]) 1); by (eres_inst_tac [("i","nat")] leqE 1); -by (asm_full_simp_tac (lambda_ss addsimps [Suc_pred,less_SucI]) 2); +by (asm_full_simp_tac (!simpset delsimps [less_Suc_eq] + addsimps [Suc_pred,less_SucI]) 2); by (excluded_middle_tac "nat < i" 1); -by (asm_full_simp_tac lambda_ss 1); +by (asm_full_simp_tac ss 1); by (eres_inst_tac [("j","nat")] leqE 1); -by (asm_simp_tac (lambda_ss addsimps [gt_pred]) 1); -by (asm_simp_tac lambda_ss 1); +by (asm_simp_tac (!simpset addsimps [gt_pred]) 1); +by (Asm_simp_tac 1); by (forward_tac [lt_trans2] 1 THEN assume_tac 1); -by (asm_simp_tac (lambda_ss addsimps [gt_pred]) 1); +by (asm_simp_tac (!simpset addsimps [gt_pred]) 1); bind_thm("subst_subst", result() RS spec RS spec RS spec RS spec RS mp); -val lambda_ss = lambda_ss addsimps - [liftn_Var,liftn_App,liftn_Fun,substn_Var,substn_App,substn_Fun]; (*** Equivalence proof for optimized substitution ***) goal Lambda.thy "!k. liftn 0 t k = t"; by(db.induct_tac "t" 1); -by(ALLGOALS(asm_simp_tac (addsplit lambda_ss))); +by(ALLGOALS(asm_simp_tac split_ss)); qed "liftn_0"; -val lambda_ss = lambda_ss addsimps [liftn_0]; +Addsimps [liftn_0]; goal Lambda.thy "!k. liftn (Suc n) t k = lift (liftn n t k) k"; by(db.induct_tac "t" 1); -by(ALLGOALS(asm_simp_tac (addsplit lambda_ss))); +by(ALLGOALS(asm_simp_tac split_ss)); by(fast_tac (HOL_cs addDs [add_lessD1]) 1); qed "liftn_lift"; -val lambda_ss = lambda_ss addsimps [liftn_lift]; +Addsimps [liftn_lift]; goal Lambda.thy "!n. substn t s n = t[liftn n s 0 / n]"; by(db.induct_tac "t" 1); -by(ALLGOALS(asm_simp_tac (addsplit lambda_ss))); +by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); qed "substn_subst_n"; -val lambda_ss = lambda_ss addsimps [substn_subst_n]; +Addsimps [substn_subst_n]; goal Lambda.thy "substn t s 0 = t[s/0]"; -by(simp_tac lambda_ss 1); +by(Simp_tac 1); qed "substn_subst_0"; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/Lambda/ParRed.ML --- a/src/HOL/Lambda/ParRed.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/Lambda/ParRed.ML Wed Oct 04 13:12:14 1995 +0100 @@ -9,8 +9,7 @@ open ParRed; -val parred_ss = lambda_ss addsimps - par_beta.intrs @ [cd_Var,cd_Fun]; +Addsimps par_beta.intrs; val par_beta_cases = map (par_beta.mk_cases db.simps) ["Var n => t", "Fun s => Fun t", @@ -23,13 +22,13 @@ goal ParRed.thy "(Var n => t) = (t = Var n)"; by(fast_tac parred_cs 1); qed "par_beta_varL"; -val parred_ss = parred_ss addsimps [par_beta_varL]; +Addsimps [par_beta_varL]; goal ParRed.thy "t => t"; by(db.induct_tac "t" 1); -by(ALLGOALS(asm_simp_tac parred_ss)); +by(ALLGOALS Asm_simp_tac); qed"par_beta_refl"; -val parred_ss = parred_ss addsimps [par_beta_refl]; +Addsimps [par_beta_refl]; goal ParRed.thy "beta <= par_beta"; br subsetI 1; @@ -53,21 +52,21 @@ goal ParRed.thy "!t' n. t => t' --> lift t n => lift t' n"; by(db.induct_tac "t" 1); -by(ALLGOALS(fast_tac (parred_cs addss parred_ss))); +by(ALLGOALS(fast_tac (parred_cs addss (!simpset)))); bind_thm("par_beta_lift", result() RS spec RS spec RS mp); -val parred_ss = parred_ss addsimps [par_beta_lift]; +Addsimps [par_beta_lift]; goal ParRed.thy "!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]"; by(db.induct_tac "t" 1); - by(asm_simp_tac (addsplit parred_ss) 1); + by(asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1); by(strip_tac 1); bes par_beta_cases 1; - by(asm_simp_tac parred_ss 1); - by(asm_simp_tac parred_ss 1); + by(Asm_simp_tac 1); + by(Asm_simp_tac 1); br (zero_less_Suc RS subst_subst RS subst) 1; - by(fast_tac (parred_cs addSIs [par_beta_lift] addss parred_ss) 1); -by(fast_tac (parred_cs addss parred_ss) 1); + by(fast_tac (parred_cs addSIs [par_beta_lift] addss (!simpset)) 1); +by(fast_tac (parred_cs addss (!simpset)) 1); bind_thm("par_beta_subst", result() RS spec RS spec RS spec RS spec RS mp RS mp); @@ -84,34 +83,34 @@ (*** cd ***) goal ParRed.thy "cd(Var n @ t) = Var n @ cd t"; -by(simp_tac (parred_ss addsimps [cd_App]) 1); +by(Simp_tac 1); qed"cd_App_Var"; goal ParRed.thy "cd((r @ s) @ t) = cd(r @ s) @ cd t"; -by(simp_tac (parred_ss addsimps [cd_App]) 1); +by(Simp_tac 1); qed"cd_App_App"; goal ParRed.thy "cd((Fun s) @ t) = (cd s)[cd t/0]"; -by(simp_tac (parred_ss addsimps [cd_App,deFun_Fun]) 1); +by(Simp_tac 1); qed"cd_App_Fun"; -val parred_ss = parred_ss addsimps [cd_App_Var,cd_App_App,cd_App_Fun]; +Addsimps [cd_App_Var,cd_App_App,cd_App_Fun]; goal ParRed.thy "!t. s => t --> t => cd s"; by(db.induct_tac "s" 1); - by(simp_tac parred_ss 1); + by(Simp_tac 1); be rev_mp 1; by(db.induct_tac "db1" 1); - by(ALLGOALS(fast_tac (parred_cs addSIs [par_beta_subst] addss parred_ss))); + by(ALLGOALS(fast_tac (parred_cs addSIs [par_beta_subst] addss (!simpset)))); bind_thm("par_beta_cd", result() RS spec RS mp); (*** Confluence (via cd) ***) goalw ParRed.thy [diamond_def] "diamond(par_beta)"; by(fast_tac (HOL_cs addIs [par_beta_cd]) 1); -qed "diamond_par_beta"; +qed "diamond_par_beta2"; goal ParRed.thy "confluent(beta)"; -by(fast_tac (HOL_cs addIs [diamond_par_beta,diamond_to_confluence, +by(fast_tac (HOL_cs addIs [diamond_par_beta2,diamond_to_confluence, par_beta_subset_beta,beta_subset_par_beta]) 1); qed"beta_confluent"; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/Subst/AList.ML --- a/src/HOL/Subst/AList.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/Subst/AList.ML Wed Oct 04 13:12:14 1995 +0100 @@ -9,7 +9,7 @@ val al_rews = let fun mk_thm s = prove_goalw AList.thy [alist_rec_def,assoc_def] s - (fn _ => [simp_tac list_ss 1]) + (fn _ => [Simp_tac 1]) in map mk_thm ["alist_rec [] c d = c", "alist_rec ((a,b)#al) c d = d a b al (alist_rec al c d)", diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/Subst/ROOT.ML --- a/src/HOL/Subst/ROOT.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/Subst/ROOT.ML Wed Oct 04 13:12:14 1995 +0100 @@ -1,4 +1,5 @@ -(* Title: HOL/Subst +(* Title: HOL/Subst/ROOT.ML + ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge @@ -26,12 +27,7 @@ writeln"Root file for Substitutions and Unification"; loadpath := ["Subst"]; -use_thy "Subst/Setplus"; -use_thy "Subst/AList"; -use_thy "Subst/UTerm"; -use_thy "Subst/UTLemmas"; +use_thy "Unifier"; -use_thy "Subst/Subst"; -use_thy "Subst/Unifier"; writeln"END: Root file for Substitutions and Unification"; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/Subst/Setplus.ML --- a/src/HOL/Subst/Setplus.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/Subst/Setplus.ML Wed Oct 04 13:12:14 1995 +0100 @@ -21,13 +21,13 @@ qed "ssubset_iff"; goal Setplus.thy "((A::'a set) <= B) = ((A < B) | (A=B))"; -by (simp_tac (set_ss addsimps [ssubset_iff]) 1); +by (simp_tac (simpset_of "Fun" addsimps [ssubset_iff]) 1); by (fast_tac set_cs 1); qed "subseteq_iff_subset_eq"; (*Rule in Modus Ponens style*) goal Setplus.thy "A < B --> c:A --> c:B"; -by (simp_tac (set_ss addsimps [ssubset_iff]) 1); +by (simp_tac (simpset_of "Fun" addsimps [ssubset_iff]) 1); by (fast_tac set_cs 1); qed "ssubsetD"; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/Subst/Subst.ML --- a/src/HOL/Subst/Subst.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/Subst/Subst.ML Wed Oct 04 13:12:14 1995 +0100 @@ -1,4 +1,5 @@ -(* Title: Substitutions/subst.ML +(* Title: HOL/Subst/subst.ML + ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge @@ -11,7 +12,7 @@ val subst_defs = [subst_def,comp_def,sdom_def]; -val raw_subst_ss = utlemmas_ss addsimps al_rews; +val raw_subst_ss = simpset_of "UTLemmas" addsimps al_rews; local fun mk_thm s = prove_goalw Subst.thy subst_defs s (fn _ => [simp_tac raw_subst_ss 1]) diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/Subst/Subst.thy --- a/src/HOL/Subst/Subst.thy Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/Subst/Subst.thy Wed Oct 04 13:12:14 1995 +0100 @@ -26,7 +26,7 @@ (%x.Const(x)) (%u v q r.Comb q r)" - comp_def "al <> bl == alist_rec al bl (%x y xs g.(x,y <| bl)#g)" + comp_def "al <> bl == alist_rec al bl (%x y xs g.(x,y <| bl)#g)" sdom_def "sdom(al) == alist_rec al {} diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/Subst/UTLemmas.ML --- a/src/HOL/Subst/UTLemmas.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/Subst/UTLemmas.ML Wed Oct 04 13:12:14 1995 +0100 @@ -1,4 +1,5 @@ -(* Title: Substitutions/UTLemmas.ML +(* Title: HOL/Subst/UTLemmas.ML + ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge @@ -9,10 +10,10 @@ (***********) -val utlemmas_defs = [vars_of_def,occs_def]; +val utlemmas_defs = [vars_of_def, occs_def]; local fun mk_thm s = prove_goalw UTLemmas.thy utlemmas_defs s - (fn _ => [simp_tac uterm_ss 1]) + (fn _ => [Simp_tac 1]) in val utlemmas_rews = map mk_thm ["vars_of(Const(c)) = {}", "vars_of(Var(x)) = {x}", @@ -22,13 +23,13 @@ "t <: Comb u v = (t=u | t=v | t <: u | t <: v)"]; end; -val utlemmas_ss = prod_ss addsimps (setplus_rews @ uterm_rews @ utlemmas_rews); +Addsimps (setplus_rews @ uterm_rews @ utlemmas_rews); (**** occs irrefl ****) goal UTLemmas.thy "t <: u & u <: v --> t <: v"; by (uterm_ind_tac "v" 1); -by (ALLGOALS (simp_tac utlemmas_ss)); +by (ALLGOALS Simp_tac); by (fast_tac HOL_cs 1); val occs_trans = store_thm("occs_trans", conjI RS (result() RS mp)); @@ -37,11 +38,11 @@ val contr_occs_trans = store_thm("contr_occs_trans", result() RS mp); goal UTLemmas.thy "t <: Comb t u"; -by (simp_tac utlemmas_ss 1); +by (Simp_tac 1); qed "occs_Comb1"; goal UTLemmas.thy "u <: Comb t u"; -by (simp_tac utlemmas_ss 1); +by (Simp_tac 1); qed "occs_Comb2"; goal HOL.thy "(~(P|Q)) = (~P & ~Q)"; @@ -50,7 +51,7 @@ goal UTLemmas.thy "~ t <: t"; by (uterm_ind_tac "t" 1); -by (ALLGOALS (simp_tac (utlemmas_ss addsimps [demorgan_disj]))); +by (ALLGOALS (simp_tac (!simpset addsimps [demorgan_disj]))); by (REPEAT (resolve_tac [impI,conjI] 1 ORELSE (etac contrapos 1 THEN etac subst 1 THEN resolve_tac [occs_Comb1,occs_Comb2] 1) ORELSE @@ -66,12 +67,12 @@ (**** vars_of lemmas ****) goal UTLemmas.thy "(v : vars_of(Var(w))) = (w=v)"; -by (simp_tac utlemmas_ss 1); +by (Simp_tac 1); by (fast_tac HOL_cs 1); qed "vars_var_iff"; goal UTLemmas.thy "(x : vars_of(t)) = (Var(x) <: t | Var(x) = t)"; by (uterm_ind_tac "t" 1); -by (ALLGOALS (simp_tac utlemmas_ss)); +by (ALLGOALS Simp_tac); by (fast_tac HOL_cs 1); qed "vars_iff_occseq"; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/Subst/UTerm.ML --- a/src/HOL/Subst/UTerm.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/Subst/UTerm.ML Wed Oct 04 13:12:14 1995 +0100 @@ -1,4 +1,5 @@ -(* Title: Substitutions/uterm.ML +(* Title: HOL/Subst/UTerm.ML + ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge @@ -180,27 +181,26 @@ qed "COMB_D"; (*Basic ss with constructors and their freeness*) -val uterm_free_simps = uterm.intrs @ - [Const_not_Comb,Comb_not_Var,Var_not_Const, - Comb_not_Const,Var_not_Comb,Const_not_Var, - Var_Var_eq,Const_Const_eq,Comb_Comb_eq, - CONST_not_COMB,COMB_not_VAR,VAR_not_CONST, - COMB_not_CONST,VAR_not_COMB,CONST_not_VAR, - VAR_VAR_eq,CONST_CONST_eq,COMB_COMB_eq]; -val uterm_free_ss = HOL_ss addsimps uterm_free_simps; +Addsimps (uterm.intrs @ + [Const_not_Comb,Comb_not_Var,Var_not_Const, + Comb_not_Const,Var_not_Comb,Const_not_Var, + Var_Var_eq,Const_Const_eq,Comb_Comb_eq, + CONST_not_COMB,COMB_not_VAR,VAR_not_CONST, + COMB_not_CONST,VAR_not_COMB,CONST_not_VAR, + VAR_VAR_eq,CONST_CONST_eq,COMB_COMB_eq]); goal UTerm.thy "!u. t~=Comb t u"; by (uterm_ind_tac "t" 1); by (rtac (Var_not_Comb RS allI) 1); by (rtac (Const_not_Comb RS allI) 1); -by (asm_simp_tac uterm_free_ss 1); +by (Asm_simp_tac 1); qed "t_not_Comb_t"; goal UTerm.thy "!t. u~=Comb t u"; by (uterm_ind_tac "u" 1); by (rtac (Var_not_Comb RS allI) 1); by (rtac (Const_not_Comb RS allI) 1); -by (asm_simp_tac uterm_free_ss 1); +by (Asm_simp_tac 1); qed "u_not_Comb_u"; @@ -213,12 +213,12 @@ goalw UTerm.thy [VAR_def] "UTerm_rec (VAR x) b c d = b(x)"; by (rtac (UTerm_rec_unfold RS trans) 1); -by (simp_tac (HOL_ss addsimps [Case_In0]) 1); +by (simp_tac (!simpset addsimps [Case_In0]) 1); qed "UTerm_rec_VAR"; goalw UTerm.thy [CONST_def] "UTerm_rec (CONST x) b c d = c(x)"; by (rtac (UTerm_rec_unfold RS trans) 1); -by (simp_tac (HOL_ss addsimps [Case_In0,Case_In1]) 1); +by (simp_tac (!simpset addsimps [Case_In0,Case_In1]) 1); qed "UTerm_rec_CONST"; goalw UTerm.thy [COMB_def] @@ -226,8 +226,8 @@ \ UTerm_rec (COMB M N) b c d = \ \ d M N (UTerm_rec M b c d) (UTerm_rec N b c d)"; by (rtac (UTerm_rec_unfold RS trans) 1); -by (simp_tac (HOL_ss addsimps [Split,Case_In1]) 1); -by (asm_simp_tac (pred_sexp_ss addsimps [In1_def]) 1); +by (simp_tac (!simpset addsimps [Split,Case_In1]) 1); +by (asm_simp_tac (!simpset addsimps [In1_def]) 1); qed "UTerm_rec_COMB"; (*** uterm_rec -- by UTerm_rec ***) @@ -235,36 +235,26 @@ val Rep_uterm_in_sexp = Rep_uterm RS (range_Leaf_subset_sexp RS uterm_subset_sexp RS subsetD); -val uterm_rec_simps = - uterm.intrs @ - [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB, - Abs_uterm_inverse, Rep_uterm_inverse, - Rep_uterm, rangeI, inj_Leaf, Inv_f_f, Rep_uterm_in_sexp]; -val uterm_rec_ss = HOL_ss addsimps uterm_rec_simps; +Addsimps [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB, + Abs_uterm_inverse, Rep_uterm_inverse, + Rep_uterm, rangeI, inj_Leaf, Inv_f_f, Rep_uterm_in_sexp]; goalw UTerm.thy [uterm_rec_def, Var_def] "uterm_rec (Var x) b c d = b(x)"; -by (simp_tac uterm_rec_ss 1); +by (Simp_tac 1); qed "uterm_rec_Var"; goalw UTerm.thy [uterm_rec_def, Const_def] "uterm_rec (Const x) b c d = c(x)"; -by (simp_tac uterm_rec_ss 1); +by (Simp_tac 1); qed "uterm_rec_Const"; goalw UTerm.thy [uterm_rec_def, Comb_def] - "uterm_rec (Comb u v) b c d = d u v (uterm_rec u b c d) (uterm_rec v b c d)"; -by (simp_tac uterm_rec_ss 1); + "uterm_rec (Comb u v) b c d = d u v (uterm_rec u b c d) (uterm_rec v b c d)"; +by (Simp_tac 1); qed "uterm_rec_Comb"; -val uterm_simps = [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB, - uterm_rec_Var, uterm_rec_Const, uterm_rec_Comb]; -val uterm_ss = uterm_free_ss addsimps uterm_simps; +Addsimps [uterm_rec_Var, uterm_rec_Const, uterm_rec_Comb]; (**********) -val uterm_rews = [uterm_rec_Var,uterm_rec_Const,uterm_rec_Comb, - t_not_Comb_t,u_not_Comb_u, - Const_not_Comb,Comb_not_Var,Var_not_Const, - Comb_not_Const,Var_not_Comb,Const_not_Var, - Var_Var_eq,Const_Const_eq,Comb_Comb_eq]; - +val uterm_rews = [t_not_Comb_t,u_not_Comb_u]; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/Subst/Unifier.ML --- a/src/HOL/Subst/Unifier.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/Subst/Unifier.ML Wed Oct 04 13:12:14 1995 +0100 @@ -1,4 +1,5 @@ -(* Title: Substitutions/unifier.ML +(* Title: HOL/Subst/unifier.ML + ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge @@ -136,7 +137,7 @@ (*** The range of a MGIU is a subset of the variables in the terms ***) val prems = goal HOL.thy "P = Q ==> (~P) = (~Q)"; -by (simp_tac (set_ss addsimps prems) 1); +by (simp_tac (subst_ss addsimps prems) 1); qed "not_cong"; val prems = goal Unifier.thy @@ -289,11 +290,12 @@ by (cut_facts_tac [prem RS UWFD2_lemma1 RS (subseteq_iff_subset_eq RS iffD1)] 1); by (imp_excluded_middle_tac "u <| s = u" 1); -by (simp_tac (set_ss addsimps [occs_Comb2] ) 1); +by (simp_tac (subst_ss delsimps (ssubset_iff :: utlemmas_rews) + addsimps [occs_Comb2]) 1); by (rtac impI 1 THEN etac subst 1 THEN assume_tac 1); by (rtac impI 1); by (rtac (conjI RS (ssubset_iff RS iffD2) RS disjI1) 1); -by (asm_simp_tac (set_ss addsimps [subseteq_iff_subset_eq]) 1); +by (asm_simp_tac (subst_ss delsimps (ssubset_iff :: utlemmas_rews) addsimps [subseteq_iff_subset_eq]) 1); by (asm_simp_tac subst_ss 1); by (fast_tac (set_cs addDs [prem RS UWFD2_lemma2]) 1); qed "UnifyWFD2"; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/ex/Acc.thy --- a/src/HOL/ex/Acc.thy Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/ex/Acc.thy Wed Oct 04 13:12:14 1995 +0100 @@ -16,7 +16,7 @@ acc :: "('a * 'a)set => 'a set" (*Accessible part*) defs - pred_def "pred x r == {y. (y,x):r}" + pred_def "pred x r == {y. (y,x):r}" inductive "acc(r)" intrs diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/ex/BT.ML --- a/src/HOL/ex/BT.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/ex/BT.ML Wed Oct 04 13:12:14 1995 +0100 @@ -10,60 +10,50 @@ (** BT simplification **) -val bt_ss = list_ss - addsimps [n_nodes_Lf, n_nodes_Br, - n_leaves_Lf, n_leaves_Br, - reflect_Lf, reflect_Br, - bt_map_Lf, bt_map_Br, - preorder_Lf, preorder_Br, - inorder_Lf, inorder_Br, - postorder_Lf, postorder_Br]; - - goal BT.thy "n_leaves(reflect(t)) = n_leaves(t)"; by (bt.induct_tac "t" 1); -by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_commute]))); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_commute]))); qed "n_leaves_reflect"; goal BT.thy "n_nodes(reflect(t)) = n_nodes(t)"; by (bt.induct_tac "t" 1); -by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_commute]))); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_commute]))); qed "n_nodes_reflect"; (*The famous relationship between the numbers of leaves and nodes*) goal BT.thy "n_leaves(t) = Suc(n_nodes(t))"; by (bt.induct_tac "t" 1); -by (ALLGOALS (asm_simp_tac bt_ss)); +by (ALLGOALS Asm_simp_tac); qed "n_leaves_nodes"; goal BT.thy "reflect(reflect(t))=t"; by (bt.induct_tac "t" 1); -by (ALLGOALS (asm_simp_tac bt_ss)); +by (ALLGOALS Asm_simp_tac); qed "reflect_reflect_ident"; goal BT.thy "bt_map f (reflect t) = reflect (bt_map f t)"; by (bt.induct_tac "t" 1); -by (ALLGOALS (asm_simp_tac bt_ss)); +by (ALLGOALS Asm_simp_tac); qed "bt_map_reflect"; goal BT.thy "inorder (bt_map f t) = map f (inorder t)"; by (bt.induct_tac "t" 1); -by (ALLGOALS (asm_simp_tac bt_ss)); +by (ALLGOALS Asm_simp_tac); qed "inorder_bt_map"; goal BT.thy "preorder (reflect t) = rev (postorder t)"; by (bt.induct_tac "t" 1); -by (ALLGOALS (asm_simp_tac (bt_ss addsimps [rev_append]))); +by (ALLGOALS Asm_simp_tac); qed "preorder_reflect"; goal BT.thy "inorder (reflect t) = rev (inorder t)"; by (bt.induct_tac "t" 1); -by (ALLGOALS (asm_simp_tac (bt_ss addsimps [rev_append]))); +by (ALLGOALS Asm_simp_tac); qed "inorder_reflect"; goal BT.thy "postorder (reflect t) = rev (preorder t)"; by (bt.induct_tac "t" 1); -by (ALLGOALS (asm_simp_tac (bt_ss addsimps [rev_append]))); +by (ALLGOALS Asm_simp_tac); qed "postorder_reflect"; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/ex/InSort.ML --- a/src/HOL/ex/InSort.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/ex/InSort.ML Wed Oct 04 13:12:14 1995 +0100 @@ -6,9 +6,6 @@ Correctness proof of insertion sort. *) -val insort_ss = sorting_ss addsimps - [InSort.ins_Nil,InSort.ins_Cons,InSort.insort_Nil,InSort.insort_Cons]; - goalw InSort.thy [Sorting.total_def] "!!f. [| total(f); ~f x y |] ==> f y x"; by(fast_tac HOL_cs 1); @@ -21,26 +18,26 @@ goal InSort.thy "list_all p (ins f x xs) = (list_all p xs & p(x))"; by(list.induct_tac "xs" 1); -by(asm_simp_tac insort_ss 1); -by(asm_simp_tac (insort_ss setloop (split_tac [expand_if])) 1); +by(Asm_simp_tac 1); +by(asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1); by(fast_tac HOL_cs 1); -val insort_ss = insort_ss addsimps [result()]; +Addsimps [result()]; goal InSort.thy "(!x. p(x) --> q(x)) --> list_all p xs --> list_all q xs"; by(list.induct_tac "xs" 1); -by(ALLGOALS(asm_simp_tac (insort_ss setloop (split_tac [expand_if])))); +by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); qed "list_all_imp"; val prems = goal InSort.thy "[| total(f); transf(f) |] ==> sorted f (ins f x xs) = sorted f xs"; by(list.induct_tac "xs" 1); -by(ALLGOALS(asm_simp_tac (insort_ss setloop (split_tac [expand_if])))); +by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); by(cut_facts_tac prems 1); by(cut_inst_tac [("p","f(a)"),("q","f(x)")] list_all_imp 1); by(fast_tac (HOL_cs addDs [totalD,transfD]) 1); -val insort_ss = insort_ss addsimps [result()]; +Addsimps [result()]; goal InSort.thy "!!f. [| total(f); transf(f) |] ==> sorted f (insort f xs)"; by(list.induct_tac "xs" 1); -by(ALLGOALS(asm_simp_tac insort_ss)); +by(ALLGOALS Asm_simp_tac); result(); diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/ex/LList.ML --- a/src/HOL/ex/LList.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/ex/LList.ML Wed Oct 04 13:12:14 1995 +0100 @@ -10,8 +10,7 @@ (** Simplification **) -val llist_ss = univ_ss addcongs [split_weak_cong, sum_case_weak_cong] - setloop split_tac [expand_split, expand_sum_case]; +simpset := !simpset setloop split_tac [expand_split, expand_sum_case]; (*For adding _eqI rules to a simpset; we must remove Pair_eq because it may turn an instance of reflexivity into a conjunction!*) @@ -64,16 +63,16 @@ (*A continuity result?*) goalw LList.thy [CONS_def] "CONS M (UN x.f(x)) = (UN x. CONS M (f x))"; -by (simp_tac (univ_ss addsimps [In1_UN1, Scons_UN1_y]) 1); +by (simp_tac (!simpset addsimps [In1_UN1, Scons_UN1_y]) 1); qed "CONS_UN1"; (*UNUSED; obsolete? goal Prod.thy "split p (%x y.UN z.f x y z) = (UN z. split p (%x y.f x y z))"; -by (simp_tac (prod_ss setloop (split_tac [expand_split])) 1); +by (simp_tac (!simpset setloop (split_tac [expand_split])) 1); qed "split_UN1"; goal Sum.thy "sum_case s f (%y.UN z.g y z) = (UN z.sum_case s f (%y.g y z))"; -by (simp_tac (sum_ss setloop (split_tac [expand_sum_case])) 1); +by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1); qed "sum_case2_UN1"; *) @@ -82,9 +81,8 @@ by (REPEAT (resolve_tac ([In1_mono,Scons_mono]@prems) 1)); qed "CONS_mono"; -val corec_fun_simps = [LList_corec_fun_def RS def_nat_rec_0, - LList_corec_fun_def RS def_nat_rec_Suc]; -val corec_fun_ss = llist_ss addsimps corec_fun_simps; +Addsimps [LList_corec_fun_def RS def_nat_rec_0, + LList_corec_fun_def RS def_nat_rec_Suc]; (** The directions of the equality are proved separately **) @@ -93,17 +91,16 @@ \ (split(%z w. CONS z (LList_corec w f))) (f a)"; by (rtac UN1_least 1); by (res_inst_tac [("n","k")] natE 1); -by (ALLGOALS (asm_simp_tac corec_fun_ss)); +by (ALLGOALS (Asm_simp_tac)); by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono, UN1_upper] 1)); qed "LList_corec_subset1"; goalw LList.thy [LList_corec_def] "sum_case (%u.NIL) (split(%z w. CONS z (LList_corec w f))) (f a) <= \ \ LList_corec a f"; -by (simp_tac (corec_fun_ss addsimps [CONS_UN1]) 1); +by (simp_tac (!simpset addsimps [CONS_UN1]) 1); by (safe_tac set_cs); -by (ALLGOALS (res_inst_tac [("x","Suc(?k)")] UN1_I THEN' - asm_simp_tac corec_fun_ss)); +by (ALLGOALS (res_inst_tac [("x","Suc(?k)")] UN1_I THEN' Asm_simp_tac)); qed "LList_corec_subset2"; (*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*) @@ -129,7 +126,7 @@ by (rtac rangeI 1); by (safe_tac set_cs); by (stac LList_corec 1); -by (simp_tac (llist_ss addsimps [list_Fun_NIL_I, list_Fun_CONS_I, CollectI] +by (simp_tac (!simpset addsimps [list_Fun_NIL_I, list_Fun_CONS_I, CollectI] |> add_eqI) 1); qed "LList_corec_type"; @@ -141,7 +138,7 @@ by (rtac rangeI 1); by (safe_tac set_cs); by (stac LList_corec 1); -by (asm_simp_tac (llist_ss addsimps [list_Fun_NIL_I]) 1); +by (asm_simp_tac (!simpset addsimps [list_Fun_NIL_I]) 1); by (fast_tac (set_cs addSIs [list_Fun_CONS_I]) 1); qed "LList_corec_type2"; @@ -162,11 +159,11 @@ by (etac LListD.elim 1); by (safe_tac (prod_cs addSEs [diagE])); by (res_inst_tac [("n", "n")] natE 1); -by (asm_simp_tac (univ_ss addsimps [ntrunc_0]) 1); +by (asm_simp_tac (!simpset addsimps [ntrunc_0]) 1); by (rename_tac "n'" 1); by (res_inst_tac [("n", "n'")] natE 1); -by (asm_simp_tac (univ_ss addsimps [CONS_def, ntrunc_one_In1]) 1); -by (asm_simp_tac (univ_ss addsimps [CONS_def, ntrunc_In1, ntrunc_Scons]) 1); +by (asm_simp_tac (!simpset addsimps [CONS_def, ntrunc_one_In1]) 1); +by (asm_simp_tac (!simpset addsimps [CONS_def, ntrunc_In1, ntrunc_Scons]) 1); qed "LListD_implies_ntrunc_equality"; (*The domain of the LListD relation*) @@ -175,7 +172,7 @@ by (rtac gfp_upperbound 1); (*avoids unfolding LListD on the rhs*) by (res_inst_tac [("P", "%x. fst``x <= ?B")] (LListD_unfold RS ssubst) 1); -by (simp_tac fst_image_ss 1); +by (Simp_tac 1); by (fast_tac univ_cs 1); qed "fst_image_LListD"; @@ -227,7 +224,7 @@ by (etac ssubst 1); by (eresolve_tac [llist.elim] 1); by (ALLGOALS - (asm_simp_tac (llist_ss addsimps [diagI, LListD_Fun_NIL_I, + (asm_simp_tac (!simpset addsimps [diagI, LListD_Fun_NIL_I, LListD_Fun_CONS_I]))); qed "diag_subset_LListD"; @@ -240,7 +237,7 @@ "!!M N. M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))"; by (rtac (LListD_eq_diag RS subst) 1); by (rtac LListD_Fun_LListD_I 1); -by (asm_simp_tac (HOL_ss addsimps [LListD_eq_diag, diagI]) 1); +by (asm_simp_tac (!simpset addsimps [LListD_eq_diag, diagI]) 1); qed "LListD_Fun_diag_I"; @@ -252,7 +249,7 @@ \ |] ==> M=N"; by (rtac (LListD_subset_diag RS subsetD RS diagE) 1); by (etac LListD_coinduct 1); -by (asm_simp_tac (HOL_ss addsimps [LListD_eq_diag]) 1); +by (asm_simp_tac (!simpset addsimps [LListD_eq_diag]) 1); by (safe_tac prod_cs); qed "LList_equalityI"; @@ -272,7 +269,7 @@ by (safe_tac set_cs); by (stac prem1 1); by (stac prem2 1); -by (simp_tac (llist_ss addsimps [LListD_Fun_NIL_I, +by (simp_tac (!simpset addsimps [LListD_Fun_NIL_I, CollectI RS LListD_Fun_CONS_I] |> add_eqI) 1); qed "LList_corec_unique"; @@ -292,7 +289,7 @@ goalw LList.thy [CONS_def] "ntrunc (Suc(Suc(k))) (CONS M N) = CONS (ntrunc k M) (ntrunc k N)"; -by (simp_tac (HOL_ss addsimps [ntrunc_Scons,ntrunc_In1]) 1); +by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_In1]) 1); qed "ntrunc_CONS"; val [prem1,prem2] = goal LList.thy @@ -305,11 +302,11 @@ by (rtac allI 1); by (stac prem1 1); by (stac prem2 1); -by (simp_tac (sum_ss setloop (split_tac [expand_split,expand_sum_case])) 1); +by (simp_tac (!simpset setloop (split_tac [expand_split,expand_sum_case])) 1); by (strip_tac 1); by (res_inst_tac [("n", "n")] natE 1); by (res_inst_tac [("n", "xc")] natE 2); -by (ALLGOALS(asm_simp_tac(nat_ss addsimps +by (ALLGOALS(asm_simp_tac(!simpset addsimps [ntrunc_0,ntrunc_one_CONS,ntrunc_CONS]))); result(); @@ -334,14 +331,14 @@ goal LList.thy "Lconst(M) = LList_corec M (%x.Inr((x,x)))"; by (rtac (equals_LList_corec RS fun_cong) 1); -by (simp_tac sum_ss 1); +by (Simp_tac 1); by (rtac Lconst 1); qed "Lconst_eq_LList_corec"; (*Thus we could have used gfp in the definition of Lconst*) goal LList.thy "gfp(%N. CONS M N) = LList_corec M (%x.Inr((x,x)))"; by (rtac (equals_LList_corec RS fun_cong) 1); -by (simp_tac sum_ss 1); +by (Simp_tac 1); by (rtac (Lconst_fun_mono RS gfp_Tarski) 1); qed "gfp_Lconst_eq_LList_corec"; @@ -387,7 +384,7 @@ goalw LList.thy [CONS_def] "(CONS M N=CONS M' N') = (M=M' & N=N')"; by (fast_tac (HOL_cs addSEs [Scons_inject, make_elim In1_inject]) 1); -qed "CONS_CONS_eq"; +qed "CONS_CONS_eq2"; bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE)); @@ -407,13 +404,12 @@ by (rtac (major RS llist.elim) 1); by (etac CONS_neq_NIL 1); by (fast_tac llist_cs 1); -qed "CONS_D"; +qed "CONS_D2"; (****** Reasoning about llist(A) ******) -(*Don't use llist_ss, as it does case splits!*) -val List_case_ss = univ_ss addsimps [List_case_NIL, List_case_CONS]; +Addsimps [List_case_NIL, List_case_CONS]; (*A special case of list_equality for functions over lazy lists*) val [Mlist,gMlist,NILcase,CONScase] = goal LList.thy @@ -442,12 +438,12 @@ goal LList.thy "Lmap f NIL = NIL"; by (rtac (Lmap_def RS def_LList_corec RS trans) 1); -by (simp_tac List_case_ss 1); +by (Simp_tac 1); qed "Lmap_NIL"; goal LList.thy "Lmap f (CONS M N) = CONS (f M) (Lmap f N)"; by (rtac (Lmap_def RS def_LList_corec RS trans) 1); -by (simp_tac List_case_ss 1); +by (Simp_tac 1); qed "Lmap_CONS"; (*Another type-checking proof by coinduction*) @@ -456,7 +452,7 @@ by (rtac (major RS imageI RS llist_coinduct) 1); by (safe_tac set_cs); by (etac llist.elim 1); -by (ALLGOALS (asm_simp_tac (HOL_ss addsimps [Lmap_NIL,Lmap_CONS]))); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS]))); by (REPEAT (ares_tac [list_Fun_NIL_I, list_Fun_CONS_I, minor, imageI, UnI1] 1)); qed "Lmap_type"; @@ -474,7 +470,7 @@ by (rtac (prem RS imageI RS LList_equalityI) 1); by (safe_tac set_cs); by (etac llist.elim 1); -by (ALLGOALS (asm_simp_tac (HOL_ss addsimps [Lmap_NIL,Lmap_CONS]))); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS]))); by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI, UnI1, rangeI RS LListD_Fun_CONS_I] 1)); qed "Lmap_compose"; @@ -483,7 +479,7 @@ by (rtac (prem RS imageI RS LList_equalityI) 1); by (safe_tac set_cs); by (etac llist.elim 1); -by (ALLGOALS (asm_simp_tac (HOL_ss addsimps [Lmap_NIL,Lmap_CONS]))); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS]))); by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI RS UnI1, rangeI RS LListD_Fun_CONS_I] 1)); qed "Lmap_ident"; @@ -493,34 +489,33 @@ goalw LList.thy [Lappend_def] "Lappend NIL NIL = NIL"; by (rtac (LList_corec RS trans) 1); -by (simp_tac List_case_ss 1); +by (Simp_tac 1); qed "Lappend_NIL_NIL"; goalw LList.thy [Lappend_def] "Lappend NIL (CONS N N') = CONS N (Lappend NIL N')"; by (rtac (LList_corec RS trans) 1); -by (simp_tac List_case_ss 1); +by (Simp_tac 1); qed "Lappend_NIL_CONS"; goalw LList.thy [Lappend_def] "Lappend (CONS M M') N = CONS M (Lappend M' N)"; by (rtac (LList_corec RS trans) 1); -by (simp_tac List_case_ss 1); +by (Simp_tac 1); qed "Lappend_CONS"; -val Lappend_ss = - List_case_ss addsimps [llist.NIL_I, Lappend_NIL_NIL, Lappend_NIL_CONS, - Lappend_CONS, LListD_Fun_CONS_I] - |> add_eqI; +Addsimps [llist.NIL_I, Lappend_NIL_NIL, Lappend_NIL_CONS, + Lappend_CONS, LListD_Fun_CONS_I, range_eqI, image_eqI]; +Delsimps [Pair_eq]; goal LList.thy "!!M. M: llist(A) ==> Lappend NIL M = M"; by (etac LList_fun_equalityI 1); -by (ALLGOALS (asm_simp_tac Lappend_ss)); +by (ALLGOALS Asm_simp_tac); qed "Lappend_NIL"; goal LList.thy "!!M. M: llist(A) ==> Lappend M NIL = M"; by (etac LList_fun_equalityI 1); -by (ALLGOALS (asm_simp_tac Lappend_ss)); +by (ALLGOALS Asm_simp_tac); qed "Lappend_NIL2"; (** Alternative type-checking proofs for Lappend **) @@ -535,7 +530,7 @@ by (eres_inst_tac [("a", "u")] llist.elim 1); by (eres_inst_tac [("a", "v")] llist.elim 1); by (ALLGOALS - (asm_simp_tac Lappend_ss THEN' + (Asm_simp_tac THEN' fast_tac (set_cs addSIs [llist.NIL_I, list_Fun_NIL_I, list_Fun_CONS_I]))); qed "Lappend_type"; @@ -547,8 +542,8 @@ by (rtac subsetI 1); by (etac imageE 1); by (eres_inst_tac [("a", "u")] llist.elim 1); -by (asm_simp_tac (Lappend_ss addsimps [Lappend_NIL, list_Fun_llist_I]) 1); -by (asm_simp_tac Lappend_ss 1); +by (asm_simp_tac (!simpset addsimps [Lappend_NIL, list_Fun_llist_I]) 1); +by (Asm_simp_tac 1); by (fast_tac (set_cs addSIs [list_Fun_CONS_I]) 1); qed "Lappend_type"; @@ -556,20 +551,16 @@ (** llist_case: case analysis for 'a llist **) -val Rep_llist_simps = - [List_case_NIL, List_case_CONS, - Abs_llist_inverse, Rep_llist_inverse, - Rep_llist, rangeI, inj_Leaf, Inv_f_f] - @ llist.intrs; -val Rep_llist_ss = llist_ss addsimps Rep_llist_simps; +Addsimps ([Abs_llist_inverse, Rep_llist_inverse, + Rep_llist, rangeI, inj_Leaf, Inv_f_f] @ llist.intrs); goalw LList.thy [llist_case_def,LNil_def] "llist_case c d LNil = c"; -by (simp_tac Rep_llist_ss 1); +by (Simp_tac 1); qed "llist_case_LNil"; goalw LList.thy [llist_case_def,LCons_def] "llist_case c d (LCons M N) = d M N"; -by (simp_tac Rep_llist_ss 1); +by (Simp_tac 1); qed "llist_case_LCons"; (*Elimination is case analysis, not induction.*) @@ -582,7 +573,7 @@ by (assume_tac 1); by (etac rangeE 1); by (rtac (inj_Rep_llist RS injD RS prem2) 1); -by (asm_simp_tac (HOL_ss addsimps [Rep_llist_LCons]) 1); +by (asm_simp_tac (!simpset delsimps [CONS_CONS_eq] addsimps [Rep_llist_LCons]) 1); by (etac (Abs_llist_inverse RS ssubst) 1); by (rtac refl 1); qed "llistE"; @@ -594,11 +585,11 @@ \ (split(%z w. LCons z (llist_corec w f))) (f a)"; by (stac LList_corec 1); by (res_inst_tac [("s","f(a)")] sumE 1); -by (asm_simp_tac (llist_ss addsimps [LList_corec_type2,Abs_llist_inverse]) 1); +by (asm_simp_tac (!simpset addsimps [LList_corec_type2]) 1); by (res_inst_tac [("p","y")] PairE 1); -by (asm_simp_tac (llist_ss addsimps [LList_corec_type2,Abs_llist_inverse]) 1); +by (asm_simp_tac (!simpset addsimps [LList_corec_type2]) 1); (*FIXME: correct case splits usd to be found automatically: -by (ASM_SIMP_TAC(llist_ss addsimps [LList_corec_type2,Abs_llist_inverse]) 1);*) +by (ASM_SIMP_TAC(!simpset addsimps [LList_corec_type2]) 1);*) qed "llist_corec"; (*definitional version of same*) @@ -617,7 +608,7 @@ "!!r A. r <= Sigma (llist A) (%x.llist(A)) ==> \ \ LListD_Fun (diag A) r <= Sigma (llist A) (%x.llist(A))"; by (stac llist_unfold 1); -by (simp_tac (HOL_ss addsimps [NIL_def, CONS_def]) 1); +by (simp_tac (!simpset addsimps [NIL_def, CONS_def]) 1); by (fast_tac univ_cs 1); qed "LListD_Fun_subset_Sigma_llist"; @@ -633,7 +624,7 @@ by (safe_tac prod_cs); by (rtac (prem RS subsetD RS SigmaE2) 1); by (assume_tac 1); -by (asm_simp_tac (HOL_ss addsimps [o_def,prod_fun,Abs_llist_inverse]) 1); +by (asm_simp_tac (!simpset addsimps [o_def,prod_fun,Abs_llist_inverse]) 1); qed "prod_fun_lemma"; goal LList.thy @@ -704,22 +695,20 @@ qed "llist_fun_equalityI"; (*simpset for llist bisimulations*) -val llistD_simps = [llist_case_LNil, llist_case_LCons, - llistD_Fun_LNil_I, llistD_Fun_LCons_I]; -(*Don't use llist_ss, as it does case splits!*) -val llistD_ss = univ_ss addsimps llistD_simps |> add_eqI; +Addsimps [llist_case_LNil, llist_case_LCons, + llistD_Fun_LNil_I, llistD_Fun_LCons_I]; (*** The functional "lmap" ***) goal LList.thy "lmap f LNil = LNil"; by (rtac (lmap_def RS def_llist_corec RS trans) 1); -by (simp_tac llistD_ss 1); +by (Simp_tac 1); qed "lmap_LNil"; goal LList.thy "lmap f (LCons M N) = LCons (f M) (lmap f N)"; by (rtac (lmap_def RS def_llist_corec RS trans) 1); -by (simp_tac llistD_ss 1); +by (Simp_tac 1); qed "lmap_LCons"; @@ -727,12 +716,12 @@ goal LList.thy "lmap (f o g) l = lmap f (lmap g l)"; by (res_inst_tac [("l","l")] llist_fun_equalityI 1); -by (ALLGOALS (simp_tac (llistD_ss addsimps [lmap_LNil, lmap_LCons]))); +by (ALLGOALS (simp_tac (!simpset addsimps [lmap_LNil, lmap_LCons]))); qed "lmap_compose"; goal LList.thy "lmap (%x.x) l = l"; by (res_inst_tac [("l","l")] llist_fun_equalityI 1); -by (ALLGOALS (simp_tac (llistD_ss addsimps [lmap_LNil, lmap_LCons]))); +by (ALLGOALS (simp_tac (!simpset addsimps [lmap_LNil, lmap_LCons]))); qed "lmap_ident"; @@ -740,7 +729,7 @@ goal LList.thy "iterates f x = LCons x (iterates f (f x))"; by (rtac (iterates_def RS def_llist_corec RS trans) 1); -by (simp_tac sum_ss 1); +by (Simp_tac 1); qed "iterates"; goal LList.thy "lmap f (iterates f x) = iterates f (f x)"; @@ -750,7 +739,7 @@ by (safe_tac set_cs); by (res_inst_tac [("x1", "f(u)")] (iterates RS ssubst) 1); by (res_inst_tac [("x1", "u")] (iterates RS ssubst) 1); -by (simp_tac (llistD_ss addsimps [lmap_LCons]) 1); +by (simp_tac (!simpset addsimps [lmap_LCons]) 1); qed "lmap_iterates"; goal LList.thy "iterates f x = LCons x (lmap f (iterates f x))"; @@ -766,12 +755,12 @@ "nat_rec n (LCons b l) (%m. lmap(f)) = \ \ LCons (nat_rec n b (%m. f)) (nat_rec n l (%m. lmap(f)))"; by (nat_ind_tac "n" 1); -by (ALLGOALS (asm_simp_tac (nat_ss addsimps [lmap_LCons]))); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [lmap_LCons]))); qed "fun_power_lmap"; goal Nat.thy "nat_rec n (g x) (%m. g) = nat_rec (Suc n) x (%m. g)"; by (nat_ind_tac "n" 1); -by (ALLGOALS (asm_simp_tac nat_ss)); +by (ALLGOALS Asm_simp_tac); qed "fun_power_Suc"; val Pair_cong = read_instantiate_sg (sign_of Prod.thy) @@ -805,31 +794,31 @@ goalw LList.thy [lappend_def] "lappend LNil LNil = LNil"; by (rtac (llist_corec RS trans) 1); -by (simp_tac llistD_ss 1); +by (Simp_tac 1); qed "lappend_LNil_LNil"; goalw LList.thy [lappend_def] "lappend LNil (LCons l l') = LCons l (lappend LNil l')"; by (rtac (llist_corec RS trans) 1); -by (simp_tac llistD_ss 1); +by (Simp_tac 1); qed "lappend_LNil_LCons"; goalw LList.thy [lappend_def] "lappend (LCons l l') N = LCons l (lappend l' N)"; by (rtac (llist_corec RS trans) 1); -by (simp_tac llistD_ss 1); +by (Simp_tac 1); qed "lappend_LCons"; goal LList.thy "lappend LNil l = l"; by (res_inst_tac [("l","l")] llist_fun_equalityI 1); by (ALLGOALS - (simp_tac (llistD_ss addsimps [lappend_LNil_LNil, lappend_LNil_LCons]))); + (simp_tac (!simpset addsimps [lappend_LNil_LNil, lappend_LNil_LCons]))); qed "lappend_LNil"; goal LList.thy "lappend l LNil = l"; by (res_inst_tac [("l","l")] llist_fun_equalityI 1); by (ALLGOALS - (simp_tac (llistD_ss addsimps [lappend_LNil_LNil, lappend_LCons]))); + (simp_tac (!simpset addsimps [lappend_LNil_LNil, lappend_LCons]))); qed "lappend_LNil2"; (*The infinite first argument blocks the second*) @@ -839,7 +828,7 @@ by (rtac rangeI 1); by (safe_tac set_cs); by (stac iterates 1); -by (simp_tac (llistD_ss addsimps [lappend_LCons]) 1); +by (simp_tac (!simpset addsimps [lappend_LCons]) 1); qed "lappend_iterates"; (** Two proofs that lmap distributes over lappend **) @@ -855,7 +844,7 @@ by (safe_tac set_cs); by (res_inst_tac [("l", "l")] llistE 1); by (res_inst_tac [("l", "n")] llistE 1); -by (ALLGOALS (asm_simp_tac (llistD_ss addsimps +by (ALLGOALS (asm_simp_tac (!simpset addsimps [lappend_LNil_LNil,lappend_LCons,lappend_LNil_LCons, lmap_LNil,lmap_LCons]))); by (REPEAT_SOME (ares_tac [llistD_Fun_LCons_I, UN1_I RS UnI1, rangeI])); @@ -868,13 +857,13 @@ (*Shorter proof of theorem above using llist_equalityI as strong coinduction*) goal LList.thy "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"; by (res_inst_tac [("l","l")] llist_fun_equalityI 1); -by (simp_tac (llistD_ss addsimps [lappend_LNil, lmap_LNil])1); -by (simp_tac (llistD_ss addsimps [lappend_LCons, lmap_LCons]) 1); +by (simp_tac (!simpset addsimps [lappend_LNil, lmap_LNil])1); +by (simp_tac (!simpset addsimps [lappend_LCons, lmap_LCons]) 1); qed "lmap_lappend_distrib"; (*Without strong coinduction, three case analyses might be needed*) goal LList.thy "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)"; by (res_inst_tac [("l","l1")] llist_fun_equalityI 1); -by (simp_tac (llistD_ss addsimps [lappend_LNil])1); -by (simp_tac (llistD_ss addsimps [lappend_LCons]) 1); +by (simp_tac (!simpset addsimps [lappend_LNil])1); +by (simp_tac (!simpset addsimps [lappend_LCons]) 1); qed "lappend_assoc"; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/ex/MT.ML --- a/src/HOL/ex/MT.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/ex/MT.ML Wed Oct 04 13:12:14 1995 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/ex/mt.ML +(* Title: HOL/ex/MT.ML ID: $Id$ Author: Jacob Frost, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge @@ -39,21 +39,21 @@ ); val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))"; -by (simp_tac (prod_ss addsimps prems) 1); +by (simp_tac (!simpset addsimps prems) 1); qed "infsys_p1"; val prems = goal MT.thy "!!a b. P (fst (a,b)) (snd (a,b)) ==> P a b"; -by (asm_full_simp_tac prod_ss 1); +by (Asm_full_simp_tac 1); qed "infsys_p2"; val prems = goal MT.thy "!!a. P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))"; -by (asm_full_simp_tac prod_ss 1); +by (Asm_full_simp_tac 1); qed "infsys_pp1"; val prems = goal MT.thy "!!a. P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c"; -by (asm_full_simp_tac prod_ss 1); +by (Asm_full_simp_tac 1); qed "infsys_pp2"; (* ############################################################ *) @@ -175,7 +175,7 @@ by (rtac eval_fun_mono 1); by (rewtac eval_fun_def); by (fast_tac set_cs 1); -qed "eval_var"; +qed "eval_var2"; val prems = goalw MT.thy [eval_def, eval_rel_def] "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)"; @@ -499,8 +499,8 @@ by (elab_e_elim_tac prems); qed "elab_app_elim_lem"; -val prems = goal MT.thy - "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; +val prems = goal MT.thy + "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; by (cut_facts_tac prems 1); by (dtac elab_app_elim_lem 1); by (fast_tac prop_cs 1); @@ -523,7 +523,8 @@ (* First strong indtroduction (co-induction) rule for hasty_rel *) -val prems = goalw MT.thy [hasty_rel_def] "c isof t ==> (v_const(c),t) : hasty_rel"; +val prems = + goalw MT.thy [hasty_rel_def] "c isof t ==> (v_const(c),t) : hasty_rel"; by (cut_facts_tac prems 1); by (rtac gfp_coind2 1); by (rewtac MT.hasty_fun_def); @@ -629,7 +630,8 @@ qed "hasty_elim_clos_lem"; val prems = goal MT.thy - "v_clos(<|ev,e,ve|>) hasty t ==> ? te.te |- fn ev => e ===> t & ve hastyenv te "; + "v_clos(<|ev,e,ve|>) hasty t ==> ? te.te |- fn ev => e ===>\ + \t & ve hastyenv te "; by (cut_facts_tac (prems RL [hasty_elim_clos_lem]) 1); by (fast_tac HOL_cs 1); qed "hasty_elim_clos"; @@ -642,12 +644,13 @@ "!!ve. [| ve hastyenv te; v hasty t |] ==> \ \ ve + {ev |-> v} hastyenv te + {ev |=> t}"; by (rewtac hasty_env_def); -by (asm_full_simp_tac (HOL_ss addsimps [ve_dom_owr, te_dom_owr]) 1); +by (asm_full_simp_tac (!simpset delsimps mem_simps + addsimps [ve_dom_owr, te_dom_owr]) 1); by (safe_tac HOL_cs); by (excluded_middle_tac "ev=x" 1); -by (asm_full_simp_tac (HOL_ss addsimps [ve_app_owr2, te_app_owr2]) 1); +by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1); by (fast_tac set_cs 1); -by (asm_simp_tac (HOL_ss addsimps [ve_app_owr1, te_app_owr1]) 1); +by (asm_simp_tac (!simpset addsimps [ve_app_owr1, te_app_owr1]) 1); qed "hasty_env1"; (* ############################################################ *) @@ -690,15 +693,16 @@ by ((forward_tac [ssubst] 1) THEN (assume_tac 2)); by (rtac hasty_rel_clos_coind 1); by (etac elab_fn 1); -by (asm_simp_tac (HOL_ss addsimps [ve_dom_owr, te_dom_owr]) 1); +by (asm_simp_tac (!simpset addsimps [ve_dom_owr, te_dom_owr]) 1); -by (asm_simp_tac (HOL_ss addsimps [ve_dom_owr]) 1); +by (asm_simp_tac (!simpset delsimps mem_simps addsimps [ve_dom_owr]) 1); by (safe_tac HOL_cs); by (excluded_middle_tac "ev2=ev1a" 1); -by (asm_full_simp_tac (HOL_ss addsimps [ve_app_owr2, te_app_owr2]) 1); +by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1); by (fast_tac set_cs 1); -by (asm_simp_tac (HOL_ss addsimps [ve_app_owr1, te_app_owr1]) 1); +by (asm_simp_tac (!simpset delsimps mem_simps + addsimps [ve_app_owr1, te_app_owr1]) 1); by (hyp_subst_tac 1); by (etac subst 1); by (fast_tac set_cs 1); @@ -779,7 +783,7 @@ by (etac exE 1); by (etac conjE 1); by (dtac hasty_const 1); -by (asm_simp_tac HOL_ss 1); +by (Asm_simp_tac 1); qed "basic_consistency_lem"; val prems = goal MT.thy @@ -789,5 +793,3 @@ by (dtac consistency 1); by (fast_tac (HOL_cs addSIs [basic_consistency_lem]) 1); qed "basic_consistency"; - - diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/ex/NatSum.ML --- a/src/HOL/ex/NatSum.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/ex/NatSum.ML Wed Oct 04 13:12:14 1995 +0100 @@ -6,38 +6,37 @@ Summing natural numbers, squares and cubes. Could be continued... *) -val natsum_ss = arith_ss addsimps - ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac); +Addsimps ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac); (*The sum of the first n positive integers equals n(n+1)/2.*) goal NatSum.thy "Suc(Suc(0))*sum (%i.i) (Suc n) = n*Suc(n)"; -by (simp_tac natsum_ss 1); +by (Simp_tac 1); by (nat_ind_tac "n" 1); -by (simp_tac natsum_ss 1); -by (asm_simp_tac natsum_ss 1); +by (Simp_tac 1); +by (Asm_simp_tac 1); qed "sum_of_naturals"; goal NatSum.thy "Suc(Suc(Suc(Suc(Suc(Suc(0))))))*sum (%i.i*i) (Suc n) = \ \ n*Suc(n)*Suc(Suc(Suc(0))*n)"; -by (simp_tac natsum_ss 1); +by (Simp_tac 1); by (nat_ind_tac "n" 1); -by (simp_tac natsum_ss 1); -by (asm_simp_tac natsum_ss 1); +by (Simp_tac 1); +by (Asm_simp_tac 1); qed "sum_of_squares"; goal NatSum.thy "Suc(Suc(Suc(Suc(0))))*sum (%i.i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)"; -by (simp_tac natsum_ss 1); +by (Simp_tac 1); by (nat_ind_tac "n" 1); -by (simp_tac natsum_ss 1); -by (asm_simp_tac natsum_ss 1); +by (Simp_tac 1); +by (Asm_simp_tac 1); qed "sum_of_cubes"; (*The sum of the first n odd numbers equals n squared.*) goal NatSum.thy "sum (%i.Suc(i+i)) n = n*n"; by (nat_ind_tac "n" 1); -by (simp_tac natsum_ss 1); -by (asm_simp_tac natsum_ss 1); +by (Simp_tac 1); +by (Asm_simp_tac 1); qed "sum_of_odds"; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/ex/Perm.ML --- a/src/HOL/ex/Perm.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/ex/Perm.ML Wed Oct 04 13:12:14 1995 +0100 @@ -26,13 +26,13 @@ (*The form of the premise lets the induction bind xs and ys.*) goal Perm.thy "!!xs. xs <~~> ys ==> xs=[] --> ys=[]"; by (etac perm_induct 1); -by (ALLGOALS (asm_simp_tac (HOL_ss addsimps list.simps))); +by (ALLGOALS Asm_simp_tac); qed "perm_Nil_lemma"; (*A more general version is actually easier to understand!*) goal Perm.thy "!!xs. xs <~~> ys ==> length(xs) = length(ys)"; by (etac perm_induct 1); -by (ALLGOALS (asm_simp_tac list_ss)); +by (ALLGOALS Asm_simp_tac); qed "perm_length"; goal Perm.thy "!!xs. xs <~~> ys ==> ys <~~> xs"; @@ -43,7 +43,7 @@ goal Perm.thy "!!xs. [| xs <~~> ys |] ==> x mem xs --> x mem ys"; by (etac perm_induct 1); by (fast_tac HOL_cs 4); -by (ALLGOALS (asm_simp_tac (list_ss setloop split_tac [expand_if]))); +by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if]))); val perm_mem_lemma = result(); bind_thm ("perm_mem", perm_mem_lemma RS mp); @@ -53,8 +53,8 @@ (*We can insert the head anywhere in the list*) goal Perm.thy "a # xs @ ys <~~> xs @ a # ys"; by (list.induct_tac "xs" 1); -by (simp_tac (list_ss addsimps [perm_refl]) 1); -by (simp_tac list_ss 1); +by (simp_tac (!simpset addsimps [perm_refl]) 1); +by (Simp_tac 1); by (etac ([perm.swap, perm.Cons] MRS perm.trans) 1); qed "perm_append_Cons"; @@ -66,8 +66,8 @@ goal Perm.thy "xs@ys <~~> ys@xs"; by (list.induct_tac "xs" 1); -by (simp_tac (list_ss addsimps [perm_refl]) 1); -by (simp_tac list_ss 1); +by (simp_tac (!simpset addsimps [perm_refl]) 1); +by (Simp_tac 1); by (etac ([perm.Cons, perm_append_Cons] MRS perm.trans) 1); qed "perm_append_swap"; @@ -75,21 +75,21 @@ goal Perm.thy "a # xs <~~> xs @ [a]"; by (rtac perm.trans 1); br perm_append_swap 2; -by (simp_tac (list_ss addsimps [perm_refl]) 1); +by (simp_tac (!simpset addsimps [perm_refl]) 1); qed "perm_append_single"; goal Perm.thy "rev xs <~~> xs"; by (list.induct_tac "xs" 1); -by (simp_tac (list_ss addsimps [perm_refl]) 1); -by (simp_tac list_ss 1); +by (simp_tac (!simpset addsimps [perm_refl]) 1); +by (Simp_tac 1); by (rtac (perm_append_single RS perm_sym RS perm.trans) 1); by (etac perm.Cons 1); qed "perm_rev"; goal Perm.thy "!!xs. xs <~~> ys ==> l@xs <~~> l@ys"; by (list.induct_tac "l" 1); -by (simp_tac list_ss 1); -by (asm_simp_tac (list_ss addsimps [perm.Cons]) 1); +by (Simp_tac 1); +by (asm_simp_tac (!simpset addsimps [perm.Cons]) 1); qed "perm_append1"; goal Perm.thy "!!xs. xs <~~> ys ==> xs@l <~~> ys@l"; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/ex/PropLog.ML --- a/src/HOL/ex/PropLog.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/ex/PropLog.ML Wed Oct 04 13:12:14 1995 +0100 @@ -62,29 +62,25 @@ (** The function eval **) -val pl_ss = set_ss addsimps - (PropLog.pl.simps @ [eval2_false, eval2_var, eval2_imp] - @ [hyps_false, hyps_var, hyps_imp]); - goalw PropLog.thy [eval_def] "tt[false] = False"; -by (simp_tac pl_ss 1); +by (Simp_tac 1); qed "eval_false"; goalw PropLog.thy [eval_def] "tt[#v] = (v:tt)"; -by (simp_tac pl_ss 1); +by (Simp_tac 1); qed "eval_var"; goalw PropLog.thy [eval_def] "tt[p->q] = (tt[p]-->tt[q])"; -by (simp_tac pl_ss 1); +by (Simp_tac 1); qed "eval_imp"; -val pl_ss = pl_ss addsimps [eval_false, eval_var, eval_imp]; +Addsimps [eval_false, eval_var, eval_imp]; (*Soundness of the rules wrt truth-table semantics*) goalw PropLog.thy [sat_def] "!!H. H |- p ==> H |= p"; by (etac thms.induct 1); by (fast_tac (set_cs addSDs [eval_imp RS iffD1 RS mp]) 5); -by (ALLGOALS (asm_simp_tac pl_ss)); +by (ALLGOALS Asm_simp_tac); qed "soundness"; (*** Towards the completeness proof ***) @@ -109,7 +105,7 @@ goal PropLog.thy "hyps p tt |- (if tt[p] then p else p->false)"; by (rtac (expand_if RS iffD2) 1); by(PropLog.pl.induct_tac "p" 1); -by (ALLGOALS (simp_tac (pl_ss addsimps [thms_I, thms.H]))); +by (ALLGOALS (simp_tac (!simpset addsimps [thms_I, thms.H]))); by (fast_tac (set_cs addIs [weaken_left_Un1, weaken_left_Un2, weaken_right, imp_false] addSEs [false_imp]) 1); @@ -146,9 +142,9 @@ we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *) goal PropLog.thy "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})"; by (PropLog.pl.induct_tac "p" 1); -by (simp_tac pl_ss 1); -by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1); -by (simp_tac pl_ss 1); +by (Simp_tac 1); +by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); +by (Simp_tac 1); by (fast_tac set_cs 1); qed "hyps_Diff"; @@ -156,9 +152,9 @@ we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *) goal PropLog.thy "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})"; by (PropLog.pl.induct_tac "p" 1); -by (simp_tac pl_ss 1); -by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1); -by (simp_tac pl_ss 1); +by (Simp_tac 1); +by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); +by (Simp_tac 1); by (fast_tac set_cs 1); qed "hyps_insert"; @@ -176,8 +172,8 @@ could probably prove the stronger hyps(p,t) : Fin(hyps(p,{}) Un hyps(p,nat))*) goal PropLog.thy "hyps p t : Fin(UN v:{x.True}. {#v, #v->false})"; by (PropLog.pl.induct_tac "p" 1); -by (ALLGOALS (simp_tac (pl_ss setloop (split_tac [expand_if])) THEN' - fast_tac (set_cs addSIs Fin.intrs@[Fin_UnI]))); +by (ALLGOALS (simp_tac (!simpset setloop (split_tac [expand_if])))); +by (ALLGOALS (fast_tac (set_cs addSIs Fin.intrs@[Fin_UnI]))); qed "hyps_finite"; val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left; @@ -187,7 +183,7 @@ val [sat] = goal PropLog.thy "{} |= p ==> !t. hyps p t - hyps p t0 |- p"; by (rtac (hyps_finite RS Fin_induct) 1); -by (simp_tac (pl_ss addsimps [sat RS sat_thms_p]) 1); +by (simp_tac (!simpset addsimps [sat RS sat_thms_p]) 1); by (safe_tac set_cs); (*Case hyps(p,t)-insert(#v,Y) |- p *) by (rtac thms_excluded_middle_rule 1); @@ -213,7 +209,7 @@ (*A semantic analogue of the Deduction Theorem*) val [sat] = goalw PropLog.thy [sat_def] "insert p H |= q ==> H |= p->q"; -by (simp_tac pl_ss 1); +by (Simp_tac 1); by (cfast_tac [sat] 1); qed "sat_imp"; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/ex/Puzzle.ML --- a/src/HOL/ex/Puzzle.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/ex/Puzzle.ML Wed Oct 04 13:12:14 1995 +0100 @@ -16,14 +16,14 @@ goal Puzzle.thy "! n. k=f(n) --> n <= f(n)"; by (res_inst_tac [("n","k")] less_induct 1); by (rtac nat_exh 1); -by (simp_tac nat_ss 1); +by (Simp_tac 1); by (rtac impI 1); by (rtac classical 1); by (dtac not_leE 1); by (subgoal_tac "f(na) <= f(f(na))" 1); by (best_tac (HOL_cs addIs [lessD,Puzzle.f_ax,le_less_trans,le_trans]) 1); by (fast_tac (HOL_cs addIs [Puzzle.f_ax]) 1); -bind_thm("lemma", result() RS spec RS mp); +val lemma = result() RS spec RS mp; goal Puzzle.thy "n <= f(n)"; by (fast_tac (HOL_cs addIs [lemma]) 1); @@ -35,8 +35,8 @@ val prems = goal Puzzle.thy "(!!n.f(n) <= f(Suc(n))) ==> m f(m) <= f(n)"; by (res_inst_tac[("n","n")]nat_induct 1); -by (simp_tac nat_ss 1); -by (simp_tac nat_ss 1); +by (Simp_tac 1); +by (Simp_tac 1); by (fast_tac (HOL_cs addIs (le_trans::prems)) 1); bind_thm("mono_lemma1", result() RS mp); diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/ex/Qsort.ML --- a/src/HOL/ex/Qsort.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/ex/Qsort.ML Wed Oct 04 13:12:14 1995 +0100 @@ -6,45 +6,45 @@ Two verifications of Quicksort *) -val ss = sorting_ss addsimps ([Qsort.qsort_Nil,Qsort.qsort_Cons]@conj_comms); +Addsimps ([Qsort.qsort_Nil,Qsort.qsort_Cons]@conj_comms); goal Qsort.thy "!x. mset (qsort le xs) x = mset xs x"; by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); -by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); +by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); result(); goal Qsort.thy "(Alls x:[x:xs.P(x)].Q(x)) = (Alls x:xs. P(x)-->Q(x))"; by(list.induct_tac "xs" 1); -by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); -val ss = ss addsimps [result()]; +by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); +Addsimps [result()]; goal Qsort.thy "((Alls x:xs.P(x)) & (Alls x:xs.Q(x))) = (Alls x:xs. P(x)&Q(x))"; by(list.induct_tac "xs" 1); -by(ALLGOALS(asm_simp_tac ss)); -val ss = ss addsimps [result()]; +by(ALLGOALS Asm_simp_tac); +Addsimps [result()]; goal HOL.thy "((~P --> Q) & (P --> Q)) = Q"; by(fast_tac HOL_cs 1); -qed "lemma"; +val lemma = result(); goal Qsort.thy "(Alls x:qsort le xs.P(x)) = (Alls x:xs.P(x))"; by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); -by(ALLGOALS(asm_simp_tac (ss addsimps [lemma]))); -val ss = ss addsimps [result()]; +by(ALLGOALS(asm_simp_tac (!simpset addsimps [lemma]))); +Addsimps [result()]; goal Qsort.thy "sorted le (xs@ys) = (sorted le xs & sorted le ys & \ \ (Alls x:xs. Alls y:ys. le x y))"; by(list.induct_tac "xs" 1); -by(ALLGOALS(asm_simp_tac ss)); -val ss = ss addsimps [result()]; +by(ALLGOALS Asm_simp_tac); +Addsimps [result()]; goal Qsort.thy "!!le. [| total(le); transf(le) |] ==> sorted le (qsort le xs)"; by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); -by(ALLGOALS(asm_full_simp_tac (ss addsimps [list_all_mem_conv]) )); +by(ALLGOALS(asm_full_simp_tac (!simpset addsimps [list_all_mem_conv]) )); by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]); by(fast_tac HOL_cs 1); result(); @@ -55,30 +55,28 @@ val sorted_Cons = rewrite_rule [list_all_mem_conv RS eq_reflection] Sorting.sorted_Cons; -val ss = list_ss addsimps - [Sorting.sorted_Nil,sorted_Cons, - Qsort.qsort_Nil,Qsort.qsort_Cons]; +Addsimps [sorted_Cons]; goal Qsort.thy "x mem qsort le xs = x mem xs"; by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); -by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); +by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); by(fast_tac HOL_cs 1); -val ss = ss addsimps [result()]; +Addsimps [result()]; goal Qsort.thy "sorted le (xs@ys) = (sorted le xs & sorted le ys & \ \ (!x. x mem xs --> (!y. y mem ys --> le x y)))"; by(list.induct_tac "xs" 1); -by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); +by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); by(fast_tac HOL_cs 1); -val ss = ss addsimps [result()]; +Addsimps [result()]; goal Qsort.thy "!!xs. [| total(le); transf(le) |] ==> sorted le (qsort le xs)"; by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); -by(simp_tac ss 1); -by(asm_full_simp_tac (ss setloop (split_tac [expand_if])) 1); +by(Simp_tac 1); +by(asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1); by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]); by(fast_tac HOL_cs 1); result(); diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/ex/SList.ML --- a/src/HOL/ex/SList.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/ex/SList.ML Wed Oct 04 13:12:14 1995 +0100 @@ -40,11 +40,11 @@ by (rtac (Rep_list RS list.induct) 1); by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [rangeE, ssubst, Abs_list_inverse RS subst] 1)); -qed "list_induct"; +qed "list_induct2"; (*Perform induction on xs. *) fun list_ind_tac a M = - EVERY [res_inst_tac [("l",a)] list_induct M, + EVERY [res_inst_tac [("l",a)] list_induct2 M, rename_last_tac a ["1"] (M+1)]; (*** Isomorphisms ***) @@ -76,8 +76,8 @@ bind_thm ("Nil_not_Cons", (Cons_not_Nil RS not_sym)); -bind_thm ("Cons_neq_Nil", (Cons_not_Nil RS notE)); -val Nil_neq_Cons = sym RS Cons_neq_Nil; +bind_thm ("Cons_neq_Nil2", (Cons_not_Nil RS notE)); +val Nil_neq_Cons = sym RS Cons_neq_Nil2; (** Injectiveness of CONS and Cons **) @@ -96,7 +96,7 @@ goalw SList.thy [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)"; by (fast_tac list_cs 1); qed "Cons_Cons_eq"; -bind_thm ("Cons_inject", (Cons_Cons_eq RS iffD1 RS conjE)); +bind_thm ("Cons_inject2", (Cons_Cons_eq RS iffD1 RS conjE)); val [major] = goal SList.thy "CONS M N: list(A) ==> M: A & N: list(A)"; by (rtac (major RS setup_induction) 1); @@ -112,28 +112,26 @@ (*Basic ss with constructors and their freeness*) -val list_free_simps = [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq, - CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq] - @ list.intrs; -val list_free_ss = HOL_ss addsimps list_free_simps; +Addsimps ([Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq, CONS_not_NIL, + NIL_not_CONS, CONS_CONS_eq] @ list.intrs); goal SList.thy "!!N. N: list(A) ==> !M. N ~= CONS M N"; by (etac list.induct 1); -by (ALLGOALS (asm_simp_tac list_free_ss)); +by (ALLGOALS Asm_simp_tac); qed "not_CONS_self"; goal SList.thy "!x. l ~= x#l"; by (list_ind_tac "l" 1); -by (ALLGOALS (asm_simp_tac list_free_ss)); -qed "not_Cons_self"; +by (ALLGOALS Asm_simp_tac); +qed "not_Cons_self2"; goal SList.thy "(xs ~= []) = (? y ys. xs = y#ys)"; by(list_ind_tac "xs" 1); -by(simp_tac list_free_ss 1); -by(asm_simp_tac list_free_ss 1); +by(Simp_tac 1); +by(Asm_simp_tac 1); by(REPEAT(resolve_tac [exI,refl,conjI] 1)); -qed "neq_Nil_conv"; +qed "neq_Nil_conv2"; (** Conversion rules for List_case: case analysis operator **) @@ -142,7 +140,7 @@ qed "List_case_NIL"; goalw SList.thy [List_case_def,CONS_def] "List_case c h (CONS M N) = h M N"; -by (simp_tac (HOL_ss addsimps [Split,Case_In1]) 1); +by (simp_tac (!simpset addsimps [Split,Case_In1]) 1); qed "List_case_CONS"; (*** List_rec -- by wf recursion on pred_sexp ***) @@ -157,12 +155,12 @@ goalw SList.thy [CONS_def,In1_def] "!!M. [| M: sexp; N: sexp |] ==> (M, CONS M N) : pred_sexp^+"; -by (asm_simp_tac pred_sexp_ss 1); +by (Asm_simp_tac 1); qed "pred_sexp_CONS_I1"; goalw SList.thy [CONS_def,In1_def] "!!M. [| M: sexp; N: sexp |] ==> (N, CONS M N) : pred_sexp^+"; -by (asm_simp_tac pred_sexp_ss 1); +by (Asm_simp_tac 1); qed "pred_sexp_CONS_I2"; val [prem] = goal SList.thy @@ -179,15 +177,13 @@ goal SList.thy "List_rec NIL c h = c"; by (rtac (List_rec_unfold RS trans) 1); -by (simp_tac (HOL_ss addsimps [List_case_NIL]) 1); +by (simp_tac (!simpset addsimps [List_case_NIL]) 1); qed "List_rec_NIL"; goal SList.thy "!!M. [| M: sexp; N: sexp |] ==> \ \ List_rec (CONS M N) c h = h M N (List_rec N c h)"; by (rtac (List_rec_unfold RS trans) 1); -by (asm_simp_tac - (HOL_ss addsimps [List_case_CONS, list.CONS_I, pred_sexp_CONS_I2, - cut_apply])1); +by (asm_simp_tac (!simpset addsimps [List_case_CONS, pred_sexp_CONS_I2]) 1); qed "List_rec_CONS"; (*** list_rec -- by List_rec ***) @@ -196,24 +192,21 @@ [range_Leaf_subset_sexp RS list_subset_sexp, Rep_list] MRS subsetD; local - val list_rec_simps = list_free_simps @ - [List_rec_NIL, List_rec_CONS, - Abs_list_inverse, Rep_list_inverse, - Rep_list, rangeI, inj_Leaf, Inv_f_f, - sexp.LeafI, Rep_list_in_sexp] + val list_rec_simps = [List_rec_NIL, List_rec_CONS, + Abs_list_inverse, Rep_list_inverse, + Rep_list, rangeI, inj_Leaf, Inv_f_f, + sexp.LeafI, Rep_list_in_sexp] in val list_rec_Nil = prove_goalw SList.thy [list_rec_def, Nil_def] "list_rec Nil c h = c" - (fn _=> [simp_tac (HOL_ss addsimps list_rec_simps) 1]); + (fn _=> [simp_tac (!simpset addsimps list_rec_simps) 1]); val list_rec_Cons = prove_goalw SList.thy [list_rec_def, Cons_def] "list_rec (a#l) c h = h a l (list_rec l c h)" - (fn _=> [simp_tac (HOL_ss addsimps list_rec_simps) 1]); + (fn _=> [simp_tac (!simpset addsimps list_rec_simps) 1]); end; -val list_simps = [List_rec_NIL, List_rec_CONS, - list_rec_Nil, list_rec_Cons]; -val list_ss = list_free_ss addsimps list_simps; +Addsimps [List_rec_NIL, List_rec_CONS, list_rec_Nil, list_rec_Cons]; (*Type checking. Useful?*) @@ -226,7 +219,7 @@ val sexp_ListA_I = A_subset_sexp RS list_subset_sexp RS subsetD; val sexp_A_I = A_subset_sexp RS subsetD; by (rtac (major RS list.induct) 1); -by (ALLGOALS(asm_simp_tac (list_ss addsimps ([sexp_A_I,sexp_ListA_I]@prems)))); +by (ALLGOALS(asm_simp_tac (!simpset addsimps ([sexp_A_I,sexp_ListA_I]@prems)))); qed "List_rec_type"; (** Generalized map functionals **) @@ -241,8 +234,8 @@ qed "Rep_map_Cons"; goalw SList.thy [Rep_map_def] "!!f. (!!x. f(x): A) ==> Rep_map f xs: list(A)"; -by (rtac list_induct 1); -by(ALLGOALS(asm_simp_tac list_ss)); +by (rtac list_induct2 1); +by(ALLGOALS Asm_simp_tac); qed "Rep_map_type"; goalw SList.thy [Abs_map_def] "Abs_map g NIL = Nil"; @@ -278,20 +271,18 @@ val [_,hd_Cons] = list_recs hd_def; val [_,tl_Cons] = list_recs tl_def; val [ttl_Nil,ttl_Cons] = list_recs ttl_def; -val [append_Nil,append_Cons] = list_recs append_def; +val [append_Nil3,append_Cons] = list_recs append_def; val [mem_Nil, mem_Cons] = list_recs mem_def; val [map_Nil,map_Cons] = list_recs map_def; val [list_case_Nil,list_case_Cons] = list_recs list_case_def; val [filter_Nil,filter_Cons] = list_recs filter_def; val [list_all_Nil,list_all_Cons] = list_recs list_all_def; -val list_ss = arith_ss addsimps - [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq, - list_rec_Nil, list_rec_Cons, - null_Nil, null_Cons, hd_Cons, tl_Cons, ttl_Nil, ttl_Cons, +Addsimps + [null_Nil, ttl_Nil, mem_Nil, mem_Cons, list_case_Nil, list_case_Cons, - append_Nil, append_Cons, + append_Nil3, append_Cons, map_Nil, map_Cons, list_all_Nil, list_all_Cons, filter_Nil, filter_Cons]; @@ -301,57 +292,54 @@ goal SList.thy "(xs@ys)@zs = xs@(ys@zs)"; by(list_ind_tac "xs" 1); -by(ALLGOALS(asm_simp_tac list_ss)); -qed "append_assoc"; +by(ALLGOALS Asm_simp_tac); +qed "append_assoc2"; goal SList.thy "xs @ [] = xs"; by(list_ind_tac "xs" 1); -by(ALLGOALS(asm_simp_tac list_ss)); -qed "append_Nil2"; +by(ALLGOALS Asm_simp_tac); +qed "append_Nil4"; (** mem **) goal SList.thy "x mem (xs@ys) = (x mem xs | x mem ys)"; by(list_ind_tac "xs" 1); -by(ALLGOALS(asm_simp_tac (list_ss setloop (split_tac [expand_if])))); -qed "mem_append"; +by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); +qed "mem_append2"; goal SList.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))"; by(list_ind_tac "xs" 1); -by(ALLGOALS(asm_simp_tac (list_ss setloop (split_tac [expand_if])))); -qed "mem_filter"; +by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); +qed "mem_filter2"; (** list_all **) goal SList.thy "(Alls x:xs.True) = True"; by(list_ind_tac "xs" 1); -by(ALLGOALS(asm_simp_tac list_ss)); -qed "list_all_True"; +by(ALLGOALS Asm_simp_tac); +qed "list_all_True2"; goal SList.thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)"; by(list_ind_tac "xs" 1); -by(ALLGOALS(asm_simp_tac list_ss)); -qed "list_all_conj"; +by(ALLGOALS Asm_simp_tac); +qed "list_all_conj2"; goal SList.thy "(Alls x:xs.P(x)) = (!x. x mem xs --> P(x))"; by(list_ind_tac "xs" 1); -by(ALLGOALS(asm_simp_tac (list_ss setloop (split_tac [expand_if])))); +by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); by(fast_tac HOL_cs 1); -qed "list_all_mem_conv"; +qed "list_all_mem_conv2"; (** The functional "map" **) -val map_simps = [Abs_map_NIL, Abs_map_CONS, - Rep_map_Nil, Rep_map_Cons, - map_Nil, map_Cons]; -val map_ss = list_free_ss addsimps map_simps; +Addsimps [Rep_map_Nil, Rep_map_Cons, Abs_map_NIL, Abs_map_CONS]; val [major,A_subset_sexp,minor] = goal SList.thy "[| M: list(A); A<=sexp; !!z. z: A ==> f(g(z)) = z |] \ \ ==> Rep_map f (Abs_map g M) = M"; by (rtac (major RS list.induct) 1); -by (ALLGOALS (asm_simp_tac(map_ss addsimps [sexp_A_I,sexp_ListA_I,minor]))); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [sexp_A_I,sexp_ListA_I,minor]))); qed "Abs_map_inverse"; (*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*) @@ -362,36 +350,33 @@ "P(list_case a f xs) = ((xs=[] --> P(a)) & \ \ (!y ys. xs=y#ys --> P(f y ys)))"; by(list_ind_tac "xs" 1); -by(ALLGOALS(asm_simp_tac list_ss)); +by(ALLGOALS Asm_simp_tac); by(fast_tac HOL_cs 1); -qed "expand_list_case"; +qed "expand_list_case2"; (** Additional mapping lemmas **) goal SList.thy "map (%x.x) xs = xs"; by (list_ind_tac "xs" 1); -by (ALLGOALS (asm_simp_tac map_ss)); -qed "map_ident"; +by (ALLGOALS Asm_simp_tac); +qed "map_ident2"; goal SList.thy "map f (xs@ys) = map f xs @ map f ys"; by (list_ind_tac "xs" 1); -by (ALLGOALS (asm_simp_tac (map_ss addsimps [append_Nil,append_Cons]))); -qed "map_append"; +by (ALLGOALS Asm_simp_tac); +qed "map_append2"; goalw SList.thy [o_def] "map (f o g) xs = map f (map g xs)"; by (list_ind_tac "xs" 1); -by (ALLGOALS (asm_simp_tac map_ss)); -qed "map_compose"; +by (ALLGOALS Asm_simp_tac); +qed "map_compose2"; goal SList.thy "!!f. (!!x. f(x): sexp) ==> \ \ Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs"; by (list_ind_tac "xs" 1); -by(ALLGOALS(asm_simp_tac(map_ss addsimps +by(ALLGOALS(asm_simp_tac(!simpset addsimps [Rep_map_type,list_sexp RS subsetD]))); qed "Abs_Rep_map"; -val list_ss = list_ss addsimps - [mem_append, mem_filter, append_assoc, append_Nil2, map_ident, - list_all_True, list_all_conj]; - +Addsimps [append_Nil4, map_ident2]; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/ex/SList.thy --- a/src/HOL/ex/SList.thy Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/ex/SList.thy Wed Oct 04 13:12:14 1995 +0100 @@ -105,16 +105,16 @@ hd_def "hd(xs) == list_rec xs (@x.True) (%x xs r.x)" tl_def "tl(xs) == list_rec xs (@xs.True) (%x xs r.xs)" (* a total version of tl: *) - ttl_def "ttl(xs) == list_rec xs [] (%x xs r.xs)" + ttl_def "ttl(xs) == list_rec xs [] (%x xs r.xs)" - mem_def "x mem xs == + mem_def "x mem xs == list_rec xs False (%y ys r. if y=x then True else r)" list_all_def "list_all P xs == list_rec xs True (%x l r. P(x) & r)" map_def "map f xs == list_rec xs [] (%x l r. f(x)#r)" - append_def "xs@ys == list_rec xs ys (%x l r. x#r)" - filter_def "filter P xs == + append_def "xs@ys == list_rec xs ys (%x l r. x#r)" + filter_def "filter P xs == list_rec xs [] (%x xs r. if P(x) then x#r else r)" - list_case_def "list_case a f xs == list_rec xs a (%x xs r.f x xs)" + list_case_def "list_case a f xs == list_rec xs a (%x xs r.f x xs)" end diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/ex/Simult.ML --- a/src/HOL/ex/Simult.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/ex/Simult.ML Wed Oct 04 13:12:14 1995 +0100 @@ -236,8 +236,8 @@ "!!M N. [| M: sexp; N: sexp |] ==> \ \ TF_rec (TCONS M N) b c d = b M N (TF_rec N b c d)"; by (rtac (TF_rec_unfold RS trans) 1); -by (simp_tac (HOL_ss addsimps [Case_In0, Split]) 1); -by (asm_simp_tac (pred_sexp_ss addsimps [In0_def]) 1); +by (simp_tac (!simpset addsimps [Case_In0, Split]) 1); +by (asm_simp_tac (!simpset addsimps [In0_def]) 1); qed "TF_rec_TCONS"; goalw Simult.thy [FNIL_def] "TF_rec FNIL b c d = c"; @@ -250,7 +250,7 @@ \ TF_rec (FCONS M N) b c d = d M N (TF_rec M b c d) (TF_rec N b c d)"; by (rtac (TF_rec_unfold RS trans) 1); by (simp_tac (HOL_ss addsimps [Case_In1, List_case_CONS]) 1); -by (asm_simp_tac (pred_sexp_ss addsimps [CONS_def,In1_def]) 1); +by (asm_simp_tac (!simpset addsimps [CONS_def,In1_def]) 1); qed "TF_rec_FCONS"; @@ -263,13 +263,13 @@ [range_Leaf_subset_sexp RS TF_subset_sexp RS (Part_subset RS subset_trans), Rep_Forest] MRS subsetD; -val tf_rec_simps = [TF_rec_TCONS, TF_rec_FNIL, TF_rec_FCONS, - TCONS_I, FNIL_I, FCONS_I, Rep_Tree, Rep_Forest, - Rep_Tree_inverse, Rep_Forest_inverse, - Abs_Tree_inverse, Abs_Forest_inverse, - inj_Leaf, Inv_f_f, sexp.LeafI, range_eqI, - Rep_Tree_in_sexp, Rep_Forest_in_sexp]; -val tf_rec_ss = HOL_ss addsimps tf_rec_simps; +val tf_rec_ss = HOL_ss addsimps + [TF_rec_TCONS, TF_rec_FNIL, TF_rec_FCONS, + TCONS_I, FNIL_I, FCONS_I, Rep_Tree, Rep_Forest, + Rep_Tree_inverse, Rep_Forest_inverse, + Abs_Tree_inverse, Abs_Forest_inverse, + inj_Leaf, Inv_f_f, sexp.LeafI, range_eqI, + Rep_Tree_in_sexp, Rep_Forest_in_sexp]; goalw Simult.thy [tree_rec_def, forest_rec_def, Tcons_def] "tree_rec (Tcons a tf) b c d = b a tf (forest_rec tf b c d)"; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/ex/Sorting.ML --- a/src/HOL/ex/Sorting.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/ex/Sorting.ML Wed Oct 04 13:12:14 1995 +0100 @@ -6,21 +6,19 @@ Some general lemmas *) -val sorting_ss = list_ss addsimps - [Sorting.mset_Nil,Sorting.mset_Cons, - Sorting.sorted_Nil,Sorting.sorted_Cons, - Sorting.sorted1_Nil,Sorting.sorted1_One,Sorting.sorted1_Cons]; +Addsimps [Sorting.mset_Nil,Sorting.mset_Cons, + Sorting.sorted_Nil,Sorting.sorted_Cons, + Sorting.sorted1_Nil,Sorting.sorted1_One,Sorting.sorted1_Cons]; goal Sorting.thy "!x.mset (xs@ys) x = mset xs x + mset ys x"; by(list.induct_tac "xs" 1); -by(ALLGOALS(asm_simp_tac (sorting_ss setloop (split_tac [expand_if])))); +by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); qed "mset_app_distr"; goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs.p(x)] x = \ \ mset xs x"; by(list.induct_tac "xs" 1); -by(ALLGOALS(asm_simp_tac (sorting_ss setloop (split_tac [expand_if])))); +by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); qed "mset_compl_add"; -val sorting_ss = sorting_ss addsimps - [mset_app_distr, mset_compl_add]; +Addsimps [mset_app_distr, mset_compl_add]; diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/ex/String.ML --- a/src/HOL/ex/String.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/ex/String.ML Wed Oct 04 13:12:14 1995 +0100 @@ -1,22 +1,20 @@ -val string_ss = list_ss addsimps (String.nibble.simps @ String.char.simps); - goal String.thy "hd(''ABCD'') = CHR ''A''"; -by(simp_tac string_ss 1); +by(Simp_tac 1); result(); goal String.thy "hd(''ABCD'') ~= CHR ''B''"; -by(simp_tac string_ss 1); +by(Simp_tac 1); result(); goal String.thy "''ABCD'' ~= ''ABCX''"; -by(simp_tac string_ss 1); +by(Simp_tac 1); result(); goal String.thy "''ABCD'' = ''ABCD''"; -by(simp_tac string_ss 1); +by(Simp_tac 1); result(); goal String.thy "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''"; -by(simp_tac string_ss 1); +by(Simp_tac 1); result(); diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/ex/Term.ML --- a/src/HOL/ex/Term.ML Wed Oct 04 13:11:57 1995 +0100 +++ b/src/HOL/ex/Term.ML Wed Oct 04 13:12:14 1995 +0100 @@ -60,8 +60,6 @@ (*** Structural Induction on the abstract type 'a term ***) -val list_all_ss = map_ss addsimps [list_all_Nil, list_all_Cons]; - val Rep_term_in_sexp = Rep_term RS (range_Leaf_subset_sexp RS term_subset_sexp RS subsetD); @@ -89,7 +87,7 @@ by (etac rev_subsetD 2); by (rtac list_subset_sexp 2); by (fast_tac set_cs 2); -by (ALLGOALS (asm_simp_tac list_all_ss)); +by (ALLGOALS Asm_simp_tac); qed "term_induct"; (*Induction for the abstract type 'a term*) @@ -99,8 +97,8 @@ \ |] ==> R(t)"; by (rtac term_induct 1); (*types force good instantiation*) by (etac rev_mp 1); -by (rtac list_induct 1); (*types force good instantiation*) -by (ALLGOALS (asm_simp_tac (list_all_ss addsimps prems))); +by (rtac list_induct2 1); (*types force good instantiation*) +by (ALLGOALS (asm_simp_tac (!simpset addsimps prems))); qed "term_induct2"; (*Perform induction on xs. *) @@ -123,10 +121,10 @@ \ Abs_map (cut h (pred_sexp^+) M) N = \ \ Abs_map h N"; by (rtac (prem RS list.induct) 1); -by (simp_tac list_all_ss 1); +by (Simp_tac 1); by (strip_tac 1); by (etac (pred_sexp_CONS_D RS conjE) 1); -by (asm_simp_tac (list_all_ss addsimps [trancl_pred_sexpD1, cut_apply]) 1); +by (asm_simp_tac (!simpset addsimps [trancl_pred_sexpD1]) 1); qed "Abs_map_lemma"; val [prem1,prem2,A_subset_sexp] = goal Term.thy @@ -137,7 +135,7 @@ [Split, prem2 RS Abs_map_lemma RS spec RS mp, pred_sexpI2 RS r_into_trancl, prem1, prem2 RS rev_subsetD, list_subset_sexp, - term_subset_sexp, A_subset_sexp])1); + term_subset_sexp, A_subset_sexp]) 1); qed "Term_rec"; (*** term_rec -- by Term_rec ***) @@ -150,11 +148,10 @@ (*Now avoids conditional rewriting with the premise N: list(term(A)), since A will be uninstantiated and will cause rewriting to fail. *) - val term_rec_ss = HOL_ss + val term_rec_ss = HOL_ss addsimps [Rep_Tlist RS (rangeI RS term.APP_I RS Abs_term_inverse), - Rep_term_in_sexp, Rep_Term_rec, Rep_term_inverse, - inj_Leaf, Inv_f_f, - Abs_Rep_map, map_ident, sexp.LeafI] + Rep_term_in_sexp, Rep_Term_rec, Rep_term_inverse, inj_Leaf, + Inv_f_f, Abs_Rep_map, map_ident2, sexp.LeafI] in val term_rec = prove_goalw Term.thy