--- a/src/HOL/Data_Structures/AVL_Bal2_Set.thy Tue Mar 18 21:39:42 2025 +0000
+++ b/src/HOL/Data_Structures/AVL_Bal2_Set.thy Wed Mar 19 22:18:52 2025 +0000
@@ -123,9 +123,7 @@
Same t' \<Rightarrow> avl t' \<and> height t' = height t |
Diff t' \<Rightarrow> avl t' \<and> height t' = height t + 1 \<and>
(\<forall>l a r. t' = Node l (a,Bal) r \<longrightarrow> a = x \<and> l = Leaf \<and> r = Leaf)"
-apply(induction x t rule: ins.induct)
-apply(auto simp: max_absorb1 split!: splits)
-done
+ by (induction x t rule: ins.induct) (auto simp: max_absorb1 split!: splits)
corollary avl_insert: "avl t \<Longrightarrow> avl(insert x t)"
using avl_ins_case[of t x] by (simp add: insert_def split: splits)
@@ -141,9 +139,7 @@
theorem inorder_ins:
"\<lbrakk> avl t; sorted(inorder t) \<rbrakk> \<Longrightarrow> inorder(tree(ins x t)) = ins_list x (inorder t)"
-apply(induction t)
-apply (auto simp: ins_list_simps split!: splits)
-done
+ by (induction t) (auto simp: ins_list_simps split!: splits)
subsubsection "Proofs about deletion"
@@ -162,17 +158,14 @@
"\<lbrakk> split_max t = (t',a); avl t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow> case t' of
Same t' \<Rightarrow> avl t' \<and> height t = height t' |
Diff t' \<Rightarrow> avl t' \<and> height t = height t' + 1"
-apply(induction t arbitrary: t' a rule: split_max_induct)
- apply(fastforce simp: max_absorb1 max_absorb2 split!: splits prod.splits)
-apply simp
-done
+proof (induction t arbitrary: t' a rule: split_max_induct)
+qed (auto simp: max_def split!: splits prod.splits)
lemma avl_del_case: "avl t \<Longrightarrow> case del x t of
Same t' \<Rightarrow> avl t' \<and> height t = height t' |
Diff t' \<Rightarrow> avl t' \<and> height t = height t' + 1"
-apply(induction x t rule: del.induct)
- apply(auto simp: max_absorb1 max_absorb2 dest: avl_split_max split!: splits prod.splits)
-done
+proof (induction x t rule: del.induct)
+qed (auto simp: max_absorb1 max_absorb2 dest: avl_split_max split!: splits prod.splits)
corollary avl_delete: "avl t \<Longrightarrow> avl(delete x t)"
using avl_del_case[of t x] by(simp add: delete_def split: splits)
@@ -180,20 +173,23 @@
lemma inorder_split_maxD:
"\<lbrakk> split_max t = (t',a); t \<noteq> Leaf; avl t \<rbrakk> \<Longrightarrow>
inorder (tree t') @ [a] = inorder t"
-apply(induction t arbitrary: t' rule: split_max.induct)
- apply(fastforce split!: splits prod.splits)
-apply simp
-done
+proof (induction t arbitrary: t' rule: split_max.induct)
+qed (auto split!: splits prod.splits)
lemma neq_Leaf_if_height_neq_0[simp]: "height t \<noteq> 0 \<Longrightarrow> t \<noteq> Leaf"
by auto
theorem inorder_del:
"\<lbrakk> avl t; sorted(inorder t) \<rbrakk> \<Longrightarrow> inorder (tree(del x t)) = del_list x (inorder t)"
-apply(induction t rule: tree2_induct)
-apply(auto simp: del_list_simps inorder_baldL inorder_baldR avl_delete inorder_split_maxD
- simp del: baldR.simps baldL.simps split!: splits prod.splits)
-done
+proof (induction t rule: tree2_induct)
+ case Leaf
+ then show ?case by simp
+next
+ case (Node x1 a b x3)
+ then show ?case
+ by (auto simp: del_list_simps inorder_baldL inorder_baldR avl_delete inorder_split_maxD
+ simp del: baldL.simps split!: splits prod.splits)
+qed
subsubsection \<open>Set Implementation\<close>
--- a/src/HOL/Data_Structures/AVL_Bal_Set.thy Tue Mar 18 21:39:42 2025 +0000
+++ b/src/HOL/Data_Structures/AVL_Bal_Set.thy Wed Mar 19 22:18:52 2025 +0000
@@ -100,9 +100,7 @@
lemma avl_insert: "avl t \<Longrightarrow>
avl(insert x t) \<and>
height(insert x t) = height t + (if incr t (insert x t) then 1 else 0)"
-apply(induction x t rule: insert.induct)
-apply(auto split!: splits)
-done
+ by (induction x t rule: insert.induct)(auto split!: splits)
text \<open>The following two auxiliary lemma merely simplify the proof of \<open>inorder_insert\<close>.\<close>
@@ -114,9 +112,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 split!: splits)
-done
+ by (induction t) (auto simp: ins_list_simps split!: splits)
subsubsection "Proofs about deletion"
@@ -137,24 +133,20 @@
lemma avl_split_max:
"\<lbrakk> split_max t = (t',a); avl t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
avl t' \<and> height t = height t' + (if incr t' t then 1 else 0)"
-apply(induction t arbitrary: t' a rule: split_max_induct)
- apply(auto simp: max_absorb1 max_absorb2 height_1_iff split!: splits prod.splits)
-done
+proof (induction t arbitrary: t' a rule: split_max_induct)
+qed (auto simp: max_absorb1 max_absorb2 height_1_iff split!: splits prod.splits)
lemma avl_delete: "avl t \<Longrightarrow>
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 height_1_iff dest: avl_split_max split!: splits prod.splits)
-done
+proof (induction x t rule: delete.induct)
+qed (auto simp: max_absorb1 max_absorb2 height_1_iff dest: avl_split_max split!: splits prod.splits)
lemma inorder_split_maxD:
"\<lbrakk> split_max t = (t',a); t \<noteq> Leaf; avl t \<rbrakk> \<Longrightarrow>
inorder t' @ [a] = inorder t"
-apply(induction t arbitrary: t' rule: split_max.induct)
- apply(fastforce split!: splits prod.splits)
-apply simp
-done
+proof (induction t arbitrary: t' rule: split_max.induct)
+qed (auto split!: splits prod.splits)
lemma neq_Leaf_if_height_neq_0: "height t \<noteq> 0 \<Longrightarrow> t \<noteq> Leaf"
by auto
@@ -164,12 +156,16 @@
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
- split_max_Leaf neq_Leaf_if_height_neq_0
- simp del: balL.simps balR.simps split!: splits prod.splits)
-done
-
+proof (induction t rule: tree2_induct)
+ case Leaf
+ then show ?case by auto
+next
+ case (Node x1 a b x3)
+ then show ?case
+ by (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)
+qed
subsubsection \<open>Set Implementation\<close>
--- a/src/HOL/Data_Structures/Braun_Tree.thy Tue Mar 18 21:39:42 2025 +0000
+++ b/src/HOL/Data_Structures/Braun_Tree.thy Wed Mar 19 22:18:52 2025 +0000
@@ -3,19 +3,19 @@
section \<open>Braun Trees\<close>
theory Braun_Tree
-imports "HOL-Library.Tree_Real"
+ imports "HOL-Library.Tree_Real"
begin
text \<open>Braun Trees were studied by Braun and Rem~\<^cite>\<open>"BraunRem"\<close>
and later Hoogerwoord~\<^cite>\<open>"Hoogerwoord"\<close>.\<close>
fun braun :: "'a tree \<Rightarrow> bool" where
-"braun Leaf = True" |
-"braun (Node l x r) = ((size l = size r \<or> size l = size r + 1) \<and> braun l \<and> braun r)"
+ "braun Leaf = True" |
+ "braun (Node l x r) = ((size l = size r \<or> size l = size r + 1) \<and> braun l \<and> braun r)"
lemma braun_Node':
"braun (Node l x r) = (size r \<le> size l \<and> size l \<le> size r + 1 \<and> braun l \<and> braun r)"
-by auto
+ by auto
text \<open>The shape of a Braun-tree is uniquely determined by its size:\<close>
@@ -45,14 +45,14 @@
numbering (\<open>braun_indices\<close>) of nodes yields an interval of numbers.\<close>
fun braun_indices :: "'a tree \<Rightarrow> nat set" where
-"braun_indices Leaf = {}" |
-"braun_indices (Node l _ r) = {1} \<union> (*) 2 ` braun_indices l \<union> Suc ` (*) 2 ` braun_indices r"
+ "braun_indices Leaf = {}" |
+ "braun_indices (Node l _ r) = {1} \<union> (*) 2 ` braun_indices l \<union> Suc ` (*) 2 ` braun_indices r"
lemma braun_indices1: "0 \<notin> braun_indices t"
-by (induction t) auto
+ by (induction t) auto
lemma finite_braun_indices: "finite(braun_indices t)"
-by (induction t) auto
+ by (induction t) auto
text "One direction:"
@@ -87,7 +87,7 @@
text "The other direction is more complicated. The following proof is due to Thomas Sewell."
lemma disj_evens_odds: "(*) 2 ` A \<inter> Suc ` (*) 2 ` B = {}"
-using double_not_eq_Suc_double by auto
+ using double_not_eq_Suc_double by auto
lemma card_braun_indices: "card (braun_indices t) = size t"
proof (induction t)
@@ -96,7 +96,7 @@
case Node
thus ?case
by(auto simp: UNION_singleton_eq_range finite_braun_indices card_Un_disjoint
- card_insert_if disj_evens_odds card_image inj_on_def braun_indices1)
+ card_insert_if disj_evens_odds card_image inj_on_def braun_indices1)
qed
lemma braun_indices_intvl_base_1:
@@ -120,19 +120,20 @@
fixes S :: "nat set"
assumes "S = {m..n} \<inter> {i. even i}"
shows "\<exists>m' n'. S = (\<lambda>i. i * 2) ` {m'..n'}"
- apply (rule exI[where x="Suc m div 2"], rule exI[where x="n div 2"])
- apply (fastforce simp add: assms mult.commute)
- done
+proof -
+ have "S = (\<lambda>i. i * 2) ` {Suc m div 2..n div 2}"
+ by (fastforce simp add: assms mult.commute)
+ then show ?thesis
+ by blast
+qed
lemma odd_of_intvl_intvl:
fixes S :: "nat set"
assumes "S = {m..n} \<inter> {i. odd i}"
shows "\<exists>m' n'. S = Suc ` (\<lambda>i. i * 2) ` {m'..n'}"
proof -
- have step1: "\<exists>m'. S = Suc ` ({m'..n - 1} \<inter> {i. even i})"
- apply (rule_tac x="if n = 0 then 1 else m - 1" in exI)
- apply (auto simp: assms image_def elim!: oddE)
- done
+ have "S = Suc ` ({if n = 0 then 1 else m - 1..n - 1} \<inter> Collect even)"
+ by (auto simp: assms image_def elim!: oddE)
thus ?thesis
by (metis even_of_intvl_intvl)
qed
@@ -148,186 +149,35 @@
lemma braun_if_braun_indices: "braun_indices t = {1..size t} \<Longrightarrow> braun t"
proof(induction t)
-case Leaf
+ case Leaf
then show ?case by simp
next
case (Node l x r)
obtain t where t: "t = Node l x r" by simp
- from Node.prems have eq: "{2 .. size t} = (\<lambda>i. i * 2) ` braun_indices l \<union> Suc ` (\<lambda>i. i * 2) ` braun_indices r"
+ then have "insert (Suc 0) ((*) 2 ` braun_indices l \<union> Suc ` (*) 2 ` braun_indices r) \<inter> {2..}
+ = {Suc 0..Suc (size l + size r)} \<inter> {2..}"
+ by (metis Node.prems One_nat_def Suc_eq_plus1 Un_insert_left braun_indices.simps(2)
+ sup_bot_left tree.size(4))
+ then have eq: "{2 .. size t} = (\<lambda>i. i * 2) ` braun_indices l \<union> Suc ` (\<lambda>i. i * 2) ` braun_indices r"
(is "?R = ?S \<union> ?T")
- apply clarsimp
- apply (drule_tac f="\<lambda>S. S \<inter> {2..}" in arg_cong)
- apply (simp add: t mult.commute Int_Un_distrib2 image_int_eq_image braun_indices1_le)
- done
+ by (simp add: t mult.commute Int_Un_distrib2 image_int_eq_image braun_indices1_le)
then have ST: "?S = ?R \<inter> {i. even i}" "?T = ?R \<inter> {i. odd i}"
by (simp_all add: Int_Un_distrib2 image_int_eq_image)
from ST have l: "braun_indices l = {1 .. size l}"
by (fastforce dest: braun_indices_intvl_base_1 dest!: even_of_intvl_intvl
- simp: mult.commute inj_image_eq_iff[OF inj_onI])
+ simp: mult.commute inj_image_eq_iff[OF inj_onI])
from ST have r: "braun_indices r = {1 .. size r}"
by (fastforce dest: braun_indices_intvl_base_1 dest!: odd_of_intvl_intvl
- simp: mult.commute inj_image_eq_iff[OF inj_onI])
+ simp: mult.commute inj_image_eq_iff[OF inj_onI])
note STa = ST[THEN eqset_imp_iff, THEN iffD2]
note STb = STa[of "size t"] STa[of "size t - 1"]
- then have sizes: "size l = size r \<or> size l = size r + 1"
- apply (clarsimp simp: t l r inj_image_mem_iff[OF inj_onI])
- apply (cases "even (size l)"; cases "even (size r)"; clarsimp elim!: oddE; fastforce)
- done
- from l r sizes show ?case
+ then have "size l = size r \<or> size l = size r + 1"
+ using t l r by atomize auto
+ with l r show ?case
by (clarsimp simp: Node.IH)
qed
lemma braun_iff_braun_indices: "braun t \<longleftrightarrow> braun_indices t = {1..size t}"
-using braun_if_braun_indices braun_indices_if_braun by blast
-
-(* An older less appealing proof:
-lemma Suc0_notin_double: "Suc 0 \<notin> ( * ) 2 ` A"
-by(auto)
-
-lemma zero_in_double_iff: "(0::nat) \<in> ( * ) 2 ` A \<longleftrightarrow> 0 \<in> A"
-by(auto)
-
-lemma Suc_in_Suc_image_iff: "Suc n \<in> Suc ` A \<longleftrightarrow> n \<in> A"
-by(auto)
-
-lemmas nat_in_image = Suc0_notin_double zero_in_double_iff Suc_in_Suc_image_iff
-
-lemma disj_union_eq_iff:
- "\<lbrakk> L1 \<inter> R2 = {}; L2 \<inter> R1 = {} \<rbrakk> \<Longrightarrow> L1 \<union> R1 = L2 \<union> R2 \<longleftrightarrow> L1 = L2 \<and> R1 = R2"
-by blast
-
-lemma inj_braun_indices: "braun_indices t1 = braun_indices t2 \<Longrightarrow> t1 = (t2::unit tree)"
-proof(induction t1 arbitrary: t2)
- case Leaf thus ?case using braun_indices.elims by blast
-next
- case (Node l1 x1 r1)
- have "t2 \<noteq> Leaf"
- proof
- assume "t2 = Leaf"
- with Node.prems show False by simp
- qed
- thus ?case using Node
- by (auto simp: neq_Leaf_iff insert_ident nat_in_image braun_indices1
- disj_union_eq_iff disj_evens_odds inj_image_eq_iff inj_def)
-qed
-
-text \<open>How many even/odd natural numbers are there between m and n?\<close>
-
-lemma card_Icc_even_nat:
- "card {i \<in> {m..n::nat}. even i} = (n+1-m + (m+1) mod 2) div 2" (is "?l m n = ?r m n")
-proof(induction "n+1 - m" arbitrary: n m)
- case 0 thus ?case by simp
-next
- case Suc
- have "m \<le> n" using Suc(2) by arith
- hence "{m..n} = insert m {m+1..n}" by auto
- hence "?l m n = card {i \<in> insert m {m+1..n}. even i}" by simp
- also have "\<dots> = ?r m n" (is "?l = ?r")
- proof (cases)
- assume "even m"
- hence "{i \<in> insert m {m+1..n}. even i} = insert m {i \<in> {m+1..n}. even i}" by auto
- hence "?l = card {i \<in> {m+1..n}. even i} + 1" by simp
- also have "\<dots> = (n-m + (m+2) mod 2) div 2 + 1" using Suc(1)[of n "m+1"] Suc(2) by simp
- also have "\<dots> = ?r" using \<open>even m\<close> \<open>m \<le> n\<close> by auto
- finally show ?thesis .
- next
- assume "odd m"
- hence "{i \<in> insert m {m+1..n}. even i} = {i \<in> {m+1..n}. even i}" by auto
- hence "?l = card ..." by simp
- also have "\<dots> = (n-m + (m+2) mod 2) div 2" using Suc(1)[of n "m+1"] Suc(2) by simp
- also have "\<dots> = ?r" using \<open>odd m\<close> \<open>m \<le> n\<close> even_iff_mod_2_eq_zero[of m] by simp
- finally show ?thesis .
- qed
- finally show ?case .
-qed
-
-lemma card_Icc_odd_nat: "card {i \<in> {m..n::nat}. odd i} = (n+1-m + m mod 2) div 2"
-proof -
- let ?A = "{i \<in> {m..n}. odd i}"
- let ?B = "{i \<in> {m+1..n+1}. even i}"
- have "card ?A = card (Suc ` ?A)" by (simp add: card_image)
- also have "Suc ` ?A = ?B" using Suc_le_D by(force simp: image_iff)
- also have "card ?B = (n+1-m + (m) mod 2) div 2"
- using card_Icc_even_nat[of "m+1" "n+1"] by simp
- finally show ?thesis .
-qed
-
-lemma compact_Icc_even: assumes "A = {i \<in> {m..n}. even i}"
-shows "A = (\<lambda>j. 2*(j-1) + m + m mod 2) ` {1..card A}" (is "_ = ?A")
-proof
- let ?a = "(n+1-m + (m+1) mod 2) div 2"
- have "\<exists>j \<in> {1..?a}. i = 2*(j-1) + m + m mod 2" if *: "i \<in> {m..n}" "even i" for i
- proof -
- let ?j = "(i - (m + m mod 2)) div 2 + 1"
- have "?j \<in> {1..?a} \<and> i = 2*(?j-1) + m + m mod 2" using * by(auto simp: mod2_eq_if) presburger+
- thus ?thesis by blast
- qed
- thus "A \<subseteq> ?A" using assms
- by(auto simp: image_iff card_Icc_even_nat simp del: atLeastAtMost_iff)
-next
- let ?a = "(n+1-m + (m+1) mod 2) div 2"
- have 1: "2 * (j - 1) + m + m mod 2 \<in> {m..n}" if *: "j \<in> {1..?a}" for j
- using * by(auto simp: mod2_eq_if)
- have 2: "even (2 * (j - 1) + m + m mod 2)" for j by presburger
- show "?A \<subseteq> A"
- apply(simp add: assms card_Icc_even_nat del: atLeastAtMost_iff One_nat_def)
- using 1 2 by blast
-qed
-
-lemma compact_Icc_odd:
- assumes "B = {i \<in> {m..n}. odd i}" shows "B = (\<lambda>i. 2*(i-1) + m + (m+1) mod 2) ` {1..card B}"
-proof -
- define A :: " nat set" where "A = Suc ` B"
- have "A = {i \<in> {m+1..n+1}. even i}"
- using Suc_le_D by(force simp add: A_def assms image_iff)
- from compact_Icc_even[OF this]
- have "A = Suc ` (\<lambda>i. 2 * (i - 1) + m + (m + 1) mod 2) ` {1..card A}"
- by (simp add: image_comp o_def)
- hence B: "B = (\<lambda>i. 2 * (i - 1) + m + (m + 1) mod 2) ` {1..card A}"
- using A_def by (simp add: inj_image_eq_iff)
- have "card A = card B" by (metis A_def bij_betw_Suc bij_betw_same_card)
- with B show ?thesis by simp
-qed
-
-lemma even_odd_decomp: assumes "\<forall>x \<in> A. even x" "\<forall>x \<in> B. odd x" "A \<union> B = {m..n}"
-shows "(let a = card A; b = card B in
- a + b = n+1-m \<and>
- A = (\<lambda>i. 2*(i-1) + m + m mod 2) ` {1..a} \<and>
- B = (\<lambda>i. 2*(i-1) + m + (m+1) mod 2) ` {1..b} \<and>
- (a = b \<or> a = b+1 \<and> even m \<or> a+1 = b \<and> odd m))"
-proof -
- let ?a = "card A" let ?b = "card B"
- have "finite A \<and> finite B"
- by (metis \<open>A \<union> B = {m..n}\<close> finite_Un finite_atLeastAtMost)
- hence ab: "?a + ?b = Suc n - m"
- by (metis Int_emptyI assms card_Un_disjoint card_atLeastAtMost)
- have A: "A = {i \<in> {m..n}. even i}" using assms by auto
- hence A': "A = (\<lambda>i. 2*(i-1) + m + m mod 2) ` {1..?a}" by(rule compact_Icc_even)
- have B: "B = {i \<in> {m..n}. odd i}" using assms by auto
- hence B': "B = (\<lambda>i. 2*(i-1) + m + (m+1) mod 2) ` {1..?b}" by(rule compact_Icc_odd)
- have "?a = ?b \<or> ?a = ?b+1 \<and> even m \<or> ?a+1 = ?b \<and> odd m"
- apply(simp add: Let_def mod2_eq_if
- card_Icc_even_nat[of m n, simplified A[symmetric]]
- card_Icc_odd_nat[of m n, simplified B[symmetric]] split!: if_splits)
- by linarith
- with ab A' B' show ?thesis by simp
-qed
-
-lemma braun_if_braun_indices: "braun_indices t = {1..size t} \<Longrightarrow> braun t"
-proof(induction t)
-case Leaf
- then show ?case by simp
-next
- case (Node t1 x2 t2)
- have 1: "i > 0 \<Longrightarrow> Suc(Suc(2 * (i - Suc 0))) = 2*i" for i::nat by(simp add: algebra_simps)
- have 2: "i > 0 \<Longrightarrow> 2 * (i - Suc 0) + 3 = 2*i + 1" for i::nat by(simp add: algebra_simps)
- have 3: "( * ) 2 ` braun_indices t1 \<union> Suc ` ( * ) 2 ` braun_indices t2 =
- {2..size t1 + size t2 + 1}" using Node.prems
- by (simp add: insert_ident Icc_eq_insert_lb_nat nat_in_image braun_indices1)
- thus ?case using Node.IH even_odd_decomp[OF _ _ 3]
- by(simp add: card_image inj_on_def card_braun_indices Let_def 1 2 inj_image_eq_iff image_comp
- cong: image_cong_simp)
-qed
-*)
+ using braun_if_braun_indices braun_indices_if_braun by blast
end
\ No newline at end of file
--- a/src/HOL/Data_Structures/Trie_Ternary.thy Tue Mar 18 21:39:42 2025 +0000
+++ b/src/HOL/Data_Structures/Trie_Ternary.thy Wed Mar 19 22:18:52 2025 +0000
@@ -39,9 +39,7 @@
lemma lookup_size[termination_simp]:
fixes t :: "('a::linorder * 'a trie3) tree"
shows "lookup t a = Some b \<Longrightarrow> size b < Suc (size_tree (\<lambda>ab. Suc (size (snd( ab)))) t)"
-apply(induction t a rule: lookup.induct)
-apply(auto split: if_splits)
-done
+ by (induction t a rule: lookup.induct)(auto split: if_splits)
definition empty3 :: "'a trie3" where
@@ -69,35 +67,27 @@
text \<open>Proof by stepwise refinement. First abs3tract to type @{typ "'a trie"}.\<close>
fun abs3 :: "'a::linorder trie3 \<Rightarrow> 'a trie" where
-"abs3 (Nd3 b t) = Nd b (\<lambda>a. map_option abs3 (lookup t a))"
+ "abs3 (Nd3 b t) = Nd b (\<lambda>a. map_option abs3 (lookup t a))"
fun invar3 :: "('a::linorder)trie3 \<Rightarrow> bool" where
-"invar3 (Nd3 b m) = (M.invar m \<and> (\<forall>a t. lookup m a = Some t \<longrightarrow> invar3 t))"
+ "invar3 (Nd3 b m) = (M.invar m \<and> (\<forall>a t. lookup m a = Some t \<longrightarrow> invar3 t))"
lemma isin_abs3: "isin3 t xs = isin (abs3 t) xs"
-apply(induction t xs rule: isin3.induct)
-apply(auto split: option.split)
-done
+ by (induction t xs rule: isin3.induct)(auto split: option.split)
lemma abs3_insert3: "invar3 t \<Longrightarrow> abs3(insert3 xs t) = insert xs (abs3 t)"
-apply(induction xs t rule: insert3.induct)
-apply(auto simp: M.map_specs Tree_Set.empty_def[symmetric] split: option.split)
-done
+proof (induction xs t rule: insert3.induct)
+qed (auto simp: M.map_specs Tree_Set.empty_def[symmetric] split: option.split)
lemma abs3_delete3: "invar3 t \<Longrightarrow> abs3(delete3 xs t) = delete xs (abs3 t)"
-apply(induction xs t rule: delete3.induct)
-apply(auto simp: M.map_specs split: option.split)
-done
+ by (induction xs t rule: delete3.induct)(auto simp: M.map_specs split: option.split)
lemma invar3_insert3: "invar3 t \<Longrightarrow> invar3 (insert3 xs t)"
-apply(induction xs t rule: insert3.induct)
-apply(auto simp: M.map_specs Tree_Set.empty_def[symmetric] split: option.split)
-done
+proof (induction xs t rule: insert3.induct)
+qed (auto simp: M.map_specs simp flip: Tree_Set.empty_def split: option.split)
lemma invar3_delete3: "invar3 t \<Longrightarrow> invar3 (delete3 xs t)"
-apply(induction xs t rule: delete3.induct)
-apply(auto simp: M.map_specs split: option.split)
-done
+ by (induction xs t rule: delete3.induct)(auto simp: M.map_specs split: option.split)
text \<open>Overall correctness w.r.t. the \<open>Set\<close> ADT:\<close>