# HG changeset patch # User nipkow # Date 889193969 -3600 # Node ID a331c1f5a23e51d7ff887ae907cfc31ebc08f721 # Parent c9d3524282017025802f979211f2ca2d8ed09d01 expand_if is now by default part of the simpset. diff -r c9d352428201 -r a331c1f5a23e src/HOL/IOA/Solve.ML --- 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]; diff -r c9d352428201 -r a331c1f5a23e src/HOL/List.ML --- 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)"; diff -r c9d352428201 -r a331c1f5a23e src/HOL/MiniML/Generalize.ML --- 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"; diff -r c9d352428201 -r a331c1f5a23e src/HOL/simpdata.ML --- 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 diff -r c9d352428201 -r a331c1f5a23e src/HOLCF/IOA/ABP/Correctness.ML --- 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); diff -r c9d352428201 -r a331c1f5a23e src/HOLCF/IOA/NTP/Correctness.ML --- 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 *) diff -r c9d352428201 -r a331c1f5a23e src/HOLCF/IOA/NTP/Impl.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] diff -r c9d352428201 -r a331c1f5a23e src/HOLCF/IOA/NTP/Multiset.ML --- 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 countm (delm M x) P = pred (countm M P)"; diff -r c9d352428201 -r a331c1f5a23e src/HOLCF/IOA/meta_theory/CompoExecs.ML --- 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"; diff -r c9d352428201 -r a331c1f5a23e src/HOLCF/IOA/meta_theory/Deadlock.ML --- 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]; diff -r c9d352428201 -r a331c1f5a23e src/HOLCF/IOA/meta_theory/RefCorrectness.ML --- 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 *) diff -r c9d352428201 -r a331c1f5a23e src/HOLCF/IOA/meta_theory/RefMappings.ML --- 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]; diff -r c9d352428201 -r a331c1f5a23e src/HOLCF/IOA/meta_theory/Sequence.ML --- 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"; diff -r c9d352428201 -r a331c1f5a23e src/HOLCF/IOA/meta_theory/SimCorrectness.ML --- 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]; (* ----------------------------------------------------------- *) diff -r c9d352428201 -r a331c1f5a23e src/HOLCF/IOA/meta_theory/TL.ML --- 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"; *)