--- a/src/HOL/Data_Structures/Tries_Binary.thy Thu Mar 30 16:10:50 2023 +0200
+++ b/src/HOL/Data_Structures/Tries_Binary.thy Sat Apr 01 15:52:40 2023 +0200
@@ -138,12 +138,12 @@
"insertP ks LfP = NdP ks True (LfP,LfP)" |
"insertP ks (NdP ps b lr) =
(case split ks ps of
- (qs,k#ks',p#ps') \<Rightarrow>
+ (qs, k#ks', p#ps') \<Rightarrow>
let tp = NdP ps' b lr; tk = NdP ks' True (LfP,LfP) in
NdP qs False (if k then (tp,tk) else (tk,tp)) |
- (qs,k#ks',[]) \<Rightarrow>
+ (qs, k#ks', []) \<Rightarrow>
NdP ps b (mod2 (insertP ks') k lr) |
- (qs,[],p#ps') \<Rightarrow>
+ (qs, [], p#ps') \<Rightarrow>
let t = NdP ps' b lr in
NdP qs True (if p then (LfP,t) else (t,LfP)) |
(qs,[],[]) \<Rightarrow> NdP ps True lr)"
@@ -156,9 +156,9 @@
"deleteP ks LfP = LfP" |
"deleteP ks (NdP ps b lr) =
(case split ks ps of
- (qs,ks',p#ps') \<Rightarrow> NdP ps b lr |
- (qs,k#ks',[]) \<Rightarrow> nodeP ps b (mod2 (deleteP ks') k lr) |
- (qs,[],[]) \<Rightarrow> nodeP ps False lr)"
+ (_, _, _#_) \<Rightarrow> NdP ps b lr |
+ (_, k#ks', []) \<Rightarrow> nodeP ps b (mod2 (deleteP ks') k lr) |
+ (_, [], []) \<Rightarrow> nodeP ps False lr)"
subsubsection \<open>Functional Correctness\<close>