--- a/src/HOLCF/Cfun2.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Cfun2.ML Mon Nov 03 14:06:27 1997 +0100
@@ -23,7 +23,7 @@
qed_goal "less_cfun" thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
(fn prems =>
[
- (simp_tac (!simpset addsimps [inst_cfun_po]) 1)
+ (simp_tac (simpset() addsimps [inst_cfun_po]) 1)
]);
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/Cfun3.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Cfun3.ML Mon Nov 03 14:06:27 1997 +0100
@@ -339,7 +339,7 @@
qed_goalw "strictify1" thy [strictify_def] "strictify`f`UU=UU" (fn _ => [
(stac beta_cfun 1),
- (simp_tac (!simpset addsimps [cont_Istrictify2,cont_Istrictify1,
+ (simp_tac (simpset() addsimps [cont_Istrictify2,cont_Istrictify1,
cont2cont_CF1L]) 1),
(stac beta_cfun 1),
(rtac cont_Istrictify2 1),
@@ -349,7 +349,7 @@
qed_goalw "strictify2" thy [strictify_def]
"~x=UU ==> strictify`f`x=f`x" (fn prems => [
(stac beta_cfun 1),
- (simp_tac (!simpset addsimps [cont_Istrictify2,cont_Istrictify1,
+ (simp_tac (simpset() addsimps [cont_Istrictify2,cont_Istrictify1,
cont2cont_CF1L]) 1),
(stac beta_cfun 1),
(rtac cont_Istrictify2 1),
@@ -370,7 +370,7 @@
(* ------------------------------------------------------------------------ *)
(* HINT: cont_tac is now installed in simplifier in Lift.ML ! *)
-(*simpset := !simpset addsolver (K (DEPTH_SOLVE_1 o cont_tac));*)
+(*simpset_ref() := simpset() addsolver (K (DEPTH_SOLVE_1 o cont_tac));*)
(* ------------------------------------------------------------------------ *)
(* some lemmata for functions with flat/chain_finite domain/range types *)
--- a/src/HOLCF/Cont.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Cont.ML Mon Nov 03 14:06:27 1997 +0100
@@ -666,7 +666,7 @@
cut_facts_tac prems 1,
strip_tac 1,
dtac (ax_flat RS spec RS spec RS mp) 1,
- fast_tac ((HOL_cs addss (!simpset addsimps [minimal]))) 1
+ fast_tac ((HOL_cs addss (simpset() addsimps [minimal]))) 1
]);
--- a/src/HOLCF/Cprod2.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Cprod2.ML Mon Nov 03 14:06:27 1997 +0100
@@ -40,7 +40,7 @@
qed_goal "minimal_cprod" thy "(UU,UU)<<p"
(fn prems =>
[
- (simp_tac(!simpset addsimps[inst_cprod_po])1)
+ (simp_tac(simpset() addsimps[inst_cprod_po])1)
]);
bind_thm ("UU_cprod_def",minimal_cprod RS minimal2UU RS sym);
@@ -62,13 +62,13 @@
(strip_tac 1),
(rtac (less_fun RS iffD2) 1),
(strip_tac 1),
- (asm_simp_tac (!simpset addsimps [inst_cprod_po]) 1)
+ (asm_simp_tac (simpset() addsimps [inst_cprod_po]) 1)
]);
qed_goalw "monofun_pair2" thy [monofun] "monofun(Pair x)"
(fn prems =>
[
- (asm_simp_tac (!simpset addsimps [inst_cprod_po]) 1)
+ (asm_simp_tac (simpset() addsimps [inst_cprod_po]) 1)
]);
qed_goal "monofun_pair" thy "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)"
--- a/src/HOLCF/Cprod3.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Cprod3.ML Mon Nov 03 14:06:27 1997 +0100
@@ -155,7 +155,7 @@
(fn prems =>
[
(stac beta_cfun 1),
- (simp_tac (!simpset addsimps [cont_pair1,cont_pair2,cont2cont_CF1L]) 1),
+ (simp_tac (simpset() addsimps [cont_pair1,cont_pair2,cont2cont_CF1L]) 1),
(stac beta_cfun 1),
(rtac cont_pair2 1),
(rtac refl 1)
@@ -287,7 +287,7 @@
[
(stac beta_cfun 1),
(Simp_tac 1),
- (simp_tac (!simpset addsimps [cfst2,csnd2]) 1)
+ (simp_tac (simpset() addsimps [cfst2,csnd2]) 1)
]);
qed_goalw "csplit3" Cprod3.thy [csplit_def]
@@ -296,7 +296,7 @@
[
(stac beta_cfun 1),
(Simp_tac 1),
- (simp_tac (!simpset addsimps [surjective_pairing_Cprod2]) 1)
+ (simp_tac (simpset() addsimps [surjective_pairing_Cprod2]) 1)
]);
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/Discrete.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Discrete.ML Mon Nov 03 14:06:27 1997 +0100
@@ -11,10 +11,10 @@
goal thy
"!!S::nat=>('a::term)discr. is_chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
-by(fast_tac (!claset addDs [discr_chain0] addEs [arg_cong]) 1);
+by(fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1);
qed "discr_chain_f_range0";
goalw thy [cont,is_lub,is_ub] "cont(%x::('a::term)discr. f x)";
-by(simp_tac (!simpset addsimps [discr_chain_f_range0]) 1);
+by(simp_tac (simpset() addsimps [discr_chain_f_range0]) 1);
qed "cont_discr";
AddIffs [cont_discr];
--- a/src/HOLCF/Discrete1.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Discrete1.ML Mon Nov 03 14:06:27 1997 +0100
@@ -22,7 +22,7 @@
goal thy
"!!S::nat=>('a::term)discr. is_chain(S) ==> range(S) = {S 0}";
-by (fast_tac (!claset addEs [discr_chain0]) 1);
+by (fast_tac (claset() addEs [discr_chain0]) 1);
qed "discr_chain_range0";
Addsimps [discr_chain_range0];
--- a/src/HOLCF/Fix.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Fix.ML Mon Nov 03 14:06:27 1997 +0100
@@ -330,7 +330,7 @@
qed_goalw "fix_eq" thy [fix_def] "fix`F = F`(fix`F)"
(fn prems =>
[
- (asm_simp_tac (!simpset addsimps [cont_Ifix]) 1),
+ (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1),
(rtac Ifix_eq 1)
]);
@@ -338,7 +338,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac (!simpset addsimps [cont_Ifix]) 1),
+ (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1),
(etac Ifix_least 1)
]);
@@ -439,7 +439,7 @@
(fn prems =>
[
(fold_goals_tac [Ifix_def]),
- (asm_simp_tac (!simpset addsimps [cont_Ifix]) 1)
+ (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1)
]);
@@ -563,7 +563,7 @@
strip_tac 1,
dtac chfin_fappR 1,
eres_inst_tac [("x","s")] allE 1,
- fast_tac (HOL_cs addss (!simpset addsimps [chfin])) 1]);
+ fast_tac (HOL_cs addss (simpset() addsimps [chfin])) 1]);
(* adm_flat not needed any more, since it is a special case of adm_chfindom *)
@@ -670,7 +670,7 @@
qed_goal "adm_eq" thy
"!!u. [|cont u ; cont v|]==> adm(%x. u x = v x)"
- (fn prems => [asm_simp_tac (!simpset addsimps [po_eq_conv]) 1]);
+ (fn prems => [asm_simp_tac (simpset() addsimps [po_eq_conv]) 1]);
@@ -691,13 +691,13 @@
val adm_disj_lemma2 = prove_goal thy
"!!Q. [| adm(Q); ? X. is_chain(X) & (!n. Q(X(n))) &\
\ lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))"
- (fn _ => [fast_tac (!claset addEs [admD] addss !simpset) 1]);
+ (fn _ => [fast_tac (claset() addEs [admD] addss simpset()) 1]);
val adm_disj_lemma3 = prove_goalw thy [is_chain]
"!!Q. is_chain(Y) ==> is_chain(%m. if m < Suc i then Y(Suc i) else Y m)"
(fn _ =>
[
- asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1,
+ asm_simp_tac (simpset() setloop (split_tac[expand_if])) 1,
safe_tac HOL_cs,
subgoal_tac "ia = i" 1,
Asm_simp_tac 1,
@@ -708,7 +708,7 @@
"!!Q. !j. i < j --> Q(Y(j)) ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)"
(fn _ =>
[
- asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1,
+ asm_simp_tac (simpset() setloop (split_tac[expand_if])) 1,
strip_tac 1,
etac allE 1,
etac mp 1,
@@ -722,7 +722,7 @@
[
safe_tac (HOL_cs addSIs [lub_equal2,adm_disj_lemma3]),
atac 2,
- asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1,
+ asm_simp_tac (simpset() setloop (split_tac[expand_if])) 1,
res_inst_tac [("x","i")] exI 1,
strip_tac 1,
trans_tac 1
--- a/src/HOLCF/Fun2.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Fun2.ML Mon Nov 03 14:06:27 1997 +0100
@@ -23,7 +23,7 @@
qed_goal "minimal_fun" thy "(%z. UU) << x"
(fn prems =>
[
- (simp_tac (!simpset addsimps [inst_fun_po,minimal]) 1)
+ (simp_tac (simpset() addsimps [inst_fun_po,minimal]) 1)
]);
bind_thm ("UU_fun_def",minimal_fun RS minimal2UU RS sym);
--- a/src/HOLCF/HOLCF.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/HOLCF.ML Mon Nov 03 14:06:27 1997 +0100
@@ -8,7 +8,7 @@
use"adm.ML";
-simpset := !simpset addSolver(fn thms =>
+simpset_ref() := simpset() addSolver(fn thms =>
(adm_tac (cut_facts_tac thms THEN' cont_tacRs)));
-val HOLCF_ss = !simpset;
+val HOLCF_ss = simpset();
--- a/src/HOLCF/IMP/Denotational.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IMP/Denotational.ML Mon Nov 03 14:06:27 1997 +0100
@@ -18,7 +18,7 @@
goalw thy [dlift_def]
"(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)";
-by (simp_tac (!simpset setloop (split_tac[expand_lift_case])) 1);
+by (simp_tac (simpset() setloop (split_tac[expand_lift_case])) 1);
qed "dlift_is_Def";
Addsimps [dlift_is_Def];
@@ -30,19 +30,19 @@
goal thy "!s t. D c`(Discr s) = (Def t) --> <c,s> -c-> t";
by (com.induct_tac "c" 1);
- by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
- by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
- by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
- by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
- by (fast_tac ((HOL_cs addIs evalc.intrs) addss !simpset) 1);
+ by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
+ by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
+ by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
+ by (simp_tac (simpset() setloop (split_tac[expand_if])) 1);
+ by (fast_tac ((HOL_cs addIs evalc.intrs) addss simpset()) 1);
by (Simp_tac 1);
by (rtac fix_ind 1);
by (fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,ax_flat_lift])) 1);
by (Simp_tac 1);
-by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (simp_tac (simpset() setloop (split_tac[expand_if])) 1);
by (safe_tac HOL_cs);
by (fast_tac (HOL_cs addIs evalc.intrs) 1);
- by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
+ by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
qed_spec_mp "D_implies_eval";
--- a/src/HOLCF/IMP/HoareEx.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IMP/HoareEx.ML Mon Nov 03 14:06:27 1997 +0100
@@ -14,6 +14,6 @@
(* simplifier with enhanced adm-tactic: *)
by (Simp_tac 1);
by (Simp_tac 1);
-by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (simp_tac (simpset() setloop (split_tac[expand_if])) 1);
by(Blast_tac 1);
qed "WHILE_rule_sound";
--- a/src/HOLCF/IOA/ABP/Correctness.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/ABP/Correctness.ML Mon Nov 03 14:06:27 1997 +0100
@@ -83,7 +83,7 @@
by (List.list.induct_tac "l" 1);
by (Simp_tac 1);
by (case_tac "list =[]" 1);
-by (asm_full_simp_tac (!simpset 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 1);
@@ -93,7 +93,7 @@
by (Asm_simp_tac 1);
by (rtac (expand_if RS ssubst) 1);
by (hyp_subst_tac 1);
-by (asm_full_simp_tac (!simpset 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 *)
@@ -109,7 +109,7 @@
(rev_red_not_nil RS mp)]) 1);
qed"last_ind_on_first";
-val impl_ss = !simpset delsimps [reduce_Cons];
+val impl_ss = simpset() delsimps [reduce_Cons];
(* Main Lemma 1 for S_pkt in showing that reduce is refinement *)
goal Correctness.thy
@@ -122,7 +122,7 @@
by (List.list.induct_tac "l" 1);
by (Simp_tac 1);
by (case_tac "list=[]" 1);
- by (asm_full_simp_tac (!simpset 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 1);
by (cut_inst_tac [("l","list")] cons_not_nil 1);
@@ -131,16 +131,16 @@
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 (!simpset 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 1);
by (case_tac "list=[]" 1);
by (cut_inst_tac [("l","list")] cons_not_nil 2);
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (auto_tac (!claset,
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (auto_tac (claset(),
impl_ss addsimps [last_ind_on_first,l_iff_red_nil]
setloop split_tac [expand_if]));
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
qed"reduce_hd";
@@ -156,7 +156,7 @@
by (Asm_full_simp_tac 1);
by (rtac (expand_if RS ssubst) 1);
by (rtac conjI 1);
-by (simp_tac (!simpset addsimps [and_de_morgan_and_absorbe]) 2);
+by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe]) 2);
by (Step_tac 1);
by (ALLGOALS (cut_inst_tac [("l","xs")] cons_not_nil));
by (Auto_tac());
@@ -169,13 +169,13 @@
goal Correctness.thy
"is_weak_ref_map reduce ch_ioa ch_fin_ioa";
-by (simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
+by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
(* ---------------- main-part ------------------- *)
by (REPEAT (rtac allI 1));
by (rtac imp_conj_lemma 1);
by (abs_action.induct_tac "a" 1);
(* ----------------- 2 cases ---------------------*)
-by (ALLGOALS (simp_tac (!simpset addsimps [externals_def])));
+by (ALLGOALS (simp_tac (simpset() addsimps [externals_def])));
(* fst case --------------------------------------*)
by (rtac impI 1);
by (rtac disjI2 1);
@@ -184,9 +184,9 @@
by (rtac impI 1);
by (REPEAT (etac conjE 1));
by (etac disjE 1);
-by (asm_full_simp_tac (!simpset 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 (!simpset 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);
@@ -210,7 +210,7 @@
the absence of internal actions. *)
goal Correctness.thy
"is_weak_ref_map (%id. id) sender_ioa sender_ioa";
-by (simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
+by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
by (TRY(
(rtac conjI 1) THEN
(* start states *)
@@ -220,13 +220,13 @@
by (rtac imp_conj_lemma 1);
by (Action.action.induct_tac "a" 1);
(* 7 cases *)
-by (ALLGOALS (simp_tac ((!simpset 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_ref_map (%id. id) receiver_ioa receiver_ioa";
-by (simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
+by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
by (TRY(
(rtac conjI 1) THEN
(* start states *)
@@ -236,12 +236,12 @@
by (rtac imp_conj_lemma 1);
by (Action.action.induct_tac "a" 1);
(* 7 cases *)
-by (ALLGOALS (simp_tac ((!simpset 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_ref_map (%id. id) env_ioa env_ioa";
-by (simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
+by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
by (TRY(
(rtac conjI 1) THEN
(* start states *)
@@ -251,11 +251,11 @@
by (rtac imp_conj_lemma 1);
by (Action.action.induct_tac "a" 1);
(* 7 cases *)
-by (ALLGOALS (simp_tac ((!simpset 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 "compatible srch_ioa rsch_ioa";
-by (simp_tac (!simpset addsimps [compatible_def,Int_def,empty_def]) 1);
+by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1);
by (rtac set_ext 1);
by (Action.action.induct_tac "x" 1);
by (ALLGOALS(Simp_tac));
@@ -263,14 +263,14 @@
(* totally the same as before *)
goal Correctness.thy "compatible srch_fin_ioa rsch_fin_ioa";
-by (simp_tac (!simpset addsimps [compatible_def,Int_def,empty_def]) 1);
+by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1);
by (rtac set_ext 1);
by (Action.action.induct_tac "x" 1);
by (ALLGOALS(Simp_tac));
val compat_single_fin_ch = result();
val ss =
- !simpset delsimps ([trans_of_def, srch_asig_def,rsch_asig_def,
+ 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,
@@ -336,7 +336,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 (!simpset addsimps [externals_def]) 1);
+ by (simp_tac (simpset() addsimps [externals_def]) 1);
val ext_single_ch = result();
@@ -354,7 +354,7 @@
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,
+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);
--- a/src/HOLCF/IOA/ABP/Lemmas.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/ABP/Lemmas.ML Mon Nov 03 14:06:27 1997 +0100
@@ -8,7 +8,7 @@
(* Logic *)
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
- by(fast_tac (!claset addDs prems) 1);
+ by(fast_tac (claset() addDs prems) 1);
qed "imp_conj_lemma";
goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)";
@@ -42,7 +42,7 @@
(* Lists *)
-val list_ss = simpset_of "List";
+val list_ss = simpset_of List.thy;
goal List.thy "hd(l@m) = (if l~=[] then hd(l) else hd(m))";
by (List.list.induct_tac "l" 1);
--- a/src/HOLCF/IOA/NTP/Abschannel.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/NTP/Abschannel.ML Mon Nov 03 14:06:27 1997 +0100
@@ -25,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 (!simpset addsimps unfold_renaming) 1);
+by(simp_tac (simpset() addsimps unfold_renaming) 1);
qed"in_srch_asig";
goal Abschannel.thy
@@ -40,20 +40,20 @@
\ C_r_s ~: actions(rsch_asig) & \
\ C_r_r(m) ~: actions(rsch_asig)";
-by(simp_tac (!simpset addsimps unfold_renaming) 1);
+by(simp_tac (simpset() addsimps unfold_renaming) 1);
qed"in_rsch_asig";
goal Abschannel.thy "srch_ioa = \
\ (srch_asig, {{|}}, srch_trans,srch_wfair,srch_sfair)";
-by (simp_tac (!simpset addsimps [srch_asig_def,srch_trans_def, asig_of_def, trans_of_def,
+by (simp_tac (simpset() addsimps [srch_asig_def,srch_trans_def, asig_of_def, trans_of_def,
wfair_of_def, sfair_of_def,srch_wfair_def,srch_sfair_def]) 1);
-by(simp_tac (!simpset addsimps unfold_renaming) 1);
+by(simp_tac (simpset() addsimps unfold_renaming) 1);
qed"srch_ioa_thm";
goal Abschannel.thy "rsch_ioa = \
\ (rsch_asig, {{|}}, rsch_trans,rsch_wfair,rsch_sfair)";
-by (simp_tac (!simpset addsimps [rsch_asig_def,rsch_trans_def, asig_of_def, trans_of_def,
+by (simp_tac (simpset() addsimps [rsch_asig_def,rsch_trans_def, asig_of_def, trans_of_def,
wfair_of_def, sfair_of_def,rsch_wfair_def,rsch_sfair_def]) 1);
-by(simp_tac (!simpset addsimps unfold_renaming) 1);
+by(simp_tac (simpset() addsimps unfold_renaming) 1);
qed"rsch_ioa_thm";
--- a/src/HOLCF/IOA/NTP/Correctness.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/NTP/Correctness.ML Mon Nov 03 14:06:27 1997 +0100
@@ -15,11 +15,11 @@
val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def,
Abschannel.srch_asig_def,Abschannel.rsch_asig_def];
-(* Two simpsets: - !simpset is basic, ss' unfolds hom_ioas *)
+(* Two simpsets: - simpset() is basic, ss' unfolds hom_ioas *)
Delsimps [split_paired_All];
-val ss' = (!simpset addsimps hom_ioas);
+val ss' = (simpset() addsimps hom_ioas);
(* A lemma about restricting the action signature of the implementation
@@ -38,22 +38,22 @@
\ | C_m_r => False \
\ | C_r_s => False \
\ | C_r_r(m) => False)";
- by (simp_tac (!simpset addsimps ([externals_def, restrict_def,
+ by (simp_tac (simpset() addsimps ([externals_def, restrict_def,
restrict_asig_def, Spec.sig_def]
@asig_projections)) 1);
by (Action.action.induct_tac "a" 1);
- by (ALLGOALS(simp_tac (!simpset addsimps [actions_def]@asig_projections)));
+ by (ALLGOALS(simp_tac (simpset() addsimps [actions_def]@asig_projections)));
(* 2 *)
- by (simp_tac (!simpset addsimps impl_ioas) 1);
- by (simp_tac (!simpset addsimps impl_asigs) 1);
- by (simp_tac (!simpset addsimps
+ by (simp_tac (simpset() addsimps impl_ioas) 1);
+ by (simp_tac (simpset() addsimps impl_asigs) 1);
+ by (simp_tac (simpset() addsimps
[asig_of_par, asig_comp_def]@asig_projections) 1);
by (simp_tac rename_ss 1);
(* 1 *)
- by (simp_tac (!simpset addsimps impl_ioas) 1);
- by (simp_tac (!simpset addsimps impl_asigs) 1);
- by (simp_tac (!simpset addsimps
+ by (simp_tac (simpset() addsimps impl_ioas) 1);
+ by (simp_tac (simpset() addsimps impl_asigs) 1);
+ by (simp_tac (simpset() addsimps
[asig_of_par, asig_comp_def]@asig_projections) 1);
qed "externals_lemma";
@@ -66,18 +66,18 @@
(* Proof of correctness *)
goalw Correctness.thy [Spec.ioa_def, is_weak_ref_map_def]
"is_weak_ref_map hom (restrict impl_ioa (externals spec_sig)) spec_ioa";
-by (simp_tac (!simpset addsimps
+by (simp_tac (simpset() addsimps
[Correctness.hom_def, cancel_restrict, externals_lemma]) 1);
by (rtac conjI 1);
by (simp_tac ss' 1);
-by (asm_simp_tac (!simpset addsimps sels) 1);
+by (asm_simp_tac (simpset() addsimps sels) 1);
by (REPEAT(rtac allI 1));
by (rtac imp_conj_lemma 1); (* from lemmas.ML *)
by (Action.action.induct_tac "a" 1);
by (asm_simp_tac (ss' setloop (split_tac [expand_if])) 1);
by (forward_tac [inv4] 1);
-by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
+by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
by (simp_tac ss' 1);
by (simp_tac ss' 1);
by (simp_tac ss' 1);
@@ -91,7 +91,7 @@
by (forward_tac [inv2] 1);
by (etac disjE 1);
by (Asm_simp_tac 1);
-by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
+by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
by (asm_simp_tac ss' 1);
by (forward_tac [inv2] 1);
@@ -101,14 +101,14 @@
by (case_tac "sq(sen(s))=[]" 1);
by (asm_full_simp_tac ss' 1);
-by (fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
+by (fast_tac (claset() addSDs [add_leD1 RS leD]) 1);
by (case_tac "m = hd(sq(sen(s)))" 1);
-by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
+by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
by (Asm_full_simp_tac 1);
-by (fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
+by (fast_tac (claset() addSDs [add_leD1 RS leD]) 1);
by (Asm_full_simp_tac 1);
qed"ntp_correct";
--- a/src/HOLCF/IOA/NTP/Impl.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/NTP/Impl.ML Mon Nov 03 14:06:27 1997 +0100
@@ -33,7 +33,7 @@
\ fst(snd(x)) = rec(x) & \
\ fst(snd(snd(x))) = srch(x) & \
\ snd(snd(snd(x))) = rsch(x)";
-by(simp_tac (!simpset addsimps
+by(simp_tac (simpset() addsimps
[sen_def,rec_def,srch_def,rsch_def]) 1);
Addsimps [result()];
@@ -51,12 +51,12 @@
(* Three Simp_sets in different sizes
----------------------------------------------
-1) !simpset does not unfold the transition relations
+1) simpset() does not unfold the transition relations
2) ss unfolds transition relations
3) renname_ss unfolds transitions and the abstract channel *)
-val ss = (!simpset addcongs [if_weak_cong]
+val ss = (simpset() addcongs [if_weak_cong]
addsimps transitions);
val rename_ss = (ss addsimps unfold_renaming);
@@ -73,18 +73,18 @@
goalw Impl.thy impl_ioas "invariant impl_ioa inv1";
by (rtac invariantI 1);
-by(asm_full_simp_tac (!simpset
+by(asm_full_simp_tac (simpset()
addsimps [inv1_def, hdr_sum_def, Sender.srcvd_def,
Sender.ssent_def, Receiver.rsent_def,Receiver.rrcvd_def]) 1);
-by(simp_tac (!simpset delsimps [trans_of_par4]
+by(simp_tac (simpset() delsimps [trans_of_par4]
addsimps [fork_lemma,inv1_def]) 1);
(* Split proof in two *)
by (rtac conjI 1);
(* First half *)
-by(asm_full_simp_tac (!simpset addsimps [Impl.inv1_def]) 1);
+by(asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]) 1);
by (rtac Action.action.induct 1);
by (EVERY1[tac, tac, tac, tac]);
@@ -101,7 +101,7 @@
(* Now the other half *)
-by(asm_full_simp_tac (!simpset addsimps [Impl.inv1_def]) 1);
+by(asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]) 1);
by (rtac Action.action.induct 1);
by(EVERY1[tac, tac]);
@@ -110,7 +110,7 @@
by (tac_ren 1);
by (rtac impI 1);
by (REPEAT (etac conjE 1));
-by (asm_simp_tac (!simpset addsimps [hdr_sum_def, Multiset.count_def,
+by (asm_simp_tac (simpset() addsimps [hdr_sum_def, Multiset.count_def,
Multiset.countm_nonempty_def]
setloop (split_tac [expand_if])) 1);
(* detour 2 *)
@@ -118,7 +118,7 @@
by (tac_ren 1);
by (rtac impI 1);
by (REPEAT (etac conjE 1));
-by (asm_full_simp_tac (!simpset addsimps [Impl.hdr_sum_def,
+by (asm_full_simp_tac (simpset() addsimps [Impl.hdr_sum_def,
Multiset.count_def,
Multiset.countm_nonempty_def,
Multiset.delm_nonempty_def,
@@ -139,10 +139,10 @@
by (rtac (countm_done_delm RS mp RS sym) 1);
by (rtac refl 1);
-by (asm_simp_tac (!simpset addsimps [Multiset.count_def]) 1);
+by (asm_simp_tac (simpset() addsimps [Multiset.count_def]) 1);
by (rtac impI 1);
-by (asm_full_simp_tac (!simpset addsimps [neg_flip]) 1);
+by (asm_full_simp_tac (simpset() addsimps [neg_flip]) 1);
by (hyp_subst_tac 1);
by (rtac countm_spurious_delm 1);
by (Simp_tac 1);
@@ -159,12 +159,12 @@
by (rtac invariantI1 1);
(* Base case *)
- by (asm_full_simp_tac (!simpset addsimps (inv2_def ::
+ by (asm_full_simp_tac (simpset() addsimps (inv2_def ::
(receiver_projections
@ sender_projections @ impl_ioas)))
1);
- by (asm_simp_tac (!simpset addsimps impl_ioas) 1);
+ by (asm_simp_tac (simpset() addsimps impl_ioas) 1);
by (Action.action.induct_tac "a" 1);
(* 10 cases. First 4 are simple, since state doesn't change *)
@@ -183,14 +183,14 @@
by (forward_tac [rewrite_rule [Impl.inv1_def]
(inv1 RS invariantE) RS conjunct1] 1);
by (tac2 1);
- by (fast_tac (!claset addDs [add_leD1,leD]) 1);
+ by (fast_tac (claset() addDs [add_leD1,leD]) 1);
(* 3 *)
by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1);
by (tac2 1);
by (fold_tac [rewrite_rule [Packet.hdr_def]Impl.hdr_sum_def]);
- by (fast_tac (!claset addDs [add_leD1,leD]) 1);
+ by (fast_tac (claset() addDs [add_leD1,leD]) 1);
(* 2 *)
by (tac2 1);
@@ -223,11 +223,11 @@
by (rtac invariantI 1);
(* Base case *)
- by (asm_full_simp_tac (!simpset addsimps
+ by (asm_full_simp_tac (simpset() addsimps
(Impl.inv3_def :: (receiver_projections
@ sender_projections @ impl_ioas))) 1);
- by (asm_simp_tac (!simpset addsimps impl_ioas) 1);
+ by (asm_simp_tac (simpset() addsimps impl_ioas) 1);
by (Action.action.induct_tac "a" 1);
val tac3 = asm_full_simp_tac (ss addsimps [inv3_def]
@@ -254,7 +254,7 @@
(* 2 *)
by (asm_full_simp_tac ss 1);
- by (simp_tac (!simpset addsimps [inv3_def]) 1);
+ by (simp_tac (simpset() addsimps [inv3_def]) 1);
by (strip_tac 1 THEN REPEAT (etac conjE 1));
by (rtac (imp_or_lem RS iffD2) 1);
by (rtac impI 1);
@@ -265,7 +265,7 @@
("k","count (rsent(rec s)) (sbit(sen s))")] le_trans 1);
by (forward_tac [rewrite_rule [inv1_def]
(inv1 RS invariantE) RS conjunct2] 1);
- by (asm_full_simp_tac (!simpset addsimps
+ by (asm_full_simp_tac (simpset() addsimps
[hdr_sum_def, Multiset.count_def]) 1);
by (rtac (less_eq_add_cong RS mp RS mp) 1);
by (rtac countm_props 1);
@@ -298,11 +298,11 @@
by (rtac invariantI 1);
(* Base case *)
- by (asm_full_simp_tac (!simpset addsimps
+ by (asm_full_simp_tac (simpset() addsimps
(Impl.inv4_def :: (receiver_projections
@ sender_projections @ impl_ioas))) 1);
- by (asm_simp_tac (!simpset addsimps impl_ioas) 1);
+ by (asm_simp_tac (simpset() addsimps impl_ioas) 1);
by (Action.action.induct_tac "a" 1);
val tac4 = asm_full_simp_tac (ss addsimps [inv4_def]
--- a/src/HOLCF/IOA/NTP/Lemmas.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/NTP/Lemmas.ML Mon Nov 03 14:06:27 1997 +0100
@@ -10,7 +10,7 @@
(* Logic *)
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
- by(fast_tac (!claset addDs prems) 1);
+ by(fast_tac (claset() addDs prems) 1);
qed "imp_conj_lemma";
goal HOL.thy "(P --> (? x. Q(x))) = (? x. P --> Q(x))";
@@ -113,8 +113,8 @@
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 (!simpset addsimps [le_eq_less_or_eq]) 1);
- by (safe_tac (!claset));
+ by (asm_full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
+ by (safe_tac (claset()));
by (rtac (less_add_cong RS mp RS mp) 1);
by (assume_tac 1);
by (assume_tac 1);
@@ -131,7 +131,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 (!simpset 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);
@@ -147,10 +147,10 @@
goal Arith.thy "Suc(x) <= y --> (? z. y = Suc(z))";
by (rtac impI 1);
- by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
- by (safe_tac (!claset));
+ by (asm_full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
+ by (safe_tac (claset()));
by (Fast_tac 2);
- by (asm_simp_tac (!simpset addsimps [suc_not_zero]) 1);
+ by (asm_simp_tac (simpset() addsimps [suc_not_zero]) 1);
qed "suc_leq_suc";
goal Arith.thy "~0<n --> n = 0";
@@ -160,8 +160,8 @@
goal Arith.thy "x < Suc(y) --> x<=y";
by (nat_ind_tac "n" 1);
- by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
- by (safe_tac (!claset));
+ by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
+ by (safe_tac (claset()));
by (etac less_imp_le 1);
qed "less_suc_imp_leq";
@@ -187,12 +187,12 @@
goal Arith.thy "((x::nat) = y + z) --> (y <= x)";
by (nat_ind_tac "y" 1);
by (Simp_tac 1);
- by (simp_tac (!simpset addsimps [le_refl RS (leq_add_leq RS mp)]) 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";
+val list_ss = simpset_of List.thy;
goal List.thy "(xs @ (y#ys)) ~= []";
by (list.induct_tac "xs" 1);
--- a/src/HOLCF/IOA/NTP/Multiset.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/NTP/Multiset.ML Mon Nov 03 14:06:27 1997 +0100
@@ -14,44 +14,44 @@
goal Multiset.thy
"count (addm M x) y = (if y=x then Suc(count M y) else count M y)";
- by (asm_simp_tac (!simpset 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 (!simpset addsimps [count_addm_simp]
+ by (simp_tac (simpset() addsimps [count_addm_simp]
setloop (split_tac [expand_if])) 1);
qed "count_leq_addm";
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 (!simpset
+ 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 (!simpset
+ by (asm_full_simp_tac (simpset()
addsimps [Multiset.delm_nonempty_def,
Multiset.countm_nonempty_def]
setloop (split_tac [expand_if])) 1);
- by (safe_tac (!claset));
+ by (safe_tac (claset()));
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 (!simpset addsimps [Multiset.countm_empty_def]) 1);
- by (simp_tac (!simpset 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 (!simpset 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 (!simpset addsimps [Multiset.delm_empty_def,
+ by (simp_tac (simpset() addsimps [Multiset.delm_empty_def,
Multiset.countm_empty_def]) 1);
- by (asm_simp_tac (!simpset 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";
@@ -59,10 +59,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 (!simpset addsimps
+ by (simp_tac (simpset() addsimps
[Multiset.delm_empty_def,Multiset.count_def,
Multiset.countm_empty_def]) 1);
- by (asm_simp_tac (!simpset addsimps
+ by (asm_simp_tac (simpset() addsimps
[Multiset.count_def,Multiset.delm_nonempty_def,
Multiset.countm_nonempty_def]
setloop (split_tac [expand_if])) 1);
@@ -71,10 +71,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 (!simpset addsimps
+ by (simp_tac (simpset() addsimps
[Multiset.delm_empty_def,
Multiset.countm_empty_def]) 1);
- by (asm_simp_tac (!simpset 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/HOLCF/IOA/NTP/Packet.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/NTP/Packet.ML Mon Nov 03 14:06:27 1997 +0100
@@ -9,7 +9,7 @@
(* Instantiation of a tautology? *)
goal Packet.thy "!x. x = packet --> hdr(x) = hdr(packet)";
- by (simp_tac (!simpset addsimps [Packet.hdr_def]) 1);
+ by (simp_tac (simpset() addsimps [Packet.hdr_def]) 1);
qed "eq_packet_imp_eq_hdr";
Addsimps [Packet.hdr_def,Packet.msg_def];
--- a/src/HOLCF/IOA/NTP/Receiver.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/NTP/Receiver.ML Mon Nov 03 14:06:27 1997 +0100
@@ -15,7 +15,7 @@
\ C_m_r : actions(receiver_asig) & \
\ C_r_s ~: actions(receiver_asig) & \
\ C_r_r(m) : actions(receiver_asig)";
- by(simp_tac (!simpset addsimps (Receiver.receiver_asig_def :: actions_def ::
+ by(simp_tac (simpset() addsimps (Receiver.receiver_asig_def :: actions_def ::
asig_projections)) 1);
qed "in_receiver_asig";
--- a/src/HOLCF/IOA/NTP/Sender.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/NTP/Sender.ML Mon Nov 03 14:06:27 1997 +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 (!simpset addsimps
+by(simp_tac (simpset() addsimps
(Sender.sender_asig_def :: actions_def ::
asig_projections)) 1);
qed "in_sender_asig";
--- a/src/HOLCF/IOA/meta_theory/Asig.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Asig.ML Mon Nov 03 14:06:27 1997 +0100
@@ -14,40 +14,40 @@
"(outputs (a,b,c) = b) & \
\ (inputs (a,b,c) = a) & \
\ (internals (a,b,c) = c)";
- by (simp_tac (!simpset addsimps asig_projections) 1);
+ by (simp_tac (simpset() addsimps asig_projections) 1);
qed "asig_triple_proj";
goal thy "!!a.[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
-by (asm_full_simp_tac (!simpset 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 thy "!!a.[|a:externals(S)|] ==> a:actions(S)";
-by (asm_full_simp_tac (!simpset addsimps [externals_def,actions_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
qed"ext_is_act";
goal thy "!!a.[|a:internals S|] ==> a:actions S";
-by (asm_full_simp_tac (!simpset addsimps [asig_internals_def,actions_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [asig_internals_def,actions_def]) 1);
qed"int_is_act";
goal thy "!!a.[|a:inputs S|] ==> a:actions S";
-by (asm_full_simp_tac (!simpset addsimps [asig_inputs_def,actions_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [asig_inputs_def,actions_def]) 1);
qed"inp_is_act";
goal thy "!!a.[|a:outputs S|] ==> a:actions S";
-by (asm_full_simp_tac (!simpset addsimps [asig_outputs_def,actions_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [asig_outputs_def,actions_def]) 1);
qed"out_is_act";
goal thy "(x: actions S & x : externals S) = (x: externals S)";
-by (fast_tac (!claset addSIs [ext_is_act]) 1 );
+by (fast_tac (claset() addSIs [ext_is_act]) 1 );
qed"ext_and_act";
goal thy "!!S. [|is_asig S;x: actions S|] ==> (x~:externals S) = (x: internals S)";
-by (asm_full_simp_tac (!simpset addsimps [actions_def,is_asig_def,externals_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [actions_def,is_asig_def,externals_def]) 1);
by (best_tac (set_cs addEs [equalityCE]) 1);
qed"not_ext_is_int";
goal thy "!!S. is_asig S ==> (x~:externals S) = (x: internals S | x~:actions S)";
-by (asm_full_simp_tac (!simpset addsimps [actions_def,is_asig_def,externals_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [actions_def,is_asig_def,externals_def]) 1);
by (best_tac (set_cs addEs [equalityCE]) 1);
qed"not_ext_is_int_or_not_act";
--- a/src/HOLCF/IOA/meta_theory/Automata.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML Mon Nov 03 14:06:27 1997 +0100
@@ -24,7 +24,7 @@
\ ((trans_of (x,y,z,w,s)) = z) & \
\ ((wfair_of (x,y,z,w,s)) = w) & \
\ ((sfair_of (x,y,z,w,s)) = s)";
- by (simp_tac (!simpset addsimps ioa_projections) 1);
+ by (simp_tac (simpset() addsimps ioa_projections) 1);
qed "ioa_triple_proj";
goalw thy [is_trans_of_def,actions_def, is_asig_def]
@@ -36,7 +36,7 @@
goal thy
"starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}";
- by (simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
+ by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1);
qed "starts_of_par";
goal thy
@@ -50,7 +50,7 @@
\ (snd(s),a,snd(t)):trans_of(B) \
\ else snd(t) = snd(s))}";
-by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
+by(simp_tac (simpset() addsimps (par_def::ioa_projections)) 1);
qed "trans_of_par";
@@ -61,20 +61,20 @@
goal thy
"actions(asig_comp a b) = actions(a) Un actions(b)";
- by (simp_tac (!simpset addsimps
+ by (simp_tac (simpset() addsimps
([actions_def,asig_comp_def]@asig_projections)) 1);
by (fast_tac (set_cs addSIs [equalityI]) 1);
qed "actions_asig_comp";
goal thy "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)";
- by (simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
+ by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1);
qed "asig_of_par";
goal thy "ext (A1||A2) = \
\ (ext A1) Un (ext A2)";
-by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_of_par,asig_comp_def,
+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);
@@ -82,7 +82,7 @@
goal thy "act (A1||A2) = \
\ (act A1) Un (act A2)";
-by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def,
+by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def,
asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1);
by (rtac set_ext 1);
by (fast_tac set_cs 1);
@@ -90,19 +90,19 @@
goal thy "inp (A1||A2) =\
\ ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))";
-by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def,
+by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def,
asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1);
qed"inputs_of_par";
goal thy "out (A1||A2) =\
\ (out A1) Un (out A2)";
-by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def,
+by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def,
asig_outputs_def,Un_def,set_diff_def]) 1);
qed"outputs_of_par";
goal thy "int (A1||A2) =\
\ (int A1) Un (int A2)";
-by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def,
+by (asm_full_simp_tac (simpset() addsimps [actions_def,asig_of_par,asig_comp_def,
asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1);
qed"internals_of_par";
@@ -111,7 +111,7 @@
section "actions and compatibility";
goal thy"compatible A B = compatible B A";
-by (asm_full_simp_tac (!simpset addsimps [compatible_def,Int_commute]) 1);
+by (asm_full_simp_tac (simpset() addsimps [compatible_def,Int_commute]) 1);
by (Auto_tac());
qed"compat_commute";
@@ -170,10 +170,10 @@
goalw thy [input_enabled_def]
"!!A. [| compatible A B; input_enabled A; input_enabled B|] \
\ ==> input_enabled (A||B)";
-by (asm_full_simp_tac (!simpset addsimps [inputs_of_par,trans_of_par]) 1);
+by (asm_full_simp_tac (simpset() addsimps [inputs_of_par,trans_of_par]) 1);
by (safe_tac set_cs);
-by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
-by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 2);
+by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
+by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 2);
(* a: inp A *)
by (case_tac "a:act B" 1);
(* a:act B *)
@@ -189,9 +189,9 @@
be exE 1;
be exE 1;
by (res_inst_tac [("x","(s2,s2a)")] exI 1);
-by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
+by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
(* a~: act B*)
-by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
+by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
by (eres_inst_tac [("x","a")] allE 1);
by (Asm_full_simp_tac 1);
by (eres_inst_tac [("x","aa")] allE 1);
@@ -204,7 +204,7 @@
(* a:act A *)
by (eres_inst_tac [("x","a")] allE 1);
by (eres_inst_tac [("x","a")] allE 1);
-by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
+by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1);
bd inpAAactB_is_inpBoroutB 1;
back();
@@ -218,9 +218,9 @@
be exE 1;
be exE 1;
by (res_inst_tac [("x","(s2,s2a)")] exI 1);
-by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
+by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
(* a~: act B*)
-by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
+by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
by (eres_inst_tac [("x","a")] allE 1);
by (Asm_full_simp_tac 1);
by (eres_inst_tac [("x","a")] allE 1);
@@ -268,25 +268,25 @@
goal thy "starts_of(restrict ioa acts) = starts_of(ioa) & \
\ trans_of(restrict ioa acts) = trans_of(ioa)";
-by (simp_tac (!simpset addsimps ([restrict_def]@ioa_projections)) 1);
+by (simp_tac (simpset() addsimps ([restrict_def]@ioa_projections)) 1);
qed "cancel_restrict_a";
goal thy "reachable (restrict ioa acts) s = reachable ioa s";
by (rtac iffI 1);
by (etac reachable.induct 1);
-by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a,reachable_0]) 1);
+by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a,reachable_0]) 1);
by (etac reachable_n 1);
-by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
+by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a]) 1);
(* <-- *)
by (etac reachable.induct 1);
by (rtac reachable_0 1);
-by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
+by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a]) 1);
by (etac reachable_n 1);
-by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
+by (asm_full_simp_tac (simpset() addsimps [cancel_restrict_a]) 1);
qed "cancel_restrict_b";
goal thy "act (restrict A acts) = act A";
-by (simp_tac (!simpset addsimps [actions_def,asig_internals_def,
+by (simp_tac (simpset() addsimps [actions_def,asig_internals_def,
asig_outputs_def,asig_inputs_def,externals_def,asig_of_def,restrict_def,
restrict_asig_def]) 1);
auto();
@@ -296,7 +296,7 @@
\ trans_of(restrict ioa acts) = trans_of(ioa) & \
\ reachable (restrict ioa acts) s = reachable ioa s & \
\ act (restrict A acts) = act A";
- by (simp_tac (!simpset addsimps [cancel_restrict_a,cancel_restrict_b,acts_restrict]) 1);
+ by (simp_tac (simpset() addsimps [cancel_restrict_a,cancel_restrict_b,acts_restrict]) 1);
qed"cancel_restrict";
(* ---------------------------------------------------------------------------------- *)
@@ -306,14 +306,14 @@
goal thy "!!f. s -a--(rename C f)-> t ==> (? x. Some(x) = f(a) & s -x--C-> t)";
-by (asm_full_simp_tac (!simpset addsimps [Let_def,rename_def,trans_of_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Let_def,rename_def,trans_of_def]) 1);
qed"trans_rename";
goal thy "!!s.[| reachable (rename C g) s |] ==> reachable C s";
by (etac reachable.induct 1);
by (rtac reachable_0 1);
-by (asm_full_simp_tac (!simpset addsimps [rename_def]@ioa_projections) 1);
+by (asm_full_simp_tac (simpset() addsimps [rename_def]@ioa_projections) 1);
by (dtac trans_rename 1);
by (etac exE 1);
by (etac conjE 1);
@@ -330,45 +330,45 @@
goal thy "!!A.[|(s,a,t):trans_of (A||B); a:act A|] \
\ ==> (fst s,a,fst t):trans_of A";
-by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
qed"trans_A_proj";
goal thy "!!A.[|(s,a,t):trans_of (A||B); a:act B|] \
\ ==> (snd s,a,snd t):trans_of B";
-by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
qed"trans_B_proj";
goal thy "!!A.[|(s,a,t):trans_of (A||B); a~:act A|]\
\ ==> fst s = fst t";
-by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
qed"trans_A_proj2";
goal thy "!!A.[|(s,a,t):trans_of (A||B); a~:act B|]\
\ ==> snd s = snd t";
-by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
qed"trans_B_proj2";
goal thy "!!A.(s,a,t):trans_of (A||B) \
\ ==> a :act A | a :act B";
-by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
qed"trans_AB_proj";
goal thy "!!A. [|a:act A;a:act B;\
\ (fst s,a,fst t):trans_of A;(snd s,a,snd t):trans_of B|]\
\ ==> (s,a,t):trans_of (A||B)";
-by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
qed"trans_AB";
goal thy "!!A. [|a:act A;a~:act B;\
\ (fst s,a,fst t):trans_of A;snd s=snd t|]\
\ ==> (s,a,t):trans_of (A||B)";
-by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
qed"trans_A_notB";
goal thy "!!A. [|a~:act A;a:act B;\
\ (snd s,a,snd t):trans_of B;fst s=fst t|]\
\ ==> (s,a,t):trans_of (A||B)";
-by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Let_def,par_def,trans_of_def]) 1);
qed"trans_notA_B";
val trans_of_defs1 = [trans_AB,trans_A_notB,trans_notA_B];
@@ -391,7 +391,7 @@
\ (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D) \
\ else snd(snd(snd(t)))=snd(snd(snd(s)))))";
- by (simp_tac (!simpset addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq,Let_def]@
+ by (simp_tac (simpset() addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq,Let_def]@
ioa_projections)
setloop (split_tac [expand_if])) 1);
qed "trans_of_par4";
@@ -404,17 +404,17 @@
(* without assumptions on A and B because is_trans_of is also incorporated in ||def *)
goalw thy [is_trans_of_def]
"is_trans_of (A||B)";
-by (simp_tac (!simpset addsimps [actions_of_par,trans_of_par]) 1);
+by (simp_tac (simpset() addsimps [actions_of_par,trans_of_par]) 1);
qed"is_trans_of_par";
goalw thy [is_trans_of_def]
"!!A. is_trans_of A ==> is_trans_of (restrict A acts)";
-by (asm_simp_tac (!simpset addsimps [cancel_restrict,acts_restrict])1);
+by (asm_simp_tac (simpset() addsimps [cancel_restrict,acts_restrict])1);
qed"is_trans_of_restrict";
goalw thy [is_trans_of_def,restrict_def,restrict_asig_def]
"!!A. is_trans_of A ==> is_trans_of (rename A f)";
-by (asm_full_simp_tac (!simpset addsimps [actions_def,trans_of_def,
+by (asm_full_simp_tac (simpset() addsimps [actions_def,trans_of_def,
asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,
asig_of_def,rename_def,rename_set_def]) 1);
auto();
@@ -422,10 +422,10 @@
goal thy "!! A. [| is_asig_of A; is_asig_of B; compatible A B|] \
\ ==> is_asig_of (A||B)";
-by (asm_full_simp_tac (!simpset addsimps [is_asig_of_def,asig_of_par,
+by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,asig_of_par,
asig_comp_def,compatible_def,asig_internals_def,asig_outputs_def,
asig_inputs_def,actions_def,is_asig_def]) 1);
-by (asm_full_simp_tac (!simpset addsimps [asig_of_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [asig_of_def]) 1);
auto();
by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
qed"is_asig_of_par";
@@ -439,7 +439,7 @@
qed"is_asig_of_restrict";
goal thy "!! A. is_asig_of A ==> is_asig_of (rename A f)";
-by (asm_full_simp_tac (!simpset addsimps [is_asig_of_def,
+by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,
rename_def,rename_set_def,asig_internals_def,asig_outputs_def,
asig_inputs_def,actions_def,is_asig_def,asig_of_def]) 1);
auto();
@@ -464,7 +464,7 @@
goalw thy [compatible_def]
"!! A. [|compatible A B; compatible A C |]==> compatible A (B||C)";
-by (asm_full_simp_tac (!simpset addsimps [internals_of_par,
+by (asm_full_simp_tac (simpset() addsimps [internals_of_par,
outputs_of_par,actions_of_par]) 1);
auto();
by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
@@ -473,7 +473,7 @@
(* FIX: better derive by previous one and compat_commute *)
goalw thy [compatible_def]
"!! A. [|compatible A C; compatible B C |]==> compatible (A||B) C";
-by (asm_full_simp_tac (!simpset addsimps [internals_of_par,
+by (asm_full_simp_tac (simpset() addsimps [internals_of_par,
outputs_of_par,actions_of_par]) 1);
auto();
by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
@@ -482,8 +482,8 @@
goalw thy [compatible_def]
"!! A. [| compatible A B; (ext B - S) Int ext A = {}|] \
\ ==> compatible A (restrict B S)";
-by (asm_full_simp_tac (!simpset addsimps [ioa_triple_proj,asig_triple_proj,
+by (asm_full_simp_tac (simpset() addsimps [ioa_triple_proj,asig_triple_proj,
externals_def,restrict_def,restrict_asig_def,actions_def]) 1);
-by (auto_tac (!claset addEs [equalityCE],!simpset));
+by (auto_tac (claset() addEs [equalityCE],simpset()));
qed"compatible_restrict";
\ No newline at end of file
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML Mon Nov 03 14:06:27 1997 +0100
@@ -21,15 +21,15 @@
goal thy "ProjA2`UU = UU";
-by (simp_tac (!simpset addsimps [ProjA2_def]) 1);
+by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
qed"ProjA2_UU";
goal thy "ProjA2`nil = nil";
-by (simp_tac (!simpset addsimps [ProjA2_def]) 1);
+by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
qed"ProjA2_nil";
goal thy "ProjA2`((a,t)>>xs) = (a,fst t) >> ProjA2`xs";
-by (simp_tac (!simpset addsimps [ProjA2_def]) 1);
+by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
qed"ProjA2_cons";
@@ -39,15 +39,15 @@
goal thy "ProjB2`UU = UU";
-by (simp_tac (!simpset addsimps [ProjB2_def]) 1);
+by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
qed"ProjB2_UU";
goal thy "ProjB2`nil = nil";
-by (simp_tac (!simpset addsimps [ProjB2_def]) 1);
+by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
qed"ProjB2_nil";
goal thy "ProjB2`((a,t)>>xs) = (a,snd t) >> ProjB2`xs";
-by (simp_tac (!simpset addsimps [ProjB2_def]) 1);
+by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
qed"ProjB2_cons";
@@ -58,11 +58,11 @@
goal thy "Filter_ex2 sig`UU=UU";
-by (simp_tac (!simpset addsimps [Filter_ex2_def]) 1);
+by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
qed"Filter_ex2_UU";
goal thy "Filter_ex2 sig`nil=nil";
-by (simp_tac (!simpset addsimps [Filter_ex2_def]) 1);
+by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
qed"Filter_ex2_nil";
goal thy "Filter_ex2 sig`(at >> xs) = \
@@ -70,7 +70,7 @@
\ then at >> (Filter_ex2 sig`xs) \
\ else Filter_ex2 sig`xs)";
-by (asm_full_simp_tac (!simpset addsimps [Filter_ex2_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
qed"Filter_ex2_cons";
@@ -92,7 +92,7 @@
by (rtac fix_eq2 1);
by (rtac stutter2_def 1);
by (rtac beta_cfun 1);
-by (simp_tac (!simpset addsimps [flift1_def]) 1);
+by (simp_tac (simpset() addsimps [flift1_def]) 1);
qed"stutter2_unfold";
goal thy "(stutter2 sig`UU) s=UU";
@@ -110,7 +110,7 @@
\ andalso (stutter2 sig`xs) (snd at))";
br trans 1;
by (stac stutter2_unfold 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def,If_and_if]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def,If_and_if]) 1);
by (Simp_tac 1);
qed"stutter2_cons";
@@ -123,16 +123,16 @@
(* ---------------------------------------------------------------- *)
goal thy "stutter sig (s, UU)";
-by (simp_tac (!simpset addsimps [stutter_def]) 1);
+by (simp_tac (simpset() addsimps [stutter_def]) 1);
qed"stutter_UU";
goal thy "stutter sig (s, nil)";
-by (simp_tac (!simpset addsimps [stutter_def]) 1);
+by (simp_tac (simpset() addsimps [stutter_def]) 1);
qed"stutter_nil";
goal thy "stutter sig (s, (a,t)>>ex) = \
\ ((a~:actions sig --> (s=t)) & stutter sig (t,ex))";
-by (simp_tac (!simpset addsimps [stutter_def]
+by (simp_tac (simpset() addsimps [stutter_def]
setloop (split_tac [expand_if]) ) 1);
qed"stutter_cons";
@@ -167,7 +167,7 @@
(* main case *)
ren "ss a t" 1;
by (safe_tac set_cs);
-by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2
+by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2
setloop (split_tac [expand_if])) 1));
qed"lemma_1_1a";
@@ -183,7 +183,7 @@
by (pair_induct_tac "xs" [stutter_def,is_exec_frag_def] 1);
(* main case *)
by (safe_tac set_cs);
-by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2
+by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2
setloop (split_tac [expand_if])) 1));
qed"lemma_1_1b";
@@ -198,7 +198,7 @@
by (pair_induct_tac "xs" [Forall_def,sforall_def,is_exec_frag_def] 1);
(* main case *)
by (safe_tac set_cs);
-by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 @
+by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2 @
[actions_asig_comp,asig_of_par]) 1));
qed"lemma_1_1c";
@@ -220,14 +220,14 @@
(* main case *)
by (rtac allI 1);
ren "ss a t s" 1;
-by (asm_full_simp_tac (!simpset addsimps trans_of_defs1 @ [actions_asig_comp,asig_of_par]
+by (asm_full_simp_tac (simpset() addsimps trans_of_defs1 @ [actions_asig_comp,asig_of_par]
setloop (split_tac [expand_if])) 1);
by (safe_tac set_cs);
(* problem with asm_full_simp_tac: (fst s) = (fst t) is too high in assumption order ! *)
by (rotate_tac ~4 1);
-by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
by (rotate_tac ~4 1);
-by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
qed"lemma_1_2";
@@ -244,17 +244,17 @@
\ stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &\
\ Forall (%x. fst x:act (A||B)) (snd ex))";
-by (simp_tac (!simpset addsimps [executions_def,ProjB_def,
+by (simp_tac (simpset() addsimps [executions_def,ProjB_def,
Filter_ex_def,ProjA_def,starts_of_par]) 1);
by (pair_tac "ex" 1);
by (rtac iffI 1);
(* ==> *)
by (REPEAT (etac conjE 1));
-by (asm_full_simp_tac (!simpset addsimps [lemma_1_1a RS spec RS mp,
+by (asm_full_simp_tac (simpset() addsimps [lemma_1_1a RS spec RS mp,
lemma_1_1b RS spec RS mp,lemma_1_1c RS spec RS mp]) 1);
(* <== *)
by (REPEAT (etac conjE 1));
-by (asm_full_simp_tac (!simpset addsimps [lemma_1_2 RS spec RS mp]) 1);
+by (asm_full_simp_tac (simpset() addsimps [lemma_1_2 RS spec RS mp]) 1);
qed"compositionality_ex";
@@ -267,9 +267,9 @@
"Execs (A||B) = par_execs (Execs A) (Execs B)";
-by (asm_full_simp_tac (!simpset addsimps [asig_of_par]) 1);
+by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1);
br set_ext 1;
-by (asm_full_simp_tac (!simpset addsimps [compositionality_ex,actions_of_par]) 1);
+by (asm_full_simp_tac (simpset() addsimps [compositionality_ex,actions_of_par]) 1);
qed"compositionality_ex_modules";
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML Mon Nov 03 14:06:27 1997 +0100
@@ -71,8 +71,8 @@
\ (x,snd a,t) >> (mkex2 A B`sch`(TL`exA)`exB) (snd a) t";
by (rtac trans 1);
by (stac mkex2_unfold 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
qed"mkex2_cons_1";
goal thy "!!x.[| x~:act A; x:act B; HD`exB=Def b|] \
@@ -80,8 +80,8 @@
\ (x,s,snd b) >> (mkex2 A B`sch`exA`(TL`exB)) s (snd b)";
by (rtac trans 1);
by (stac mkex2_unfold 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
qed"mkex2_cons_2";
goal thy "!!x.[| x:act A; x:act B; HD`exA=Def a;HD`exB=Def b|] \
@@ -90,8 +90,8 @@
\ (mkex2 A B`sch`(TL`exA)`(TL`exB)) (snd a) (snd b)";
by (rtac trans 1);
by (stac mkex2_unfold 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
qed"mkex2_cons_3";
Addsimps [mkex2_UU,mkex2_nil,mkex2_cons_1,mkex2_cons_2,mkex2_cons_3];
@@ -102,17 +102,17 @@
(* ---------------------------------------------------------------- *)
goal thy "mkex A B UU (s,exA) (t,exB) = ((s,t),UU)";
-by (simp_tac (!simpset addsimps [mkex_def]) 1);
+by (simp_tac (simpset() addsimps [mkex_def]) 1);
qed"mkex_UU";
goal thy "mkex A B nil (s,exA) (t,exB) = ((s,t),nil)";
-by (simp_tac (!simpset addsimps [mkex_def]) 1);
+by (simp_tac (simpset() addsimps [mkex_def]) 1);
qed"mkex_nil";
goal thy "!!x.[| x:act A; x~:act B |] \
\ ==> mkex A B (x>>sch) (s,a>>exA) (t,exB) = \
\ ((s,t), (x,snd a,t) >> snd (mkex A B sch (snd a,exA) (t,exB)))";
-by (simp_tac (!simpset addsimps [mkex_def]
+by (simp_tac (simpset() addsimps [mkex_def]
setloop (split_tac [expand_if]) ) 1);
by (cut_inst_tac [("exA","a>>exA")] mkex2_cons_1 1);
by (Auto_tac());
@@ -121,7 +121,7 @@
goal thy "!!x.[| x~:act A; x:act B |] \
\ ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) = \
\ ((s,t), (x,s,snd b) >> snd (mkex A B sch (s,exA) (snd b,exB)))";
-by (simp_tac (!simpset addsimps [mkex_def]
+by (simp_tac (simpset() addsimps [mkex_def]
setloop (split_tac [expand_if]) ) 1);
by (cut_inst_tac [("exB","b>>exB")] mkex2_cons_2 1);
by (Auto_tac());
@@ -130,7 +130,7 @@
goal thy "!!x.[| x:act A; x:act B |] \
\ ==> mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) = \
\ ((s,t), (x,snd a,snd b) >> snd (mkex A B sch (snd a,exA) (snd b,exB)))";
-by (simp_tac (!simpset addsimps [mkex_def]
+by (simp_tac (simpset() addsimps [mkex_def]
setloop (split_tac [expand_if]) ) 1);
by (cut_inst_tac [("exB","b>>exB"),("exA","a>>exA")] mkex2_cons_3 1);
by (Auto_tac());
@@ -162,7 +162,7 @@
"filter_act`(Filter_ex2 (asig_of A)`xs)=\
\ Filter (%a. a:act A)`(filter_act`xs)";
-by (simp_tac (!simpset addsimps [MapFilter,o_def]) 1);
+by (simp_tac (simpset() addsimps [MapFilter,o_def]) 1);
qed"lemma_2_1a";
@@ -192,7 +192,7 @@
by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
(* main case *)
by (safe_tac set_cs);
-by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 @
+by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2 @
[actions_asig_comp,asig_of_par]) 1));
qed"sch_actions_in_AorB";
@@ -216,7 +216,7 @@
(* main case *)
(* splitting into 4 cases according to a:A, a:B *)
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
by (safe_tac set_cs);
(* Case y:A, y:B *)
@@ -241,7 +241,7 @@
by (Asm_full_simp_tac 1);
(* Case y~:A, y~:B *)
-by (asm_full_simp_tac (!simpset addsimps [asig_of_par,actions_asig_comp]) 1);
+by (asm_full_simp_tac (simpset() addsimps [asig_of_par,actions_asig_comp]) 1);
qed"Mapfst_mkex_is_sch";
@@ -249,7 +249,7 @@
fun mkex_induct_tac sch exA exB =
EVERY1[Seq_induct_tac sch [Filter_def,Forall_def,sforall_def,mkex_def,stutter_def],
- asm_full_simp_tac (!simpset setloop split_tac [expand_if]),
+ asm_full_simp_tac (simpset() setloop split_tac [expand_if]),
SELECT_GOAL (safe_tac set_cs),
Seq_case_simp_tac exA,
Seq_case_simp_tac exB,
@@ -258,7 +258,7 @@
Asm_full_simp_tac,
Seq_case_simp_tac exA,
Asm_full_simp_tac,
- asm_full_simp_tac (!simpset addsimps [asig_of_par,actions_asig_comp])
+ asm_full_simp_tac (simpset() addsimps [asig_of_par,actions_asig_comp])
];
@@ -287,7 +287,7 @@
\ ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))";
by (cut_facts_tac [stutterA_mkex] 1);
-by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjA_def,mkex_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [stutter_def,ProjA_def,mkex_def]) 1);
by (REPEAT (etac allE 1));
by (dtac mp 1);
by (assume_tac 2);
@@ -318,7 +318,7 @@
\ ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))";
by (cut_facts_tac [stutterB_mkex] 1);
-by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjB_def,mkex_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [stutter_def,ProjB_def,mkex_def]) 1);
by (REPEAT (etac allE 1));
by (dtac mp 1);
by (assume_tac 2);
@@ -362,7 +362,7 @@
goal thy "!! sch ex. \
\ Filter (%a. a:act AB)`sch = filter_act`ex \
\ ==> ex = Zip`(Filter (%a. a:act AB)`sch)`(Map snd`ex)";
-by (asm_full_simp_tac (!simpset addsimps [filter_act_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [filter_act_def]) 1);
by (rtac (Zip_Map_fst_snd RS sym) 1);
qed"trick_against_eq_in_ass";
@@ -377,15 +377,15 @@
\ Filter (%a. a:act A)`sch = filter_act`(snd exA) ;\
\ Filter (%a. a:act B)`sch = filter_act`(snd exB) |]\
\ ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA";
-by (asm_full_simp_tac (!simpset addsimps [ProjA_def,Filter_ex_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [ProjA_def,Filter_ex_def]) 1);
by (pair_tac "exA" 1);
by (pair_tac "exB" 1);
by (rtac conjI 1);
-by (simp_tac (!simpset addsimps [mkex_def]) 1);
+by (simp_tac (simpset() addsimps [mkex_def]) 1);
by (stac trick_against_eq_in_ass 1);
back();
by (assume_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [filter_mkex_is_exA_tmp]) 1);
+by (asm_full_simp_tac (simpset() addsimps [filter_mkex_is_exA_tmp]) 1);
qed"filter_mkex_is_exA";
@@ -421,15 +421,15 @@
\ Filter (%a. a:act A)`sch = filter_act`(snd exA) ;\
\ Filter (%a. a:act B)`sch = filter_act`(snd exB) |]\
\ ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB";
-by (asm_full_simp_tac (!simpset addsimps [ProjB_def,Filter_ex_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [ProjB_def,Filter_ex_def]) 1);
by (pair_tac "exA" 1);
by (pair_tac "exB" 1);
by (rtac conjI 1);
-by (simp_tac (!simpset addsimps [mkex_def]) 1);
+by (simp_tac (simpset() addsimps [mkex_def]) 1);
by (stac trick_against_eq_in_ass 1);
back();
by (assume_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [filter_mkex_is_exB_tmp]) 1);
+by (asm_full_simp_tac (simpset() addsimps [filter_mkex_is_exB_tmp]) 1);
qed"filter_mkex_is_exB";
(* --------------------------------------------------------------------- *)
@@ -460,21 +460,21 @@
\ Filter (%a. a:act B)`sch : schedules B &\
\ Forall (%x. x:act (A||B)) sch)";
-by (simp_tac (!simpset addsimps [schedules_def, has_schedule_def]) 1);
+by (simp_tac (simpset() addsimps [schedules_def, has_schedule_def]) 1);
by (safe_tac set_cs);
(* ==> *)
by (res_inst_tac [("x","Filter_ex (asig_of A) (ProjA ex)")] bexI 1);
-by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 2);
-by (simp_tac (!simpset addsimps [Filter_ex_def,ProjA_def,
+by (asm_full_simp_tac (simpset() addsimps [compositionality_ex]) 2);
+by (simp_tac (simpset() addsimps [Filter_ex_def,ProjA_def,
lemma_2_1a,lemma_2_1b]) 1);
by (res_inst_tac [("x","Filter_ex (asig_of B) (ProjB ex)")] bexI 1);
-by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 2);
-by (simp_tac (!simpset addsimps [Filter_ex_def,ProjB_def,
+by (asm_full_simp_tac (simpset() addsimps [compositionality_ex]) 2);
+by (simp_tac (simpset() addsimps [Filter_ex_def,ProjB_def,
lemma_2_1a,lemma_2_1b]) 1);
-by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
by (pair_tac "ex" 1);
by (etac conjE 1);
-by (asm_full_simp_tac (!simpset addsimps [sch_actions_in_AorB]) 1);
+by (asm_full_simp_tac (simpset() addsimps [sch_actions_in_AorB]) 1);
(* <== *)
@@ -485,16 +485,16 @@
(* mkex actions are just the oracle *)
by (pair_tac "exA" 1);
by (pair_tac "exB" 1);
-by (asm_full_simp_tac (!simpset addsimps [Mapfst_mkex_is_sch]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Mapfst_mkex_is_sch]) 1);
(* mkex is an execution -- use compositionality on ex-level *)
-by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 1);
-by (asm_full_simp_tac (!simpset addsimps
+by (asm_full_simp_tac (simpset() addsimps [compositionality_ex]) 1);
+by (asm_full_simp_tac (simpset() addsimps
[stutter_mkex_on_A, stutter_mkex_on_B,
filter_mkex_is_exB,filter_mkex_is_exA]) 1);
by (pair_tac "exA" 1);
by (pair_tac "exB" 1);
-by (asm_full_simp_tac (!simpset addsimps [mkex_actions_in_AorB]) 1);
+by (asm_full_simp_tac (simpset() addsimps [mkex_actions_in_AorB]) 1);
qed"compositionality_sch";
@@ -507,9 +507,9 @@
"Scheds (A||B) = par_scheds (Scheds A) (Scheds B)";
-by (asm_full_simp_tac (!simpset addsimps [asig_of_par]) 1);
+by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1);
br set_ext 1;
-by (asm_full_simp_tac (!simpset addsimps [compositionality_sch,actions_of_par]) 1);
+by (asm_full_simp_tac (simpset() addsimps [compositionality_sch,actions_of_par]) 1);
qed"compositionality_sch_modules";
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Mon Nov 03 14:06:27 1997 +0100
@@ -67,8 +67,8 @@
\ `schB))";
by (rtac trans 1);
by (stac mksch_unfold 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
-by (simp_tac (!simpset addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
+by (simp_tac (simpset() addsimps [Cons_def]) 1);
qed"mksch_cons1";
goal thy "!!x.[|x~:act A;x:act B|] \
@@ -78,8 +78,8 @@
\ ))";
by (rtac trans 1);
by (stac mksch_unfold 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
-by (simp_tac (!simpset addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
+by (simp_tac (simpset() addsimps [Cons_def]) 1);
qed"mksch_cons2";
goal thy "!!x.[|x:act A;x:act B|] \
@@ -91,8 +91,8 @@
\ )";
by (rtac trans 1);
by (stac mksch_unfold 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
-by (simp_tac (!simpset addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def,If_and_if]) 1);
+by (simp_tac (simpset() addsimps [Cons_def]) 1);
qed"mksch_cons3";
val compotr_simps =[mksch_UU,mksch_nil, mksch_cons1,mksch_cons2,mksch_cons3];
@@ -151,24 +151,24 @@
\ --> Forall (%x. x:act (A||B)) (mksch A B`tr`schA`schB)";
by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
by (safe_tac set_cs);
-by (asm_full_simp_tac (!simpset addsimps [actions_of_par]) 1);
+by (asm_full_simp_tac (simpset() addsimps [actions_of_par]) 1);
by (case_tac "a:act A" 1);
by (case_tac "a:act B" 1);
(* a:A, a:B *)
by (Asm_full_simp_tac 1);
by (rtac (Forall_Conc_impl RS mp) 1);
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
+by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
by (rtac (Forall_Conc_impl RS mp) 1);
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
+by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
(* a:A,a~:B *)
by (Asm_full_simp_tac 1);
by (rtac (Forall_Conc_impl RS mp) 1);
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
+by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
by (case_tac "a:act B" 1);
(* a~:A, a:B *)
by (Asm_full_simp_tac 1);
by (rtac (Forall_Conc_impl RS mp) 1);
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
+by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
(* a~:A,a~:B *)
by (Auto_tac());
qed"ForallAorB_mksch1";
@@ -182,7 +182,7 @@
by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
by (safe_tac set_cs);
by (rtac (Forall_Conc_impl RS mp) 1);
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,
+by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,
intA_is_not_actB,int_is_act]) 1);
qed"ForallBnA_mksch";
@@ -197,7 +197,7 @@
by (safe_tac set_cs);
by (Asm_full_simp_tac 1);
by (rtac (Forall_Conc_impl RS mp) 1);
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,
+by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,
intA_is_not_actB,int_is_act]) 1);
qed"ForallAnB_mksch";
@@ -217,7 +217,7 @@
by (etac Seq_Finite_ind 1);
by (Asm_full_simp_tac 1);
(* main case *)
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
by (safe_tac set_cs);
(* a: act A; a: act B *)
@@ -226,7 +226,7 @@
back();
by (REPEAT (etac conjE 1));
(* Finite (tw iA x) and Finite (tw iB y) *)
-by (asm_full_simp_tac (!simpset addsimps
+by (asm_full_simp_tac (simpset() addsimps
[not_ext_is_int_or_not_act,FiniteConc]) 1);
(* now for conclusion IH applicable, but assumptions have to be transformed *)
by (dres_inst_tac [("x","x"),
@@ -236,7 +236,7 @@
("g","Filter (%a. a:act B)`s")] subst_lemma2 1);
by (assume_tac 1);
(* IH *)
-by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
+by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
(* a: act B; a~: act A *)
@@ -244,14 +244,14 @@
by (REPEAT (etac conjE 1));
(* Finite (tw iB y) *)
-by (asm_full_simp_tac (!simpset addsimps
+by (asm_full_simp_tac (simpset() addsimps
[not_ext_is_int_or_not_act,FiniteConc]) 1);
(* now for conclusion IH applicable, but assumptions have to be transformed *)
by (dres_inst_tac [("x","y"),
("g","Filter (%a. a:act B)`s")] subst_lemma2 1);
by (assume_tac 1);
(* IH *)
-by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
+by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
(* a~: act B; a: act A *)
@@ -259,19 +259,19 @@
by (REPEAT (etac conjE 1));
(* Finite (tw iA x) *)
-by (asm_full_simp_tac (!simpset addsimps
+by (asm_full_simp_tac (simpset() addsimps
[not_ext_is_int_or_not_act,FiniteConc]) 1);
(* now for conclusion IH applicable, but assumptions have to be transformed *)
by (dres_inst_tac [("x","x"),
("g","Filter (%a. a:act A)`s")] subst_lemma2 1);
by (assume_tac 1);
(* IH *)
-by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
+by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
(* a~: act B; a~: act A *)
-by (fast_tac (!claset addSIs [ext_is_act]
- addss (!simpset addsimps [externals_of_par]) ) 1);
+by (fast_tac (claset() addSIs [ext_is_act]
+ addss (simpset() addsimps [externals_of_par]) ) 1);
qed"FiniteL_mksch";
bind_thm("FiniteL_mksch1", FiniteL_mksch RS spec RS spec RS mp);
@@ -310,10 +310,10 @@
("g","Filter (%a. a:act B)`(s@@z)")] subst_lemma2 1);
by (assume_tac 1);
Addsimps [FilterConc];
-by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
+by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
(* apply IH *)
by (eres_inst_tac [("x","TL`(Dropwhile (%a. a:int B)`y)")] allE 1);
-by (asm_full_simp_tac (!simpset addsimps [ForallTL,ForallDropwhile])1);
+by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile])1);
by (REPEAT (etac exE 1));
by (REPEAT (etac conjE 1));
by (Asm_full_simp_tac 1);
@@ -324,9 +324,9 @@
by (res_inst_tac [("x","Takewhile (%a. a:int B)`y @@ a>>y1")] exI 1);
by (res_inst_tac [("x","y2")] exI 1);
(* elminate all obligations up to two depending on Conc_assoc *)
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, intA_is_not_actB,
+by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, intA_is_not_actB,
int_is_act,FilterPTakewhileQnil,int_is_not_ext]) 1);
-by (simp_tac (!simpset addsimps [Conc_assoc]) 1);
+by (simp_tac (simpset() addsimps [Conc_assoc]) 1);
qed"reduceA_mksch1";
bind_thm("reduceA_mksch",conjI RSN (6,conjI RSN (5,reduceA_mksch1 RS spec RS mp)));
@@ -365,10 +365,10 @@
("g","Filter (%a. a:act A)`(s@@z)")] subst_lemma2 1);
by (assume_tac 1);
Addsimps [FilterConc];
-by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
+by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
(* apply IH *)
by (eres_inst_tac [("x","TL`(Dropwhile (%a. a:int A)`x)")] allE 1);
-by (asm_full_simp_tac (!simpset addsimps [ForallTL,ForallDropwhile])1);
+by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile])1);
by (REPEAT (etac exE 1));
by (REPEAT (etac conjE 1));
by (Asm_full_simp_tac 1);
@@ -379,9 +379,9 @@
by (res_inst_tac [("x","Takewhile (%a. a:int A)`x @@ a>>x1")] exI 1);
by (res_inst_tac [("x","x2")] exI 1);
(* elminate all obligations up to two depending on Conc_assoc *)
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, intA_is_not_actB,
+by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, intA_is_not_actB,
int_is_act,FilterPTakewhileQnil,int_is_not_ext]) 1);
-by (simp_tac (!simpset addsimps [Conc_assoc]) 1);
+by (simp_tac (simpset() addsimps [Conc_assoc]) 1);
qed"reduceB_mksch1";
bind_thm("reduceB_mksch",conjI RSN (6,conjI RSN (5,reduceB_mksch1 RS spec RS mp)));
@@ -398,7 +398,7 @@
by (Auto_tac());
by (Seq_case_simp_tac "tr" 1);
(* tr = UU *)
-by (asm_full_simp_tac (!simpset addsimps [nil_is_Conc]) 1);
+by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc]) 1);
(* tr = nil *)
by (Auto_tac());
(* tr = Conc *)
@@ -408,17 +408,17 @@
by (case_tac "s:act B" 1);
by (rotate_tac ~2 1);
by (rotate_tac ~2 2);
-by (asm_full_simp_tac (!simpset addsimps [nil_is_Conc,nil_is_Conc2]) 1);
-by (asm_full_simp_tac (!simpset addsimps [nil_is_Conc,nil_is_Conc2]) 1);
+by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc,nil_is_Conc2]) 1);
+by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc,nil_is_Conc2]) 1);
by (case_tac "s:act B" 1);
by (rotate_tac ~2 1);
-by (asm_full_simp_tac (!simpset addsimps [nil_is_Conc,nil_is_Conc2]) 1);
-by (fast_tac (!claset addSIs [ext_is_act]
- addss (!simpset addsimps [externals_of_par]) ) 1);
+by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc,nil_is_Conc2]) 1);
+by (fast_tac (claset() addSIs [ext_is_act]
+ addss (simpset() addsimps [externals_of_par]) ) 1);
(* main case *)
by (Seq_case_simp_tac "tr" 1);
(* tr = UU *)
-by (asm_full_simp_tac (!simpset addsimps [Conc_Conc_eq]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Conc_Conc_eq]) 1);
by (Auto_tac());
(* tr = nil ok *)
(* tr = Conc *)
@@ -436,7 +436,7 @@
by (asm_full_simp_tac (HOL_basic_ss addsimps [mksch_cons3]) 2);
by (eres_inst_tac [("x","sb@@Takewhile (%a. a: int A)`a @@ Takewhile (%a. a:int B)`b@@(aaa>>nil)")] allE 2);
by (eres_inst_tac [("x","sa")] allE 2);
-by (asm_full_simp_tac (!simpset addsimps [Conc_assoc])2);
+by (asm_full_simp_tac (simpset() addsimps [Conc_assoc])2);
@@ -446,7 +446,7 @@
by (case_tac "aaa:act B" 1);
by (rotate_tac ~2 1);
by (rotate_tac ~2 2);
-by (asm_full_simp_tac (!simpset addsimps [Conc_Conc_eq]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Conc_Conc_eq]) 1);
@@ -491,7 +491,7 @@
(* main case *)
(* splitting into 4 cases according to a:A, a:B *)
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
by (safe_tac set_cs);
(* Case a:A, a:B *)
@@ -500,7 +500,7 @@
back();
by (REPEAT (etac conjE 1));
(* filtering internals of A in schA and of B in schB is nil *)
-by (asm_full_simp_tac (!simpset addsimps
+by (asm_full_simp_tac (simpset() addsimps
[FilterPTakewhileQnil,not_ext_is_int_or_not_act,
externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
(* conclusion of IH ok, but assumptions of IH have to be transformed *)
@@ -509,37 +509,37 @@
by (dres_inst_tac [("x","schB")] subst_lemma1 1);
by (assume_tac 1);
(* IH *)
-by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
+by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
(* Case a:B, a~:A *)
by (forward_tac [divide_Seq] 1);
by (REPEAT (etac conjE 1));
(* filtering internals of A is nil *)
-by (asm_full_simp_tac (!simpset addsimps
+by (asm_full_simp_tac (simpset() addsimps
[FilterPTakewhileQnil,not_ext_is_int_or_not_act,
externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
by (dres_inst_tac [("x","schB")] subst_lemma1 1);
back();
by (assume_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
+by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
(* Case a:A, a~:B *)
by (forward_tac [divide_Seq] 1);
by (REPEAT (etac conjE 1));
(* filtering internals of A is nil *)
-by (asm_full_simp_tac (!simpset addsimps
+by (asm_full_simp_tac (simpset() addsimps
[FilterPTakewhileQnil,not_ext_is_int_or_not_act,
externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
by (dres_inst_tac [("x","schA")] subst_lemma1 1);
by (assume_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
+by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
(* Case a~:A, a~:B *)
-by (fast_tac (!claset addSIs [ext_is_act]
- addss (!simpset addsimps [externals_of_par]) ) 1);
+by (fast_tac (claset() addSIs [ext_is_act]
+ addss (simpset() addsimps [externals_of_par]) ) 1);
qed"FilterA_mksch_is_tr";
@@ -573,13 +573,13 @@
by (subgoal_tac "schA=nil" 1);
by (Asm_simp_tac 1);
(* first side: mksch = nil *)
-by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPnil,ForallBnAmksch,FiniteL_mksch],
- !simpset)) 1);
+by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPnil,ForallBnAmksch,FiniteL_mksch],
+ simpset())) 1);
(* second side: schA = nil *)
by (eres_inst_tac [("A","A")] LastActExtimplnil 1);
by (Asm_simp_tac 1);
-by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPnil],
- !simpset)) 1);
+by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPnil],
+ simpset())) 1);
(* case ~ Finite s *)
@@ -587,15 +587,15 @@
by (subgoal_tac "schA=UU" 1);
by (Asm_simp_tac 1);
(* first side: mksch = UU *)
-by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPUU,
+by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU,
(finiteR_mksch RS mp COMP rev_contrapos),
ForallBnAmksch],
- !simpset)) 1);
+ simpset())) 1);
(* schA = UU *)
by (eres_inst_tac [("A","A")] LastActExtimplUU 1);
by (Asm_simp_tac 1);
-by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPUU],
- !simpset)) 1);
+by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU],
+ simpset())) 1);
(* case" ~ Forall (%x.x:act B & x~:act A) s" *)
@@ -649,7 +649,7 @@
by (rtac take_reduction 1);
(* f A (tw iA) = tw ~eA *)
-by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
+by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act,
not_ext_is_int_or_not_act]) 1);
by (rtac refl 1);
@@ -661,12 +661,12 @@
*)
(* assumption schB *)
-by (asm_full_simp_tac (!simpset addsimps [ext_and_act]) 1);
+by (asm_full_simp_tac (simpset() addsimps [ext_and_act]) 1);
(* assumption schA *)
by (dres_inst_tac [("x","schA"),
("g","Filter (%a. a:act A)`s2")] subst_lemma2 1);
by (assume_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil]) 1);
+by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil]) 1);
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
by (dres_inst_tac [("sch1.0","y1")] LastActExtsmall2 1);
@@ -725,8 +725,8 @@
by (subgoal_tac "schA=nil" 1);
by (Asm_simp_tac 1);
(* first side: mksch = nil *)
-by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPnil,ForallBnAmksch,FiniteL_mksch1],
- !simpset)) 1);
+by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPnil,ForallBnAmksch,FiniteL_mksch1],
+ simpset())) 1);
(* second side: schA = nil *)
by (eres_inst_tac [("A","A")] LastActExtimplnil 1);
by (Asm_simp_tac 1);
@@ -740,10 +740,10 @@
by (subgoal_tac "schA=UU" 1);
by (Asm_simp_tac 1);
(* first side: mksch = UU *)
-by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPUU,
+by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU,
(finiteR_mksch RS mp COMP rev_contrapos),
ForallBnAmksch],
- !simpset)) 1);
+ simpset())) 1);
(* schA = UU *)
by (eres_inst_tac [("A","A")] LastActExtimplUU 1);
by (Asm_simp_tac 1);
@@ -807,25 +807,25 @@
by (rtac take_reduction 1);
(* f A (tw iA) = tw ~eA *)
-by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
+by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act,
not_ext_is_int_or_not_act]) 1);
by (rtac refl 1);
-by (asm_full_simp_tac (!simpset addsimps [int_is_act,
+by (asm_full_simp_tac (simpset() addsimps [int_is_act,
not_ext_is_int_or_not_act]) 1);
by (rotate_tac ~11 1);
(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
(* assumption Forall tr *)
-by (asm_full_simp_tac (!simpset addsimps [Forall_Conc]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Forall_Conc]) 1);
(* assumption schB *)
-by (asm_full_simp_tac (!simpset addsimps [Forall_Conc,ext_and_act]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Forall_Conc,ext_and_act]) 1);
by (REPEAT (etac conjE 1));
(* assumption schA *)
by (dres_inst_tac [("x","schA"),
("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
by (assume_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
+by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
by (forw_inst_tac [("sch1.0","y1")] LastActExtsmall2 1);
@@ -835,7 +835,7 @@
by (dres_inst_tac [("s","schA"),
("P","Forall (%x. x:act A)")] subst 1);
by (assume_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, int_is_act]) 1);
+by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, int_is_act]) 1);
(* case x:actions(asig_of A) & x: actions(asig_of B) *)
@@ -863,12 +863,12 @@
by (assume_tac 1);
(* f A (tw iA) = tw ~eA *)
-by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
+by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act,
not_ext_is_int_or_not_act]) 1);
(* rewrite assumption forall and schB *)
by (rotate_tac 13 1);
-by (asm_full_simp_tac (!simpset addsimps [ext_and_act]) 1);
+by (asm_full_simp_tac (simpset() addsimps [ext_and_act]) 1);
(* divide_Seq for schB2 *)
by (forw_inst_tac [("y","y2")] (sym RS antisym_less_inverse RS conjunct1 RS divide_Seq) 1);
@@ -877,10 +877,10 @@
by (dres_inst_tac [("x","schA"),
("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
by (assume_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
+by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
(* f A (tw iB schB2) = nil *)
-by (asm_full_simp_tac (!simpset addsimps [int_is_not_ext,not_ext_is_int_or_not_act,
+by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext,not_ext_is_int_or_not_act,
FilterPTakewhileQnil,intA_is_not_actB]) 1);
@@ -895,7 +895,7 @@
by (dres_inst_tac [("x","y2"),
("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
by (assume_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1);
+by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1);
(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
@@ -904,7 +904,7 @@
by (dres_inst_tac [("sch","y2"),("P","%a. a:int B")] LastActExtsmall1 1);
(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
-by (asm_full_simp_tac (!simpset addsimps [ForallTL,ForallDropwhile]) 1);
+by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile]) 1);
(* case x~:A & x:B *)
(* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
@@ -915,9 +915,9 @@
(* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
by (rotate_tac ~9 1);
(* reduce forall assumption from tr to (x>>rs) *)
-by (asm_full_simp_tac (!simpset addsimps [externals_of_par]) 1);
+by (asm_full_simp_tac (simpset() addsimps [externals_of_par]) 1);
by (REPEAT (etac conjE 1));
-by (fast_tac (!claset addSIs [ext_is_act]) 1);
+by (fast_tac (claset() addSIs [ext_is_act]) 1);
qed"FilterAmksch_is_schA";
@@ -967,8 +967,8 @@
by (subgoal_tac "schB=nil" 1);
by (Asm_simp_tac 1);
(* first side: mksch = nil *)
-by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPnil,ForallAnBmksch,FiniteL_mksch1],
- !simpset)) 1);
+by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPnil,ForallAnBmksch,FiniteL_mksch1],
+ simpset())) 1);
(* second side: schA = nil *)
by (eres_inst_tac [("A","B")] LastActExtimplnil 1);
by (Asm_simp_tac 1);
@@ -982,10 +982,10 @@
by (subgoal_tac "schB=UU" 1);
by (Asm_simp_tac 1);
(* first side: mksch = UU *)
-by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPUU,
+by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU,
(finiteR_mksch RS mp COMP rev_contrapos),
ForallAnBmksch],
- !simpset)) 1);
+ simpset())) 1);
(* schA = UU *)
by (eres_inst_tac [("A","B")] LastActExtimplUU 1);
by (Asm_simp_tac 1);
@@ -1049,25 +1049,25 @@
by (rtac take_reduction 1);
(* f B (tw iB) = tw ~eB *)
-by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
+by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act,
not_ext_is_int_or_not_act]) 1);
by (rtac refl 1);
-by (asm_full_simp_tac (!simpset addsimps [int_is_act,
+by (asm_full_simp_tac (simpset() addsimps [int_is_act,
not_ext_is_int_or_not_act]) 1);
by (rotate_tac ~11 1);
(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
(* assumption Forall tr *)
-by (asm_full_simp_tac (!simpset addsimps [Forall_Conc]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Forall_Conc]) 1);
(* assumption schA *)
-by (asm_full_simp_tac (!simpset addsimps [Forall_Conc,ext_and_act]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Forall_Conc,ext_and_act]) 1);
by (REPEAT (etac conjE 1));
(* assumption schB *)
by (dres_inst_tac [("x","schB"),
("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
by (assume_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
+by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
by (dres_inst_tac [("sch","schB"),("P","%a. a:int B")] LastActExtsmall1 1);
by (forw_inst_tac [("sch1.0","x1")] LastActExtsmall2 1);
@@ -1077,7 +1077,7 @@
by (dres_inst_tac [("s","schB"),
("P","Forall (%x. x:act B)")] subst 1);
by (assume_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, int_is_act]) 1);
+by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, int_is_act]) 1);
(* case x:actions(asig_of A) & x: actions(asig_of B) *)
@@ -1105,12 +1105,12 @@
by (assume_tac 1);
(* f B (tw iB) = tw ~eB *)
-by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
+by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act,
not_ext_is_int_or_not_act]) 1);
(* rewrite assumption forall and schB *)
by (rotate_tac 13 1);
-by (asm_full_simp_tac (!simpset addsimps [ext_and_act]) 1);
+by (asm_full_simp_tac (simpset() addsimps [ext_and_act]) 1);
(* divide_Seq for schB2 *)
by (forw_inst_tac [("y","x2")] (sym RS antisym_less_inverse RS conjunct1 RS divide_Seq) 1);
@@ -1119,10 +1119,10 @@
by (dres_inst_tac [("x","schB"),
("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
by (assume_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
+by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
(* f B (tw iA schA2) = nil *)
-by (asm_full_simp_tac (!simpset addsimps [int_is_not_ext,not_ext_is_int_or_not_act,
+by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext,not_ext_is_int_or_not_act,
FilterPTakewhileQnil,intA_is_not_actB]) 1);
@@ -1137,7 +1137,7 @@
by (dres_inst_tac [("x","x2"),
("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
by (assume_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1);
+by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1);
(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
by (dres_inst_tac [("sch","schB"),("P","%a. a:int B")] LastActExtsmall1 1);
@@ -1146,7 +1146,7 @@
by (dres_inst_tac [("sch","x2"),("P","%a. a:int A")] LastActExtsmall1 1);
(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
-by (asm_full_simp_tac (!simpset addsimps [ForallTL,ForallDropwhile]) 1);
+by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile]) 1);
(* case x~:B & x:A *)
(* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
@@ -1157,9 +1157,9 @@
(* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
by (rotate_tac ~9 1);
(* reduce forall assumption from tr to (x>>rs) *)
-by (asm_full_simp_tac (!simpset addsimps [externals_of_par]) 1);
+by (asm_full_simp_tac (simpset() addsimps [externals_of_par]) 1);
by (REPEAT (etac conjE 1));
-by (fast_tac (!claset addSIs [ext_is_act]) 1);
+by (fast_tac (claset() addSIs [ext_is_act]) 1);
qed"FilterBmksch_is_schB";
@@ -1177,19 +1177,19 @@
\ Filter (%a. a:act B)`tr : traces B &\
\ Forall (%x. x:ext(A||B)) tr)";
-by (simp_tac (!simpset addsimps [traces_def,has_trace_def]) 1);
+by (simp_tac (simpset() addsimps [traces_def,has_trace_def]) 1);
by (safe_tac set_cs);
(* ==> *)
(* There is a schedule of A *)
by (res_inst_tac [("x","Filter (%a. a:act A)`sch")] bexI 1);
-by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 2);
-by (asm_full_simp_tac (!simpset addsimps [compatibility_consequence1,
+by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 2);
+by (asm_full_simp_tac (simpset() addsimps [compatibility_consequence1,
externals_of_par,ext1_ext2_is_not_act1]) 1);
(* There is a schedule of B *)
by (res_inst_tac [("x","Filter (%a. a:act B)`sch")] bexI 1);
-by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 2);
-by (asm_full_simp_tac (!simpset addsimps [compatibility_consequence2,
+by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 2);
+by (asm_full_simp_tac (simpset() addsimps [compatibility_consequence2,
externals_of_par,ext1_ext2_is_not_act2]) 1);
(* Traces of A||B have only external actions from A or B *)
by (rtac ForallPFilterP 1);
@@ -1215,11 +1215,11 @@
by (res_inst_tac [("x","mksch A B`tr`schA`schB")] bexI 1);
(* External actions of mksch are just the oracle *)
-by (asm_full_simp_tac (!simpset addsimps [FilterA_mksch_is_tr RS spec RS spec RS mp]) 1);
+by (asm_full_simp_tac (simpset() addsimps [FilterA_mksch_is_tr RS spec RS spec RS mp]) 1);
(* mksch is a schedule -- use compositionality on sch-level *)
-by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 1);
-by (asm_full_simp_tac (!simpset addsimps [FilterAmksch_is_schA,FilterBmksch_is_schB]) 1);
+by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 1);
+by (asm_full_simp_tac (simpset() addsimps [FilterAmksch_is_schA,FilterBmksch_is_schB]) 1);
by (etac ForallAorB_mksch 1);
by (etac ForallPForallQ 1);
by (etac ext_is_act 1);
@@ -1238,9 +1238,9 @@
\ is_asig(asig_of A); is_asig(asig_of B)|] \
\==> Traces (A||B) = par_traces (Traces A) (Traces B)";
-by (asm_full_simp_tac (!simpset addsimps [asig_of_par]) 1);
+by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1);
br set_ext 1;
-by (asm_full_simp_tac (!simpset addsimps [compositionality_tr,externals_of_par]) 1);
+by (asm_full_simp_tac (simpset() addsimps [compositionality_tr,externals_of_par]) 1);
qed"compositionality_tr_modules";
--- a/src/HOLCF/IOA/meta_theory/Compositionality.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML Mon Nov 03 14:06:27 1997 +0100
@@ -20,7 +20,7 @@
(* i.e.: [| (! x. P x --> (Q x = R x)) ; Forall P tr |] ==> Filter Q`tr = Filter R`tr *)
by (assume_tac 2);
by (rtac compatibility_consequence3 1);
-by (REPEAT (asm_full_simp_tac (!simpset
+by (REPEAT (asm_full_simp_tac (simpset()
addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1));
qed"Filter_actAisFilter_extA";
@@ -38,7 +38,7 @@
by (rtac ForallPFilterQR 1);
by (assume_tac 2);
by (rtac compatibility_consequence4 1);
-by (REPEAT (asm_full_simp_tac (!simpset
+by (REPEAT (asm_full_simp_tac (simpset()
addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1));
qed"Filter_actAisFilter_extA2";
@@ -58,29 +58,29 @@
\ B1 =<| B2 |] \
\ ==> (A1 || B1) =<| (A2 || B2)";
-by (asm_full_simp_tac (!simpset addsimps [is_asig_of_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def]) 1);
by (forw_inst_tac [("A2","A1")] (compat_commute RS iffD1) 1);
by (forw_inst_tac [("A2","A2")] (compat_commute RS iffD1) 1);
-by (asm_full_simp_tac (!simpset addsimps [ioa_implements_def,
+by (asm_full_simp_tac (simpset() addsimps [ioa_implements_def,
inputs_of_par,outputs_of_par,externals_of_par]) 1);
by (safe_tac set_cs);
-by (asm_full_simp_tac (!simpset addsimps [compositionality_tr]) 1);
+by (asm_full_simp_tac (simpset() addsimps [compositionality_tr]) 1);
by (subgoal_tac "ext A1 = ext A2 & ext B1 = ext B2" 1);
-by (asm_full_simp_tac (!simpset addsimps [externals_def]) 2);
+by (asm_full_simp_tac (simpset() addsimps [externals_def]) 2);
by (REPEAT (etac conjE 1));
(* rewrite with proven subgoal *)
-by (asm_full_simp_tac (!simpset addsimps [externals_of_par]) 1);
+by (asm_full_simp_tac (simpset() addsimps [externals_of_par]) 1);
by (safe_tac set_cs);
(* 2 goals, the 3rd has been solved automatically *)
(* 1: Filter A2 x : traces A2 *)
by (dres_inst_tac [("A","traces A1")] subsetD 1);
by (assume_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [Filter_actAisFilter_extA]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Filter_actAisFilter_extA]) 1);
(* 2: Filter B2 x : traces B2 *)
by (dres_inst_tac [("A","traces B1")] subsetD 1);
by (assume_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [Filter_actAisFilter_extA2]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Filter_actAisFilter_extA2]) 1);
qed"compositionality";
--- a/src/HOLCF/IOA/meta_theory/Deadlock.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML Mon Nov 03 14:06:27 1997 +0100
@@ -12,14 +12,14 @@
goal thy "!! sch. [| Filter (%x. x:act A)`sch : schedules A; a:inp A; input_enabled A; Finite sch|] \
\ ==> Filter (%x. x:act A)`sch @@ a>>nil : schedules A";
-by (asm_full_simp_tac (!simpset addsimps [schedules_def,has_schedule_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [schedules_def,has_schedule_def]) 1);
by (safe_tac set_cs);
by (forward_tac [inp_is_act] 1);
-by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
by (pair_tac "ex" 1);
ren "sch s ex" 1;
by (subgoal_tac "Finite ex" 1);
-by (asm_full_simp_tac (!simpset addsimps [filter_act_def]) 2);
+by (asm_full_simp_tac (simpset() addsimps [filter_act_def]) 2);
by (rtac (Map2Finite RS iffD1) 2);
by (res_inst_tac [("t","Map fst`ex")] subst 2);
by (assume_tac 2);
@@ -29,7 +29,7 @@
by (etac allE 1);
by (etac exE 1);
(* using input-enabledness *)
-by (asm_full_simp_tac (!simpset addsimps [input_enabled_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [input_enabled_def]) 1);
by (REPEAT (etac conjE 1));
by (eres_inst_tac [("x","a")] allE 1);
by (Asm_full_simp_tac 1);
@@ -37,7 +37,7 @@
by (etac exE 1);
(* instantiate execution *)
by (res_inst_tac [("x","(s,ex @@ (a,s2)>>nil)")] exI 1);
-by (asm_full_simp_tac (!simpset addsimps [filter_act_def,MapConc]) 1);
+by (asm_full_simp_tac (simpset() addsimps [filter_act_def,MapConc]) 1);
by (eres_inst_tac [("t","u")] lemma_2_1 1);
by (Asm_full_simp_tac 1);
by (rtac sym 1);
@@ -55,10 +55,10 @@
\ Filter (%x. x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
\ ==> (sch @@ a>>nil) : schedules (A||B)";
-by (asm_full_simp_tac (!simpset addsimps [compositionality_sch,locals_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [compositionality_sch,locals_def]) 1);
by (rtac conjI 1);
(* a : act (A||B) *)
-by (asm_full_simp_tac (!simpset addsimps [actions_of_par]) 2);
+by (asm_full_simp_tac (simpset() addsimps [actions_of_par]) 2);
by (rtac disjI1 2);
by (etac disjE 2);
by (etac int_is_act 2);
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Mon Nov 03 14:06:27 1997 +0100
@@ -27,7 +27,7 @@
by (rtac fix_eq2 1);
by (rtac corresp_exC_def 1);
by (rtac beta_cfun 1);
-by (simp_tac (!simpset addsimps [flift1_def]) 1);
+by (simp_tac (simpset() addsimps [flift1_def]) 1);
qed"corresp_exC_unfold";
goal thy "(corresp_exC A f`UU) s=UU";
@@ -45,7 +45,7 @@
\ @@ ((corresp_exC A f`xs) (snd at))";
by (rtac trans 1);
by (stac corresp_exC_unfold 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
by (Simp_tac 1);
qed"corresp_exC_cons";
@@ -77,7 +77,7 @@
\ is_exec_frag A (f s,@x. move A x (f s) a (f t))";
by (cut_inst_tac [] move_is_move 1);
by (REPEAT (assume_tac 1));
-by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
qed"move_subprop1";
goal thy
@@ -85,7 +85,7 @@
\ Finite ((@x. move A x (f s) a (f t)))";
by (cut_inst_tac [] move_is_move 1);
by (REPEAT (assume_tac 1));
-by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
qed"move_subprop2";
goal thy
@@ -93,7 +93,7 @@
\ laststate (f s,@x. move A x (f s) a (f t)) = (f t)";
by (cut_inst_tac [] move_is_move 1);
by (REPEAT (assume_tac 1));
-by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
qed"move_subprop3";
goal thy
@@ -103,7 +103,7 @@
by (cut_inst_tac [] move_is_move 1);
by (REPEAT (assume_tac 1));
-by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
qed"move_subprop4";
@@ -120,7 +120,7 @@
goal thy "mk_trace C`(ex1 @@ ex2)= (mk_trace C`ex1) @@ (mk_trace C`ex2)";
-by (simp_tac (!simpset addsimps [mk_trace_def,filter_act_def,
+by (simp_tac (simpset() addsimps [mk_trace_def,filter_act_def,
FilterConc,MapConc]) 1);
qed"mk_traceConc";
@@ -138,12 +138,12 @@
by (pair_induct_tac "xs" [is_exec_frag_def] 1);
(* cons case *)
by (safe_tac set_cs);
-by (asm_full_simp_tac (!simpset addsimps [mk_traceConc]) 1);
+by (asm_full_simp_tac (simpset() addsimps [mk_traceConc]) 1);
by (forward_tac [reachable.reachable_n] 1);
by (assume_tac 1);
by (eres_inst_tac [("x","y")] allE 1);
by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [move_subprop4]
+by (asm_full_simp_tac (simpset() addsimps [move_subprop4]
setloop split_tac [expand_if] ) 1);
qed"lemma_1";
@@ -224,7 +224,7 @@
"!!f. [| ext C = ext A; is_ref_map f C A |] \
\ ==> traces C <= traces A";
- by (simp_tac(!simpset addsimps [has_trace_def2])1);
+ by (simp_tac(simpset() addsimps [has_trace_def2])1);
by (safe_tac set_cs);
(* give execution of abstract automata *)
@@ -234,17 +234,17 @@
by (pair_tac "ex" 1);
by (etac (lemma_1 RS spec RS mp) 1);
by (REPEAT (atac 1));
- by (asm_full_simp_tac (!simpset addsimps [executions_def,reachable.reachable_0]) 1);
+ by (asm_full_simp_tac (simpset() addsimps [executions_def,reachable.reachable_0]) 1);
(* corresp_ex is execution, Lemma 2 *)
by (pair_tac "ex" 1);
- by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
+ by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
(* start state *)
by (rtac conjI 1);
- by (asm_full_simp_tac (!simpset addsimps [is_ref_map_def,corresp_ex_def]) 1);
+ by (asm_full_simp_tac (simpset() addsimps [is_ref_map_def,corresp_ex_def]) 1);
(* is-execution-fragment *)
by (etac (lemma_2 RS spec RS mp) 1);
- by (asm_full_simp_tac (!simpset addsimps [reachable.reachable_0]) 1);
+ by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
qed"trace_inclusion";
--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML Mon Nov 03 14:06:27 1997 +0100
@@ -13,15 +13,15 @@
(* ---------------------------------------------------------------------------- *)
goal thy "laststate (s,UU) = s";
-by (simp_tac (!simpset addsimps [laststate_def]) 1);
+by (simp_tac (simpset() addsimps [laststate_def]) 1);
qed"laststate_UU";
goal thy "laststate (s,nil) = s";
-by (simp_tac (!simpset addsimps [laststate_def]) 1);
+by (simp_tac (simpset() addsimps [laststate_def]) 1);
qed"laststate_nil";
goal thy "!! ex. Finite ex ==> laststate (s,at>>ex) = laststate (snd at,ex)";
-by (simp_tac (!simpset addsimps [laststate_def]) 1);
+by (simp_tac (simpset() addsimps [laststate_def]) 1);
by (case_tac "ex=nil" 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
@@ -45,14 +45,14 @@
goal thy"!!f. s -a--A-> t ==> ? ex. move A ex s a t";
by (res_inst_tac [("x","(a,t)>>nil")] exI 1);
-by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
qed"transition_is_ex";
goal thy"!!f. (~a:ext A) & s=t ==> ? ex. move A ex s a t";
by (res_inst_tac [("x","nil")] exI 1);
-by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
qed"nothing_is_ex";
@@ -60,7 +60,7 @@
\ ==> ? ex. move A ex s a s''";
by (res_inst_tac [("x","(a,s')>>(a',s'')>>nil")] exI 1);
-by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
qed"ei_transitions_are_ex";
@@ -70,7 +70,7 @@
\ ? ex. move A ex s1 a1 s4";
by (res_inst_tac [("x","(a1,s2)>>(a2,s3)>>(a3,s4)>>nil")] exI 1);
-by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
qed"eii_transitions_are_ex";
@@ -92,23 +92,23 @@
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
- by(fast_tac (!claset addDs prems) 1);
+ by(fast_tac (claset() addDs prems) 1);
val lemma = result();
goal thy "!!f.[| is_weak_ref_map f C A |]\
\ ==> (is_weak_ref_map f (rename C g) (rename A g))";
-by (asm_full_simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
by (rtac conjI 1);
(* 1: start states *)
-by (asm_full_simp_tac (!simpset addsimps [rename_def,rename_set_def,starts_of_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [rename_def,rename_set_def,starts_of_def]) 1);
(* 2: reachable transitions *)
by (REPEAT (rtac allI 1));
by (rtac lemma 1);
-by (simp_tac (!simpset addsimps [rename_def,rename_set_def]) 1);
-by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_inputs_def,
+by (simp_tac (simpset() addsimps [rename_def,rename_set_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 (!claset));
+by (safe_tac (claset()));
by (stac expand_if 1);
by (rtac conjI 1);
by (rtac impI 1);
@@ -132,7 +132,7 @@
by (forward_tac [reachable_rename] 1);
by (Asm_full_simp_tac 1);
(* x is internal *)
-by (simp_tac (!simpset addcongs [conj_cong]) 1);
+by (simp_tac (simpset() addcongs [conj_cong]) 1);
by (rtac impI 1);
by (etac conjE 1);
by (forward_tac [reachable_rename] 1);
--- a/src/HOLCF/IOA/meta_theory/Seq.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.ML Mon Nov 03 14:06:27 1997 +0100
@@ -357,32 +357,32 @@
by (Simp_tac 1);
by (Simp_tac 1);
(* main case *)
-by (asm_full_simp_tac (!simpset setloop split_If_tac) 1);
+by (asm_full_simp_tac (simpset() setloop split_If_tac) 1);
qed"sfiltersconc";
goal thy "sforall P (stakewhile`P`x)";
-by (simp_tac (!simpset addsimps [sforall_def]) 1);
+by (simp_tac (simpset() addsimps [sforall_def]) 1);
by (res_inst_tac[("x","x")] seq.ind 1);
(* adm *)
-by (simp_tac (!simpset addsimps [adm_trick_1]) 1);
+by (simp_tac (simpset() addsimps [adm_trick_1]) 1);
(* base cases *)
by (Simp_tac 1);
by (Simp_tac 1);
(* main case *)
-by (asm_full_simp_tac (!simpset setloop split_If_tac) 1);
+by (asm_full_simp_tac (simpset() setloop split_If_tac) 1);
qed"sforallPstakewhileP";
goal thy "sforall P (sfilter`P`x)";
-by (simp_tac (!simpset addsimps [sforall_def]) 1);
+by (simp_tac (simpset() addsimps [sforall_def]) 1);
by (res_inst_tac[("x","x")] seq.ind 1);
(* adm *)
(* FIX should be refined in _one_ tactic *)
-by (simp_tac (!simpset addsimps [adm_trick_1]) 1);
+by (simp_tac (simpset() addsimps [adm_trick_1]) 1);
(* base cases *)
by (Simp_tac 1);
by (Simp_tac 1);
(* main case *)
-by (asm_full_simp_tac (!simpset setloop split_If_tac) 1);
+by (asm_full_simp_tac (simpset() setloop split_If_tac) 1);
qed"forallPsfilterP";
@@ -413,7 +413,7 @@
goal thy "Finite x --> a~=UU --> x=a##xs --> Finite xs";
by (strip_tac 1);
by (etac sfinite.elim 1);
-by (fast_tac (HOL_cs addss !simpset) 1);
+by (fast_tac (HOL_cs addss simpset()) 1);
by (fast_tac (HOL_cs addSDs seq.injects) 1);
qed"Finite_cons_a";
@@ -471,13 +471,13 @@
------------------------------------------------------------------ *)
goal thy "seq_finite nil";
-by (simp_tac (!simpset addsimps [seq.sfinite_def]) 1);
+by (simp_tac (simpset() addsimps [seq.sfinite_def]) 1);
by (res_inst_tac [("x","Suc 0")] exI 1);
-by (simp_tac (!simpset addsimps seq.rews) 1);
+by (simp_tac (simpset() addsimps seq.rews) 1);
qed"seq_finite_nil";
goal thy "seq_finite UU";
-by (simp_tac (!simpset addsimps [seq.sfinite_def]) 1);
+by (simp_tac (simpset() addsimps [seq.sfinite_def]) 1);
qed"seq_finite_UU";
Addsimps[seq_finite_nil,seq_finite_UU];
@@ -494,9 +494,9 @@
by (rtac (logic_lemma RS mp RS mp) 1);
by (rtac trf_impl_tf 1);
by (rtac seq_finite_ind 1);
-by (simp_tac (!simpset addsimps [Finite_def]) 1);
-by (simp_tac (!simpset addsimps [Finite_def]) 1);
-by (asm_full_simp_tac (!simpset addsimps [Finite_def]) 1);
+by (simp_tac (simpset() addsimps [Finite_def]) 1);
+by (simp_tac (simpset() addsimps [Finite_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Finite_def]) 1);
qed"Finite_ind";
@@ -505,17 +505,17 @@
(* adm *)
(* hier grosses Problem !!!!!!!!!!!!!!! *)
-by (simp_tac (!simpset addsimps [Finite_def]) 2);
-by (simp_tac (!simpset addsimps [Finite_def]) 2);
+by (simp_tac (simpset() addsimps [Finite_def]) 2);
+by (simp_tac (simpset() addsimps [Finite_def]) 2);
(* main case *)
-by (asm_full_simp_tac (!simpset addsimps [Finite_def,seq.sfinite_def]) 2);
+by (asm_full_simp_tac (simpset() addsimps [Finite_def,seq.sfinite_def]) 2);
by (rtac impI 2);
by (rotate_tac 2 2);
by (Asm_full_simp_tac 2);
by (etac exE 2);
by (res_inst_tac [("x","Suc n")] exI 2);
-by (asm_full_simp_tac (!simpset addsimps seq.rews) 2);
+by (asm_full_simp_tac (simpset() addsimps seq.rews) 2);
qed"tf_is_trf";
*)
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Mon Nov 03 14:06:27 1997 +0100
@@ -19,15 +19,15 @@
(* ---------------------------------------------------------------- *)
goal thy "Map f`UU =UU";
-by (simp_tac (!simpset addsimps [Map_def]) 1);
+by (simp_tac (simpset() addsimps [Map_def]) 1);
qed"Map_UU";
goal thy "Map f`nil =nil";
-by (simp_tac (!simpset addsimps [Map_def]) 1);
+by (simp_tac (simpset() addsimps [Map_def]) 1);
qed"Map_nil";
goal thy "Map f`(x>>xs)=(f x) >> Map f`xs";
-by (simp_tac (!simpset addsimps [Map_def, Cons_def,flift2_def]) 1);
+by (simp_tac (simpset() addsimps [Map_def, Cons_def,flift2_def]) 1);
qed"Map_cons";
(* ---------------------------------------------------------------- *)
@@ -35,15 +35,15 @@
(* ---------------------------------------------------------------- *)
goal thy "Filter P`UU =UU";
-by (simp_tac (!simpset addsimps [Filter_def]) 1);
+by (simp_tac (simpset() addsimps [Filter_def]) 1);
qed"Filter_UU";
goal thy "Filter P`nil =nil";
-by (simp_tac (!simpset addsimps [Filter_def]) 1);
+by (simp_tac (simpset() addsimps [Filter_def]) 1);
qed"Filter_nil";
goal thy "Filter P`(x>>xs)= (if P x then x>>(Filter P`xs) else Filter P`xs)";
-by (simp_tac (!simpset addsimps [Filter_def, Cons_def,flift2_def,If_and_if]) 1);
+by (simp_tac (simpset() addsimps [Filter_def, Cons_def,flift2_def,If_and_if]) 1);
qed"Filter_cons";
(* ---------------------------------------------------------------- *)
@@ -51,15 +51,15 @@
(* ---------------------------------------------------------------- *)
goal thy "Forall P UU";
-by (simp_tac (!simpset addsimps [Forall_def,sforall_def]) 1);
+by (simp_tac (simpset() addsimps [Forall_def,sforall_def]) 1);
qed"Forall_UU";
goal thy "Forall P nil";
-by (simp_tac (!simpset addsimps [Forall_def,sforall_def]) 1);
+by (simp_tac (simpset() addsimps [Forall_def,sforall_def]) 1);
qed"Forall_nil";
goal thy "Forall P (x>>xs)= (P x & Forall P xs)";
-by (simp_tac (!simpset addsimps [Forall_def, sforall_def,
+by (simp_tac (simpset() addsimps [Forall_def, sforall_def,
Cons_def,flift2_def]) 1);
qed"Forall_cons";
@@ -69,7 +69,7 @@
goal thy "(x>>xs) @@ y = x>>(xs @@y)";
-by (simp_tac (!simpset addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Cons_def]) 1);
qed"Conc_cons";
(* ---------------------------------------------------------------- *)
@@ -77,15 +77,15 @@
(* ---------------------------------------------------------------- *)
goal thy "Takewhile P`UU =UU";
-by (simp_tac (!simpset addsimps [Takewhile_def]) 1);
+by (simp_tac (simpset() addsimps [Takewhile_def]) 1);
qed"Takewhile_UU";
goal thy "Takewhile P`nil =nil";
-by (simp_tac (!simpset addsimps [Takewhile_def]) 1);
+by (simp_tac (simpset() addsimps [Takewhile_def]) 1);
qed"Takewhile_nil";
goal thy "Takewhile P`(x>>xs)= (if P x then x>>(Takewhile P`xs) else nil)";
-by (simp_tac (!simpset addsimps [Takewhile_def, Cons_def,flift2_def,If_and_if]) 1);
+by (simp_tac (simpset() addsimps [Takewhile_def, Cons_def,flift2_def,If_and_if]) 1);
qed"Takewhile_cons";
(* ---------------------------------------------------------------- *)
@@ -93,15 +93,15 @@
(* ---------------------------------------------------------------- *)
goal thy "Dropwhile P`UU =UU";
-by (simp_tac (!simpset addsimps [Dropwhile_def]) 1);
+by (simp_tac (simpset() addsimps [Dropwhile_def]) 1);
qed"Dropwhile_UU";
goal thy "Dropwhile P`nil =nil";
-by (simp_tac (!simpset addsimps [Dropwhile_def]) 1);
+by (simp_tac (simpset() addsimps [Dropwhile_def]) 1);
qed"Dropwhile_nil";
goal thy "Dropwhile P`(x>>xs)= (if P x then Dropwhile P`xs else x>>xs)";
-by (simp_tac (!simpset addsimps [Dropwhile_def, Cons_def,flift2_def,If_and_if]) 1);
+by (simp_tac (simpset() addsimps [Dropwhile_def, Cons_def,flift2_def,If_and_if]) 1);
qed"Dropwhile_cons";
(* ---------------------------------------------------------------- *)
@@ -110,17 +110,17 @@
goal thy "Last`UU =UU";
-by (simp_tac (!simpset addsimps [Last_def]) 1);
+by (simp_tac (simpset() addsimps [Last_def]) 1);
qed"Last_UU";
goal thy "Last`nil =UU";
-by (simp_tac (!simpset addsimps [Last_def]) 1);
+by (simp_tac (simpset() addsimps [Last_def]) 1);
qed"Last_nil";
goal thy "Last`(x>>xs)= (if xs=nil then Def x else Last`xs)";
-by (simp_tac (!simpset addsimps [Last_def, Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Last_def, Cons_def]) 1);
by (res_inst_tac [("x","xs")] seq.casedist 1);
-by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
by (REPEAT (Asm_simp_tac 1));
qed"Last_cons";
@@ -130,15 +130,15 @@
(* ---------------------------------------------------------------- *)
goal thy "Flat`UU =UU";
-by (simp_tac (!simpset addsimps [Flat_def]) 1);
+by (simp_tac (simpset() addsimps [Flat_def]) 1);
qed"Flat_UU";
goal thy "Flat`nil =nil";
-by (simp_tac (!simpset addsimps [Flat_def]) 1);
+by (simp_tac (simpset() addsimps [Flat_def]) 1);
qed"Flat_nil";
goal thy "Flat`(x##xs)= x @@ (Flat`xs)";
-by (simp_tac (!simpset addsimps [Flat_def, Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Flat_def, Cons_def]) 1);
qed"Flat_cons";
@@ -181,7 +181,7 @@
goal thy "Zip`(x>>xs)`nil= UU";
by (stac Zip_unfold 1);
-by (simp_tac (!simpset addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Cons_def]) 1);
qed"Zip_cons_nil";
goal thy "Zip`(x>>xs)`(y>>ys)= (x,y) >> Zip`xs`ys";
@@ -190,7 +190,7 @@
by (Simp_tac 1);
(* FIX: Why Simp_tac 2 times. Does continuity in simpflication make job sometimes not
completely ready ? *)
-by (simp_tac (!simpset addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Cons_def]) 1);
qed"Zip_cons";
@@ -240,11 +240,11 @@
section "Cons";
goal thy "a>>s = (Def a)##s";
-by (simp_tac (!simpset addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Cons_def]) 1);
qed"Cons_def2";
goal thy "x = UU | x = nil | (? a s. x = a >> s)";
-by (simp_tac (!simpset addsimps [Cons_def2]) 1);
+by (simp_tac (simpset() addsimps [Cons_def2]) 1);
by (cut_facts_tac [seq.exhaust] 1);
by (fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1]) 1);
qed"Seq_exhaust";
@@ -279,7 +279,7 @@
by (rtac notI 1);
by (dtac antisym_less 1);
by (Simp_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_not_UU]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_not_UU]) 1);
qed"Cons_not_less_UU";
goal thy "~a>>s << nil";
@@ -294,7 +294,7 @@
qed"Cons_not_nil";
goal thy "nil ~= a>>s";
-by (simp_tac (!simpset addsimps [Cons_def2]) 1);
+by (simp_tac (simpset() addsimps [Cons_def2]) 1);
qed"Cons_not_nil2";
goal thy "(a>>s = b>>t) = (a = b & s = t)";
@@ -306,7 +306,7 @@
qed"Cons_inject_eq";
goal thy "(a>>s<<b>>t) = (a = b & s<<t)";
-by (simp_tac (!simpset addsimps [Cons_def2]) 1);
+by (simp_tac (simpset() addsimps [Cons_def2]) 1);
by (stac (Def_inject_less_eq RS sym) 1);
back();
by (rtac iffI 1);
@@ -320,7 +320,7 @@
qed"Cons_inject_less_eq";
goal thy "seq_take (Suc n)`(a>>x) = a>> (seq_take n`x)";
-by (simp_tac (!simpset addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Cons_def]) 1);
qed"seq_take_Cons";
Addsimps [Cons_not_nil2,Cons_inject_eq,Cons_inject_less_eq,seq_take_Cons,
@@ -343,7 +343,7 @@
by (etac seq.ind 1);
by (REPEAT (atac 1));
by (def_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
qed"Seq_induct";
goal thy "!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |] \
@@ -351,21 +351,21 @@
by (etac seq_finite_ind 1);
by (REPEAT (atac 1));
by (def_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
qed"Seq_FinitePartial_ind";
goal thy "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x";
by (etac sfinite.induct 1);
by (assume_tac 1);
by (def_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
qed"Seq_Finite_ind";
(* rws are definitions to be unfolded for admissibility check *)
fun Seq_induct_tac s rws i = res_inst_tac [("x",s)] Seq_induct i
THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac (i+1))))
- THEN simp_tac (!simpset addsimps rws) i;
+ THEN simp_tac (simpset() addsimps rws) i;
fun Seq_Finite_induct_tac i = etac Seq_Finite_ind i
THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac i)));
@@ -378,7 +378,7 @@
res_inst_tac [("x",s)] Seq_induct i
THEN pair_tac "a" (i+3)
THEN (REPEAT_DETERM (CHANGED (Simp_tac (i+1))))
- THEN simp_tac (!simpset addsimps rws) i;
+ THEN simp_tac (simpset() addsimps rws) i;
@@ -387,11 +387,11 @@
section "HD,TL";
goal thy "HD`(x>>y) = Def x";
-by (simp_tac (!simpset addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Cons_def]) 1);
qed"HD_Cons";
goal thy "TL`(x>>y) = y";
-by (simp_tac (!simpset addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Cons_def]) 1);
qed"TL_Cons";
Addsimps [HD_Cons,TL_Cons];
@@ -401,7 +401,7 @@
section "Finite, Partial, Infinite";
goal thy "Finite (a>>xs) = Finite xs";
-by (simp_tac (!simpset addsimps [Cons_def2,Finite_cons]) 1);
+by (simp_tac (simpset() addsimps [Cons_def2,Finite_cons]) 1);
qed"Finite_Cons";
Addsimps [Finite_Cons];
@@ -421,7 +421,7 @@
by (strip_tac 1);
by (Seq_case_simp_tac "x" 1);
by (Seq_case_simp_tac "y" 1);
-by (SELECT_GOAL (auto_tac (!claset,!simpset))1);
+by (SELECT_GOAL (auto_tac (claset(),simpset()))1);
by (eres_inst_tac [("x","sa")] allE 1);
by (eres_inst_tac [("x","y")] allE 1);
by (Asm_full_simp_tac 1);
@@ -463,7 +463,7 @@
goal thy "!! s. Finite s ==> Finite (Filter P`s)";
by (Seq_Finite_induct_tac 1);
-by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
qed"FiniteFilter";
@@ -545,12 +545,12 @@
goal thy "!! s. Finite s ==> s~=nil --> Last`s~=UU";
by (Seq_Finite_induct_tac 1);
-by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
qed"Finite_Last1";
goal thy "!! s. Finite s ==> Last`s=UU --> s=nil";
by (Seq_Finite_induct_tac 1);
-by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
by (fast_tac HOL_cs 1);
qed"Finite_Last2";
@@ -563,11 +563,11 @@
goal thy "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
by (Seq_induct_tac "s" [Filter_def] 1);
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
qed"FilterPQ";
goal thy "Filter P`(x @@ y) = (Filter P`x @@ Filter P`y)";
-by (simp_tac (!simpset addsimps [Filter_def,sfiltersconc]) 1);
+by (simp_tac (simpset() addsimps [Filter_def,sfiltersconc]) 1);
qed"FilterConc";
(* ------------------------------------------------------------------------------------ *)
@@ -584,7 +584,7 @@
goal thy "Filter P`(Map f`x) = Map f`(Filter (P o f)`x)";
by (Seq_induct_tac "x" [] 1);
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
qed"MapFilter";
goal thy "nil = (Map f`s) --> s= nil";
@@ -629,7 +629,7 @@
goal thy "Forall P s --> Forall P (Dropwhile Q`s)";
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
-by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
qed"ForallDropwhile1";
bind_thm ("ForallDropwhile",ForallDropwhile1 RS mp);
@@ -666,7 +666,7 @@
goal thy "Forall P (Filter P`x)";
-by (simp_tac (!simpset addsimps [Filter_def,Forall_def,forallPsfilterP]) 1);
+by (simp_tac (simpset() addsimps [Filter_def,Forall_def,forallPsfilterP]) 1);
qed"ForallPFilterP";
(* holds also in other direction, then equal to forallPfilterP *)
@@ -707,7 +707,7 @@
by (Simp_tac 1);
by (Simp_tac 1);
(* main case *)
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
qed"FilternPnilForallP1";
bind_thm ("FilternPnilForallP",FilternPnilForallP1 RS mp);
@@ -716,12 +716,12 @@
goal thy "!! ys. Finite ys ==> Filter P`ys ~= UU";
by (Seq_Finite_induct_tac 1);
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
qed"FilterUU_nFinite_lemma1";
goal thy "~ Forall (%x. ~P x) ys --> Filter P`ys ~= UU";
by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
qed"FilterUU_nFinite_lemma2";
goal thy "!! P. Filter P`ys = UU ==> \
@@ -729,7 +729,7 @@
by (rtac conjI 1);
by (cut_inst_tac [] (FilterUU_nFinite_lemma2 RS mp COMP rev_contrapos) 1);
by (Auto_tac());
-by (blast_tac (!claset addSDs [FilterUU_nFinite_lemma1]) 1);
+by (blast_tac (claset() addSDs [FilterUU_nFinite_lemma1]) 1);
qed"FilternPUUForallP";
@@ -755,7 +755,7 @@
goal thy "Forall P (Takewhile P`x)";
-by (simp_tac (!simpset addsimps [Forall_def,Takewhile_def,sforallPstakewhileP]) 1);
+by (simp_tac (simpset() addsimps [Forall_def,Takewhile_def,sforallPstakewhileP]) 1);
qed"ForallPTakewhileP";
@@ -787,7 +787,7 @@
goal thy "Takewhile P`(Takewhile P`s) = Takewhile P`s";
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
-by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
qed"Takewhile_idempotent";
goal thy "Forall P s --> Takewhile (%x. Q x | (~P x))`s = Takewhile Q`s";
@@ -903,7 +903,7 @@
goal thy "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 = seq_take k`y2|] \
\ ==> seq_take n`(x @@ (s>>y1)) = seq_take n`(y @@ (t>>y2))";
-by (auto_tac (!claset addSIs [take_reduction1 RS spec RS mp],!simpset));
+by (auto_tac (claset() addSIs [take_reduction1 RS spec RS mp],simpset()));
qed"take_reduction";
(* ------------------------------------------------------------------
@@ -924,7 +924,7 @@
goal thy "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 << seq_take k`y2|] \
\ ==> seq_take n`(x @@ (s>>y1)) << seq_take n`(y @@ (t>>y2))";
-by (auto_tac (!claset addSIs [take_reduction_less1 RS spec RS mp],!simpset));
+by (auto_tac (claset() addSIs [take_reduction_less1 RS spec RS mp],simpset()));
qed"take_reduction_less";
@@ -962,7 +962,7 @@
\ ==> (f (s1 @@ y>>s2)) = (g (s1 @@ y>>s2)) |] \
\ ==> A x --> (f x)=(g x)";
by (case_tac "Forall Q x" 1);
-by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
+by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
qed"take_lemma_principle1";
goal thy "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
@@ -971,7 +971,7 @@
\ = seq_take n`(g (s1 @@ y>>s2)) |] \
\ ==> A x --> (f x)=(g x)";
by (case_tac "Forall Q x" 1);
-by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
+by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
by (resolve_tac seq.take_lemmas 1);
by (Auto_tac());
qed"take_lemma_principle2";
@@ -1001,9 +1001,9 @@
by (Simp_tac 1);
by (rtac allI 1);
by (case_tac "Forall Q xa" 1);
-by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
- !simpset)) 1);
-by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
+by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
+ simpset())) 1);
+by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
qed"take_lemma_induct";
@@ -1022,9 +1022,9 @@
by (rtac less_induct 1);
by (rtac allI 1);
by (case_tac "Forall Q xa" 1);
-by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
- !simpset)) 1);
-by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
+by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
+ simpset())) 1);
+by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
qed"take_lemma_less_induct";
@@ -1076,9 +1076,9 @@
by (rtac less_induct 1);
by (rtac allI 1);
by (case_tac "Forall Q xa" 1);
-by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
- !simpset)) 1);
-by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
+by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
+ simpset())) 1);
+by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
qed"take_lemma_less_induct";
@@ -1103,9 +1103,9 @@
by (rtac less_induct 1);
by (rtac allI 1);
by (case_tac "Forall Q xa" 1);
-by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
- !simpset)) 1);
-by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
+by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
+ simpset())) 1);
+by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
qed"take_lemma_less_induct";
@@ -1151,21 +1151,21 @@
\ Filter (%x. P x & Q x)`s";
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
qed"Filter_lemma1";
goal thy "!! s. Finite s ==> \
\ (Forall (%x. (~P x) | (~ Q x)) s \
\ --> Filter P`(Filter Q`s) = nil)";
by (Seq_Finite_induct_tac 1);
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
qed"Filter_lemma2";
goal thy "!! s. Finite s ==> \
\ Forall (%x. (~P x) | (~ Q x)) s \
\ --> Filter (%x. P x & Q x)`s = nil";
by (Seq_Finite_induct_tac 1);
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
qed"Filter_lemma3";
@@ -1175,8 +1175,8 @@
(take_lemma_induct RS mp) 1);
(* FIX: better support for A = %x. True *)
by (Fast_tac 3);
-by (asm_full_simp_tac (!simpset addsimps [Filter_lemma1]) 1);
-by (asm_full_simp_tac (!simpset addsimps [Filter_lemma2,Filter_lemma3]
+by (asm_full_simp_tac (simpset() addsimps [Filter_lemma1]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Filter_lemma2,Filter_lemma3]
setloop split_tac [expand_if]) 1);
qed"FilterPQ_takelemma";
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Mon Nov 03 14:06:27 1997 +0100
@@ -49,8 +49,8 @@
\ @@ (x>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`t))";
by (rtac trans 1);
by (stac oraclebuild_unfold 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
-by (simp_tac (!simpset addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
+by (simp_tac (simpset() addsimps [Cons_def]) 1);
qed"oraclebuild_cons";
@@ -64,7 +64,7 @@
"!! s. [| Forall (%a.~ P a) s; Finite s|] \
\ ==> Cut P s =nil";
by (subgoal_tac "Filter P`s = nil" 1);
-by (asm_simp_tac (!simpset addsimps [oraclebuild_nil]) 1);
+by (asm_simp_tac (simpset() addsimps [oraclebuild_nil]) 1);
by (rtac ForallQFilterPnil 1);
by (REPEAT (atac 1));
qed"Cut_nil";
@@ -73,7 +73,7 @@
"!! s. [| Forall (%a.~ P a) s; ~Finite s|] \
\ ==> Cut P s =UU";
by (subgoal_tac "Filter P`s= UU" 1);
-by (asm_simp_tac (!simpset addsimps [oraclebuild_UU]) 1);
+by (asm_simp_tac (simpset() addsimps [oraclebuild_UU]) 1);
by (rtac ForallQFilterPUU 1);
by (REPEAT (atac 1));
qed"Cut_UU";
@@ -83,7 +83,7 @@
\ ==> Cut P (ss @@ (t>> rs)) \
\ = ss @@ (t >> Cut P rs)";
-by (asm_full_simp_tac (!simpset addsimps [ForallQFilterPnil,oraclebuild_cons,
+by (asm_full_simp_tac (simpset() addsimps [ForallQFilterPnil,oraclebuild_cons,
TakewhileConc,DropwhileConc]) 1);
qed"Cut_Cons";
@@ -100,12 +100,12 @@
(take_lemma_induct RS mp) 1);
by (Fast_tac 3);
by (case_tac "Finite s" 1);
-by (asm_full_simp_tac (!simpset addsimps [Cut_nil,
+by (asm_full_simp_tac (simpset() addsimps [Cut_nil,
ForallQFilterPnil]) 1);
-by (asm_full_simp_tac (!simpset addsimps [Cut_UU,
+by (asm_full_simp_tac (simpset() addsimps [Cut_UU,
ForallQFilterPUU]) 1);
(* main case *)
-by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,ForallQFilterPnil]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,ForallQFilterPnil]) 1);
by (Auto_tac());
qed"FilterCut";
@@ -117,12 +117,12 @@
(take_lemma_less_induct RS mp) 1);
by (Fast_tac 3);
by (case_tac "Finite s" 1);
-by (asm_full_simp_tac (!simpset addsimps [Cut_nil,
+by (asm_full_simp_tac (simpset() addsimps [Cut_nil,
ForallQFilterPnil]) 1);
-by (asm_full_simp_tac (!simpset addsimps [Cut_UU,
+by (asm_full_simp_tac (simpset() addsimps [Cut_UU,
ForallQFilterPUU]) 1);
(* main case *)
-by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,ForallQFilterPnil]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,ForallQFilterPnil]) 1);
by (rtac take_reduction 1);
by (Auto_tac());
qed"Cut_idemp";
@@ -135,17 +135,17 @@
(take_lemma_less_induct RS mp) 1);
by (Fast_tac 3);
by (case_tac "Finite s" 1);
-by (asm_full_simp_tac (!simpset addsimps [Cut_nil]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cut_nil]) 1);
by (rtac (Cut_nil RS sym) 1);
-by (asm_full_simp_tac (!simpset addsimps [ForallMap,o_def]) 1);
-by (asm_full_simp_tac (!simpset addsimps [Map2Finite]) 1);
+by (asm_full_simp_tac (simpset() addsimps [ForallMap,o_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Map2Finite]) 1);
(* csae ~ Finite s *)
-by (asm_full_simp_tac (!simpset addsimps [Cut_UU]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cut_UU]) 1);
by (rtac (Cut_UU RS sym) 1);
-by (asm_full_simp_tac (!simpset addsimps [ForallMap,o_def]) 1);
-by (asm_full_simp_tac (!simpset addsimps [Map2Finite]) 1);
+by (asm_full_simp_tac (simpset() addsimps [ForallMap,o_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Map2Finite]) 1);
(* main case *)
-by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,MapConc,
+by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,MapConc,
ForallMap,FiniteMap1,o_def]) 1);
by (rtac take_reduction 1);
by (Auto_tac());
@@ -165,13 +165,13 @@
ren "na n s" 1;
by (case_tac "Forall (%x. ~ P x) s" 1);
by (rtac (take_lemma_less RS iffD2 RS spec) 1);
-by (asm_full_simp_tac (!simpset addsimps [Cut_UU]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cut_UU]) 1);
(* main case *)
by (dtac divide_Seq3 1);
by (REPEAT (etac exE 1));
by (REPEAT (etac conjE 1));
by (hyp_subst_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [Cut_Cons]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cut_Cons]) 1);
by (rtac take_reduction_less 1);
(* auto makes also reasoning about Finiteness of parts of s ! *)
by (Auto_tac());
@@ -194,13 +194,13 @@
ren "na n s" 1;
by (case_tac "Forall (%x. ~ P x) s" 1);
by (rtac (seq_take_lemma RS iffD2 RS spec) 1);
-by (asm_full_simp_tac (!simpset addsimps [Cut_nil]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cut_nil]) 1);
(* main case *)
by (dtac divide_Seq3 1);
by (REPEAT (etac exE 1));
by (REPEAT (etac conjE 1));
by (hyp_subst_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,Conc_assoc]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,Conc_assoc]) 1);
by (rtac take_reduction 1);
qed_spec_mp"Cut_prefixcl_Finite";
@@ -237,7 +237,7 @@
by (safe_tac set_cs);
by (res_inst_tac [("x","filter_act`(Cut (%a. fst a:ext A) (snd ex))")] exI 1);
-by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
by (pair_tac "ex" 1);
by (safe_tac set_cs);
by (res_inst_tac [("x","(x,Cut (%a. fst a:ext A) y)")] exI 1);
@@ -245,21 +245,21 @@
(* Subgoal 1: Lemma: propagation of execution through Cut *)
-by (asm_full_simp_tac (!simpset addsimps [execThruCut]) 1);
+by (asm_full_simp_tac (simpset() addsimps [execThruCut]) 1);
(* Subgoal 2: Lemma: Filter P s = Filter P (Cut P s) *)
-by (simp_tac (!simpset addsimps [filter_act_def]) 1);
+by (simp_tac (simpset() addsimps [filter_act_def]) 1);
by (subgoal_tac "Map fst`(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst`y)" 1);
by (rtac (rewrite_rule [o_def] MapCut) 2);
-by (asm_full_simp_tac (!simpset addsimps [FilterCut RS sym]) 1);
+by (asm_full_simp_tac (simpset() addsimps [FilterCut RS sym]) 1);
(* Subgoal 3: Lemma: Cut idempotent *)
-by (simp_tac (!simpset addsimps [LastActExtsch_def,filter_act_def]) 1);
+by (simp_tac (simpset() addsimps [LastActExtsch_def,filter_act_def]) 1);
by (subgoal_tac "Map fst`(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst`y)" 1);
by (rtac (rewrite_rule [o_def] MapCut) 2);
-by (asm_full_simp_tac (!simpset addsimps [Cut_idemp]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cut_idemp]) 1);
qed"exists_LastActExtsch";
--- a/src/HOLCF/IOA/meta_theory/Traces.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML Mon Nov 03 14:06:27 1997 +0100
@@ -23,15 +23,15 @@
goal thy "filter_act`UU = UU";
-by (simp_tac (!simpset addsimps [filter_act_def]) 1);
+by (simp_tac (simpset() addsimps [filter_act_def]) 1);
qed"filter_act_UU";
goal thy "filter_act`nil = nil";
-by (simp_tac (!simpset addsimps [filter_act_def]) 1);
+by (simp_tac (simpset() addsimps [filter_act_def]) 1);
qed"filter_act_nil";
goal thy "filter_act`(x>>xs) = (fst x) >> filter_act`xs";
-by (simp_tac (!simpset addsimps [filter_act_def]) 1);
+by (simp_tac (simpset() addsimps [filter_act_def]) 1);
qed"filter_act_cons";
Addsimps [filter_act_UU,filter_act_nil,filter_act_cons];
@@ -42,11 +42,11 @@
(* ---------------------------------------------------------------- *)
goal thy "mk_trace A`UU=UU";
-by (simp_tac (!simpset addsimps [mk_trace_def]) 1);
+by (simp_tac (simpset() addsimps [mk_trace_def]) 1);
qed"mk_trace_UU";
goal thy "mk_trace A`nil=nil";
-by (simp_tac (!simpset addsimps [mk_trace_def]) 1);
+by (simp_tac (simpset() addsimps [mk_trace_def]) 1);
qed"mk_trace_nil";
goal thy "mk_trace A`(at >> xs) = \
@@ -54,7 +54,7 @@
\ then (fst at) >> (mk_trace A`xs) \
\ else mk_trace A`xs)";
-by (asm_full_simp_tac (!simpset addsimps [mk_trace_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [mk_trace_def]) 1);
qed"mk_trace_cons";
Addsimps [mk_trace_UU,mk_trace_nil,mk_trace_cons];
@@ -74,7 +74,7 @@
by (rtac fix_eq2 1);
by (rtac is_exec_fragC_def 1);
by (rtac beta_cfun 1);
-by (simp_tac (!simpset addsimps [flift1_def]) 1);
+by (simp_tac (simpset() addsimps [flift1_def]) 1);
qed"is_exec_fragC_unfold";
goal thy "(is_exec_fragC A`UU) s=UU";
@@ -92,7 +92,7 @@
\ andalso (is_exec_fragC A`xs)(snd pr))";
by (rtac trans 1);
by (stac is_exec_fragC_unfold 1);
-by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
by (Simp_tac 1);
qed"is_exec_fragC_cons";
@@ -105,17 +105,17 @@
(* ---------------------------------------------------------------- *)
goal thy "is_exec_frag A (s, UU)";
-by (simp_tac (!simpset addsimps [is_exec_frag_def]) 1);
+by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1);
qed"is_exec_frag_UU";
goal thy "is_exec_frag A (s, nil)";
-by (simp_tac (!simpset addsimps [is_exec_frag_def]) 1);
+by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1);
qed"is_exec_frag_nil";
goal thy "is_exec_frag A (s, (a,t)>>ex) = \
\ (((s,a,t):trans_of A) & \
\ is_exec_frag A (t, ex))";
-by (simp_tac (!simpset addsimps [is_exec_frag_def]) 1);
+by (simp_tac (simpset() addsimps [is_exec_frag_def]) 1);
qed"is_exec_frag_cons";
@@ -169,14 +169,14 @@
(* main case *)
ren "ss a t" 1;
by (safe_tac set_cs);
-by (REPEAT (asm_full_simp_tac (!simpset addsimps [is_trans_of_def]) 1));
+by (REPEAT (asm_full_simp_tac (simpset() addsimps [is_trans_of_def]) 1));
qed"execfrag_in_sig";
goal thy
"!! A.[| is_trans_of A; x:executions A |] ==> \
\ Forall (%a. a:act A) (filter_act`(snd x))";
-by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
by (pair_tac "x" 1);
by (rtac (execfrag_in_sig RS spec RS mp) 1);
by (Auto_tac());
@@ -186,7 +186,7 @@
"!! A.[| is_trans_of A; x:schedules A |] ==> \
\ Forall (%a. a:act A) x";
-by (fast_tac (!claset addSIs [exec_in_sig]) 1);
+by (fast_tac (claset() addSIs [exec_in_sig]) 1);
qed"scheds_in_sig";
--- a/src/HOLCF/Lift.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Lift.ML Mon Nov 03 14:06:27 1997 +0100
@@ -28,7 +28,7 @@
by (strip_tac 1);
by (res_inst_tac [("x","y")] Lift_cases 1);
by (Asm_simp_tac 1);
-by (fast_tac (HOL_cs addss !simpset) 1);
+by (fast_tac (HOL_cs addss simpset()) 1);
qed"cont_flift1_not_arg";
(* flift1 is continuous in a variable that occurs either
@@ -69,11 +69,11 @@
fun cont_tac i = resolve_tac cont_lemmas2 i;
fun cont_tacR i = REPEAT (cont_tac i);
-fun cont_tacRs i = simp_tac (!simpset addsimps [flift1_def,flift2_def]) i THEN
+fun cont_tacRs i = simp_tac (simpset() addsimps [flift1_def,flift2_def]) i THEN
REPEAT (cont_tac i);
-simpset := !simpset addSolver (K (DEPTH_SOLVE_1 o cont_tac));
+simpset_ref() := simpset() addSolver (K (DEPTH_SOLVE_1 o cont_tac));
@@ -83,19 +83,19 @@
goal thy "flift1 f`(Def x) = (f x)";
-by (simp_tac (!simpset addsimps [flift1_def]) 1);
+by (simp_tac (simpset() addsimps [flift1_def]) 1);
qed"flift1_Def";
goal thy "flift2 f`(Def x) = Def (f x)";
-by (simp_tac (!simpset addsimps [flift2_def]) 1);
+by (simp_tac (simpset() addsimps [flift2_def]) 1);
qed"flift2_Def";
goal thy "flift1 f`UU = UU";
-by (simp_tac (!simpset addsimps [flift1_def]) 1);
+by (simp_tac (simpset() addsimps [flift1_def]) 1);
qed"flift1_UU";
goal thy "flift2 f`UU = UU";
-by (simp_tac (!simpset addsimps [flift2_def]) 1);
+by (simp_tac (simpset() addsimps [flift2_def]) 1);
qed"flift2_UU";
Addsimps [flift1_Def,flift2_Def,flift1_UU,flift2_UU];
--- a/src/HOLCF/Lift2.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Lift2.ML Mon Nov 03 14:06:27 1997 +0100
@@ -21,7 +21,7 @@
(* ------------------------------------------------------------------------ *)
goal Lift2.thy "Undef << x";
-by (simp_tac (!simpset addsimps [inst_lift_po]) 1);
+by (simp_tac (simpset() addsimps [inst_lift_po]) 1);
qed"minimal_lift";
bind_thm ("UU_lift_def",minimal_lift RS minimal2UU RS sym);
@@ -83,7 +83,7 @@
by (etac spec 1);
by (subgoal_tac "!x y. x<<(y::('a)lift) --> x=Undef | x=y" 1);
-by (simp_tac (!simpset addsimps [inst_lift_po]) 2);
+by (simp_tac (simpset() addsimps [inst_lift_po]) 2);
by (rtac (chain_mono2_po RS exE) 1);
by (Fast_tac 1);
by (atac 1);
--- a/src/HOLCF/Lift3.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Lift3.ML Mon Nov 03 14:06:27 1997 +0100
@@ -25,7 +25,7 @@
local
val case1' = prove_goal thy "lift_case f1 f2 UU = f1"
- (fn _ => [simp_tac (!simpset addsimps lift.simps) 1]);
+ (fn _ => [simp_tac (simpset() addsimps lift.simps) 1]);
val case2' = prove_goal thy "lift_case f1 f2 (Def a) = f2 a"
(fn _ => [Simp_tac 1]);
val distinct1' = prove_goal thy "UU ~= Def a"
@@ -125,12 +125,12 @@
by (stac (hd lift.inject RS sym) 1);
back();
by (rtac iffI 1);
-by (asm_full_simp_tac (!simpset addsimps [inst_lift_po] ) 1);
+by (asm_full_simp_tac (simpset() addsimps [inst_lift_po] ) 1);
by (etac (antisym_less_inverse RS conjunct1) 1);
qed"Def_inject_less_eq";
goal thy "Def x << y = (Def x = y)";
-by (simp_tac (!simpset addsimps [less_lift]) 1);
+by (simp_tac (simpset() addsimps [less_lift]) 1);
qed"Def_less_is_eq";
Addsimps [Def_less_is_eq];
@@ -140,7 +140,7 @@
(* ---------------------------------------------------------- *)
goal thy "! x y::'a lift. x << y --> x = UU | x = y";
-by (simp_tac (!simpset addsimps [less_lift]) 1);
+by (simp_tac (simpset() addsimps [less_lift]) 1);
qed"ax_flat_lift";
(* Two specific lemmas for the combination of LCF and HOL terms *)
--- a/src/HOLCF/One.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/One.ML Mon Nov 03 14:06:27 1997 +0100
@@ -37,7 +37,7 @@
fun prover t = prove_goalw thy [ONE_def] t
(fn prems =>
[
- (asm_simp_tac (!simpset addsimps [inst_lift_po]) 1)
+ (asm_simp_tac (simpset() addsimps [inst_lift_po]) 1)
]);
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/Pcpo.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Pcpo.ML Mon Nov 03 14:06:27 1997 +0100
@@ -56,7 +56,7 @@
safe_tac (HOL_cs addSIs [antisym_less]),
fast_tac (HOL_cs addSEs [chain_mono3]) 1,
dtac sym 1,
- fast_tac ((HOL_cs addSEs [is_ub_thelub]) addss !simpset) 1
+ fast_tac ((HOL_cs addSEs [is_ub_thelub]) addss simpset()) 1
]);
@@ -314,7 +314,7 @@
[
cut_facts_tac prems 1,
fast_tac (HOL_cs addss
- (!simpset addsimps [chfin,finite_chain_def])) 1
+ (simpset() addsimps [chfin,finite_chain_def])) 1
]);
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/Porder.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Porder.ML Mon Nov 03 14:06:27 1997 +0100
@@ -70,7 +70,7 @@
[
Safe_tac,
(rtac nat_less_cases 1),
- (ALLGOALS (fast_tac (!claset addIs [refl_less, chain_mono RS mp])))]);
+ (ALLGOALS (fast_tac (claset() addIs [refl_less, chain_mono RS mp])))]);
(* ------------------------------------------------------------------------ *)
(* technical lemmas about lub and is_lub *)
@@ -114,7 +114,7 @@
goal thy "lub{x} = x";
by (rtac thelubI 1);
-by (simp_tac (!simpset addsimps [is_lub,is_ub]) 1);
+by (simp_tac (simpset() addsimps [is_lub,is_ub]) 1);
qed "lub_singleton";
Addsimps [lub_singleton];
--- a/src/HOLCF/Sprod3.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Sprod3.ML Mon Nov 03 14:06:27 1997 +0100
@@ -319,7 +319,7 @@
(fn prems =>
[
(stac beta_cfun 1),
- (simp_tac (!simpset addsimps [cont_Ispair2, cont_Ispair1,
+ (simp_tac (simpset() addsimps [cont_Ispair2, cont_Ispair1,
cont2cont_CF1L]) 1),
(stac beta_cfun 1),
(rtac cont_Ispair2 1),
--- a/src/HOLCF/Ssum0.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Ssum0.ML Mon Nov 03 14:06:27 1997 +0100
@@ -388,6 +388,6 @@
(* instantiate the simplifier *)
(* ------------------------------------------------------------------------ *)
-val Ssum0_ss = (simpset_of "Cfun3") addsimps
+val Ssum0_ss = (simpset_of Cfun3.thy) addsimps
[(strict_IsinlIsinr RS sym),Iwhen1,Iwhen2,Iwhen3];
--- a/src/HOLCF/Ssum2.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Ssum2.ML Mon Nov 03 14:06:27 1997 +0100
@@ -27,25 +27,25 @@
qed_goal "less_ssum3a" thy "Isinl x << Isinl y = x << y"
(fn prems =>
[
- (simp_tac (!simpset addsimps [less_ssum2a]) 1)
+ (simp_tac (simpset() addsimps [less_ssum2a]) 1)
]);
qed_goal "less_ssum3b" thy "Isinr x << Isinr y = x << y"
(fn prems =>
[
- (simp_tac (!simpset addsimps [less_ssum2b]) 1)
+ (simp_tac (simpset() addsimps [less_ssum2b]) 1)
]);
qed_goal "less_ssum3c" thy "Isinl x << Isinr y = (x = UU)"
(fn prems =>
[
- (simp_tac (!simpset addsimps [less_ssum2c]) 1)
+ (simp_tac (simpset() addsimps [less_ssum2c]) 1)
]);
qed_goal "less_ssum3d" thy "Isinr x << Isinl y = (x = UU)"
(fn prems =>
[
- (simp_tac (!simpset addsimps [less_ssum2d]) 1)
+ (simp_tac (simpset() addsimps [less_ssum2d]) 1)
]);
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/Ssum3.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Ssum3.ML Mon Nov 03 14:06:27 1997 +0100
@@ -261,7 +261,7 @@
(res_inst_tac [("t","Y(i)")] ssubst 1),
(atac 1),
(fast_tac HOL_cs 1),
- (simp_tac (simpset_of "Cfun3") 1),
+ (simp_tac (simpset_of Cfun3.thy) 1),
(rtac (monofun_fapp2 RS ch2ch_monofun) 1),
(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
(etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
@@ -325,7 +325,7 @@
(res_inst_tac [("t","Y(i)")] ssubst 1),
(atac 1),
(fast_tac HOL_cs 1),
- (simp_tac (simpset_of "Cfun3") 1),
+ (simp_tac (simpset_of Cfun3.thy) 1),
(rtac (monofun_fapp2 RS ch2ch_monofun) 1),
(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
(etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
@@ -691,9 +691,9 @@
(fn prems =>
[
(res_inst_tac [("p","z")] ssumE 1),
- (asm_simp_tac ((simpset_of "Cfun3") addsimps [sswhen1,sswhen2,sswhen3]) 1),
- (asm_simp_tac ((simpset_of "Cfun3") addsimps [sswhen1,sswhen2,sswhen3]) 1),
- (asm_simp_tac ((simpset_of "Cfun3") addsimps [sswhen1,sswhen2,sswhen3]) 1)
+ (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sswhen1,sswhen2,sswhen3]) 1),
+ (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sswhen1,sswhen2,sswhen3]) 1),
+ (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [sswhen1,sswhen2,sswhen3]) 1)
]);
--- a/src/HOLCF/Tr.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Tr.ML Mon Nov 03 14:06:27 1997 +0100
@@ -16,7 +16,7 @@
[
(lift.induct_tac "t" 1),
(fast_tac HOL_cs 1),
- (fast_tac (HOL_cs addss !simpset) 1)
+ (fast_tac (HOL_cs addss simpset()) 1)
]);
qed_goal "trE" thy
@@ -40,7 +40,7 @@
(fn prems =>
[
(res_inst_tac [("p","y")] trE 1),
- (REPEAT(asm_simp_tac (!simpset addsimps
+ (REPEAT(asm_simp_tac (simpset() addsimps
[o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1))
]);
@@ -129,28 +129,28 @@
qed"andalso_and";
goal thy "(Def x ~=FF)= x";
-by (simp_tac (!simpset addsimps [FF_def]) 1);
+by (simp_tac (simpset() addsimps [FF_def]) 1);
qed"Def_bool1";
goal thy "(Def x = FF) = (~x)";
-by (simp_tac (!simpset addsimps [FF_def]) 1);
+by (simp_tac (simpset() addsimps [FF_def]) 1);
by (fast_tac HOL_cs 1);
qed"Def_bool2";
goal thy "(Def x = TT) = x";
-by (simp_tac (!simpset addsimps [TT_def]) 1);
+by (simp_tac (simpset() addsimps [TT_def]) 1);
qed"Def_bool3";
goal thy "(Def x ~= TT) = (~x)";
-by (simp_tac (!simpset addsimps [TT_def]) 1);
+by (simp_tac (simpset() addsimps [TT_def]) 1);
qed"Def_bool4";
goal thy
"(If Def P then A else B fi)= (if P then A else B)";
by (res_inst_tac [("p","Def P")] trE 1);
by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (!simpset addsimps tr_defs@[flift1_def,o_def]) 1);
-by (asm_full_simp_tac (!simpset addsimps tr_defs@[flift1_def,o_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps tr_defs@[flift1_def,o_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps tr_defs@[flift1_def,o_def]) 1);
qed"If_and_if";
Addsimps [Def_bool1,Def_bool2,Def_bool3,Def_bool4];
--- a/src/HOLCF/Up1.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Up1.ML Mon Nov 03 14:06:27 1997 +0100
@@ -9,7 +9,7 @@
qed_goal "Abs_Up_inverse2" thy "Rep_Up (Abs_Up y) = y"
(fn prems =>
[
- (simp_tac (!simpset addsimps [Up_def,Abs_Up_inverse]) 1)
+ (simp_tac (simpset() addsimps [Up_def,Abs_Up_inverse]) 1)
]);
qed_goalw "Exh_Up" thy [Iup_def ]
@@ -90,7 +90,7 @@
(rtac refl 1)
]);
-val Up0_ss = (simpset_of "Cfun3") addsimps [Ifup1,Ifup2];
+val Up0_ss = (simpset_of Cfun3.thy) addsimps [Ifup1,Ifup2];
qed_goalw "less_up1a" thy [less_up_def]
"Abs_Up(Inl ())<< z"
--- a/src/HOLCF/Up2.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Up2.ML Mon Nov 03 14:06:27 1997 +0100
@@ -26,7 +26,7 @@
qed_goal "minimal_up" thy "Abs_Up(Inl ()) << z"
(fn prems =>
[
- (simp_tac (!simpset addsimps [less_up1a]) 1)
+ (simp_tac (simpset() addsimps [less_up1a]) 1)
]);
bind_thm ("UU_up_def",minimal_up RS minimal2UU RS sym);
@@ -45,13 +45,13 @@
qed_goal "less_up2b" thy "~ Iup(x) << Abs_Up(Inl ())"
(fn prems =>
[
- (simp_tac (!simpset addsimps [less_up1b]) 1)
+ (simp_tac (simpset() addsimps [less_up1b]) 1)
]);
qed_goal "less_up2c" thy "(Iup(x)<<Iup(y)) = (x<<y)"
(fn prems =>
[
- (simp_tac (!simpset addsimps [less_up1c]) 1)
+ (simp_tac (simpset() addsimps [less_up1c]) 1)
]);
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/Up3.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/Up3.ML Mon Nov 03 14:06:27 1997 +0100
@@ -188,7 +188,7 @@
(asm_simp_tac (Up0_ss addsimps [cont_Iup]) 1)
]);
-val tac = (simp_tac (!simpset addsimps [cont_Iup,cont_Ifup1,
+val tac = (simp_tac (simpset() addsimps [cont_Iup,cont_Ifup1,
cont_Ifup2,cont2cont_CF1L]) 1);
qed_goalw "fup1" thy [up_def,fup_def] "fup`f`UU=UU"
@@ -337,8 +337,8 @@
(fn prems =>
[
(res_inst_tac [("p","x")] upE1 1),
- (asm_simp_tac ((simpset_of "Cfun3") addsimps [fup1,fup2]) 1),
- (asm_simp_tac ((simpset_of "Cfun3") addsimps [fup1,fup2]) 1)
+ (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1),
+ (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1)
]);
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/domain/theorems.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/domain/theorems.ML Mon Nov 03 14:06:27 1997 +0100
@@ -373,7 +373,7 @@
(* ----- theorems concerning finite approximation and finite induction ------ *)
local
- val iterate_Cprod_ss = simpset_of "Fix"
+ val iterate_Cprod_ss = simpset_of Fix.thy
addsimps [cfst_strict, csnd_strict]addsimps Cprod_rews;
val copy_con_rews = copy_rews @ con_rews;
val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
--- a/src/HOLCF/ex/Dagstuhl.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/ex/Dagstuhl.ML Mon Nov 03 14:06:27 1997 +0100
@@ -34,10 +34,10 @@
val prems = goal Dagstuhl.thy "YS = YYS";
by (resolve_tac stream.take_lemmas 1);
by (nat_ind_tac "n" 1);
-by (simp_tac (!simpset addsimps stream.rews) 1);
+by (simp_tac (simpset() addsimps stream.rews) 1);
by (stac YS_def2 1);
by (stac YYS_def2 1);
-by (asm_simp_tac (!simpset addsimps stream.rews) 1);
+by (asm_simp_tac (simpset() addsimps stream.rews) 1);
by (rtac (lemma5 RS sym RS subst) 1);
by (rtac refl 1);
val wir_moel=result();
@@ -53,7 +53,7 @@
by (rtac fix_least 1);
by (stac beta_cfun 1);
by (cont_tacR 1);
-by (simp_tac (!simpset addsimps [YS_def2 RS sym]) 1);
+by (simp_tac (simpset() addsimps [YS_def2 RS sym]) 1);
val lemma6=result();
val prems = goal Dagstuhl.thy "YS << YYS";
--- a/src/HOLCF/ex/Dnat.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/ex/Dnat.ML Mon Nov 03 14:06:27 1997 +0100
@@ -56,12 +56,12 @@
(res_inst_tac [("x","y")] dnat.casedist 1),
(fast_tac (HOL_cs addSIs [UU_I]) 1),
(Asm_simp_tac 1),
- (asm_simp_tac (!simpset addsimps dnat.dist_les) 1),
+ (asm_simp_tac (simpset() addsimps dnat.dist_les) 1),
(rtac allI 1),
(res_inst_tac [("x","y")] dnat.casedist 1),
(fast_tac (HOL_cs addSIs [UU_I]) 1),
- (asm_simp_tac (!simpset addsimps dnat.dist_les) 1),
- (asm_simp_tac (!simpset addsimps dnat.rews) 1),
+ (asm_simp_tac (simpset() addsimps dnat.dist_les) 1),
+ (asm_simp_tac (simpset() addsimps dnat.rews) 1),
(strip_tac 1),
(subgoal_tac "d<<da" 1),
(etac allE 1),
--- a/src/HOLCF/ex/Hoare.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/ex/Hoare.ML Mon Nov 03 14:06:27 1997 +0100
@@ -136,7 +136,7 @@
(res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1),
(rtac mp 1),
(etac spec 1),
- (simp_tac (!simpset addsimps [less_Suc_eq]) 1),
+ (simp_tac (simpset() addsimps [less_Suc_eq]) 1),
(simp_tac HOLCF_ss 1),
(etac mp 1),
(strip_tac 1),
@@ -153,7 +153,7 @@
[
(nat_ind_tac "k" 1),
(Simp_tac 1),
-(simp_tac (!simpset addsimps [less_Suc_eq]) 1),
+(simp_tac (simpset() addsimps [less_Suc_eq]) 1),
(strip_tac 1),
(res_inst_tac [("s","q`(iterate k g x)")] trans 1),
(rtac trans 1),
@@ -210,7 +210,7 @@
(simp_tac HOLCF_ss 1),
(rtac trans 1),
(rtac p_def3 1),
- (simp_tac (!simpset delsimps [iterate_Suc]
+ (simp_tac (simpset() delsimps [iterate_Suc]
addsimps [iterate_Suc RS sym]) 1),
(eres_inst_tac [("s","FF")] ssubst 1),
(simp_tac HOLCF_ss 1)
--- a/src/HOLCF/ex/Loop.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/ex/Loop.ML Mon Nov 03 14:06:27 1997 +0100
@@ -119,7 +119,7 @@
(nat_ind_tac "k" 1),
(Asm_simp_tac 1),
(strip_tac 1),
- (simp_tac (!simpset addsimps [step_def2]) 1),
+ (simp_tac (simpset() addsimps [step_def2]) 1),
(res_inst_tac [("p","b`(iterate k (step`b`g) x)")] trE 1),
(etac notE 1),
(asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1),
--- a/src/HOLCF/ex/Stream.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/ex/Stream.ML Mon Nov 03 14:06:27 1997 +0100
@@ -169,14 +169,14 @@
val stream_take_lemma2 = prove_goal thy
"! s2. stream_take n`s2 = s2 --> stream_take (Suc n)`s2=s2" (fn prems => [
(nat_ind_tac "n" 1),
- (simp_tac (!simpset addsimps stream_rews) 1),
+ (simp_tac (simpset() addsimps stream_rews) 1),
(strip_tac 1),
(hyp_subst_tac 1),
- (simp_tac (!simpset addsimps stream_rews) 1),
+ (simp_tac (simpset() addsimps stream_rews) 1),
(rtac allI 1),
(res_inst_tac [("s","s2")] streamE 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
+ (asm_simp_tac (simpset() addsimps stream_rews) 1),
+ (asm_simp_tac (simpset() addsimps stream_rews) 1),
(strip_tac 1 ),
(subgoal_tac "stream_take n1`xs = xs" 1),
(rtac ((hd stream_inject) RS conjunct2) 2),