[STATEMENT]
lemma list_comb_cond_inj:
  assumes "list_comb f xs = list_comb g ys" "left_nesting f = left_nesting g"
  shows "xs = ys" "f = g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = ys &&& f = g
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
list_comb f xs = list_comb g ys
left_nesting f = left_nesting g

goal (1 subgoal):
 1. xs = ys &&& f = g
[PROOF STEP]
proof (induction xs arbitrary: f g ys)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>f g ys. \<lbrakk>list_comb f [] = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> [] = ys
 2. \<And>f g ys. \<lbrakk>list_comb f [] = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
 3. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> a # xs = ys
 4. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. \<And>f g ys. \<lbrakk>list_comb f [] = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> [] = ys
 2. \<And>f g ys. \<lbrakk>list_comb f [] = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
 3. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> a # xs = ys
 4. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
[PROOF STEP]
fix f g :: 'a
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>f g ys. \<lbrakk>list_comb f [] = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> [] = ys
 2. \<And>f g ys. \<lbrakk>list_comb f [] = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
 3. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> a # xs = ys
 4. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
[PROOF STEP]
fix ys
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>f g ys. \<lbrakk>list_comb f [] = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> [] = ys
 2. \<And>f g ys. \<lbrakk>list_comb f [] = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
 3. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> a # xs = ys
 4. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
[PROOF STEP]
assume prems: "list_comb f [] = list_comb g ys" "left_nesting f = left_nesting g"
[PROOF STATE]
proof (state)
this:
list_comb f [] = list_comb g ys
left_nesting f = left_nesting g

goal (4 subgoals):
 1. \<And>f g ys. \<lbrakk>list_comb f [] = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> [] = ys
 2. \<And>f g ys. \<lbrakk>list_comb f [] = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
 3. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> a # xs = ys
 4. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
[PROOF STEP]
hence "left_nesting f = left_nesting g + length ys"
[PROOF STATE]
proof (prove)
using this:
list_comb f [] = list_comb g ys
left_nesting f = left_nesting g

goal (1 subgoal):
 1. left_nesting f = left_nesting g + length ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
left_nesting f = left_nesting g + length ys

goal (4 subgoals):
 1. \<And>f g ys. \<lbrakk>list_comb f [] = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> [] = ys
 2. \<And>f g ys. \<lbrakk>list_comb f [] = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
 3. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> a # xs = ys
 4. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
list_comb f [] = list_comb g ys
left_nesting f = left_nesting g
left_nesting f = left_nesting g + length ys
[PROOF STEP]
show "[] = ys" "f = g"
[PROOF STATE]
proof (prove)
using this:
list_comb f [] = list_comb g ys
left_nesting f = left_nesting g
left_nesting f = left_nesting g + length ys

goal (1 subgoal):
 1. [] = ys &&& f = g
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
[] = ys
f = g

goal (2 subgoals):
 1. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> a # xs = ys
 2. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> a # xs = ys
 2. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>list_comb ?f xs = list_comb ?g ?ys; left_nesting ?f = left_nesting ?g\<rbrakk> \<Longrightarrow> xs = ?ys
\<lbrakk>list_comb ?f xs = list_comb ?g ?ys; left_nesting ?f = left_nesting ?g\<rbrakk> \<Longrightarrow> ?f = ?g

goal (2 subgoals):
 1. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> a # xs = ys
 2. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
[PROOF STEP]
fix f g ys
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> a # xs = ys
 2. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
[PROOF STEP]
assume prems: "list_comb f (x # xs) = list_comb g ys" "left_nesting f = left_nesting g"
[PROOF STATE]
proof (state)
this:
list_comb f (x # xs) = list_comb g ys
left_nesting f = left_nesting g

goal (2 subgoals):
 1. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> a # xs = ys
 2. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
[PROOF STEP]
hence "left_nesting (list_comb f (x # xs)) = left_nesting (list_comb g ys)"
[PROOF STATE]
proof (prove)
using this:
list_comb f (x # xs) = list_comb g ys
left_nesting f = left_nesting g

goal (1 subgoal):
 1. left_nesting (list_comb f (x # xs)) = left_nesting (list_comb g ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
left_nesting (list_comb f (x # xs)) = left_nesting (list_comb g ys)

goal (2 subgoals):
 1. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> a # xs = ys
 2. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
[PROOF STEP]
hence "Suc (left_nesting f + length xs) = left_nesting g + length ys"
[PROOF STATE]
proof (prove)
using this:
left_nesting (list_comb f (x # xs)) = left_nesting (list_comb g ys)

goal (1 subgoal):
 1. Suc (left_nesting f + length xs) = left_nesting g + length ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (left_nesting f + length xs) = left_nesting g + length ys

goal (2 subgoals):
 1. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> a # xs = ys
 2. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
list_comb f (x # xs) = list_comb g ys
left_nesting f = left_nesting g
Suc (left_nesting f + length xs) = left_nesting g + length ys
[PROOF STEP]
have "length ys = Suc (length xs)"
[PROOF STATE]
proof (prove)
using this:
list_comb f (x # xs) = list_comb g ys
left_nesting f = left_nesting g
Suc (left_nesting f + length xs) = left_nesting g + length ys

goal (1 subgoal):
 1. length ys = Suc (length xs)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
length ys = Suc (length xs)

goal (2 subgoals):
 1. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> a # xs = ys
 2. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length ys = Suc (length xs)
[PROOF STEP]
obtain z zs where "ys = z # zs"
[PROOF STATE]
proof (prove)
using this:
length ys = Suc (length xs)

goal (1 subgoal):
 1. (\<And>z zs. ys = z # zs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis length_Suc_conv)
[PROOF STATE]
proof (state)
this:
ys = z # zs

goal (2 subgoals):
 1. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> a # xs = ys
 2. \<And>a xs f g ys. \<lbrakk>\<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> xs = ys; \<And>f g ys. \<lbrakk>list_comb f xs = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g; list_comb f (a # xs) = list_comb g ys; left_nesting f = left_nesting g\<rbrakk> \<Longrightarrow> f = g
[PROOF STEP]
thus "x # xs = ys" "f = g"
[PROOF STATE]
proof (prove)
using this:
ys = z # zs

goal (1 subgoal):
 1. x # xs = ys &&& f = g
[PROOF STEP]
using prems Cons[where ys = zs and f = "app f x" and g = "app g z"]
[PROOF STATE]
proof (prove)
using this:
ys = z # zs
list_comb f (x # xs) = list_comb g ys
left_nesting f = left_nesting g
\<lbrakk>list_comb (app f x) xs = list_comb (app g z) zs; left_nesting (app f x) = left_nesting (app g z)\<rbrakk> \<Longrightarrow> xs = zs
\<lbrakk>list_comb (app f x) xs = list_comb (app g z) zs; left_nesting (app f x) = left_nesting (app g z)\<rbrakk> \<Longrightarrow> app f x = app g z

goal (1 subgoal):
 1. x # xs = ys &&& f = g
[PROOF STEP]
by (auto dest: app_inject)
[PROOF STATE]
proof (state)
this:
x # xs = ys
f = g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_comb_inj_second: "inj (list_comb f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (list_comb f)
[PROOF STEP]
by (metis injI list_comb_cond_inj)


[STATEMENT]
lemma list_comb_semi_inj:
  assumes "length xs = length ys"
  assumes "list_comb f xs = list_comb g ys"
  shows "xs = ys" "f = g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = ys &&& f = g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = ys
 2. f = g
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
length xs = length ys
list_comb f xs = list_comb g ys
[PROOF STEP]
have "left_nesting (list_comb f xs) = left_nesting (list_comb g ys)"
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
list_comb f xs = list_comb g ys

goal (1 subgoal):
 1. left_nesting (list_comb f xs) = left_nesting (list_comb g ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
left_nesting (list_comb f xs) = left_nesting (list_comb g ys)

goal (2 subgoals):
 1. xs = ys
 2. f = g
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
length xs = length ys
list_comb f xs = list_comb g ys
left_nesting (list_comb f xs) = left_nesting (list_comb g ys)
[PROOF STEP]
have "left_nesting f = left_nesting g"
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
list_comb f xs = list_comb g ys
left_nesting (list_comb f xs) = left_nesting (list_comb g ys)

goal (1 subgoal):
 1. left_nesting f = left_nesting g
[PROOF STEP]
unfolding list_comb_nesting
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
list_comb f xs = list_comb g ys
left_nesting f + length xs = left_nesting g + length ys

goal (1 subgoal):
 1. left_nesting f = left_nesting g
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
left_nesting f = left_nesting g

goal (2 subgoals):
 1. xs = ys
 2. f = g
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
length xs = length ys
list_comb f xs = list_comb g ys
left_nesting f = left_nesting g
[PROOF STEP]
show "xs = ys" "f = g"
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
list_comb f xs = list_comb g ys
left_nesting f = left_nesting g

goal (1 subgoal):
 1. xs = ys &&& f = g
[PROOF STEP]
by (metis list_comb_cond_inj)+
[PROOF STATE]
proof (state)
this:
xs = ys
f = g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma no_abs_induct[consumes 1, case_names free const app, induct pred: no_abs]:
  assumes "no_abs t"
  assumes "\<And>name. P (free name)"
  assumes "\<And>name. P (const name)"
  assumes "\<And>t\<^sub>1 t\<^sub>2. P t\<^sub>1 \<Longrightarrow> no_abs t\<^sub>1 \<Longrightarrow> P t\<^sub>2 \<Longrightarrow> no_abs t\<^sub>2 \<Longrightarrow> P (app t\<^sub>1 t\<^sub>2)"
  shows "P t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P t
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
no_abs t

goal (1 subgoal):
 1. P t
[PROOF STEP]
proof (induction rule: no_abs.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>\<And>u\<^sub>1 u\<^sub>2. \<lbrakk>t = app u\<^sub>1 u\<^sub>2; no_abs u\<^sub>1\<rbrakk> \<Longrightarrow> P u\<^sub>1; \<And>u\<^sub>1 u\<^sub>2. \<lbrakk>t = app u\<^sub>1 u\<^sub>2; no_abs u\<^sub>2\<rbrakk> \<Longrightarrow> P u\<^sub>2; no_abs t\<rbrakk> \<Longrightarrow> P t
[PROOF STEP]
case (1 t)
[PROOF STATE]
proof (state)
this:
\<lbrakk>t = app ?u\<^sub>1 ?u\<^sub>2; no_abs ?u\<^sub>1\<rbrakk> \<Longrightarrow> P ?u\<^sub>1
\<lbrakk>t = app ?u\<^sub>1 ?u\<^sub>2; no_abs ?u\<^sub>2\<rbrakk> \<Longrightarrow> P ?u\<^sub>2
no_abs t

goal (1 subgoal):
 1. \<And>t. \<lbrakk>\<And>u\<^sub>1 u\<^sub>2. \<lbrakk>t = app u\<^sub>1 u\<^sub>2; no_abs u\<^sub>1\<rbrakk> \<Longrightarrow> P u\<^sub>1; \<And>u\<^sub>1 u\<^sub>2. \<lbrakk>t = app u\<^sub>1 u\<^sub>2; no_abs u\<^sub>2\<rbrakk> \<Longrightarrow> P u\<^sub>2; no_abs t\<rbrakk> \<Longrightarrow> P t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P t
[PROOF STEP]
proof (cases rule: pre_term_class.term_cases[where t = t])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>name. t = free name \<Longrightarrow> P t
 2. \<And>name. t = const name \<Longrightarrow> P t
 3. \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> P t
 4. \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> P t
[PROOF STEP]
case (free name)
[PROOF STATE]
proof (state)
this:
t = free name

goal (4 subgoals):
 1. \<And>name. t = free name \<Longrightarrow> P t
 2. \<And>name. t = const name \<Longrightarrow> P t
 3. \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> P t
 4. \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> P t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t = free name
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t = free name

goal (1 subgoal):
 1. P t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t = free name
no_abs t
P (free ?name)
P (const ?name)
\<lbrakk>P ?t\<^sub>1; no_abs ?t\<^sub>1; P ?t\<^sub>2; no_abs ?t\<^sub>2\<rbrakk> \<Longrightarrow> P (app ?t\<^sub>1 ?t\<^sub>2)

goal (1 subgoal):
 1. P t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P t

goal (3 subgoals):
 1. \<And>name. t = const name \<Longrightarrow> P t
 2. \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> P t
 3. \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> P t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>name. t = const name \<Longrightarrow> P t
 2. \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> P t
 3. \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> P t
[PROOF STEP]
case (const name)
[PROOF STATE]
proof (state)
this:
t = const name

goal (3 subgoals):
 1. \<And>name. t = const name \<Longrightarrow> P t
 2. \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> P t
 3. \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> P t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t = const name
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t = const name

goal (1 subgoal):
 1. P t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t = const name
no_abs t
P (free ?name)
P (const ?name)
\<lbrakk>P ?t\<^sub>1; no_abs ?t\<^sub>1; P ?t\<^sub>2; no_abs ?t\<^sub>2\<rbrakk> \<Longrightarrow> P (app ?t\<^sub>1 ?t\<^sub>2)

goal (1 subgoal):
 1. P t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P t

goal (2 subgoals):
 1. \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> P t
 2. \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> P t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> P t
 2. \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> P t
[PROOF STEP]
case (app u\<^sub>1 u\<^sub>2)
[PROOF STATE]
proof (state)
this:
t = app u\<^sub>1 u\<^sub>2

goal (2 subgoals):
 1. \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> P t
 2. \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> P t
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
no_abs t
P (free ?name)
P (const ?name)
\<lbrakk>P ?t\<^sub>1; no_abs ?t\<^sub>1; P ?t\<^sub>2; no_abs ?t\<^sub>2\<rbrakk> \<Longrightarrow> P (app ?t\<^sub>1 ?t\<^sub>2)
t = app u\<^sub>1 u\<^sub>2
[PROOF STEP]
have "P u\<^sub>1" "P u\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
no_abs t
P (free ?name)
P (const ?name)
\<lbrakk>P ?t\<^sub>1; no_abs ?t\<^sub>1; P ?t\<^sub>2; no_abs ?t\<^sub>2\<rbrakk> \<Longrightarrow> P (app ?t\<^sub>1 ?t\<^sub>2)
t = app u\<^sub>1 u\<^sub>2

goal (1 subgoal):
 1. P u\<^sub>1 &&& P u\<^sub>2
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
no_abs t
P (free ?name)
P (const ?name)
\<lbrakk>P ?t\<^sub>1; no_abs ?t\<^sub>1; P ?t\<^sub>2; no_abs ?t\<^sub>2\<rbrakk> \<Longrightarrow> P (app ?t\<^sub>1 ?t\<^sub>2)
t = app u\<^sub>1 u\<^sub>2
\<lbrakk>t = app ?u\<^sub>1 ?u\<^sub>2; no_abs ?u\<^sub>1\<rbrakk> \<Longrightarrow> P ?u\<^sub>1
\<lbrakk>t = app ?u\<^sub>1 ?u\<^sub>2; no_abs ?u\<^sub>2\<rbrakk> \<Longrightarrow> P ?u\<^sub>2
no_abs t

goal (1 subgoal):
 1. P u\<^sub>1 &&& P u\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P u\<^sub>1
P u\<^sub>2

goal (2 subgoals):
 1. \<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> P t
 2. \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> P t
[PROOF STEP]
with assms \<open>no_abs t\<close>
[PROOF STATE]
proof (chain)
picking this:
no_abs t
P (free ?name)
P (const ?name)
\<lbrakk>P ?t\<^sub>1; no_abs ?t\<^sub>1; P ?t\<^sub>2; no_abs ?t\<^sub>2\<rbrakk> \<Longrightarrow> P (app ?t\<^sub>1 ?t\<^sub>2)
no_abs t
P u\<^sub>1
P u\<^sub>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
no_abs t
P (free ?name)
P (const ?name)
\<lbrakk>P ?t\<^sub>1; no_abs ?t\<^sub>1; P ?t\<^sub>2; no_abs ?t\<^sub>2\<rbrakk> \<Longrightarrow> P (app ?t\<^sub>1 ?t\<^sub>2)
no_abs t
P u\<^sub>1
P u\<^sub>2

goal (1 subgoal):
 1. P t
[PROOF STEP]
unfolding \<open>t = _\<close>
[PROOF STATE]
proof (prove)
using this:
no_abs t
P (free ?name)
P (const ?name)
\<lbrakk>P ?t\<^sub>1; no_abs ?t\<^sub>1; P ?t\<^sub>2; no_abs ?t\<^sub>2\<rbrakk> \<Longrightarrow> P (app ?t\<^sub>1 ?t\<^sub>2)
no_abs (app u\<^sub>1 u\<^sub>2)
P u\<^sub>1
P u\<^sub>2

goal (1 subgoal):
 1. P (app u\<^sub>1 u\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P t

goal (1 subgoal):
 1. \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> P t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> P t
[PROOF STEP]
case other
[PROOF STATE]
proof (state)
this:
unfree t = None
unapp t = None
unconst t = None

goal (1 subgoal):
 1. \<lbrakk>unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> P t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
unfree t = None
unapp t = None
unconst t = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
unfree t = None
unapp t = None
unconst t = None

goal (1 subgoal):
 1. P t
[PROOF STEP]
using \<open>no_abs t\<close>
[PROOF STATE]
proof (prove)
using this:
unfree t = None
unapp t = None
unconst t = None
no_abs t

goal (1 subgoal):
 1. P t
[PROOF STEP]
apply (subst (asm) no_abs.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unfree t = None; unapp t = None; unconst t = None; term_cases (\<lambda>_. True) (\<lambda>_. True) (\<lambda>t u. no_abs t \<and> no_abs u) False t\<rbrakk> \<Longrightarrow> P t
[PROOF STEP]
apply (subst (asm) term_cases_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unfree t = None; unapp t = None; unconst t = None; case unconst t of None \<Rightarrow> case unfree t of None \<Rightarrow> case unapp t of None \<Rightarrow> False | Some (t, u) \<Rightarrow> no_abs t \<and> no_abs u | Some name \<Rightarrow> True | Some name \<Rightarrow> True\<rbrakk> \<Longrightarrow> P t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma no_abs_cases[consumes 1, cases pred: no_abs]:
  assumes "no_abs t"
  obtains (free) name where "t = free name"
        | (const) name where "t = const name"
        | (app) t\<^sub>1 t\<^sub>2 where "t = app t\<^sub>1 t\<^sub>2" "no_abs t\<^sub>1" "no_abs t\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
proof (cases rule: pre_term_class.term_cases[where t = t])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>name. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; t = free name\<rbrakk> \<Longrightarrow> thesis
 2. \<And>name. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; t = const name\<rbrakk> \<Longrightarrow> thesis
 3. \<And>u\<^sub>1 u\<^sub>2. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; t = app u\<^sub>1 u\<^sub>2\<rbrakk> \<Longrightarrow> thesis
 4. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (app u\<^sub>1 u\<^sub>2)
[PROOF STATE]
proof (state)
this:
t = app u\<^sub>1 u\<^sub>2

goal (4 subgoals):
 1. \<And>name. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; t = free name\<rbrakk> \<Longrightarrow> thesis
 2. \<And>name. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; t = const name\<rbrakk> \<Longrightarrow> thesis
 3. \<And>u\<^sub>1 u\<^sub>2. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; t = app u\<^sub>1 u\<^sub>2\<rbrakk> \<Longrightarrow> thesis
 4. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
apply (rule that(3))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. t = app ?t\<^sub>1 ?t\<^sub>2
 2. no_abs ?t\<^sub>1
 3. no_abs ?t\<^sub>2
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. no_abs u\<^sub>1
 2. no_abs u\<^sub>2
[PROOF STEP]
using \<open>no_abs t\<close>
[PROOF STATE]
proof (prove)
using this:
no_abs t

goal (2 subgoals):
 1. no_abs u\<^sub>1
 2. no_abs u\<^sub>2
[PROOF STEP]
unfolding \<open>t = _\<close>
[PROOF STATE]
proof (prove)
using this:
no_abs (app u\<^sub>1 u\<^sub>2)

goal (2 subgoals):
 1. no_abs u\<^sub>1
 2. no_abs u\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
thesis

goal (3 subgoals):
 1. \<And>name. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; t = free name\<rbrakk> \<Longrightarrow> thesis
 2. \<And>name. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; t = const name\<rbrakk> \<Longrightarrow> thesis
 3. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>name. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; t = free name\<rbrakk> \<Longrightarrow> thesis
 2. \<And>name. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; t = const name\<rbrakk> \<Longrightarrow> thesis
 3. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case other
[PROOF STATE]
proof (state)
this:
unfree t = None
unapp t = None
unconst t = None

goal (3 subgoals):
 1. \<And>name. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; t = free name\<rbrakk> \<Longrightarrow> thesis
 2. \<And>name. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; t = const name\<rbrakk> \<Longrightarrow> thesis
 3. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
unfree t = None
unapp t = None
unconst t = None
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
unfree t = None
unapp t = None
unconst t = None

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>no_abs t\<close>
[PROOF STATE]
proof (prove)
using this:
unfree t = None
unapp t = None
unconst t = None
no_abs t

goal (1 subgoal):
 1. False
[PROOF STEP]
apply (subst (asm) no_abs.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unfree t = None; unapp t = None; unconst t = None; term_cases (\<lambda>_. True) (\<lambda>_. True) (\<lambda>t u. no_abs t \<and> no_abs u) False t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (auto simp: term_cases_def)
[PROOF STATE]
proof (state)
this:
False

goal (3 subgoals):
 1. \<And>name. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; t = free name\<rbrakk> \<Longrightarrow> thesis
 2. \<And>name. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; t = const name\<rbrakk> \<Longrightarrow> thesis
 3. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; unfree t = None; unapp t = None; unconst t = None\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
thesis

goal (2 subgoals):
 1. \<And>name. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; t = free name\<rbrakk> \<Longrightarrow> thesis
 2. \<And>name. \<lbrakk>\<And>name. t = free name \<Longrightarrow> thesis; \<And>name. t = const name \<Longrightarrow> thesis; \<And>t\<^sub>1 t\<^sub>2. \<lbrakk>t = app t\<^sub>1 t\<^sub>2; no_abs t\<^sub>1; no_abs t\<^sub>2\<rbrakk> \<Longrightarrow> thesis; t = const name\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
qed


[STATEMENT]
lemma list_comb: "P (list_comb f xs) \<longleftrightarrow> P f \<and> list_all P xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (list_comb f xs) = (P f \<and> list_all P xs)
[PROOF STEP]
by (induction xs arbitrary: f) auto


[STATEMENT]
lemma match:
  assumes "match pat t = Some env" "P t"
  shows "fmpred (\<lambda>_. P) env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmpred (\<lambda>_. P) env
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
match pat t = Some env
P t

goal (1 subgoal):
 1. fmpred (\<lambda>_. P) env
[PROOF STEP]
by (induction pat t env rule: match_some_induct) auto


[STATEMENT]
lemma matchs:
  assumes "matchs pats ts = Some env" "list_all P ts"
  shows "fmpred (\<lambda>_. P) env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmpred (\<lambda>_. P) env
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
matchs pats ts = Some env
list_all P ts

goal (1 subgoal):
 1. fmpred (\<lambda>_. P) env
[PROOF STEP]
by (induction pats ts arbitrary: env rule: matchs.induct) (auto elim!: option_bindE intro: match)


[STATEMENT]
lemma rewrite_step:
  assumes "(lhs, rhs) \<turnstile> t \<rightarrow> t'" "P t" "P rhs"
  shows "P t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P t'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(lhs, rhs) \<turnstile> t \<rightarrow> t'
P t
P rhs

goal (1 subgoal):
 1. P t'
[PROOF STEP]
by (auto intro: match subst)


[STATEMENT]
lemma list_comb: "P (list_comb f xs) \<longleftrightarrow> P f \<or> list_ex P xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (list_comb f xs) = (P f \<or> list_ex P xs)
[PROOF STEP]
by (induction xs arbitrary: f) auto


[STATEMENT]
lemma match:
  assumes "match pat t = Some env" "\<not> P t"
  shows "fmpred (\<lambda>_ t. \<not> P t) env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmpred (\<lambda>_ t. \<not> P t) env
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
match pat t = Some env
\<not> P t

goal (1 subgoal):
 1. fmpred (\<lambda>_ t. \<not> P t) env
[PROOF STEP]
by (induction pat t env rule: match_some_induct) auto


[STATEMENT]
lemma related_match:
  assumes "match x u = Some env" "P t u"
  obtains env' where "match x t = Some env'" "P_env env' env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>env'. \<lbrakk>match x t = Some env'; P_env env' env\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
match x u = Some env
P t u

goal (1 subgoal):
 1. (\<And>env'. \<lbrakk>match x t = Some env'; P_env env' env\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (induction x u env arbitrary: t thesis rule: match_some_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>t\<^sub>1 t\<^sub>2 u\<^sub>1 u\<^sub>2 env\<^sub>1 env\<^sub>2 t thesis. \<lbrakk>\<And>t thesis. \<lbrakk>\<And>env'. \<lbrakk>match t\<^sub>1 t = Some env'; P_env env' env\<^sub>1\<rbrakk> \<Longrightarrow> thesis; P t u\<^sub>1\<rbrakk> \<Longrightarrow> thesis; match t\<^sub>1 u\<^sub>1 = Some env\<^sub>1; \<And>t thesis. \<lbrakk>\<And>env'. \<lbrakk>match t\<^sub>2 t = Some env'; P_env env' env\<^sub>2\<rbrakk> \<Longrightarrow> thesis; P t u\<^sub>2\<rbrakk> \<Longrightarrow> thesis; match t\<^sub>2 u\<^sub>2 = Some env\<^sub>2; \<And>env'. \<lbrakk>match (t\<^sub>1 $ t\<^sub>2) t = Some env'; P_env env' (env\<^sub>1 ++\<^sub>f env\<^sub>2)\<rbrakk> \<Longrightarrow> thesis; P t (app u\<^sub>1 u\<^sub>2)\<rbrakk> \<Longrightarrow> thesis
 2. \<And>name t thesis. \<lbrakk>\<And>env'. \<lbrakk>match (Const name) t = Some env'; P_env env' fmempty\<rbrakk> \<Longrightarrow> thesis; P t (const name)\<rbrakk> \<Longrightarrow> thesis
 3. \<And>name u t thesis. \<lbrakk>\<And>env'. \<lbrakk>match (Free name) t = Some env'; P_env env' (fmupd name u fmempty)\<rbrakk> \<Longrightarrow> thesis; P t u\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (app v\<^sub>1 v\<^sub>2 w\<^sub>1 w\<^sub>2 env\<^sub>1 env\<^sub>2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>env'. \<lbrakk>match v\<^sub>1 ?t1 = Some env'; P_env env' env\<^sub>1\<rbrakk> \<Longrightarrow> ?thesis1; P ?t1 w\<^sub>1\<rbrakk> \<Longrightarrow> ?thesis1
\<lbrakk>\<And>env'. \<lbrakk>match v\<^sub>2 ?t1 = Some env'; P_env env' env\<^sub>2\<rbrakk> \<Longrightarrow> ?thesis1; P ?t1 w\<^sub>2\<rbrakk> \<Longrightarrow> ?thesis1
match v\<^sub>1 w\<^sub>1 = Some env\<^sub>1
match v\<^sub>2 w\<^sub>2 = Some env\<^sub>2
\<lbrakk>match (v\<^sub>1 $ v\<^sub>2) t = Some ?env'1; P_env ?env'1 (env\<^sub>1 ++\<^sub>f env\<^sub>2)\<rbrakk> \<Longrightarrow> thesis
P t (app w\<^sub>1 w\<^sub>2)

goal (3 subgoals):
 1. \<And>t\<^sub>1 t\<^sub>2 u\<^sub>1 u\<^sub>2 env\<^sub>1 env\<^sub>2 t thesis. \<lbrakk>\<And>t thesis. \<lbrakk>\<And>env'. \<lbrakk>match t\<^sub>1 t = Some env'; P_env env' env\<^sub>1\<rbrakk> \<Longrightarrow> thesis; P t u\<^sub>1\<rbrakk> \<Longrightarrow> thesis; match t\<^sub>1 u\<^sub>1 = Some env\<^sub>1; \<And>t thesis. \<lbrakk>\<And>env'. \<lbrakk>match t\<^sub>2 t = Some env'; P_env env' env\<^sub>2\<rbrakk> \<Longrightarrow> thesis; P t u\<^sub>2\<rbrakk> \<Longrightarrow> thesis; match t\<^sub>2 u\<^sub>2 = Some env\<^sub>2; \<And>env'. \<lbrakk>match (t\<^sub>1 $ t\<^sub>2) t = Some env'; P_env env' (env\<^sub>1 ++\<^sub>f env\<^sub>2)\<rbrakk> \<Longrightarrow> thesis; P t (app u\<^sub>1 u\<^sub>2)\<rbrakk> \<Longrightarrow> thesis
 2. \<And>name t thesis. \<lbrakk>\<And>env'. \<lbrakk>match (Const name) t = Some env'; P_env env' fmempty\<rbrakk> \<Longrightarrow> thesis; P t (const name)\<rbrakk> \<Longrightarrow> thesis
 3. \<And>name u t thesis. \<lbrakk>\<And>env'. \<lbrakk>match (Free name) t = Some env'; P_env env' (fmupd name u fmempty)\<rbrakk> \<Longrightarrow> thesis; P t u\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
obtain u\<^sub>1 u\<^sub>2 where "t = app u\<^sub>1 u\<^sub>2" "P u\<^sub>1 w\<^sub>1" "P u\<^sub>2 w\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u\<^sub>1 u\<^sub>2. \<lbrakk>t = app u\<^sub>1 u\<^sub>2; P u\<^sub>1 w\<^sub>1; P u\<^sub>2 w\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using P_t_app[OF \<open>P t (app w\<^sub>1 w\<^sub>2)\<close>]
[PROOF STATE]
proof (prove)
using this:
\<exists>t\<^sub>1 t\<^sub>2. t = app t\<^sub>1 t\<^sub>2 \<and> P t\<^sub>1 w\<^sub>1 \<and> P t\<^sub>2 w\<^sub>2

goal (1 subgoal):
 1. (\<And>u\<^sub>1 u\<^sub>2. \<lbrakk>t = app u\<^sub>1 u\<^sub>2; P u\<^sub>1 w\<^sub>1; P u\<^sub>2 w\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t = app u\<^sub>1 u\<^sub>2
P u\<^sub>1 w\<^sub>1
P u\<^sub>2 w\<^sub>2

goal (3 subgoals):
 1. \<And>t\<^sub>1 t\<^sub>2 u\<^sub>1 u\<^sub>2 env\<^sub>1 env\<^sub>2 t thesis. \<lbrakk>\<And>t thesis. \<lbrakk>\<And>env'. \<lbrakk>match t\<^sub>1 t = Some env'; P_env env' env\<^sub>1\<rbrakk> \<Longrightarrow> thesis; P t u\<^sub>1\<rbrakk> \<Longrightarrow> thesis; match t\<^sub>1 u\<^sub>1 = Some env\<^sub>1; \<And>t thesis. \<lbrakk>\<And>env'. \<lbrakk>match t\<^sub>2 t = Some env'; P_env env' env\<^sub>2\<rbrakk> \<Longrightarrow> thesis; P t u\<^sub>2\<rbrakk> \<Longrightarrow> thesis; match t\<^sub>2 u\<^sub>2 = Some env\<^sub>2; \<And>env'. \<lbrakk>match (t\<^sub>1 $ t\<^sub>2) t = Some env'; P_env env' (env\<^sub>1 ++\<^sub>f env\<^sub>2)\<rbrakk> \<Longrightarrow> thesis; P t (app u\<^sub>1 u\<^sub>2)\<rbrakk> \<Longrightarrow> thesis
 2. \<And>name t thesis. \<lbrakk>\<And>env'. \<lbrakk>match (Const name) t = Some env'; P_env env' fmempty\<rbrakk> \<Longrightarrow> thesis; P t (const name)\<rbrakk> \<Longrightarrow> thesis
 3. \<And>name u t thesis. \<lbrakk>\<And>env'. \<lbrakk>match (Free name) t = Some env'; P_env env' (fmupd name u fmempty)\<rbrakk> \<Longrightarrow> thesis; P t u\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with app
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>env'. \<lbrakk>match v\<^sub>1 ?t1 = Some env'; P_env env' env\<^sub>1\<rbrakk> \<Longrightarrow> ?thesis1; P ?t1 w\<^sub>1\<rbrakk> \<Longrightarrow> ?thesis1
\<lbrakk>\<And>env'. \<lbrakk>match v\<^sub>2 ?t1 = Some env'; P_env env' env\<^sub>2\<rbrakk> \<Longrightarrow> ?thesis1; P ?t1 w\<^sub>2\<rbrakk> \<Longrightarrow> ?thesis1
match v\<^sub>1 w\<^sub>1 = Some env\<^sub>1
match v\<^sub>2 w\<^sub>2 = Some env\<^sub>2
\<lbrakk>match (v\<^sub>1 $ v\<^sub>2) t = Some ?env'1; P_env ?env'1 (env\<^sub>1 ++\<^sub>f env\<^sub>2)\<rbrakk> \<Longrightarrow> thesis
P t (app w\<^sub>1 w\<^sub>2)
t = app u\<^sub>1 u\<^sub>2
P u\<^sub>1 w\<^sub>1
P u\<^sub>2 w\<^sub>2
[PROOF STEP]
obtain env\<^sub>1' env\<^sub>2'
    where "match v\<^sub>1 u\<^sub>1 = Some env\<^sub>1'" "P_env env\<^sub>1' env\<^sub>1"
      and "match v\<^sub>2 u\<^sub>2 = Some env\<^sub>2'" "P_env env\<^sub>2' env\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>env'. \<lbrakk>match v\<^sub>1 ?t1 = Some env'; P_env env' env\<^sub>1\<rbrakk> \<Longrightarrow> ?thesis1; P ?t1 w\<^sub>1\<rbrakk> \<Longrightarrow> ?thesis1
\<lbrakk>\<And>env'. \<lbrakk>match v\<^sub>2 ?t1 = Some env'; P_env env' env\<^sub>2\<rbrakk> \<Longrightarrow> ?thesis1; P ?t1 w\<^sub>2\<rbrakk> \<Longrightarrow> ?thesis1
match v\<^sub>1 w\<^sub>1 = Some env\<^sub>1
match v\<^sub>2 w\<^sub>2 = Some env\<^sub>2
\<lbrakk>match (v\<^sub>1 $ v\<^sub>2) t = Some ?env'1; P_env ?env'1 (env\<^sub>1 ++\<^sub>f env\<^sub>2)\<rbrakk> \<Longrightarrow> thesisa__
P t (app w\<^sub>1 w\<^sub>2)
t = app u\<^sub>1 u\<^sub>2
P u\<^sub>1 w\<^sub>1
P u\<^sub>2 w\<^sub>2

goal (1 subgoal):
 1. (\<And>env\<^sub>1' env\<^sub>2'. \<lbrakk>match v\<^sub>1 u\<^sub>1 = Some env\<^sub>1'; P_env env\<^sub>1' env\<^sub>1; match v\<^sub>2 u\<^sub>2 = Some env\<^sub>2'; P_env env\<^sub>2' env\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
match v\<^sub>1 u\<^sub>1 = Some env\<^sub>1'
P_env env\<^sub>1' env\<^sub>1
match v\<^sub>2 u\<^sub>2 = Some env\<^sub>2'
P_env env\<^sub>2' env\<^sub>2

goal (3 subgoals):
 1. \<And>t\<^sub>1 t\<^sub>2 u\<^sub>1 u\<^sub>2 env\<^sub>1 env\<^sub>2 t thesis. \<lbrakk>\<And>t thesis. \<lbrakk>\<And>env'. \<lbrakk>match t\<^sub>1 t = Some env'; P_env env' env\<^sub>1\<rbrakk> \<Longrightarrow> thesis; P t u\<^sub>1\<rbrakk> \<Longrightarrow> thesis; match t\<^sub>1 u\<^sub>1 = Some env\<^sub>1; \<And>t thesis. \<lbrakk>\<And>env'. \<lbrakk>match t\<^sub>2 t = Some env'; P_env env' env\<^sub>2\<rbrakk> \<Longrightarrow> thesis; P t u\<^sub>2\<rbrakk> \<Longrightarrow> thesis; match t\<^sub>2 u\<^sub>2 = Some env\<^sub>2; \<And>env'. \<lbrakk>match (t\<^sub>1 $ t\<^sub>2) t = Some env'; P_env env' (env\<^sub>1 ++\<^sub>f env\<^sub>2)\<rbrakk> \<Longrightarrow> thesis; P t (app u\<^sub>1 u\<^sub>2)\<rbrakk> \<Longrightarrow> thesis
 2. \<And>name t thesis. \<lbrakk>\<And>env'. \<lbrakk>match (Const name) t = Some env'; P_env env' fmempty\<rbrakk> \<Longrightarrow> thesis; P t (const name)\<rbrakk> \<Longrightarrow> thesis
 3. \<And>name u t thesis. \<lbrakk>\<And>env'. \<lbrakk>match (Free name) t = Some env'; P_env env' (fmupd name u fmempty)\<rbrakk> \<Longrightarrow> thesis; P t u\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence "match (v\<^sub>1 $ v\<^sub>2) (app u\<^sub>1 u\<^sub>2) = Some (env\<^sub>1' ++\<^sub>f env\<^sub>2')"
[PROOF STATE]
proof (prove)
using this:
match v\<^sub>1 u\<^sub>1 = Some env\<^sub>1'
P_env env\<^sub>1' env\<^sub>1
match v\<^sub>2 u\<^sub>2 = Some env\<^sub>2'
P_env env\<^sub>2' env\<^sub>2

goal (1 subgoal):
 1. match (v\<^sub>1 $ v\<^sub>2) (app u\<^sub>1 u\<^sub>2) = Some (env\<^sub>1' ++\<^sub>f env\<^sub>2')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
match (v\<^sub>1 $ v\<^sub>2) (app u\<^sub>1 u\<^sub>2) = Some (env\<^sub>1' ++\<^sub>f env\<^sub>2')

goal (3 subgoals):
 1. \<And>t\<^sub>1 t\<^sub>2 u\<^sub>1 u\<^sub>2 env\<^sub>1 env\<^sub>2 t thesis. \<lbrakk>\<And>t thesis. \<lbrakk>\<And>env'. \<lbrakk>match t\<^sub>1 t = Some env'; P_env env' env\<^sub>1\<rbrakk> \<Longrightarrow> thesis; P t u\<^sub>1\<rbrakk> \<Longrightarrow> thesis; match t\<^sub>1 u\<^sub>1 = Some env\<^sub>1; \<And>t thesis. \<lbrakk>\<And>env'. \<lbrakk>match t\<^sub>2 t = Some env'; P_env env' env\<^sub>2\<rbrakk> \<Longrightarrow> thesis; P t u\<^sub>2\<rbrakk> \<Longrightarrow> thesis; match t\<^sub>2 u\<^sub>2 = Some env\<^sub>2; \<And>env'. \<lbrakk>match (t\<^sub>1 $ t\<^sub>2) t = Some env'; P_env env' (env\<^sub>1 ++\<^sub>f env\<^sub>2)\<rbrakk> \<Longrightarrow> thesis; P t (app u\<^sub>1 u\<^sub>2)\<rbrakk> \<Longrightarrow> thesis
 2. \<And>name t thesis. \<lbrakk>\<And>env'. \<lbrakk>match (Const name) t = Some env'; P_env env' fmempty\<rbrakk> \<Longrightarrow> thesis; P t (const name)\<rbrakk> \<Longrightarrow> thesis
 3. \<And>name u t thesis. \<lbrakk>\<And>env'. \<lbrakk>match (Free name) t = Some env'; P_env env' (fmupd name u fmempty)\<rbrakk> \<Longrightarrow> thesis; P t u\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (rule app.prems)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. match (v\<^sub>1 $ v\<^sub>2) t = Some ?env'1
 2. P_env ?env'1 (env\<^sub>1 ++\<^sub>f env\<^sub>2)
[PROOF STEP]
show "match (v\<^sub>1 $ v\<^sub>2) t = Some (env\<^sub>1' ++\<^sub>f env\<^sub>2')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match (v\<^sub>1 $ v\<^sub>2) t = Some (env\<^sub>1' ++\<^sub>f env\<^sub>2')
[PROOF STEP]
unfolding \<open>t = _\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match (v\<^sub>1 $ v\<^sub>2) (app u\<^sub>1 u\<^sub>2) = Some (env\<^sub>1' ++\<^sub>f env\<^sub>2')
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
match (v\<^sub>1 $ v\<^sub>2) t = Some (env\<^sub>1' ++\<^sub>f env\<^sub>2')

goal (1 subgoal):
 1. P_env (env\<^sub>1' ++\<^sub>f env\<^sub>2') (env\<^sub>1 ++\<^sub>f env\<^sub>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P_env (env\<^sub>1' ++\<^sub>f env\<^sub>2') (env\<^sub>1 ++\<^sub>f env\<^sub>2)
[PROOF STEP]
show "P_env (env\<^sub>1' ++\<^sub>f env\<^sub>2') (env\<^sub>1 ++\<^sub>f env\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P_env (env\<^sub>1' ++\<^sub>f env\<^sub>2') (env\<^sub>1 ++\<^sub>f env\<^sub>2)
[PROOF STEP]
by rule fact+
[PROOF STATE]
proof (state)
this:
P_env (env\<^sub>1' ++\<^sub>f env\<^sub>2') (env\<^sub>1 ++\<^sub>f env\<^sub>2)

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

goal (2 subgoals):
 1. \<And>name t thesis. \<lbrakk>\<And>env'. \<lbrakk>match (Const name) t = Some env'; P_env env' fmempty\<rbrakk> \<Longrightarrow> thesis; P t (const name)\<rbrakk> \<Longrightarrow> thesis
 2. \<And>name u t thesis. \<lbrakk>\<And>env'. \<lbrakk>match (Free name) t = Some env'; P_env env' (fmupd name u fmempty)\<rbrakk> \<Longrightarrow> thesis; P t u\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
qed (auto split: option.splits if_splits dest: P_t_const)


[STATEMENT]
lemma list_combI:
  assumes "list_all2 P us\<^sub>1 us\<^sub>2" "P t\<^sub>1 t\<^sub>2"
  shows "P (list_comb t\<^sub>1 us\<^sub>1) (list_comb t\<^sub>2 us\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (list_comb t\<^sub>1 us\<^sub>1) (list_comb t\<^sub>2 us\<^sub>2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
list_all2 P us\<^sub>1 us\<^sub>2
P t\<^sub>1 t\<^sub>2

goal (1 subgoal):
 1. P (list_comb t\<^sub>1 us\<^sub>1) (list_comb t\<^sub>2 us\<^sub>2)
[PROOF STEP]
by (induction arbitrary: t\<^sub>1 t\<^sub>2 rule: list.rel_induct) (auto intro: P_app_app)


[STATEMENT]
lemma list_combE:
  assumes "P t (name $$ args)"
  obtains args' where "t = name $$ args'" "list_all2 P args' args"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' args\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P t (name $$ args)

goal (1 subgoal):
 1. (\<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' args\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (induction args arbitrary: t thesis rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t thesis. \<lbrakk>\<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' []\<rbrakk> \<Longrightarrow> thesis; P t (name $$ [])\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x xs t thesis. \<lbrakk>\<And>t thesis. \<lbrakk>\<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' xs\<rbrakk> \<Longrightarrow> thesis; P t (name $$ xs)\<rbrakk> \<Longrightarrow> thesis; \<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' (xs @ [x])\<rbrakk> \<Longrightarrow> thesis; P t (name $$ (xs @ [x]))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<lbrakk>t = name $$ ?args'1; list_all2 P ?args'1 []\<rbrakk> \<Longrightarrow> thesis
P t (name $$ [])

goal (2 subgoals):
 1. \<And>t thesis. \<lbrakk>\<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' []\<rbrakk> \<Longrightarrow> thesis; P t (name $$ [])\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x xs t thesis. \<lbrakk>\<And>t thesis. \<lbrakk>\<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' xs\<rbrakk> \<Longrightarrow> thesis; P t (name $$ xs)\<rbrakk> \<Longrightarrow> thesis; \<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' (xs @ [x])\<rbrakk> \<Longrightarrow> thesis; P t (name $$ (xs @ [x]))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence "P t (const name)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>t = name $$ ?args'1; list_all2 P ?args'1 []\<rbrakk> \<Longrightarrow> thesis
P t (name $$ [])

goal (1 subgoal):
 1. P t (const name)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P t (const name)

goal (2 subgoals):
 1. \<And>t thesis. \<lbrakk>\<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' []\<rbrakk> \<Longrightarrow> thesis; P t (name $$ [])\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x xs t thesis. \<lbrakk>\<And>t thesis. \<lbrakk>\<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' xs\<rbrakk> \<Longrightarrow> thesis; P t (name $$ xs)\<rbrakk> \<Longrightarrow> thesis; \<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' (xs @ [x])\<rbrakk> \<Longrightarrow> thesis; P t (name $$ (xs @ [x]))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence "t = const name"
[PROOF STATE]
proof (prove)
using this:
P t (const name)

goal (1 subgoal):
 1. t = const name
[PROOF STEP]
using P_t_const
[PROOF STATE]
proof (prove)
using this:
P t (const name)
P ?t (const ?name) \<Longrightarrow> ?t = const ?name

goal (1 subgoal):
 1. t = const name
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t = const name

goal (2 subgoals):
 1. \<And>t thesis. \<lbrakk>\<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' []\<rbrakk> \<Longrightarrow> thesis; P t (name $$ [])\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x xs t thesis. \<lbrakk>\<And>t thesis. \<lbrakk>\<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' xs\<rbrakk> \<Longrightarrow> thesis; P t (name $$ xs)\<rbrakk> \<Longrightarrow> thesis; \<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' (xs @ [x])\<rbrakk> \<Longrightarrow> thesis; P t (name $$ (xs @ [x]))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with Nil
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>t = name $$ ?args'1; list_all2 P ?args'1 []\<rbrakk> \<Longrightarrow> thesis
P t (name $$ [])
t = const name
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>t = name $$ ?args'1; list_all2 P ?args'1 []\<rbrakk> \<Longrightarrow> thesis
P t (name $$ [])
t = const name

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

goal (1 subgoal):
 1. \<And>x xs t thesis. \<lbrakk>\<And>t thesis. \<lbrakk>\<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' xs\<rbrakk> \<Longrightarrow> thesis; P t (name $$ xs)\<rbrakk> \<Longrightarrow> thesis; \<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' (xs @ [x])\<rbrakk> \<Longrightarrow> thesis; P t (name $$ (xs @ [x]))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs t thesis. \<lbrakk>\<And>t thesis. \<lbrakk>\<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' xs\<rbrakk> \<Longrightarrow> thesis; P t (name $$ xs)\<rbrakk> \<Longrightarrow> thesis; \<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' (xs @ [x])\<rbrakk> \<Longrightarrow> thesis; P t (name $$ (xs @ [x]))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>args'. \<lbrakk>?t1 = name $$ args'; list_all2 P args' xs\<rbrakk> \<Longrightarrow> ?thesis1; P ?t1 (name $$ xs)\<rbrakk> \<Longrightarrow> ?thesis1
\<lbrakk>t = name $$ ?args'1; list_all2 P ?args'1 (xs @ [x])\<rbrakk> \<Longrightarrow> thesis
P t (name $$ (xs @ [x]))

goal (1 subgoal):
 1. \<And>x xs t thesis. \<lbrakk>\<And>t thesis. \<lbrakk>\<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' xs\<rbrakk> \<Longrightarrow> thesis; P t (name $$ xs)\<rbrakk> \<Longrightarrow> thesis; \<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' (xs @ [x])\<rbrakk> \<Longrightarrow> thesis; P t (name $$ (xs @ [x]))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence "P t (app (name $$ xs) x)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>args'. \<lbrakk>?t1 = name $$ args'; list_all2 P args' xs\<rbrakk> \<Longrightarrow> ?thesis1; P ?t1 (name $$ xs)\<rbrakk> \<Longrightarrow> ?thesis1
\<lbrakk>t = name $$ ?args'1; list_all2 P ?args'1 (xs @ [x])\<rbrakk> \<Longrightarrow> thesis
P t (name $$ (xs @ [x]))

goal (1 subgoal):
 1. P t (app (name $$ xs) x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P t (app (name $$ xs) x)

goal (1 subgoal):
 1. \<And>x xs t thesis. \<lbrakk>\<And>t thesis. \<lbrakk>\<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' xs\<rbrakk> \<Longrightarrow> thesis; P t (name $$ xs)\<rbrakk> \<Longrightarrow> thesis; \<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' (xs @ [x])\<rbrakk> \<Longrightarrow> thesis; P t (name $$ (xs @ [x]))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
obtain t' y where "t = app t' y" "P t' (name $$ xs)" "P y x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t' y. \<lbrakk>t = app t' y; P t' (name $$ xs); P y x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using P_t_app[OF \<open>P t (app (name $$ xs) x)\<close>]
[PROOF STATE]
proof (prove)
using this:
\<exists>t\<^sub>1 t\<^sub>2. t = app t\<^sub>1 t\<^sub>2 \<and> P t\<^sub>1 (name $$ xs) \<and> P t\<^sub>2 x

goal (1 subgoal):
 1. (\<And>t' y. \<lbrakk>t = app t' y; P t' (name $$ xs); P y x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t = app t' y
P t' (name $$ xs)
P y x

goal (1 subgoal):
 1. \<And>x xs t thesis. \<lbrakk>\<And>t thesis. \<lbrakk>\<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' xs\<rbrakk> \<Longrightarrow> thesis; P t (name $$ xs)\<rbrakk> \<Longrightarrow> thesis; \<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' (xs @ [x])\<rbrakk> \<Longrightarrow> thesis; P t (name $$ (xs @ [x]))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with snoc
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>args'. \<lbrakk>?t1 = name $$ args'; list_all2 P args' xs\<rbrakk> \<Longrightarrow> ?thesis1; P ?t1 (name $$ xs)\<rbrakk> \<Longrightarrow> ?thesis1
\<lbrakk>t = name $$ ?args'1; list_all2 P ?args'1 (xs @ [x])\<rbrakk> \<Longrightarrow> thesis
P t (name $$ (xs @ [x]))
t = app t' y
P t' (name $$ xs)
P y x
[PROOF STEP]
obtain ys where "t' = name $$ ys" "list_all2 P ys xs"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>args'. \<lbrakk>?t1 = name $$ args'; list_all2 P args' xs\<rbrakk> \<Longrightarrow> ?thesis1; P ?t1 (name $$ xs)\<rbrakk> \<Longrightarrow> ?thesis1
\<lbrakk>t = name $$ ?args'1; list_all2 P ?args'1 (xs @ [x])\<rbrakk> \<Longrightarrow> thesisa__
P t (name $$ (xs @ [x]))
t = app t' y
P t' (name $$ xs)
P y x

goal (1 subgoal):
 1. (\<And>ys. \<lbrakk>t' = name $$ ys; list_all2 P ys xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t' = name $$ ys
list_all2 P ys xs

goal (1 subgoal):
 1. \<And>x xs t thesis. \<lbrakk>\<And>t thesis. \<lbrakk>\<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' xs\<rbrakk> \<Longrightarrow> thesis; P t (name $$ xs)\<rbrakk> \<Longrightarrow> thesis; \<And>args'. \<lbrakk>t = name $$ args'; list_all2 P args' (xs @ [x])\<rbrakk> \<Longrightarrow> thesis; P t (name $$ (xs @ [x]))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (rule snoc.prems)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t = name $$ ?args'1
 2. list_all2 P ?args'1 (xs @ [x])
[PROOF STEP]
show "t = name $$ (ys @ [y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = name $$ (ys @ [y])
[PROOF STEP]
unfolding \<open>t = app t' y\<close> \<open>t' = name $$ ys\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app (name $$ ys) y = name $$ (ys @ [y])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t = name $$ (ys @ [y])

goal (1 subgoal):
 1. list_all2 P (ys @ [y]) (xs @ [x])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_all2 P (ys @ [y]) (xs @ [x])
[PROOF STEP]
have "list_all2 P [y] [x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all2 P [y] [x]
[PROOF STEP]
using \<open>P y x\<close>
[PROOF STATE]
proof (prove)
using this:
P y x

goal (1 subgoal):
 1. list_all2 P [y] [x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
list_all2 P [y] [x]

goal (1 subgoal):
 1. list_all2 P (ys @ [y]) (xs @ [x])
[PROOF STEP]
thus "list_all2 P (ys @ [y]) (xs @ [x])"
[PROOF STATE]
proof (prove)
using this:
list_all2 P [y] [x]

goal (1 subgoal):
 1. list_all2 P (ys @ [y]) (xs @ [x])
[PROOF STEP]
using \<open>list_all2 P ys xs\<close>
[PROOF STATE]
proof (prove)
using this:
list_all2 P [y] [x]
list_all2 P ys xs

goal (1 subgoal):
 1. list_all2 P (ys @ [y]) (xs @ [x])
[PROOF STEP]
by (metis list_all2_appendI)
[PROOF STATE]
proof (state)
this:
list_all2 P (ys @ [y]) (xs @ [x])

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unconst_rel: "P t u \<Longrightarrow> unconst t = unconst u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P t u \<Longrightarrow> unconst t = unconst u
[PROOF STEP]
by (metis P_const_t P_t_const const_name_simps(2) is_const_def unconst_const)


[STATEMENT]
lemma unapp_rel: "P t u \<Longrightarrow> rel_option (rel_prod P P) (unapp t) (unapp u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P t u \<Longrightarrow> rel_option (rel_prod P P) (unapp t) (unapp u)
[PROOF STEP]
by (smt P_app_t P_t_app is_app_def left_right_simps(3) option.rel_sel option.sel option.simps(3) rel_prod_inject unapp_app)


[STATEMENT]
lemma match_rel:
  assumes "P t u"
  shows "rel_option P_env (match p t) (match p u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_option P_env (match p t) (match p u)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P t u

goal (1 subgoal):
 1. rel_option P_env (match p t) (match p u)
[PROOF STEP]
proof (induction p arbitrary: t u)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x t u. P t u \<Longrightarrow> rel_option P_env (match (Const x) t) (match (Const x) u)
 2. \<And>x t u. P t u \<Longrightarrow> rel_option P_env (match (Free x) t) (match (Free x) u)
 3. \<And>p t u. \<lbrakk>\<And>t u. P t u \<Longrightarrow> rel_option P_env (match p t) (match p u); P t u\<rbrakk> \<Longrightarrow> rel_option P_env (match (\<Lambda> p) t) (match (\<Lambda> p) u)
 4. \<And>x t u. P t u \<Longrightarrow> rel_option P_env (match (Bound x) t) (match (Bound x) u)
 5. \<And>p1 p2 t u. \<lbrakk>\<And>t u. P t u \<Longrightarrow> rel_option P_env (match p1 t) (match p1 u); \<And>t u. P t u \<Longrightarrow> rel_option P_env (match p2 t) (match p2 u); P t u\<rbrakk> \<Longrightarrow> rel_option P_env (match (p1 $ p2) t) (match (p1 $ p2) u)
[PROOF STEP]
case (Const name)
[PROOF STATE]
proof (state)
this:
P t u

goal (5 subgoals):
 1. \<And>x t u. P t u \<Longrightarrow> rel_option P_env (match (Const x) t) (match (Const x) u)
 2. \<And>x t u. P t u \<Longrightarrow> rel_option P_env (match (Free x) t) (match (Free x) u)
 3. \<And>p t u. \<lbrakk>\<And>t u. P t u \<Longrightarrow> rel_option P_env (match p t) (match p u); P t u\<rbrakk> \<Longrightarrow> rel_option P_env (match (\<Lambda> p) t) (match (\<Lambda> p) u)
 4. \<And>x t u. P t u \<Longrightarrow> rel_option P_env (match (Bound x) t) (match (Bound x) u)
 5. \<And>p1 p2 t u. \<lbrakk>\<And>t u. P t u \<Longrightarrow> rel_option P_env (match p1 t) (match p1 u); \<And>t u. P t u \<Longrightarrow> rel_option P_env (match p2 t) (match p2 u); P t u\<rbrakk> \<Longrightarrow> rel_option P_env (match (p1 $ p2) t) (match (p1 $ p2) u)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P t u

goal (1 subgoal):
 1. rel_option P_env (match (Const name) t) (match (Const name) u)
[PROOF STEP]
by (auto split: option.splits simp: unconst_rel)
[PROOF STATE]
proof (state)
this:
rel_option P_env (match (Const name) t) (match (Const name) u)

goal (4 subgoals):
 1. \<And>x t u. P t u \<Longrightarrow> rel_option P_env (match (Free x) t) (match (Free x) u)
 2. \<And>p t u. \<lbrakk>\<And>t u. P t u \<Longrightarrow> rel_option P_env (match p t) (match p u); P t u\<rbrakk> \<Longrightarrow> rel_option P_env (match (\<Lambda> p) t) (match (\<Lambda> p) u)
 3. \<And>x t u. P t u \<Longrightarrow> rel_option P_env (match (Bound x) t) (match (Bound x) u)
 4. \<And>p1 p2 t u. \<lbrakk>\<And>t u. P t u \<Longrightarrow> rel_option P_env (match p1 t) (match p1 u); \<And>t u. P t u \<Longrightarrow> rel_option P_env (match p2 t) (match p2 u); P t u\<rbrakk> \<Longrightarrow> rel_option P_env (match (p1 $ p2) t) (match (p1 $ p2) u)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x t u. P t u \<Longrightarrow> rel_option P_env (match (Free x) t) (match (Free x) u)
 2. \<And>p t u. \<lbrakk>\<And>t u. P t u \<Longrightarrow> rel_option P_env (match p t) (match p u); P t u\<rbrakk> \<Longrightarrow> rel_option P_env (match (\<Lambda> p) t) (match (\<Lambda> p) u)
 3. \<And>x t u. P t u \<Longrightarrow> rel_option P_env (match (Bound x) t) (match (Bound x) u)
 4. \<And>p1 p2 t u. \<lbrakk>\<And>t u. P t u \<Longrightarrow> rel_option P_env (match p1 t) (match p1 u); \<And>t u. P t u \<Longrightarrow> rel_option P_env (match p2 t) (match p2 u); P t u\<rbrakk> \<Longrightarrow> rel_option P_env (match (p1 $ p2) t) (match (p1 $ p2) u)
[PROOF STEP]
case (App p1 p2)
[PROOF STATE]
proof (state)
this:
P ?t1 ?u1 \<Longrightarrow> rel_option P_env (match p1 ?t1) (match p1 ?u1)
P ?t1 ?u1 \<Longrightarrow> rel_option P_env (match p2 ?t1) (match p2 ?u1)
P t u

goal (4 subgoals):
 1. \<And>x t u. P t u \<Longrightarrow> rel_option P_env (match (Free x) t) (match (Free x) u)
 2. \<And>p t u. \<lbrakk>\<And>t u. P t u \<Longrightarrow> rel_option P_env (match p t) (match p u); P t u\<rbrakk> \<Longrightarrow> rel_option P_env (match (\<Lambda> p) t) (match (\<Lambda> p) u)
 3. \<And>x t u. P t u \<Longrightarrow> rel_option P_env (match (Bound x) t) (match (Bound x) u)
 4. \<And>p1 p2 t u. \<lbrakk>\<And>t u. P t u \<Longrightarrow> rel_option P_env (match p1 t) (match p1 u); \<And>t u. P t u \<Longrightarrow> rel_option P_env (match p2 t) (match p2 u); P t u\<rbrakk> \<Longrightarrow> rel_option P_env (match (p1 $ p2) t) (match (p1 $ p2) u)
[PROOF STEP]
hence "rel_option (rel_prod P P) (unapp t) (unapp u)"
[PROOF STATE]
proof (prove)
using this:
P ?t1 ?u1 \<Longrightarrow> rel_option P_env (match p1 ?t1) (match p1 ?u1)
P ?t1 ?u1 \<Longrightarrow> rel_option P_env (match p2 ?t1) (match p2 ?u1)
P t u

goal (1 subgoal):
 1. rel_option (rel_prod P P) (unapp t) (unapp u)
[PROOF STEP]
by (metis unapp_rel)
[PROOF STATE]
proof (state)
this:
rel_option (rel_prod P P) (unapp t) (unapp u)

goal (4 subgoals):
 1. \<And>x t u. P t u \<Longrightarrow> rel_option P_env (match (Free x) t) (match (Free x) u)
 2. \<And>p t u. \<lbrakk>\<And>t u. P t u \<Longrightarrow> rel_option P_env (match p t) (match p u); P t u\<rbrakk> \<Longrightarrow> rel_option P_env (match (\<Lambda> p) t) (match (\<Lambda> p) u)
 3. \<And>x t u. P t u \<Longrightarrow> rel_option P_env (match (Bound x) t) (match (Bound x) u)
 4. \<And>p1 p2 t u. \<lbrakk>\<And>t u. P t u \<Longrightarrow> rel_option P_env (match p1 t) (match p1 u); \<And>t u. P t u \<Longrightarrow> rel_option P_env (match p2 t) (match p2 u); P t u\<rbrakk> \<Longrightarrow> rel_option P_env (match (p1 $ p2) t) (match (p1 $ p2) u)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
rel_option (rel_prod P P) (unapp t) (unapp u)

goal (1 subgoal):
 1. rel_option P_env (match (p1 $ p2) t) (match (p1 $ p2) u)
[PROOF STEP]
using App
[PROOF STATE]
proof (prove)
using this:
rel_option (rel_prod P P) (unapp t) (unapp u)
P ?t1 ?u1 \<Longrightarrow> rel_option P_env (match p1 ?t1) (match p1 ?u1)
P ?t1 ?u1 \<Longrightarrow> rel_option P_env (match p2 ?t1) (match p2 ?u1)
P t u

goal (1 subgoal):
 1. rel_option P_env (match (p1 $ p2) t) (match (p1 $ p2) u)
[PROOF STEP]
by cases (auto split: option.splits intro!: rel_option_bind)
[PROOF STATE]
proof (state)
this:
rel_option P_env (match (p1 $ p2) t) (match (p1 $ p2) u)

goal (3 subgoals):
 1. \<And>x t u. P t u \<Longrightarrow> rel_option P_env (match (Free x) t) (match (Free x) u)
 2. \<And>p t u. \<lbrakk>\<And>t u. P t u \<Longrightarrow> rel_option P_env (match p t) (match p u); P t u\<rbrakk> \<Longrightarrow> rel_option P_env (match (\<Lambda> p) t) (match (\<Lambda> p) u)
 3. \<And>x t u. P t u \<Longrightarrow> rel_option P_env (match (Bound x) t) (match (Bound x) u)
[PROOF STEP]
qed auto


[STATEMENT]
lemma find_match_rel:
  assumes "list_all2 (rel_prod (=) P) cs cs'" "P t t'"
  shows "rel_option (rel_prod P_env (rel_prod (=) P)) (find_match cs t) (find_match cs' t')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_option (rel_prod P_env (rel_prod (=) P)) (find_match cs t) (find_match cs' t')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
list_all2 (rel_prod (=) P) cs cs'
P t t'

goal (1 subgoal):
 1. rel_option (rel_prod P_env (rel_prod (=) P)) (find_match cs t) (find_match cs' t')
[PROOF STEP]
proof induction
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P t t' \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match [] t) (find_match [] t')
 2. \<And>x xs y ys. \<lbrakk>rel_prod (=) P x y; list_all2 (rel_prod (=) P) xs ys; P t t' \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match xs t) (find_match ys t'); P t t'\<rbrakk> \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match (x # xs) t) (find_match (y # ys) t')
[PROOF STEP]
case (Cons x xs y ys)
[PROOF STATE]
proof (state)
this:
rel_prod (=) P x y
list_all2 (rel_prod (=) P) xs ys
P t t' \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match xs t) (find_match ys t')
P t t'

goal (2 subgoals):
 1. P t t' \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match [] t) (find_match [] t')
 2. \<And>x xs y ys. \<lbrakk>rel_prod (=) P x y; list_all2 (rel_prod (=) P) xs ys; P t t' \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match xs t) (find_match ys t'); P t t'\<rbrakk> \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match (x # xs) t) (find_match (y # ys) t')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rel_prod (=) P x y
list_all2 (rel_prod (=) P) xs ys
P t t' \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match xs t) (find_match ys t')
P t t'

goal (2 subgoals):
 1. P t t' \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match [] t) (find_match [] t')
 2. \<And>x xs y ys. \<lbrakk>rel_prod (=) P x y; list_all2 (rel_prod (=) P) xs ys; P t t' \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match xs t) (find_match ys t'); P t t'\<rbrakk> \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match (x # xs) t) (find_match (y # ys) t')
[PROOF STEP]
obtain px tx py ty where "x = (px, tx)" "y = (py, ty)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>px tx py ty. \<lbrakk>x = (px, tx); y = (py, ty)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases x, cases y) auto
[PROOF STATE]
proof (state)
this:
x = (px, tx)
y = (py, ty)

goal (2 subgoals):
 1. P t t' \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match [] t) (find_match [] t')
 2. \<And>x xs y ys. \<lbrakk>rel_prod (=) P x y; list_all2 (rel_prod (=) P) xs ys; P t t' \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match xs t) (find_match ys t'); P t t'\<rbrakk> \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match (x # xs) t) (find_match (y # ys) t')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = (px, tx)
y = (py, ty)

goal (2 subgoals):
 1. P t t' \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match [] t) (find_match [] t')
 2. \<And>x xs y ys. \<lbrakk>rel_prod (=) P x y; list_all2 (rel_prod (=) P) xs ys; P t t' \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match xs t) (find_match ys t'); P t t'\<rbrakk> \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match (x # xs) t) (find_match (y # ys) t')
[PROOF STEP]
note match_rel[OF Cons(4), where p = px]
[PROOF STATE]
proof (state)
this:
rel_option P_env (match px t) (match px t')

goal (2 subgoals):
 1. P t t' \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match [] t) (find_match [] t')
 2. \<And>x xs y ys. \<lbrakk>rel_prod (=) P x y; list_all2 (rel_prod (=) P) xs ys; P t t' \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match xs t) (find_match ys t'); P t t'\<rbrakk> \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match (x # xs) t) (find_match (y # ys) t')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rel_prod (=) P x y
list_all2 (rel_prod (=) P) xs ys
P t t' \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match xs t) (find_match ys t')
P t t'
x = (px, tx)
y = (py, ty)
rel_option P_env (match px t) (match px t')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
rel_prod (=) P x y
list_all2 (rel_prod (=) P) xs ys
P t t' \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match xs t) (find_match ys t')
P t t'
x = (px, tx)
y = (py, ty)
rel_option P_env (match px t) (match px t')

goal (1 subgoal):
 1. rel_option (rel_prod P_env (rel_prod (=) P)) (find_match (x # xs) t) (find_match (y # ys) t')
[PROOF STEP]
by (auto elim: option.rel_cases)
[PROOF STATE]
proof (state)
this:
rel_option (rel_prod P_env (rel_prod (=) P)) (find_match (x # xs) t) (find_match (y # ys) t')

goal (1 subgoal):
 1. P t t' \<Longrightarrow> rel_option (rel_prod P_env (rel_prod (=) P)) (find_match [] t) (find_match [] t')
[PROOF STEP]
qed auto


[STATEMENT]
lemma convert_term_id:
  assumes "no_abs t"
  shows "convert_term t = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convert_term t = t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
no_abs t

goal (1 subgoal):
 1. convert_term t = t
[PROOF STEP]
by induction auto


[STATEMENT]
lemma convert_term_no_abs:
  assumes "no_abs t"
  shows "no_abs (convert_term t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_abs (convert_term t)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
no_abs t

goal (1 subgoal):
 1. no_abs (convert_term t)
[PROOF STEP]
by induction auto


[STATEMENT]
lemma convert_term_inj:
  assumes "no_abs t" "no_abs t'" "convert_term t = convert_term t'"
  shows "t = t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = t'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
no_abs t
no_abs t'
convert_term t = convert_term t'

goal (1 subgoal):
 1. t = t'
[PROOF STEP]
proof (induction t arbitrary: t')
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>name t'. \<lbrakk>no_abs t'; convert_term (free name) = convert_term t'\<rbrakk> \<Longrightarrow> free name = t'
 2. \<And>name t'. \<lbrakk>no_abs t'; convert_term (const name) = convert_term t'\<rbrakk> \<Longrightarrow> const name = t'
 3. \<And>t\<^sub>1 t\<^sub>2 t'. \<lbrakk>\<And>t'. \<lbrakk>no_abs t'; convert_term t\<^sub>1 = convert_term t'\<rbrakk> \<Longrightarrow> t\<^sub>1 = t'; no_abs t\<^sub>1; \<And>t'. \<lbrakk>no_abs t'; convert_term t\<^sub>2 = convert_term t'\<rbrakk> \<Longrightarrow> t\<^sub>2 = t'; no_abs t\<^sub>2; no_abs t'; convert_term (app t\<^sub>1 t\<^sub>2) = convert_term t'\<rbrakk> \<Longrightarrow> app t\<^sub>1 t\<^sub>2 = t'
[PROOF STEP]
case (free name)
[PROOF STATE]
proof (state)
this:
no_abs t'
convert_term (free name) = convert_term t'

goal (3 subgoals):
 1. \<And>name t'. \<lbrakk>no_abs t'; convert_term (free name) = convert_term t'\<rbrakk> \<Longrightarrow> free name = t'
 2. \<And>name t'. \<lbrakk>no_abs t'; convert_term (const name) = convert_term t'\<rbrakk> \<Longrightarrow> const name = t'
 3. \<And>t\<^sub>1 t\<^sub>2 t'. \<lbrakk>\<And>t'. \<lbrakk>no_abs t'; convert_term t\<^sub>1 = convert_term t'\<rbrakk> \<Longrightarrow> t\<^sub>1 = t'; no_abs t\<^sub>1; \<And>t'. \<lbrakk>no_abs t'; convert_term t\<^sub>2 = convert_term t'\<rbrakk> \<Longrightarrow> t\<^sub>2 = t'; no_abs t\<^sub>2; no_abs t'; convert_term (app t\<^sub>1 t\<^sub>2) = convert_term t'\<rbrakk> \<Longrightarrow> app t\<^sub>1 t\<^sub>2 = t'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
no_abs t'
convert_term (free name) = convert_term t'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
no_abs t'
convert_term (free name) = convert_term t'

goal (1 subgoal):
 1. free name = t'
[PROOF STEP]
by cases (auto dest: term_inject)
[PROOF STATE]
proof (state)
this:
free name = t'

goal (2 subgoals):
 1. \<And>name t'. \<lbrakk>no_abs t'; convert_term (const name) = convert_term t'\<rbrakk> \<Longrightarrow> const name = t'
 2. \<And>t\<^sub>1 t\<^sub>2 t'. \<lbrakk>\<And>t'. \<lbrakk>no_abs t'; convert_term t\<^sub>1 = convert_term t'\<rbrakk> \<Longrightarrow> t\<^sub>1 = t'; no_abs t\<^sub>1; \<And>t'. \<lbrakk>no_abs t'; convert_term t\<^sub>2 = convert_term t'\<rbrakk> \<Longrightarrow> t\<^sub>2 = t'; no_abs t\<^sub>2; no_abs t'; convert_term (app t\<^sub>1 t\<^sub>2) = convert_term t'\<rbrakk> \<Longrightarrow> app t\<^sub>1 t\<^sub>2 = t'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>name t'. \<lbrakk>no_abs t'; convert_term (const name) = convert_term t'\<rbrakk> \<Longrightarrow> const name = t'
 2. \<And>t\<^sub>1 t\<^sub>2 t'. \<lbrakk>\<And>t'. \<lbrakk>no_abs t'; convert_term t\<^sub>1 = convert_term t'\<rbrakk> \<Longrightarrow> t\<^sub>1 = t'; no_abs t\<^sub>1; \<And>t'. \<lbrakk>no_abs t'; convert_term t\<^sub>2 = convert_term t'\<rbrakk> \<Longrightarrow> t\<^sub>2 = t'; no_abs t\<^sub>2; no_abs t'; convert_term (app t\<^sub>1 t\<^sub>2) = convert_term t'\<rbrakk> \<Longrightarrow> app t\<^sub>1 t\<^sub>2 = t'
[PROOF STEP]
case (const name)
[PROOF STATE]
proof (state)
this:
no_abs t'
convert_term (const name) = convert_term t'

goal (2 subgoals):
 1. \<And>name t'. \<lbrakk>no_abs t'; convert_term (const name) = convert_term t'\<rbrakk> \<Longrightarrow> const name = t'
 2. \<And>t\<^sub>1 t\<^sub>2 t'. \<lbrakk>\<And>t'. \<lbrakk>no_abs t'; convert_term t\<^sub>1 = convert_term t'\<rbrakk> \<Longrightarrow> t\<^sub>1 = t'; no_abs t\<^sub>1; \<And>t'. \<lbrakk>no_abs t'; convert_term t\<^sub>2 = convert_term t'\<rbrakk> \<Longrightarrow> t\<^sub>2 = t'; no_abs t\<^sub>2; no_abs t'; convert_term (app t\<^sub>1 t\<^sub>2) = convert_term t'\<rbrakk> \<Longrightarrow> app t\<^sub>1 t\<^sub>2 = t'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
no_abs t'
convert_term (const name) = convert_term t'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
no_abs t'
convert_term (const name) = convert_term t'

goal (1 subgoal):
 1. const name = t'
[PROOF STEP]
by cases (auto dest: term_inject)
[PROOF STATE]
proof (state)
this:
const name = t'

goal (1 subgoal):
 1. \<And>t\<^sub>1 t\<^sub>2 t'. \<lbrakk>\<And>t'. \<lbrakk>no_abs t'; convert_term t\<^sub>1 = convert_term t'\<rbrakk> \<Longrightarrow> t\<^sub>1 = t'; no_abs t\<^sub>1; \<And>t'. \<lbrakk>no_abs t'; convert_term t\<^sub>2 = convert_term t'\<rbrakk> \<Longrightarrow> t\<^sub>2 = t'; no_abs t\<^sub>2; no_abs t'; convert_term (app t\<^sub>1 t\<^sub>2) = convert_term t'\<rbrakk> \<Longrightarrow> app t\<^sub>1 t\<^sub>2 = t'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t\<^sub>1 t\<^sub>2 t'. \<lbrakk>\<And>t'. \<lbrakk>no_abs t'; convert_term t\<^sub>1 = convert_term t'\<rbrakk> \<Longrightarrow> t\<^sub>1 = t'; no_abs t\<^sub>1; \<And>t'. \<lbrakk>no_abs t'; convert_term t\<^sub>2 = convert_term t'\<rbrakk> \<Longrightarrow> t\<^sub>2 = t'; no_abs t\<^sub>2; no_abs t'; convert_term (app t\<^sub>1 t\<^sub>2) = convert_term t'\<rbrakk> \<Longrightarrow> app t\<^sub>1 t\<^sub>2 = t'
[PROOF STEP]
case (app t\<^sub>1 t\<^sub>2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>no_abs ?t'; convert_term t\<^sub>1 = convert_term ?t'\<rbrakk> \<Longrightarrow> t\<^sub>1 = ?t'
\<lbrakk>no_abs ?t'; convert_term t\<^sub>2 = convert_term ?t'\<rbrakk> \<Longrightarrow> t\<^sub>2 = ?t'
no_abs t\<^sub>1
no_abs t\<^sub>2
no_abs t'
convert_term (app t\<^sub>1 t\<^sub>2) = convert_term t'

goal (1 subgoal):
 1. \<And>t\<^sub>1 t\<^sub>2 t'. \<lbrakk>\<And>t'. \<lbrakk>no_abs t'; convert_term t\<^sub>1 = convert_term t'\<rbrakk> \<Longrightarrow> t\<^sub>1 = t'; no_abs t\<^sub>1; \<And>t'. \<lbrakk>no_abs t'; convert_term t\<^sub>2 = convert_term t'\<rbrakk> \<Longrightarrow> t\<^sub>2 = t'; no_abs t\<^sub>2; no_abs t'; convert_term (app t\<^sub>1 t\<^sub>2) = convert_term t'\<rbrakk> \<Longrightarrow> app t\<^sub>1 t\<^sub>2 = t'
[PROOF STEP]
from \<open>no_abs t'\<close>
[PROOF STATE]
proof (chain)
picking this:
no_abs t'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
no_abs t'

goal (1 subgoal):
 1. app t\<^sub>1 t\<^sub>2 = t'
[PROOF STEP]
apply cases
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>name. t' = free name \<Longrightarrow> app t\<^sub>1 t\<^sub>2 = t'
 2. \<And>name. t' = const name \<Longrightarrow> app t\<^sub>1 t\<^sub>2 = t'
 3. \<And>t\<^sub>1' t\<^sub>2'. \<lbrakk>t' = app t\<^sub>1' t\<^sub>2'; no_abs t\<^sub>1'; no_abs t\<^sub>2'\<rbrakk> \<Longrightarrow> app t\<^sub>1 t\<^sub>2 = t'
[PROOF STEP]
using app
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>no_abs ?t'; convert_term t\<^sub>1 = convert_term ?t'\<rbrakk> \<Longrightarrow> t\<^sub>1 = ?t'
\<lbrakk>no_abs ?t'; convert_term t\<^sub>2 = convert_term ?t'\<rbrakk> \<Longrightarrow> t\<^sub>2 = ?t'
no_abs t\<^sub>1
no_abs t\<^sub>2
no_abs t'
convert_term (app t\<^sub>1 t\<^sub>2) = convert_term t'

goal (3 subgoals):
 1. \<And>name. t' = free name \<Longrightarrow> app t\<^sub>1 t\<^sub>2 = t'
 2. \<And>name. t' = const name \<Longrightarrow> app t\<^sub>1 t\<^sub>2 = t'
 3. \<And>t\<^sub>1' t\<^sub>2'. \<lbrakk>t' = app t\<^sub>1' t\<^sub>2'; no_abs t\<^sub>1'; no_abs t\<^sub>2'\<rbrakk> \<Longrightarrow> app t\<^sub>1 t\<^sub>2 = t'
[PROOF STEP]
by (auto dest: term_inject)
[PROOF STATE]
proof (state)
this:
app t\<^sub>1 t\<^sub>2 = t'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma convert_term_idem:
  assumes "no_abs t"
  shows "convert_term (convert_term t) = convert_term t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convert_term (convert_term t) = convert_term t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
no_abs t

goal (1 subgoal):
 1. convert_term (convert_term t) = convert_term t
[PROOF STEP]
by (induction t) auto


[STATEMENT]
lemma convert_term_frees[simp]:
  assumes "no_abs t"
  shows "frees (convert_term t) = frees t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frees (convert_term t) = frees t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
no_abs t

goal (1 subgoal):
 1. frees (convert_term t) = frees t
[PROOF STEP]
by induction auto


[STATEMENT]
lemma convert_term_consts[simp]:
  assumes "no_abs t"
  shows "consts (convert_term t) = consts t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consts (convert_term t) = consts t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
no_abs t

goal (1 subgoal):
 1. consts (convert_term t) = consts t
[PROOF STEP]
by induction auto


[STATEMENT]
lemma convert_term_match:
  assumes "match t u = Some env"
  shows "match t (convert_term u) = Some (fmmap convert_term env)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match t (convert_term u) = Some (fmmap convert_term env)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
match t u = Some env

goal (1 subgoal):
 1. match t (convert_term u) = Some (fmmap convert_term env)
[PROOF STEP]
by (induction t u env rule: match_some_induct) auto


[STATEMENT]
lemma  "\<delta>(null::('\<AA>)Real) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> null = false
[PROOF STEP]
by simp


[STATEMENT]
lemma  "\<upsilon>(null::('\<AA>)Real) = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<upsilon> null = true
[PROOF STEP]
by simp


[STATEMENT]
lemma [simp,code_unfold]: "\<delta> (\<lambda>_. \<lfloor>\<lfloor>n\<rfloor>\<rfloor>) = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> (\<lambda>_. \<lfloor>\<lfloor>n\<rfloor>\<rfloor>) = true
[PROOF STEP]
by(simp add:defined_def true_def
               bot_fun_def bot_option_def null_fun_def null_option_def)


[STATEMENT]
lemma [simp,code_unfold]: "\<upsilon> (\<lambda>_. \<lfloor>\<lfloor>n\<rfloor>\<rfloor>) = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<upsilon> (\<lambda>_. \<lfloor>\<lfloor>n\<rfloor>\<rfloor>) = true
[PROOF STEP]
by(simp add:valid_def true_def
               bot_fun_def bot_option_def)


[STATEMENT]
lemma [simp,code_unfold]: "\<delta> \<zero>.\<zero> = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> \<zero>.\<zero> = true
[PROOF STEP]
by(simp add:OclReal0_def)


[STATEMENT]
lemma [simp,code_unfold]: "\<upsilon> \<zero>.\<zero> = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<upsilon> \<zero>.\<zero> = true
[PROOF STEP]
by(simp add:OclReal0_def)


[STATEMENT]
lemma [simp,code_unfold]: "\<delta> \<one>.\<zero> = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> \<one>.\<zero> = true
[PROOF STEP]
by(simp add:OclReal1_def)


[STATEMENT]
lemma [simp,code_unfold]: "\<upsilon> \<one>.\<zero> = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<upsilon> \<one>.\<zero> = true
[PROOF STEP]
by(simp add:OclReal1_def)


[STATEMENT]
lemma [simp,code_unfold]: "\<delta> \<two>.\<zero> = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> \<two>.\<zero> = true
[PROOF STEP]
by(simp add:OclReal2_def)


[STATEMENT]
lemma [simp,code_unfold]: "\<upsilon> \<two>.\<zero> = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<upsilon> \<two>.\<zero> = true
[PROOF STEP]
by(simp add:OclReal2_def)


[STATEMENT]
lemma [simp,code_unfold]: "\<delta> \<six>.\<zero> = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> \<six>.\<zero> = true
[PROOF STEP]
by(simp add:OclReal6_def)


[STATEMENT]
lemma [simp,code_unfold]: "\<upsilon> \<six>.\<zero> = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<upsilon> \<six>.\<zero> = true
[PROOF STEP]
by(simp add:OclReal6_def)


[STATEMENT]
lemma [simp,code_unfold]: "\<delta> \<eight>.\<zero> = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> \<eight>.\<zero> = true
[PROOF STEP]
by(simp add:OclReal8_def)


[STATEMENT]
lemma [simp,code_unfold]: "\<upsilon> \<eight>.\<zero> = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<upsilon> \<eight>.\<zero> = true
[PROOF STEP]
by(simp add:OclReal8_def)


[STATEMENT]
lemma [simp,code_unfold]: "\<delta> \<nine>.\<zero> = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> \<nine>.\<zero> = true
[PROOF STEP]
by(simp add:OclReal9_def)


[STATEMENT]
lemma [simp,code_unfold]: "\<upsilon> \<nine>.\<zero> = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<upsilon> \<nine>.\<zero> = true
[PROOF STEP]
by(simp add:OclReal9_def)


[STATEMENT]
lemma OclAdd\<^sub>R\<^sub>e\<^sub>a\<^sub>l_commute: "(X +\<^sub>r\<^sub>e\<^sub>a\<^sub>l Y) = (Y +\<^sub>r\<^sub>e\<^sub>a\<^sub>l X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X +\<^sub>r\<^sub>e\<^sub>a\<^sub>l Y) = (Y +\<^sub>r\<^sub>e\<^sub>a\<^sub>l X)
[PROOF STEP]
by(rule ext,auto simp:true_def false_def OclAdd\<^sub>R\<^sub>e\<^sub>a\<^sub>l_def invalid_def
                   split: option.split option.split_asm
                          bool.split bool.split_asm)