equal
deleted
inserted
replaced
257 primrec swap where |
257 primrec swap where |
258 "swap (Leaf c) a b = |
258 "swap (Leaf c) a b = |
259 (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" | |
259 (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" | |
260 "swap (Branch t u) a b = Branch (swap t a b) (swap u a b)" |
260 "swap (Branch t u) a b = Branch (swap t a b) (swap u a b)" |
261 |
261 |
262 lemma "\<lbrakk>a \<in> labels t; b \<in> labels t; a \<noteq> b\<rbrakk> \<Longrightarrow> labels (swap t a b) = labels t" |
262 lemma "{a, b} \<subseteq> labels t \<Longrightarrow> labels (swap t a b) = labels t" |
263 nitpick |
263 nitpick |
264 proof (induct t) |
264 proof (induct t) |
265 case Leaf thus ?case by simp |
265 case Leaf thus ?case by simp |
266 next |
266 next |
267 case (Branch t u) thus ?case |
267 case (Branch t u) thus ?case |