author | paulson |

Tue Apr 24 12:19:58 2001 +0200 (2001-04-24) | |

changeset 11265 | 4f2e6c87a57f |

parent 11264 | a47a9288f3f6 |

child 11266 | 70c9ebbffc49 |

removal of image_Collect as a default simprule

src/HOL/Lattice/Bounds.thy | file | annotate | diff | revisions | |

src/HOL/List.ML | file | annotate | diff | revisions | |

src/HOL/equalities.ML | file | annotate | diff | revisions |

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)}))";