author | haftmann |

Sat, 19 Oct 2019 20:41:03 +0200 | |

changeset 71101 | 38298c04c12e |

parent 71100 | 3ed399935d7c |

child 71102 | 8c2bef3df488 |

more lemmas

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

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

--- a/src/HOL/List.thy Sat Oct 19 16:16:24 2019 +0200 +++ b/src/HOL/List.thy Sat Oct 19 20:41:03 2019 +0200 @@ -2698,6 +2698,42 @@ with xs ys show ?thesis .. qed +lemma semilattice_map2: + "semilattice (map2 (\<^bold>*))" if "semilattice (\<^bold>*)" + for f (infixl "\<^bold>*" 70) +proof - + from that interpret semilattice f . + show ?thesis + proof + show "map2 (\<^bold>*) (map2 (\<^bold>*) xs ys) zs = map2 (\<^bold>*) xs (map2 (\<^bold>*) ys zs)" + for xs ys zs :: "'a list" + proof (induction "zip xs (zip ys zs)" arbitrary: xs ys zs) + case Nil + from Nil [symmetric] show ?case + by (auto simp add: zip_eq_Nil_iff) + next + case (Cons xyz xyzs) + from Cons.hyps(2) [symmetric] show ?case + by (rule zip_eq_ConsE) (erule zip_eq_ConsE, + auto intro: Cons.hyps(1) simp add: ac_simps) + qed + show "map2 (\<^bold>*) xs ys = map2 (\<^bold>*) ys xs" + for xs ys :: "'a list" + proof (induction "zip xs ys" arbitrary: xs ys) + case Nil + then show ?case + by (auto simp add: zip_eq_Nil_iff dest: sym) + next + case (Cons xy xys) + from Cons.hyps(2) [symmetric] show ?case + by (rule zip_eq_ConsE) (auto intro: Cons.hyps(1) simp add: ac_simps) + qed + show "map2 (\<^bold>*) xs xs = xs" + for xs :: "'a list" + by (induction xs) simp_all + qed +qed + lemma pair_list_eqI: assumes "map fst xs = map fst ys" and "map snd xs = map snd ys" shows "xs = ys"

--- a/src/HOL/Parity.thy Sat Oct 19 16:16:24 2019 +0200 +++ b/src/HOL/Parity.thy Sat Oct 19 20:41:03 2019 +0200 @@ -448,6 +448,38 @@ finally show ?thesis . qed +lemma numeral_Bit0_div_2: + "numeral (num.Bit0 n) div 2 = numeral n" +proof - + have "numeral (num.Bit0 n) = numeral n + numeral n" + by (simp only: numeral.simps) + also have "\<dots> = numeral n * 2" + by (simp add: mult_2_right) + finally have "numeral (num.Bit0 n) div 2 = numeral n * 2 div 2" + by simp + also have "\<dots> = numeral n" + by (rule nonzero_mult_div_cancel_right) simp + finally show ?thesis . +qed + +lemma numeral_Bit1_div_2: + "numeral (num.Bit1 n) div 2 = numeral n" +proof - + have "numeral (num.Bit1 n) = numeral n + numeral n + 1" + by (simp only: numeral.simps) + also have "\<dots> = numeral n * 2 + 1" + by (simp add: mult_2_right) + finally have "numeral (num.Bit1 n) div 2 = (numeral n * 2 + 1) div 2" + by simp + also have "\<dots> = numeral n * 2 div 2 + 1 div 2" + using dvd_triv_right by (rule div_plus_div_distrib_dvd_left) + also have "\<dots> = numeral n * 2 div 2" + by simp + also have "\<dots> = numeral n" + by (rule nonzero_mult_div_cancel_right) simp + finally show ?thesis . +qed + end class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat @@ -1061,4 +1093,8 @@ "drop_bit n (Suc 0) = of_bool (n = 0)" using drop_bit_of_1 [where ?'a = nat] by simp +lemma push_bit_minus_one: + "push_bit n (- 1 :: int) = - (2 ^ n)" + by (simp add: push_bit_eq_mult) + end