[STATEMENT]
lemma konig:
  assumes inf: "\<not>finite T"
  assumes wellformed: "wf_tree T"
  shows "\<exists>c. wf_infpath c \<and> (\<forall>n. (c n) \<in> T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. wf_infpath c \<and> (\<forall>n. c n \<in> T)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_infpath ?c \<and> (\<forall>n. ?c n \<in> T)
[PROOF STEP]
let ?subtree = "subtree T"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_infpath ?c \<and> (\<forall>n. ?c n \<in> T)
[PROOF STEP]
let ?nextnode = "\<lambda>ds. (if \<not>finite (?subtree (ds @ [Left])) then ds @ [Left] else ds @ [Right])"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_infpath ?c \<and> (\<forall>n. ?c n \<in> T)
[PROOF STEP]
let ?c = "buildchain ?nextnode"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_infpath ?c \<and> (\<forall>n. ?c n \<in> T)
[PROOF STEP]
have is_chain: "wf_infpath ?c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_infpath (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf_infpath (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]))

goal (1 subgoal):
 1. wf_infpath ?c \<and> (\<forall>n. ?c n \<in> T)
[PROOF STEP]
from wellformed
[PROOF STATE]
proof (chain)
picking this:
wf_tree T
[PROOF STEP]
have prefix: "\<forall>ds d. (ds @ d) \<in> T \<longrightarrow> ds \<in> T"
[PROOF STATE]
proof (prove)
using this:
wf_tree T

goal (1 subgoal):
 1. wf_tree T
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
wf_tree T

goal (1 subgoal):
 1. wf_infpath ?c \<and> (\<forall>n. ?c n \<in> T)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
wf_tree T

goal (1 subgoal):
 1. wf_infpath ?c \<and> (\<forall>n. ?c n \<in> T)
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_infpath ?c \<and> (\<forall>n. ?c n \<in> T)
[PROOF STEP]
have "(?c n) \<in> T \<and> \<not>finite (?subtree (?c n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n))
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) 0 \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) 0))
 2. \<And>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n)) \<Longrightarrow> buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) 0 \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) 0))
 2. \<And>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n)) \<Longrightarrow> buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))
[PROOF STEP]
have "\<exists>ds. ds \<in> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ds. ds \<in> T
[PROOF STEP]
using inf
[PROOF STATE]
proof (prove)
using this:
infinite T

goal (1 subgoal):
 1. \<exists>ds. ds \<in> T
[PROOF STEP]
by (simp add: not_finite_existsD)
[PROOF STATE]
proof (state)
this:
\<exists>ds. ds \<in> T

goal (2 subgoals):
 1. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) 0 \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) 0))
 2. \<And>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n)) \<Longrightarrow> buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>ds. ds \<in> T
[PROOF STEP]
obtain ds where "ds \<in> T"
[PROOF STATE]
proof (prove)
using this:
\<exists>ds. ds \<in> T

goal (1 subgoal):
 1. (\<And>ds. ds \<in> T \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ds \<in> T

goal (2 subgoals):
 1. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) 0 \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) 0))
 2. \<And>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n)) \<Longrightarrow> buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ds \<in> T
[PROOF STEP]
have "([]@ds) \<in> T"
[PROOF STATE]
proof (prove)
using this:
ds \<in> T

goal (1 subgoal):
 1. [] @ ds \<in> T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[] @ ds \<in> T

goal (2 subgoals):
 1. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) 0 \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) 0))
 2. \<And>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n)) \<Longrightarrow> buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[] @ ds \<in> T
[PROOF STEP]
have "[] \<in> T"
[PROOF STATE]
proof (prove)
using this:
[] @ ds \<in> T

goal (1 subgoal):
 1. [] \<in> T
[PROOF STEP]
using prefix
[PROOF STATE]
proof (prove)
using this:
[] @ ds \<in> T
wf_tree T

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

goal (2 subgoals):
 1. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) 0 \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) 0))
 2. \<And>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n)) \<Longrightarrow> buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[] \<in> T
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[] \<in> T

goal (1 subgoal):
 1. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) 0 \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) 0))
[PROOF STEP]
using inf
[PROOF STATE]
proof (prove)
using this:
[] \<in> T
infinite T

goal (1 subgoal):
 1. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) 0 \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) 0))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) 0 \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) 0))

goal (1 subgoal):
 1. \<And>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n)) \<Longrightarrow> buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n)) \<Longrightarrow> buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n))

goal (1 subgoal):
 1. \<And>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n)) \<Longrightarrow> buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))
[PROOF STEP]
from Suc
[PROOF STATE]
proof (chain)
picking this:
buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n))
[PROOF STEP]
have next_in:  "(?c n) \<in> T"
[PROOF STATE]
proof (prove)
using this:
buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n))

goal (1 subgoal):
 1. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T

goal (1 subgoal):
 1. \<And>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n)) \<Longrightarrow> buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))
[PROOF STEP]
from Suc
[PROOF STATE]
proof (chain)
picking this:
buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n))
[PROOF STEP]
have next_inf: "\<not>finite (?subtree (?c n))"
[PROOF STATE]
proof (prove)
using this:
buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n))

goal (1 subgoal):
 1. infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n))

goal (1 subgoal):
 1. \<And>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n)) \<Longrightarrow> buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))
[PROOF STEP]
from next_inf
[PROOF STATE]
proof (chain)
picking this:
infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n))
[PROOF STEP]
have next_next_inf:
           "\<not>finite (?subtree (?nextnode (?c n)))"
[PROOF STATE]
proof (prove)
using this:
infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n))

goal (1 subgoal):
 1. infinite (subtree T (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]))
[PROOF STEP]
using inf_subs
[PROOF STATE]
proof (prove)
using this:
infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n))
infinite (subtree ?T ?ds) \<Longrightarrow> infinite (subtree ?T (?ds @ [Left])) \<or> infinite (subtree ?T (?ds @ [Right]))

goal (1 subgoal):
 1. infinite (subtree T (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infinite (subtree T (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]))

goal (1 subgoal):
 1. \<And>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n)) \<Longrightarrow> buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infinite (subtree T (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]))
[PROOF STEP]
have "\<exists>ds. ds \<in> ?subtree (?nextnode (?c n))"
[PROOF STATE]
proof (prove)
using this:
infinite (subtree T (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]))

goal (1 subgoal):
 1. \<exists>ds. ds \<in> subtree T (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right])
[PROOF STEP]
by (simp add: not_finite_existsD)
[PROOF STATE]
proof (state)
this:
\<exists>ds. ds \<in> subtree T (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right])

goal (1 subgoal):
 1. \<And>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n)) \<Longrightarrow> buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>ds. ds \<in> subtree T (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right])
[PROOF STEP]
obtain ds where dss: "ds \<in> ?subtree (?nextnode (?c n))"
[PROOF STATE]
proof (prove)
using this:
\<exists>ds. ds \<in> subtree T (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right])

goal (1 subgoal):
 1. (\<And>ds. ds \<in> subtree T (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ds \<in> subtree T (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right])

goal (1 subgoal):
 1. \<And>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n)) \<Longrightarrow> buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ds \<in> subtree T (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right])
[PROOF STEP]
have "ds \<in> T" "\<exists>suf. ds = (?nextnode (?c n)) @ suf"
[PROOF STATE]
proof (prove)
using this:
ds \<in> subtree T (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right])

goal (1 subgoal):
 1. ds \<in> T &&& \<exists>suf. ds = (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]) @ suf
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ds \<in> T
\<exists>suf. ds = (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]) @ suf

goal (1 subgoal):
 1. \<And>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n)) \<Longrightarrow> buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ds \<in> T
\<exists>suf. ds = (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]) @ suf
[PROOF STEP]
obtain suf where "ds \<in> T \<and> ds = (?nextnode (?c n)) @ suf"
[PROOF STATE]
proof (prove)
using this:
ds \<in> T
\<exists>suf. ds = (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]) @ suf

goal (1 subgoal):
 1. (\<And>suf. ds \<in> T \<and> ds = (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]) @ suf \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ds \<in> T \<and> ds = (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]) @ suf

goal (1 subgoal):
 1. \<And>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n)) \<Longrightarrow> buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ds \<in> T \<and> ds = (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]) @ suf
[PROOF STEP]
have "(?nextnode (?c n)) \<in> T"
[PROOF STATE]
proof (prove)
using this:
ds \<in> T \<and> ds = (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]) @ suf

goal (1 subgoal):
 1. (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]) \<in> T
[PROOF STEP]
using prefix
[PROOF STATE]
proof (prove)
using this:
ds \<in> T \<and> ds = (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]) @ suf
wf_tree T

goal (1 subgoal):
 1. (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]) \<in> T
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]) \<in> T

goal (1 subgoal):
 1. \<And>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n)) \<Longrightarrow> buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]) \<in> T
[PROOF STEP]
have "(?c (Suc n)) \<in> T"
[PROOF STATE]
proof (prove)
using this:
(if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]) \<in> T

goal (1 subgoal):
 1. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T

goal (1 subgoal):
 1. \<And>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n)) \<Longrightarrow> buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T

goal (1 subgoal):
 1. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))
[PROOF STEP]
using next_next_inf
[PROOF STATE]
proof (prove)
using this:
buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T
infinite (subtree T (if infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left])) then buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Left] else buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n @ [Right]))

goal (1 subgoal):
 1. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n) \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) (Suc n)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n))

goal (1 subgoal):
 1. wf_infpath ?c \<and> (\<forall>n. ?c n \<in> T)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) ?n2 \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) ?n2))

goal (1 subgoal):
 1. wf_infpath ?c \<and> (\<forall>n. ?c n \<in> T)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) ?n2 \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) ?n2))
[PROOF STEP]
show "wf_infpath ?c \<and> (\<forall>n. (?c n)\<in> T) "
[PROOF STATE]
proof (prove)
using this:
buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) ?n2 \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) ?n2))

goal (1 subgoal):
 1. wf_infpath (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right])) \<and> (\<forall>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T)
[PROOF STEP]
using is_chain
[PROOF STATE]
proof (prove)
using this:
buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) ?n2 \<in> T \<and> infinite (subtree T (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) ?n2))
wf_infpath (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]))

goal (1 subgoal):
 1. wf_infpath (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right])) \<and> (\<forall>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf_infpath (buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right])) \<and> (\<forall>n. buildchain (\<lambda>ds. if infinite (subtree T (ds @ [Left])) then ds @ [Left] else ds @ [Right]) n \<in> T)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_jvmprog_is_wf: "wf_jvm_prog\<^bsub>P\<^bsub>\<Phi>\<^esub>\<^esub> (P\<^bsub>wf\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_jvm_prog\<^bsub>P\<^bsub>\<Phi>\<^esub>\<^esub> P\<^bsub>wf\<^esub>
[PROOF STEP]
using Rep_wf_jvmprog [of P]
[PROOF STATE]
proof (prove)
using this:
Rep_wf_jvmprog P \<in> wf_jvmprog

goal (1 subgoal):
 1. wf_jvm_prog\<^bsub>P\<^bsub>\<Phi>\<^esub>\<^esub> P\<^bsub>wf\<^esub>
[PROOF STEP]
by (auto simp: wf_jvmprog_def split_beta)


[STATEMENT]
lemma find_handler_decr [simp]: "find_handler_for P Exc cs \<noteq> c#cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_handler_for P Exc cs \<noteq> c # cs
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. find_handler_for P Exc cs = c # cs \<Longrightarrow> False
[PROOF STEP]
assume "find_handler_for P Exc cs = c#cs"
[PROOF STATE]
proof (state)
this:
find_handler_for P Exc cs = c # cs

goal (1 subgoal):
 1. find_handler_for P Exc cs = c # cs \<Longrightarrow> False
[PROOF STEP]
hence "length cs < length (find_handler_for P Exc cs)"
[PROOF STATE]
proof (prove)
using this:
find_handler_for P Exc cs = c # cs

goal (1 subgoal):
 1. length cs < length (find_handler_for P Exc cs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length cs < length (find_handler_for P Exc cs)

goal (1 subgoal):
 1. find_handler_for P Exc cs = c # cs \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
length cs < length (find_handler_for P Exc cs)

goal (1 subgoal):
 1. False
[PROOF STEP]
by (induct cs, auto)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stkss_length [simp]: "length (stkss P cs stk) = length cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (stkss P cs stk) = length cs
[PROOF STEP]
by (induct cs) auto


[STATEMENT]
lemma locss_length [simp]: "length (locss P cs loc) = length cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (locss P cs loc) = length cs
[PROOF STEP]
by (induct cs) auto


[STATEMENT]
lemma nth_stkss:
  "\<lbrakk> a < length cs; b < length (stkss P cs stk ! (length cs - Suc a)) \<rbrakk>
  \<Longrightarrow> stkss P cs stk ! (length cs - Suc a) !
    (length (stkss P cs stk ! (length cs - Suc a)) - Suc b) = stk (a,b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < length cs; b < length (stkss P cs stk ! (length cs - Suc a))\<rbrakk> \<Longrightarrow> stkss P cs stk ! (length cs - Suc a) ! (length (stkss P cs stk ! (length cs - Suc a)) - Suc b) = stk (a, b)
[PROOF STEP]
proof (induct cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>a < length []; b < length (stkss P [] stk ! (length [] - Suc a))\<rbrakk> \<Longrightarrow> stkss P [] stk ! (length [] - Suc a) ! (length (stkss P [] stk ! (length [] - Suc a)) - Suc b) = stk (a, b)
 2. \<And>aa cs. \<lbrakk>\<lbrakk>a < length cs; b < length (stkss P cs stk ! (length cs - Suc a))\<rbrakk> \<Longrightarrow> stkss P cs stk ! (length cs - Suc a) ! (length (stkss P cs stk ! (length cs - Suc a)) - Suc b) = stk (a, b); a < length (aa # cs); b < length (stkss P (aa # cs) stk ! (length (aa # cs) - Suc a))\<rbrakk> \<Longrightarrow> stkss P (aa # cs) stk ! (length (aa # cs) - Suc a) ! (length (stkss P (aa # cs) stk ! (length (aa # cs) - Suc a)) - Suc b) = stk (a, b)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
a < length []
b < length (stkss P [] stk ! (length [] - Suc a))

goal (2 subgoals):
 1. \<lbrakk>a < length []; b < length (stkss P [] stk ! (length [] - Suc a))\<rbrakk> \<Longrightarrow> stkss P [] stk ! (length [] - Suc a) ! (length (stkss P [] stk ! (length [] - Suc a)) - Suc b) = stk (a, b)
 2. \<And>aa cs. \<lbrakk>\<lbrakk>a < length cs; b < length (stkss P cs stk ! (length cs - Suc a))\<rbrakk> \<Longrightarrow> stkss P cs stk ! (length cs - Suc a) ! (length (stkss P cs stk ! (length cs - Suc a)) - Suc b) = stk (a, b); a < length (aa # cs); b < length (stkss P (aa # cs) stk ! (length (aa # cs) - Suc a))\<rbrakk> \<Longrightarrow> stkss P (aa # cs) stk ! (length (aa # cs) - Suc a) ! (length (stkss P (aa # cs) stk ! (length (aa # cs) - Suc a)) - Suc b) = stk (a, b)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
a < length []
b < length (stkss P [] stk ! (length [] - Suc a))

goal (1 subgoal):
 1. stkss P [] stk ! (length [] - Suc a) ! (length (stkss P [] stk ! (length [] - Suc a)) - Suc b) = stk (a, b)
[PROOF STEP]
by (simp add: nth_Cons')
[PROOF STATE]
proof (state)
this:
stkss P [] stk ! (length [] - Suc a) ! (length (stkss P [] stk ! (length [] - Suc a)) - Suc b) = stk (a, b)

goal (1 subgoal):
 1. \<And>aa cs. \<lbrakk>\<lbrakk>a < length cs; b < length (stkss P cs stk ! (length cs - Suc a))\<rbrakk> \<Longrightarrow> stkss P cs stk ! (length cs - Suc a) ! (length (stkss P cs stk ! (length cs - Suc a)) - Suc b) = stk (a, b); a < length (aa # cs); b < length (stkss P (aa # cs) stk ! (length (aa # cs) - Suc a))\<rbrakk> \<Longrightarrow> stkss P (aa # cs) stk ! (length (aa # cs) - Suc a) ! (length (stkss P (aa # cs) stk ! (length (aa # cs) - Suc a)) - Suc b) = stk (a, b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa cs. \<lbrakk>\<lbrakk>a < length cs; b < length (stkss P cs stk ! (length cs - Suc a))\<rbrakk> \<Longrightarrow> stkss P cs stk ! (length cs - Suc a) ! (length (stkss P cs stk ! (length cs - Suc a)) - Suc b) = stk (a, b); a < length (aa # cs); b < length (stkss P (aa # cs) stk ! (length (aa # cs) - Suc a))\<rbrakk> \<Longrightarrow> stkss P (aa # cs) stk ! (length (aa # cs) - Suc a) ! (length (stkss P (aa # cs) stk ! (length (aa # cs) - Suc a)) - Suc b) = stk (a, b)
[PROOF STEP]
case (Cons aa cs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>a < length cs; b < length (stkss P cs stk ! (length cs - Suc a))\<rbrakk> \<Longrightarrow> stkss P cs stk ! (length cs - Suc a) ! (length (stkss P cs stk ! (length cs - Suc a)) - Suc b) = stk (a, b)
a < length (aa # cs)
b < length (stkss P (aa # cs) stk ! (length (aa # cs) - Suc a))

goal (1 subgoal):
 1. \<And>aa cs. \<lbrakk>\<lbrakk>a < length cs; b < length (stkss P cs stk ! (length cs - Suc a))\<rbrakk> \<Longrightarrow> stkss P cs stk ! (length cs - Suc a) ! (length (stkss P cs stk ! (length cs - Suc a)) - Suc b) = stk (a, b); a < length (aa # cs); b < length (stkss P (aa # cs) stk ! (length (aa # cs) - Suc a))\<rbrakk> \<Longrightarrow> stkss P (aa # cs) stk ! (length (aa # cs) - Suc a) ! (length (stkss P (aa # cs) stk ! (length (aa # cs) - Suc a)) - Suc b) = stk (a, b)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a < length cs; b < length (stkss P cs stk ! (length cs - Suc a))\<rbrakk> \<Longrightarrow> stkss P cs stk ! (length cs - Suc a) ! (length (stkss P cs stk ! (length cs - Suc a)) - Suc b) = stk (a, b)
a < length (aa # cs)
b < length (stkss P (aa # cs) stk ! (length (aa # cs) - Suc a))

goal (1 subgoal):
 1. stkss P (aa # cs) stk ! (length (aa # cs) - Suc a) ! (length (stkss P (aa # cs) stk ! (length (aa # cs) - Suc a)) - Suc b) = stk (a, b)
[PROOF STEP]
by (cases aa, auto simp add: nth_Cons' rev_nth less_Suc_eq)
[PROOF STATE]
proof (state)
this:
stkss P (aa # cs) stk ! (length (aa # cs) - Suc a) ! (length (stkss P (aa # cs) stk ! (length (aa # cs) - Suc a)) - Suc b) = stk (a, b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nth_locss:
  "\<lbrakk> a < length cs; b < length (locss P cs loc ! (length cs - Suc a)) \<rbrakk>
  \<Longrightarrow> locss P cs loc ! (length cs - Suc a) ! b = loc (a,b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < length cs; b < length (locss P cs loc ! (length cs - Suc a))\<rbrakk> \<Longrightarrow> locss P cs loc ! (length cs - Suc a) ! b = loc (a, b)
[PROOF STEP]
proof (induct cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>a < length []; b < length (locss P [] loc ! (length [] - Suc a))\<rbrakk> \<Longrightarrow> locss P [] loc ! (length [] - Suc a) ! b = loc (a, b)
 2. \<And>aa cs. \<lbrakk>\<lbrakk>a < length cs; b < length (locss P cs loc ! (length cs - Suc a))\<rbrakk> \<Longrightarrow> locss P cs loc ! (length cs - Suc a) ! b = loc (a, b); a < length (aa # cs); b < length (locss P (aa # cs) loc ! (length (aa # cs) - Suc a))\<rbrakk> \<Longrightarrow> locss P (aa # cs) loc ! (length (aa # cs) - Suc a) ! b = loc (a, b)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
a < length []
b < length (locss P [] loc ! (length [] - Suc a))

goal (2 subgoals):
 1. \<lbrakk>a < length []; b < length (locss P [] loc ! (length [] - Suc a))\<rbrakk> \<Longrightarrow> locss P [] loc ! (length [] - Suc a) ! b = loc (a, b)
 2. \<And>aa cs. \<lbrakk>\<lbrakk>a < length cs; b < length (locss P cs loc ! (length cs - Suc a))\<rbrakk> \<Longrightarrow> locss P cs loc ! (length cs - Suc a) ! b = loc (a, b); a < length (aa # cs); b < length (locss P (aa # cs) loc ! (length (aa # cs) - Suc a))\<rbrakk> \<Longrightarrow> locss P (aa # cs) loc ! (length (aa # cs) - Suc a) ! b = loc (a, b)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
a < length []
b < length (locss P [] loc ! (length [] - Suc a))

goal (1 subgoal):
 1. locss P [] loc ! (length [] - Suc a) ! b = loc (a, b)
[PROOF STEP]
by (simp add: nth_Cons')
[PROOF STATE]
proof (state)
this:
locss P [] loc ! (length [] - Suc a) ! b = loc (a, b)

goal (1 subgoal):
 1. \<And>aa cs. \<lbrakk>\<lbrakk>a < length cs; b < length (locss P cs loc ! (length cs - Suc a))\<rbrakk> \<Longrightarrow> locss P cs loc ! (length cs - Suc a) ! b = loc (a, b); a < length (aa # cs); b < length (locss P (aa # cs) loc ! (length (aa # cs) - Suc a))\<rbrakk> \<Longrightarrow> locss P (aa # cs) loc ! (length (aa # cs) - Suc a) ! b = loc (a, b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa cs. \<lbrakk>\<lbrakk>a < length cs; b < length (locss P cs loc ! (length cs - Suc a))\<rbrakk> \<Longrightarrow> locss P cs loc ! (length cs - Suc a) ! b = loc (a, b); a < length (aa # cs); b < length (locss P (aa # cs) loc ! (length (aa # cs) - Suc a))\<rbrakk> \<Longrightarrow> locss P (aa # cs) loc ! (length (aa # cs) - Suc a) ! b = loc (a, b)
[PROOF STEP]
case (Cons aa cs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>a < length cs; b < length (locss P cs loc ! (length cs - Suc a))\<rbrakk> \<Longrightarrow> locss P cs loc ! (length cs - Suc a) ! b = loc (a, b)
a < length (aa # cs)
b < length (locss P (aa # cs) loc ! (length (aa # cs) - Suc a))

goal (1 subgoal):
 1. \<And>aa cs. \<lbrakk>\<lbrakk>a < length cs; b < length (locss P cs loc ! (length cs - Suc a))\<rbrakk> \<Longrightarrow> locss P cs loc ! (length cs - Suc a) ! b = loc (a, b); a < length (aa # cs); b < length (locss P (aa # cs) loc ! (length (aa # cs) - Suc a))\<rbrakk> \<Longrightarrow> locss P (aa # cs) loc ! (length (aa # cs) - Suc a) ! b = loc (a, b)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a < length cs; b < length (locss P cs loc ! (length cs - Suc a))\<rbrakk> \<Longrightarrow> locss P cs loc ! (length cs - Suc a) ! b = loc (a, b)
a < length (aa # cs)
b < length (locss P (aa # cs) loc ! (length (aa # cs) - Suc a))

goal (1 subgoal):
 1. locss P (aa # cs) loc ! (length (aa # cs) - Suc a) ! b = loc (a, b)
[PROOF STEP]
by (cases aa, auto simp: nth_Cons' (* nth_locs *) less_Suc_eq)
[PROOF STATE]
proof (state)
this:
locss P (aa # cs) loc ! (length (aa # cs) - Suc a) ! b = loc (a, b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hd_stks [simp]: "n \<noteq> 0 \<Longrightarrow> hd (stks n stk) = stk(n - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> hd (stks n stk) = stk (n - 1)
[PROOF STEP]
by (cases n, simp_all)


[STATEMENT]
lemma hd_tl_stks: "n > 1 \<Longrightarrow> hd (tl (stks n stk)) = stk(n - 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < n \<Longrightarrow> hd (tl (stks n stk)) = stk (n - 2)
[PROOF STEP]
by (cases n, auto)


[STATEMENT]
lemma stkss_purge:
  "length cs \<le> a \<Longrightarrow> stkss P cs (stk((a,b) := c)) = stkss P cs stk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length cs \<le> a \<Longrightarrow> stkss P cs (stk((a, b) := c)) = stkss P cs stk
[PROOF STEP]
by (induct cs, auto (* simp: stks_purge *))


[STATEMENT]
lemma stkss_purge':
  "length cs \<le> a \<Longrightarrow> stkss P cs (\<lambda>s. if s = (a, b) then c else stk s) = stkss P cs stk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length cs \<le> a \<Longrightarrow> stkss P cs (\<lambda>s. if s = (a, b) then c else stk s) = stkss P cs stk
[PROOF STEP]
by (fold fun_upd_def, simp only: stkss_purge)


[STATEMENT]
lemma locss_purge:
  "length cs \<le> a \<Longrightarrow> locss P cs (loc((a,b) := c)) = locss P cs loc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length cs \<le> a \<Longrightarrow> locss P cs (loc((a, b) := c)) = locss P cs loc
[PROOF STEP]
by (induct cs, auto (*simp: locs_purge *))


[STATEMENT]
lemma locss_purge':
  "length cs \<le> a \<Longrightarrow> locss P cs (\<lambda>s. if s = (a, b) then c else loc s) = locss P cs loc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length cs \<le> a \<Longrightarrow> locss P cs (\<lambda>s. if s = (a, b) then c else loc s) = locss P cs loc
[PROOF STEP]
by (fold fun_upd_def, simp only: locss_purge)


[STATEMENT]
lemma locs_pullout [simp]:
  "locs b (loc(n := e)) = (locs b loc) [n := e]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. locs b (loc(n := e)) = (locs b loc)[n := e]
[PROOF STEP]
proof (induct b)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. locs 0 (loc(n := e)) = (locs 0 loc)[n := e]
 2. \<And>b. locs b (loc(n := e)) = (locs b loc)[n := e] \<Longrightarrow> locs (Suc b) (loc(n := e)) = (locs (Suc b) loc)[n := e]
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. locs 0 (loc(n := e)) = (locs 0 loc)[n := e]
 2. \<And>b. locs b (loc(n := e)) = (locs b loc)[n := e] \<Longrightarrow> locs (Suc b) (loc(n := e)) = (locs (Suc b) loc)[n := e]
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. locs 0 (loc(n := e)) = (locs 0 loc)[n := e]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
locs 0 (loc(n := e)) = (locs 0 loc)[n := e]

goal (1 subgoal):
 1. \<And>b. locs b (loc(n := e)) = (locs b loc)[n := e] \<Longrightarrow> locs (Suc b) (loc(n := e)) = (locs (Suc b) loc)[n := e]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. locs b (loc(n := e)) = (locs b loc)[n := e] \<Longrightarrow> locs (Suc b) (loc(n := e)) = (locs (Suc b) loc)[n := e]
[PROOF STEP]
case (Suc b)
[PROOF STATE]
proof (state)
this:
locs b (loc(n := e)) = (locs b loc)[n := e]

goal (1 subgoal):
 1. \<And>b. locs b (loc(n := e)) = (locs b loc)[n := e] \<Longrightarrow> locs (Suc b) (loc(n := e)) = (locs (Suc b) loc)[n := e]
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
locs b (loc(n := e)) = (locs b loc)[n := e]

goal (1 subgoal):
 1. locs (Suc b) (loc(n := e)) = (locs (Suc b) loc)[n := e]
[PROOF STEP]
by (cases "n - b", auto simp: list_update_append not_less_eq less_Suc_eq)
[PROOF STATE]
proof (state)
this:
locs (Suc b) (loc(n := e)) = (locs (Suc b) loc)[n := e]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma locs_pullout' [simp]:
  "locs b (\<lambda>a. if a = n then e else loc (c, a)) = (locs b (\<lambda>a. loc (c, a))) [n := e]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. locs b (\<lambda>a. if a = n then e else loc (c, a)) = (locs b (\<lambda>a. loc (c, a)))[n := e]
[PROOF STEP]
by (fold fun_upd_def) simp


[STATEMENT]
lemma stks_pullout:
  "n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk) [b - Suc n := e]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk)[b - Suc n := e]
[PROOF STEP]
proof (induct b)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n < 0 \<Longrightarrow> stks 0 (stk(n := e)) = (stks 0 stk)[0 - Suc n := e]
 2. \<And>b. \<lbrakk>n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk)[b - Suc n := e]; n < Suc b\<rbrakk> \<Longrightarrow> stks (Suc b) (stk(n := e)) = (stks (Suc b) stk)[Suc b - Suc n := e]
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
n < 0

goal (2 subgoals):
 1. n < 0 \<Longrightarrow> stks 0 (stk(n := e)) = (stks 0 stk)[0 - Suc n := e]
 2. \<And>b. \<lbrakk>n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk)[b - Suc n := e]; n < Suc b\<rbrakk> \<Longrightarrow> stks (Suc b) (stk(n := e)) = (stks (Suc b) stk)[Suc b - Suc n := e]
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n < 0

goal (1 subgoal):
 1. stks 0 (stk(n := e)) = (stks 0 stk)[0 - Suc n := e]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stks 0 (stk(n := e)) = (stks 0 stk)[0 - Suc n := e]

goal (1 subgoal):
 1. \<And>b. \<lbrakk>n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk)[b - Suc n := e]; n < Suc b\<rbrakk> \<Longrightarrow> stks (Suc b) (stk(n := e)) = (stks (Suc b) stk)[Suc b - Suc n := e]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk)[b - Suc n := e]; n < Suc b\<rbrakk> \<Longrightarrow> stks (Suc b) (stk(n := e)) = (stks (Suc b) stk)[Suc b - Suc n := e]
[PROOF STEP]
case (Suc b)
[PROOF STATE]
proof (state)
this:
n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk)[b - Suc n := e]
n < Suc b

goal (1 subgoal):
 1. \<And>b. \<lbrakk>n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk)[b - Suc n := e]; n < Suc b\<rbrakk> \<Longrightarrow> stks (Suc b) (stk(n := e)) = (stks (Suc b) stk)[Suc b - Suc n := e]
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk)[b - Suc n := e]
n < Suc b

goal (1 subgoal):
 1. stks (Suc b) (stk(n := e)) = (stks (Suc b) stk)[Suc b - Suc n := e]
[PROOF STEP]
proof (cases "b = n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk)[b - Suc n := e]; n < Suc b; b = n\<rbrakk> \<Longrightarrow> stks (Suc b) (stk(n := e)) = (stks (Suc b) stk)[Suc b - Suc n := e]
 2. \<lbrakk>n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk)[b - Suc n := e]; n < Suc b; b \<noteq> n\<rbrakk> \<Longrightarrow> stks (Suc b) (stk(n := e)) = (stks (Suc b) stk)[Suc b - Suc n := e]
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b = n

goal (2 subgoals):
 1. \<lbrakk>n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk)[b - Suc n := e]; n < Suc b; b = n\<rbrakk> \<Longrightarrow> stks (Suc b) (stk(n := e)) = (stks (Suc b) stk)[Suc b - Suc n := e]
 2. \<lbrakk>n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk)[b - Suc n := e]; n < Suc b; b \<noteq> n\<rbrakk> \<Longrightarrow> stks (Suc b) (stk(n := e)) = (stks (Suc b) stk)[Suc b - Suc n := e]
[PROOF STEP]
with Suc
[PROOF STATE]
proof (chain)
picking this:
n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk)[b - Suc n := e]
n < Suc b
b = n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk)[b - Suc n := e]
n < Suc b
b = n

goal (1 subgoal):
 1. stks (Suc b) (stk(n := e)) = (stks (Suc b) stk)[Suc b - Suc n := e]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
stks (Suc b) (stk(n := e)) = (stks (Suc b) stk)[Suc b - Suc n := e]

goal (1 subgoal):
 1. \<lbrakk>n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk)[b - Suc n := e]; n < Suc b; b \<noteq> n\<rbrakk> \<Longrightarrow> stks (Suc b) (stk(n := e)) = (stks (Suc b) stk)[Suc b - Suc n := e]
[PROOF STEP]
(*      by (auto simp: stks_purge') *)
[PROOF STATE]
proof (state)
this:
stks (Suc b) (stk(n := e)) = (stks (Suc b) stk)[Suc b - Suc n := e]

goal (1 subgoal):
 1. \<lbrakk>n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk)[b - Suc n := e]; n < Suc b; b \<noteq> n\<rbrakk> \<Longrightarrow> stks (Suc b) (stk(n := e)) = (stks (Suc b) stk)[Suc b - Suc n := e]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk)[b - Suc n := e]; n < Suc b; b \<noteq> n\<rbrakk> \<Longrightarrow> stks (Suc b) (stk(n := e)) = (stks (Suc b) stk)[Suc b - Suc n := e]
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b \<noteq> n

goal (1 subgoal):
 1. \<lbrakk>n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk)[b - Suc n := e]; n < Suc b; b \<noteq> n\<rbrakk> \<Longrightarrow> stks (Suc b) (stk(n := e)) = (stks (Suc b) stk)[Suc b - Suc n := e]
[PROOF STEP]
with Suc
[PROOF STATE]
proof (chain)
picking this:
n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk)[b - Suc n := e]
n < Suc b
b \<noteq> n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n < b \<Longrightarrow> stks b (stk(n := e)) = (stks b stk)[b - Suc n := e]
n < Suc b
b \<noteq> n

goal (1 subgoal):
 1. stks (Suc b) (stk(n := e)) = (stks (Suc b) stk)[Suc b - Suc n := e]
[PROOF STEP]
by (cases "b - n") (auto intro!: nth_equalityI simp: nth_list_update)
[PROOF STATE]
proof (state)
this:
stks (Suc b) (stk(n := e)) = (stks (Suc b) stk)[Suc b - Suc n := e]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
stks (Suc b) (stk(n := e)) = (stks (Suc b) stk)[Suc b - Suc n := e]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nth_tl : "xs \<noteq> [] \<Longrightarrow> tl xs ! n = xs ! (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> tl xs ! n = xs ! Suc n
[PROOF STEP]
by (cases xs, simp_all)


[STATEMENT]
lemma f2c_Nil [simp]: "framestack_to_callstack [] = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. framestack_to_callstack [] = []
[PROOF STEP]
by (simp add: framestack_to_callstack_def)


[STATEMENT]
lemma f2c_Cons [simp]:
  "framestack_to_callstack ((stk,loc,C,M,pc)#frs) = (C,M,pc)#(framestack_to_callstack frs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. framestack_to_callstack ((stk, loc, C, M, pc) # frs) = (C, M, pc) # framestack_to_callstack frs
[PROOF STEP]
by (simp add: framestack_to_callstack_def)


[STATEMENT]
lemma f2c_length [simp]:
  "length (framestack_to_callstack frs) = length frs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (framestack_to_callstack frs) = length frs
[PROOF STEP]
by (simp add: framestack_to_callstack_def)


[STATEMENT]
lemma f2c_s2jvm_id [simp]:
  "framestack_to_callstack
    (snd(snd(state_to_jvm_state P cs s))) =
  cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. framestack_to_callstack (snd (snd (state_to_jvm_state P cs s))) = cs
[PROOF STEP]
by (cases s, simp add: framestack_to_callstack_def)


[STATEMENT]
lemma f2c_s2jvm_id' [simp]:
  "framestack_to_callstack
  (zip (stkss P cs stk) (zip (locss P cs loc) cs)) = cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. framestack_to_callstack (zip (stkss P cs stk) (zip (locss P cs loc) cs)) = cs
[PROOF STEP]
by (simp add: framestack_to_callstack_def)


[STATEMENT]
lemma f2c_append [simp]:
  "framestack_to_callstack (frs @ frs') =
  (framestack_to_callstack frs) @ (framestack_to_callstack frs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. framestack_to_callstack (frs @ frs') = framestack_to_callstack frs @ framestack_to_callstack frs'
[PROOF STEP]
by (simp add: framestack_to_callstack_def)


[STATEMENT]
lemma JVMCFG_Exit_no_sourcenode [dest]:
  assumes edge:"prog \<turnstile> (_Exit_) -et\<rightarrow> n'"
  shows "False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
have "\<lbrakk>prog \<turnstile> n -et\<rightarrow> n'; n = (_Exit_)\<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prog \<turnstile> n -et\<rightarrow> n'; n = (_Exit_)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (auto elim!: JVM_CFG.cases)
[PROOF STATE]
proof (state)
this:
\<lbrakk>prog \<turnstile> n -et\<rightarrow> n'; n = (_Exit_)\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>prog \<turnstile> ?n2 -et\<rightarrow> n'; ?n2 = (_Exit_)\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. False
[PROOF STEP]
with edge
[PROOF STATE]
proof (chain)
picking this:
prog \<turnstile> (_Exit_) -et\<rightarrow> n'
\<lbrakk>prog \<turnstile> ?n2 -et\<rightarrow> n'; ?n2 = (_Exit_)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prog \<turnstile> (_Exit_) -et\<rightarrow> n'
\<lbrakk>prog \<turnstile> ?n2 -et\<rightarrow> n'; ?n2 = (_Exit_)\<rbrakk> \<Longrightarrow> False

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma JVMCFG_Entry_no_targetnode [dest]:
  assumes edge:"prog \<turnstile> n -et\<rightarrow> (_Entry_)"
  shows "False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
fix n'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
have "\<lbrakk>prog \<turnstile> n -et\<rightarrow> n'; n' = (_Entry_)\<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prog \<turnstile> n -et\<rightarrow> n'; n' = (_Entry_)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (auto elim!: JVM_CFG.cases)
[PROOF STATE]
proof (state)
this:
\<lbrakk>prog \<turnstile> n -et\<rightarrow> n'; n' = (_Entry_)\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>prog \<turnstile> n -et\<rightarrow> ?n'2; ?n'2 = (_Entry_)\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. False
[PROOF STEP]
with edge
[PROOF STATE]
proof (chain)
picking this:
prog \<turnstile> n -et\<rightarrow> (_Entry_)
\<lbrakk>prog \<turnstile> n -et\<rightarrow> ?n'2; ?n'2 = (_Entry_)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prog \<turnstile> n -et\<rightarrow> (_Entry_)
\<lbrakk>prog \<turnstile> n -et\<rightarrow> ?n'2; ?n'2 = (_Entry_)\<rbrakk> \<Longrightarrow> False

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma JVMCFG_EntryD:
  "\<lbrakk>(P,C,M) \<turnstile> n -et\<rightarrow> n'; n = (_Entry_)\<rbrakk>
  \<Longrightarrow> (n' = (_Exit_) \<and> et = (\<lambda>s. False)\<^sub>\<surd>) \<or> (n' = (_ [(C,M,0)],None _) \<and> et = (\<lambda>s. True)\<^sub>\<surd>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P, C, M) \<turnstile> n -et\<rightarrow> n'; n = (_Entry_)\<rbrakk> \<Longrightarrow> n' = (_Exit_) \<and> et = (\<lambda>s. False)\<^sub>\<surd> \<or> n' = (_ [(C, M, 0)],None _) \<and> et = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
by (erule JVM_CFG.cases) simp_all


[STATEMENT]
lemma JVMCFG_edge_det:
  "\<lbrakk>prog \<turnstile> n -et\<rightarrow> n'; prog \<turnstile> n -et'\<rightarrow> n'\<rbrakk> \<Longrightarrow> et = et'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prog \<turnstile> n -et\<rightarrow> n'; prog \<turnstile> n -et'\<rightarrow> n'\<rbrakk> \<Longrightarrow> et = et'
[PROOF STEP]
by (erule JVM_CFG.cases, (erule JVM_CFG.cases, fastforce+)+)


[STATEMENT]
lemma "(27 :: 4 word) = -5"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 27 = - 5
[PROOF STEP]
by simp


[STATEMENT]
lemma "(27 :: 4 word) = 11"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 27 = 11
[PROOF STEP]
by simp


[STATEMENT]
lemma "27 \<noteq> (11 :: 6 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 27 \<noteq> 11
[PROOF STEP]
by simp


[STATEMENT]
lemma "(127 :: 6 word) = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 127 = - 1
[PROOF STEP]
by simp


[STATEMENT]
lemma "word_pred 2 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_pred 2 = 1
[PROOF STEP]
by simp


[STATEMENT]
lemma "word_succ (- 3) = -2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_succ (- 3) = - 2
[PROOF STEP]
by simp


[STATEMENT]
lemma "23 < (27::8 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 23 < 27
[PROOF STEP]
by simp


[STATEMENT]
lemma "23 \<le> (27::8 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 23 \<le> 27
[PROOF STEP]
by simp


[STATEMENT]
lemma "\<not> 23 < (27::2 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 23 < 27
[PROOF STEP]
by simp


[STATEMENT]
lemma "0 < (4::3 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 4
[PROOF STEP]
by simp


[STATEMENT]
lemma "1 < (4::3 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < 4
[PROOF STEP]
by simp


[STATEMENT]
lemma "0 < (1::3 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1
[PROOF STEP]
by simp


[STATEMENT]
lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + 2 * b + c - b = b + c + a
[PROOF STEP]
by simp


[STATEMENT]
lemma "uint (234567 :: 10 word) = 71"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uint 234567 = 71
[PROOF STEP]
by simp


[STATEMENT]
lemma "uint (-234567 :: 10 word) = 953"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uint (- 234567) = 953
[PROOF STEP]
by simp


[STATEMENT]
lemma "sint (234567 :: 10 word) = 71"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sint 234567 = 71
[PROOF STEP]
by simp


[STATEMENT]
lemma "sint (-234567 :: 10 word) = -71"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sint (- 234567) = - 71
[PROOF STEP]
by simp


[STATEMENT]
lemma "uint (1 :: 10 word) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uint 1 = 1
[PROOF STEP]
by simp


[STATEMENT]
lemma "unat (-234567 :: 10 word) = 953"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat (- 234567) = 953
[PROOF STEP]
by simp


[STATEMENT]
lemma "unat (1 :: 10 word) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat 1 = 1
[PROOF STEP]
by simp


[STATEMENT]
lemma "ucast (0b1010 :: 4 word) = (0b10 :: 2 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ucast 10 = 2
[PROOF STEP]
by simp


[STATEMENT]
lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ucast 10 = 10
[PROOF STEP]
by simp


[STATEMENT]
lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scast 10 = 58
[PROOF STEP]
by simp


[STATEMENT]
lemma "ucast (1 :: 4 word) = (1 :: 2 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ucast 1 = 1
[PROOF STEP]
by simp


[STATEMENT]
lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < x \<Longrightarrow> i < i + 1
[PROOF STEP]
by unat_arith


[STATEMENT]
lemma "0b110 AND 0b101 = (0b100 :: 32 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 6 AND 5 = 4
[PROOF STEP]
by simp


[STATEMENT]
lemma "0b110 OR 0b011 = (0b111 :: 8 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 6 OR 3 = 7
[PROOF STEP]
by simp


[STATEMENT]
lemma "0xF0 XOR 0xFF = (0x0F :: 8 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 240 XOR 255 = 15
[PROOF STEP]
by simp


[STATEMENT]
lemma "NOT (0xF0 :: 16 word) = 0xFF0F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NOT 240 = 65295
[PROOF STEP]
by simp


[STATEMENT]
lemma "0 AND 5 = (0 :: 8 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 AND 5 = 0
[PROOF STEP]
by simp


[STATEMENT]
lemma "1 AND 1 = (1 :: 8 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 AND 1 = 1
[PROOF STEP]
by simp


[STATEMENT]
lemma "1 AND 0 = (0 :: 8 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 AND 0 = 0
[PROOF STEP]
by simp


[STATEMENT]
lemma "1 AND 5 = (1 :: 8 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 AND 5 = 1
[PROOF STEP]
by simp


[STATEMENT]
lemma "1 OR 6 = (7 :: 8 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 OR 6 = 7
[PROOF STEP]
by simp


[STATEMENT]
lemma "1 OR 1 = (1 :: 8 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 OR 1 = 1
[PROOF STEP]
by simp


[STATEMENT]
lemma "1 XOR 7 = (6 :: 8 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 XOR 7 = 6
[PROOF STEP]
by simp


[STATEMENT]
lemma "1 XOR 1 = (0 :: 8 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 XOR 1 = 0
[PROOF STEP]
by simp


[STATEMENT]
lemma "NOT 1 = (254 :: 8 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NOT 1 = 254
[PROOF STEP]
by simp


[STATEMENT]
lemma "NOT 0 = (255 :: 8 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NOT 0 = 255
[PROOF STEP]
by simp


[STATEMENT]
lemma "(-1 :: 32 word) = 0xFFFFFFFF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - 1 = 4294967295
[PROOF STEP]
by simp


[STATEMENT]
lemma "bit (0b0010 :: 4 word) 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit 2 1
[PROOF STEP]
by simp


[STATEMENT]
lemma "\<not> bit (0b0010 :: 4 word) 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> bit 2 0
[PROOF STEP]
by simp


[STATEMENT]
lemma "\<not> bit (0b1000 :: 3 word) 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> bit 8 4
[PROOF STEP]
by simp


[STATEMENT]
lemma "\<not> bit (1 :: 3 word) 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> bit 1 2
[PROOF STEP]
by simp


[STATEMENT]
lemma "bit (0b11000 :: 10 word) n = (n = 4 \<or> n = 3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit 24 n = (n = 4 \<or> n = 3)
[PROOF STEP]
by (auto simp add: bit_numeral_rec bit_1_iff split: nat.splits)


[STATEMENT]
lemma "set_bit 55 7 True = (183::'a::len word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit 55 7 True = 183
[PROOF STEP]
by simp


[STATEMENT]
lemma "set_bit 0b0010 7 True = (0b10000010::'a::len word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit 2 7 True = 130
[PROOF STEP]
by simp


[STATEMENT]
lemma "set_bit 0b0010 1 False = (0::'a::len word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit 2 1 False = 0
[PROOF STEP]
by simp


[STATEMENT]
lemma "set_bit 1 3 True = (0b1001::'a::len word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit 1 3 True = 9
[PROOF STEP]
by simp


[STATEMENT]
lemma "set_bit 1 0 False = (0::'a::len word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit 1 0 False = 0
[PROOF STEP]
by simp


[STATEMENT]
lemma "set_bit 0 3 True = (0b1000::'a::len word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit 0 3 True = 8
[PROOF STEP]
by simp


[STATEMENT]
lemma "set_bit 0 3 False = (0::'a::len word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit 0 3 False = 0
[PROOF STEP]
by simp


[STATEMENT]
lemma "odd (0b0101::'a::len word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd 5
[PROOF STEP]
by simp


[STATEMENT]
lemma "even (0b1000::'a::len word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even 8
[PROOF STEP]
by simp


[STATEMENT]
lemma "odd (1::'a::len word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd 1
[PROOF STEP]
by simp


[STATEMENT]
lemma "even (0::'a::len word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even 0
[PROOF STEP]
by simp


[STATEMENT]
lemma "\<not> msb (0b0101::4 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> msb 5
[PROOF STEP]
by simp


[STATEMENT]
lemma   "msb (0b1000::4 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. msb 8
[PROOF STEP]
by simp


[STATEMENT]
lemma "\<not> msb (1::4 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> msb 1
[PROOF STEP]
by simp


[STATEMENT]
lemma "\<not> msb (0::4 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> msb 0
[PROOF STEP]
by simp


[STATEMENT]
lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::len word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_cat 27 27 = 2843
[PROOF STEP]
by simp


[STATEMENT]
lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_cat 3 15 = 207
[PROOF STEP]
by simp


[STATEMENT]
lemma "0b1011 << 2 = (0b101100::'a::len word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 11 << 2 = 44
[PROOF STEP]
by simp


[STATEMENT]
lemma "0b1011 >> 2 = (0b10::8 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 11 >> 2 = 2
[PROOF STEP]
by simp


[STATEMENT]
lemma "0b1011 >>> 2 = (0b10::8 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 11 >>> 2 = 2
[PROOF STEP]
by simp


[STATEMENT]
lemma "1 << 2 = (0b100::'a::len word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 << 2 = 4
[PROOF STEP]
apply simp?
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
oops


[STATEMENT]
lemma "slice 3 (0b101111::6 word) = (0b101::3 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slice 3 47 = 5
[PROOF STEP]
by simp


[STATEMENT]
lemma "slice 3 (1::6 word) = (0::3 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slice 3 1 = 0
[PROOF STEP]
apply simp?
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slice 3 1 = 0
[PROOF STEP]
oops


[STATEMENT]
lemma "word_rotr 2 0b0110 = (0b1001::4 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_rotr 2 6 = 9
[PROOF STEP]
by simp


[STATEMENT]
lemma "word_rotl 1 0b1110 = (0b1101::4 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_rotl 1 14 = 13
[PROOF STEP]
by simp


[STATEMENT]
lemma "word_roti 2 0b1110 = (0b1011::4 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_roti 2 14 = 11
[PROOF STEP]
by simp


[STATEMENT]
lemma "word_roti (- 2) 0b0110 = (0b1001::4 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_roti (- 2) 6 = 9
[PROOF STEP]
by simp


[STATEMENT]
lemma "word_rotr 2 0 = (0::4 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_rotr 2 0 = 0
[PROOF STEP]
by simp


[STATEMENT]
lemma "word_rotr 2 1 = (0b0100::4 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_rotr 2 1 = 4
[PROOF STEP]
apply simp?
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_rotr 2 1 = 4
[PROOF STEP]
oops


[STATEMENT]
lemma "word_rotl 2 1 = (0b0100::4 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_rotl 2 1 = 4
[PROOF STEP]
apply simp?
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_rotl 2 1 = 4
[PROOF STEP]
oops


[STATEMENT]
lemma "word_roti (- 2) 1 = (0b0100::4 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_roti (- 2) 1 = 4
[PROOF STEP]
apply simp?
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_rotl 2 1 = 4
[PROOF STEP]
oops


[STATEMENT]
lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x AND 65280 OR x AND 255 = x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x AND 65280 OR x AND 255 = x
[PROOF STEP]
have "(x AND 0xff00) OR (x AND 0x00ff) = x AND (0xff00 OR 0x00ff)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x AND 65280 OR x AND 255 = x AND (65280 OR 255)
[PROOF STEP]
by (simp only: word_ao_dist2)
[PROOF STATE]
proof (state)
this:
x AND 65280 OR x AND 255 = x AND (65280 OR 255)

goal (1 subgoal):
 1. x AND 65280 OR x AND 255 = x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x AND 65280 OR x AND 255 = x AND (65280 OR 255)

goal (1 subgoal):
 1. x AND 65280 OR x AND 255 = x
[PROOF STEP]
have "0xff00 OR 0x00ff = (-1::16 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 65280 OR 255 = - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
65280 OR 255 = - 1

goal (1 subgoal):
 1. x AND 65280 OR x AND 255 = x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
65280 OR 255 = - 1

goal (1 subgoal):
 1. x AND 65280 OR x AND 255 = x
[PROOF STEP]
have "x AND -1 = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x AND - 1 = x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x AND - 1 = x

goal (1 subgoal):
 1. x AND 65280 OR x AND 255 = x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x AND 65280 OR x AND 255 = x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x AND 65280 OR x AND 255 = x

goal (1 subgoal):
 1. x AND 65280 OR x AND 255 = x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x AND 65280 OR x AND 255 = x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "word_next (255:: 8 word) = 255"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_next 255 = 255
[PROOF STEP]
by eval


[STATEMENT]
lemma "word_prev (2:: 8 word) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_prev 2 = 1
[PROOF STEP]
by eval


[STATEMENT]
lemma "word_prev (0:: 8 word) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_prev 0 = 0
[PROOF STEP]
by eval


[STATEMENT]
lemma "1 < (1024::32 word) \<and> 1 \<le> (1024::32 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < 1024 \<and> 1 \<le> 1024
[PROOF STEP]
by simp


[STATEMENT]
lemma "of_bl [True, False, True, True] = (0b1011::'a::len word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl [True, False, True, True] = 11
[PROOF STEP]
by simp


[STATEMENT]
lemma "to_bl (0b110::4 word) = [False, True, True, False]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl 6 = [False, True, True, False]
[PROOF STEP]
by simp


[STATEMENT]
lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl (replicate 32 True) = 4294967295
[PROOF STEP]
by (simp add: numeral_eq_Suc)


[STATEMENT]
lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x AND 65280 OR x AND 255 = x
[PROOF STEP]
by word_bitwise


[STATEMENT]
lemma "(x AND NOT 3) >> 4 << 2 = ((x >> 2) AND NOT 3)"
  for x :: "10 word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x AND NOT 3 >> 4 << 2 = (x >> 2) AND NOT 3
[PROOF STEP]
by word_bitwise


[STATEMENT]
lemma "((x AND -8) >> 3) AND 7 = (x AND 56) >> 3"
  for x :: "12 word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x AND - 8 >> 3) AND 7 = x AND 56 >> 3
[PROOF STEP]
by word_bitwise


[STATEMENT]
lemma "x \<le> 42 \<Longrightarrow> x \<le> 89"
  for x :: "8 word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> 42 \<Longrightarrow> x \<le> 89
[PROOF STEP]
apply word_bitwise
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> bit x 7 \<and> \<not> bit x 6 \<and> (bit x 5 \<longrightarrow> \<not> bit x 4 \<and> (bit x 3 \<longrightarrow> \<not> bit x 2 \<and> (bit x 1 \<longrightarrow> \<not> bit x 0))) \<Longrightarrow> \<not> bit x 7 \<and> (bit x 6 \<longrightarrow> \<not> bit x 5 \<and> (bit x 3 \<longrightarrow> bit x 4 \<longrightarrow> \<not> bit x 2 \<and> \<not> bit x 1))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "(x AND 1023) = 0 \<Longrightarrow> x \<le> -1024"
  for x :: \<open>32 word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x AND 1023 = 0 \<Longrightarrow> x \<le> - 1024
[PROOF STEP]
apply word_bitwise
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> bit x 0 \<and> \<not> bit x 1 \<and> \<not> bit x 2 \<and> \<not> bit x 3 \<and> \<not> bit x 4 \<and> \<not> bit x 5 \<and> \<not> bit x 6 \<and> \<not> bit x 7 \<and> \<not> bit x 8 \<and> \<not> bit x 9 \<Longrightarrow> bit x 10 \<longrightarrow> bit x 11 \<longrightarrow> bit x 12 \<longrightarrow> bit x 13 \<longrightarrow> bit x 14 \<longrightarrow> bit x 15 \<longrightarrow> bit x 16 \<longrightarrow> bit x 17 \<longrightarrow> bit x 18 \<longrightarrow> bit x 19 \<longrightarrow> bit x 20 \<longrightarrow> bit x 21 \<longrightarrow> bit x 22 \<longrightarrow> bit x 23 \<longrightarrow> bit x 24 \<longrightarrow> bit x 25 \<longrightarrow> bit x 26 \<longrightarrow> bit x 27 \<longrightarrow> bit x 28 \<longrightarrow> bit x 29 \<longrightarrow> bit x 30 \<longrightarrow> bit x 31 \<longrightarrow> \<not> bit x 9 \<and> \<not> bit x 8 \<and> \<not> bit x 7 \<and> \<not> bit x 6 \<and> \<not> bit x 5 \<and> \<not> bit x 4 \<and> \<not> bit x 3 \<and> \<not> bit x 2 \<and> \<not> bit x 1 \<and> \<not> bit x 0
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma shiftr_overflow: "32 \<le> a \<Longrightarrow> b >> a = 0"
  for b :: \<open>32 word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 32 \<le> a \<Longrightarrow> b >> a = 0
[PROOF STEP]
apply word_bitwise
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 32 \<le> a \<Longrightarrow> takefill False (Suc (Suc (Suc (Suc 28)))) (drop a [bit b 0, bit b 1, bit b 2, bit b 3, bit b 4, bit b 5, bit b 6, bit b 7, bit b 8, bit b 9, bit b 10, bit b 11, bit b 12, bit b 13, bit b 14, bit b 15, bit b 16, bit b 17, bit b 18, bit b 19, bit b 20, bit b 21, bit b 22, bit b 23, bit b 24, bit b 25, bit b 26, bit b 27, bit b 28, bit b 29, bit b 30, bit b 31]) = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False]
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "((x :: 32 word) >> 3) AND 7 = (x AND 56) >> 3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x >> 3) AND 7 = x AND 56 >> 3
[PROOF STEP]
by word_bitwise


[STATEMENT]
lemma Show_Read_bool_id: \<open>STR_is_bool s \<Longrightarrow> (Show\<^sub>b\<^sub>o\<^sub>o\<^sub>l (Read\<^sub>b\<^sub>o\<^sub>o\<^sub>l s) = s)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. STR_is_bool s \<Longrightarrow> Show\<^sub>b\<^sub>o\<^sub>o\<^sub>l (Read\<^sub>b\<^sub>o\<^sub>o\<^sub>l s) = s
[PROOF STEP]
using STR_is_bool_def
[PROOF STATE]
proof (prove)
using this:
STR_is_bool ?s = (Show\<^sub>b\<^sub>o\<^sub>o\<^sub>l (Read\<^sub>b\<^sub>o\<^sub>o\<^sub>l ?s) = ?s)

goal (1 subgoal):
 1. STR_is_bool s \<Longrightarrow> Show\<^sub>b\<^sub>o\<^sub>o\<^sub>l (Read\<^sub>b\<^sub>o\<^sub>o\<^sub>l s) = s
[PROOF STEP]
by fastforce


[STATEMENT]
lemma STR_is_bool_split: \<open>STR_is_bool s \<Longrightarrow> s = ''False'' \<or> s = ''True''\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. STR_is_bool s \<Longrightarrow> s = ''False'' \<or> s = ''True''
[PROOF STEP]
by(auto simp: STR_is_bool_def Read\<^sub>b\<^sub>o\<^sub>o\<^sub>l_def Show\<^sub>b\<^sub>o\<^sub>o\<^sub>l_def)


[STATEMENT]
lemma Read_Show_bool_id: \<open>Read\<^sub>b\<^sub>o\<^sub>o\<^sub>l (Show\<^sub>b\<^sub>o\<^sub>o\<^sub>l b) = b\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Read\<^sub>b\<^sub>o\<^sub>o\<^sub>l (Show\<^sub>b\<^sub>o\<^sub>o\<^sub>l b) = b
[PROOF STEP]
by(auto simp: Read\<^sub>b\<^sub>o\<^sub>o\<^sub>l_def Show\<^sub>b\<^sub>o\<^sub>o\<^sub>l_def)


[STATEMENT]
lemma Show_Read_bool'_id: \<open>strL_is_bool' s \<Longrightarrow> (ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l (ReadL\<^sub>b\<^sub>o\<^sub>o\<^sub>l s) = s)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strL_is_bool' s \<Longrightarrow> \<lceil>\<lfloor>s\<rfloor>\<rceil> = s
[PROOF STEP]
using strL_is_bool'_def
[PROOF STATE]
proof (prove)
using this:
strL_is_bool' ?s = (\<lceil>\<lfloor>?s\<rfloor>\<rceil> = ?s)

goal (1 subgoal):
 1. strL_is_bool' s \<Longrightarrow> \<lceil>\<lfloor>s\<rfloor>\<rceil> = s
[PROOF STEP]
by fastforce


[STATEMENT]
lemma strL_is_bool'_split:  \<open>strL_is_bool' s \<Longrightarrow> s = STR ''False'' \<or> s = STR ''True''\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strL_is_bool' s \<Longrightarrow> s = STR ''False'' \<or> s = STR ''True''
[PROOF STEP]
by(auto simp: strL_is_bool'_def ReadL\<^sub>b\<^sub>o\<^sub>o\<^sub>l_def ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l_def)


[STATEMENT]
lemma Read_Show_bool'_id: \<open>ReadL\<^sub>b\<^sub>o\<^sub>o\<^sub>l (ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l b) = b\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lceil>b\<rceil>\<rfloor> = b
[PROOF STEP]
by(auto simp: ReadL\<^sub>b\<^sub>o\<^sub>o\<^sub>l_def ShowL\<^sub>b\<^sub>o\<^sub>o\<^sub>l_def)


[STATEMENT]
lemma nat_of_digit_digit_of_nat_id:
    \<open>x < 10 \<Longrightarrow> nat_of_digit (digit_of_nat x) = x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < 10 \<Longrightarrow> nat_of_digit (digit_of_nat x) = x
[PROOF STEP]
by(simp add:nat_of_digit_def digit_of_nat_def)


[STATEMENT]
lemma img_digit_of_nat:
\<open>n < 10 \<Longrightarrow> digit_of_nat n \<in> {CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'',
                              CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9''}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < 10 \<Longrightarrow> digit_of_nat n \<in> {CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9''}
[PROOF STEP]
by(simp add:nat_of_digit_def digit_of_nat_def)


[STATEMENT]
lemma digit_of_nat_nat_of_digit_id:
    \<open>c \<in> {CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'',
          CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9''}
      \<Longrightarrow> digit_of_nat (nat_of_digit c) = c\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<in> {CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9''} \<Longrightarrow> digit_of_nat (nat_of_digit c) = c
[PROOF STEP]
by(code_simp, auto)


[STATEMENT]
lemma nat_explode'_not_empty: \<open>nat_explode' n \<noteq> []\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_explode' n \<noteq> []
[PROOF STEP]
by (smt (z3) list.simps(3) nat_explode'.simps)


[STATEMENT]
lemma nat_explode_not_empty: \<open>nat_explode n \<noteq> []\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_explode n \<noteq> []
[PROOF STEP]
using nat_explode'_not_empty nat_explode_def
[PROOF STATE]
proof (prove)
using this:
nat_explode' ?n \<noteq> []
nat_explode ?x = rev (nat_explode' ?x)

goal (1 subgoal):
 1. nat_explode n \<noteq> []
[PROOF STEP]
by auto


[STATEMENT]
lemma nat_explode'_ne_suc: \<open>\<exists> n. nat_explode' (Suc n) \<noteq> nat_explode' n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. nat_explode' (Suc n) \<noteq> nat_explode' n
[PROOF STEP]
by(rule exI [of _ \<open>0::nat\<close>], simp)


[STATEMENT]
lemma nat_explode'_digit: \<open>hd (nat_explode' n ) < 10\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (nat_explode' n) < 10
[PROOF STEP]
proof(induct  \<open>n\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. hd (nat_explode' 0) < 10
 2. \<And>n. hd (nat_explode' n) < 10 \<Longrightarrow> hd (nat_explode' (Suc n)) < 10
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. hd (nat_explode' 0) < 10
 2. \<And>n. hd (nat_explode' n) < 10 \<Longrightarrow> hd (nat_explode' (Suc n)) < 10
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (nat_explode' 0) < 10
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hd (nat_explode' 0) < 10

goal (1 subgoal):
 1. \<And>n. hd (nat_explode' n) < 10 \<Longrightarrow> hd (nat_explode' (Suc n)) < 10
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. hd (nat_explode' n) < 10 \<Longrightarrow> hd (nat_explode' (Suc n)) < 10
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
hd (nat_explode' n) < 10

goal (1 subgoal):
 1. \<And>n. hd (nat_explode' n) < 10 \<Longrightarrow> hd (nat_explode' (Suc n)) < 10
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd (nat_explode' n) < 10
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
hd (nat_explode' n) < 10

goal (1 subgoal):
 1. hd (nat_explode' (Suc n)) < 10
[PROOF STEP]
proof (cases \<open>n < 9\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>hd (nat_explode' n) < 10; n < 9\<rbrakk> \<Longrightarrow> hd (nat_explode' (Suc n)) < 10
 2. \<lbrakk>hd (nat_explode' n) < 10; \<not> n < 9\<rbrakk> \<Longrightarrow> hd (nat_explode' (Suc n)) < 10
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n < 9

goal (2 subgoals):
 1. \<lbrakk>hd (nat_explode' n) < 10; n < 9\<rbrakk> \<Longrightarrow> hd (nat_explode' (Suc n)) < 10
 2. \<lbrakk>hd (nat_explode' n) < 10; \<not> n < 9\<rbrakk> \<Longrightarrow> hd (nat_explode' (Suc n)) < 10
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n < 9
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n < 9

goal (1 subgoal):
 1. hd (nat_explode' (Suc n)) < 10
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hd (nat_explode' (Suc n)) < 10

goal (1 subgoal):
 1. \<lbrakk>hd (nat_explode' n) < 10; \<not> n < 9\<rbrakk> \<Longrightarrow> hd (nat_explode' (Suc n)) < 10
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>hd (nat_explode' n) < 10; \<not> n < 9\<rbrakk> \<Longrightarrow> hd (nat_explode' (Suc n)) < 10
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> n < 9

goal (1 subgoal):
 1. \<lbrakk>hd (nat_explode' n) < 10; \<not> n < 9\<rbrakk> \<Longrightarrow> hd (nat_explode' (Suc n)) < 10
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> n < 9
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> n < 9

goal (1 subgoal):
 1. hd (nat_explode' (Suc n)) < 10
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hd (nat_explode' (Suc n)) < 10

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
hd (nat_explode' (Suc n)) < 10

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma div_ten_less: \<open>n \<noteq> 0 \<Longrightarrow> ((n::nat) div 10) < n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> n div 10 < n
[PROOF STEP]
by simp


[STATEMENT]
lemma unroll_nat_explode':
 \<open>\<not> n < 10 \<Longrightarrow> (case n < 10 of True \<Rightarrow> [n mod 10] | False \<Rightarrow> n mod 10 # nat_explode' (n div 10)) =
       (n mod 10 # nat_explode' (n div 10))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> n < 10 \<Longrightarrow> (case n < 10 of True \<Rightarrow> [n mod 10] | False \<Rightarrow> n mod 10 # nat_explode' (n div 10)) = n mod 10 # nat_explode' (n div 10)
[PROOF STEP]
by simp


[STATEMENT]
lemma nat_explode_mod_10_ident: \<open>map (\<lambda> x. x mod 10) (nat_explode' n) = nat_explode' n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>x. x mod 10) (nat_explode' n) = nat_explode' n
[PROOF STEP]
proof (cases \<open>n < 10\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n < 10 \<Longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' n) = nat_explode' n
 2. \<not> n < 10 \<Longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' n) = nat_explode' n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n < 10

goal (2 subgoals):
 1. n < 10 \<Longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' n) = nat_explode' n
 2. \<not> n < 10 \<Longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' n) = nat_explode' n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n < 10
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n < 10

goal (1 subgoal):
 1. map (\<lambda>x. x mod 10) (nat_explode' n) = nat_explode' n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map (\<lambda>x. x mod 10) (nat_explode' n) = nat_explode' n

goal (1 subgoal):
 1. \<not> n < 10 \<Longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' n) = nat_explode' n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> n < 10 \<Longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' n) = nat_explode' n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> n < 10

goal (1 subgoal):
 1. \<not> n < 10 \<Longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' n) = nat_explode' n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> n < 10
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> n < 10

goal (1 subgoal):
 1. map (\<lambda>x. x mod 10) (nat_explode' n) = nat_explode' n
[PROOF STEP]
proof (induct \<open>n\<close> rule: nat_less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. \<not> m < 10 \<longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' m) = nat_explode' m; \<not> n < 10\<rbrakk> \<Longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' n) = nat_explode' n
[PROOF STEP]
case (1 n)
[PROOF STATE]
proof (state)
this:
\<forall>m<n. \<not> m < 10 \<longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' m) = nat_explode' m
\<not> n < 10

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. \<not> m < 10 \<longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' m) = nat_explode' m; \<not> n < 10\<rbrakk> \<Longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' n) = nat_explode' n
[PROOF STEP]
note * = this
[PROOF STATE]
proof (state)
this:
\<forall>m<n. \<not> m < 10 \<longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' m) = nat_explode' m
\<not> n < 10

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. \<not> m < 10 \<longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' m) = nat_explode' m; \<not> n < 10\<rbrakk> \<Longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' n) = nat_explode' n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>m<n. \<not> m < 10 \<longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' m) = nat_explode' m
\<not> n < 10
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>m<n. \<not> m < 10 \<longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' m) = nat_explode' m
\<not> n < 10

goal (1 subgoal):
 1. map (\<lambda>x. x mod 10) (nat_explode' n) = nat_explode' n
[PROOF STEP]
using div_ten_less
[PROOF STATE]
proof (prove)
using this:
\<forall>m<n. \<not> m < 10 \<longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' m) = nat_explode' m
\<not> n < 10
?n \<noteq> 0 \<Longrightarrow> ?n div 10 < ?n

goal (1 subgoal):
 1. map (\<lambda>x. x mod 10) (nat_explode' n) = nat_explode' n
[PROOF STEP]
apply(simp (no_asm))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. \<not> m < 10 \<longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' m) = nat_explode' m; \<not> n < 10; \<And>n. n \<noteq> 0 \<Longrightarrow> n div 10 < n\<rbrakk> \<Longrightarrow> map (\<lambda>x. x mod 10) (case n < 10 of True \<Rightarrow> [n mod 10] | False \<Rightarrow> n mod 10 # nat_explode' (n div 10)) = (case n < 10 of True \<Rightarrow> [n mod 10] | False \<Rightarrow> n mod 10 # nat_explode' (n div 10))
[PROOF STEP]
using unroll_nat_explode'[of n] *
[PROOF STATE]
proof (prove)
using this:
\<not> n < 10 \<Longrightarrow> (case n < 10 of True \<Rightarrow> [n mod 10] | False \<Rightarrow> n mod 10 # nat_explode' (n div 10)) = n mod 10 # nat_explode' (n div 10)
\<forall>m<n. \<not> m < 10 \<longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' m) = nat_explode' m
\<not> n < 10

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. \<not> m < 10 \<longrightarrow> map (\<lambda>x. x mod 10) (nat_explode' m) = nat_explode' m; \<not> n < 10; \<And>n. n \<noteq> 0 \<Longrightarrow> n div 10 < n\<rbrakk> \<Longrightarrow> map (\<lambda>x. x mod 10) (case n < 10 of True \<Rightarrow> [n mod 10] | False \<Rightarrow> n mod 10 # nat_explode' (n div 10)) = (case n < 10 of True \<Rightarrow> [n mod 10] | False \<Rightarrow> n mod 10 # nat_explode' (n div 10))
[PROOF STEP]
by (smt (z3) list.simps(8) list.simps(9) mod_div_trivial mod_eq_self_iff_div_eq_0
                 nat_explode'.simps zero_less_numeral)
[PROOF STATE]
proof (state)
this:
map (\<lambda>x. x mod 10) (nat_explode' n) = nat_explode' n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
map (\<lambda>x. x mod 10) (nat_explode' n) = nat_explode' n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nat_explode'_digits: \<open>\<forall> d \<in> set (nat_explode' n). d < 10\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>d\<in>set (nat_explode' n). d < 10
[PROOF STEP]
using image_set[of \<open>(\<lambda> x. x mod 10)\<close> \<open>(nat_explode' n)\<close>]
        nat_explode_mod_10_ident[symmetric]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. x mod 10) ` set (nat_explode' n) = set (map (\<lambda>x. x mod 10) (nat_explode' n))
nat_explode' ?n = map (\<lambda>x. x mod 10) (nat_explode' ?n)

goal (1 subgoal):
 1. \<forall>d\<in>set (nat_explode' n). d < 10
[PROOF STEP]
by (metis (no_types, lifting) Euclidean_Division.div_eq_0_iff
                                imageE mod_div_trivial zero_neq_numeral)


[STATEMENT]
lemma nat_explode_digits: \<open>\<forall> d \<in> set (nat_explode n). d < 10\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>d\<in>set (nat_explode n). d < 10
[PROOF STEP]
using nat_explode_def set_rev
[PROOF STATE]
proof (prove)
using this:
nat_explode ?x = rev (nat_explode' ?x)
set (rev ?xs) = set ?xs

goal (1 subgoal):
 1. \<forall>d\<in>set (nat_explode n). d < 10
[PROOF STEP]
by (metis nat_explode'_digits)


[STATEMENT]
lemma nat_implode_append:
 \<open>nat_implode (a@[b]) = (1*b + foldr (+) (map (\<lambda>(p, y). 10 ^ p * y) (enumerate (Suc 0) (rev a))) 0 )\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_implode (a @ [b]) = (1::'a) * b + foldr (+) (map (\<lambda>(p, y). (10::'a) ^ p * y) (enumerate (Suc 0) (rev a))) (0::'a)
[PROOF STEP]
by(simp add:nat_implode_def)