equal
deleted
inserted
replaced
1414 moreover from True kvs'[symmetric] refl refl n2' |
1414 moreover from True kvs'[symmetric] refl refl n2' |
1415 have "Q (n div 2) kvs'" by(rule IH) |
1415 have "Q (n div 2) kvs'" by(rule IH) |
1416 moreover note feven[unfolded feven_def] |
1416 moreover note feven[unfolded feven_def] |
1417 (* FIXME: why does by(rule feven[unfolded feven_def]) not work? *) |
1417 (* FIXME: why does by(rule feven[unfolded feven_def]) not work? *) |
1418 ultimately have "P (2 * (n div 2)) kvs" by - |
1418 ultimately have "P (2 * (n div 2)) kvs" by - |
1419 thus ?thesis using True by (metis div_mod_equality' minus_nat.diff_0 mult.commute) |
1419 thus ?thesis using True by (metis minus_mod_eq_div_mult [symmetric] minus_nat.diff_0 mult.commute) |
1420 next |
1420 next |
1421 case False note ge0 |
1421 case False note ge0 |
1422 moreover from "1.prems" have n2: "n div 2 \<le> length kvs" by simp |
1422 moreover from "1.prems" have n2: "n div 2 \<le> length kvs" by simp |
1423 moreover from False n2 have "P (n div 2) kvs" by(rule IH) |
1423 moreover from False n2 have "P (n div 2) kvs" by(rule IH) |
1424 moreover from length_rbtreeify_f[OF n2] ge0 "1.prems" obtain t k v kvs' |
1424 moreover from length_rbtreeify_f[OF n2] ge0 "1.prems" obtain t k v kvs' |
1460 moreover from True kvs'[symmetric] refl refl n2' |
1460 moreover from True kvs'[symmetric] refl refl n2' |
1461 have "Q (n div 2) kvs'" by(rule IH) |
1461 have "Q (n div 2) kvs'" by(rule IH) |
1462 moreover note geven[unfolded geven_def] |
1462 moreover note geven[unfolded geven_def] |
1463 ultimately have "Q (2 * (n div 2)) kvs" by - |
1463 ultimately have "Q (2 * (n div 2)) kvs" by - |
1464 thus ?thesis using True |
1464 thus ?thesis using True |
1465 by(metis div_mod_equality' minus_nat.diff_0 mult.commute) |
1465 by(metis minus_mod_eq_div_mult [symmetric] minus_nat.diff_0 mult.commute) |
1466 next |
1466 next |
1467 case False note ge0 |
1467 case False note ge0 |
1468 moreover from "2.prems" have n2: "n div 2 \<le> length kvs" by simp |
1468 moreover from "2.prems" have n2: "n div 2 \<le> length kvs" by simp |
1469 moreover from False n2 have "P (n div 2) kvs" by(rule IH) |
1469 moreover from False n2 have "P (n div 2) kvs" by(rule IH) |
1470 moreover from length_rbtreeify_f[OF n2] ge0 "2.prems" False obtain t k v kvs' |
1470 moreover from length_rbtreeify_f[OF n2] ge0 "2.prems" False obtain t k v kvs' |