--- a/src/HOL/Data_Structures/AVL_Bal_Set.thy Mon May 18 12:59:01 2020 +0200
+++ b/src/HOL/Data_Structures/AVL_Bal_Set.thy Tue May 19 09:33:16 2020 +0200
@@ -86,11 +86,14 @@
LT \<Rightarrow> let l' = delete x l in if decr l l' then balR l' a ba r else Node l' (a,ba) r |
GT \<Rightarrow> let r' = delete x r in if decr r r' then balL l a ba r' else Node l (a,ba) r')"
+
+subsection \<open>Proofs\<close>
+
lemmas split_max_induct = split_max.induct[case_names Node Leaf]
lemmas splits = if_splits tree.splits bal.splits
-subsection \<open>Proofs\<close>
+declare Let_def [simp]
subsubsection "Proofs about insertion"
@@ -112,7 +115,7 @@
theorem inorder_insert:
"\<lbrakk> avl t; sorted(inorder t) \<rbrakk> \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
apply(induction t)
-apply (auto simp: ins_list_simps Let_def split!: splits)
+apply (auto simp: ins_list_simps split!: splits)
done
@@ -143,7 +146,7 @@
avl (delete x t) \<and>
height t = height (delete x t) + (if decr t (delete x t) then 1 else 0)"
apply(induction x t rule: delete.induct)
- apply(auto simp: max_absorb1 max_absorb2 Let_def height_1_iff dest: avl_split_max split!: splits prod.splits)
+ apply(auto simp: max_absorb1 max_absorb2 height_1_iff dest: avl_split_max split!: splits prod.splits)
done
lemma inorder_split_maxD:
@@ -163,7 +166,7 @@
theorem inorder_delete:
"\<lbrakk> avl t; sorted(inorder t) \<rbrakk> \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
apply(induction t rule: tree2_induct)
-apply(auto simp: del_list_simps inorder_balR inorder_balL avl_delete inorder_split_maxD Let_def
+apply(auto simp: del_list_simps inorder_balR inorder_balL avl_delete inorder_split_maxD
split_max_Leaf neq_Leaf_if_height_neq_0
simp del: balL.simps balR.simps split!: splits prod.splits)
done
--- a/src/HOL/Data_Structures/Array_Braun.thy Mon May 18 12:59:01 2020 +0200
+++ b/src/HOL/Data_Structures/Array_Braun.thy Tue May 19 09:33:16 2020 +0200
@@ -279,11 +279,13 @@
"size_fast Leaf = 0" |
"size_fast (Node l x r) = (let n = size_fast r in 1 + 2*n + diff l n)"
+declare Let_def[simp]
+
lemma diff: "braun t \<Longrightarrow> size t : {n, n + 1} \<Longrightarrow> diff t n = size t - n"
by(induction t arbitrary: n) auto
lemma size_fast: "braun t \<Longrightarrow> size_fast t = size t"
-by(induction t) (auto simp add: Let_def diff)
+by(induction t) (auto simp add: diff)
subsubsection \<open>Initialization with 1 element\<close>
@@ -468,7 +470,7 @@
theorem length_brauns:
"length (brauns k xs) = min (length xs) (2 ^ k)"
proof (induct xs arbitrary: k rule: measure_induct_rule[where f=length])
- case (less xs) thus ?case by (simp add: brauns.simps[of k xs] Let_def length_nodes)
+ case (less xs) thus ?case by (simp add: brauns.simps[of k xs] length_nodes)
qed
theorem brauns_correct:
@@ -484,7 +486,7 @@
using \<open>xs \<noteq> []\<close> by (simp add: take_nths_drop)
show ?case
using less.prems
- by (auto simp: brauns.simps[of k xs] Let_def nth_nodes take_nths_take_nths
+ by (auto simp: brauns.simps[of k xs] nth_nodes take_nths_take_nths
IH take_nths_empty hd_take_nths length_brauns)
qed
@@ -503,12 +505,12 @@
show ?case
proof cases
assume "xs = []"
- thus ?thesis by(simp add: Let_def)
+ thus ?thesis by(simp)
next
assume "xs \<noteq> []"
let ?zs = "drop (2^k) xs"
have "t_brauns k xs = t_brauns (k+1) ?zs + 4 * min (2^k) (length xs)"
- using \<open>xs \<noteq> []\<close> by(simp add: Let_def)
+ using \<open>xs \<noteq> []\<close> by(simp)
also have "\<dots> = 4 * length ?zs + 4 * min (2^k) (length xs)"
using less[of ?zs "k+1"] \<open>xs \<noteq> []\<close>
by (simp)
@@ -603,7 +605,7 @@
apply(auto simp: nth_append braun_list_not_Nil take_nths_eq_single braun_list_Nil hd_drop_conv_nth)
done
thus ?thesis
- by (clarsimp simp: list_fast_rec.simps[of ts] o_def list_fast_rec_all_Leaf Let_def)
+ by (clarsimp simp: list_fast_rec.simps[of ts] o_def list_fast_rec_all_Leaf)
next
case False
with less.prems(2) have *:
@@ -621,7 +623,7 @@
by (auto intro!: Nat.diff_less less.hyps[where k= "Suc k"]
simp: nth_append * take_nths_drop algebra_simps)
from less.prems(1) False show ?thesis
- by (auto simp: list_fast_rec.simps[of ts] 1 2 Let_def * all_set_conv_all_nth)
+ by (auto simp: list_fast_rec.simps[of ts] 1 2 * all_set_conv_all_nth)
qed
qed
@@ -644,12 +646,12 @@
proof cases
assume "?us = []"
thus ?thesis using t_list_fast_rec.simps[of ts]
- by(simp add: Let_def sum_list_Suc)
+ by(simp add: sum_list_Suc)
next
assume "?us \<noteq> []"
let ?children = "map left ?us @ map right ?us"
have "t_list_fast_rec ts = t_list_fast_rec ?children + 5 * length ?us + length ts"
- using \<open>?us \<noteq> []\<close> t_list_fast_rec.simps[of ts] by(simp add: Let_def)
+ using \<open>?us \<noteq> []\<close> t_list_fast_rec.simps[of ts] by(simp)
also have "\<dots> \<le> (\<Sum>t\<leftarrow>?children. 7 * size t + 1) + 5 * length ?us + length ts"
using less[of "?children"] list_fast_rec_term[of "?us"] \<open>?us \<noteq> []\<close>
by (simp)
--- a/src/HOL/Data_Structures/Balance.thy Mon May 18 12:59:01 2020 +0200
+++ b/src/HOL/Data_Structures/Balance.thy Tue May 19 09:33:16 2020 +0200
@@ -15,6 +15,7 @@
in (Node l (hd ys) r, zs)))"
declare bal.simps[simp del]
+declare Let_def[simp]
definition bal_list :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a tree" where
"bal_list n xs = fst (bal n xs)"
@@ -52,7 +53,7 @@
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: Let_def bal_simps split: prod.splits)
+ 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
have IH2: "tl ys = inorder r @ zs \<and> size r = ?m'"
@@ -113,7 +114,7 @@
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 Let_def split: prod.splits)
+ 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
@@ -149,7 +150,7 @@
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 Let_def split: prod.splits)
+ 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
@@ -216,7 +217,7 @@
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 Let_def split: prod.splits)
+ 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 "wbalanced r"
using rec1 rec2 bal_length[OF _ rec1] "1.prems"(1) by(intro "1.IH"(2)) auto
--- a/src/HOL/Data_Structures/RBT_Set2.thy Mon May 18 12:59:01 2020 +0200
+++ b/src/HOL/Data_Structures/RBT_Set2.thy Tue May 19 09:33:16 2020 +0200
@@ -35,6 +35,8 @@
subsection "Functional Correctness Proofs"
+declare Let_def[simp]
+
lemma split_minD:
"split_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> x # inorder t' = inorder t"
by(induction t arbitrary: t' rule: split_min.induct)
@@ -43,7 +45,7 @@
lemma inorder_del:
"sorted(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
by(induction x t rule: del.induct)
- (auto simp: del_list_simps inorder_baldL inorder_baldR split_minD Let_def split: prod.splits)
+ (auto simp: del_list_simps inorder_baldL inorder_baldR split_minD split: prod.splits)
lemma inorder_delete:
"sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
@@ -73,7 +75,7 @@
(color t = Red \<longrightarrow> bheight (del x t) = bheight t \<and> invc (del x t)) \<and>
(color t = Black \<longrightarrow> bheight (del x t) = bheight t - 1 \<and> invc2 (del x t))"
apply(induction x t rule: del.induct)
-apply(auto simp: inv_baldR inv_baldL invc2I Let_def dest!: inv_split_min dest: neq_LeafD
+apply(auto simp: inv_baldR inv_baldL invc2I dest!: inv_split_min dest: neq_LeafD
split!: prod.splits if_splits)
done
@@ -106,7 +108,7 @@
proof cases
assume "x > a"
show ?thesis using \<open>a < x\<close> "2.IH"(2) "2.prems" neq_LeafD[of r] inv_baldR[of _ "del x r"]
- by(auto simp: Let_def split: if_split)
+ by(auto split: if_split)
next
assume "\<not> x > a"
--- a/src/HOL/Data_Structures/Set2_Join.thy Mon May 18 12:59:01 2020 +0200
+++ b/src/HOL/Data_Structures/Set2_Join.thy Tue May 19 09:33:16 2020 +0200
@@ -29,7 +29,7 @@
assumes inv_Node: "\<lbrakk> inv (Node l (a,b) r) \<rbrakk> \<Longrightarrow> inv l \<and> inv r"
begin
-declare set_join [simp]
+declare set_join [simp] Let_def[simp]
subsection "\<open>split_min\<close>"
@@ -227,7 +227,7 @@
proof(induction t1 t2 rule: inter.induct)
case (1 t1 t2)
thus ?case
- by(fastforce simp: inter.simps[of t1 t2] set_tree_inter split Let_def
+ by(fastforce simp: inter.simps[of t1 t2] set_tree_inter split
intro!: bst_join bst_join2 split: tree.split prod.split)
qed
@@ -235,7 +235,7 @@
proof(induction t1 t2 rule: inter.induct)
case (1 t1 t2)
thus ?case
- by(auto simp: inter.simps[of t1 t2] inv_join inv_join2 split_inv Let_def
+ by(auto simp: inter.simps[of t1 t2] inv_join inv_join2 split_inv
split!: tree.split prod.split dest: inv_Node)
qed
@@ -291,7 +291,7 @@
proof(induction t1 t2 rule: diff.induct)
case (1 t1 t2)
thus ?case
- by(fastforce simp: diff.simps[of t1 t2] set_tree_diff split Let_def
+ by(fastforce simp: diff.simps[of t1 t2] set_tree_diff split
intro!: bst_join bst_join2 split: tree.split prod.split)
qed
@@ -299,7 +299,7 @@
proof(induction t1 t2 rule: diff.induct)
case (1 t1 t2)
thus ?case
- by(auto simp: diff.simps[of t1 t2] inv_join inv_join2 split_inv Let_def
+ by(auto simp: diff.simps[of t1 t2] inv_join inv_join2 split_inv
split!: tree.split prod.split dest: inv_Node)
qed