[STATEMENT]
lemma tm_onestroke_induct_halts: "\<exists> stp. is_final (steps0 (1, [], <nl:: nat list>) tm_onestroke stp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>stp. is_final (steps0 (1, [], <nl>) tm_onestroke stp)
[PROOF STEP]
proof (induct rule: measure_tm_onestroke_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>stp. \<not> is_final (steps0 (1, [], <nl>) tm_onestroke stp) \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
case (Step stp)
[PROOF STATE]
proof (state)
this:
\<not> is_final (steps0 (1, [], <nl>) tm_onestroke stp)

goal (1 subgoal):
 1. \<And>stp. \<not> is_final (steps0 (1, [], <nl>) tm_onestroke stp) \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> is_final (steps0 (1, [], <nl>) tm_onestroke stp)
[PROOF STEP]
have "\<not>is_final (steps0 (1, [], <nl>) tm_onestroke stp)"
[PROOF STATE]
proof (prove)
using this:
\<not> is_final (steps0 (1, [], <nl>) tm_onestroke stp)

goal (1 subgoal):
 1. \<not> is_final (steps0 (1, [], <nl>) tm_onestroke stp)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<not> is_final (steps0 (1, [], <nl>) tm_onestroke stp)

goal (1 subgoal):
 1. \<And>stp. \<not> is_final (steps0 (1, [], <nl>) tm_onestroke stp) \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
have "inv_tm_onestroke (steps0 (1, [], <nl>) tm_onestroke stp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_tm_onestroke (steps0 (1, [], <nl>) tm_onestroke stp)
[PROOF STEP]
proof (rule_tac inv_tm_onestroke_steps)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv_tm_onestroke (1, [], <nl>)
[PROOF STEP]
show "inv_tm_onestroke (1, [], <nl>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_tm_onestroke (1, [], <nl>)
[PROOF STEP]
by (auto simp add: noDblBk_tape_of_nat_list)
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (1, [], <nl>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (steps0 (1, [], <nl>) tm_onestroke stp)

goal (1 subgoal):
 1. \<And>stp. \<not> is_final (steps0 (1, [], <nl>) tm_onestroke stp) \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
show "(steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp)
         \<in> measure_tm_onestroke"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
proof (cases "steps0 (1, [], <nl>) tm_onestroke stp")
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c. steps0 (1, [], <nl>) tm_onestroke stp = (a, b, c) \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
case (fields s l r)
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)

goal (1 subgoal):
 1. \<And>a b c. steps0 (1, [], <nl>) tm_onestroke stp = (a, b, c) \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
[PROOF STEP]
have cf_cases: "steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)

goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)

goal (1 subgoal):
 1. \<And>a b c. steps0 (1, [], <nl>) tm_onestroke stp = (a, b, c) \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
proof (rule tm_onestroke_cases)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. inv_tm_onestroke (?s, ?l, ?r)
 2. ?s = 0 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 3. ?s = 1 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 4. ?s = 2 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 5. ?s = 3 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
from \<open>inv_tm_onestroke (steps0 (1, [], <nl>) tm_onestroke stp)\<close> and cf_cases
[PROOF STATE]
proof (chain)
picking this:
inv_tm_onestroke (steps0 (1, [], <nl>) tm_onestroke stp)
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
[PROOF STEP]
show "inv_tm_onestroke (s, l, r)"
[PROOF STATE]
proof (prove)
using this:
inv_tm_onestroke (steps0 (1, [], <nl>) tm_onestroke stp)
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)

goal (1 subgoal):
 1. inv_tm_onestroke (s, l, r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv_tm_onestroke (s, l, r)

goal (4 subgoals):
 1. s = 0 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. s = 1 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 3. s = 2 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 4. s = 3 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. s = 0 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. s = 1 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 3. s = 2 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 4. s = 3 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
assume "s=0"
[PROOF STATE]
proof (state)
this:
s = 0

goal (4 subgoals):
 1. s = 0 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. s = 1 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 3. s = 2 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 4. s = 3 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with cf_cases \<open>\<not>is_final (steps0 (1, [], <nl>) tm_onestroke stp)\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
\<not> is_final (steps0 (1, [], <nl>) tm_onestroke stp)
s = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
\<not> is_final (steps0 (1, [], <nl>) tm_onestroke stp)
s = 0

goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke

goal (3 subgoals):
 1. s = 1 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. s = 2 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 3. s = 3 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. s = 1 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. s = 2 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 3. s = 3 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
assume "s=1"
[PROOF STATE]
proof (state)
this:
s = 1

goal (3 subgoals):
 1. s = 1 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. s = 2 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 3. s = 3 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
proof (cases r)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r = [] \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. \<And>a list. r = a # list \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
r = []

goal (2 subgoals):
 1. r = [] \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. \<And>a list. r = a # list \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r = []
[PROOF STEP]
have "r = []"
[PROOF STATE]
proof (prove)
using this:
r = []

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

goal (2 subgoals):
 1. r = [] \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. \<And>a list. r = a # list \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with cf_cases and \<open>s=1\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 1
r = []
[PROOF STEP]
have "steps0 (1, [], <nl>) tm_onestroke stp = (1, l, [])"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 1
r = []

goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke stp = (1, l, [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke stp = (1, l, [])

goal (2 subgoals):
 1. r = [] \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. \<And>a list. r = a # list \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
have "steps0 (1, [], <nl>) tm_onestroke (Suc stp) =
              step0 (steps0 (1,[], <nl>) tm_onestroke stp) tm_onestroke"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke
[PROOF STEP]
by (rule step_red)
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke

goal (2 subgoals):
 1. r = [] \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. \<And>a list. r = a # list \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke

goal (2 subgoals):
 1. r = [] \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. \<And>a list. r = a # list \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with cf_cases and \<open>s=1\<close> and \<open>r = []\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 1
r = []
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke
[PROOF STEP]
have "... = step0 (1,l,[]) tm_onestroke"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 1
r = []
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke

goal (1 subgoal):
 1. step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke = step0 (1, l, []) tm_onestroke
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke = step0 (1, l, []) tm_onestroke

goal (2 subgoals):
 1. r = [] \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. \<And>a list. r = a # list \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke = step0 (1, l, []) tm_onestroke

goal (2 subgoals):
 1. r = [] \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. \<And>a list. r = a # list \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
have "... = (3,Bk#l,[])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step0 (1, l, []) tm_onestroke = (3, Bk # l, [])
[PROOF STEP]
by (auto simp add: tm_onestroke_def numeral_eqs_upto_12 step.simps steps.simps)
[PROOF STATE]
proof (state)
this:
step0 (1, l, []) tm_onestroke = (3, Bk # l, [])

goal (2 subgoals):
 1. r = [] \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. \<And>a list. r = a # list \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (3, Bk # l, [])
[PROOF STEP]
have "steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (3,Bk#l,[])"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (3, Bk # l, [])

goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (3, Bk # l, [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (3, Bk # l, [])

goal (2 subgoals):
 1. r = [] \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. \<And>a list. r = a # list \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with \<open>steps0 (1, [], <nl>) tm_onestroke stp = (1, l, [])\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (1, l, [])
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (3, Bk # l, [])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (1, l, [])
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (3, Bk # l, [])

goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
by (auto simp add: measure_tm_onestroke_def)
[PROOF STATE]
proof (state)
this:
(steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke

goal (1 subgoal):
 1. \<And>a list. r = a # list \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. r = a # list \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
case (Cons a rs)
[PROOF STATE]
proof (state)
this:
r = a # rs

goal (1 subgoal):
 1. \<And>a list. r = a # list \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r = a # rs
[PROOF STEP]
have "r = a # rs"
[PROOF STATE]
proof (prove)
using this:
r = a # rs

goal (1 subgoal):
 1. r = a # rs
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
r = a # rs

goal (1 subgoal):
 1. \<And>a list. r = a # list \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
proof (cases "a")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = Bk \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
case Bk
[PROOF STATE]
proof (state)
this:
a = Bk

goal (2 subgoals):
 1. a = Bk \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Bk
[PROOF STEP]
have "a=Bk"
[PROOF STATE]
proof (prove)
using this:
a = Bk

goal (1 subgoal):
 1. a = Bk
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
a = Bk

goal (2 subgoals):
 1. a = Bk \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with cf_cases and \<open>s=1\<close> and \<open>r = a # rs\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 1
r = a # rs
a = Bk
[PROOF STEP]
have "steps0 (1, [], <nl>) tm_onestroke stp = (1, l, Bk#rs)"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 1
r = a # rs
a = Bk

goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke stp = (1, l, Bk # rs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke stp = (1, l, Bk # rs)

goal (2 subgoals):
 1. a = Bk \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
have "steps0 (1, [], <nl>) tm_onestroke (Suc stp) =
                step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke
[PROOF STEP]
by (rule step_red)
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke

goal (2 subgoals):
 1. a = Bk \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke

goal (2 subgoals):
 1. a = Bk \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with cf_cases and \<open>s=1\<close> and \<open>r = a # rs\<close> and \<open>a=Bk\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 1
r = a # rs
a = Bk
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke
[PROOF STEP]
have "... = step0 ((1, l, Bk#rs)) tm_onestroke"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 1
r = a # rs
a = Bk
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke

goal (1 subgoal):
 1. step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke = step0 (1, l, Bk # rs) tm_onestroke
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke = step0 (1, l, Bk # rs) tm_onestroke

goal (2 subgoals):
 1. a = Bk \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke = step0 (1, l, Bk # rs) tm_onestroke

goal (2 subgoals):
 1. a = Bk \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
have "... = (3,Bk#l,rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step0 (1, l, Bk # rs) tm_onestroke = (3, Bk # l, rs)
[PROOF STEP]
by (auto simp add: tm_onestroke_def numeral_eqs_upto_12 step.simps steps.simps)
[PROOF STATE]
proof (state)
this:
step0 (1, l, Bk # rs) tm_onestroke = (3, Bk # l, rs)

goal (2 subgoals):
 1. a = Bk \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (3, Bk # l, rs)
[PROOF STEP]
have "steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (3,Bk#l,rs)"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (3, Bk # l, rs)

goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (3, Bk # l, rs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (3, Bk # l, rs)

goal (2 subgoals):
 1. a = Bk \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with \<open>steps0 (1, [], <nl>) tm_onestroke stp = (1, l, Bk#rs)\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (1, l, Bk # rs)
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (3, Bk # l, rs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (1, l, Bk # rs)
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (3, Bk # l, rs)

goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
by (auto simp add: measure_tm_onestroke_def)
[PROOF STATE]
proof (state)
this:
(steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke

goal (1 subgoal):
 1. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
case Oc
[PROOF STATE]
proof (state)
this:
a = Oc

goal (1 subgoal):
 1. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Oc
[PROOF STEP]
have "a=Oc"
[PROOF STATE]
proof (prove)
using this:
a = Oc

goal (1 subgoal):
 1. a = Oc
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
a = Oc

goal (1 subgoal):
 1. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with cf_cases and \<open>s=1\<close> and \<open>r = a # rs\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 1
r = a # rs
a = Oc
[PROOF STEP]
have "steps0 (1, [], <nl>) tm_onestroke stp = (1, l, Oc#rs)"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 1
r = a # rs
a = Oc

goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke stp = (1, l, Oc # rs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke stp = (1, l, Oc # rs)

goal (1 subgoal):
 1. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
have "steps0 (1, [], <nl>) tm_onestroke (Suc stp) =
                step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke
[PROOF STEP]
by (rule step_red)
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke

goal (1 subgoal):
 1. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke

goal (1 subgoal):
 1. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with cf_cases and \<open>s=1\<close> and \<open>r = a # rs\<close> and \<open>a=Oc\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 1
r = a # rs
a = Oc
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke
[PROOF STEP]
have "... = step0 ((1, l, Oc#rs)) tm_onestroke"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 1
r = a # rs
a = Oc
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke

goal (1 subgoal):
 1. step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke = step0 (1, l, Oc # rs) tm_onestroke
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke = step0 (1, l, Oc # rs) tm_onestroke

goal (1 subgoal):
 1. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke = step0 (1, l, Oc # rs) tm_onestroke

goal (1 subgoal):
 1. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
have "... = (2,l,Bk#rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step0 (1, l, Oc # rs) tm_onestroke = (2, l, Bk # rs)
[PROOF STEP]
by (auto simp add: tm_onestroke_def numeral_eqs_upto_12 step.simps steps.simps)
[PROOF STATE]
proof (state)
this:
step0 (1, l, Oc # rs) tm_onestroke = (2, l, Bk # rs)

goal (1 subgoal):
 1. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (2, l, Bk # rs)
[PROOF STEP]
have "steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (2,l,Bk#rs)"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (2, l, Bk # rs)

goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (2, l, Bk # rs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (2, l, Bk # rs)

goal (1 subgoal):
 1. a = Oc \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with \<open>steps0 (1, [], <nl>) tm_onestroke stp = (1, l, Oc#rs)\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (1, l, Oc # rs)
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (2, l, Bk # rs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (1, l, Oc # rs)
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (2, l, Bk # rs)

goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
by (auto simp add: measure_tm_onestroke_def)
[PROOF STATE]
proof (state)
this:
(steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke

goal (2 subgoals):
 1. s = 2 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. s = 3 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s = 2 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. s = 3 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
assume "s=2"
[PROOF STATE]
proof (state)
this:
s = 2

goal (2 subgoals):
 1. s = 2 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. s = 3 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
from cf_cases and \<open>s=2\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 2
[PROOF STEP]
have "steps0 (1, [], <nl>) tm_onestroke stp = (2, l, r)"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 2

goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke stp = (2, l, r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke stp = (2, l, r)

goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with \<open>inv_tm_onestroke (steps0 (1, [], <nl>) tm_onestroke stp)\<close>
[PROOF STATE]
proof (chain)
picking this:
inv_tm_onestroke (steps0 (1, [], <nl>) tm_onestroke stp)
steps0 (1, [], <nl>) tm_onestroke stp = (2, l, r)
[PROOF STEP]
have "(\<exists>rs. r = Bk#rs)"
[PROOF STATE]
proof (prove)
using this:
inv_tm_onestroke (steps0 (1, [], <nl>) tm_onestroke stp)
steps0 (1, [], <nl>) tm_onestroke stp = (2, l, r)

goal (1 subgoal):
 1. \<exists>rs. r = Bk # rs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>rs. r = Bk # rs

goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>rs. r = Bk # rs
[PROOF STEP]
obtain rs where "r = Bk#rs"
[PROOF STATE]
proof (prove)
using this:
\<exists>rs. r = Bk # rs

goal (1 subgoal):
 1. (\<And>rs. r = Bk # rs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r = Bk # rs

goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with \<open>steps0 (1, [], <nl>) tm_onestroke stp = (2, l, r)\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (2, l, r)
r = Bk # rs
[PROOF STEP]
have "steps0 (1, [], <nl>) tm_onestroke stp = (2, l, Bk#rs)"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (2, l, r)
r = Bk # rs

goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke stp = (2, l, Bk # rs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke stp = (2, l, Bk # rs)

goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
have "steps0 (1, [], <nl>) tm_onestroke (Suc stp) =
              step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke
[PROOF STEP]
by (rule step_red)
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke

goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke

goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with cf_cases and \<open>s=2\<close> and \<open>r = Bk#rs\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 2
r = Bk # rs
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke
[PROOF STEP]
have "... = step0 (2,l,Bk#rs) tm_onestroke"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 2
r = Bk # rs
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke

goal (1 subgoal):
 1. step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke = step0 (2, l, Bk # rs) tm_onestroke
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke = step0 (2, l, Bk # rs) tm_onestroke

goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke = step0 (2, l, Bk # rs) tm_onestroke

goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
have "... = (1,Bk#l,rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step0 (2, l, Bk # rs) tm_onestroke = (1, Bk # l, rs)
[PROOF STEP]
by (auto simp add: tm_onestroke_def numeral_eqs_upto_12 step.simps steps.simps)
[PROOF STATE]
proof (state)
this:
step0 (2, l, Bk # rs) tm_onestroke = (1, Bk # l, rs)

goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (1, Bk # l, rs)
[PROOF STEP]
have "steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (1,Bk#l,rs)"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (1, Bk # l, rs)

goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (1, Bk # l, rs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (1, Bk # l, rs)

goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with \<open>steps0 (1, [], <nl>) tm_onestroke stp = (2, l, Bk#rs)\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (2, l, Bk # rs)
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (1, Bk # l, rs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (2, l, Bk # rs)
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (1, Bk # l, rs)

goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
by (auto simp add: measure_tm_onestroke_def)
[PROOF STATE]
proof (state)
this:
(steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke

goal (1 subgoal):
 1. s = 3 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s = 3 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
assume "s=3"
[PROOF STATE]
proof (state)
this:
s = 3

goal (1 subgoal):
 1. s = 3 \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
from cf_cases and \<open>s=3\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 3
[PROOF STEP]
have "steps0 (1, [], <nl>) tm_onestroke stp = (3, l, r)"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 3

goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke stp = (3, l, r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke stp = (3, l, r)

goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with \<open>inv_tm_onestroke (steps0 (1,[], <nl>) tm_onestroke stp)\<close>
[PROOF STATE]
proof (chain)
picking this:
inv_tm_onestroke (steps0 (1, [], <nl>) tm_onestroke stp)
steps0 (1, [], <nl>) tm_onestroke stp = (3, l, r)
[PROOF STEP]
have "(r= [] \<or> (\<exists>rs. r = Oc#rs))"
[PROOF STATE]
proof (prove)
using this:
inv_tm_onestroke (steps0 (1, [], <nl>) tm_onestroke stp)
steps0 (1, [], <nl>) tm_onestroke stp = (3, l, r)

goal (1 subgoal):
 1. r = [] \<or> (\<exists>rs. r = Oc # rs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r = [] \<or> (\<exists>rs. r = Oc # rs)

goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r = [] \<or> (\<exists>rs. r = Oc # rs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r = [] \<or> (\<exists>rs. r = Oc # rs)

goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r = [] \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. \<exists>rs. r = Oc # rs \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
assume "r = []"
[PROOF STATE]
proof (state)
this:
r = []

goal (2 subgoals):
 1. r = [] \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. \<exists>rs. r = Oc # rs \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with cf_cases and \<open>s=3\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 3
r = []
[PROOF STEP]
have "steps0 (1, [], <nl>) tm_onestroke stp = (3, l, [])"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 3
r = []

goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke stp = (3, l, [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke stp = (3, l, [])

goal (2 subgoals):
 1. r = [] \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. \<exists>rs. r = Oc # rs \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
have "steps0 (1, [], <nl>) tm_onestroke (Suc stp) =
                step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke
[PROOF STEP]
by (rule step_red)
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke

goal (2 subgoals):
 1. r = [] \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. \<exists>rs. r = Oc # rs \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke

goal (2 subgoals):
 1. r = [] \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. \<exists>rs. r = Oc # rs \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with cf_cases and \<open>s=3\<close> and \<open>r = []\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 3
r = []
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke
[PROOF STEP]
have "... = step0 (3,l,[]) tm_onestroke"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 3
r = []
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke

goal (1 subgoal):
 1. step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke = step0 (3, l, []) tm_onestroke
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke = step0 (3, l, []) tm_onestroke

goal (2 subgoals):
 1. r = [] \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. \<exists>rs. r = Oc # rs \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke = step0 (3, l, []) tm_onestroke

goal (2 subgoals):
 1. r = [] \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. \<exists>rs. r = Oc # rs \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
have "... = (0,l,[Oc])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step0 (3, l, []) tm_onestroke = (0, l, [Oc])
[PROOF STEP]
by (auto simp add: tm_onestroke_def numeral_eqs_upto_12 step.simps steps.simps)
[PROOF STATE]
proof (state)
this:
step0 (3, l, []) tm_onestroke = (0, l, [Oc])

goal (2 subgoals):
 1. r = [] \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. \<exists>rs. r = Oc # rs \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (0, l, [Oc])
[PROOF STEP]
have "steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (0,l,[Oc])"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (0, l, [Oc])

goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (0, l, [Oc])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (0, l, [Oc])

goal (2 subgoals):
 1. r = [] \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
 2. \<exists>rs. r = Oc # rs \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with \<open>steps0 (1, [], <nl>) tm_onestroke stp = (3, l, [])\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (3, l, [])
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (0, l, [Oc])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (3, l, [])
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (0, l, [Oc])

goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
by (auto simp add: measure_tm_onestroke_def)
[PROOF STATE]
proof (state)
this:
(steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke

goal (1 subgoal):
 1. \<exists>rs. r = Oc # rs \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>rs. r = Oc # rs \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
assume "\<exists>rs. r = Oc # rs"
[PROOF STATE]
proof (state)
this:
\<exists>rs. r = Oc # rs

goal (1 subgoal):
 1. \<exists>rs. r = Oc # rs \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>rs. r = Oc # rs
[PROOF STEP]
obtain rs where "r = Oc # rs"
[PROOF STATE]
proof (prove)
using this:
\<exists>rs. r = Oc # rs

goal (1 subgoal):
 1. (\<And>rs. r = Oc # rs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r = Oc # rs

goal (1 subgoal):
 1. \<exists>rs. r = Oc # rs \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with cf_cases and \<open>s=3\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 3
r = Oc # rs
[PROOF STEP]
have "steps0 (1, [], <nl>) tm_onestroke stp = (3, l,Oc # rs)"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 3
r = Oc # rs

goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke stp = (3, l, Oc # rs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke stp = (3, l, Oc # rs)

goal (1 subgoal):
 1. \<exists>rs. r = Oc # rs \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
have "steps0 (1, [], <nl>) tm_onestroke (Suc stp) =
                step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke
[PROOF STEP]
by (rule step_red)
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke

goal (1 subgoal):
 1. \<exists>rs. r = Oc # rs \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke

goal (1 subgoal):
 1. \<exists>rs. r = Oc # rs \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with cf_cases and \<open>s=3\<close> and \<open>r = Oc # rs\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 3
r = Oc # rs
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke
[PROOF STEP]
have "... = step0 (3,l,Oc # rs) tm_onestroke"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (s, l, r)
s = 3
r = Oc # rs
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke

goal (1 subgoal):
 1. step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke = step0 (3, l, Oc # rs) tm_onestroke
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke = step0 (3, l, Oc # rs) tm_onestroke

goal (1 subgoal):
 1. \<exists>rs. r = Oc # rs \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
step0 (steps0 (1, [], <nl>) tm_onestroke stp) tm_onestroke = step0 (3, l, Oc # rs) tm_onestroke

goal (1 subgoal):
 1. \<exists>rs. r = Oc # rs \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
have "... = (2,l,Bk#rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step0 (3, l, Oc # rs) tm_onestroke = (2, l, Bk # rs)
[PROOF STEP]
by (auto simp add: tm_onestroke_def numeral_eqs_upto_12 step.simps steps.simps)
[PROOF STATE]
proof (state)
this:
step0 (3, l, Oc # rs) tm_onestroke = (2, l, Bk # rs)

goal (1 subgoal):
 1. \<exists>rs. r = Oc # rs \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (2, l, Bk # rs)
[PROOF STEP]
have "steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (2,l,Bk#rs)"
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (2, l, Bk # rs)

goal (1 subgoal):
 1. steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (2, l, Bk # rs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (2, l, Bk # rs)

goal (1 subgoal):
 1. \<exists>rs. r = Oc # rs \<Longrightarrow> (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
with \<open>steps0 (1, [], <nl>) tm_onestroke stp = (3, l,Oc # rs)\<close>
[PROOF STATE]
proof (chain)
picking this:
steps0 (1, [], <nl>) tm_onestroke stp = (3, l, Oc # rs)
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (2, l, Bk # rs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
steps0 (1, [], <nl>) tm_onestroke stp = (3, l, Oc # rs)
steps0 (1, [], <nl>) tm_onestroke (Suc stp) = (2, l, Bk # rs)

goal (1 subgoal):
 1. (steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke
[PROOF STEP]
by (auto simp add: measure_tm_onestroke_def)
[PROOF STATE]
proof (state)
this:
(steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(steps0 (1, [], <nl>) tm_onestroke (Suc stp), steps0 (1, [], <nl>) tm_onestroke stp) \<in> measure_tm_onestroke

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tm_onestroke_total_correctness:
  "\<lbrace> \<lambda>tap. tap = ([], <nl:: nat list>) \<rbrace> tm_onestroke \<lbrace> \<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc]  @ Bk \<up>l) \<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], <nl>)\<rbrace> tm_onestroke \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, [Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
proof (rule tm_onestroke_partial_correctness)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>stp. is_final (steps0 (1, [], <nl>) tm_onestroke stp)
[PROOF STEP]
show "\<exists>stp. is_final (steps0 (1, [], <nl>) tm_onestroke stp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>stp. is_final (steps0 (1, [], <nl>) tm_onestroke stp)
[PROOF STEP]
using  tm_onestroke_induct_halts
[PROOF STATE]
proof (prove)
using this:
\<exists>stp. is_final (steps0 (1, [], <?nl>) tm_onestroke stp)

goal (1 subgoal):
 1. \<exists>stp. is_final (steps0 (1, [], <nl>) tm_onestroke stp)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>stp. is_final (steps0 (1, [], <nl>) tm_onestroke stp)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma to_list_ga_rec_rule:
    assumes "imp_set_iterate is_set is_it it_init it_has_next it_next"
    assumes "imp_list_prepend is_list l_prepend"
    assumes FIN: "finite it"
    shows "
    < is_it s si it iti * is_list l li >
      to_list_ga_rec it_has_next it_next l_prepend iti li
    < \<lambda>r. \<exists>\<^sub>Al'. is_set s si
      * is_list l' r
      * \<up>(set l' = set l \<union> it) >\<^sub>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <is_it s si it iti * is_list l li> to_list_ga_rec it_has_next it_next l_prepend iti li <\<lambda>r. \<exists>\<^sub>Al'. is_set s si * is_list l' r * \<up> (set l' = set l \<union> it)>\<^sub>t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. <is_it s si it iti * is_list l li> to_list_ga_rec it_has_next it_next l_prepend iti li <\<lambda>r. \<exists>\<^sub>Al'. is_set s si * is_list l' r * \<up> (set l' = set l \<union> it)>\<^sub>t
[PROOF STEP]
interpret imp_set_iterate is_set is_it it_init it_has_next it_next
      + imp_list_prepend is_list l_prepend
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_set_iterate is_set is_it it_init it_has_next it_next &&& imp_list_prepend is_list l_prepend
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. <is_it s si it iti * is_list l li> to_list_ga_rec it_has_next it_next l_prepend iti li <\<lambda>r. \<exists>\<^sub>Al'. is_set s si * is_list l' r * \<up> (set l' = set l \<union> it)>\<^sub>t
[PROOF STEP]
from FIN
[PROOF STATE]
proof (chain)
picking this:
finite it
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite it

goal (1 subgoal):
 1. <is_it s si it iti * is_list l li> to_list_ga_rec it_has_next it_next l_prepend iti li <\<lambda>r. \<exists>\<^sub>Al'. is_set s si * is_list l' r * \<up> (set l' = set l \<union> it)>\<^sub>t
[PROOF STEP]
proof (induction arbitrary: l li iti rule: finite_psubset_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A l li iti. \<lbrakk>finite A; \<And>B l li iti. B \<subset> A \<Longrightarrow> <is_it s si B iti * is_list l li> to_list_ga_rec it_has_next it_next l_prepend iti li <\<lambda>r. \<exists>\<^sub>Al'. is_set s si * is_list l' r * \<up> (set l' = set l \<union> B)>\<^sub>t\<rbrakk> \<Longrightarrow> <is_it s si A iti * is_list l li> to_list_ga_rec it_has_next it_next l_prepend iti li <\<lambda>r. \<exists>\<^sub>Al'. is_set s si * is_list l' r * \<up> (set l' = set l \<union> A)>\<^sub>t
[PROOF STEP]
case (psubset it)
[PROOF STATE]
proof (state)
this:
finite it
?B \<subset> it \<Longrightarrow> <is_it s si ?B ?iti * is_list ?l ?li> to_list_ga_rec it_has_next it_next l_prepend ?iti ?li <\<lambda>r. \<exists>\<^sub>Al'. is_set s si * is_list l' r * \<up> (set l' = set ?l \<union> ?B)>\<^sub>t

goal (1 subgoal):
 1. \<And>A l li iti. \<lbrakk>finite A; \<And>B l li iti. B \<subset> A \<Longrightarrow> <is_it s si B iti * is_list l li> to_list_ga_rec it_has_next it_next l_prepend iti li <\<lambda>r. \<exists>\<^sub>Al'. is_set s si * is_list l' r * \<up> (set l' = set l \<union> B)>\<^sub>t\<rbrakk> \<Longrightarrow> <is_it s si A iti * is_list l li> to_list_ga_rec it_has_next it_next l_prepend iti li <\<lambda>r. \<exists>\<^sub>Al'. is_set s si * is_list l' r * \<up> (set l' = set l \<union> A)>\<^sub>t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <is_it s si it iti * is_list l li> to_list_ga_rec it_has_next it_next l_prepend iti li <\<lambda>r. \<exists>\<^sub>Al'. is_set s si * is_list l' r * \<up> (set l' = set l \<union> it)>\<^sub>t
[PROOF STEP]
apply (subst to_list_ga_rec.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <is_it s si it iti * is_list l li> it_has_next iti \<bind> (\<lambda>b. if b then it_next iti \<bind> (\<lambda>(x, it). l_prepend x li \<bind> to_list_ga_rec it_has_next it_next l_prepend it) else return li) <\<lambda>r. \<exists>\<^sub>Al'. is_set s si * is_list l' r * \<up> (set l' = set l \<union> it)>\<^sub>t
[PROOF STEP]
apply (sep_auto heap: psubset.IH)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it = {} \<Longrightarrow> is_it s si {} iti * is_list l li * true \<Longrightarrow>\<^sub>A is_set s si * is_list l li * true
[PROOF STEP]
apply (rule ent_frame_fwd[OF quit_iteration])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. it = {} \<Longrightarrow> is_it s si {} iti * is_list l li * true \<Longrightarrow>\<^sub>A is_it ?s158 ?p158 ?s'158 ?it158 * ?F157
 2. it = {} \<Longrightarrow> is_set ?s158 ?p158 * true * ?F157 \<Longrightarrow>\<^sub>A is_set s si * is_list l li * true
[PROOF STEP]
apply frame_inference
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it = {} \<Longrightarrow> is_set s si * true * (is_list l li * true) \<Longrightarrow>\<^sub>A is_set s si * is_list l li * true
[PROOF STEP]
apply solve_entails
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
<is_it s si it iti * is_list l li> to_list_ga_rec it_has_next it_next l_prepend iti li <\<lambda>r. \<exists>\<^sub>Al'. is_set s si * is_list l' r * \<up> (set l' = set l \<union> it)>\<^sub>t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
<is_it s si it iti * is_list l li> to_list_ga_rec it_has_next it_next l_prepend iti li <\<lambda>r. \<exists>\<^sub>Al'. is_set s si * is_list l' r * \<up> (set l' = set l \<union> it)>\<^sub>t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma to_list_ga_rule:
    assumes IT: "imp_set_iterate is_set is_it it_init it_has_next it_next"
    assumes EM: "imp_list_empty is_list l_empty"
    assumes PREP: "imp_list_prepend is_list l_prepend"
    assumes FIN: "finite s"
    shows "
    <is_set s si>
    to_list_ga it_init it_has_next it_next
      l_empty l_prepend si
    <\<lambda>r. \<exists>\<^sub>Al. is_set s si * is_list l r * true * \<up>(set l = s)>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <is_set s si> to_list_ga it_init it_has_next it_next l_empty l_prepend si <\<lambda>r. \<exists>\<^sub>Al. is_set s si * is_list l r * true * \<up> (set l = s)>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. <is_set s si> to_list_ga it_init it_has_next it_next l_empty l_prepend si <\<lambda>r. \<exists>\<^sub>Al. is_set s si * is_list l r * true * \<up> (set l = s)>
[PROOF STEP]
interpret imp_list_empty is_list l_empty +
      imp_set_iterate is_set is_it it_init it_has_next it_next
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_list_empty is_list l_empty &&& imp_set_iterate is_set is_it it_init it_has_next it_next
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. <is_set s si> to_list_ga it_init it_has_next it_next l_empty l_prepend si <\<lambda>r. \<exists>\<^sub>Al. is_set s si * is_list l r * true * \<up> (set l = s)>
[PROOF STEP]
note [sep_heap_rules] = to_list_ga_rec_rule[OF IT PREP]
[PROOF STATE]
proof (state)
this:
finite ?it \<Longrightarrow> <is_it ?s ?si ?it ?iti * is_list ?l ?li> to_list_ga_rec it_has_next it_next l_prepend ?iti ?li <\<lambda>r. \<exists>\<^sub>Al'. is_set ?s ?si * is_list l' r * \<up> (set l' = set ?l \<union> ?it)>\<^sub>t

goal (1 subgoal):
 1. <is_set s si> to_list_ga it_init it_has_next it_next l_empty l_prepend si <\<lambda>r. \<exists>\<^sub>Al. is_set s si * is_list l r * true * \<up> (set l = s)>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <is_set s si> to_list_ga it_init it_has_next it_next l_empty l_prepend si <\<lambda>r. \<exists>\<^sub>Al. is_set s si * is_list l r * true * \<up> (set l = s)>
[PROOF STEP]
unfolding to_list_ga_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <is_set s si> it_init si \<bind> (\<lambda>it. l_empty \<bind> (\<lambda>l. to_list_ga_rec it_has_next it_next l_prepend it l \<bind> return)) <\<lambda>r. \<exists>\<^sub>Al. is_set s si * is_list l r * true * \<up> (set l = s)>
[PROOF STEP]
by (sep_auto simp: FIN)
[PROOF STATE]
proof (state)
this:
<is_set s si> to_list_ga it_init it_has_next it_next l_empty l_prepend si <\<lambda>r. \<exists>\<^sub>Al. is_set s si * is_list l r * true * \<up> (set l = s)>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "(bf_and a b) as \<longleftrightarrow> a as \<and> b as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bf_and a b as = (a as \<and> b as)
[PROOF STEP]
unfolding bf_and_def  bf_ite_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if a as then b as else False) = (a as \<and> b as)
[PROOF STEP]
by meson


[STATEMENT]
lemma bf_not_alt: "bf_not a as \<longleftrightarrow> \<not>a as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bf_not a as = (\<not> a as)
[PROOF STEP]
unfolding bf_not_def bf_ite_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if a as then False else True) = (\<not> a as)
[PROOF STEP]
by meson


[STATEMENT]
lemma bf_if_alt: "bf_if v t e = (\<lambda>l. if l v then t l else e l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bf_if v t e = (\<lambda>l. if l v then t l else e l)
[PROOF STEP]
unfolding bf_if_def bf_ite_def bf_lit_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>l. if l v then t l else e l) = (\<lambda>l. if l v then t l else e l)
[PROOF STEP]
..


[STATEMENT]
lemma bf_biimp_alt: "bf_biimp a b = (\<lambda>l. a l \<longleftrightarrow> b l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bf_biimp a b = (\<lambda>l. a l = b l)
[PROOF STEP]
unfolding bf_biimp_def bf_not_def bf_ite_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>l. if a l then b l else if b l then False else True) = (\<lambda>l. a l = b l)
[PROOF STEP]
by(simp add: fun_eq_iff)


[STATEMENT]
lemma bf_xor_alt: "bf_xor a b = (bf_ite a (bf_not b) b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bf_xor a b = bf_ite a (bf_not b) b
[PROOF STEP]
(* two application version *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bf_xor a b = bf_ite a (bf_not b) b
[PROOF STEP]
unfolding bf_xor_def bf_biimp_def bf_not_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bf_ite (bf_ite a b (bf_ite b bf_False bf_True)) bf_False bf_True = bf_ite a (bf_ite b bf_False bf_True) b
[PROOF STEP]
unfolding bf_ite_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>l. if if a l then b l else if b l then False else True then False else True) = (\<lambda>l. if a l then if b l then False else True else b l)
[PROOF STEP]
by simp


[STATEMENT]
lemma bf_imp_alt: "bf_imp a b = bf_or (bf_not a) b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bf_imp a b = bf_or (bf_not a) b
[PROOF STEP]
unfolding bf_or_def bf_not_def bf_imp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bf_ite a b bf_True = bf_ite (bf_ite a bf_False bf_True) bf_True b
[PROOF STEP]
unfolding bf_ite_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>l. if a l then b l else True) = (\<lambda>l. if if a l then False else True then True else b l)
[PROOF STEP]
unfolding fun_eq_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (if a x then b x else True) = (if if a x then False else True then True else b x)
[PROOF STEP]
by simp


[STATEMENT]
lemma [dest!,elim!]: "bf_False = bf_True \<Longrightarrow> False" "bf_True = bf_False \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bf_False = bf_True \<Longrightarrow> False) &&& (bf_True = bf_False \<Longrightarrow> False)
[PROOF STEP]
unfolding fun_eq_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. False = True \<Longrightarrow> False) &&& (\<forall>x. True = False \<Longrightarrow> False)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma "var \<notin> bf_vars (bf_restrict var val ex)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var \<notin> bf_vars (bf_restrict var val ex)
[PROOF STEP]
unfolding bf_vars_def bf_restrict_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var \<notin> {v. \<exists>as. ex (as(v := True, var := val)) \<noteq> ex (as(v := False, var := val))}
[PROOF STEP]
by(simp)


[STATEMENT]
lemma brace90shannon: "bf_ite F G H ass =
  bf_ite (\<lambda>l. l i)
         (bf_ite (bf_restrict i True F) (bf_restrict i True G) (bf_restrict i True H))
         (bf_ite (bf_restrict i False F) (bf_restrict i False G) (bf_restrict i False H)) ass"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bf_ite F G H ass = bf_ite (\<lambda>l. l i) (bf_ite (bf_restrict i True F) (bf_restrict i True G) (bf_restrict i True H)) (bf_ite (bf_restrict i False F) (bf_restrict i False G) (bf_restrict i False H)) ass
[PROOF STEP]
unfolding bf_ite_def bf_restrict_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if F ass then G ass else H ass) = (if ass i then if F (ass(i := True)) then G (ass(i := True)) else H (ass(i := True)) else if F (ass(i := False)) then G (ass(i := False)) else H (ass(i := False)))
[PROOF STEP]
by (auto simp add: fun_upd_idem)


[STATEMENT]
lemma word_rel_append:
  "word_rel v w O word_rel v w' = word_rel v (w @ w')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_rel v w O word_rel v w' = word_rel v (w @ w')
[PROOF STEP]
by (rule sym) (induct w, auto)


[STATEMENT]
lemma rel_word_rel: "rel v r = (\<Union>w\<in>lang r. word_rel v w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel v r = \<Union> (word_rel v ` lang r)
[PROOF STEP]
proof (induct r)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. rel v Zero = \<Union> (word_rel v ` lang Zero)
 2. rel v One = \<Union> (word_rel v ` lang One)
 3. \<And>x. rel v (Atom x) = \<Union> (word_rel v ` lang (Atom x))
 4. \<And>r1 r2. \<lbrakk>rel v r1 = \<Union> (word_rel v ` lang r1); rel v r2 = \<Union> (word_rel v ` lang r2)\<rbrakk> \<Longrightarrow> rel v (Plus r1 r2) = \<Union> (word_rel v ` lang (Plus r1 r2))
 5. \<And>r1 r2. \<lbrakk>rel v r1 = \<Union> (word_rel v ` lang r1); rel v r2 = \<Union> (word_rel v ` lang r2)\<rbrakk> \<Longrightarrow> rel v (Times r1 r2) = \<Union> (word_rel v ` lang (Times r1 r2))
 6. \<And>r. rel v r = \<Union> (word_rel v ` lang r) \<Longrightarrow> rel v (Star r) = \<Union> (word_rel v ` lang (Star r))
[PROOF STEP]
case Times
[PROOF STATE]
proof (state)
this:
rel v r1_ = \<Union> (word_rel v ` lang r1_)
rel v r2_ = \<Union> (word_rel v ` lang r2_)

goal (6 subgoals):
 1. rel v Zero = \<Union> (word_rel v ` lang Zero)
 2. rel v One = \<Union> (word_rel v ` lang One)
 3. \<And>x. rel v (Atom x) = \<Union> (word_rel v ` lang (Atom x))
 4. \<And>r1 r2. \<lbrakk>rel v r1 = \<Union> (word_rel v ` lang r1); rel v r2 = \<Union> (word_rel v ` lang r2)\<rbrakk> \<Longrightarrow> rel v (Plus r1 r2) = \<Union> (word_rel v ` lang (Plus r1 r2))
 5. \<And>r1 r2. \<lbrakk>rel v r1 = \<Union> (word_rel v ` lang r1); rel v r2 = \<Union> (word_rel v ` lang r2)\<rbrakk> \<Longrightarrow> rel v (Times r1 r2) = \<Union> (word_rel v ` lang (Times r1 r2))
 6. \<And>r. rel v r = \<Union> (word_rel v ` lang r) \<Longrightarrow> rel v (Star r) = \<Union> (word_rel v ` lang (Star r))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
rel v r1_ = \<Union> (word_rel v ` lang r1_)
rel v r2_ = \<Union> (word_rel v ` lang r2_)

goal (1 subgoal):
 1. rel v (Times r1_ r2_) = \<Union> (word_rel v ` lang (Times r1_ r2_))
[PROOF STEP]
by (auto simp: rel_def word_rel_append conc_def relcomp_UNION_distrib relcomp_UNION_distrib2)
[PROOF STATE]
proof (state)
this:
rel v (Times r1_ r2_) = \<Union> (word_rel v ` lang (Times r1_ r2_))

goal (5 subgoals):
 1. rel v Zero = \<Union> (word_rel v ` lang Zero)
 2. rel v One = \<Union> (word_rel v ` lang One)
 3. \<And>x. rel v (Atom x) = \<Union> (word_rel v ` lang (Atom x))
 4. \<And>r1 r2. \<lbrakk>rel v r1 = \<Union> (word_rel v ` lang r1); rel v r2 = \<Union> (word_rel v ` lang r2)\<rbrakk> \<Longrightarrow> rel v (Plus r1 r2) = \<Union> (word_rel v ` lang (Plus r1 r2))
 5. \<And>r. rel v r = \<Union> (word_rel v ` lang r) \<Longrightarrow> rel v (Star r) = \<Union> (word_rel v ` lang (Star r))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. rel v Zero = \<Union> (word_rel v ` lang Zero)
 2. rel v One = \<Union> (word_rel v ` lang One)
 3. \<And>x. rel v (Atom x) = \<Union> (word_rel v ` lang (Atom x))
 4. \<And>r1 r2. \<lbrakk>rel v r1 = \<Union> (word_rel v ` lang r1); rel v r2 = \<Union> (word_rel v ` lang r2)\<rbrakk> \<Longrightarrow> rel v (Plus r1 r2) = \<Union> (word_rel v ` lang (Plus r1 r2))
 5. \<And>r. rel v r = \<Union> (word_rel v ` lang r) \<Longrightarrow> rel v (Star r) = \<Union> (word_rel v ` lang (Star r))
[PROOF STEP]
case (Star r)
[PROOF STATE]
proof (state)
this:
rel v r = \<Union> (word_rel v ` lang r)

goal (5 subgoals):
 1. rel v Zero = \<Union> (word_rel v ` lang Zero)
 2. rel v One = \<Union> (word_rel v ` lang One)
 3. \<And>x. rel v (Atom x) = \<Union> (word_rel v ` lang (Atom x))
 4. \<And>r1 r2. \<lbrakk>rel v r1 = \<Union> (word_rel v ` lang r1); rel v r2 = \<Union> (word_rel v ` lang r2)\<rbrakk> \<Longrightarrow> rel v (Plus r1 r2) = \<Union> (word_rel v ` lang (Plus r1 r2))
 5. \<And>r. rel v r = \<Union> (word_rel v ` lang r) \<Longrightarrow> rel v (Star r) = \<Union> (word_rel v ` lang (Star r))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
rel v r = \<Union> (word_rel v ` lang r)

goal (5 subgoals):
 1. rel v Zero = \<Union> (word_rel v ` lang Zero)
 2. rel v One = \<Union> (word_rel v ` lang One)
 3. \<And>x. rel v (Atom x) = \<Union> (word_rel v ` lang (Atom x))
 4. \<And>r1 r2. \<lbrakk>rel v r1 = \<Union> (word_rel v ` lang r1); rel v r2 = \<Union> (word_rel v ` lang r2)\<rbrakk> \<Longrightarrow> rel v (Plus r1 r2) = \<Union> (word_rel v ` lang (Plus r1 r2))
 5. \<And>r. rel v r = \<Union> (word_rel v ` lang r) \<Longrightarrow> rel v (Star r) = \<Union> (word_rel v ` lang (Star r))
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. rel v Zero = \<Union> (word_rel v ` lang Zero)
 2. rel v One = \<Union> (word_rel v ` lang One)
 3. \<And>x. rel v (Atom x) = \<Union> (word_rel v ` lang (Atom x))
 4. \<And>r1 r2. \<lbrakk>rel v r1 = \<Union> (word_rel v ` lang r1); rel v r2 = \<Union> (word_rel v ` lang r2)\<rbrakk> \<Longrightarrow> rel v (Plus r1 r2) = \<Union> (word_rel v ` lang (Plus r1 r2))
 5. \<And>r. rel v r = \<Union> (word_rel v ` lang r) \<Longrightarrow> rel v (Star r) = \<Union> (word_rel v ` lang (Star r))
[PROOF STEP]
have "(rel v r) ^^ n = (\<Union>w \<in> lang r ^^ n. word_rel v w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel v r ^^ n = \<Union> (word_rel v ` (lang r ^^ n))
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rel v r ^^ 0 = \<Union> (word_rel v ` (lang r ^^ 0))
 2. \<And>n. rel v r ^^ n = \<Union> (word_rel v ` (lang r ^^ n)) \<Longrightarrow> rel v r ^^ Suc n = \<Union> (word_rel v ` (lang r ^^ Suc n))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. rel v r ^^ 0 = \<Union> (word_rel v ` (lang r ^^ 0))
 2. \<And>n. rel v r ^^ n = \<Union> (word_rel v ` (lang r ^^ n)) \<Longrightarrow> rel v r ^^ Suc n = \<Union> (word_rel v ` (lang r ^^ Suc n))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel v r ^^ 0 = \<Union> (word_rel v ` (lang r ^^ 0))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rel v r ^^ 0 = \<Union> (word_rel v ` (lang r ^^ 0))

goal (1 subgoal):
 1. \<And>n. rel v r ^^ n = \<Union> (word_rel v ` (lang r ^^ n)) \<Longrightarrow> rel v r ^^ Suc n = \<Union> (word_rel v ` (lang r ^^ Suc n))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. rel v r ^^ n = \<Union> (word_rel v ` (lang r ^^ n)) \<Longrightarrow> rel v r ^^ Suc n = \<Union> (word_rel v ` (lang r ^^ Suc n))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
rel v r ^^ n = \<Union> (word_rel v ` (lang r ^^ n))

goal (1 subgoal):
 1. \<And>n. rel v r ^^ n = \<Union> (word_rel v ` (lang r ^^ n)) \<Longrightarrow> rel v r ^^ Suc n = \<Union> (word_rel v ` (lang r ^^ Suc n))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
rel v r ^^ n = \<Union> (word_rel v ` (lang r ^^ n))

goal (1 subgoal):
 1. rel v r ^^ Suc n = \<Union> (word_rel v ` (lang r ^^ Suc n))
[PROOF STEP]
unfolding relpow.simps relpow_commute[symmetric]
[PROOF STATE]
proof (prove)
using this:
rel v r ^^ n = \<Union> (word_rel v ` (lang r ^^ n))

goal (1 subgoal):
 1. rel v r O rel v r ^^ n = \<Union> (word_rel v ` (lang r ^^ Suc n))
[PROOF STEP]
by (auto simp add: Star conc_def word_rel_append
          relcomp_UNION_distrib relcomp_UNION_distrib2)
[PROOF STATE]
proof (state)
this:
rel v r ^^ Suc n = \<Union> (word_rel v ` (lang r ^^ Suc n))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel v r ^^ n = \<Union> (word_rel v ` (lang r ^^ n))

goal (5 subgoals):
 1. rel v Zero = \<Union> (word_rel v ` lang Zero)
 2. rel v One = \<Union> (word_rel v ` lang One)
 3. \<And>x. rel v (Atom x) = \<Union> (word_rel v ` lang (Atom x))
 4. \<And>r1 r2. \<lbrakk>rel v r1 = \<Union> (word_rel v ` lang r1); rel v r2 = \<Union> (word_rel v ` lang r2)\<rbrakk> \<Longrightarrow> rel v (Plus r1 r2) = \<Union> (word_rel v ` lang (Plus r1 r2))
 5. \<And>r. rel v r = \<Union> (word_rel v ` lang r) \<Longrightarrow> rel v (Star r) = \<Union> (word_rel v ` lang (Star r))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
rel v r ^^ ?n2 = \<Union> (word_rel v ` (lang r ^^ ?n2))

goal (5 subgoals):
 1. rel v Zero = \<Union> (word_rel v ` lang Zero)
 2. rel v One = \<Union> (word_rel v ` lang One)
 3. \<And>x. rel v (Atom x) = \<Union> (word_rel v ` lang (Atom x))
 4. \<And>r1 r2. \<lbrakk>rel v r1 = \<Union> (word_rel v ` lang r1); rel v r2 = \<Union> (word_rel v ` lang r2)\<rbrakk> \<Longrightarrow> rel v (Plus r1 r2) = \<Union> (word_rel v ` lang (Plus r1 r2))
 5. \<And>r. rel v r = \<Union> (word_rel v ` lang r) \<Longrightarrow> rel v (Star r) = \<Union> (word_rel v ` lang (Star r))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
rel v r ^^ ?n2 = \<Union> (word_rel v ` (lang r ^^ ?n2))

goal (1 subgoal):
 1. rel v (Star r) = \<Union> (word_rel v ` lang (Star r))
[PROOF STEP]
unfolding rel.simps
[PROOF STATE]
proof (prove)
using this:
rel v r ^^ ?n2 = \<Union> (word_rel v ` (lang r ^^ ?n2))

goal (1 subgoal):
 1. (rel v r)\<^sup>* = \<Union> (word_rel v ` lang (Star r))
[PROOF STEP]
by (force simp: rtrancl_power star_def)
[PROOF STATE]
proof (state)
this:
rel v (Star r) = \<Union> (word_rel v ` lang (Star r))

goal (4 subgoals):
 1. rel v Zero = \<Union> (word_rel v ` lang Zero)
 2. rel v One = \<Union> (word_rel v ` lang One)
 3. \<And>x. rel v (Atom x) = \<Union> (word_rel v ` lang (Atom x))
 4. \<And>r1 r2. \<lbrakk>rel v r1 = \<Union> (word_rel v ` lang r1); rel v r2 = \<Union> (word_rel v ` lang r2)\<rbrakk> \<Longrightarrow> rel v (Plus r1 r2) = \<Union> (word_rel v ` lang (Plus r1 r2))
[PROOF STEP]
qed auto


[STATEMENT]
lemma soundness:
 "lang r = lang s \<Longrightarrow> rel v r = rel v s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lang r = lang s \<Longrightarrow> rel v r = rel v s
[PROOF STEP]
unfolding rel_word_rel
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lang r = lang s \<Longrightarrow> \<Union> (word_rel v ` lang r) = \<Union> (word_rel v ` lang s)
[PROOF STEP]
by auto


[STATEMENT]
lemma lookup_map_keys: "Mapping.lookup (map_keys f m) x = (if f -` {x} \<noteq> {} then Mapping.lookup m (THE k. f -` {x} = {k}) else None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.lookup (map_keys f m) x = (if f -` {x} \<noteq> {} then Mapping.lookup m (THE k. f -` {x} = {k}) else None)
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f m x. (if f -` {x} \<noteq> {} then m (THE k. f -` {x} = {k}) else None) = (if f -` {x} \<noteq> {} then m (THE k. f -` {x} = {k}) else None)
[PROOF STEP]
..


[STATEMENT]
lemma Mapping_Mapping_lookup [simp, code_unfold]: "Mapping.Mapping (Mapping.lookup m) = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping (Mapping.lookup m) = m
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma Mapping_eq_lookup: "m = m' \<longleftrightarrow> Mapping.lookup m = Mapping.lookup m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (m = m') = (Mapping.lookup m = Mapping.lookup m')
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma map_of_map_if_conv:
  "map_of (map (\<lambda>k. (k, f k)) xs) x = (if (x \<in> set xs) then Some (f x) else None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (map (\<lambda>k. (k, f k)) xs) x = (if x \<in> set xs then Some (f x) else None)
[PROOF STEP]
by (clarsimp simp: map_of_map_restrict)


[STATEMENT]
lemma Mapping_lookup_map: "Mapping.lookup (Mapping.map f g m) a = map_option g (Mapping.lookup m (f a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.lookup (Mapping.map f g m) a = map_option g (Mapping.lookup m (f a))
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma Mapping_lookup_map_default: "Mapping.lookup (Mapping.map_default k d f m) k' = (if k = k'
  then (Some \<circ> f) (case Mapping.lookup m k of None \<Rightarrow> d | Some x \<Rightarrow> x)
  else Mapping.lookup m k')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.lookup (Mapping.map_default k d f m) k' = (if k = k' then (Some \<circ> f) (case Mapping.lookup m k of None \<Rightarrow> d | Some x \<Rightarrow> x) else Mapping.lookup m k')
[PROOF STEP]
unfolding Mapping.map_default_def Mapping.default_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.lookup (Mapping.map_entry k f (if k \<in> Mapping.keys m then m else Mapping.update k d m)) k' = (if k = k' then (Some \<circ> f) (case Mapping.lookup m k of None \<Rightarrow> d | Some x \<Rightarrow> x) else Mapping.lookup m k')
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma Mapping_lookup_mapping_add: "Mapping.lookup (mapping_add m1 m2) k =
  case_option (Mapping.lookup m1 k) Some (Mapping.lookup m2 k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.lookup (mapping_add m1 m2) k = (case Mapping.lookup m2 k of None \<Rightarrow> Mapping.lookup m1 k | Some x \<Rightarrow> Some x)
[PROOF STEP]
by transfer (simp add: map_add_def)


[STATEMENT]
lemma Mapping_lookup_map_values: "Mapping.lookup (map_values f m) k =
  Option.bind (Mapping.lookup m k) (f k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.lookup (map_values f m) k = Option.bind (Mapping.lookup m k) (f k)
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma lookup_fold_update [simp]: "Mapping.lookup (fold (\<lambda>n. Mapping.update n (g n)) xs m) x
  = (if (x \<in> set xs) then Some (g x) else Mapping.lookup m x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.lookup (fold (\<lambda>n. Mapping.update n (g n)) xs m) x = (if x \<in> set xs then Some (g x) else Mapping.lookup m x)
[PROOF STEP]
by transfer (rule fold_update_conv)


[STATEMENT]
lemma mapping_eq_iff: "m1 = m2 \<longleftrightarrow> (\<forall>k. Mapping.lookup m1 k = Mapping.lookup m2 k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (m1 = m2) = (\<forall>k. Mapping.lookup m1 k = Mapping.lookup m2 k)
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma lookup_delete: "Mapping.lookup (Mapping.delete k m) k' = (if k = k' then None else Mapping.lookup m k')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.lookup (Mapping.delete k m) k' = (if k = k' then None else Mapping.lookup m k')
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma keys_map_values: "Mapping.keys (map_values f m) = Mapping.keys m - {k\<in>Mapping.keys m. f k (the (Mapping.lookup m k)) = None}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.keys (map_values f m) = Mapping.keys m - {k \<in> Mapping.keys m. f k (the (Mapping.lookup m k)) = None}
[PROOF STEP]
by transfer (auto simp add: bind_eq_Some_conv)


[STATEMENT]
lemma map_default_eq: "Mapping.map_default k v f m = m \<longleftrightarrow> (\<exists>v. Mapping.lookup m k = Some v \<and> f v = v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Mapping.map_default k v f m = m) = (\<exists>v. Mapping.lookup m k = Some v \<and> f v = v)
[PROOF STEP]
apply (clarsimp simp: Mapping.map_default_def Mapping.default_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (k \<in> Mapping.keys m \<longrightarrow> (Mapping.map_entry k f m = m) = (\<exists>v. Mapping.lookup m k = Some v \<and> f v = v)) \<and> (k \<notin> Mapping.keys m \<longrightarrow> (Mapping.map_entry k f (Mapping.update k v m) = m) = (\<exists>v. Mapping.lookup m k = Some v \<and> f v = v))
[PROOF STEP]
by transfer' (auto simp: fun_eq_iff split: if_splits)


[STATEMENT]
lemma lookup_update_cases: "Mapping.lookup (Mapping.update k v m) k' = (if k=k' then Some v else Mapping.lookup m k')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.lookup (Mapping.update k v m) k' = (if k = k' then Some v else Mapping.lookup m k')
[PROOF STEP]
by (cases "k=k'", simp_all add: Mapping.lookup_update Mapping.lookup_update_neq)


[STATEMENT]
lemma f_eq': "f x = m * x + f 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x = m * x + f 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f x = m * x + f 0
[PROOF STEP]
have rec: "f (b + 1) = f b + m" for b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (b + 1) = f b + m
[PROOF STEP]
using f_eq[of 0 b] f_eq[of "-1" "b + 1"]
[PROOF STATE]
proof (prove)
using this:
f (2 * 0) + 2 * f b = f (f (0 + b))
f (2 * - 1) + 2 * f (b + 1) = f (f (- 1 + (b + 1)))

goal (1 subgoal):
 1. f (b + 1) = f b + m
[PROOF STEP]
by (simp add: m_def)
[PROOF STATE]
proof (state)
this:
f (?b + 1) = f ?b + m

goal (1 subgoal):
 1. f x = m * x + f 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f (?b + 1) = f ?b + m

goal (1 subgoal):
 1. f x = m * x + f 0
[PROOF STEP]
have "f (b - 1) = f b - m" for b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (b - 1) = f b - m
[PROOF STEP]
using rec[of "b - 1"]
[PROOF STATE]
proof (prove)
using this:
f (b - 1 + 1) = f (b - 1) + m

goal (1 subgoal):
 1. f (b - 1) = f b - m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (?b - 1) = f ?b - m

goal (1 subgoal):
 1. f x = m * x + f 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f (?b + 1) = f ?b + m
f (?b - 1) = f ?b - m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f (?b + 1) = f ?b + m
f (?b - 1) = f ?b - m

goal (1 subgoal):
 1. f x = m * x + f 0
[PROOF STEP]
by (induction x rule: int_induct[of _ 0]) (auto simp: algebra_simps)
[PROOF STATE]
proof (state)
this:
f x = m * x + f 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma f_eq'_aux [simp]: "NO_MATCH 0 x \<Longrightarrow> f x = m * x + f 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NO_MATCH (0::'a) x \<Longrightarrow> f x = m * x + f 0
[PROOF STEP]
by (rule f_eq')


[STATEMENT]
lemma f_classification: "(\<forall>x. f x = 0) \<or> (\<forall>x. f x = 2 * x + f 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. f x = 0) \<or> (\<forall>x. f x = 2 * x + f 0)
[PROOF STEP]
using f_eq[of 0 0] f_eq[of 0 1]
[PROOF STATE]
proof (prove)
using this:
f (2 * 0) + 2 * f 0 = f (f (0 + 0))
f (2 * 0) + 2 * f 1 = f (f (0 + 1))

goal (1 subgoal):
 1. (\<forall>x. f x = 0) \<or> (\<forall>x. f x = 2 * x + f 0)
[PROOF STEP]
by auto


[STATEMENT]
lemma step_zero [simp]: "step 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step 0 = 0
[PROOF STEP]
by (simp add: step_def)


[STATEMENT]
lemma phase_step: "(phase r * nSteps) + step r = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phase r * nSteps + step r = r
[PROOF STEP]
by (auto simp add: phase_def step_def)


[STATEMENT]
lemma alpha_lt_N: "\<alpha> < N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> < N
[PROOF STEP]
using EltN majE
[PROOF STATE]
proof (prove)
using this:
E < N
N + nSteps * \<alpha> \<le> nSteps * E

goal (1 subgoal):
 1. \<alpha> < N
[PROOF STEP]
by auto


[STATEMENT]
lemma alpha_lt_T: "\<alpha> < T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> < T
[PROOF STEP]
using majT alpha_lt_N
[PROOF STATE]
proof (prove)
using this:
N + nSteps * \<alpha> \<le> nSteps * T
\<alpha> < N

goal (1 subgoal):
 1. \<alpha> < T
[PROOF STEP]
by auto


[STATEMENT]
lemma alpha_lt_E: "\<alpha> < E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> < E
[PROOF STEP]
using majE alpha_lt_N
[PROOF STATE]
proof (prove)
using this:
N + nSteps * \<alpha> \<le> nSteps * E
\<alpha> < N

goal (1 subgoal):
 1. \<alpha> < E
[PROOF STEP]
by auto


[STATEMENT]
lemma [sepref_fr_rules]: "(uncurry mop_plusi,uncurry mop_plus) \<in> nat_assn\<^sup>k*\<^sub>anat_assn\<^sup>k \<rightarrow>\<^sub>a nat_assn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (uncurry mop_plusi, uncurry mop_plus) \<in> nat_assn\<^sup>k *\<^sub>a nat_assn\<^sup>k \<rightarrow>\<^sub>a nat_assn
[PROOF STEP]
by (sep_auto intro!: hfrefI hn_refineI simp: pure_def)


[STATEMENT]
lemma ID_unfold_vars: "ID x y T \<Longrightarrow> x\<equiv>y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ID x y T \<Longrightarrow> x \<equiv> y
[PROOF STEP]
by simp


[STATEMENT]
lemma [sepref_import_param]: "(prio,prio) \<in> Id \<rightarrow> Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (prio, prio) \<in> Id \<rightarrow> Id
[PROOF STEP]
by simp


[STATEMENT]
lemma [sepref_import_param]:
      "((\<le>), (\<le>)::'b \<Rightarrow> _) \<in> Id \<rightarrow> Id \<rightarrow> bool_rel"
      "((<), (<)::'b \<Rightarrow> _) \<in> Id \<rightarrow> Id \<rightarrow> bool_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<le>), (\<le>)) \<in> Id \<rightarrow> Id \<rightarrow> bool_rel &&& ((<), (<)) \<in> Id \<rightarrow> Id \<rightarrow> bool_rel
[PROOF STEP]
by simp_all


[STATEMENT]
lemma [def_pat_rules]:
      "heapstruct.prio_of_op$prio \<equiv> PR_CONST prio_of_op"
      "heapstruct.sink_op$prio \<equiv> PR_CONST sink_op"
      "heapstruct.swim_op$prio \<equiv> PR_CONST swim_op"
      "heapstruct.repair_op$prio \<equiv> PR_CONST repair_op"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((heapstruct.prio_of_op $ prio \<equiv> PR_CONST prio_of_op) &&& heapstruct.sink_op $ prio \<equiv> PR_CONST sink_op) &&& (heapstruct.swim_op $ prio \<equiv> PR_CONST swim_op) &&& heapstruct.repair_op $ prio \<equiv> PR_CONST repair_op
[PROOF STEP]
by simp_all


[STATEMENT]
lemma inline_calls_map_Val_append [simp]:
  "inline_calls f (map Val vs @ es) = map Val vs @ inline_calls f es"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inline_calls f (map Val vs @ es) = map Val vs @ inline_calls f es
[PROOF STEP]
by(induct vs, auto)


[STATEMENT]
lemma inline_call_eq_Val_aux:
  "inline_call e E = Val v \<Longrightarrow> call E = \<lfloor>aMvs\<rfloor> \<Longrightarrow> e = Val v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inline_call e E = Val v; call E = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> e = Val v
[PROOF STEP]
by(induct E)(auto split: if_split_asm)


[STATEMENT]
lemma inline_calls_eq_empty [simp]: "inline_calls e es = [] \<longleftrightarrow> es = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inline_calls e es = []) = (es = [])
[PROOF STEP]
by(cases es, auto)


[STATEMENT]
lemma inline_calls_map_Val [simp]: "inline_calls e (map Val vs) = map Val vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inline_calls e (map Val vs) = map Val vs
[PROOF STEP]
by(induct vs) auto


[STATEMENT]
lemma Throw_eq_inline_call_eq [dest]:
  "inline_call e E = Throw a \<Longrightarrow> call E = \<lfloor>aMvs\<rfloor> \<Longrightarrow> Throw a = e \<or> addr a = e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inline_call e E = Throw a; call E = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> Throw a = e \<or> addr a = e
[PROOF STEP]
by(auto dest: inline_call_eq_Throw[OF sym])


[STATEMENT]
lemma is_vals_inline_calls [dest]:
  "\<lbrakk> is_vals (inline_calls e es); calls es = \<lfloor>aMvs\<rfloor> \<rbrakk> \<Longrightarrow> is_val e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_vals (inline_calls e es); calls es = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> is_val e
[PROOF STEP]
by(induct es, auto split: if_split_asm)


[STATEMENT]
lemma [dest]: "\<lbrakk> inline_calls e es = map Val vs; calls es = \<lfloor>aMvs\<rfloor> \<rbrakk> \<Longrightarrow> is_val e"
              "\<lbrakk> map Val vs = inline_calls e es; calls es = \<lfloor>aMvs\<rfloor> \<rbrakk> \<Longrightarrow> is_val e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>inline_calls e es = map Val vs; calls es = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> is_val e) &&& (\<lbrakk>map Val vs = inline_calls e es; calls es = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> is_val e)
[PROOF STEP]
by(fastforce intro!: is_vals_inline_calls del: is_val.intros simp add: is_vals_conv elim: sym)+


[STATEMENT]
lemma inline_calls_eq_Val_Throw [dest]:
  "\<lbrakk> inline_calls e es = map Val vs @ Throw a # es'; calls es = \<lfloor>aMvs\<rfloor> \<rbrakk> \<Longrightarrow> e = Throw a \<or> is_val e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inline_calls e es = map Val vs @ Throw a # es'; calls es = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> e = Throw a \<or> is_val e
[PROOF STEP]
apply(induct es arbitrary: vs a es')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>vs a es'. \<lbrakk>inline_calls e [] = map Val vs @ Throw a # es'; calls [] = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> e = Throw a \<or> is_val e
 2. \<And>a es vs aa es'. \<lbrakk>\<And>vs a es'. \<lbrakk>inline_calls e es = map Val vs @ Throw a # es'; calls es = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> e = Throw a \<or> is_val e; inline_calls e (a # es) = map Val vs @ Throw aa # es'; calls (a # es) = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> e = Throw aa \<or> is_val e
[PROOF STEP]
apply(auto simp add: Cons_eq_append_conv split: if_split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Val_Throw_eq_inline_calls [dest]:
  "\<lbrakk> map Val vs @ Throw a # es' = inline_calls e es; calls es = \<lfloor>aMvs\<rfloor> \<rbrakk> \<Longrightarrow> Throw a = e \<or> is_val e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>map Val vs @ Throw a # es' = inline_calls e es; calls es = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> Throw a = e \<or> is_val e
[PROOF STEP]
by(auto dest: inline_calls_eq_Val_Throw[OF sym])