summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Tue, 24 Apr 2001 12:19:58 +0200 | |

changeset 11265 | 4f2e6c87a57f |

parent 11264 | a47a9288f3f6 |

child 11266 | 70c9ebbffc49 |

removal of image_Collect as a default simprule

--- a/src/HOL/Lattice/Bounds.thy Tue Apr 24 12:19:01 2001 +0200 +++ b/src/HOL/Lattice/Bounds.thy Tue Apr 24 12:19:58 2001 +0200 @@ -315,7 +315,7 @@ hence "is_Inf (dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b}) (dual inf)" by (simp only: dual_Inf dual_leq) also have "dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b} = {b'. \<forall>a' \<in> dual ` A. a' \<sqsubseteq> b'}" - by (auto iff: dual_ball dual_Collect) (* FIXME !? *) + by (auto iff: dual_ball dual_Collect simp add: image_Collect) (* FIXME !? *) finally have "is_Inf \<dots> (dual inf)" . hence "is_Sup (dual ` A) (dual inf)" by (rule Inf_Sup)

--- a/src/HOL/List.ML Tue Apr 24 12:19:01 2001 +0200 +++ b/src/HOL/List.ML Tue Apr 24 12:19:58 2001 +0200 @@ -1374,6 +1374,7 @@ qed "wf_lex"; AddSIs [wf_lex]; + Goal "lexn r n = \ \ {(xs,ys). length xs = n & length ys = n & \ @@ -1381,15 +1382,14 @@ by (induct_tac "n" 1); by (Simp_tac 1); by (Blast_tac 1); -by (asm_full_simp_tac (simpset() - addsimps [lex_prod_def]) 1); -by (auto_tac (claset(), simpset())); +by (asm_full_simp_tac (simpset() addsimps [image_Collect, lex_prod_def]) 1); +by Auto_tac; by (Blast_tac 1); by (rename_tac "a xys x xs' y ys'" 1); by (res_inst_tac [("x","a#xys")] exI 1); by (Simp_tac 1); by (case_tac "xys" 1); - by (ALLGOALS (asm_full_simp_tac (simpset()))); + by (ALLGOALS Asm_full_simp_tac); by (Blast_tac 1); qed "lexn_conv";

--- a/src/HOL/equalities.ML Tue Apr 24 12:19:01 2001 +0200 +++ b/src/HOL/equalities.ML Tue Apr 24 12:19:58 2001 +0200 @@ -142,10 +142,12 @@ qed "image_is_empty"; AddIffs [image_is_empty]; +(*NOT suitable as a default simprule: the RHS isn't simpler than the LHS, + with its implicit quantifier and conjunction. Also image enjoys better + equational properties than does the RHS.*) Goal "f ` {x. P x} = {f x | x. P x}"; by (Blast_tac 1); qed "image_Collect"; -Addsimps [image_Collect]; Goalw [image_def] "(%x. if P x then f x else g x) ` S \ \ = (f ` (S Int {x. P x})) Un (g ` (S Int {x. ~(P x)}))";