--- a/src/HOL/Data_Structures/AA_Map.thy Thu Nov 09 10:24:00 2017 +0100
+++ b/src/HOL/Data_Structures/AA_Map.thy Fri Nov 10 22:05:30 2017 +0100
@@ -72,64 +72,62 @@
lemma invar_update: "invar t \<Longrightarrow> invar(update a b t)"
proof(induction t)
- case (Node n l xy r)
+ case N: (Node n l xy r)
hence il: "invar l" and ir: "invar r" by auto
+ note iil = N.IH(1)[OF il]
+ note iir = N.IH(2)[OF ir]
obtain x y where [simp]: "xy = (x,y)" by fastforce
- note N = Node
let ?t = "Node n l xy r"
have "a < x \<or> a = x \<or> x < a" by auto
moreover
- { assume "a < x"
- note iil = Node.IH(1)[OF il]
- have ?case
- proof (cases rule: lvl_update[of a b l])
- case (Same) thus ?thesis
- using \<open>a<x\<close> invar_NodeL[OF Node.prems iil Same]
- by (simp add: skew_invar split_invar del: invar.simps)
+ have ?case if "a < x"
+ proof (cases rule: lvl_update[of a b l])
+ case (Same) thus ?thesis
+ using \<open>a<x\<close> invar_NodeL[OF N.prems iil Same]
+ by (simp add: skew_invar split_invar del: invar.simps)
+ next
+ case (Incr)
+ then obtain t1 w t2 where ial[simp]: "update a b l = Node n t1 w t2"
+ using N.prems by (auto simp: lvl_Suc_iff)
+ have l12: "lvl t1 = lvl t2"
+ by (metis Incr(1) ial lvl_update_incr_iff tree.inject)
+ have "update a b ?t = split(skew(Node n (update a b l) xy r))"
+ by(simp add: \<open>a<x\<close>)
+ also have "skew(Node n (update a b l) xy r) = Node n t1 w (Node n t2 xy r)"
+ by(simp)
+ also have "invar(split \<dots>)"
+ proof (cases r)
+ case Leaf
+ hence "l = Leaf" using N.prems by(auto simp: lvl_0_iff)
+ thus ?thesis using Leaf ial by simp
next
- case (Incr)
- then obtain t1 w t2 where ial[simp]: "update a b l = Node n t1 w t2"
- using Node.prems by (auto simp: lvl_Suc_iff)
- have l12: "lvl t1 = lvl t2"
- by (metis Incr(1) ial lvl_update_incr_iff tree.inject)
- have "update a b ?t = split(skew(Node n (update a b l) xy r))"
- by(simp add: \<open>a<x\<close>)
- also have "skew(Node n (update a b l) xy r) = Node n t1 w (Node n t2 xy r)"
- by(simp)
- also have "invar(split \<dots>)"
- proof (cases r)
- case Leaf
- hence "l = Leaf" using Node.prems by(auto simp: lvl_0_iff)
- thus ?thesis using Leaf ial by simp
+ case [simp]: (Node m t3 y t4)
+ show ?thesis (*using N(3) iil l12 by(auto)*)
+ proof cases
+ assume "m = n" thus ?thesis using N(3) iil by(auto)
next
- case [simp]: (Node m t3 y t4)
- show ?thesis (*using N(3) iil l12 by(auto)*)
- proof cases
- assume "m = n" thus ?thesis using N(3) iil by(auto)
- next
- assume "m \<noteq> n" thus ?thesis using N(3) iil l12 by(auto)
- qed
+ assume "m \<noteq> n" thus ?thesis using N(3) iil l12 by(auto)
qed
- finally show ?thesis .
qed
- }
+ finally show ?thesis .
+ qed
moreover
- { assume "x < a"
- note iir = Node.IH(2)[OF ir]
+ have ?case if "x < a"
+ proof -
from \<open>invar ?t\<close> have "n = lvl r \<or> n = lvl r + 1" by auto
- hence ?case
+ thus ?case
proof
assume 0: "n = lvl r"
have "update a b ?t = split(skew(Node n l xy (update a b r)))"
using \<open>a>x\<close> by(auto)
also have "skew(Node n l xy (update a b r)) = Node n l xy (update a b r)"
- using Node.prems by(simp add: skew_case split: tree.split)
+ using N.prems by(simp add: skew_case split: tree.split)
also have "invar(split \<dots>)"
proof -
from lvl_update_sngl[OF ir sngl_if_invar[OF \<open>invar ?t\<close> 0], of a b]
obtain t1 p t2 where iar: "update a b r = Node n t1 p t2"
- using Node.prems 0 by (auto simp: lvl_Suc_iff)
- from Node.prems iar 0 iir
+ using N.prems 0 by (auto simp: lvl_Suc_iff)
+ from N.prems iar 0 iir
show ?thesis by (auto simp: split_case split: tree.splits)
qed
finally show ?thesis .
@@ -139,7 +137,7 @@
show ?thesis
proof (cases rule: lvl_update[of a b r])
case (Same)
- show ?thesis using \<open>x<a\<close> il ir invar_NodeR[OF Node.prems 1 iir Same]
+ show ?thesis using \<open>x<a\<close> il ir invar_NodeR[OF N.prems 1 iir Same]
by (auto simp add: skew_invar split_invar)
next
case (Incr)
@@ -147,8 +145,9 @@
by (auto simp add: skew_invar split_invar split: if_splits)
qed
qed
- }
- moreover { assume "a = x" hence ?case using Node.prems by auto }
+ qed
+ moreover
+ have "a = x \<Longrightarrow> ?case" using N.prems by auto
ultimately show ?case by blast
qed simp
--- a/src/HOL/Data_Structures/AA_Set.thy Thu Nov 09 10:24:00 2017 +0100
+++ b/src/HOL/Data_Structures/AA_Set.thy Fri Nov 10 22:05:30 2017 +0100
@@ -201,63 +201,61 @@
lemma invar_insert: "invar t \<Longrightarrow> invar(insert a t)"
proof(induction t)
- case (Node n l x r)
+ case N: (Node n l x r)
hence il: "invar l" and ir: "invar r" by auto
- note N = Node
+ note iil = N.IH(1)[OF il]
+ note iir = N.IH(2)[OF ir]
let ?t = "Node n l x r"
have "a < x \<or> a = x \<or> x < a" by auto
moreover
- { assume "a < x"
- note iil = Node.IH(1)[OF il]
- have ?case
- proof (cases rule: lvl_insert[of a l])
- case (Same) thus ?thesis
- using \<open>a<x\<close> invar_NodeL[OF Node.prems iil Same]
- by (simp add: skew_invar split_invar del: invar.simps)
+ have ?case if "a < x"
+ proof (cases rule: lvl_insert[of a l])
+ case (Same) thus ?thesis
+ using \<open>a<x\<close> invar_NodeL[OF N.prems iil Same]
+ by (simp add: skew_invar split_invar del: invar.simps)
+ next
+ case (Incr)
+ then obtain t1 w t2 where ial[simp]: "insert a l = Node n t1 w t2"
+ using N.prems by (auto simp: lvl_Suc_iff)
+ have l12: "lvl t1 = lvl t2"
+ by (metis Incr(1) ial lvl_insert_incr_iff tree.inject)
+ have "insert a ?t = split(skew(Node n (insert a l) x r))"
+ by(simp add: \<open>a<x\<close>)
+ also have "skew(Node n (insert a l) x r) = Node n t1 w (Node n t2 x r)"
+ by(simp)
+ also have "invar(split \<dots>)"
+ proof (cases r)
+ case Leaf
+ hence "l = Leaf" using N.prems by(auto simp: lvl_0_iff)
+ thus ?thesis using Leaf ial by simp
next
- case (Incr)
- then obtain t1 w t2 where ial[simp]: "insert a l = Node n t1 w t2"
- using Node.prems by (auto simp: lvl_Suc_iff)
- have l12: "lvl t1 = lvl t2"
- by (metis Incr(1) ial lvl_insert_incr_iff tree.inject)
- have "insert a ?t = split(skew(Node n (insert a l) x r))"
- by(simp add: \<open>a<x\<close>)
- also have "skew(Node n (insert a l) x r) = Node n t1 w (Node n t2 x r)"
- by(simp)
- also have "invar(split \<dots>)"
- proof (cases r)
- case Leaf
- hence "l = Leaf" using Node.prems by(auto simp: lvl_0_iff)
- thus ?thesis using Leaf ial by simp
+ case [simp]: (Node m t3 y t4)
+ show ?thesis (*using N(3) iil l12 by(auto)*)
+ proof cases
+ assume "m = n" thus ?thesis using N(3) iil by(auto)
next
- case [simp]: (Node m t3 y t4)
- show ?thesis (*using N(3) iil l12 by(auto)*)
- proof cases
- assume "m = n" thus ?thesis using N(3) iil by(auto)
- next
- assume "m \<noteq> n" thus ?thesis using N(3) iil l12 by(auto)
- qed
+ assume "m \<noteq> n" thus ?thesis using N(3) iil l12 by(auto)
qed
- finally show ?thesis .
qed
- }
+ finally show ?thesis .
+ qed
moreover
- { assume "x < a"
- note iir = Node.IH(2)[OF ir]
+ have ?case if "x < a"
+ proof -
from \<open>invar ?t\<close> have "n = lvl r \<or> n = lvl r + 1" by auto
- hence ?case
+ thus ?case
proof
assume 0: "n = lvl r"
have "insert a ?t = split(skew(Node n l x (insert a r)))"
using \<open>a>x\<close> by(auto)
also have "skew(Node n l x (insert a r)) = Node n l x (insert a r)"
- using Node.prems by(simp add: skew_case split: tree.split)
+ using N.prems by(simp add: skew_case split: tree.split)
also have "invar(split \<dots>)"
proof -
from lvl_insert_sngl[OF ir sngl_if_invar[OF \<open>invar ?t\<close> 0], of a]
obtain t1 y t2 where iar: "insert a r = Node n t1 y t2"
- using Node.prems 0 by (auto simp: lvl_Suc_iff)
- from Node.prems iar 0 iir
+ using N.prems 0 by (auto simp: lvl_Suc_iff)
+ from N.prems iar 0 iir
show ?thesis by (auto simp: split_case split: tree.splits)
qed
finally show ?thesis .
@@ -267,7 +265,7 @@
show ?thesis
proof (cases rule: lvl_insert[of a r])
case (Same)
- show ?thesis using \<open>x<a\<close> il ir invar_NodeR[OF Node.prems 1 iir Same]
+ show ?thesis using \<open>x<a\<close> il ir invar_NodeR[OF N.prems 1 iir Same]
by (auto simp add: skew_invar split_invar)
next
case (Incr)
@@ -275,8 +273,9 @@
by (auto simp add: skew_invar split_invar split: if_splits)
qed
qed
- }
- moreover { assume "a = x" hence ?case using Node.prems by auto }
+ qed
+ moreover
+ have "a = x \<Longrightarrow> ?case" using N.prems by auto
ultimately show ?case by blast
qed simp
--- a/src/HOL/Data_Structures/Brother12_Map.thy Thu Nov 09 10:24:00 2017 +0100
+++ b/src/HOL/Data_Structures/Brother12_Map.thy Fri Nov 10 22:05:30 2017 +0100
@@ -126,61 +126,58 @@
{ case 1
then obtain l a b r where [simp]: "t = N2 l (a,b) r" and
lr: "l \<in> T h" "r \<in> T h" "l \<in> B h \<or> r \<in> B h" by auto
- { assume "x < a"
- have ?case
- proof cases
- assume "l \<in> B h"
- from n2_type3[OF Suc.IH(1)[OF this] lr(2)]
- show ?thesis using `x<a` by(simp)
- next
- assume "l \<notin> B h"
- hence "l \<in> U h" "r \<in> B h" using lr by auto
- from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)]
- show ?thesis using `x<a` by(simp)
- qed
- } moreover
- { assume "x > a"
- have ?case
+ have ?case if "x < a"
+ proof cases
+ assume "l \<in> B h"
+ from n2_type3[OF Suc.IH(1)[OF this] lr(2)]
+ show ?thesis using `x<a` by(simp)
+ next
+ assume "l \<notin> B h"
+ hence "l \<in> U h" "r \<in> B h" using lr by auto
+ from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)]
+ show ?thesis using `x<a` by(simp)
+ qed
+ moreover
+ have ?case if "x > a"
+ proof cases
+ assume "r \<in> B h"
+ from n2_type3[OF lr(1) Suc.IH(1)[OF this]]
+ show ?thesis using `x>a` by(simp)
+ next
+ assume "r \<notin> B h"
+ hence "l \<in> B h" "r \<in> U h" using lr by auto
+ from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]]
+ show ?thesis using `x>a` by(simp)
+ qed
+ moreover
+ have ?case if [simp]: "x=a"
+ proof (cases "del_min r")
+ case None
+ show ?thesis
proof cases
assume "r \<in> B h"
- from n2_type3[OF lr(1) Suc.IH(1)[OF this]]
- show ?thesis using `x>a` by(simp)
+ with del_minNoneN0[OF this None] lr show ?thesis by(simp)
next
assume "r \<notin> B h"
- hence "l \<in> B h" "r \<in> U h" using lr by auto
- from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]]
- show ?thesis using `x>a` by(simp)
+ hence "r \<in> U h" using lr by auto
+ with del_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
qed
- } moreover
- { assume [simp]: "x=a"
- have ?case
- proof (cases "del_min r")
- case None
- show ?thesis
- proof cases
- assume "r \<in> B h"
- with del_minNoneN0[OF this None] lr show ?thesis by(simp)
- next
- assume "r \<notin> B h"
- hence "r \<in> U h" using lr by auto
- with del_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
- qed
+ next
+ case [simp]: (Some br')
+ obtain b r' where [simp]: "br' = (b,r')" by fastforce
+ show ?thesis
+ proof cases
+ assume "r \<in> B h"
+ from del_min_type(1)[OF this] n2_type3[OF lr(1)]
+ show ?thesis by simp
next
- case [simp]: (Some br')
- obtain b r' where [simp]: "br' = (b,r')" by fastforce
- show ?thesis
- proof cases
- assume "r \<in> B h"
- from del_min_type(1)[OF this] n2_type3[OF lr(1)]
- show ?thesis by simp
- next
- assume "r \<notin> B h"
- hence "l \<in> B h" and "r \<in> U h" using lr by auto
- from del_min_type(2)[OF this(2)] n2_type2[OF this(1)]
- show ?thesis by simp
- qed
+ assume "r \<notin> B h"
+ hence "l \<in> B h" and "r \<in> U h" using lr by auto
+ from del_min_type(2)[OF this(2)] n2_type2[OF this(1)]
+ show ?thesis by simp
qed
- } ultimately show ?case by auto
+ qed
+ ultimately show ?case by auto
}
{ case 2 with Suc.IH(1) show ?case by auto }
qed auto
--- a/src/HOL/Data_Structures/Brother12_Set.thy Thu Nov 09 10:24:00 2017 +0100
+++ b/src/HOL/Data_Structures/Brother12_Set.thy Fri Nov 10 22:05:30 2017 +0100
@@ -258,9 +258,9 @@
then obtain t1 a t2 where [simp]: "t = N2 t1 a t2" and
t1: "t1 \<in> T h" and t2: "t2 \<in> T h" and t12: "t1 \<in> B h \<or> t2 \<in> B h"
by auto
- { assume "x < a"
- hence "?case \<longleftrightarrow> n2 (ins x t1) a t2 \<in> Bp (Suc h)" by simp
- also have "\<dots>"
+ have ?case if "x < a"
+ proof -
+ have "n2 (ins x t1) a t2 \<in> Bp (Suc h)"
proof cases
assume "t1 \<in> B h"
with t2 show ?thesis by (simp add: Suc.IH(1) n2_type)
@@ -269,12 +269,12 @@
hence 1: "t1 \<in> U h" and 2: "t2 \<in> B h" using t1 t12 by auto
show ?thesis by (metis Suc.IH(2)[OF 1] Bp_if_B[OF 2] n2_type)
qed
- finally have ?case .
- }
+ with `x < a` show ?case by simp
+ qed
moreover
- { assume "a < x"
- hence "?case \<longleftrightarrow> n2 t1 a (ins x t2) \<in> Bp (Suc h)" by simp
- also have "\<dots>"
+ have ?case if "a < x"
+ proof -
+ have "n2 t1 a (ins x t2) \<in> Bp (Suc h)"
proof cases
assume "t2 \<in> B h"
with t1 show ?thesis by (simp add: Suc.IH(1) n2_type)
@@ -283,12 +283,14 @@
hence 1: "t1 \<in> B h" and 2: "t2 \<in> U h" using t2 t12 by auto
show ?thesis by (metis Bp_if_B[OF 1] Suc.IH(2)[OF 2] n2_type)
qed
- }
- moreover
- { assume "x = a"
+ with `a < x` show ?case by simp
+ qed
+ moreover
+ have ?case if "x = a"
+ proof -
from 1 have "t \<in> Bp (Suc h)" by(rule Bp_if_B)
- hence "?case" using `x = a` by simp
- }
+ thus "?case" using `x = a` by simp
+ qed
ultimately show ?case by auto
next
case 2 thus ?case using Suc(1) n1_type by fastforce }
@@ -398,61 +400,58 @@
{ case 1
then obtain l a r where [simp]: "t = N2 l a r" and
lr: "l \<in> T h" "r \<in> T h" "l \<in> B h \<or> r \<in> B h" by auto
- { assume "x < a"
- have ?case
- proof cases
- assume "l \<in> B h"
- from n2_type3[OF Suc.IH(1)[OF this] lr(2)]
- show ?thesis using `x<a` by(simp)
- next
- assume "l \<notin> B h"
- hence "l \<in> U h" "r \<in> B h" using lr by auto
- from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)]
- show ?thesis using `x<a` by(simp)
- qed
- } moreover
- { assume "x > a"
- have ?case
+ have ?case if "x < a"
+ proof cases
+ assume "l \<in> B h"
+ from n2_type3[OF Suc.IH(1)[OF this] lr(2)]
+ show ?thesis using `x<a` by(simp)
+ next
+ assume "l \<notin> B h"
+ hence "l \<in> U h" "r \<in> B h" using lr by auto
+ from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)]
+ show ?thesis using `x<a` by(simp)
+ qed
+ moreover
+ have ?case if "x > a"
+ proof cases
+ assume "r \<in> B h"
+ from n2_type3[OF lr(1) Suc.IH(1)[OF this]]
+ show ?thesis using `x>a` by(simp)
+ next
+ assume "r \<notin> B h"
+ hence "l \<in> B h" "r \<in> U h" using lr by auto
+ from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]]
+ show ?thesis using `x>a` by(simp)
+ qed
+ moreover
+ have ?case if [simp]: "x=a"
+ proof (cases "del_min r")
+ case None
+ show ?thesis
proof cases
assume "r \<in> B h"
- from n2_type3[OF lr(1) Suc.IH(1)[OF this]]
- show ?thesis using `x>a` by(simp)
+ with del_minNoneN0[OF this None] lr show ?thesis by(simp)
next
assume "r \<notin> B h"
- hence "l \<in> B h" "r \<in> U h" using lr by auto
- from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]]
- show ?thesis using `x>a` by(simp)
+ hence "r \<in> U h" using lr by auto
+ with del_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
qed
- } moreover
- { assume [simp]: "x=a"
- have ?case
- proof (cases "del_min r")
- case None
- show ?thesis
- proof cases
- assume "r \<in> B h"
- with del_minNoneN0[OF this None] lr show ?thesis by(simp)
- next
- assume "r \<notin> B h"
- hence "r \<in> U h" using lr by auto
- with del_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
- qed
+ next
+ case [simp]: (Some br')
+ obtain b r' where [simp]: "br' = (b,r')" by fastforce
+ show ?thesis
+ proof cases
+ assume "r \<in> B h"
+ from del_min_type(1)[OF this] n2_type3[OF lr(1)]
+ show ?thesis by simp
next
- case [simp]: (Some br')
- obtain b r' where [simp]: "br' = (b,r')" by fastforce
- show ?thesis
- proof cases
- assume "r \<in> B h"
- from del_min_type(1)[OF this] n2_type3[OF lr(1)]
- show ?thesis by simp
- next
- assume "r \<notin> B h"
- hence "l \<in> B h" and "r \<in> U h" using lr by auto
- from del_min_type(2)[OF this(2)] n2_type2[OF this(1)]
- show ?thesis by simp
- qed
+ assume "r \<notin> B h"
+ hence "l \<in> B h" and "r \<in> U h" using lr by auto
+ from del_min_type(2)[OF this(2)] n2_type2[OF this(1)]
+ show ?thesis by simp
qed
- } ultimately show ?case by auto
+ qed
+ ultimately show ?case by auto
}
{ case 2 with Suc.IH(1) show ?case by auto }
qed auto