--- 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";
--- 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
--- 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]
--- 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,s> -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,s> -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,s> -c-> t ==> (s,t) : C(c)";
--- 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);
--- 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()];
--- 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";
-
-
--- 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);
--- 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";
--- 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()];
--- 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();
--- 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);
-
--- 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 --> 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<x --> 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<x --> (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<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 "unzero_less";
(* Odd proof. Why do induction? *)
goal Arith.thy "((x::nat) = y + z) --> (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);
--- 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<count M x --> 0<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.count_def,
Multiset.countm_empty_def]) 1);
- by (asm_simp_tac (arith_ss addsimps
+ by (asm_simp_tac (!simpset addsimps
[Multiset.count_def,Multiset.delm_nonempty_def,
Multiset.countm_nonempty_def]
setloop (split_tac [expand_if])) 1);
@@ -73,10 +73,10 @@
goal Multiset.thy
"!!P. P(x) ==> 0<count M x --> 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]
--- 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
--- 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 =
--- 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";
--- 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
--- 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<n then fst ex i \
\ else (if i=n then Some a else None), \
\ %i.if i<Suc n then snd ex i else t)")] bexI 1);
by(res_inst_tac [("x","Suc(n)")] exI 1);
- by(simp_tac SS 1);
- by(asm_simp_tac (SS delsimps [less_Suc_eq]) 1);
+ by(Simp_tac 1);
+ by(asm_simp_tac (!simpset delsimps [less_Suc_eq]) 1);
by(REPEAT(rtac allI 1));
by(res_inst_tac [("m","na"),("n","n")] (make_elim less_linear) 1);
be disjE 1;
- by(asm_simp_tac SS 1);
+ by(Asm_simp_tac 1);
be disjE 1;
- by(asm_simp_tac SS 1);
+ by(Asm_simp_tac 1);
by(fast_tac HOL_cs 1);
by(forward_tac [less_not_sym] 1);
- by(asm_simp_tac (SS addsimps [less_not_refl2]) 1);
+ by(asm_simp_tac (!simpset addsimps [less_not_refl2]) 1);
qed "reachable_n";
val [p1,p2] = goalw IOA.thy [invariant_def]
@@ -82,7 +82,7 @@
by (fast_tac (set_cs addIs [p1,reachable_0]) 1);
by (eres_inst_tac[("x","n1")]allE 1);
by (eres_inst_tac[("P","%x.!a.?Q x a"), ("opt","fst ex n1")] optE 1);
- by (asm_simp_tac HOL_ss 1);
+ by (Asm_simp_tac 1);
by (safe_tac HOL_cs);
by (etac (p2 RS mp) 1);
by (ALLGOALS(fast_tac(set_cs addDs [hd Option.option.inject RS iffD1,
@@ -103,14 +103,14 @@
goal IOA.thy
"actions(asig_comp a b) = actions(a) Un actions(b)";
- by(simp_tac (prod_ss addsimps
+ by(simp_tac (!simpset addsimps
([actions_def,asig_comp_def]@asig_projections)) 1);
by(fast_tac eq_cs 1);
qed "actions_asig_comp";
goal IOA.thy
"starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}";
- by(simp_tac (SS addsimps (par_def::ioa_projections)) 1);
+ by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
qed "starts_of_par";
(* Every state in an execution is reachable *)
@@ -134,7 +134,7 @@
\ (if a:actions(asig_of(D)) then \
\ (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D) \
\ else snd(snd(snd(t)))=snd(snd(snd(s)))))";
- by(simp_tac (SS addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq]@
+ by(simp_tac (!simpset addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq]@
ioa_projections)
setloop (split_tac [expand_if])) 1);
qed "trans_of_par4";
@@ -142,31 +142,31 @@
goal IOA.thy "starts_of(restrict ioa acts) = starts_of(ioa) & \
\ trans_of(restrict ioa acts) = trans_of(ioa) & \
\ reachable (restrict ioa acts) s = reachable ioa s";
-by(simp_tac (SS addsimps ([is_execution_fragment_def,executions_def,
+by(simp_tac (!simpset addsimps ([is_execution_fragment_def,executions_def,
reachable_def,restrict_def]@ioa_projections)) 1);
qed "cancel_restrict";
goal IOA.thy "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)";
- by(simp_tac (SS addsimps (par_def::ioa_projections)) 1);
+ by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
qed "asig_of_par";
goal IOA.thy "externals(asig_of(A1||A2)) = \
\ (externals(asig_of(A1)) Un 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,Un_def,set_diff_def]) 1);
+by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_of_par,asig_comp_def,asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1);
by (rtac set_ext 1);
by (fast_tac set_cs 1);
qed"externals_of_par";
goalw IOA.thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
"!! a. [| compat_ioas A1 A2; 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"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";
--- 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";
--- 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";
--- 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*)
--- 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<z2; z2<z3 |] ==> 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<zsuc(z)";
@@ -602,9 +601,9 @@
by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc]));
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
by (safe_tac intrel_cs);
-by (asm_full_simp_tac (intrel_ss addsimps ([znat_def, zadd])) 1);
+by (asm_full_simp_tac (!simpset addsimps ([znat_def, zadd])) 1);
by (asm_full_simp_tac
- (HOL_ss addsimps [add_left_cancel, add_assoc, add_Suc_right RS sym]) 1);
+ (!simpset delsimps [add_Suc_right] addsimps [add_left_cancel, add_assoc, add_Suc_right RS sym]) 1);
by (resolve_tac [less_not_refl2 RS notE] 1);
by (etac sym 2);
by (REPEAT (resolve_tac [lessI, trans_less_add2, less_SucI] 1));
@@ -633,7 +632,7 @@
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, Image_iff, Bex_def]) 1);
+ (!simpset addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
by (etac disjE 2);
by (assume_tac 2);
@@ -641,7 +640,7 @@
(swap_res_tac [exI] 1 THEN
swap_res_tac [exI] 1 THEN
etac conjI 1 THEN
- simp_tac (arith_ss addsimps add_ac) 1));
+ simp_tac (!simpset addsimps add_ac) 1));
qed "zless_linear";
@@ -650,12 +649,12 @@
goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def]
"($#m < $#n) = (m<n)";
by (simp_tac
- (intrel_ss addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
+ (!simpset addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
by (fast_tac (HOL_cs addIs [add_commute] addSEs [less_add_eq_less]) 1);
qed "zless_eq_less";
goalw Integ.thy [zle_def, le_def] "($#m <= $#n) = (m<=n)";
-by (simp_tac (HOL_ss addsimps [zless_eq_less]) 1);
+by (simp_tac (!simpset addsimps [zless_eq_less]) 1);
qed "zle_eq_le";
goalw Integ.thy [zle_def] "!!w. ~(w<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";
--- 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]
--- 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<j ==> (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<i ==> (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";
--- 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";
--- 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)",
--- 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";
--- 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";
--- 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])
--- 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 {}
--- 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";
--- 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];
--- 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";
--- 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
--- 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";
--- 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();
--- 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";
--- 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";
-
-
--- 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";
--- 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";
--- 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";
--- 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<n --> 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);
--- 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();
--- 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];
--- 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
--- 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)";
--- 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];
--- 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();
--- 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