[STATEMENT]
lemma optimum_splitLeaf:
assumes "consistent t" "optimum t" "a \<in> alphabet t" "b \<notin> alphabet t"
        "freq t a = w\<^sub>a + w\<^sub>b" "\<forall>c \<in> alphabet t. freq t c \<ge> w\<^sub>a \<and> freq t c \<ge> w\<^sub>b"
shows "optimum (splitLeaf t w\<^sub>a a w\<^sub>b b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. optimum (splitLeaf t w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
proof (unfold optimum_def, clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. \<lbrakk>consistent u; alphabet (splitLeaf t w\<^sub>a a w\<^sub>b b) = alphabet u; freq (splitLeaf t w\<^sub>a a w\<^sub>b b) = freq u\<rbrakk> \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. \<lbrakk>consistent u; alphabet (splitLeaf t w\<^sub>a a w\<^sub>b b) = alphabet u; freq (splitLeaf t w\<^sub>a a w\<^sub>b b) = freq u\<rbrakk> \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
let ?t' = "splitLeaf t w\<^sub>a a w\<^sub>b b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. \<lbrakk>consistent u; alphabet (splitLeaf t w\<^sub>a a w\<^sub>b b) = alphabet u; freq (splitLeaf t w\<^sub>a a w\<^sub>b b) = freq u\<rbrakk> \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
assume c\<^sub>u: "consistent u" and a\<^sub>u: "alphabet ?t' = alphabet u" and
    f\<^sub>u: "freq ?t' = freq u"
[PROOF STATE]
proof (state)
this:
consistent u
alphabet (splitLeaf t w\<^sub>a a w\<^sub>b b) = alphabet u
freq (splitLeaf t w\<^sub>a a w\<^sub>b b) = freq u

goal (1 subgoal):
 1. \<And>u. \<lbrakk>consistent u; alphabet (splitLeaf t w\<^sub>a a w\<^sub>b b) = alphabet u; freq (splitLeaf t w\<^sub>a a w\<^sub>b b) = freq u\<rbrakk> \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
show "cost ?t' \<le> cost u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
proof (cases "height ?t' = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) = 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
 2. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
height (splitLeaf t w\<^sub>a a w\<^sub>b b) = 0

goal (2 subgoals):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) = 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
 2. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
height (splitLeaf t w\<^sub>a a w\<^sub>b b) = 0

goal (1 subgoal):
 1. cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
hence h\<^sub>u: "height u > 0"
[PROOF STATE]
proof (prove)
using this:
height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0

goal (1 subgoal):
 1. 0 < height u
[PROOF STEP]
using a\<^sub>u assms
[PROOF STATE]
proof (prove)
using this:
height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0
alphabet (splitLeaf t w\<^sub>a a w\<^sub>b b) = alphabet u
consistent t
optimum t
a \<in> alphabet t
b \<notin> alphabet t
freq t a = w\<^sub>a + w\<^sub>b
\<forall>c\<in>alphabet t. w\<^sub>a \<le> freq t c \<and> w\<^sub>b \<le> freq t c

goal (1 subgoal):
 1. 0 < height u
[PROOF STEP]
by (auto intro: height_gt_0_alphabet_eq_imp_height_gt_0)
[PROOF STATE]
proof (state)
this:
0 < height u

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
have a\<^sub>a: "a \<in> alphabet u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> alphabet u
[PROOF STEP]
using a\<^sub>u assms
[PROOF STATE]
proof (prove)
using this:
alphabet (splitLeaf t w\<^sub>a a w\<^sub>b b) = alphabet u
consistent t
optimum t
a \<in> alphabet t
b \<notin> alphabet t
freq t a = w\<^sub>a + w\<^sub>b
\<forall>c\<in>alphabet t. w\<^sub>a \<le> freq t c \<and> w\<^sub>b \<le> freq t c

goal (1 subgoal):
 1. a \<in> alphabet u
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
a \<in> alphabet u

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
have a\<^sub>b: "b \<in> alphabet u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in> alphabet u
[PROOF STEP]
using a\<^sub>u assms
[PROOF STATE]
proof (prove)
using this:
alphabet (splitLeaf t w\<^sub>a a w\<^sub>b b) = alphabet u
consistent t
optimum t
a \<in> alphabet t
b \<notin> alphabet t
freq t a = w\<^sub>a + w\<^sub>b
\<forall>c\<in>alphabet t. w\<^sub>a \<le> freq t c \<and> w\<^sub>b \<le> freq t c

goal (1 subgoal):
 1. b \<in> alphabet u
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
b \<in> alphabet u

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
have ab: "a \<noteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
consistent t
optimum t
a \<in> alphabet t
b \<notin> alphabet t
freq t a = w\<^sub>a + w\<^sub>b
\<forall>c\<in>alphabet t. w\<^sub>a \<le> freq t c \<and> w\<^sub>b \<le> freq t c

goal (1 subgoal):
 1. a \<noteq> b
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<noteq> b

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
from exists_at_height[OF c\<^sub>u]
[PROOF STATE]
proof (chain)
picking this:
\<exists>a\<in>alphabet u. depth u a = height u
[PROOF STEP]
obtain c where a\<^sub>c: "c \<in> alphabet u" and d\<^sub>c: "depth u c = height u"
[PROOF STATE]
proof (prove)
using this:
\<exists>a\<in>alphabet u. depth u a = height u

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>c \<in> alphabet u; depth u c = height u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
c \<in> alphabet u
depth u c = height u

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
let ?d = "sibling u c"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
have dc: "?d \<noteq> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sibling u c \<noteq> c
[PROOF STEP]
using d\<^sub>c c\<^sub>u h\<^sub>u a\<^sub>c
[PROOF STATE]
proof (prove)
using this:
depth u c = height u
consistent u
0 < height u
c \<in> alphabet u

goal (1 subgoal):
 1. sibling u c \<noteq> c
[PROOF STEP]
by (metis depth_height_imp_sibling_ne)
[PROOF STATE]
proof (state)
this:
sibling u c \<noteq> c

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
have a\<^sub>d: "?d \<in> alphabet u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sibling u c \<in> alphabet u
[PROOF STEP]
using dc
[PROOF STATE]
proof (prove)
using this:
sibling u c \<noteq> c

goal (1 subgoal):
 1. sibling u c \<in> alphabet u
[PROOF STEP]
by (rule sibling_ne_imp_sibling_in_alphabet)
[PROOF STATE]
proof (state)
this:
sibling u c \<in> alphabet u

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
have d\<^sub>d: "depth u ?d = height u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. depth u (sibling u c) = height u
[PROOF STEP]
using d\<^sub>c c\<^sub>u
[PROOF STATE]
proof (prove)
using this:
depth u c = height u
consistent u

goal (1 subgoal):
 1. depth u (sibling u c) = height u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
depth u (sibling u c) = height u

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
let ?u' = "swapFourSyms u a b c ?d"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
have c\<^sub>u\<^sub>': "consistent ?u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent (swapFourSyms u a b c (sibling u c))
[PROOF STEP]
using c\<^sub>u
[PROOF STATE]
proof (prove)
using this:
consistent u

goal (1 subgoal):
 1. consistent (swapFourSyms u a b c (sibling u c))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
consistent (swapFourSyms u a b c (sibling u c))

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
have a\<^sub>u\<^sub>': "alphabet ?u' = alphabet u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphabet (swapFourSyms u a b c (sibling u c)) = alphabet u
[PROOF STEP]
using a\<^sub>a a\<^sub>b a\<^sub>c a\<^sub>d a\<^sub>u
[PROOF STATE]
proof (prove)
using this:
a \<in> alphabet u
b \<in> alphabet u
c \<in> alphabet u
sibling u c \<in> alphabet u
alphabet (splitLeaf t w\<^sub>a a w\<^sub>b b) = alphabet u

goal (1 subgoal):
 1. alphabet (swapFourSyms u a b c (sibling u c)) = alphabet u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
alphabet (swapFourSyms u a b c (sibling u c)) = alphabet u

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
have f\<^sub>u\<^sub>': "freq ?u' = freq u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freq (swapFourSyms u a b c (sibling u c)) = freq u
[PROOF STEP]
using a\<^sub>a a\<^sub>b a\<^sub>c a\<^sub>d c\<^sub>u f\<^sub>u
[PROOF STATE]
proof (prove)
using this:
a \<in> alphabet u
b \<in> alphabet u
c \<in> alphabet u
sibling u c \<in> alphabet u
consistent u
freq (splitLeaf t w\<^sub>a a w\<^sub>b b) = freq u

goal (1 subgoal):
 1. freq (swapFourSyms u a b c (sibling u c)) = freq u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
freq (swapFourSyms u a b c (sibling u c)) = freq u

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
have s\<^sub>a: "sibling ?u' a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sibling (swapFourSyms u a b c (sibling u c)) a = b
[PROOF STEP]
using c\<^sub>u a\<^sub>a a\<^sub>b a\<^sub>c ab dc
[PROOF STATE]
proof (prove)
using this:
consistent u
a \<in> alphabet u
b \<in> alphabet u
c \<in> alphabet u
a \<noteq> b
sibling u c \<noteq> c

goal (1 subgoal):
 1. sibling (swapFourSyms u a b c (sibling u c)) a = b
[PROOF STEP]
by (rule sibling_swapFourSyms_when_4th_is_sibling)
[PROOF STATE]
proof (state)
this:
sibling (swapFourSyms u a b c (sibling u c)) a = b

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
let ?v = "mergeSibling ?u' a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
have c\<^sub>v: "consistent ?v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent (mergeSibling (swapFourSyms u a b c (sibling u c)) a)
[PROOF STEP]
using c\<^sub>u\<^sub>'
[PROOF STATE]
proof (prove)
using this:
consistent (swapFourSyms u a b c (sibling u c))

goal (1 subgoal):
 1. consistent (mergeSibling (swapFourSyms u a b c (sibling u c)) a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
consistent (mergeSibling (swapFourSyms u a b c (sibling u c)) a)

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
have a\<^sub>v: "alphabet ?v = alphabet t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphabet (mergeSibling (swapFourSyms u a b c (sibling u c)) a) = alphabet t
[PROOF STEP]
using s\<^sub>a c\<^sub>u\<^sub>' a\<^sub>u\<^sub>' a\<^sub>a a\<^sub>u assms
[PROOF STATE]
proof (prove)
using this:
sibling (swapFourSyms u a b c (sibling u c)) a = b
consistent (swapFourSyms u a b c (sibling u c))
alphabet (swapFourSyms u a b c (sibling u c)) = alphabet u
a \<in> alphabet u
alphabet (splitLeaf t w\<^sub>a a w\<^sub>b b) = alphabet u
consistent t
optimum t
a \<in> alphabet t
b \<notin> alphabet t
freq t a = w\<^sub>a + w\<^sub>b
\<forall>c\<in>alphabet t. w\<^sub>a \<le> freq t c \<and> w\<^sub>b \<le> freq t c

goal (1 subgoal):
 1. alphabet (mergeSibling (swapFourSyms u a b c (sibling u c)) a) = alphabet t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
alphabet (mergeSibling (swapFourSyms u a b c (sibling u c)) a) = alphabet t

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
have f\<^sub>v: "freq ?v = freq t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freq (mergeSibling (swapFourSyms u a b c (sibling u c)) a) = freq t
[PROOF STEP]
using s\<^sub>a c\<^sub>u\<^sub>' a\<^sub>u\<^sub>' f\<^sub>u\<^sub>' f\<^sub>u[THEN sym] ab a\<^sub>u[THEN sym] assms
[PROOF STATE]
proof (prove)
using this:
sibling (swapFourSyms u a b c (sibling u c)) a = b
consistent (swapFourSyms u a b c (sibling u c))
alphabet (swapFourSyms u a b c (sibling u c)) = alphabet u
freq (swapFourSyms u a b c (sibling u c)) = freq u
freq u = freq (splitLeaf t w\<^sub>a a w\<^sub>b b)
a \<noteq> b
alphabet u = alphabet (splitLeaf t w\<^sub>a a w\<^sub>b b)
consistent t
optimum t
a \<in> alphabet t
b \<notin> alphabet t
freq t a = w\<^sub>a + w\<^sub>b
\<forall>c\<in>alphabet t. w\<^sub>a \<le> freq t c \<and> w\<^sub>b \<le> freq t c

goal (1 subgoal):
 1. freq (mergeSibling (swapFourSyms u a b c (sibling u c)) a) = freq t
[PROOF STEP]
by (simp add: freq_mergeSibling ext)
[PROOF STATE]
proof (state)
this:
freq (mergeSibling (swapFourSyms u a b c (sibling u c)) a) = freq t

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
have "cost ?t' = cost t + w\<^sub>a + w\<^sub>b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cost (splitLeaf t w\<^sub>a a w\<^sub>b b) = cost t + w\<^sub>a + w\<^sub>b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
consistent t
optimum t
a \<in> alphabet t
b \<notin> alphabet t
freq t a = w\<^sub>a + w\<^sub>b
\<forall>c\<in>alphabet t. w\<^sub>a \<le> freq t c \<and> w\<^sub>b \<le> freq t c

goal (1 subgoal):
 1. cost (splitLeaf t w\<^sub>a a w\<^sub>b b) = cost t + w\<^sub>a + w\<^sub>b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cost (splitLeaf t w\<^sub>a a w\<^sub>b b) = cost t + w\<^sub>a + w\<^sub>b

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cost (splitLeaf t w\<^sub>a a w\<^sub>b b) = cost t + w\<^sub>a + w\<^sub>b

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
have "\<dots> \<le> cost ?v + w\<^sub>a + w\<^sub>b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cost t + w\<^sub>a + w\<^sub>b \<le> cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + w\<^sub>a + w\<^sub>b
[PROOF STEP]
using c\<^sub>v a\<^sub>v f\<^sub>v \<open>optimum t\<close>
[PROOF STATE]
proof (prove)
using this:
consistent (mergeSibling (swapFourSyms u a b c (sibling u c)) a)
alphabet (mergeSibling (swapFourSyms u a b c (sibling u c)) a) = alphabet t
freq (mergeSibling (swapFourSyms u a b c (sibling u c)) a) = freq t
optimum t

goal (1 subgoal):
 1. cost t + w\<^sub>a + w\<^sub>b \<le> cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + w\<^sub>a + w\<^sub>b
[PROOF STEP]
by (simp add: optimum_def)
[PROOF STATE]
proof (state)
this:
cost t + w\<^sub>a + w\<^sub>b \<le> cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + w\<^sub>a + w\<^sub>b

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cost t + w\<^sub>a + w\<^sub>b \<le> cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + w\<^sub>a + w\<^sub>b

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
have "\<dots> = cost ?u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + w\<^sub>a + w\<^sub>b = cost (swapFourSyms u a b c (sibling u c))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + w\<^sub>a + w\<^sub>b = cost (swapFourSyms u a b c (sibling u c))
[PROOF STEP]
have "cost ?v + freq ?u' a + freq ?u' (sibling ?u' a) = cost ?u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + freq (swapFourSyms u a b c (sibling u c)) a + freq (swapFourSyms u a b c (sibling u c)) (sibling (swapFourSyms u a b c (sibling u c)) a) = cost (swapFourSyms u a b c (sibling u c))
[PROOF STEP]
using c\<^sub>u\<^sub>' s\<^sub>a assms
[PROOF STATE]
proof (prove)
using this:
consistent (swapFourSyms u a b c (sibling u c))
sibling (swapFourSyms u a b c (sibling u c)) a = b
consistent t
optimum t
a \<in> alphabet t
b \<notin> alphabet t
freq t a = w\<^sub>a + w\<^sub>b
\<forall>c\<in>alphabet t. w\<^sub>a \<le> freq t c \<and> w\<^sub>b \<le> freq t c

goal (1 subgoal):
 1. cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + freq (swapFourSyms u a b c (sibling u c)) a + freq (swapFourSyms u a b c (sibling u c)) (sibling (swapFourSyms u a b c (sibling u c)) a) = cost (swapFourSyms u a b c (sibling u c))
[PROOF STEP]
by (subst cost_mergeSibling) auto
[PROOF STATE]
proof (state)
this:
cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + freq (swapFourSyms u a b c (sibling u c)) a + freq (swapFourSyms u a b c (sibling u c)) (sibling (swapFourSyms u a b c (sibling u c)) a) = cost (swapFourSyms u a b c (sibling u c))

goal (1 subgoal):
 1. cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + w\<^sub>a + w\<^sub>b = cost (swapFourSyms u a b c (sibling u c))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + freq (swapFourSyms u a b c (sibling u c)) a + freq (swapFourSyms u a b c (sibling u c)) (sibling (swapFourSyms u a b c (sibling u c)) a) = cost (swapFourSyms u a b c (sibling u c))

goal (1 subgoal):
 1. cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + w\<^sub>a + w\<^sub>b = cost (swapFourSyms u a b c (sibling u c))
[PROOF STEP]
have "w\<^sub>a = freq ?u' a" "w\<^sub>b = freq ?u' b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w\<^sub>a = freq (swapFourSyms u a b c (sibling u c)) a &&& w\<^sub>b = freq (swapFourSyms u a b c (sibling u c)) b
[PROOF STEP]
using f\<^sub>u\<^sub>' f\<^sub>u[THEN sym] assms
[PROOF STATE]
proof (prove)
using this:
freq (swapFourSyms u a b c (sibling u c)) = freq u
freq u = freq (splitLeaf t w\<^sub>a a w\<^sub>b b)
consistent t
optimum t
a \<in> alphabet t
b \<notin> alphabet t
freq t a = w\<^sub>a + w\<^sub>b
\<forall>c\<in>alphabet t. w\<^sub>a \<le> freq t c \<and> w\<^sub>b \<le> freq t c

goal (1 subgoal):
 1. w\<^sub>a = freq (swapFourSyms u a b c (sibling u c)) a &&& w\<^sub>b = freq (swapFourSyms u a b c (sibling u c)) b
[PROOF STEP]
by clarsimp+
[PROOF STATE]
proof (state)
this:
w\<^sub>a = freq (swapFourSyms u a b c (sibling u c)) a
w\<^sub>b = freq (swapFourSyms u a b c (sibling u c)) b

goal (1 subgoal):
 1. cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + w\<^sub>a + w\<^sub>b = cost (swapFourSyms u a b c (sibling u c))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + freq (swapFourSyms u a b c (sibling u c)) a + freq (swapFourSyms u a b c (sibling u c)) (sibling (swapFourSyms u a b c (sibling u c)) a) = cost (swapFourSyms u a b c (sibling u c))
w\<^sub>a = freq (swapFourSyms u a b c (sibling u c)) a
w\<^sub>b = freq (swapFourSyms u a b c (sibling u c)) b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + freq (swapFourSyms u a b c (sibling u c)) a + freq (swapFourSyms u a b c (sibling u c)) (sibling (swapFourSyms u a b c (sibling u c)) a) = cost (swapFourSyms u a b c (sibling u c))
w\<^sub>a = freq (swapFourSyms u a b c (sibling u c)) a
w\<^sub>b = freq (swapFourSyms u a b c (sibling u c)) b

goal (1 subgoal):
 1. cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + w\<^sub>a + w\<^sub>b = cost (swapFourSyms u a b c (sibling u c))
[PROOF STEP]
using s\<^sub>a
[PROOF STATE]
proof (prove)
using this:
cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + freq (swapFourSyms u a b c (sibling u c)) a + freq (swapFourSyms u a b c (sibling u c)) (sibling (swapFourSyms u a b c (sibling u c)) a) = cost (swapFourSyms u a b c (sibling u c))
w\<^sub>a = freq (swapFourSyms u a b c (sibling u c)) a
w\<^sub>b = freq (swapFourSyms u a b c (sibling u c)) b
sibling (swapFourSyms u a b c (sibling u c)) a = b

goal (1 subgoal):
 1. cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + w\<^sub>a + w\<^sub>b = cost (swapFourSyms u a b c (sibling u c))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + w\<^sub>a + w\<^sub>b = cost (swapFourSyms u a b c (sibling u c))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + w\<^sub>a + w\<^sub>b = cost (swapFourSyms u a b c (sibling u c))

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cost (mergeSibling (swapFourSyms u a b c (sibling u c)) a) + w\<^sub>a + w\<^sub>b = cost (swapFourSyms u a b c (sibling u c))

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
have "\<dots> \<le> cost u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cost (swapFourSyms u a b c (sibling u c)) \<le> cost u
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cost (swapFourSyms u a b c (sibling u c)) \<le> cost u
[PROOF STEP]
have "minima u a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. minima u a b
[PROOF STEP]
using a\<^sub>u f\<^sub>u assms
[PROOF STATE]
proof (prove)
using this:
alphabet (splitLeaf t w\<^sub>a a w\<^sub>b b) = alphabet u
freq (splitLeaf t w\<^sub>a a w\<^sub>b b) = freq u
consistent t
optimum t
a \<in> alphabet t
b \<notin> alphabet t
freq t a = w\<^sub>a + w\<^sub>b
\<forall>c\<in>alphabet t. w\<^sub>a \<le> freq t c \<and> w\<^sub>b \<le> freq t c

goal (1 subgoal):
 1. minima u a b
[PROOF STEP]
by (subst twice_freq_le_imp_minima) auto
[PROOF STATE]
proof (state)
this:
minima u a b

goal (1 subgoal):
 1. cost (swapFourSyms u a b c (sibling u c)) \<le> cost u
[PROOF STEP]
with c\<^sub>u
[PROOF STATE]
proof (chain)
picking this:
consistent u
minima u a b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
consistent u
minima u a b

goal (1 subgoal):
 1. cost (swapFourSyms u a b c (sibling u c)) \<le> cost u
[PROOF STEP]
using a\<^sub>c a\<^sub>d d\<^sub>c d\<^sub>d dc[THEN not_sym]
[PROOF STATE]
proof (prove)
using this:
consistent u
minima u a b
c \<in> alphabet u
sibling u c \<in> alphabet u
depth u c = height u
depth u (sibling u c) = height u
c \<noteq> sibling u c

goal (1 subgoal):
 1. cost (swapFourSyms u a b c (sibling u c)) \<le> cost u
[PROOF STEP]
by (rule cost_swapFourSyms_le)
[PROOF STATE]
proof (state)
this:
cost (swapFourSyms u a b c (sibling u c)) \<le> cost u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cost (swapFourSyms u a b c (sibling u c)) \<le> cost u

goal (1 subgoal):
 1. height (splitLeaf t w\<^sub>a a w\<^sub>b b) \<noteq> 0 \<Longrightarrow> cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u

goal (1 subgoal):
 1. cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cost (splitLeaf t w\<^sub>a a w\<^sub>b b) \<le> cost u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cachedWeight_splitLeaf[simp]:
"cachedWeight (splitLeaf t w\<^sub>a a w\<^sub>b b) = cachedWeight t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cachedWeight (splitLeaf t w\<^sub>a a w\<^sub>b b) = cachedWeight t
[PROOF STEP]
by (case_tac t) simp+


[STATEMENT]
lemma splitLeaf\<^sub>F_insortTree_when_in_alphabet_left[simp]:
"\<lbrakk>a \<in> alphabet t; consistent t; a \<notin> alphabet\<^sub>F ts; freq t a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow>
 splitLeaf\<^sub>F (insortTree t ts) w\<^sub>a a w\<^sub>b b = insortTree (splitLeaf t w\<^sub>a a w\<^sub>b b) ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> alphabet t; consistent t; a \<notin> alphabet\<^sub>F ts; freq t a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf\<^sub>F (insortTree t ts) w\<^sub>a a w\<^sub>b b = insortTree (splitLeaf t w\<^sub>a a w\<^sub>b b) ts
[PROOF STEP]
by (induct ts) simp+


[STATEMENT]
lemma splitLeaf\<^sub>F_insortTree_when_in_alphabet\<^sub>F_tail[simp]:
"\<lbrakk>a \<in> alphabet\<^sub>F ts; consistent\<^sub>F ts; a \<notin> alphabet t; freq\<^sub>F ts a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow>
 splitLeaf\<^sub>F (insortTree t ts) w\<^sub>a a w\<^sub>b b =
 insortTree t (splitLeaf\<^sub>F ts w\<^sub>a a w\<^sub>b b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> alphabet\<^sub>F ts; consistent\<^sub>F ts; a \<notin> alphabet t; freq\<^sub>F ts a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf\<^sub>F (insortTree t ts) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F ts w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
proof (induct ts)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>a \<in> alphabet\<^sub>F []; consistent\<^sub>F []; a \<notin> alphabet t; freq\<^sub>F [] a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf\<^sub>F (insortTree t []) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F [] w\<^sub>a a w\<^sub>b b)
 2. \<And>aa ts. \<lbrakk>\<lbrakk>a \<in> alphabet\<^sub>F ts; consistent\<^sub>F ts; a \<notin> alphabet t; freq\<^sub>F ts a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf\<^sub>F (insortTree t ts) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F ts w\<^sub>a a w\<^sub>b b); a \<in> alphabet\<^sub>F (aa # ts); consistent\<^sub>F (aa # ts); a \<notin> alphabet t; freq\<^sub>F (aa # ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf\<^sub>F (insortTree t (aa # ts)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (aa # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
a \<in> alphabet\<^sub>F []
consistent\<^sub>F []
a \<notin> alphabet t
freq\<^sub>F [] a = w\<^sub>a + w\<^sub>b

goal (2 subgoals):
 1. \<lbrakk>a \<in> alphabet\<^sub>F []; consistent\<^sub>F []; a \<notin> alphabet t; freq\<^sub>F [] a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf\<^sub>F (insortTree t []) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F [] w\<^sub>a a w\<^sub>b b)
 2. \<And>aa ts. \<lbrakk>\<lbrakk>a \<in> alphabet\<^sub>F ts; consistent\<^sub>F ts; a \<notin> alphabet t; freq\<^sub>F ts a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf\<^sub>F (insortTree t ts) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F ts w\<^sub>a a w\<^sub>b b); a \<in> alphabet\<^sub>F (aa # ts); consistent\<^sub>F (aa # ts); a \<notin> alphabet t; freq\<^sub>F (aa # ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf\<^sub>F (insortTree t (aa # ts)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (aa # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
a \<in> alphabet\<^sub>F []
consistent\<^sub>F []
a \<notin> alphabet t
freq\<^sub>F [] a = w\<^sub>a + w\<^sub>b

goal (1 subgoal):
 1. splitLeaf\<^sub>F (insortTree t []) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F [] w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
splitLeaf\<^sub>F (insortTree t []) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F [] w\<^sub>a a w\<^sub>b b)

goal (1 subgoal):
 1. \<And>aa ts. \<lbrakk>\<lbrakk>a \<in> alphabet\<^sub>F ts; consistent\<^sub>F ts; a \<notin> alphabet t; freq\<^sub>F ts a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf\<^sub>F (insortTree t ts) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F ts w\<^sub>a a w\<^sub>b b); a \<in> alphabet\<^sub>F (aa # ts); consistent\<^sub>F (aa # ts); a \<notin> alphabet t; freq\<^sub>F (aa # ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf\<^sub>F (insortTree t (aa # ts)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (aa # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa ts. \<lbrakk>\<lbrakk>a \<in> alphabet\<^sub>F ts; consistent\<^sub>F ts; a \<notin> alphabet t; freq\<^sub>F ts a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf\<^sub>F (insortTree t ts) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F ts w\<^sub>a a w\<^sub>b b); a \<in> alphabet\<^sub>F (aa # ts); consistent\<^sub>F (aa # ts); a \<notin> alphabet t; freq\<^sub>F (aa # ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf\<^sub>F (insortTree t (aa # ts)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (aa # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
case (Cons u us)
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<in> alphabet\<^sub>F us; consistent\<^sub>F us; a \<notin> alphabet t; freq\<^sub>F us a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf\<^sub>F (insortTree t us) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F us w\<^sub>a a w\<^sub>b b)
a \<in> alphabet\<^sub>F (u # us)
consistent\<^sub>F (u # us)
a \<notin> alphabet t
freq\<^sub>F (u # us) a = w\<^sub>a + w\<^sub>b

goal (1 subgoal):
 1. \<And>aa ts. \<lbrakk>\<lbrakk>a \<in> alphabet\<^sub>F ts; consistent\<^sub>F ts; a \<notin> alphabet t; freq\<^sub>F ts a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf\<^sub>F (insortTree t ts) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F ts w\<^sub>a a w\<^sub>b b); a \<in> alphabet\<^sub>F (aa # ts); consistent\<^sub>F (aa # ts); a \<notin> alphabet t; freq\<^sub>F (aa # ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf\<^sub>F (insortTree t (aa # ts)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (aa # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. splitLeaf\<^sub>F (insortTree t (u # us)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (u # us) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
proof (cases "a \<in> alphabet u")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<in> alphabet u \<Longrightarrow> splitLeaf\<^sub>F (insortTree t (u # us)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (u # us) w\<^sub>a a w\<^sub>b b)
 2. a \<notin> alphabet u \<Longrightarrow> splitLeaf\<^sub>F (insortTree t (u # us)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (u # us) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<in> alphabet u

goal (2 subgoals):
 1. a \<in> alphabet u \<Longrightarrow> splitLeaf\<^sub>F (insortTree t (u # us)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (u # us) w\<^sub>a a w\<^sub>b b)
 2. a \<notin> alphabet u \<Longrightarrow> splitLeaf\<^sub>F (insortTree t (u # us)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (u # us) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
hence "a \<notin> alphabet\<^sub>F us"
[PROOF STATE]
proof (prove)
using this:
a \<in> alphabet u

goal (1 subgoal):
 1. a \<notin> alphabet\<^sub>F us
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
a \<in> alphabet u
\<lbrakk>a \<in> alphabet\<^sub>F us; consistent\<^sub>F us; a \<notin> alphabet t; freq\<^sub>F us a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf\<^sub>F (insortTree t us) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F us w\<^sub>a a w\<^sub>b b)
a \<in> alphabet\<^sub>F (u # us)
consistent\<^sub>F (u # us)
a \<notin> alphabet t
freq\<^sub>F (u # us) a = w\<^sub>a + w\<^sub>b

goal (1 subgoal):
 1. a \<notin> alphabet\<^sub>F us
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<notin> alphabet\<^sub>F us

goal (2 subgoals):
 1. a \<in> alphabet u \<Longrightarrow> splitLeaf\<^sub>F (insortTree t (u # us)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (u # us) w\<^sub>a a w\<^sub>b b)
 2. a \<notin> alphabet u \<Longrightarrow> splitLeaf\<^sub>F (insortTree t (u # us)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (u # us) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<notin> alphabet\<^sub>F us

goal (1 subgoal):
 1. splitLeaf\<^sub>F (insortTree t (u # us)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (u # us) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
a \<notin> alphabet\<^sub>F us
\<lbrakk>a \<in> alphabet\<^sub>F us; consistent\<^sub>F us; a \<notin> alphabet t; freq\<^sub>F us a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf\<^sub>F (insortTree t us) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F us w\<^sub>a a w\<^sub>b b)
a \<in> alphabet\<^sub>F (u # us)
consistent\<^sub>F (u # us)
a \<notin> alphabet t
freq\<^sub>F (u # us) a = w\<^sub>a + w\<^sub>b

goal (1 subgoal):
 1. splitLeaf\<^sub>F (insortTree t (u # us)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (u # us) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
splitLeaf\<^sub>F (insortTree t (u # us)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (u # us) w\<^sub>a a w\<^sub>b b)

goal (1 subgoal):
 1. a \<notin> alphabet u \<Longrightarrow> splitLeaf\<^sub>F (insortTree t (u # us)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (u # us) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<notin> alphabet u \<Longrightarrow> splitLeaf\<^sub>F (insortTree t (u # us)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (u # us) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<notin> alphabet u

goal (1 subgoal):
 1. a \<notin> alphabet u \<Longrightarrow> splitLeaf\<^sub>F (insortTree t (u # us)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (u # us) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<notin> alphabet u

goal (1 subgoal):
 1. splitLeaf\<^sub>F (insortTree t (u # us)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (u # us) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
a \<notin> alphabet u
\<lbrakk>a \<in> alphabet\<^sub>F us; consistent\<^sub>F us; a \<notin> alphabet t; freq\<^sub>F us a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf\<^sub>F (insortTree t us) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F us w\<^sub>a a w\<^sub>b b)
a \<in> alphabet\<^sub>F (u # us)
consistent\<^sub>F (u # us)
a \<notin> alphabet t
freq\<^sub>F (u # us) a = w\<^sub>a + w\<^sub>b

goal (1 subgoal):
 1. splitLeaf\<^sub>F (insortTree t (u # us)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (u # us) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
splitLeaf\<^sub>F (insortTree t (u # us)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (u # us) w\<^sub>a a w\<^sub>b b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
splitLeaf\<^sub>F (insortTree t (u # us)) w\<^sub>a a w\<^sub>b b = insortTree t (splitLeaf\<^sub>F (u # us) w\<^sub>a a w\<^sub>b b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma splitLeaf_huffman_commute:
"\<lbrakk>consistent\<^sub>F ts; ts \<noteq> []; a \<in> alphabet\<^sub>F ts; freq\<^sub>F ts a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow>
 splitLeaf (huffman ts) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F ts w\<^sub>a a w\<^sub>b b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent\<^sub>F ts; ts \<noteq> []; a \<in> alphabet\<^sub>F ts; freq\<^sub>F ts a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman ts) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F ts w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
proof (induct ts rule: huffman.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>t. \<lbrakk>consistent\<^sub>F [t]; [t] \<noteq> []; a \<in> alphabet\<^sub>F [t]; freq\<^sub>F [t] a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman [t]) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F [t] w\<^sub>a a w\<^sub>b b)
 2. \<And>t\<^sub>1 t\<^sub>2 ts. \<lbrakk>\<lbrakk>consistent\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts \<noteq> []; a \<in> alphabet\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); freq\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) w\<^sub>a a w\<^sub>b b); consistent\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts); t\<^sub>1 # t\<^sub>2 # ts \<noteq> []; a \<in> alphabet\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts); freq\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
 3. \<lbrakk>consistent\<^sub>F []; [] \<noteq> []; a \<in> alphabet\<^sub>F []; freq\<^sub>F [] a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman []) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F [] w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
case (1 t)
[PROOF STATE]
proof (state)
this:
consistent\<^sub>F [t]
[t] \<noteq> []
a \<in> alphabet\<^sub>F [t]
freq\<^sub>F [t] a = w\<^sub>a + w\<^sub>b

goal (3 subgoals):
 1. \<And>t. \<lbrakk>consistent\<^sub>F [t]; [t] \<noteq> []; a \<in> alphabet\<^sub>F [t]; freq\<^sub>F [t] a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman [t]) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F [t] w\<^sub>a a w\<^sub>b b)
 2. \<And>t\<^sub>1 t\<^sub>2 ts. \<lbrakk>\<lbrakk>consistent\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts \<noteq> []; a \<in> alphabet\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); freq\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) w\<^sub>a a w\<^sub>b b); consistent\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts); t\<^sub>1 # t\<^sub>2 # ts \<noteq> []; a \<in> alphabet\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts); freq\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
 3. \<lbrakk>consistent\<^sub>F []; [] \<noteq> []; a \<in> alphabet\<^sub>F []; freq\<^sub>F [] a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman []) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F [] w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
consistent\<^sub>F [t]
[t] \<noteq> []
a \<in> alphabet\<^sub>F [t]
freq\<^sub>F [t] a = w\<^sub>a + w\<^sub>b

goal (1 subgoal):
 1. splitLeaf (huffman [t]) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F [t] w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
splitLeaf (huffman [t]) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F [t] w\<^sub>a a w\<^sub>b b)

goal (2 subgoals):
 1. \<And>t\<^sub>1 t\<^sub>2 ts. \<lbrakk>\<lbrakk>consistent\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts \<noteq> []; a \<in> alphabet\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); freq\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) w\<^sub>a a w\<^sub>b b); consistent\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts); t\<^sub>1 # t\<^sub>2 # ts \<noteq> []; a \<in> alphabet\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts); freq\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
 2. \<lbrakk>consistent\<^sub>F []; [] \<noteq> []; a \<in> alphabet\<^sub>F []; freq\<^sub>F [] a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman []) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F [] w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t\<^sub>1 t\<^sub>2 ts. \<lbrakk>\<lbrakk>consistent\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts \<noteq> []; a \<in> alphabet\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); freq\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) w\<^sub>a a w\<^sub>b b); consistent\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts); t\<^sub>1 # t\<^sub>2 # ts \<noteq> []; a \<in> alphabet\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts); freq\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
 2. \<lbrakk>consistent\<^sub>F []; [] \<noteq> []; a \<in> alphabet\<^sub>F []; freq\<^sub>F [] a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman []) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F [] w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
case (2 t\<^sub>1 t\<^sub>2 ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>consistent\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts \<noteq> []; a \<in> alphabet\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); freq\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) w\<^sub>a a w\<^sub>b b)
consistent\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts)
t\<^sub>1 # t\<^sub>2 # ts \<noteq> []
a \<in> alphabet\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts)
freq\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) a = w\<^sub>a + w\<^sub>b

goal (2 subgoals):
 1. \<And>t\<^sub>1 t\<^sub>2 ts. \<lbrakk>\<lbrakk>consistent\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts \<noteq> []; a \<in> alphabet\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); freq\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) w\<^sub>a a w\<^sub>b b); consistent\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts); t\<^sub>1 # t\<^sub>2 # ts \<noteq> []; a \<in> alphabet\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts); freq\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
 2. \<lbrakk>consistent\<^sub>F []; [] \<noteq> []; a \<in> alphabet\<^sub>F []; freq\<^sub>F [] a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman []) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F [] w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
note hyps = 2
[PROOF STATE]
proof (state)
this:
\<lbrakk>consistent\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts \<noteq> []; a \<in> alphabet\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); freq\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) w\<^sub>a a w\<^sub>b b)
consistent\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts)
t\<^sub>1 # t\<^sub>2 # ts \<noteq> []
a \<in> alphabet\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts)
freq\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) a = w\<^sub>a + w\<^sub>b

goal (2 subgoals):
 1. \<And>t\<^sub>1 t\<^sub>2 ts. \<lbrakk>\<lbrakk>consistent\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts \<noteq> []; a \<in> alphabet\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); freq\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) w\<^sub>a a w\<^sub>b b); consistent\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts); t\<^sub>1 # t\<^sub>2 # ts \<noteq> []; a \<in> alphabet\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts); freq\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
 2. \<lbrakk>consistent\<^sub>F []; [] \<noteq> []; a \<in> alphabet\<^sub>F []; freq\<^sub>F [] a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman []) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F [] w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
proof (cases "a \<in> alphabet t\<^sub>1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<in> alphabet t\<^sub>1 \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
 2. a \<notin> alphabet t\<^sub>1 \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<in> alphabet t\<^sub>1

goal (2 subgoals):
 1. a \<in> alphabet t\<^sub>1 \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
 2. a \<notin> alphabet t\<^sub>1 \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
hence "a \<notin> alphabet t\<^sub>2" "a \<notin> alphabet\<^sub>F ts"
[PROOF STATE]
proof (prove)
using this:
a \<in> alphabet t\<^sub>1

goal (1 subgoal):
 1. a \<notin> alphabet t\<^sub>2 &&& a \<notin> alphabet\<^sub>F ts
[PROOF STEP]
using hyps
[PROOF STATE]
proof (prove)
using this:
a \<in> alphabet t\<^sub>1
\<lbrakk>consistent\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts \<noteq> []; a \<in> alphabet\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); freq\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) w\<^sub>a a w\<^sub>b b)
consistent\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts)
t\<^sub>1 # t\<^sub>2 # ts \<noteq> []
a \<in> alphabet\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts)
freq\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) a = w\<^sub>a + w\<^sub>b

goal (1 subgoal):
 1. a \<notin> alphabet t\<^sub>2 &&& a \<notin> alphabet\<^sub>F ts
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<notin> alphabet t\<^sub>2
a \<notin> alphabet\<^sub>F ts

goal (2 subgoals):
 1. a \<in> alphabet t\<^sub>1 \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
 2. a \<notin> alphabet t\<^sub>1 \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<notin> alphabet t\<^sub>2
a \<notin> alphabet\<^sub>F ts

goal (1 subgoal):
 1. splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
using hyps
[PROOF STATE]
proof (prove)
using this:
a \<notin> alphabet t\<^sub>2
a \<notin> alphabet\<^sub>F ts
\<lbrakk>consistent\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts \<noteq> []; a \<in> alphabet\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); freq\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) w\<^sub>a a w\<^sub>b b)
consistent\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts)
t\<^sub>1 # t\<^sub>2 # ts \<noteq> []
a \<in> alphabet\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts)
freq\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) a = w\<^sub>a + w\<^sub>b

goal (1 subgoal):
 1. splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
by (simp add: uniteTrees_def)
[PROOF STATE]
proof (state)
this:
splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)

goal (1 subgoal):
 1. a \<notin> alphabet t\<^sub>1 \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<notin> alphabet t\<^sub>1 \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<notin> alphabet t\<^sub>1

goal (1 subgoal):
 1. a \<notin> alphabet t\<^sub>1 \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
note a\<^sub>1 = False
[PROOF STATE]
proof (state)
this:
a \<notin> alphabet t\<^sub>1

goal (1 subgoal):
 1. a \<notin> alphabet t\<^sub>1 \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
proof (cases "a \<in> alphabet t\<^sub>2")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<in> alphabet t\<^sub>2 \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
 2. a \<notin> alphabet t\<^sub>2 \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<in> alphabet t\<^sub>2

goal (2 subgoals):
 1. a \<in> alphabet t\<^sub>2 \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
 2. a \<notin> alphabet t\<^sub>2 \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
hence "a \<notin> alphabet\<^sub>F ts"
[PROOF STATE]
proof (prove)
using this:
a \<in> alphabet t\<^sub>2

goal (1 subgoal):
 1. a \<notin> alphabet\<^sub>F ts
[PROOF STEP]
using hyps
[PROOF STATE]
proof (prove)
using this:
a \<in> alphabet t\<^sub>2
\<lbrakk>consistent\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts \<noteq> []; a \<in> alphabet\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); freq\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) w\<^sub>a a w\<^sub>b b)
consistent\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts)
t\<^sub>1 # t\<^sub>2 # ts \<noteq> []
a \<in> alphabet\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts)
freq\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) a = w\<^sub>a + w\<^sub>b

goal (1 subgoal):
 1. a \<notin> alphabet\<^sub>F ts
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<notin> alphabet\<^sub>F ts

goal (2 subgoals):
 1. a \<in> alphabet t\<^sub>2 \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
 2. a \<notin> alphabet t\<^sub>2 \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<notin> alphabet\<^sub>F ts

goal (1 subgoal):
 1. splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
using a\<^sub>1 hyps
[PROOF STATE]
proof (prove)
using this:
a \<notin> alphabet\<^sub>F ts
a \<notin> alphabet t\<^sub>1
\<lbrakk>consistent\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts \<noteq> []; a \<in> alphabet\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); freq\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) w\<^sub>a a w\<^sub>b b)
consistent\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts)
t\<^sub>1 # t\<^sub>2 # ts \<noteq> []
a \<in> alphabet\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts)
freq\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) a = w\<^sub>a + w\<^sub>b

goal (1 subgoal):
 1. splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
by (simp add: uniteTrees_def)
[PROOF STATE]
proof (state)
this:
splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)

goal (1 subgoal):
 1. a \<notin> alphabet t\<^sub>2 \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<notin> alphabet t\<^sub>2 \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<notin> alphabet t\<^sub>2

goal (1 subgoal):
 1. a \<notin> alphabet t\<^sub>2 \<Longrightarrow> splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<notin> alphabet t\<^sub>2

goal (1 subgoal):
 1. splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
using a\<^sub>1 hyps
[PROOF STATE]
proof (prove)
using this:
a \<notin> alphabet t\<^sub>2
a \<notin> alphabet t\<^sub>1
\<lbrakk>consistent\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts \<noteq> []; a \<in> alphabet\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts); freq\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (insortTree (uniteTrees t\<^sub>1 t\<^sub>2) ts) w\<^sub>a a w\<^sub>b b)
consistent\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts)
t\<^sub>1 # t\<^sub>2 # ts \<noteq> []
a \<in> alphabet\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts)
freq\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) a = w\<^sub>a + w\<^sub>b

goal (1 subgoal):
 1. splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
splitLeaf (huffman (t\<^sub>1 # t\<^sub>2 # ts)) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F (t\<^sub>1 # t\<^sub>2 # ts) w\<^sub>a a w\<^sub>b b)

goal (1 subgoal):
 1. \<lbrakk>consistent\<^sub>F []; [] \<noteq> []; a \<in> alphabet\<^sub>F []; freq\<^sub>F [] a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman []) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F [] w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>consistent\<^sub>F []; [] \<noteq> []; a \<in> alphabet\<^sub>F []; freq\<^sub>F [] a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman []) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F [] w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
consistent\<^sub>F []
[] \<noteq> []
a \<in> alphabet\<^sub>F []
freq\<^sub>F [] a = w\<^sub>a + w\<^sub>b

goal (1 subgoal):
 1. \<lbrakk>consistent\<^sub>F []; [] \<noteq> []; a \<in> alphabet\<^sub>F []; freq\<^sub>F [] a = w\<^sub>a + w\<^sub>b\<rbrakk> \<Longrightarrow> splitLeaf (huffman []) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F [] w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
consistent\<^sub>F []
[] \<noteq> []
a \<in> alphabet\<^sub>F []
freq\<^sub>F [] a = w\<^sub>a + w\<^sub>b

goal (1 subgoal):
 1. splitLeaf (huffman []) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F [] w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
splitLeaf (huffman []) w\<^sub>a a w\<^sub>b b = huffman (splitLeaf\<^sub>F [] w\<^sub>a a w\<^sub>b b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma max_0_imp_0[simp]:
"(max x y = (0::nat)) = (x = 0 \<and> y = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (max x y = 0) = (x = 0 \<and> y = 0)
[PROOF STEP]
by auto


[STATEMENT]
theorem optimum_huffman:
"\<lbrakk>consistent\<^sub>F ts; height\<^sub>F ts = 0; sortedByWeight ts; ts \<noteq> []\<rbrakk> \<Longrightarrow>
 optimum (huffman ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent\<^sub>F ts; height\<^sub>F ts = 0; sortedByWeight ts; ts \<noteq> []\<rbrakk> \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
txt \<open>
The input @{term ts} is assumed to be a nonempty consistent list of leaf nodes
sorted by weight. The proof is by induction on the length of the forest
@{term ts}. Let @{term ts} be
$$\vcenter{\hbox{\includegraphics[scale=1.25]{forest-flat.pdf}}}$$
with $w_a \le w_b \le w_c \le w_d \le \cdots \le w_z$. If @{term ts} consists
of a single leaf node, the node has cost 0 and is therefore optimum. If
@{term ts} has length 2 or more, the first step of the algorithm leaves us with
the term
$${\it huffman\/}\enskip\; \vcenter{\hbox{\includegraphics[scale=1.25]%
    {forest-uniteTrees.pdf}}}$$
In the diagram, we put the newly created tree at position 2 in the forest; in
general, it could be anywhere. By @{thm [source] splitLeaf_huffman_commute},
the above tree equals\strut
$${\it splitLeaf\/}\;\left({\it huffman\/}\enskip\;
  \vcenter{\hbox{\includegraphics[scale=1.25]{forest-uniteTrees-flat.pdf}}}
  \;\right)\,\<open>w\<^sub>a a w\<^sub>b b\<close>.$$
To prove that this tree is optimum, it suffices by
@{thm [source] optimum_splitLeaf} to show that\strut
$${\it huffman\/}\enskip\;
  \vcenter{\hbox{\includegraphics[scale=1.25]{forest-uniteTrees-flat.pdf}}}$$
is optimum, which follows from the induction hypothesis.\strut
\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>consistent\<^sub>F ts; height\<^sub>F ts = 0; sortedByWeight ts; ts \<noteq> []\<rbrakk> \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
proof (induct ts rule: length_induct)
  \<comment> \<open>\sc Complete induction step\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> consistent\<^sub>F ys \<longrightarrow> height\<^sub>F ys = 0 \<longrightarrow> sortedByWeight ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> optimum (huffman ys); consistent\<^sub>F xs; height\<^sub>F xs = 0; sortedByWeight xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> optimum (huffman xs)
[PROOF STEP]
case (1 ts)
[PROOF STATE]
proof (state)
this:
\<forall>ys. length ys < length ts \<longrightarrow> consistent\<^sub>F ys \<longrightarrow> height\<^sub>F ys = 0 \<longrightarrow> sortedByWeight ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> optimum (huffman ys)
consistent\<^sub>F ts
height\<^sub>F ts = 0
sortedByWeight ts
ts \<noteq> []

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> consistent\<^sub>F ys \<longrightarrow> height\<^sub>F ys = 0 \<longrightarrow> sortedByWeight ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> optimum (huffman ys); consistent\<^sub>F xs; height\<^sub>F xs = 0; sortedByWeight xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> optimum (huffman xs)
[PROOF STEP]
note hyps = 1
[PROOF STATE]
proof (state)
this:
\<forall>ys. length ys < length ts \<longrightarrow> consistent\<^sub>F ys \<longrightarrow> height\<^sub>F ys = 0 \<longrightarrow> sortedByWeight ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> optimum (huffman ys)
consistent\<^sub>F ts
height\<^sub>F ts = 0
sortedByWeight ts
ts \<noteq> []

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> consistent\<^sub>F ys \<longrightarrow> height\<^sub>F ys = 0 \<longrightarrow> sortedByWeight ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> optimum (huffman ys); consistent\<^sub>F xs; height\<^sub>F xs = 0; sortedByWeight xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> optimum (huffman xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
proof (cases ts)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ts = [] \<Longrightarrow> optimum (huffman ts)
 2. \<And>a list. ts = a # list \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
ts = []

goal (2 subgoals):
 1. ts = [] \<Longrightarrow> optimum (huffman ts)
 2. \<And>a list. ts = a # list \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ts = []

goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
using \<open>ts \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
ts = []
ts \<noteq> []

goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
optimum (huffman ts)

goal (1 subgoal):
 1. \<And>a list. ts = a # list \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. ts = a # list \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
case (Cons t\<^sub>a ts')
[PROOF STATE]
proof (state)
this:
ts = t\<^sub>a # ts'

goal (1 subgoal):
 1. \<And>a list. ts = a # list \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
note ts = Cons
[PROOF STATE]
proof (state)
this:
ts = t\<^sub>a # ts'

goal (1 subgoal):
 1. \<And>a list. ts = a # list \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
proof (cases ts')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ts' = [] \<Longrightarrow> optimum (huffman ts)
 2. \<And>a list. ts' = a # list \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
ts' = []

goal (2 subgoals):
 1. ts' = [] \<Longrightarrow> optimum (huffman ts)
 2. \<And>a list. ts' = a # list \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ts' = []

goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
using ts hyps
[PROOF STATE]
proof (prove)
using this:
ts' = []
ts = t\<^sub>a # ts'
\<forall>ys. length ys < length ts \<longrightarrow> consistent\<^sub>F ys \<longrightarrow> height\<^sub>F ys = 0 \<longrightarrow> sortedByWeight ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> optimum (huffman ys)
consistent\<^sub>F ts
height\<^sub>F ts = 0
sortedByWeight ts
ts \<noteq> []

goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
by (simp add: optimum_def)
[PROOF STATE]
proof (state)
this:
optimum (huffman ts)

goal (1 subgoal):
 1. \<And>a list. ts' = a # list \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. ts' = a # list \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
case (Cons t\<^sub>b ts'')
[PROOF STATE]
proof (state)
this:
ts' = t\<^sub>b # ts''

goal (1 subgoal):
 1. \<And>a list. ts' = a # list \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
note ts' = Cons
[PROOF STATE]
proof (state)
this:
ts' = t\<^sub>b # ts''

goal (1 subgoal):
 1. \<And>a list. ts' = a # list \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
proof (cases t\<^sub>a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x11 x12. t\<^sub>a = Leaf x11 x12 \<Longrightarrow> optimum (huffman ts)
 2. \<And>x21 x22 x23. t\<^sub>a = Node x21 x22 x23 \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
case (Leaf w\<^sub>a a)
[PROOF STATE]
proof (state)
this:
t\<^sub>a = Leaf w\<^sub>a a

goal (2 subgoals):
 1. \<And>x11 x12. t\<^sub>a = Leaf x11 x12 \<Longrightarrow> optimum (huffman ts)
 2. \<And>x21 x22 x23. t\<^sub>a = Node x21 x22 x23 \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
note l\<^sub>a = Leaf
[PROOF STATE]
proof (state)
this:
t\<^sub>a = Leaf w\<^sub>a a

goal (2 subgoals):
 1. \<And>x11 x12. t\<^sub>a = Leaf x11 x12 \<Longrightarrow> optimum (huffman ts)
 2. \<And>x21 x22 x23. t\<^sub>a = Node x21 x22 x23 \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
proof (cases t\<^sub>b)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x11 x12. t\<^sub>b = Leaf x11 x12 \<Longrightarrow> optimum (huffman ts)
 2. \<And>x21 x22 x23. t\<^sub>b = Node x21 x22 x23 \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
case (Leaf w\<^sub>b b)
[PROOF STATE]
proof (state)
this:
t\<^sub>b = Leaf w\<^sub>b b

goal (2 subgoals):
 1. \<And>x11 x12. t\<^sub>b = Leaf x11 x12 \<Longrightarrow> optimum (huffman ts)
 2. \<And>x21 x22 x23. t\<^sub>b = Node x21 x22 x23 \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
note l\<^sub>b = Leaf
[PROOF STATE]
proof (state)
this:
t\<^sub>b = Leaf w\<^sub>b b

goal (2 subgoals):
 1. \<And>x11 x12. t\<^sub>b = Leaf x11 x12 \<Longrightarrow> optimum (huffman ts)
 2. \<And>x21 x22 x23. t\<^sub>b = Node x21 x22 x23 \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
let ?us = "insortTree (uniteTrees t\<^sub>a t\<^sub>b) ts''"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
let ?us' = "insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts''"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
let ?t\<^sub>s = "splitLeaf (huffman ?us') w\<^sub>a a w\<^sub>b b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
have e\<^sub>1: "huffman ts = huffman ?us"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. huffman ts = huffman (insortTree (uniteTrees t\<^sub>a t\<^sub>b) ts'')
[PROOF STEP]
using ts' ts
[PROOF STATE]
proof (prove)
using this:
ts' = t\<^sub>b # ts''
ts = t\<^sub>a # ts'

goal (1 subgoal):
 1. huffman ts = huffman (insortTree (uniteTrees t\<^sub>a t\<^sub>b) ts'')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
huffman ts = huffman (insortTree (uniteTrees t\<^sub>a t\<^sub>b) ts'')

goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
have e\<^sub>2: "huffman ?us = ?t\<^sub>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. huffman (insortTree (uniteTrees t\<^sub>a t\<^sub>b) ts'') = splitLeaf (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')) w\<^sub>a a w\<^sub>b b
[PROOF STEP]
using l\<^sub>a l\<^sub>b ts' ts hyps
[PROOF STATE]
proof (prove)
using this:
t\<^sub>a = Leaf w\<^sub>a a
t\<^sub>b = Leaf w\<^sub>b b
ts' = t\<^sub>b # ts''
ts = t\<^sub>a # ts'
\<forall>ys. length ys < length ts \<longrightarrow> consistent\<^sub>F ys \<longrightarrow> height\<^sub>F ys = 0 \<longrightarrow> sortedByWeight ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> optimum (huffman ys)
consistent\<^sub>F ts
height\<^sub>F ts = 0
sortedByWeight ts
ts \<noteq> []

goal (1 subgoal):
 1. huffman (insortTree (uniteTrees t\<^sub>a t\<^sub>b) ts'') = splitLeaf (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')) w\<^sub>a a w\<^sub>b b
[PROOF STEP]
by (auto simp: splitLeaf_huffman_commute uniteTrees_def)
[PROOF STATE]
proof (state)
this:
huffman (insortTree (uniteTrees t\<^sub>a t\<^sub>b) ts'') = splitLeaf (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')) w\<^sub>a a w\<^sub>b b

goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
have "optimum (huffman ?us')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. optimum (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts''))
[PROOF STEP]
using l\<^sub>a ts' ts hyps
[PROOF STATE]
proof (prove)
using this:
t\<^sub>a = Leaf w\<^sub>a a
ts' = t\<^sub>b # ts''
ts = t\<^sub>a # ts'
\<forall>ys. length ys < length ts \<longrightarrow> consistent\<^sub>F ys \<longrightarrow> height\<^sub>F ys = 0 \<longrightarrow> sortedByWeight ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> optimum (huffman ys)
consistent\<^sub>F ts
height\<^sub>F ts = 0
sortedByWeight ts
ts \<noteq> []

goal (1 subgoal):
 1. optimum (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts''))
[PROOF STEP]
by (drule_tac x = ?us' in spec)
                 (auto dest: sortedByWeight_Cons_imp_sortedByWeight
                  simp: sortedByWeight_insortTree)
[PROOF STATE]
proof (state)
this:
optimum (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts''))

goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
hence "optimum ?t\<^sub>s"
[PROOF STATE]
proof (prove)
using this:
optimum (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts''))

goal (1 subgoal):
 1. optimum (splitLeaf (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
using l\<^sub>a l\<^sub>b ts' ts hyps
[PROOF STATE]
proof (prove)
using this:
optimum (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts''))
t\<^sub>a = Leaf w\<^sub>a a
t\<^sub>b = Leaf w\<^sub>b b
ts' = t\<^sub>b # ts''
ts = t\<^sub>a # ts'
\<forall>ys. length ys < length ts \<longrightarrow> consistent\<^sub>F ys \<longrightarrow> height\<^sub>F ys = 0 \<longrightarrow> sortedByWeight ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> optimum (huffman ys)
consistent\<^sub>F ts
height\<^sub>F ts = 0
sortedByWeight ts
ts \<noteq> []

goal (1 subgoal):
 1. optimum (splitLeaf (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>optimum (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')); t\<^sub>a = Leaf w\<^sub>a a; t\<^sub>b = Leaf w\<^sub>b b; ts' = Leaf w\<^sub>b b # ts''; ts = Leaf w\<^sub>a a # Leaf w\<^sub>b b # ts''; \<forall>ys. length ys < Suc (Suc (length ts'')) \<longrightarrow> consistent\<^sub>F ys \<longrightarrow> height\<^sub>F ys = 0 \<longrightarrow> sortedByWeight ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> optimum (huffman ys); b \<noteq> a \<and> a \<notin> alphabet\<^sub>F ts'' \<and> b \<notin> alphabet\<^sub>F ts'' \<and> consistent\<^sub>F ts''; height\<^sub>F ts'' = 0; w\<^sub>a \<le> w\<^sub>b \<and> sortedByWeight (Leaf w\<^sub>b b # ts'')\<rbrakk> \<Longrightarrow> optimum (splitLeaf (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')) w\<^sub>a a w\<^sub>b b)
[PROOF STEP]
apply (rule optimum_splitLeaf)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>optimum (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')); t\<^sub>a = Leaf w\<^sub>a a; t\<^sub>b = Leaf w\<^sub>b b; ts' = Leaf w\<^sub>b b # ts''; ts = Leaf w\<^sub>a a # Leaf w\<^sub>b b # ts''; \<forall>ys. length ys < Suc (Suc (length ts'')) \<longrightarrow> consistent\<^sub>F ys \<longrightarrow> height\<^sub>F ys = 0 \<longrightarrow> sortedByWeight ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> optimum (huffman ys); b \<noteq> a \<and> a \<notin> alphabet\<^sub>F ts'' \<and> b \<notin> alphabet\<^sub>F ts'' \<and> consistent\<^sub>F ts''; height\<^sub>F ts'' = 0; w\<^sub>a \<le> w\<^sub>b \<and> sortedByWeight (Leaf w\<^sub>b b # ts'')\<rbrakk> \<Longrightarrow> consistent (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts''))
 2. \<lbrakk>optimum (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')); t\<^sub>a = Leaf w\<^sub>a a; t\<^sub>b = Leaf w\<^sub>b b; ts' = Leaf w\<^sub>b b # ts''; ts = Leaf w\<^sub>a a # Leaf w\<^sub>b b # ts''; \<forall>ys. length ys < Suc (Suc (length ts'')) \<longrightarrow> consistent\<^sub>F ys \<longrightarrow> height\<^sub>F ys = 0 \<longrightarrow> sortedByWeight ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> optimum (huffman ys); b \<noteq> a \<and> a \<notin> alphabet\<^sub>F ts'' \<and> b \<notin> alphabet\<^sub>F ts'' \<and> consistent\<^sub>F ts''; height\<^sub>F ts'' = 0; w\<^sub>a \<le> w\<^sub>b \<and> sortedByWeight (Leaf w\<^sub>b b # ts'')\<rbrakk> \<Longrightarrow> optimum (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts''))
 3. \<lbrakk>optimum (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')); t\<^sub>a = Leaf w\<^sub>a a; t\<^sub>b = Leaf w\<^sub>b b; ts' = Leaf w\<^sub>b b # ts''; ts = Leaf w\<^sub>a a # Leaf w\<^sub>b b # ts''; \<forall>ys. length ys < Suc (Suc (length ts'')) \<longrightarrow> consistent\<^sub>F ys \<longrightarrow> height\<^sub>F ys = 0 \<longrightarrow> sortedByWeight ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> optimum (huffman ys); b \<noteq> a \<and> a \<notin> alphabet\<^sub>F ts'' \<and> b \<notin> alphabet\<^sub>F ts'' \<and> consistent\<^sub>F ts''; height\<^sub>F ts'' = 0; w\<^sub>a \<le> w\<^sub>b \<and> sortedByWeight (Leaf w\<^sub>b b # ts'')\<rbrakk> \<Longrightarrow> a \<in> alphabet (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts''))
 4. \<lbrakk>optimum (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')); t\<^sub>a = Leaf w\<^sub>a a; t\<^sub>b = Leaf w\<^sub>b b; ts' = Leaf w\<^sub>b b # ts''; ts = Leaf w\<^sub>a a # Leaf w\<^sub>b b # ts''; \<forall>ys. length ys < Suc (Suc (length ts'')) \<longrightarrow> consistent\<^sub>F ys \<longrightarrow> height\<^sub>F ys = 0 \<longrightarrow> sortedByWeight ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> optimum (huffman ys); b \<noteq> a \<and> a \<notin> alphabet\<^sub>F ts'' \<and> b \<notin> alphabet\<^sub>F ts'' \<and> consistent\<^sub>F ts''; height\<^sub>F ts'' = 0; w\<^sub>a \<le> w\<^sub>b \<and> sortedByWeight (Leaf w\<^sub>b b # ts'')\<rbrakk> \<Longrightarrow> b \<notin> alphabet (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts''))
 5. \<lbrakk>optimum (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')); t\<^sub>a = Leaf w\<^sub>a a; t\<^sub>b = Leaf w\<^sub>b b; ts' = Leaf w\<^sub>b b # ts''; ts = Leaf w\<^sub>a a # Leaf w\<^sub>b b # ts''; \<forall>ys. length ys < Suc (Suc (length ts'')) \<longrightarrow> consistent\<^sub>F ys \<longrightarrow> height\<^sub>F ys = 0 \<longrightarrow> sortedByWeight ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> optimum (huffman ys); b \<noteq> a \<and> a \<notin> alphabet\<^sub>F ts'' \<and> b \<notin> alphabet\<^sub>F ts'' \<and> consistent\<^sub>F ts''; height\<^sub>F ts'' = 0; w\<^sub>a \<le> w\<^sub>b \<and> sortedByWeight (Leaf w\<^sub>b b # ts'')\<rbrakk> \<Longrightarrow> freq (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')) a = w\<^sub>a + w\<^sub>b
 6. \<lbrakk>optimum (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')); t\<^sub>a = Leaf w\<^sub>a a; t\<^sub>b = Leaf w\<^sub>b b; ts' = Leaf w\<^sub>b b # ts''; ts = Leaf w\<^sub>a a # Leaf w\<^sub>b b # ts''; \<forall>ys. length ys < Suc (Suc (length ts'')) \<longrightarrow> consistent\<^sub>F ys \<longrightarrow> height\<^sub>F ys = 0 \<longrightarrow> sortedByWeight ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> optimum (huffman ys); b \<noteq> a \<and> a \<notin> alphabet\<^sub>F ts'' \<and> b \<notin> alphabet\<^sub>F ts'' \<and> consistent\<^sub>F ts''; height\<^sub>F ts'' = 0; w\<^sub>a \<le> w\<^sub>b \<and> sortedByWeight (Leaf w\<^sub>b b # ts'')\<rbrakk> \<Longrightarrow> \<forall>c\<in>alphabet (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')). w\<^sub>a \<le> freq (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')) c \<and> w\<^sub>b \<le> freq (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')) c
[PROOF STEP]
by (auto dest!: height\<^sub>F_0_imp_Leaf_freq\<^sub>F_in_set
                  sortedByWeight_Cons_imp_forall_weight_ge)
[PROOF STATE]
proof (state)
this:
optimum (splitLeaf (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')) w\<^sub>a a w\<^sub>b b)

goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
thus "optimum (huffman ts)"
[PROOF STATE]
proof (prove)
using this:
optimum (splitLeaf (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')) w\<^sub>a a w\<^sub>b b)

goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
using e\<^sub>1 e\<^sub>2
[PROOF STATE]
proof (prove)
using this:
optimum (splitLeaf (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')) w\<^sub>a a w\<^sub>b b)
huffman ts = huffman (insortTree (uniteTrees t\<^sub>a t\<^sub>b) ts'')
huffman (insortTree (uniteTrees t\<^sub>a t\<^sub>b) ts'') = splitLeaf (huffman (insortTree (Leaf (w\<^sub>a + w\<^sub>b) a) ts'')) w\<^sub>a a w\<^sub>b b

goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
optimum (huffman ts)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
optimum (huffman ts)

goal (1 subgoal):
 1. \<And>x21 x22 x23. t\<^sub>b = Node x21 x22 x23 \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22 x23. t\<^sub>b = Node x21 x22 x23 \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
case Node
[PROOF STATE]
proof (state)
this:
t\<^sub>b = Node x21_ x22_ x23_

goal (1 subgoal):
 1. \<And>x21 x22 x23. t\<^sub>b = Node x21 x22 x23 \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
t\<^sub>b = Node x21_ x22_ x23_

goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
using ts' ts hyps
[PROOF STATE]
proof (prove)
using this:
t\<^sub>b = Node x21_ x22_ x23_
ts' = t\<^sub>b # ts''
ts = t\<^sub>a # ts'
\<forall>ys. length ys < length ts \<longrightarrow> consistent\<^sub>F ys \<longrightarrow> height\<^sub>F ys = 0 \<longrightarrow> sortedByWeight ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> optimum (huffman ys)
consistent\<^sub>F ts
height\<^sub>F ts = 0
sortedByWeight ts
ts \<noteq> []

goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
optimum (huffman ts)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
optimum (huffman ts)

goal (1 subgoal):
 1. \<And>x21 x22 x23. t\<^sub>a = Node x21 x22 x23 \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22 x23. t\<^sub>a = Node x21 x22 x23 \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
case Node
[PROOF STATE]
proof (state)
this:
t\<^sub>a = Node x21_ x22_ x23_

goal (1 subgoal):
 1. \<And>x21 x22 x23. t\<^sub>a = Node x21 x22 x23 \<Longrightarrow> optimum (huffman ts)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
t\<^sub>a = Node x21_ x22_ x23_

goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
using ts' ts hyps
[PROOF STATE]
proof (prove)
using this:
t\<^sub>a = Node x21_ x22_ x23_
ts' = t\<^sub>b # ts''
ts = t\<^sub>a # ts'
\<forall>ys. length ys < length ts \<longrightarrow> consistent\<^sub>F ys \<longrightarrow> height\<^sub>F ys = 0 \<longrightarrow> sortedByWeight ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> optimum (huffman ys)
consistent\<^sub>F ts
height\<^sub>F ts = 0
sortedByWeight ts
ts \<noteq> []

goal (1 subgoal):
 1. optimum (huffman ts)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
optimum (huffman ts)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
optimum (huffman ts)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
optimum (huffman ts)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
optimum (huffman ts)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_ks [simp]:
   "(x \<noteq> kno) = (x = unk)"
   "(x \<noteq> unk) = (x = kno)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<noteq> kno) = (x = unk) &&& (x \<noteq> unk) = (x = kno)
[PROOF STEP]
by (cases x, clarsimp+)+


[STATEMENT]
lemma not_ps [simp]:
  "(x \<noteq> noreq) = (x = req)"
  "(x \<noteq> req) = (x = noreq)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<noteq> noreq) = (x = req) &&& (x \<noteq> req) = (x = noreq)
[PROOF STEP]
by (cases x, clarsimp+)+


[STATEMENT]
lemma not_ffs [simp]:
  "(x \<noteq> val) = (x = inv)"
  "(x \<noteq> inv) = (x = val)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<noteq> val) = (x = Aodv_Basic.inv) &&& (x \<noteq> Aodv_Basic.inv) = (x = val)
[PROOF STEP]
by (cases x, clarsimp+)+


[STATEMENT]
lemma vp_snocI:
  "\<lbrakk>n -as\<rightarrow>\<^sub>\<surd>* n'; n' -[a]\<rightarrow>* n''; \<forall>Q p ret fs. kind a \<noteq> Q\<hookleftarrow>\<^bsub>p\<^esub>ret \<rbrakk> \<Longrightarrow> n -as @ [a]\<rightarrow>\<^sub>\<surd>* n''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n -as\<rightarrow>\<^sub>\<surd>* n'; n' -[a]\<rightarrow>* n''; \<forall>Q p ret fs. kind a \<noteq> Q\<hookleftarrow>\<^bsub>p\<^esub>ret\<rbrakk> \<Longrightarrow> n -as @ [a]\<rightarrow>\<^sub>\<surd>* n''
[PROOF STEP]
by (cases "kind a") (auto intro: path_Append valid_path_aux_Append simp: vp_def valid_path_def)


[STATEMENT]
lemma valid_node_cases' [case_names Source Target, consumes 1]:
  "\<lbrakk> valid_node n; \<And>e. \<lbrakk> valid_edge e; sourcenode e = n \<rbrakk> \<Longrightarrow> thesis;
  \<And>e. \<lbrakk> valid_edge e; targetnode e = n \<rbrakk> \<Longrightarrow> thesis \<rbrakk>
  \<Longrightarrow> thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_node n; \<And>e. \<lbrakk>valid_edge e; sourcenode e = n\<rbrakk> \<Longrightarrow> thesis; \<And>e. \<lbrakk>valid_edge e; targetnode e = n\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: valid_node_def)


[STATEMENT]
lemma disjE_strong: "\<lbrakk>P \<or> Q; P \<Longrightarrow> R; \<lbrakk>Q; \<not> P\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<or> Q; P \<Longrightarrow> R; \<lbrakk>Q; \<not> P\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
[PROOF STEP]
by auto


[STATEMENT]
lemma distinct_classes'':
  "''C'' \<noteq> Object"
  "''C'' \<noteq> NullPointer"
  "''C'' \<noteq> OutOfMemory"
  "''C'' \<noteq> ClassCast"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (''C'' \<noteq> Object &&& ''C'' \<noteq> NullPointer) &&& ''C'' \<noteq> OutOfMemory &&& ''C'' \<noteq> ClassCast
[PROOF STEP]
by (simp_all add: Object_def NullPointer_def OutOfMemory_def ClassCast_def)


[STATEMENT]
lemma i_max_2D: "i < Suc (Suc 0) \<Longrightarrow> i = 0 \<or> i = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < Suc (Suc 0) \<Longrightarrow> i = 0 \<or> i = 1
[PROOF STEP]
by auto


[STATEMENT]
lemma EP_wf: "wf_jvm_prog\<^bsub>Phi_EP\<^esub> EP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_jvm_prog\<^bsub>Phi_EP\<^esub> EP
[PROOF STEP]
unfolding wf_jvm_prog_phi_def wf_prog_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_syscls EP \<and> (\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c) \<and> Auxiliary.distinct_fst EP
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. wf_syscls EP
 2. (\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c) \<and> Auxiliary.distinct_fst EP
[PROOF STEP]
show "wf_syscls EP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_syscls EP
[PROOF STEP]
by (simp add: EP_def wf_syscls_def SystemClasses_def sys_xcpts_def
      ObjectC_def NullPointerC_def OutOfMemoryC_def ClassCastC_def)
[PROOF STATE]
proof (state)
this:
wf_syscls EP

goal (1 subgoal):
 1. (\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c) \<and> Auxiliary.distinct_fst EP
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c) \<and> Auxiliary.distinct_fst EP
[PROOF STEP]
have distinct_EP: "distinct_fst EP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Auxiliary.distinct_fst EP
[PROOF STEP]
by (auto simp: EP_def SystemClasses_def ObjectC_def NullPointerC_def OutOfMemoryC_def
      ClassCastC_def)
[PROOF STATE]
proof (state)
this:
Auxiliary.distinct_fst EP

goal (1 subgoal):
 1. (\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c) \<and> Auxiliary.distinct_fst EP
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Auxiliary.distinct_fst EP

goal (1 subgoal):
 1. (\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c) \<and> Auxiliary.distinct_fst EP
[PROOF STEP]
have classes_wf:
    "\<forall>c\<in>set EP. wf_cdecl
    (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. c \<in> set EP \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c
[PROOF STEP]
fix C
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. c \<in> set EP \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c
[PROOF STEP]
assume C_in_EP: "C \<in> set EP"
[PROOF STATE]
proof (state)
this:
C \<in> set EP

goal (1 subgoal):
 1. \<And>c. c \<in> set EP \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c
[PROOF STEP]
show "wf_cdecl
      (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
[PROOF STEP]
proof (cases "C \<in> set SystemClasses")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. C \<in> set SystemClasses \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
 2. C \<notin> set SystemClasses \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
C \<in> set SystemClasses

goal (2 subgoals):
 1. C \<in> set SystemClasses \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
 2. C \<notin> set SystemClasses \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
C \<in> set SystemClasses

goal (1 subgoal):
 1. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
[PROOF STEP]
by (auto simp: wf_cdecl_def SystemClasses_def ObjectC_def NullPointerC_def
          OutOfMemoryC_def ClassCastC_def EP_def class_def)
[PROOF STATE]
proof (state)
this:
wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C

goal (1 subgoal):
 1. C \<notin> set SystemClasses \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C \<notin> set SystemClasses \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
C \<notin> set SystemClasses

goal (1 subgoal):
 1. C \<notin> set SystemClasses \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
[PROOF STEP]
with C_in_EP
[PROOF STATE]
proof (chain)
picking this:
C \<in> set EP
C \<notin> set SystemClasses
[PROOF STEP]
have "C = (''C'', the (class EP ''C''))"
[PROOF STATE]
proof (prove)
using this:
C \<in> set EP
C \<notin> set SystemClasses

goal (1 subgoal):
 1. C = (''C'', the (class EP ''C''))
[PROOF STEP]
by (auto simp: EP_def SystemClasses_def class_def)
[PROOF STATE]
proof (state)
this:
C = (''C'', the (class EP ''C''))

goal (1 subgoal):
 1. C \<notin> set SystemClasses \<Longrightarrow> wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
C = (''C'', the (class EP ''C''))

goal (1 subgoal):
 1. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C
[PROOF STEP]
by (auto dest!: i_max_2D elim: Methods.cases
          simp: wf_cdecl_def class_def EP_def wf_mdecl_def wt_method_def Phi_EP_def
          wt_start_def check_types_def states_def JVM_SemiType.sl_def SystemClasses_def
          stk_esl_def upto_esl_def loc_sl_def SemiType.esl_def ObjectC_def
          SemiType.sup_def Err.sl_def Err.le_def err_def Listn.sl_def Method_def
          Err.esl_def Opt.esl_def Product.esl_def relevant_entries_def)
[PROOF STATE]
proof (state)
this:
wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c

goal (1 subgoal):
 1. (\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c) \<and> Auxiliary.distinct_fst EP
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Auxiliary.distinct_fst EP
\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c
[PROOF STEP]
show "(\<forall>c\<in>set EP. wf_cdecl
    (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c) \<and>
    distinct_fst EP"
[PROOF STATE]
proof (prove)
using this:
Auxiliary.distinct_fst EP
\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c

goal (1 subgoal):
 1. (\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c) \<and> Auxiliary.distinct_fst EP
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>c\<in>set EP. wf_cdecl (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (Phi_EP C M)) EP c) \<and> Auxiliary.distinct_fst EP

goal:
No subgoals!
[PROOF STEP]
qed