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

author | haftmann |

Sun, 09 Feb 2020 10:21:01 +0000 | |

changeset 71423 | 7ae4dcf332ae |

parent 71422 | 5d5be87330b5 |

child 71424 | e83fe2c31088 |

more lemmas

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

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

src/HOL/ex/Bit_Lists.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/List.thy Sat Feb 08 15:18:58 2020 +0100 +++ b/src/HOL/List.thy Sun Feb 09 10:21:01 2020 +0000 @@ -2791,6 +2791,15 @@ by (induct xs ys rule: list_induct2) (simp_all add: prod_eqI) qed +lemma hd_zip: + \<open>hd (zip xs ys) = (hd xs, hd ys)\<close> if \<open>xs \<noteq> []\<close> and \<open>ys \<noteq> []\<close> + using that by (cases xs; cases ys) simp_all + +lemma last_zip: + \<open>last (zip xs ys) = (last xs, last ys)\<close> if \<open>xs \<noteq> []\<close> and \<open>ys \<noteq> []\<close> + and \<open>length xs = length ys\<close> + using that by (cases xs rule: rev_cases; cases ys rule: rev_cases) simp_all + subsubsection \<open>\<^const>\<open>list_all2\<close>\<close>

--- a/src/HOL/Parity.thy Sat Feb 08 15:18:58 2020 +0100 +++ b/src/HOL/Parity.thy Sun Feb 09 10:21:01 2020 +0000 @@ -1106,6 +1106,10 @@ \<open>even (drop_bit n a) \<longleftrightarrow> \<not> bit a n\<close> by (simp add: bit_iff_odd_drop_bit) +lemma div_push_bit_of_1_eq_drop_bit: + \<open>a div push_bit n 1 = drop_bit n a\<close> + by (simp add: push_bit_eq_mult drop_bit_eq_div) + lemma bits_ident: "push_bit n (drop_bit n a) + take_bit n a = a" using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div)

--- a/src/HOL/ex/Bit_Lists.thy Sat Feb 08 15:18:58 2020 +0100 +++ b/src/HOL/ex/Bit_Lists.thy Sun Feb 09 10:21:01 2020 +0000 @@ -8,16 +8,6 @@ Word "HOL-Library.More_List" begin -lemma hd_zip: - \<open>hd (zip xs ys) = (hd xs, hd ys)\<close> if \<open>xs \<noteq> []\<close> and \<open>ys \<noteq> []\<close> - using that by (cases xs; cases ys) simp_all - -lemma last_zip: - \<open>last (zip xs ys) = (last xs, last ys)\<close> if \<open>xs \<noteq> []\<close> and \<open>ys \<noteq> []\<close> - and \<open>length xs = length ys\<close> - using that by (cases xs rule: rev_cases; cases ys rule: rev_cases) simp_all - - subsection \<open>Fragments of algebraic bit representations\<close> context comm_semiring_1