more lemmas
authorhaftmann
Wed May 01 10:40:42 2019 +0000 (6 months ago)
changeset 70226accbd801fefa
parent 70225 129757af1096
child 70227 ce9134bdc1d4
more lemmas
src/HOL/List.thy
src/HOL/Num.thy
src/HOL/Parity.thy
     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