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

author | nipkow |

Sun, 17 Jun 2018 20:31:51 +0200 | |

changeset 68460 | b047339bd11c |

parent 68457 | 517aa9076fc9 |

child 68461 | 8dea233d4bae |

added simp rules

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

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

--- a/src/HOL/Map.thy Sun Jun 17 13:10:14 2018 +0200 +++ b/src/HOL/Map.thy Sun Jun 17 20:31:51 2018 +0200 @@ -133,6 +133,10 @@ by (induction xys) simp_all qed simp +lemma empty_eq_map_of_iff [simp]: + "empty = map_of xys \<longleftrightarrow> xys = []" +by(subst eq_commute) simp + lemma map_of_eq_None_iff: "(map_of xys x = None) = (x \<notin> fst ` (set xys))" by (induct xys) simp_all

--- a/src/HOL/Option.thy Sun Jun 17 13:10:14 2018 +0200 +++ b/src/HOL/Option.thy Sun Jun 17 20:31:51 2018 +0200 @@ -36,6 +36,9 @@ lemma not_Some_eq [iff]: "(\<forall>y. x \<noteq> Some y) \<longleftrightarrow> x = None" by (induct x) auto +lemma comp_the_Some[simp]: "the o Some = id" +by auto + text \<open>Although it may appear that both of these equalities are helpful only when applied to assumptions, in practice it seems better to give them the uniform iff attribute.\<close>