# HG changeset patch # User wenzelm # Date 878562387 -3600 # Node ID 71e05eb27fb6ebe75a39d40069817fd8e7fb9f76 # Parent ddd1c18121e04ba8616bd809aaa08107b6ac82ba isatool fixclasimp; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Cfun2.ML --- 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) ]); (* ------------------------------------------------------------------------ *) diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Cfun3.ML --- 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 *) diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Cont.ML --- 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 ]); diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Cprod2.ML --- 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)< [ - (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< (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)" diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Cprod3.ML --- 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) ]); (* ------------------------------------------------------------------------ *) diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Discrete.ML --- 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]; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Discrete1.ML --- 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]; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Fix.ML --- 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 diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Fun2.ML --- 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); diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/HOLCF.ML --- 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(); diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IMP/Denotational.ML --- 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-> 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"; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IMP/HoareEx.ML --- 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"; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/ABP/Correctness.ML --- 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); diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/ABP/Lemmas.ML --- 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); diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/NTP/Abschannel.ML --- 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"; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/NTP/Correctness.ML --- 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"; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/NTP/Impl.ML --- 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] diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/NTP/Lemmas.ML --- 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 = 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); diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/NTP/Multiset.ML --- 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 0 0 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] diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/NTP/Packet.ML --- 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]; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/NTP/Receiver.ML --- 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"; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/NTP/Sender.ML --- 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"; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/meta_theory/Asig.ML --- 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"; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/meta_theory/Automata.ML --- 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 diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/meta_theory/CompoExecs.ML --- 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"; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/meta_theory/CompoScheds.ML --- 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"; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/meta_theory/CompoTraces.ML --- 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"; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/meta_theory/Compositionality.ML --- 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"; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/meta_theory/Deadlock.ML --- 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); diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/meta_theory/RefCorrectness.ML --- 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"; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/meta_theory/RefMappings.ML --- 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); diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/meta_theory/Seq.ML --- 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"; *) diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/meta_theory/Sequence.ML --- 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<>t) = (a = b & s<>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 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 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"; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/meta_theory/ShortExecutions.ML --- 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"; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/IOA/meta_theory/Traces.ML --- 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"; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Lift.ML --- 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]; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Lift2.ML --- 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); diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Lift3.ML --- 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 *) diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/One.ML --- 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) ]); (* ------------------------------------------------------------------------ *) diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Pcpo.ML --- 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 ]); (* ------------------------------------------------------------------------ *) diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Porder.ML --- 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]; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Sprod3.ML --- 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), diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Ssum0.ML --- 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]; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Ssum2.ML --- 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) ]); (* ------------------------------------------------------------------------ *) diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Ssum3.ML --- 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) ]); diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Tr.ML --- 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]; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Up1.ML --- 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" diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Up2.ML --- 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)< [ - (simp_tac (!simpset addsimps [less_up1c]) 1) + (simp_tac (simpset() addsimps [less_up1c]) 1) ]); (* ------------------------------------------------------------------------ *) diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/Up3.ML --- 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) ]); (* ------------------------------------------------------------------------ *) diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/domain/theorems.ML --- 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; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/ex/Dagstuhl.ML --- 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"; diff -r ddd1c18121e0 -r 71e05eb27fb6 src/HOLCF/ex/Dnat.ML --- 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< 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),