author nipkow Sun, 24 May 2020 08:20:05 +0200 changeset 71858 864fade05842 parent 71856 e9df7895e331 child 71859 059d2cf529d4
simpler inductions
```--- a/src/HOL/Data_Structures/Balance.thy	Fri May 22 19:21:16 2020 +0200
+++ b/src/HOL/Data_Structures/Balance.thy	Sun May 24 08:20:05 2020 +0200
@@ -42,23 +42,23 @@
lemma bal_inorder:
"\<lbrakk> n \<le> length xs; bal n xs = (t,zs) \<rbrakk>
\<Longrightarrow> xs = inorder t @ zs \<and> size t = n"
-proof(induction n xs arbitrary: t zs rule: bal.induct)
-  case (1 n xs) show ?case
+proof(induction n arbitrary: xs t zs rule: less_induct)
+  case (less n) show ?case
proof cases
-    assume "n = 0" thus ?thesis using 1 by (simp add: bal_simps)
+    assume "n = 0" thus ?thesis using less.prems by (simp add: bal_simps)
next
assume [arith]: "n \<noteq> 0"
let ?m = "n div 2" let ?m' = "n - 1 - ?m"
-    from "1.prems"(2) obtain l r ys where
+    from less.prems(2) obtain l r ys where
b1: "bal ?m xs = (l,ys)" and
b2: "bal ?m' (tl ys) = (r,zs)" and
t: "t = \<langle>l, hd ys, r\<rangle>"
by(auto simp: bal_simps split: prod.splits)
have IH1: "xs = inorder l @ ys \<and> size l = ?m"
-      using b1 "1.prems"(1) by(intro "1.IH"(1)) auto
+      using b1 less.prems(1) by(intro less.IH) auto
have IH2: "tl ys = inorder r @ zs \<and> size r = ?m'"
-      using b1 b2 IH1 "1.prems"(1) by(intro "1.IH"(2)) auto
-    show ?thesis using t IH1 IH2  "1.prems"(1) hd_Cons_tl[of ys] by fastforce
+      using  b2 IH1 less.prems(1) by(intro less.IH) auto
+    show ?thesis using t IH1 IH2 less.prems(1) hd_Cons_tl[of ys] by fastforce
qed
qed

@@ -102,24 +102,24 @@

lemma min_height_bal:
"\<lbrakk> n \<le> length xs; bal n xs = (t,zs) \<rbrakk> \<Longrightarrow> min_height t = nat(\<lfloor>log 2 (n + 1)\<rfloor>)"
-proof(induction n xs arbitrary: t zs rule: bal.induct)
-  case (1 n xs)
+proof(induction n arbitrary: xs t zs rule: less_induct)
+  case (less n)
show ?case
proof cases
-    assume "n = 0" thus ?thesis using "1.prems"(2) by (simp add: bal_simps)
+    assume "n = 0" thus ?thesis using less.prems(2) by (simp add: bal_simps)
next
assume [arith]: "n \<noteq> 0"
let ?m = "n div 2" let ?m' = "n - 1 - ?m"
-    from "1.prems" obtain l r ys where
+    from less.prems obtain l r ys where
b1: "bal ?m xs = (l,ys)" and
b2: "bal ?m' (tl ys) = (r,zs)" and
t: "t = \<langle>l, hd ys, r\<rangle>"
by(auto simp: bal_simps split: prod.splits)
let ?hl = "nat (floor(log 2 (?m + 1)))"
let ?hr = "nat (floor(log 2 (?m' + 1)))"
-    have IH1: "min_height l = ?hl" using "1.IH"(1) b1 "1.prems"(1) by simp
+    have IH1: "min_height l = ?hl" using less.IH[OF _ _ b1] less.prems(1) by simp
have IH2: "min_height r = ?hr"
-      using "1.prems"(1) bal_length[OF _ b1] b1 b2 by(intro "1.IH"(2)) auto
+      using less.prems(1) bal_length[OF _ b1] b2 by(intro less.IH) auto
have "(n+1) div 2 \<ge> 1" by arith
hence 0: "log 2 ((n+1) div 2) \<ge> 0" by simp
have "?m' \<le> ?m" by arith
@@ -138,24 +138,24 @@

lemma height_bal:
"\<lbrakk> n \<le> length xs; bal n xs = (t,zs) \<rbrakk> \<Longrightarrow> height t = nat \<lceil>log 2 (n + 1)\<rceil>"
-proof(induction n xs arbitrary: t zs rule: bal.induct)
-  case (1 n xs) show ?case
+proof(induction n arbitrary: xs t zs rule: less_induct)
+  case (less n) show ?case
proof cases
assume "n = 0" thus ?thesis
-      using "1.prems" by (simp add: bal_simps)
+      using less.prems by (simp add: bal_simps)
next
assume [arith]: "n \<noteq> 0"
let ?m = "n div 2" let ?m' = "n - 1 - ?m"
-    from "1.prems" obtain l r ys where
+    from less.prems obtain l r ys where
b1: "bal ?m xs = (l,ys)" and
b2: "bal ?m' (tl ys) = (r,zs)" and
t: "t = \<langle>l, hd ys, r\<rangle>"
by(auto simp: bal_simps split: prod.splits)
let ?hl = "nat \<lceil>log 2 (?m + 1)\<rceil>"
let ?hr = "nat \<lceil>log 2 (?m' + 1)\<rceil>"
-    have IH1: "height l = ?hl" using "1.IH"(1) b1 "1.prems"(1) by simp
+    have IH1: "height l = ?hl" using less.IH[OF _ _ b1] less.prems(1) by simp
have IH2: "height r = ?hr"
-      using b1 b2 bal_length[OF _ b1] "1.prems"(1) by(intro "1.IH"(2)) auto
+      using b2 bal_length[OF _ b1] less.prems(1) by(intro less.IH) auto
have 0: "log 2 (?m + 1) \<ge> 0" by simp
have "?m' \<le> ?m" by arith
hence le: "?hr \<le> ?hl"
@@ -205,23 +205,23 @@
by (simp add: balance_tree_def)

lemma wbalanced_bal: "\<lbrakk> n \<le> length xs; bal n xs = (t,ys) \<rbrakk> \<Longrightarrow> wbalanced t"
-proof(induction n xs arbitrary: t ys rule: bal.induct)
-  case (1 n xs)
+proof(induction n arbitrary: xs t ys rule: less_induct)
+  case (less n)
show ?case
proof cases
assume "n = 0"
-    thus ?thesis using "1.prems"(2) by(simp add: bal_simps)
+    thus ?thesis using less.prems(2) by(simp add: bal_simps)
next
assume [arith]: "n \<noteq> 0"
-    with "1.prems" obtain l ys r zs where
+    with less.prems obtain l ys r zs where
rec1: "bal (n div 2) xs = (l, ys)" and
rec2: "bal (n - 1 - n div 2) (tl ys) = (r, zs)" and
t: "t = \<langle>l, hd ys, r\<rangle>"
by(auto simp add: bal_simps split: prod.splits)
-    have l: "wbalanced l" using "1.IH"(1)[OF \<open>n\<noteq>0\<close> refl _ rec1] "1.prems"(1) by linarith
+    have l: "wbalanced l" using less.IH[OF _ _ rec1] less.prems(1) by linarith
have "wbalanced r"
-      using rec1 rec2 bal_length[OF _ rec1] "1.prems"(1) by(intro "1.IH"(2)) auto
-    with l t bal_length[OF _ rec1] "1.prems"(1) bal_inorder[OF _ rec1] bal_inorder[OF _ rec2]
+      using rec1 rec2 bal_length[OF _ rec1] less.prems(1) by(intro less.IH) auto
+    with l t bal_length[OF _ rec1] less.prems(1) bal_inorder[OF _ rec1] bal_inorder[OF _ rec2]
show ?thesis by auto
qed
qed```