expand_if is now by default part of the simpset.
authornipkow
Fri Mar 06 15:19:29 1998 +0100 (1998-03-06)
changeset 4681a331c1f5a23e
parent 4680 c9d352428201
child 4682 ff081854fc86
expand_if is now by default part of the simpset.
src/HOL/IOA/Solve.ML
src/HOL/List.ML
src/HOL/MiniML/Generalize.ML
src/HOL/simpdata.ML
src/HOLCF/IOA/ABP/Correctness.ML
src/HOLCF/IOA/NTP/Correctness.ML
src/HOLCF/IOA/NTP/Impl.ML
src/HOLCF/IOA/NTP/Multiset.ML
src/HOLCF/IOA/meta_theory/CompoExecs.ML
src/HOLCF/IOA/meta_theory/Deadlock.ML
src/HOLCF/IOA/meta_theory/RefCorrectness.ML
src/HOLCF/IOA/meta_theory/RefMappings.ML
src/HOLCF/IOA/meta_theory/Sequence.ML
src/HOLCF/IOA/meta_theory/SimCorrectness.ML
src/HOLCF/IOA/meta_theory/TL.ML
     1.1 --- a/src/HOL/IOA/Solve.ML	Thu Mar 05 10:47:27 1998 +0100
     1.2 +++ b/src/HOL/IOA/Solve.ML	Fri Mar 06 15:19:29 1998 +0100
     1.3 @@ -101,9 +101,9 @@
     1.4                  addsplits [expand_if,split_option_case]) 1);
     1.5  qed"comp2_reachable";
     1.6  
     1.7 +Delsplits [expand_if];
     1.8  
     1.9  (* Composition of possibility-mappings *)
    1.10 -
    1.11  goalw Solve.thy [is_weak_pmap_def] "!!f g.[| is_weak_pmap f C1 A1 & \
    1.12  \               externals(asig_of(A1))=externals(asig_of(C1)) &\
    1.13  \               is_weak_pmap g C2 A2 &  \
    1.14 @@ -207,3 +207,5 @@
    1.15  by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
    1.16  by Auto_tac;
    1.17  qed"rename_through_pmap";
    1.18 +
    1.19 +Addsplits [expand_if];
     2.1 --- a/src/HOL/List.ML	Thu Mar 05 10:47:27 1998 +0100
     2.2 +++ b/src/HOL/List.ML	Fri Mar 06 15:19:29 1998 +0100
     2.3 @@ -479,9 +479,6 @@
     2.4   by (rtac allI 1);
     2.5   by (exhaust_tac "xs" 1);
     2.6    by (ALLGOALS Asm_simp_tac);
     2.7 -by (rtac allI 1);
     2.8 -by (exhaust_tac "xs" 1);
     2.9 - by (ALLGOALS Asm_simp_tac);
    2.10  qed_spec_mp "nth_append";
    2.11  
    2.12  goal thy "!n. n < length xs --> (map f xs)!n = f(xs!n)";
     3.1 --- a/src/HOL/MiniML/Generalize.ML	Thu Mar 05 10:47:27 1998 +0100
     3.2 +++ b/src/HOL/MiniML/Generalize.ML	Fri Mar 06 15:19:29 1998 +0100
     3.3 @@ -60,7 +60,6 @@
     3.4  by (case_tac "nat : free_tv A" 1);
     3.5  by (Asm_simp_tac 1);
     3.6  by (Asm_simp_tac 1);
     3.7 -by (Asm_full_simp_tac 1);
     3.8  qed_spec_mp "new_tv_compatible_gen";
     3.9  
    3.10  goalw thy [gen_ML_def] "!!A. gen A t = gen_ML A t";
    3.11 @@ -71,19 +70,18 @@
    3.12  
    3.13  goal thy "!!S. (free_tv S) Int ((free_tv t) - (free_tv A)) = {} \
    3.14  \          --> gen ($ S A) ($ S t) = $ S (gen A t)";
    3.15 -by (typ.induct_tac "t" 1);
    3.16 -by (strip_tac 1);
    3.17 -by (case_tac "nat:(free_tv A)" 1);
    3.18 +by (induct_tac "t" 1);
    3.19 + by (strip_tac 1);
    3.20 + by (case_tac "nat:(free_tv A)" 1);
    3.21 +  by (Asm_simp_tac 1);
    3.22 + by (Asm_full_simp_tac 1);
    3.23 + by (subgoal_tac "nat ~: free_tv S" 1);
    3.24 +  by (Fast_tac 2);
    3.25 + by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def]) 1);
    3.26 + by (cut_facts_tac [free_tv_app_subst_scheme_list] 1);
    3.27 + by (Fast_tac 1);
    3.28  by (Asm_simp_tac 1);
    3.29 -by (Asm_full_simp_tac 1);
    3.30 -by (subgoal_tac "nat ~: free_tv S" 1);
    3.31 -by (Fast_tac 2);
    3.32 -by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def,de_Morgan_disj]) 1);
    3.33 -by (split_tac [expand_if] 1);
    3.34 -by (cut_facts_tac [free_tv_app_subst_scheme_list] 1);
    3.35 -by (Fast_tac 1);
    3.36 -by (Asm_simp_tac 1);
    3.37 -by (Best_tac 1);
    3.38 +by (Blast_tac 1);
    3.39  qed_spec_mp "gen_subst_commutes";
    3.40  
    3.41  goal Generalize.thy "free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t";
     4.1 --- a/src/HOL/simpdata.ML	Thu Mar 05 10:47:27 1998 +0100
     4.2 +++ b/src/HOL/simpdata.ML	Fri Mar 06 15:19:29 1998 +0100
     4.3 @@ -334,13 +334,23 @@
     4.4  val split_asm_tac = mk_case_split_asm_tac split_tac 
     4.5  			(disjE,conjE,exE,contrapos,contrapos2,notnotD);
     4.6  
     4.7 -infix 4 addsplits;
     4.8 +infix 4 addsplits delsplits;
     4.9 +
    4.10  fun ss addsplits splits =
    4.11    let fun addsplit(ss,split) =
    4.12          let val name = "split " ^ const_of_split_thm split
    4.13          in ss addloop (name,split_tac [split]) end
    4.14    in foldl addsplit (ss,splits) end;
    4.15  
    4.16 +fun ss delsplits splits =
    4.17 +  let fun delsplit(ss,split) =
    4.18 +        let val name = "split " ^ const_of_split_thm split
    4.19 +        in ss delloop name end
    4.20 +  in foldl delsplit (ss,splits) end;
    4.21 +
    4.22 +fun Addsplits splits = (simpset_ref() := simpset() addsplits splits);
    4.23 +fun Delsplits splits = (simpset_ref() := simpset() delsplits splits);
    4.24 +
    4.25  qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
    4.26    (K [split_tac [expand_if] 1, blast_tac HOL_cs 1]);
    4.27  
    4.28 @@ -385,7 +395,8 @@
    4.29  			    setSSolver   safe_solver
    4.30  			    setSolver  unsafe_solver
    4.31  			    setmksimps (mksimps mksimps_pairs)
    4.32 -			    setmkeqTrue mk_meta_eq_True;
    4.33 +			    setmkeqTrue mk_meta_eq_True
    4.34 +                            addsplits [expand_if];
    4.35  
    4.36  val HOL_ss = 
    4.37      HOL_basic_ss addsimps 
     5.1 --- a/src/HOLCF/IOA/ABP/Correctness.ML	Thu Mar 05 10:47:27 1998 +0100
     5.2 +++ b/src/HOLCF/IOA/ABP/Correctness.ML	Fri Mar 06 15:19:29 1998 +0100
     5.3 @@ -167,6 +167,7 @@
     5.4            C h a n n e l   A b s t r a c t i o n
     5.5   *******************************************************************)
     5.6  
     5.7 +Delsplits [expand_if];
     5.8  goal Correctness.thy 
     5.9        "is_weak_ref_map reduce ch_ioa ch_fin_ioa";
    5.10  by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
    5.11 @@ -253,6 +254,7 @@
    5.12  (* 7 cases *)
    5.13  by (ALLGOALS (simp_tac ((simpset() addsimps [externals_def]) setloop (split_tac [expand_if]))));
    5.14  qed"env_unchanged";
    5.15 +Addsplits [expand_if];
    5.16  
    5.17  goal Correctness.thy "compatible srch_ioa rsch_ioa"; 
    5.18  by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1);
     6.1 --- a/src/HOLCF/IOA/NTP/Correctness.ML	Thu Mar 05 10:47:27 1998 +0100
     6.2 +++ b/src/HOLCF/IOA/NTP/Correctness.ML	Fri Mar 06 15:19:29 1998 +0100
     6.3 @@ -66,11 +66,11 @@
     6.4  (* Proof of correctness *)
     6.5  goalw Correctness.thy [Spec.ioa_def, is_weak_ref_map_def]
     6.6    "is_weak_ref_map hom (restrict impl_ioa (externals spec_sig)) spec_ioa";
     6.7 -by (simp_tac (simpset() addsimps 
     6.8 +by (simp_tac (simpset() delsplits [expand_if] addsimps 
     6.9      [Correctness.hom_def, cancel_restrict, externals_lemma]) 1);
    6.10  by (rtac conjI 1);
    6.11 -by (simp_tac ss' 1);
    6.12 -by (asm_simp_tac (simpset() addsimps sels) 1);
    6.13 + by (simp_tac ss' 1);
    6.14 + by (asm_simp_tac (simpset() addsimps sels) 1);
    6.15  by (REPEAT(rtac allI 1));
    6.16  by (rtac imp_conj_lemma 1);   (* from lemmas.ML *)
    6.17  
     7.1 --- a/src/HOLCF/IOA/NTP/Impl.ML	Thu Mar 05 10:47:27 1998 +0100
     7.2 +++ b/src/HOLCF/IOA/NTP/Impl.ML	Fri Mar 06 15:19:29 1998 +0100
     7.3 @@ -84,7 +84,8 @@
     7.4  by (rtac conjI 1); 
     7.5  
     7.6  (* First half *)
     7.7 -by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]) 1);
     7.8 +by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]
     7.9 +                                 delsplits [expand_if]) 1);
    7.10  by (rtac Action.action.induct 1);
    7.11  
    7.12  by (EVERY1[tac, tac, tac, tac]);
    7.13 @@ -101,7 +102,8 @@
    7.14  
    7.15  
    7.16  (* Now the other half *)
    7.17 -by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]) 1);
    7.18 +by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]
    7.19 +                                 delsplits [expand_if]) 1);
    7.20  by (rtac Action.action.induct 1);
    7.21  by (EVERY1[tac, tac]);
    7.22  
    7.23 @@ -161,7 +163,7 @@
    7.24                             @ sender_projections @ impl_ioas)))
    7.25        1);
    7.26  
    7.27 -  by (asm_simp_tac (simpset() addsimps impl_ioas) 1);
    7.28 +  by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [expand_if]) 1);
    7.29    by (Action.action.induct_tac "a" 1);
    7.30  
    7.31    (* 10 cases. First 4 are simple, since state doesn't change *)
    7.32 @@ -222,7 +224,7 @@
    7.33                      (Impl.inv3_def :: (receiver_projections 
    7.34                                         @ sender_projections @ impl_ioas))) 1);
    7.35  
    7.36 -  by (asm_simp_tac (simpset() addsimps impl_ioas) 1);
    7.37 +  by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [expand_if]) 1);
    7.38    by (Action.action.induct_tac "a" 1);
    7.39  
    7.40  val tac3 = asm_full_simp_tac (ss addsimps [inv3_def] 
    7.41 @@ -297,7 +299,7 @@
    7.42                      (Impl.inv4_def :: (receiver_projections 
    7.43                                         @ sender_projections @ impl_ioas))) 1);
    7.44  
    7.45 -  by (asm_simp_tac (simpset() addsimps impl_ioas) 1);
    7.46 +  by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [expand_if]) 1);
    7.47    by (Action.action.induct_tac "a" 1);
    7.48  
    7.49  val tac4 =  asm_full_simp_tac (ss addsimps [inv4_def]
     8.1 --- a/src/HOLCF/IOA/NTP/Multiset.ML	Thu Mar 05 10:47:27 1998 +0100
     8.2 +++ b/src/HOLCF/IOA/NTP/Multiset.ML	Fri Mar 06 15:19:29 1998 +0100
     8.3 @@ -39,12 +39,10 @@
     8.4  qed "count_delm_simp";
     8.5  
     8.6  goal Multiset.thy "!!M. (!x. P(x) --> Q(x)) ==> (countm M P <= countm M Q)";
     8.7 -  by (res_inst_tac [("M","M")] Multiset.induction 1);
     8.8 -  by (simp_tac (simpset() addsimps [Multiset.countm_empty_def]) 1);
     8.9 -  by (simp_tac (simpset() addsimps[Multiset.countm_nonempty_def]) 1);
    8.10 -  by (etac add_le_mono 1);
    8.11 -  by (asm_full_simp_tac (simpset() addsimps [le_eq_less_or_eq]
    8.12 -                                  setloop (split_tac [expand_if])) 1);
    8.13 +by (res_inst_tac [("M","M")] Multiset.induction 1);
    8.14 + by (simp_tac (simpset() addsimps [Multiset.countm_empty_def]) 1);
    8.15 +by (simp_tac (simpset() addsimps[Multiset.countm_nonempty_def]) 1);
    8.16 +auto();
    8.17  qed "countm_props";
    8.18  
    8.19  goal Multiset.thy "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P";
    8.20 @@ -66,7 +64,7 @@
    8.21                         [Multiset.count_def,Multiset.delm_nonempty_def,
    8.22                          Multiset.countm_nonempty_def]
    8.23                      setloop (split_tac [expand_if])) 1);
    8.24 -val pos_count_imp_pos_countm = store_thm("pos_count_imp_pos_countm", standard(result() RS mp));
    8.25 +qed_spec_mp "pos_count_imp_pos_countm";
    8.26  
    8.27  goal Multiset.thy
    8.28     "!!P. P(x) ==> 0<count M x --> countm (delm M x) P = pred (countm M P)";
     9.1 --- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Thu Mar 05 10:47:27 1998 +0100
     9.2 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Fri Mar 06 15:19:29 1998 +0100
     9.3 @@ -217,17 +217,13 @@
     9.4  
     9.5  by (pair_induct_tac "xs" [Forall_def,sforall_def,
     9.6           is_exec_frag_def, stutter_def] 1);
     9.7 -(* main case *)
     9.8 -by (rtac allI 1); 
     9.9 -ren "ss a t s" 1;
    9.10 -by (asm_full_simp_tac (simpset() addsimps trans_of_defs1 @ [actions_asig_comp,asig_of_par]
    9.11 -               setloop (split_tac [expand_if])) 1);
    9.12 +by (asm_full_simp_tac (simpset() addsimps trans_of_defs1 @ [actions_asig_comp,asig_of_par]) 1);
    9.13  by (safe_tac set_cs);
    9.14  (* problem with asm_full_simp_tac: (fst s) = (fst t) is too high in assumption order ! *)
    9.15  by (rotate_tac ~4 1);
    9.16 -by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
    9.17 +by (Asm_full_simp_tac 1);
    9.18  by (rotate_tac ~4 1);
    9.19 -by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
    9.20 +by (Asm_full_simp_tac 1);
    9.21  qed"lemma_1_2";
    9.22  
    9.23  
    10.1 --- a/src/HOLCF/IOA/meta_theory/Deadlock.ML	Thu Mar 05 10:47:27 1998 +0100
    10.2 +++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML	Fri Mar 06 15:19:29 1998 +0100
    10.3 @@ -50,7 +50,7 @@
    10.4      Needs compositionality on schedule level, input-enabledness, compatibility
    10.5                      and distributivity of is_exec_frag over @@
    10.6  **********************************************************************************)
    10.7 -
    10.8 +Delsplits [expand_if];
    10.9  goal thy "!! sch. [| a : local A; Finite sch; sch : schedules (A||B); \
   10.10  \            Filter (%x. x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
   10.11  \          ==> (sch @@ a>>nil) : schedules (A||B)";
   10.12 @@ -59,10 +59,8 @@
   10.13  by (rtac conjI 1);
   10.14  (* a : act (A||B) *)
   10.15  by (asm_full_simp_tac (simpset() addsimps [actions_of_par]) 2);
   10.16 -by (rtac disjI1 2);
   10.17 -by (etac disjE 2);
   10.18 -by (etac int_is_act 2);
   10.19 -by (etac out_is_act 2);
   10.20 +by(blast_tac (claset() addDs [int_is_act,out_is_act]) 2);
   10.21 +
   10.22  (* Filter B (sch@@[a]) : schedules B *)
   10.23  
   10.24  by (case_tac "a:int A" 1);
   10.25 @@ -76,7 +74,7 @@
   10.26  (* case a:act B *)
   10.27  by (Asm_full_simp_tac 1);
   10.28  by (subgoal_tac "a:out A" 1);
   10.29 -by (Fast_tac 2);
   10.30 +by (Blast_tac 2);
   10.31  by (dtac outAactB_is_inpB 1);
   10.32  by (assume_tac 1);
   10.33  by (assume_tac 1);
   10.34 @@ -85,6 +83,7 @@
   10.35  by (REPEAT (atac 1));
   10.36  qed"IOA_deadlock_free";
   10.37  
   10.38 +Addsplits [expand_if];
   10.39  
   10.40  
   10.41  
    11.1 --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Thu Mar 05 10:47:27 1998 +0100
    11.2 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Fri Mar 06 15:19:29 1998 +0100
    11.3 @@ -129,7 +129,7 @@
    11.4  (* ------------------------------------------------------
    11.5                   Lemma 1 :Traces coincide  
    11.6     ------------------------------------------------------- *)
    11.7 -
    11.8 +Delsplits[expand_if];
    11.9  goalw thy [corresp_ex_def]
   11.10    "!!f.[|is_ref_map f C A; ext C = ext A|] ==>  \     
   11.11  \        !s. reachable C s & is_exec_frag C (s,xs) --> \
   11.12 @@ -146,7 +146,7 @@
   11.13  by (asm_full_simp_tac (simpset() addsimps [move_subprop4] 
   11.14                            setloop split_tac [expand_if] ) 1);
   11.15  qed"lemma_1";
   11.16 -
   11.17 +Addsplits[expand_if];
   11.18  
   11.19  (* ------------------------------------------------------------------ *)
   11.20  (*                   The following lemmata contribute to              *)
    12.1 --- a/src/HOLCF/IOA/meta_theory/RefMappings.ML	Thu Mar 05 10:47:27 1998 +0100
    12.2 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML	Fri Mar 06 15:19:29 1998 +0100
    12.3 @@ -68,7 +68,7 @@
    12.4    by (fast_tac (claset() addDs prems) 1);
    12.5  val lemma = result();
    12.6  
    12.7 -
    12.8 +Delsplits [expand_if];
    12.9  goal thy "!!f.[| is_weak_ref_map f C A |]\
   12.10  \                      ==> (is_weak_ref_map f (rename C g) (rename A g))";
   12.11  by (asm_full_simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
   12.12 @@ -111,5 +111,6 @@
   12.13  by (forward_tac  [reachable_rename] 1);
   12.14  by Auto_tac;
   12.15  qed"rename_through_pmap";
   12.16 +Addsplits [expand_if];
   12.17  
   12.18  
    13.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Thu Mar 05 10:47:27 1998 +0100
    13.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Fri Mar 06 15:19:29 1998 +0100
    13.3 @@ -463,7 +463,6 @@
    13.4  
    13.5  goal thy "!! s. Finite s ==> Finite (Filter P`s)";
    13.6  by (Seq_Finite_induct_tac 1);
    13.7 -by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
    13.8  qed"FiniteFilter";
    13.9  
   13.10  
   13.11 @@ -545,12 +544,10 @@
   13.12  
   13.13  goal thy "!! s. Finite s ==> s~=nil --> Last`s~=UU";
   13.14  by (Seq_Finite_induct_tac  1);
   13.15 -by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
   13.16  qed"Finite_Last1";
   13.17  
   13.18  goal thy "!! s. Finite s ==> Last`s=UU --> s=nil";
   13.19  by (Seq_Finite_induct_tac  1);
   13.20 -by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
   13.21  by (fast_tac HOL_cs 1);
   13.22  qed"Finite_Last2";
   13.23  
   13.24 @@ -563,7 +560,6 @@
   13.25  
   13.26  goal thy "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
   13.27  by (Seq_induct_tac "s" [Filter_def] 1);
   13.28 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
   13.29  qed"FilterPQ";
   13.30  
   13.31  goal thy "Filter P`(x @@ y) = (Filter P`x @@ Filter P`y)";
   13.32 @@ -584,7 +580,6 @@
   13.33  
   13.34  goal thy "Filter P`(Map f`x) = Map f`(Filter (P o f)`x)";
   13.35  by (Seq_induct_tac "x" [] 1);
   13.36 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
   13.37  qed"MapFilter";
   13.38  
   13.39  goal thy "nil = (Map f`s) --> s= nil";
   13.40 @@ -629,7 +624,6 @@
   13.41  
   13.42  goal thy "Forall P s  --> Forall P (Dropwhile Q`s)";
   13.43  by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
   13.44 -by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
   13.45  qed"ForallDropwhile1";
   13.46  
   13.47  bind_thm ("ForallDropwhile",ForallDropwhile1 RS mp);
   13.48 @@ -644,7 +638,7 @@
   13.49  by (Asm_full_simp_tac 1);
   13.50  by Auto_tac;
   13.51  qed"Forall_prefix";
   13.52 - 
   13.53 +
   13.54  bind_thm ("Forall_prefixclosed",Forall_prefix RS spec RS mp RS mp);
   13.55  
   13.56  
   13.57 @@ -716,12 +710,10 @@
   13.58  
   13.59  goal thy "!! ys. Finite ys ==> Filter P`ys ~= UU";
   13.60  by (Seq_Finite_induct_tac 1);
   13.61 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
   13.62  qed"FilterUU_nFinite_lemma1";
   13.63  
   13.64  goal thy "~ Forall (%x. ~P x) ys --> Filter P`ys ~= UU";
   13.65  by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
   13.66 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
   13.67  qed"FilterUU_nFinite_lemma2";
   13.68  
   13.69  goal thy   "!! P. Filter P`ys = UU ==> \
   13.70 @@ -787,7 +779,6 @@
   13.71  
   13.72  goal thy "Takewhile P`(Takewhile P`s) = Takewhile P`s";
   13.73  by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
   13.74 -by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
   13.75  qed"Takewhile_idempotent";
   13.76  
   13.77  goal thy "Forall P s --> Takewhile (%x. Q x | (~P x))`s = Takewhile Q`s";
   13.78 @@ -830,10 +821,8 @@
   13.79  by (rtac adm_all 1);
   13.80  by (Asm_full_simp_tac 1); 
   13.81  by (case_tac "P a" 1);
   13.82 -by (Asm_full_simp_tac 1); 
   13.83 -by (rtac impI 1);
   13.84 -by (hyp_subst_tac 1);
   13.85 -by (Asm_full_simp_tac 1); 
   13.86 + by (Asm_full_simp_tac 1); 
   13.87 + by (Blast_tac 1);
   13.88  (* ~ P a *)
   13.89  by (Asm_full_simp_tac 1); 
   13.90  qed"divide_Seq_lemma";
   13.91 @@ -851,9 +840,6 @@
   13.92  (* Pay attention: is only admissible with chain-finite package to be added to 
   13.93          adm test *)
   13.94  by (Seq_induct_tac "y" [Forall_def,sforall_def] 1);
   13.95 -by (case_tac "P a" 1);
   13.96 -by (Asm_full_simp_tac 1); 
   13.97 -by (Asm_full_simp_tac 1); 
   13.98  qed"nForall_HDFilter";
   13.99  
  13.100  
  13.101 @@ -1152,21 +1138,18 @@
  13.102  \             Filter (%x. P x & Q x)`s";
  13.103  
  13.104  by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
  13.105 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
  13.106  qed"Filter_lemma1";
  13.107  
  13.108  goal thy "!! s. Finite s ==>  \
  13.109  \         (Forall (%x. (~P x) | (~ Q x)) s  \
  13.110  \         --> Filter P`(Filter Q`s) = nil)";
  13.111  by (Seq_Finite_induct_tac 1);
  13.112 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
  13.113  qed"Filter_lemma2";
  13.114  
  13.115  goal thy "!! s. Finite s ==>  \
  13.116  \         Forall (%x. (~P x) | (~ Q x)) s  \
  13.117  \         --> Filter (%x. P x & Q x)`s = nil";
  13.118  by (Seq_Finite_induct_tac 1);
  13.119 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
  13.120  qed"Filter_lemma3";
  13.121  
  13.122  
    14.1 --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Thu Mar 05 10:47:27 1998 +0100
    14.2 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Fri Mar 06 15:19:29 1998 +0100
    14.3 @@ -156,6 +156,7 @@
    14.4                   Lemma 1 :Traces coincide  
    14.5     ------------------------------------------------------- *)
    14.6  
    14.7 +Delsplits[expand_if];
    14.8  goal thy 
    14.9    "!!f.[|is_simulation R C A; ext C = ext A|] ==>  \     
   14.10  \        !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> \
   14.11 @@ -178,6 +179,7 @@
   14.12         rewrite_rule [Let_def] move_subprop4_sim] 
   14.13     setloop split_tac [expand_if] ) 1);
   14.14  qed_spec_mp"traces_coincide_sim";
   14.15 +Addsplits[expand_if];
   14.16  
   14.17  
   14.18  (* ----------------------------------------------------------- *)
    15.1 --- a/src/HOLCF/IOA/meta_theory/TL.ML	Thu Mar 05 10:47:27 1998 +0100
    15.2 +++ b/src/HOLCF/IOA/meta_theory/TL.ML	Fri Mar 06 15:19:29 1998 +0100
    15.3 @@ -138,7 +138,7 @@
    15.4  
    15.5  val tsuffix_TL2 = conjI RS tsuffix_TL;
    15.6  
    15.7 -
    15.8 +Delsplits[expand_if];
    15.9  goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def,AND_def,Box_def] 
   15.10     "s~=UU & s~=nil --> (s |= [] F .--> (F .& (Next ([] F))))";
   15.11  auto();
   15.12 @@ -152,6 +152,7 @@
   15.13  by (REPEAT (atac 1));
   15.14  auto();
   15.15  qed"LTL1";
   15.16 +Addsplits[expand_if];
   15.17  
   15.18  
   15.19  goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
   15.20 @@ -188,4 +189,4 @@
   15.21  (* works only if validT is defined without restriction to s~=UU, s~=nil *)
   15.22  goal thy "!! P. validT P ==> validT (Next P)";
   15.23  by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Next_def])1);
   15.24 -(* qed"NextTauto"; *)
   15.25 \ No newline at end of file
   15.26 +(* qed"NextTauto"; *)