expand_if is now by default part of the simpset.
--- a/src/HOL/IOA/Solve.ML Thu Mar 05 10:47:27 1998 +0100
+++ b/src/HOL/IOA/Solve.ML Fri Mar 06 15:19:29 1998 +0100
@@ -101,9 +101,9 @@
addsplits [expand_if,split_option_case]) 1);
qed"comp2_reachable";
+Delsplits [expand_if];
(* Composition of possibility-mappings *)
-
goalw Solve.thy [is_weak_pmap_def] "!!f g.[| is_weak_pmap f C1 A1 & \
\ externals(asig_of(A1))=externals(asig_of(C1)) &\
\ is_weak_pmap g C2 A2 & \
@@ -207,3 +207,5 @@
by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
by Auto_tac;
qed"rename_through_pmap";
+
+Addsplits [expand_if];
--- a/src/HOL/List.ML Thu Mar 05 10:47:27 1998 +0100
+++ b/src/HOL/List.ML Fri Mar 06 15:19:29 1998 +0100
@@ -479,9 +479,6 @@
by (rtac allI 1);
by (exhaust_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
-by (rtac allI 1);
-by (exhaust_tac "xs" 1);
- by (ALLGOALS Asm_simp_tac);
qed_spec_mp "nth_append";
goal thy "!n. n < length xs --> (map f xs)!n = f(xs!n)";
--- a/src/HOL/MiniML/Generalize.ML Thu Mar 05 10:47:27 1998 +0100
+++ b/src/HOL/MiniML/Generalize.ML Fri Mar 06 15:19:29 1998 +0100
@@ -60,7 +60,6 @@
by (case_tac "nat : free_tv A" 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
-by (Asm_full_simp_tac 1);
qed_spec_mp "new_tv_compatible_gen";
goalw thy [gen_ML_def] "!!A. gen A t = gen_ML A t";
@@ -71,19 +70,18 @@
goal thy "!!S. (free_tv S) Int ((free_tv t) - (free_tv A)) = {} \
\ --> gen ($ S A) ($ S t) = $ S (gen A t)";
-by (typ.induct_tac "t" 1);
-by (strip_tac 1);
-by (case_tac "nat:(free_tv A)" 1);
+by (induct_tac "t" 1);
+ by (strip_tac 1);
+ by (case_tac "nat:(free_tv A)" 1);
+ by (Asm_simp_tac 1);
+ by (Asm_full_simp_tac 1);
+ by (subgoal_tac "nat ~: free_tv S" 1);
+ by (Fast_tac 2);
+ by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def]) 1);
+ by (cut_facts_tac [free_tv_app_subst_scheme_list] 1);
+ by (Fast_tac 1);
by (Asm_simp_tac 1);
-by (Asm_full_simp_tac 1);
-by (subgoal_tac "nat ~: free_tv S" 1);
-by (Fast_tac 2);
-by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def,de_Morgan_disj]) 1);
-by (split_tac [expand_if] 1);
-by (cut_facts_tac [free_tv_app_subst_scheme_list] 1);
-by (Fast_tac 1);
-by (Asm_simp_tac 1);
-by (Best_tac 1);
+by (Blast_tac 1);
qed_spec_mp "gen_subst_commutes";
goal Generalize.thy "free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t";
--- a/src/HOL/simpdata.ML Thu Mar 05 10:47:27 1998 +0100
+++ b/src/HOL/simpdata.ML Fri Mar 06 15:19:29 1998 +0100
@@ -334,13 +334,23 @@
val split_asm_tac = mk_case_split_asm_tac split_tac
(disjE,conjE,exE,contrapos,contrapos2,notnotD);
-infix 4 addsplits;
+infix 4 addsplits delsplits;
+
fun ss addsplits splits =
let fun addsplit(ss,split) =
let val name = "split " ^ const_of_split_thm split
in ss addloop (name,split_tac [split]) end
in foldl addsplit (ss,splits) end;
+fun ss delsplits splits =
+ let fun delsplit(ss,split) =
+ let val name = "split " ^ const_of_split_thm split
+ in ss delloop name end
+ in foldl delsplit (ss,splits) end;
+
+fun Addsplits splits = (simpset_ref() := simpset() addsplits splits);
+fun Delsplits splits = (simpset_ref() := simpset() delsplits splits);
+
qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
(K [split_tac [expand_if] 1, blast_tac HOL_cs 1]);
@@ -385,7 +395,8 @@
setSSolver safe_solver
setSolver unsafe_solver
setmksimps (mksimps mksimps_pairs)
- setmkeqTrue mk_meta_eq_True;
+ setmkeqTrue mk_meta_eq_True
+ addsplits [expand_if];
val HOL_ss =
HOL_basic_ss addsimps
--- a/src/HOLCF/IOA/ABP/Correctness.ML Thu Mar 05 10:47:27 1998 +0100
+++ b/src/HOLCF/IOA/ABP/Correctness.ML Fri Mar 06 15:19:29 1998 +0100
@@ -167,6 +167,7 @@
C h a n n e l A b s t r a c t i o n
*******************************************************************)
+Delsplits [expand_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);
@@ -253,6 +254,7 @@
(* 7 cases *)
by (ALLGOALS (simp_tac ((simpset() addsimps [externals_def]) setloop (split_tac [expand_if]))));
qed"env_unchanged";
+Addsplits [expand_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/NTP/Correctness.ML Thu Mar 05 10:47:27 1998 +0100
+++ b/src/HOLCF/IOA/NTP/Correctness.ML Fri Mar 06 15:19:29 1998 +0100
@@ -66,11 +66,11 @@
(* 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() delsplits [expand_if] 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 (simp_tac ss' 1);
+ by (asm_simp_tac (simpset() addsimps sels) 1);
by (REPEAT(rtac allI 1));
by (rtac imp_conj_lemma 1); (* from lemmas.ML *)
--- a/src/HOLCF/IOA/NTP/Impl.ML Thu Mar 05 10:47:27 1998 +0100
+++ b/src/HOLCF/IOA/NTP/Impl.ML Fri Mar 06 15:19:29 1998 +0100
@@ -84,7 +84,8 @@
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]
+ delsplits [expand_if]) 1);
by (rtac Action.action.induct 1);
by (EVERY1[tac, tac, tac, tac]);
@@ -101,7 +102,8 @@
(* 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]
+ delsplits [expand_if]) 1);
by (rtac Action.action.induct 1);
by (EVERY1[tac, tac]);
@@ -161,7 +163,7 @@
@ sender_projections @ impl_ioas)))
1);
- by (asm_simp_tac (simpset() addsimps impl_ioas) 1);
+ by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [expand_if]) 1);
by (Action.action.induct_tac "a" 1);
(* 10 cases. First 4 are simple, since state doesn't change *)
@@ -222,7 +224,7 @@
(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 delsplits [expand_if]) 1);
by (Action.action.induct_tac "a" 1);
val tac3 = asm_full_simp_tac (ss addsimps [inv3_def]
@@ -297,7 +299,7 @@
(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 delsplits [expand_if]) 1);
by (Action.action.induct_tac "a" 1);
val tac4 = asm_full_simp_tac (ss addsimps [inv4_def]
--- a/src/HOLCF/IOA/NTP/Multiset.ML Thu Mar 05 10:47:27 1998 +0100
+++ b/src/HOLCF/IOA/NTP/Multiset.ML Fri Mar 06 15:19:29 1998 +0100
@@ -39,12 +39,10 @@
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 (etac add_le_mono 1);
- by (asm_full_simp_tac (simpset() addsimps [le_eq_less_or_eq]
- setloop (split_tac [expand_if])) 1);
+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);
+auto();
qed "countm_props";
goal Multiset.thy "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P";
@@ -66,7 +64,7 @@
[Multiset.count_def,Multiset.delm_nonempty_def,
Multiset.countm_nonempty_def]
setloop (split_tac [expand_if])) 1);
-val pos_count_imp_pos_countm = store_thm("pos_count_imp_pos_countm", standard(result() RS mp));
+qed_spec_mp "pos_count_imp_pos_countm";
goal Multiset.thy
"!!P. P(x) ==> 0<count M x --> countm (delm M x) P = pred (countm M P)";
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML Thu Mar 05 10:47:27 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML Fri Mar 06 15:19:29 1998 +0100
@@ -217,17 +217,13 @@
by (pair_induct_tac "xs" [Forall_def,sforall_def,
is_exec_frag_def, stutter_def] 1);
-(* 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]
- setloop (split_tac [expand_if])) 1);
+by (asm_full_simp_tac (simpset() addsimps trans_of_defs1 @ [actions_asig_comp,asig_of_par]) 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 1);
by (rotate_tac ~4 1);
-by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
+by (Asm_full_simp_tac 1);
qed"lemma_1_2";
--- a/src/HOLCF/IOA/meta_theory/Deadlock.ML Thu Mar 05 10:47:27 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML Fri Mar 06 15:19:29 1998 +0100
@@ -50,7 +50,7 @@
Needs compositionality on schedule level, input-enabledness, compatibility
and distributivity of is_exec_frag over @@
**********************************************************************************)
-
+Delsplits [expand_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)";
@@ -59,10 +59,8 @@
by (rtac conjI 1);
(* a : act (A||B) *)
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);
-by (etac out_is_act 2);
+by(blast_tac (claset() addDs [int_is_act,out_is_act]) 2);
+
(* Filter B (sch@@[a]) : schedules B *)
by (case_tac "a:int A" 1);
@@ -76,7 +74,7 @@
(* case a:act B *)
by (Asm_full_simp_tac 1);
by (subgoal_tac "a:out A" 1);
-by (Fast_tac 2);
+by (Blast_tac 2);
by (dtac outAactB_is_inpB 1);
by (assume_tac 1);
by (assume_tac 1);
@@ -85,6 +83,7 @@
by (REPEAT (atac 1));
qed"IOA_deadlock_free";
+Addsplits [expand_if];
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Thu Mar 05 10:47:27 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Fri Mar 06 15:19:29 1998 +0100
@@ -129,7 +129,7 @@
(* ------------------------------------------------------
Lemma 1 :Traces coincide
------------------------------------------------------- *)
-
+Delsplits[expand_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) --> \
@@ -146,7 +146,7 @@
by (asm_full_simp_tac (simpset() addsimps [move_subprop4]
setloop split_tac [expand_if] ) 1);
qed"lemma_1";
-
+Addsplits[expand_if];
(* ------------------------------------------------------------------ *)
(* The following lemmata contribute to *)
--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML Thu Mar 05 10:47:27 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML Fri Mar 06 15:19:29 1998 +0100
@@ -68,7 +68,7 @@
by (fast_tac (claset() addDs prems) 1);
val lemma = result();
-
+Delsplits [expand_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);
@@ -111,5 +111,6 @@
by (forward_tac [reachable_rename] 1);
by Auto_tac;
qed"rename_through_pmap";
+Addsplits [expand_if];
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Thu Mar 05 10:47:27 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Fri Mar 06 15:19:29 1998 +0100
@@ -463,7 +463,6 @@
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);
qed"FiniteFilter";
@@ -545,12 +544,10 @@
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);
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 (fast_tac HOL_cs 1);
qed"Finite_Last2";
@@ -563,7 +560,6 @@
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);
qed"FilterPQ";
goal thy "Filter P`(x @@ y) = (Filter P`x @@ Filter P`y)";
@@ -584,7 +580,6 @@
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);
qed"MapFilter";
goal thy "nil = (Map f`s) --> s= nil";
@@ -629,7 +624,6 @@
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);
qed"ForallDropwhile1";
bind_thm ("ForallDropwhile",ForallDropwhile1 RS mp);
@@ -644,7 +638,7 @@
by (Asm_full_simp_tac 1);
by Auto_tac;
qed"Forall_prefix";
-
+
bind_thm ("Forall_prefixclosed",Forall_prefix RS spec RS mp RS mp);
@@ -716,12 +710,10 @@
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);
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);
qed"FilterUU_nFinite_lemma2";
goal thy "!! P. Filter P`ys = UU ==> \
@@ -787,7 +779,6 @@
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);
qed"Takewhile_idempotent";
goal thy "Forall P s --> Takewhile (%x. Q x | (~P x))`s = Takewhile Q`s";
@@ -830,10 +821,8 @@
by (rtac adm_all 1);
by (Asm_full_simp_tac 1);
by (case_tac "P a" 1);
-by (Asm_full_simp_tac 1);
-by (rtac impI 1);
-by (hyp_subst_tac 1);
-by (Asm_full_simp_tac 1);
+ by (Asm_full_simp_tac 1);
+ by (Blast_tac 1);
(* ~ P a *)
by (Asm_full_simp_tac 1);
qed"divide_Seq_lemma";
@@ -851,9 +840,6 @@
(* Pay attention: is only admissible with chain-finite package to be added to
adm test *)
by (Seq_induct_tac "y" [Forall_def,sforall_def] 1);
-by (case_tac "P a" 1);
-by (Asm_full_simp_tac 1);
-by (Asm_full_simp_tac 1);
qed"nForall_HDFilter";
@@ -1152,21 +1138,18 @@
\ 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);
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);
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);
qed"Filter_lemma3";
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Thu Mar 05 10:47:27 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Fri Mar 06 15:19:29 1998 +0100
@@ -156,6 +156,7 @@
Lemma 1 :Traces coincide
------------------------------------------------------- *)
+Delsplits[expand_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 --> \
@@ -178,6 +179,7 @@
rewrite_rule [Let_def] move_subprop4_sim]
setloop split_tac [expand_if] ) 1);
qed_spec_mp"traces_coincide_sim";
+Addsplits[expand_if];
(* ----------------------------------------------------------- *)
--- a/src/HOLCF/IOA/meta_theory/TL.ML Thu Mar 05 10:47:27 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/TL.ML Fri Mar 06 15:19:29 1998 +0100
@@ -138,7 +138,7 @@
val tsuffix_TL2 = conjI RS tsuffix_TL;
-
+Delsplits[expand_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();
@@ -152,6 +152,7 @@
by (REPEAT (atac 1));
auto();
qed"LTL1";
+Addsplits[expand_if];
goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def]
@@ -188,4 +189,4 @@
(* works only if validT is defined without restriction to s~=UU, s~=nil *)
goal thy "!! P. validT P ==> validT (Next P)";
by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Next_def])1);
-(* qed"NextTauto"; *)
\ No newline at end of file
+(* qed"NextTauto"; *)