summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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