author | haftmann |

Wed May 01 10:40:42 2019 +0000 (6 months ago) | |

changeset 70226 | accbd801fefa |

parent 70225 | 129757af1096 |

child 70227 | ce9134bdc1d4 |

more lemmas

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

src/HOL/Num.thy | file | annotate | diff | revisions | |

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

1.1 --- a/src/HOL/List.thy Wed May 01 10:40:40 2019 +0000 1.2 +++ b/src/HOL/List.thy Wed May 01 10:40:42 2019 +0000 1.3 @@ -2678,6 +2678,26 @@ 1.4 from this that show ?thesis by fastforce 1.5 qed 1.6 1.7 +lemma zip_eq_Nil_iff: 1.8 + "zip xs ys = [] \<longleftrightarrow> xs = [] \<or> ys = []" 1.9 + by (cases xs; cases ys) simp_all 1.10 + 1.11 +lemma zip_eq_ConsE: 1.12 + assumes "zip xs ys = xy # xys" 1.13 + obtains x xs' y ys' where "xs = x # xs'" 1.14 + and "ys = y # ys'" and "xy = (x, y)" 1.15 + and "xys = zip xs' ys'" 1.16 +proof - 1.17 + from assms have "xs \<noteq> []" and "ys \<noteq> []" 1.18 + using zip_eq_Nil_iff [of xs ys] by simp_all 1.19 + then obtain x xs' y ys' where xs: "xs = x # xs'" 1.20 + and ys: "ys = y # ys'" 1.21 + by (cases xs; cases ys) auto 1.22 + with assms have "xy = (x, y)" and "xys = zip xs' ys'" 1.23 + by simp_all 1.24 + with xs ys show ?thesis .. 1.25 +qed 1.26 + 1.27 lemma pair_list_eqI: 1.28 assumes "map fst xs = map fst ys" and "map snd xs = map snd ys" 1.29 shows "xs = ys"

2.1 --- a/src/HOL/Num.thy Wed May 01 10:40:40 2019 +0000 2.2 +++ b/src/HOL/Num.thy Wed May 01 10:40:42 2019 +0000 2.3 @@ -229,6 +229,10 @@ 2.4 lemma sqr_conv_mult: "sqr x = x * x" 2.5 by (simp add: num_eq_iff nat_of_num_sqr nat_of_num_mult) 2.6 2.7 +lemma num_double [simp]: 2.8 + "num.Bit0 num.One * n = num.Bit0 n" 2.9 + by (simp add: num_eq_iff nat_of_num_mult) 2.10 + 2.11 2.12 subsection \<open>Binary numerals\<close> 2.13

3.1 --- a/src/HOL/Parity.thy Wed May 01 10:40:40 2019 +0000 3.2 +++ b/src/HOL/Parity.thy Wed May 01 10:40:42 2019 +0000 3.3 @@ -519,12 +519,11 @@ 3.4 by simp 3.5 qed 3.6 3.7 -lemma parity_induct [case_names zero even odd]: 3.8 - assumes zero: "P 0" 3.9 - assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)" 3.10 - assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))" 3.11 - shows "P n" 3.12 -proof (induct n rule: less_induct) 3.13 +lemma nat_parity_induct [case_names zero even odd]: 3.14 + "P n" if zero: "P 0" 3.15 + and even: "\<And>n. P n \<Longrightarrow> n > 0 \<Longrightarrow> P (2 * n)" 3.16 + and odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))" 3.17 +proof (induction n rule: less_induct) 3.18 case (less n) 3.19 show "P n" 3.20 proof (cases "n = 0") 3.21 @@ -535,7 +534,11 @@ 3.22 show ?thesis 3.23 proof (cases "even n") 3.24 case True 3.25 - with hyp even [of "n div 2"] show ?thesis 3.26 + then have "n \<noteq> 1" 3.27 + by auto 3.28 + with \<open>n \<noteq> 0\<close> have "n div 2 > 0" 3.29 + by simp 3.30 + with \<open>even n\<close> hyp even [of "n div 2"] show ?thesis 3.31 by simp 3.32 next 3.33 case False 3.34 @@ -545,6 +548,63 @@ 3.35 qed 3.36 qed 3.37 3.38 +lemma int_parity_induct [case_names zero minus even odd]: 3.39 + "P k" if zero_int: "P 0" 3.40 + and minus_int: "P (- 1)" 3.41 + and even_int: "\<And>k. P k \<Longrightarrow> k \<noteq> 0 \<Longrightarrow> P (k * 2)" 3.42 + and odd_int: "\<And>k. P k \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> P (1 + (k * 2))" for k :: int 3.43 +proof (cases "k \<ge> 0") 3.44 + case True 3.45 + define n where "n = nat k" 3.46 + with True have "k = int n" 3.47 + by simp 3.48 + then show "P k" 3.49 + proof (induction n arbitrary: k rule: nat_parity_induct) 3.50 + case zero 3.51 + then show ?case 3.52 + by (simp add: zero_int) 3.53 + next 3.54 + case (even n) 3.55 + have "P (int n * 2)" 3.56 + by (rule even_int) (use even in simp_all) 3.57 + with even show ?case 3.58 + by (simp add: ac_simps) 3.59 + next 3.60 + case (odd n) 3.61 + have "P (1 + (int n * 2))" 3.62 + by (rule odd_int) (use odd in simp_all) 3.63 + with odd show ?case 3.64 + by (simp add: ac_simps) 3.65 + qed 3.66 +next 3.67 + case False 3.68 + define n where "n = nat (- k - 1)" 3.69 + with False have "k = - int n - 1" 3.70 + by simp 3.71 + then show "P k" 3.72 + proof (induction n arbitrary: k rule: nat_parity_induct) 3.73 + case zero 3.74 + then show ?case 3.75 + by (simp add: minus_int) 3.76 + next 3.77 + case (even n) 3.78 + have "P (1 + (- int (Suc n) * 2))" 3.79 + by (rule odd_int) (use even in \<open>simp_all add: algebra_simps\<close>) 3.80 + also have "\<dots> = - int (2 * n) - 1" 3.81 + by (simp add: algebra_simps) 3.82 + finally show ?case 3.83 + using even by simp 3.84 + next 3.85 + case (odd n) 3.86 + have "P (- int (Suc n) * 2)" 3.87 + by (rule even_int) (use odd in \<open>simp_all add: algebra_simps\<close>) 3.88 + also have "\<dots> = - int (Suc (2 * n)) - 1" 3.89 + by (simp add: algebra_simps) 3.90 + finally show ?case 3.91 + using odd by simp 3.92 + qed 3.93 +qed 3.94 + 3.95 lemma not_mod2_eq_Suc_0_eq_0 [simp]: 3.96 "n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0" 3.97 using not_mod_2_eq_1_eq_0 [of n] by simp 3.98 @@ -956,4 +1016,14 @@ 3.99 "drop_bit n (Suc 0) = of_bool (n = 0)" 3.100 using drop_bit_of_1 [where ?'a = nat] by simp 3.101 3.102 + 3.103 +subsection \<open>Legacy\<close> 3.104 + 3.105 +lemma parity_induct [case_names zero even odd]: 3.106 + assumes zero: "P 0" 3.107 + assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)" 3.108 + assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))" 3.109 + shows "P n" 3.110 + using assms by (rule nat_parity_induct) 3.111 + 3.112 end