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

author | berghofe |

Sun, 10 Jan 2010 18:09:11 +0100 | |

changeset 34910 | b23bd3ee4813 |

parent 34909 | a799687944af |

child 34911 | 771830d3bd5e |

same_append_eq / append_same_eq are now used for simplifying induction rules.

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/List.thy Sun Jan 10 18:06:30 2010 +0100 +++ b/src/HOL/List.thy Sun Jan 10 18:09:11 2010 +0100 @@ -578,13 +578,13 @@ apply fastsimp done -lemma same_append_eq [iff]: "(xs @ ys = xs @ zs) = (ys = zs)" +lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)" by simp lemma append1_eq_conv [iff]: "(xs @ [x] = ys @ [y]) = (xs = ys \<and> x = y)" by simp -lemma append_same_eq [iff]: "(ys @ xs = zs @ xs) = (ys = zs)" +lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)" by simp lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])"