# HG changeset patch # User berghofe # Date 1033397295 -7200 # Node ID 55d32e76ef4e136f79cc51cdb036c250780ea9d8 # Parent 2edf034c902a461709967f1b09971baacaaf0df7 Adapted to new simplifier. diff -r 2edf034c902a -r 55d32e76ef4e src/HOL/IMP/Machines.thy --- a/src/HOL/IMP/Machines.thy Mon Sep 30 16:47:03 2002 +0200 +++ b/src/HOL/IMP/Machines.thy Mon Sep 30 16:48:15 2002 +0200 @@ -193,7 +193,7 @@ apply simp apply(rule rev_revD) apply simp - apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj) + apply(simp (no_asm_use) add: neq_Nil_conv append_eq_conv_conj, clarify)+ apply(drule sym) apply simp apply(rule rev_revD) diff -r 2edf034c902a -r 55d32e76ef4e src/HOL/IMPP/Hoare.ML --- a/src/HOL/IMPP/Hoare.ML Mon Sep 30 16:47:03 2002 +0200 +++ b/src/HOL/IMPP/Hoare.ML Mon Sep 30 16:48:15 2002 +0200 @@ -179,7 +179,7 @@ by (Blast_tac 1); (* cut *) by (Blast_tac 1); (* weaken *) by (ALLGOALS (EVERY'[REPEAT o thin_tac "?x : hoare_derivs", - Clarsimp_tac, REPEAT o smp_tac 1])); + Simp_tac, Clarify_tac, REPEAT o smp_tac 1])); by (ALLGOALS (full_simp_tac (simpset() addsimps [triple_valid_def2]))); by (EVERY'[strip_tac, smp_tac 2, Blast_tac] 1); (* conseq *) by (ALLGOALS Clarsimp_tac); (* Skip, Ass, Local *) @@ -273,10 +273,9 @@ by (resolve_tac (premises()(*hoare_derivs.asm*)) 1); by (Fast_tac 1); by (resolve_tac (tl(premises())(*MGT_BodyN*)) 1); -byev[dtac spec 1, etac impE 1, etac impE 2, etac impE 3, dtac spec 4,etac mp 4]; -by (eresolve_tac (tl(tl(tl(premises())))) 4); +byev[dtac spec 1, etac impE 1, etac impE 2, dtac spec 3,etac mp 3]; +by (eresolve_tac (tl(tl(tl(premises())))) 3); by (Fast_tac 1); -by (etac Suc_leD 1); by (dtac finite_subset 1); by (etac finite_imageI 1); by (Asm_simp_tac 1); diff -r 2edf034c902a -r 55d32e76ef4e src/HOL/Induct/LFilter.thy --- a/src/HOL/Induct/LFilter.thy Mon Sep 30 16:47:03 2002 +0200 +++ b/src/HOL/Induct/LFilter.thy Mon Sep 30 16:48:15 2002 +0200 @@ -125,7 +125,6 @@ lemma lfilter_eq_LNil: "lfilter p l = LNil ==> l ~: Domain(findRel p)" apply (auto iff: Domain_findRel_iff) -apply (rotate_tac 1, simp) done lemma lfilter_eq_LCons [rule_format]: diff -r 2edf034c902a -r 55d32e76ef4e src/HOL/Induct/SList.thy --- a/src/HOL/Induct/SList.thy Mon Sep 30 16:47:03 2002 +0200 +++ b/src/HOL/Induct/SList.thy Mon Sep 30 16:48:15 2002 +0200 @@ -875,7 +875,8 @@ apply (erule all_dupE) apply (rule trans) prefer 2 apply assumption -apply (simp add: assoc [THEN spec, THEN spec, THEN spec, THEN sym]) +apply (simp (no_asm_use) add: assoc [THEN spec, THEN spec, THEN spec, THEN sym]) +apply simp done lemma foldl_append_sym: diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/IMP/Equiv.thy --- a/src/ZF/IMP/Equiv.thy Mon Sep 30 16:47:03 2002 +0200 +++ b/src/ZF/IMP/Equiv.thy Mon Sep 30 16:48:15 2002 +0200 @@ -38,7 +38,7 @@ lemma com1: " -c-> sigma' ==> \ C(c)" apply (erule evalc.induct) - apply simp_all + apply (simp_all (no_asm_simp)) txt {* @{text skip} *} apply fast txt {* @{text assign} *} diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/Induct/Multiset.ML --- a/src/ZF/Induct/Multiset.ML Mon Sep 30 16:47:03 2002 +0200 +++ b/src/ZF/Induct/Multiset.ML Mon Sep 30 16:48:15 2002 +0200 @@ -51,13 +51,6 @@ Addsimps [domain_of_fun]; Delrules [domainE]; -(* The following tactic moves the condition `simp_cond' to the begining - of the list of hypotheses and then makes simplifications accordingly *) - -fun rotate_simp_tac simp_cond i = -(dres_inst_tac [("psi", simp_cond)] asm_rl i THEN rotate_tac ~1 i - THEN Asm_full_simp_tac i); - (* A useful simplification rule *) Goal "(f:A -> nat-{0}) <-> f:A->nat&(ALL a:A. f`a:nat & 0 < f`a)"; @@ -73,7 +66,7 @@ "[| multiset(M); mset_of(M)<=A |] ==> M:Mult(A)"; by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff, mset_of_def])); -by (rotate_simp_tac "M:?u" 1); +by (Asm_full_simp_tac 1); by (res_inst_tac [("B1","nat-{0}")] (FiniteFun_mono RS subsetD) 1); by (ALLGOALS(Asm_simp_tac)); by (rtac (Finite_into_Fin RSN (2, Fin_mono RS subsetD) RS fun_FiniteFunI) 1); @@ -157,7 +150,7 @@ by (rewtac mset_of_def); by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [multiset_fun_iff]))); by (ALLGOALS(Clarify_tac)); -by (ALLGOALS(rotate_simp_tac "M:?u")); +by (ALLGOALS Asm_full_simp_tac); by Auto_tac; qed "mset_of_diff"; Addsimps [mset_of_diff]; @@ -341,7 +334,7 @@ "[| multiset(M); a:mset_of(M) |] ==> 0 < mcount(M, a)"; by (Clarify_tac 1); by (rewrite_goals_tac [mcount_def, mset_of_def]); -by (rotate_simp_tac "M:?u" 1); +by (Asm_full_simp_tac 1); by (asm_full_simp_tac (simpset() addsimps [multiset_fun_iff]) 1); qed "mcount_elem"; @@ -441,8 +434,6 @@ by (rtac sym 1 THEN rtac equalityI 1); by (rewrite_goals_tac [mcount_def, mset_of_def]); by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff])); -by (ALLGOALS(rotate_simp_tac "M:?u")); -by (ALLGOALS(rotate_simp_tac "N:?u")); by (ALLGOALS(dres_inst_tac [("x", "x")] spec)); by (case_tac "x:Aa" 2 THEN case_tac "x:A" 1); by Auto_tac; @@ -455,8 +446,6 @@ by (blast_tac (claset() addIs [equality_lemma]) 2); by (rewrite_goals_tac [multiset_def, mset_of_def]); by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff])); -by (rotate_simp_tac "M:?u" 1); -by (rotate_simp_tac "N:?u" 1); by (rtac fun_extension 1); by (Blast_tac 1 THEN Blast_tac 1); by (dres_inst_tac [("x", "x")] spec 1); @@ -535,7 +524,6 @@ by (rewrite_goals_tac [mset_of_def, mcount_def]); by (case_tac "x:A" 1); by Auto_tac; -by (rotate_simp_tac "M:?u" 2); by (subgoal_tac "$# M ` x $+ #-1 = $# M ` x $- $# 1" 1); by (etac ssubst 1); by (rtac int_of_diff 1); @@ -592,9 +580,6 @@ by (auto_tac (claset(), simpset() addsimps [mset_of_def, multiset_def, multiset_fun_iff, msize_def]@prems)); -by (rotate_simp_tac "M:?u" 1); -by (rotate_simp_tac "M:?u" 2); -by (rotate_simp_tac "ALL a:A. ?u(a)" 1); by (subgoal_tac "setsum(%x. $# mcount(M, x), A)=$# succ(x)" 1); by (dtac setsum_succD 1 THEN Auto_tac); by (case_tac "1 , funrestrict(M, A-{a}))" 1); by (rtac fun_cons_funrestrict_eq 2); by (subgoal_tac "cons(a, A-{a}) = A" 2); @@ -660,7 +643,7 @@ by (Blast_tac 1); by (asm_simp_tac (simpset() addsimps [mset_of_def]) 1); by (dres_inst_tac [("b", "if ?u then ?v else ?w")] sym 1); -by (ALLGOALS(rotate_simp_tac "ALL x:A. ?u(x)")); +by (ALLGOALS Asm_full_simp_tac); by (subgoal_tac "{x:A - {a} . 0 < funrestrict(M, A - {x}) ` x} = A - {a}" 1); by (auto_tac (claset() addSIs [setsum_cong], simpset() addsimps [zdiff_eq_iff, @@ -692,7 +675,7 @@ "[| multiset(M); a ~:mset_of(M) |] ==> M +# {#a#} = cons(, M)"; by (auto_tac (claset(), simpset() addsimps [munion_def])); by (rewtac mset_of_def); -by (rotate_simp_tac "M:?u" 1); +by (Asm_full_simp_tac 1); by (rtac fun_extension 1 THEN rtac lam_type 1); by (ALLGOALS(Asm_full_simp_tac)); by (auto_tac (claset(), simpset() @@ -707,7 +690,7 @@ by (auto_tac (claset(), simpset() addsimps [munion_def, multiset_fun_iff, msingle_def])); by (rewtac mset_of_def); -by (rotate_simp_tac "M:?u" 1); +by (Asm_full_simp_tac 1); by (subgoal_tac "A Un {a} = A" 1); by (rtac fun_extension 1); by (auto_tac (claset() addDs [domain_type] @@ -767,7 +750,6 @@ Goalw [multiset_def, mset_of_def] "[| multiset(M); a:mset_of(M) |] ==> natify(M`a) = M`a"; by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff])); -by (rotate_simp_tac "M:?u" 1); qed "natify_elem_is_self"; Addsimps [natify_elem_is_self]; @@ -1024,8 +1006,6 @@ by (case_tac "a ~: mset_of(I)" 1); by (auto_tac (claset(), simpset() addsimps [mcount_def, mset_of_def, multiset_def, multiset_fun_iff])); -by (rotate_simp_tac "I:?u" 1); -by (rotate_simp_tac "J:?u" 1); by (auto_tac (claset() addDs [domain_type], simpset() addsimps [lemma])); qed "mdiff_union_single_conv"; @@ -1141,7 +1121,6 @@ by (asm_full_simp_tac (simpset() addsimps [multirel1_iff, Mult_iff_multiset]) 1); by (Force_tac 1); (*Now we know J' ~= 0*) -by (rotate_simp_tac "multiset(J')" 1); by (dtac sym 1 THEN rotate_tac ~1 1); by (Asm_full_simp_tac 1); by (thin_tac "$# x = msize(J')" 1); @@ -1215,7 +1194,6 @@ by (forw_inst_tac [("B", "mset_of(K)")] part_ord_subset 1); by (ALLGOALS(Asm_full_simp_tac)); by (auto_tac (claset(), simpset() addsimps [multiset_def, mset_of_def])); -by (rotate_simp_tac "K:?u" 1); qed "irrefl_on_multirel"; Goalw [multirel_def, trans_on_def] "trans[Mult(A)](multirel(A, r))"; diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/Integ/Bin.thy --- a/src/ZF/Integ/Bin.thy Mon Sep 30 16:47:03 2002 +0200 +++ b/src/ZF/Integ/Bin.thy Mon Sep 30 16:48:15 2002 +0200 @@ -365,12 +365,9 @@ apply (subgoal_tac "integ_of (w) : int") apply typecheck apply (drule int_cases) -apply (auto elim!: boolE simp add: int_of_add [symmetric]) -apply (simp_all add: zcompare_rls zminus_zadd_distrib [symmetric] +apply (safe elim!: boolE) +apply (simp_all (asm_lr) add: zcompare_rls zminus_zadd_distrib [symmetric] int_of_add [symmetric]) -apply (subgoal_tac "znegative ($- $# succ (n)) <-> znegative ($# succ (n))") - apply (simp (no_asm_use)) -apply simp done lemma iszero_integ_of_0: diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/Integ/Int.thy --- a/src/ZF/Integ/Int.thy Mon Sep 30 16:47:03 2002 +0200 +++ b/src/ZF/Integ/Int.thy Mon Sep 30 16:48:15 2002 +0200 @@ -678,7 +678,6 @@ lemma zless_not_refl [iff]: "~ (z$ (x ~= y) <-> (x $< y | y $< x)" diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/Integ/IntDiv.thy --- a/src/ZF/Integ/IntDiv.thy Mon Sep 30 16:47:03 2002 +0200 +++ b/src/ZF/Integ/IntDiv.thy Mon Sep 30 16:48:15 2002 +0200 @@ -229,7 +229,6 @@ apply (erule natE) apply (simp_all add: zadd_zmult_distrib zadd_zless_mono zle_def) apply (frule nat_0_le) -apply (erule (1) notE impE) apply (subgoal_tac "i $+ (i $+ $# xa $* i) $< j $+ (j $+ $# xa $* j) ") apply (simp (no_asm_use)) apply (rule zadd_zless_mono) @@ -392,7 +391,6 @@ apply (subgoal_tac "q = q'") prefer 2 apply (blast intro: unique_quotient) apply (simp add: quorem_def) -apply auto done diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/Resid/Redex.thy --- a/src/ZF/Resid/Redex.thy Mon Sep 30 16:47:03 2002 +0200 +++ b/src/ZF/Resid/Redex.thy Mon Sep 30 16:48:15 2002 +0200 @@ -178,11 +178,7 @@ lemma union_preserve_regular [rule_format]: "u ~ v ==> regular(u)-->regular(v)-->regular(u un v)" -apply (erule Scomp.induct, auto) -(*select the given assumption for simplification*) -apply (erule_tac P = "regular (Fun (?u) un ?v) " in rev_mp) -apply simp -done + by (erule Scomp.induct, auto) end diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/Resid/Reduction.thy --- a/src/ZF/Resid/Reduction.thy Mon Sep 30 16:47:03 2002 +0200 +++ b/src/ZF/Resid/Reduction.thy Mon Sep 30 16:48:15 2002 +0200 @@ -236,8 +236,6 @@ "u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)" apply (erule Scomp.induct) apply (auto simp add: unmmark_subst_rec) -apply (drule_tac psi = "Fun (?u) =1=> ?w" in asm_rl) -apply auto done lemma completeness: "[|u \ lambda; u~v; regular(v)|] ==> u =1=> unmark(u|>v)" diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/Resid/Residuals.thy --- a/src/ZF/Resid/Residuals.thy Mon Sep 30 16:47:03 2002 +0200 +++ b/src/ZF/Resid/Residuals.thy Mon Sep 30 16:48:15 2002 +0200 @@ -118,10 +118,7 @@ lemma resfunc_type [simp]: "[|s~t; regular(t)|]==> regular(t) --> s |> t \ redexes" -apply (erule Scomp.induct, auto) -apply (drule_tac psi = "Fun (?u) |> ?v \ redexes" in asm_rl) -apply auto -done + by (erule Scomp.induct, auto) (* ------------------------------------------------------------------------- *) (* Commutation theorem *) @@ -138,7 +135,6 @@ lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))" apply (erule Scomp.induct, safe) apply (simp_all add: lift_rec_Var subst_Var lift_subst) -apply (rotate_tac -2, simp) done lemma residuals_subst_rec: @@ -169,7 +165,6 @@ lemma residuals_preserve_reg [rule_format, simp]: "u~v ==> regular(u) --> regular(v) --> regular(u|>v)" apply (erule Scomp.induct, auto) -apply (drule_tac psi = "regular (Fun (?u) |> ?v)" in asm_rl, force)+ done (* ------------------------------------------------------------------------- *) diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/UNITY/UNITY.ML --- a/src/ZF/UNITY/UNITY.ML Mon Sep 30 16:47:03 2002 +0200 +++ b/src/ZF/UNITY/UNITY.ML Mon Sep 30 16:48:15 2002 +0200 @@ -609,7 +609,7 @@ "[| F : stable(C); F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')"; by (cut_inst_tac [("F", "F")] Acts_type 1); by Auto_tac; -by (Force_tac 1); +by (Blast.depth_tac (claset()) 10 1); qed "stable_constrains_Un"; Goalw [stable_def, constrains_def, st_set_def] diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/UNITY/Union.ML --- a/src/ZF/UNITY/Union.ML Mon Sep 30 16:47:03 2002 +0200 +++ b/src/ZF/UNITY/Union.ML Mon Sep 30 16:48:15 2002 +0200 @@ -592,8 +592,7 @@ (*For safety_prop to hold, the property must be satisfiable!*) Goal "safety_prop(A co B) <-> (A <= B & st_set(A))"; by (simp_tac (simpset() addsimps [safety_prop_def, constrains_def, st_set_def]) 1); -by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset())); -by (REPEAT(Blast_tac 1)); +by (Blast_tac 1); qed "safety_prop_constrains"; AddIffs [safety_prop_constrains]; diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/UNITY/WFair.ML --- a/src/ZF/UNITY/WFair.ML Mon Sep 30 16:47:03 2002 +0200 +++ b/src/ZF/UNITY/WFair.ML Mon Sep 30 16:48:15 2002 +0200 @@ -21,8 +21,8 @@ Goalw [stable_def, constrains_def, transient_def] "[| F : stable(A); F : transient(A) |] ==> A = 0"; -by Auto_tac; -by (Blast_tac 1); +by (Asm_full_simp_tac 1); +by (Blast.depth_tac (claset()) 10 1); qed "stable_transient_empty"; Goalw [transient_def, st_set_def] diff -r 2edf034c902a -r 55d32e76ef4e src/ZF/ex/Limit.thy --- a/src/ZF/ex/Limit.thy Mon Sep 30 16:47:03 2002 +0200 +++ b/src/ZF/ex/Limit.thy Mon Sep 30 16:48:15 2002 +0200 @@ -1620,7 +1620,7 @@ m \ nat |]==>R" apply (rule le_exists, assumption) prefer 2 apply (simp add: lt_nat_in_nat) -apply (rule le_trans [THEN le_exists], assumption+, auto) +apply (rule le_trans [THEN le_exists], assumption+, force+) done lemma eps_split_left_le: