removal of image_Collect as a default simprule
authorpaulson
Tue Apr 24 12:19:58 2001 +0200 (2001-04-24)
changeset 112654f2e6c87a57f
parent 11264 a47a9288f3f6
child 11266 70c9ebbffc49
removal of image_Collect as a default simprule
src/HOL/Lattice/Bounds.thy
src/HOL/List.ML
src/HOL/equalities.ML
     1.1 --- a/src/HOL/Lattice/Bounds.thy	Tue Apr 24 12:19:01 2001 +0200
     1.2 +++ b/src/HOL/Lattice/Bounds.thy	Tue Apr 24 12:19:58 2001 +0200
     1.3 @@ -315,7 +315,7 @@
     1.4    hence "is_Inf (dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b}) (dual inf)"
     1.5      by (simp only: dual_Inf dual_leq)
     1.6    also have "dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b} = {b'. \<forall>a' \<in> dual ` A. a' \<sqsubseteq> b'}"
     1.7 -    by (auto iff: dual_ball dual_Collect)  (* FIXME !? *)
     1.8 +    by (auto iff: dual_ball dual_Collect simp add: image_Collect)  (* FIXME !? *)
     1.9    finally have "is_Inf \<dots> (dual inf)" .
    1.10    hence "is_Sup (dual ` A) (dual inf)"
    1.11      by (rule Inf_Sup)
     2.1 --- a/src/HOL/List.ML	Tue Apr 24 12:19:01 2001 +0200
     2.2 +++ b/src/HOL/List.ML	Tue Apr 24 12:19:58 2001 +0200
     2.3 @@ -1374,6 +1374,7 @@
     2.4  qed "wf_lex";
     2.5  AddSIs [wf_lex];
     2.6  
     2.7 +
     2.8  Goal
     2.9   "lexn r n = \
    2.10  \ {(xs,ys). length xs = n & length ys = n & \
    2.11 @@ -1381,15 +1382,14 @@
    2.12  by (induct_tac "n" 1);
    2.13   by (Simp_tac 1);
    2.14   by (Blast_tac 1);
    2.15 -by (asm_full_simp_tac (simpset() 
    2.16 -				addsimps [lex_prod_def]) 1);
    2.17 -by (auto_tac (claset(), simpset()));
    2.18 +by (asm_full_simp_tac (simpset() addsimps [image_Collect, lex_prod_def]) 1);
    2.19 +by Auto_tac;
    2.20    by (Blast_tac 1);
    2.21   by (rename_tac "a xys x xs' y ys'" 1);
    2.22   by (res_inst_tac [("x","a#xys")] exI 1);
    2.23   by (Simp_tac 1);
    2.24  by (case_tac "xys" 1);
    2.25 - by (ALLGOALS (asm_full_simp_tac (simpset())));
    2.26 + by (ALLGOALS Asm_full_simp_tac);
    2.27  by (Blast_tac 1);
    2.28  qed "lexn_conv";
    2.29  
     3.1 --- a/src/HOL/equalities.ML	Tue Apr 24 12:19:01 2001 +0200
     3.2 +++ b/src/HOL/equalities.ML	Tue Apr 24 12:19:58 2001 +0200
     3.3 @@ -142,10 +142,12 @@
     3.4  qed "image_is_empty";
     3.5  AddIffs [image_is_empty];
     3.6  
     3.7 +(*NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
     3.8 +  with its implicit quantifier and conjunction.  Also image enjoys better
     3.9 +  equational properties than does the RHS.*)
    3.10  Goal "f ` {x. P x} = {f x | x. P x}";
    3.11  by (Blast_tac 1);
    3.12  qed "image_Collect";
    3.13 -Addsimps [image_Collect];
    3.14  
    3.15  Goalw [image_def] "(%x. if P x then f x else g x) ` S   \
    3.16  \                = (f ` (S Int {x. P x})) Un (g ` (S Int {x. ~(P x)}))";