# HG changeset patch
# User haftmann
# Date 1556707242 0
# Node ID accbd801fefa9311e3432127253c093533e7e3f2
# Parent  129757af1096fde913cc64247aa3f9db05302250
more lemmas

diff -r 129757af1096 -r accbd801fefa src/HOL/List.thy
--- a/src/HOL/List.thy	Wed May 01 10:40:40 2019 +0000
+++ b/src/HOL/List.thy	Wed May 01 10:40:42 2019 +0000
@@ -2678,6 +2678,26 @@
   from this that show ?thesis by fastforce
 qed
 
+lemma zip_eq_Nil_iff:
+  "zip xs ys = [] \<longleftrightarrow> xs = [] \<or> ys = []"
+  by (cases xs; cases ys) simp_all
+
+lemma zip_eq_ConsE:
+  assumes "zip xs ys = xy # xys"
+  obtains x xs' y ys' where "xs = x # xs'"
+    and "ys = y # ys'" and "xy = (x, y)"
+    and "xys = zip xs' ys'"
+proof -
+  from assms have "xs \<noteq> []" and "ys \<noteq> []"
+    using zip_eq_Nil_iff [of xs ys] by simp_all
+  then obtain x xs' y ys'  where xs: "xs = x # xs'"
+    and ys: "ys = y # ys'"
+    by (cases xs; cases ys) auto
+  with assms have "xy = (x, y)" and "xys = zip xs' ys'"
+    by simp_all
+  with xs ys show ?thesis ..
+qed
+
 lemma pair_list_eqI:
   assumes "map fst xs = map fst ys" and "map snd xs = map snd ys"
   shows "xs = ys"
diff -r 129757af1096 -r accbd801fefa src/HOL/Num.thy
--- a/src/HOL/Num.thy	Wed May 01 10:40:40 2019 +0000
+++ b/src/HOL/Num.thy	Wed May 01 10:40:42 2019 +0000
@@ -229,6 +229,10 @@
 lemma sqr_conv_mult: "sqr x = x * x"
   by (simp add: num_eq_iff nat_of_num_sqr nat_of_num_mult)
 
+lemma num_double [simp]:
+  "num.Bit0 num.One * n = num.Bit0 n"
+  by (simp add: num_eq_iff nat_of_num_mult)
+
 
 subsection \<open>Binary numerals\<close>
 
diff -r 129757af1096 -r accbd801fefa src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Wed May 01 10:40:40 2019 +0000
+++ b/src/HOL/Parity.thy	Wed May 01 10:40:42 2019 +0000
@@ -519,12 +519,11 @@
     by simp
 qed
 
-lemma parity_induct [case_names zero even odd]:
-  assumes zero: "P 0"
-  assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
-  assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
-  shows "P n"
-proof (induct n rule: less_induct)
+lemma nat_parity_induct [case_names zero even odd]:
+  "P n" if zero: "P 0"
+    and even: "\<And>n. P n \<Longrightarrow> n > 0 \<Longrightarrow> P (2 * n)"
+    and odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
+proof (induction n rule: less_induct)
   case (less n)
   show "P n"
   proof (cases "n = 0")
@@ -535,7 +534,11 @@
     show ?thesis
     proof (cases "even n")
       case True
-      with hyp even [of "n div 2"] show ?thesis
+      then have "n \<noteq> 1"
+        by auto
+      with \<open>n \<noteq> 0\<close> have "n div 2 > 0"
+        by simp
+      with \<open>even n\<close> hyp even [of "n div 2"] show ?thesis
         by simp
     next
       case False
@@ -545,6 +548,63 @@
   qed
 qed
 
+lemma int_parity_induct [case_names zero minus even odd]:
+  "P k" if zero_int: "P 0"
+    and minus_int: "P (- 1)"
+    and even_int: "\<And>k. P k \<Longrightarrow> k \<noteq> 0 \<Longrightarrow> P (k * 2)"
+    and odd_int: "\<And>k. P k \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> P (1 + (k * 2))" for k :: int
+proof (cases "k \<ge> 0")
+  case True
+  define n where "n = nat k"
+  with True have "k = int n"
+    by simp
+  then show "P k"
+  proof (induction n arbitrary: k rule: nat_parity_induct)
+    case zero
+    then show ?case
+      by (simp add: zero_int)
+  next
+    case (even n)
+    have "P (int n * 2)"
+      by (rule even_int) (use even in simp_all)
+    with even show ?case
+      by (simp add: ac_simps)
+  next
+    case (odd n)
+    have "P (1 + (int n * 2))"
+      by (rule odd_int) (use odd in simp_all)
+    with odd show ?case
+      by (simp add: ac_simps)
+  qed
+next
+  case False
+  define n where "n = nat (- k - 1)"
+  with False have "k = - int n - 1"
+    by simp
+  then show "P k"
+  proof (induction n arbitrary: k rule: nat_parity_induct)
+    case zero
+    then show ?case
+      by (simp add: minus_int)
+  next
+    case (even n)
+    have "P (1 + (- int (Suc n) * 2))"
+      by (rule odd_int) (use even in \<open>simp_all add: algebra_simps\<close>)
+    also have "\<dots> = - int (2 * n) - 1"
+      by (simp add: algebra_simps)
+    finally show ?case
+      using even by simp
+  next
+    case (odd n)
+    have "P (- int (Suc n) * 2)"
+      by (rule even_int) (use odd in \<open>simp_all add: algebra_simps\<close>)
+    also have "\<dots> = - int (Suc (2 * n)) - 1"
+      by (simp add: algebra_simps)
+    finally show ?case
+      using odd by simp
+  qed
+qed
+
 lemma not_mod2_eq_Suc_0_eq_0 [simp]:
   "n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0"
   using not_mod_2_eq_1_eq_0 [of n] by simp
@@ -956,4 +1016,14 @@
   "drop_bit n (Suc 0) = of_bool (n = 0)"
   using drop_bit_of_1 [where ?'a = nat] by simp
 
+
+subsection \<open>Legacy\<close>
+
+lemma parity_induct [case_names zero even odd]:
+  assumes zero: "P 0"
+  assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
+  assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
+  shows "P n"
+  using assms by (rule nat_parity_induct)
+
 end