--- a/src/HOLCF/Fix.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/Fix.ML Mon Apr 27 16:47:50 1998 +0200
@@ -697,7 +697,7 @@
"!!Q. chain(Y) ==> 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 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 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 1,
res_inst_tac [("x","i")] exI 1,
strip_tac 1,
trans_tac 1
--- a/src/HOLCF/IMP/Denotational.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IMP/Denotational.ML Mon Apr 27 16:47:50 1998 +0200
@@ -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() addsplits [split_lift_case]) 1);
qed "dlift_is_Def";
Addsimps [dlift_is_Def];
@@ -33,13 +33,13 @@
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 (Simp_tac 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 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);
--- a/src/HOLCF/IMP/HoareEx.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IMP/HoareEx.ML Mon Apr 27 16:47:50 1998 +0200
@@ -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 1);
by (Blast_tac 1);
qed "WHILE_rule_sound";
--- a/src/HOLCF/IOA/ABP/Correctness.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.ML Mon Apr 27 16:47:50 1998 +0200
@@ -54,7 +54,7 @@
by (REPEAT (rtac allI 1));
by (rtac impI 1);
by (hyp_subst_tac 1);
- by (stac expand_if 1);
+ by (stac split_if 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
val l_iff_red_nil = result();
@@ -72,7 +72,7 @@
by (asm_full_simp_tac list_ss 1);
by (REPEAT (rtac allI 1));
by (rtac impI 1);
-by (stac expand_if 1);
+by (stac split_if 1);
by (REPEAT(hyp_subst_tac 1));
by (etac subst 1);
by (Simp_tac 1);
@@ -91,7 +91,7 @@
by (Asm_full_simp_tac 1);
by (REPEAT (etac exE 1));
by (Asm_simp_tac 1);
-by (stac expand_if 1);
+by (stac split_if 1);
by (hyp_subst_tac 1);
by (asm_full_simp_tac (simpset() addsimps [reverse_Cons]) 1);
qed"rev_red_not_nil";
@@ -104,7 +104,7 @@
by (asm_full_simp_tac list_ss 1);
by (REPEAT (rtac allI 1));
by (rtac impI 1);
- by (stac expand_if 1);
+ by (stac split_if 1);
by (asm_full_simp_tac (list_ss addsimps [reverse_Cons,hd_append,
(rev_red_not_nil RS mp)]) 1);
qed"last_ind_on_first";
@@ -116,7 +116,7 @@
"if x=hd(reverse(reduce(l))) & reduce(l)~=[] then \
\ reduce(l@[x])=reduce(l) else \
\ reduce(l@[x])=reduce(l)@[x]";
-by (stac expand_if 1);
+by (stac split_if 1);
by (rtac conjI 1);
(* --> *)
by (List.list.induct_tac "l" 1);
@@ -136,11 +136,11 @@
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 (Asm_full_simp_tac 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);
+ setloop split_tac [split_if]));
+by (Asm_full_simp_tac 1);
qed"reduce_hd";
@@ -154,7 +154,7 @@
by (Asm_full_simp_tac 1);
by (REPEAT (etac exE 1));
by (Asm_full_simp_tac 1);
-by (stac expand_if 1);
+by (stac split_if 1);
by (rtac conjI 1);
by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe]) 2);
by (Step_tac 1);
@@ -167,7 +167,7 @@
C h a n n e l A b s t r a c t i o n
*******************************************************************)
-Delsplits [expand_if];
+Delsplits [split_if];
goal Correctness.thy
"is_weak_ref_map reduce ch_ioa ch_fin_ioa";
by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
@@ -221,7 +221,7 @@
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] addsplits [split_if])));
qed"sender_unchanged";
(* 2 copies of before *)
@@ -237,7 +237,7 @@
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] addsplits [split_if])));
qed"receiver_unchanged";
goal Correctness.thy
@@ -252,9 +252,9 @@
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] addsplits [split_if])));
qed"env_unchanged";
-Addsplits [expand_if];
+Addsplits [split_if];
goal Correctness.thy "compatible srch_ioa rsch_ioa";
by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1);
--- a/src/HOLCF/IOA/ABP/Lemmas.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/ABP/Lemmas.ML Mon Apr 27 16:47:50 1998 +0200
@@ -16,7 +16,7 @@
val and_de_morgan_and_absorbe = result();
goal HOL.thy "(if C then A else B) --> (A|B)";
-by (stac expand_if 1);
+by (stac split_if 1);
by (Fast_tac 1);
val bool_if_impl_or = result();
--- a/src/HOLCF/IOA/NTP/Correctness.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Correctness.ML Mon Apr 27 16:47:50 1998 +0200
@@ -68,7 +68,7 @@
(* 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() delsplits [expand_if] addsimps
+by (simp_tac (simpset() delsplits [split_if] addsimps
[Correctness.hom_def, cancel_restrict, externals_lemma]) 1);
by (rtac conjI 1);
by (simp_tac ss' 1);
@@ -77,7 +77,7 @@
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 (asm_simp_tac (ss' addsplits [split_if]) 1);
by (forward_tac [inv4] 1);
by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
by (simp_tac ss' 1);
--- a/src/HOLCF/IOA/NTP/Impl.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Impl.ML Mon Apr 27 16:47:50 1998 +0200
@@ -60,12 +60,8 @@
addsimps transitions);
val rename_ss = (ss addsimps unfold_renaming);
-
-
-val tac = asm_simp_tac ((ss addcongs [conj_cong])
- setloop (split_tac [expand_if]));
-val tac_ren = asm_simp_tac ((rename_ss addcongs [conj_cong])
- setloop (split_tac [expand_if]));
+val tac = asm_simp_tac (ss addcongs [conj_cong] addsplits [split_if]);
+val tac_ren = asm_simp_tac (rename_ss addcongs [conj_cong] addsplits [split_if]);
@@ -85,7 +81,7 @@
(* First half *)
by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]
- delsplits [expand_if]) 1);
+ delsplits [split_if]) 1);
by (rtac Action.action.induct 1);
by (EVERY1[tac, tac, tac, tac]);
@@ -103,7 +99,7 @@
(* Now the other half *)
by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]
- delsplits [expand_if]) 1);
+ delsplits [split_if]) 1);
by (rtac Action.action.induct 1);
by (EVERY1[tac, tac]);
@@ -114,7 +110,7 @@
by (REPEAT (etac conjE 1));
by (asm_simp_tac (simpset() addsimps [hdr_sum_def, Multiset.count_def,
Multiset.countm_nonempty_def]
- addsplits [expand_if]) 1);
+ addsplits [split_if]) 1);
(* detour 2 *)
by (tac 1);
by (tac_ren 1);
@@ -124,7 +120,7 @@
Multiset.count_def,
Multiset.countm_nonempty_def,
Multiset.delm_nonempty_def]
- addsplits [expand_if]) 1);
+ addsplits [split_if]) 1);
by (rtac allI 1);
by (rtac conjI 1);
by (rtac impI 1);
@@ -163,7 +159,7 @@
@ sender_projections @ impl_ioas)))
1);
- by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [expand_if]) 1);
+ by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
by (Action.action.induct_tac "a" 1);
(* 10 cases. First 4 are simple, since state doesn't change *)
@@ -224,11 +220,10 @@
(Impl.inv3_def :: (receiver_projections
@ sender_projections @ impl_ioas))) 1);
- by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [expand_if]) 1);
+ by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
by (Action.action.induct_tac "a" 1);
-val tac3 = asm_full_simp_tac (ss addsimps [inv3_def]
- setloop (split_tac [expand_if]));
+val tac3 = asm_full_simp_tac (ss addsimps [inv3_def] addsplits [split_if]);
(* 10 - 8 *)
@@ -291,11 +286,11 @@
(Impl.inv4_def :: (receiver_projections
@ sender_projections @ impl_ioas))) 1);
- by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [expand_if]) 1);
+ by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
by (Action.action.induct_tac "a" 1);
val tac4 = asm_full_simp_tac (ss addsimps [inv4_def]
- setloop (split_tac [expand_if]));
+ setloop (split_tac [split_if]));
(* 10 - 2 *)
--- a/src/HOLCF/IOA/NTP/Lemmas.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Lemmas.ML Mon Apr 27 16:47:50 1998 +0200
@@ -36,7 +36,7 @@
(* Arithmetic *)
goal Arith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))";
-by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [expand_nat_case]) 1);
+by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [split_nat_case]) 1);
by (Blast_tac 1);
qed "pred_suc";
--- a/src/HOLCF/IOA/NTP/Multiset.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Multiset.ML Mon Apr 27 16:47:50 1998 +0200
@@ -15,27 +15,23 @@
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
- [Multiset.count_def,Multiset.countm_nonempty_def]
- setloop (split_tac [expand_if])) 1);
+ [Multiset.count_def,Multiset.countm_nonempty_def]) 1);
qed "count_addm_simp";
goal Multiset.thy "count M y <= count (addm M x) y";
- by (simp_tac (simpset() addsimps [count_addm_simp]
- setloop (split_tac [expand_if])) 1);
+ by (simp_tac (simpset() addsimps [count_addm_simp]) 1);
qed "count_leq_addm";
goalw Multiset.thy [Multiset.count_def]
"count (delm M x) y = (if y=x then count M y - 1 else count M y)";
- by (res_inst_tac [("M","M")] Multiset.induction 1);
- 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 (res_inst_tac [("M","M")] Multiset.induction 1);
+by (asm_simp_tac (simpset()
+ addsimps [Multiset.delm_empty_def,Multiset.countm_empty_def]) 1);
+by (asm_full_simp_tac (simpset()
addsimps [Multiset.delm_nonempty_def,
- Multiset.countm_nonempty_def]
- setloop (split_tac [expand_if])) 1);
- by Safe_tac;
- by (Asm_full_simp_tac 1);
+ Multiset.countm_nonempty_def]) 1);
+by Safe_tac;
+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)";
@@ -50,8 +46,7 @@
by (simp_tac (simpset() addsimps [Multiset.delm_empty_def,
Multiset.countm_empty_def]) 1);
by (asm_simp_tac (simpset() addsimps[Multiset.countm_nonempty_def,
- Multiset.delm_nonempty_def]
- setloop (split_tac [expand_if])) 1);
+ Multiset.delm_nonempty_def]) 1);
qed "countm_spurious_delm";
@@ -62,8 +57,7 @@
Multiset.countm_empty_def]) 1);
by (asm_simp_tac (simpset() addsimps
[Multiset.count_def,Multiset.delm_nonempty_def,
- Multiset.countm_nonempty_def]
- setloop (split_tac [expand_if])) 1);
+ Multiset.countm_nonempty_def]) 1);
qed_spec_mp "pos_count_imp_pos_countm";
goal Multiset.thy
@@ -74,8 +68,7 @@
Multiset.countm_empty_def]) 1);
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]
- addsplits [expand_if]) 1);
+ Multiset.countm_nonempty_def,pos_count_imp_pos_countm]) 1);
qed "countm_done_delm";
--- a/src/HOLCF/IOA/meta_theory/Abstraction.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML Mon Apr 27 16:47:50 1998 +0200
@@ -511,7 +511,7 @@
temp_sat_def, satisfies_def,Next_def]
"!! h. [| temp_strengthening P Q h |]\
\ ==> temp_strengthening (Next P) (Next Q) h";
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (Asm_full_simp_tac 1);
by (safe_tac set_cs);
by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
--- a/src/HOLCF/IOA/meta_theory/Automata.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML Mon Apr 27 16:47:50 1998 +0200
@@ -393,8 +393,7 @@
\ 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]@
- ioa_projections)
- setloop (split_tac [expand_if])) 1);
+ ioa_projections)) 1);
qed "trans_of_par4";
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML Mon Apr 27 16:47:50 1998 +0200
@@ -132,8 +132,7 @@
goal thy "stutter sig (s, (a,t)>>ex) = \
\ ((a~:actions sig --> (s=t)) & stutter sig (t,ex))";
-by (simp_tac (simpset() addsimps [stutter_def]
- setloop (split_tac [expand_if]) ) 1);
+by (simp_tac (simpset() addsimps [stutter_def]) 1);
qed"stutter_cons";
(* ----------------------------------------------------------------------------------- *)
@@ -167,8 +166,7 @@
(* main case *)
ren "ss a t" 1;
by (safe_tac set_cs);
-by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2
- setloop (split_tac [expand_if])) 1));
+by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2) 1));
qed"lemma_1_1a";
@@ -183,8 +181,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
- setloop (split_tac [expand_if])) 1));
+by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2) 1));
qed"lemma_1_1b";
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML Mon Apr 27 16:47:50 1998 +0200
@@ -112,8 +112,7 @@
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]
- setloop (split_tac [expand_if]) ) 1);
+by (simp_tac (simpset() addsimps [mkex_def]) 1);
by (cut_inst_tac [("exA","a>>exA")] mkex2_cons_1 1);
by Auto_tac;
qed"mkex_cons_1";
@@ -121,8 +120,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]
- setloop (split_tac [expand_if]) ) 1);
+by (simp_tac (simpset() addsimps [mkex_def]) 1);
by (cut_inst_tac [("exB","b>>exB")] mkex2_cons_2 1);
by Auto_tac;
qed"mkex_cons_2";
@@ -130,8 +128,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]
- setloop (split_tac [expand_if]) ) 1);
+by (simp_tac (simpset() addsimps [mkex_def]) 1);
by (cut_inst_tac [("exB","b>>exB"),("exA","a>>exA")] mkex2_cons_3 1);
by Auto_tac;
qed"mkex_cons_3";
@@ -216,7 +213,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 1);
by (safe_tac set_cs);
(* Case y:A, y:B *)
@@ -249,7 +246,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,
SELECT_GOAL (safe_tac set_cs),
Seq_case_simp_tac exA,
Seq_case_simp_tac exB,
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Mon Apr 27 16:47:50 1998 +0200
@@ -209,7 +209,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 1);
by (safe_tac set_cs);
(* a: act A; a: act B *)
@@ -479,7 +479,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 1);
by (safe_tac set_cs);
(* Case a:A, a:B *)
--- a/src/HOLCF/IOA/meta_theory/Deadlock.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML Mon Apr 27 16:47:50 1998 +0200
@@ -50,7 +50,7 @@
Needs compositionality on schedule level, input-enabledness, compatibility
and distributivity of is_exec_frag over @@
**********************************************************************************)
-Delsplits [expand_if];
+Delsplits [split_if];
goal thy "!! sch. [| a : local A; Finite sch; sch : schedules (A||B); \
\ Filter (%x. x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
\ ==> (sch @@ a>>nil) : schedules (A||B)";
@@ -83,7 +83,7 @@
by (REPEAT (atac 1));
qed"IOA_deadlock_free";
-Addsplits [expand_if];
+Addsplits [split_if];
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Mon Apr 27 16:47:50 1998 +0200
@@ -129,7 +129,7 @@
(* ------------------------------------------------------
Lemma 1 :Traces coincide
------------------------------------------------------- *)
-Delsplits[expand_if];
+Delsplits[split_if];
goalw thy [corresp_ex_def]
"!!f.[|is_ref_map f C A; ext C = ext A|] ==> \
\ !s. reachable C s & is_exec_frag C (s,xs) --> \
@@ -144,9 +144,9 @@
by (eres_inst_tac [("x","y")] allE 1);
by (Asm_full_simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [move_subprop4]
- setloop split_tac [expand_if] ) 1);
+ addsplits [split_if]) 1);
qed"lemma_1";
-Addsplits[expand_if];
+Addsplits[split_if];
(* ------------------------------------------------------------------ *)
(* The following lemmata contribute to *)
--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML Mon Apr 27 16:47:50 1998 +0200
@@ -68,7 +68,7 @@
by (fast_tac (claset() addDs prems) 1);
val lemma = result();
-Delsplits [expand_if];
+Delsplits [split_if];
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);
@@ -82,7 +82,7 @@
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;
-by (stac expand_if 1);
+by (stac split_if 1);
by (rtac conjI 1);
by (rtac impI 1);
by (etac disjE 1);
@@ -111,6 +111,6 @@
by (forward_tac [reachable_rename] 1);
by Auto_tac;
qed"rename_through_pmap";
-Addsplits [expand_if];
+Addsplits [split_if];
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Mon Apr 27 16:47:50 1998 +0200
@@ -120,7 +120,7 @@
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 (res_inst_tac [("x","xs")] seq.casedist 1);
-by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (Asm_simp_tac 1);
by (REPEAT (Asm_simp_tac 1));
qed"Last_cons";
@@ -699,7 +699,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 1);
qed"FilternPnilForallP1";
bind_thm ("FilternPnilForallP",FilternPnilForallP1 RS mp);
@@ -1158,8 +1158,7 @@
(* 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]
- setloop split_tac [expand_if]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Filter_lemma2,Filter_lemma3]) 1);
qed"FilterPQ_takelemma";
Addsimps [FilterPQ];
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Mon Apr 27 16:47:50 1998 +0200
@@ -156,7 +156,7 @@
Lemma 1 :Traces coincide
------------------------------------------------------- *)
-Delsplits[expand_if];
+Delsplits[split_if];
goal thy
"!!f.[|is_simulation R C A; ext C = ext A|] ==> \
\ !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> \
@@ -177,9 +177,9 @@
by (asm_full_simp_tac (simpset() addsimps
[rewrite_rule [Let_def] move_subprop5_sim,
rewrite_rule [Let_def] move_subprop4_sim]
- setloop split_tac [expand_if] ) 1);
+ addsplits [split_if]) 1);
qed_spec_mp"traces_coincide_sim";
-Addsplits[expand_if];
+Addsplits[split_if];
(* ----------------------------------------------------------- *)
--- a/src/HOLCF/IOA/meta_theory/TL.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/TL.ML Mon Apr 27 16:47:50 1998 +0200
@@ -138,7 +138,7 @@
val tsuffix_TL2 = conjI RS tsuffix_TL;
-Delsplits[expand_if];
+Delsplits[split_if];
goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def,AND_def,Box_def]
"s~=UU & s~=nil --> (s |= [] F .--> (F .& (Next ([] F))))";
auto();
@@ -146,33 +146,33 @@
by (eres_inst_tac [("x","s")] allE 1);
by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_refl])1);
(* []F .--> Next [] F *)
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (asm_full_simp_tac (simpset() addsplits [split_if]) 1);
auto();
bd tsuffix_TL2 1;
by (REPEAT (atac 1));
auto();
qed"LTL1";
-Addsplits[expand_if];
+Addsplits[split_if];
goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def]
"s |= .~ (Next F) .--> (Next (.~ F))";
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (Asm_full_simp_tac 1);
qed"LTL2a";
goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def]
"s |= (Next (.~ F)) .--> (.~ (Next F))";
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (Asm_full_simp_tac 1);
qed"LTL2b";
goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def]
"ex |= (Next (F .--> G)) .--> (Next F) .--> (Next G)";
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (Asm_full_simp_tac 1);
qed"LTL3";
goalw thy [Next_def,satisfies_def,Box_def,NOT_def,IMPLIES_def]
"s |= [] (F .--> Next F) .--> F .--> []F";
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (Asm_full_simp_tac 1);
auto();
--- a/src/HOLCF/IOA/meta_theory/TLS.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/TLS.ML Mon Apr 27 16:47:50 1998 +0200
@@ -84,7 +84,7 @@
\ ==> ex |== (Init (%(s,a,t). P s) .& Init (%(s,a,t). s -a--A-> t) \
\ .--> (Next (Init (%(s,a,t).Q s))))";
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (Asm_full_simp_tac 1);
by (pair_tac "ex" 1);
by (Seq_case_simp_tac "y" 1);
--- a/src/HOLCF/Lift3.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/Lift3.ML Mon Apr 27 16:47:50 1998 +0200
@@ -94,12 +94,6 @@
by (fast_tac (HOL_cs addSEs prems) 1);
qed"Lift_cases";
-goal thy
- "P(lift_case a b x) = ((x=UU --> P a) & (!y. x = Def y --> P(b y)))";
-by (lift.induct_tac "x" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "expand_lift_case";
-
goal thy "(x~=UU)=(? y. x=Def y)";
by (rtac iffI 1);
by (rtac Lift_cases 1);
--- a/src/HOLCF/Sprod0.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/Sprod0.ML Mon Apr 27 16:47:50 1998 +0200
@@ -19,11 +19,11 @@
(EVERY1 [rtac CollectI, rtac exI,rtac exI, rtac refl])
]);
-qed_goal "inj_onto_Abs_Sprod" Sprod0.thy
- "inj_onto Abs_Sprod Sprod"
+qed_goal "inj_on_Abs_Sprod" Sprod0.thy
+ "inj_on Abs_Sprod Sprod"
(fn prems =>
[
- (rtac inj_onto_inverseI 1),
+ (rtac inj_on_inverseI 1),
(etac Abs_Sprod_inverse 1)
]);
@@ -80,7 +80,7 @@
(cut_facts_tac prems 1),
(etac inject_Spair_Rep 1),
(atac 1),
- (etac (inj_onto_Abs_Sprod RS inj_ontoD) 1),
+ (etac (inj_on_Abs_Sprod RS inj_onD) 1),
(rtac SprodI 1),
(rtac SprodI 1)
]);
@@ -132,7 +132,7 @@
[
(cut_facts_tac prems 1),
(rtac defined_Spair_Rep_rev 1),
- (rtac (inj_onto_Abs_Sprod RS inj_ontoD) 1),
+ (rtac (inj_on_Abs_Sprod RS inj_onD) 1),
(atac 1),
(rtac SprodI 1),
(rtac SprodI 1)
--- a/src/HOLCF/Ssum0.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/Ssum0.ML Mon Apr 27 16:47:50 1998 +0200
@@ -30,10 +30,10 @@
(rtac refl 1)
]);
-qed_goal "inj_onto_Abs_Ssum" Ssum0.thy "inj_onto Abs_Ssum Ssum"
+qed_goal "inj_on_Abs_Ssum" Ssum0.thy "inj_on Abs_Ssum Ssum"
(fn prems =>
[
- (rtac inj_onto_inverseI 1),
+ (rtac inj_on_inverseI 1),
(etac Abs_Ssum_inverse 1)
]);
@@ -89,7 +89,7 @@
[
(cut_facts_tac prems 1),
(rtac noteq_SinlSinr_Rep 1),
- (etac (inj_onto_Abs_Ssum RS inj_ontoD) 1),
+ (etac (inj_on_Abs_Ssum RS inj_onD) 1),
(rtac SsumIl 1),
(rtac SsumIr 1)
]);
@@ -184,7 +184,7 @@
[
(cut_facts_tac prems 1),
(rtac inject_Sinl_Rep 1),
- (etac (inj_onto_Abs_Ssum RS inj_ontoD) 1),
+ (etac (inj_on_Abs_Ssum RS inj_onD) 1),
(rtac SsumIl 1),
(rtac SsumIl 1)
]);
@@ -195,7 +195,7 @@
[
(cut_facts_tac prems 1),
(rtac inject_Sinr_Rep 1),
- (etac (inj_onto_Abs_Ssum RS inj_ontoD) 1),
+ (etac (inj_on_Abs_Ssum RS inj_onD) 1),
(rtac SsumIr 1),
(rtac SsumIr 1)
]);
--- a/src/HOLCF/Tr.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/Tr.ML Mon Apr 27 16:47:50 1998 +0200
@@ -99,10 +99,10 @@
"P (If2 Q x y ) = ((Q=UU --> P UU) & (Q=TT --> P x) & (Q=FF --> P y))";
by (res_inst_tac [("p","Q")] trE 1);
by (REPEAT (Asm_full_simp_tac 1));
-qed"expand_If2";
+qed"split_If2";
val split_If_tac =
- simp_tac (HOL_basic_ss addsimps [symmetric If2_def]) THEN' (split_tac [expand_If2]);
+ simp_tac (HOL_basic_ss addsimps [symmetric If2_def]) THEN' (split_tac [split_If2]);