[STATEMENT]
lemma always_create_res:"\<forall>ts. \<exists>ts'. (ts \<^bold>\<midarrow>r(c)\<^bold>\<rightarrow> ts')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ts. \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ts. \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
let ?type =
    "{ts ::(cars\<Rightarrow>real)*(cars\<Rightarrow>lanes)*(cars\<Rightarrow>lanes)*(cars\<Rightarrow>real\<Rightarrow>real)*(cars\<Rightarrow>real)*(cars\<Rightarrow>real).
           (\<forall>c. ((fst (snd ts))) c \<sqinter> ((fst (snd (snd ts)))) c = \<emptyset> )  \<and>
           (\<forall>c. |(fst (snd ts)) c| \<ge> 1) \<and>
           (\<forall>c. |(fst (snd ts)) c| \<le> 2) \<and>
           (\<forall>c. |(fst (snd (snd ts)) c)| \<le> 1) \<and>
           (\<forall>c. |(fst (snd ts)) c| + |(fst (snd (snd ts))) c| \<le> 2) \<and>
           (\<forall>c. (fst(snd(snd (ts)))) c \<noteq> \<emptyset> \<longrightarrow>
                  (\<exists> n. Rep_nat_int(fst (snd ts) c)\<union>Rep_nat_int(fst (snd (snd ts)) c)
                     = {n, n+1})) \<and>
           (\<forall>c . fst (snd (snd (snd (snd (ts))))) c > 0) \<and>
           (\<forall>c.  snd (snd (snd (snd (snd (ts))))) c > 0)
     }"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ts. \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
fix ts
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ts. \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
show " \<exists>ts'. (ts \<^bold>\<midarrow>r(c)\<^bold>\<rightarrow> ts')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
proof (cases "clm ts c = \<emptyset>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. clm ts c = bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
 2. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
clm ts c = bot

goal (2 subgoals):
 1. clm ts c = bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
 2. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
obtain ts' where ts'_def:"ts' = ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ts'. ts' = ts \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ts' = ts

goal (2 subgoals):
 1. clm ts c = bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
 2. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ts' = ts
[PROOF STEP]
have "ts \<^bold>\<midarrow>r(c)\<^bold>\<rightarrow> ts'"
[PROOF STATE]
proof (prove)
using this:
ts' = ts

goal (1 subgoal):
 1. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
using create_reservation_def True fun_upd_triv nat_int.un_empty_absorb1
[PROOF STATE]
proof (prove)
using this:
ts' = ts
?ts \<^bold>\<midarrow>r( ?c ) \<^bold>\<rightarrow> ?ts' \<equiv> pos ?ts' = pos ?ts \<and> res ?ts' = (res ?ts)(?c := res ?ts ?c \<squnion> clm ?ts ?c) \<and> dyn ?ts' = dyn ?ts \<and> clm ?ts' = (clm ?ts)(?c := bot) \<and> physical_size ?ts' = physical_size ?ts \<and> braking_distance ?ts' = braking_distance ?ts
clm ts c = bot
?f(?x := ?f ?x) = ?f
?i \<squnion> bot = ?i

goal (1 subgoal):
 1. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'

goal (2 subgoals):
 1. clm ts c = bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
 2. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'

goal (1 subgoal):
 1. \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
clm ts c \<noteq> bot

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
obtain ts' where ts'_def: "ts'=  (pos ts,
                                (res ts)(c:=( (res ts c)\<squnion> (clm ts c) )),
                                (clm ts)(c:=\<emptyset>),
                                (dyn ts), (physical_size ts), (braking_distance ts))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ts'. ts' = (pos ts, (res ts)(c := res ts c \<squnion> clm ts c), (clm ts)(c := bot), dyn ts, physical_size ts, braking_distance ts) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ts' = (pos ts, (res ts)(c := res ts c \<squnion> clm ts c), (clm ts)(c := bot), dyn ts, physical_size ts, braking_distance ts)

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
have disj:"\<forall>c .(((fst (snd ts'))) c \<sqinter> ((fst (snd (snd ts')))) c = \<emptyset>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. fst (snd ts') c \<sqinter> fst (snd (snd ts')) c = bot
[PROOF STEP]
by (simp add: disjoint nat_int.inter_empty1 ts'_def)
[PROOF STATE]
proof (state)
this:
\<forall>c. fst (snd ts') c \<sqinter> fst (snd (snd ts')) c = bot

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
have re_geq_one:"\<forall>d. |fst (snd ts') d| \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>d. 1 \<le> |fst (snd ts') d|
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>d. 1 \<le> |fst (snd ts') d|
[PROOF STEP]
fix d
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>d. 1 \<le> |fst (snd ts') d|
[PROOF STEP]
show " |fst (snd ts') d| \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> |fst (snd ts') d|
[PROOF STEP]
proof (cases "c = d")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c = d \<Longrightarrow> 1 \<le> |fst (snd ts') d|
 2. c \<noteq> d \<Longrightarrow> 1 \<le> |fst (snd ts') d|
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
c = d

goal (2 subgoals):
 1. c = d \<Longrightarrow> 1 \<le> |fst (snd ts') d|
 2. c \<noteq> d \<Longrightarrow> 1 \<le> |fst (snd ts') d|
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c = d
[PROOF STEP]
have "fst (snd ts') d = res ts d \<squnion> clm ts c"
[PROOF STATE]
proof (prove)
using this:
c = d

goal (1 subgoal):
 1. fst (snd ts') d = res ts d \<squnion> clm ts c
[PROOF STEP]
by (simp add: ts'_def)
[PROOF STATE]
proof (state)
this:
fst (snd ts') d = res ts d \<squnion> clm ts c

goal (2 subgoals):
 1. c = d \<Longrightarrow> 1 \<le> |fst (snd ts') d|
 2. c \<noteq> d \<Longrightarrow> 1 \<le> |fst (snd ts') d|
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (snd ts') d = res ts d \<squnion> clm ts c
[PROOF STEP]
have "res ts d \<sqsubseteq> fst (snd ts') d"
[PROOF STATE]
proof (prove)
using this:
fst (snd ts') d = res ts d \<squnion> clm ts c

goal (1 subgoal):
 1. res ts d \<le> fst (snd ts') d
[PROOF STEP]
by (metis False True Un_ac(3) nat_int.un_subset1 nat_int.un_subset2
              nat_int.union_def traffic.clm_consec_res)
[PROOF STATE]
proof (state)
this:
res ts d \<le> fst (snd ts') d

goal (2 subgoals):
 1. c = d \<Longrightarrow> 1 \<le> |fst (snd ts') d|
 2. c \<noteq> d \<Longrightarrow> 1 \<le> |fst (snd ts') d|
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
res ts d \<le> fst (snd ts') d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
res ts d \<le> fst (snd ts') d

goal (1 subgoal):
 1. 1 \<le> |fst (snd ts') d|
[PROOF STEP]
by (metis bot.extremum_uniqueI card_non_empty_geq_one traffic.atLeastOneRes)
[PROOF STATE]
proof (state)
this:
1 \<le> |fst (snd ts') d|

goal (1 subgoal):
 1. c \<noteq> d \<Longrightarrow> 1 \<le> |fst (snd ts') d|
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c \<noteq> d \<Longrightarrow> 1 \<le> |fst (snd ts') d|
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
c \<noteq> d

goal (1 subgoal):
 1. c \<noteq> d \<Longrightarrow> 1 \<le> |fst (snd ts') d|
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c \<noteq> d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c \<noteq> d

goal (1 subgoal):
 1. 1 \<le> |fst (snd ts') d|
[PROOF STEP]
using traffic.atLeastOneRes ts'_def
[PROOF STATE]
proof (prove)
using this:
c \<noteq> d
1 \<le> |res ?ts ?c|
ts' = (pos ts, (res ts)(c := res ts c \<squnion> clm ts c), (clm ts)(c := bot), dyn ts, physical_size ts, braking_distance ts)

goal (1 subgoal):
 1. 1 \<le> |fst (snd ts') d|
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 \<le> |fst (snd ts') d|

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
1 \<le> |fst (snd ts') d|

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>d. 1 \<le> |fst (snd ts') d|

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
have re_leq_two:"\<forall>c. |(fst (snd ts')) c| \<le> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. |fst (snd ts') c| \<le> 2
[PROOF STEP]
by (metis (no_types, lifting) Un_commute add.commute
          atMostTwoLanes atMostTwoRes nat_int.card_un_add clm_consec_res fun_upd_apply
          nat_int.union_def False prod.sel(1) prod.sel(2) ts'_def)
[PROOF STATE]
proof (state)
this:
\<forall>c. |fst (snd ts') c| \<le> 2

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
have cl_leq_one:"\<forall>c. |(fst (snd (snd ts'))) c| \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. |fst (snd (snd ts')) c| \<le> 1
[PROOF STEP]
using atMostOneClm nat_int.card_empty_zero ts'_def
[PROOF STATE]
proof (prove)
using this:
|clm ?ts ?c| \<le> 1
|bot| = 0
ts' = (pos ts, (res ts)(c := res ts c \<squnion> clm ts c), (clm ts)(c := bot), dyn ts, physical_size ts, braking_distance ts)

goal (1 subgoal):
 1. \<forall>c. |fst (snd (snd ts')) c| \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>c. |fst (snd (snd ts')) c| \<le> 1

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
have add_leq_two:"\<forall>c . |(fst (snd ts')) c| + |(fst (snd (snd ts'))) c| \<le> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. |fst (snd ts') c| + |fst (snd (snd ts')) c| \<le> 2
[PROOF STEP]
by (metis (no_types, lifting) Suc_1 add_Suc add_diff_cancel_left'
          add_mono_thms_linordered_semiring(1) card_non_empty_geq_one cl_leq_one
          fun_upd_apply le_SucE one_add_one prod.sel(1) prod.sel(2) re_leq_two
          traffic.atMostTwoLanes ts'_def)
[PROOF STATE]
proof (state)
this:
\<forall>c. |fst (snd ts') c| + |fst (snd (snd ts')) c| \<le> 2

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
have clNextRe :
      "\<forall>c. (((fst (snd (snd ts'))) c) \<noteq> \<emptyset> \<longrightarrow>
        (\<exists> n. Rep_nat_int ((fst (snd ts')) c) \<union> Rep_nat_int (fst (snd (snd ts')) c)
          = {n, n+1}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. fst (snd (snd ts')) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts') c) \<union> Rep_nat_int (fst (snd (snd ts')) c) = {n, n + 1})
[PROOF STEP]
using clmNextRes ts'_def
[PROOF STATE]
proof (prove)
using this:
clm ?ts ?c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (res ?ts ?c) \<union> Rep_nat_int (clm ?ts ?c) = {n, n + 1})
ts' = (pos ts, (res ts)(c := res ts c \<squnion> clm ts c), (clm ts)(c := bot), dyn ts, physical_size ts, braking_distance ts)

goal (1 subgoal):
 1. \<forall>c. fst (snd (snd ts')) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts') c) \<union> Rep_nat_int (fst (snd (snd ts')) c) = {n, n + 1})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>c. fst (snd (snd ts')) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts') c) \<union> Rep_nat_int (fst (snd (snd ts')) c) = {n, n + 1})

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
have ps_ge_zero: "(\<forall>c . fst (snd (snd (snd (snd (ts'))))) c > 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. 0 < fst (snd (snd (snd (snd ts')))) c
[PROOF STEP]
using ts'_def psGeZero
[PROOF STATE]
proof (prove)
using this:
ts' = (pos ts, (res ts)(c := res ts c \<squnion> clm ts c), (clm ts)(c := bot), dyn ts, physical_size ts, braking_distance ts)
\<forall>c. 0 < physical_size ?ts c

goal (1 subgoal):
 1. \<forall>c. 0 < fst (snd (snd (snd (snd ts')))) c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>c. 0 < fst (snd (snd (snd (snd ts')))) c

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
have sd_ge_zero: "(\<forall>c . snd (snd (snd (snd (snd (ts'))))) c > 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. 0 < snd (snd (snd (snd (snd ts')))) c
[PROOF STEP]
using ts'_def sdGeZero
[PROOF STATE]
proof (prove)
using this:
ts' = (pos ts, (res ts)(c := res ts c \<squnion> clm ts c), (clm ts)(c := bot), dyn ts, physical_size ts, braking_distance ts)
\<forall>c. 0 < braking_distance ?ts c

goal (1 subgoal):
 1. \<forall>c. 0 < snd (snd (snd (snd (snd ts')))) c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>c. 0 < snd (snd (snd (snd (snd ts')))) c

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
have ts'_type:
      "ts'\<in> ?type"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts' \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}
[PROOF STEP]
using  ts'_def disj  re_geq_one re_leq_two cl_leq_one add_leq_two
        clNextRe mem_Collect_eq  ps_ge_zero  sd_ge_zero
[PROOF STATE]
proof (prove)
using this:
ts' = (pos ts, (res ts)(c := res ts c \<squnion> clm ts c), (clm ts)(c := bot), dyn ts, physical_size ts, braking_distance ts)
\<forall>c. fst (snd ts') c \<sqinter> fst (snd (snd ts')) c = bot
\<forall>d. 1 \<le> |fst (snd ts') d|
\<forall>c. |fst (snd ts') c| \<le> 2
\<forall>c. |fst (snd (snd ts')) c| \<le> 1
\<forall>c. |fst (snd ts') c| + |fst (snd (snd ts')) c| \<le> 2
\<forall>c. fst (snd (snd ts')) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts') c) \<union> Rep_nat_int (fst (snd (snd ts')) c) = {n, n + 1})
(?a \<in> Collect ?P) = ?P ?a
\<forall>c. 0 < fst (snd (snd (snd (snd ts')))) c
\<forall>c. 0 < snd (snd (snd (snd (snd ts')))) c

goal (1 subgoal):
 1. ts' \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ts' \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
have rep_eq:"Rep_traffic (Abs_traffic ts') = ts'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_traffic (Abs_traffic ts') = ts'
[PROOF STEP]
using ts'_def ts'_type Abs_traffic_inverse
[PROOF STATE]
proof (prove)
using this:
ts' = (pos ts, (res ts)(c := res ts c \<squnion> clm ts c), (clm ts)(c := bot), dyn ts, physical_size ts, braking_distance ts)
ts' \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}
?y \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)} \<Longrightarrow> Rep_traffic (Abs_traffic ?y) = ?y

goal (1 subgoal):
 1. Rep_traffic (Abs_traffic ts') = ts'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Rep_traffic (Abs_traffic ts') = ts'

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
have sp_eq:"(pos (Abs_traffic ts')) = (pos ts) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pos (Abs_traffic ts') = pos ts
[PROOF STEP]
using rep_eq ts'_def Rep_traffic pos_def
[PROOF STATE]
proof (prove)
using this:
Rep_traffic (Abs_traffic ts') = ts'
ts' = (pos ts, (res ts)(c := res ts c \<squnion> clm ts c), (clm ts)(c := bot), dyn ts, physical_size ts, braking_distance ts)
Rep_traffic ?x \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}
pos ?ts \<equiv> fst (Rep_traffic ?ts)

goal (1 subgoal):
 1. pos (Abs_traffic ts') = pos ts
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pos (Abs_traffic ts') = pos ts

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
have res_eq:"(res  (Abs_traffic ts')) = (res ts)(c:=( (res ts c)\<squnion> (clm ts c) ))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. res (Abs_traffic ts') = (res ts)(c := res ts c \<squnion> clm ts c)
[PROOF STEP]
using Rep_traffic ts'_def ts'_type Abs_traffic_inverse rep_eq res_def clm_def
        fstI sndI
[PROOF STATE]
proof (prove)
using this:
Rep_traffic ?x \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}
ts' = (pos ts, (res ts)(c := res ts c \<squnion> clm ts c), (clm ts)(c := bot), dyn ts, physical_size ts, braking_distance ts)
ts' \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}
?y \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)} \<Longrightarrow> Rep_traffic (Abs_traffic ?y) = ?y
Rep_traffic (Abs_traffic ts') = ts'
res ?ts \<equiv> fst (snd (Rep_traffic ?ts))
clm ?ts \<equiv> fst (snd (snd (Rep_traffic ?ts)))
?x = (?y, ?z) \<Longrightarrow> fst ?x = ?y
?x = (?y, ?z) \<Longrightarrow> snd ?x = ?z

goal (1 subgoal):
 1. res (Abs_traffic ts') = (res ts)(c := res ts c \<squnion> clm ts c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
res (Abs_traffic ts') = (res ts)(c := res ts c \<squnion> clm ts c)

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
have dyn_eq:"(dyn  (Abs_traffic ts')) = (dyn ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dyn (Abs_traffic ts') = dyn ts
[PROOF STEP]
using Rep_traffic ts'_def ts'_type Abs_traffic_inverse rep_eq dyn_def fstI sndI
[PROOF STATE]
proof (prove)
using this:
Rep_traffic ?x \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}
ts' = (pos ts, (res ts)(c := res ts c \<squnion> clm ts c), (clm ts)(c := bot), dyn ts, physical_size ts, braking_distance ts)
ts' \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}
?y \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)} \<Longrightarrow> Rep_traffic (Abs_traffic ?y) = ?y
Rep_traffic (Abs_traffic ts') = ts'
dyn ?ts \<equiv> fst (snd (snd (snd (Rep_traffic ?ts))))
?x = (?y, ?z) \<Longrightarrow> fst ?x = ?y
?x = (?y, ?z) \<Longrightarrow> snd ?x = ?z

goal (1 subgoal):
 1. dyn (Abs_traffic ts') = dyn ts
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dyn (Abs_traffic ts') = dyn ts

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
have clm_eq:"(clm  (Abs_traffic ts')) = (clm ts)(c:=\<emptyset>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clm (Abs_traffic ts') = (clm ts)(c := bot)
[PROOF STEP]
using ts'_def ts'_type Abs_traffic_inverse rep_eq clm_def fstI sndI Rep_traffic
[PROOF STATE]
proof (prove)
using this:
ts' = (pos ts, (res ts)(c := res ts c \<squnion> clm ts c), (clm ts)(c := bot), dyn ts, physical_size ts, braking_distance ts)
ts' \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}
?y \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)} \<Longrightarrow> Rep_traffic (Abs_traffic ?y) = ?y
Rep_traffic (Abs_traffic ts') = ts'
clm ?ts \<equiv> fst (snd (snd (Rep_traffic ?ts)))
?x = (?y, ?z) \<Longrightarrow> fst ?x = ?y
?x = (?y, ?z) \<Longrightarrow> snd ?x = ?z
Rep_traffic ?x \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}

goal (1 subgoal):
 1. clm (Abs_traffic ts') = (clm ts)(c := bot)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
clm (Abs_traffic ts') = (clm ts)(c := bot)

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
clm (Abs_traffic ts') = (clm ts)(c := bot)
[PROOF STEP]
have "ts  \<^bold>\<midarrow>r(c)\<^bold>\<rightarrow> Abs_traffic ts'"
[PROOF STATE]
proof (prove)
using this:
clm (Abs_traffic ts') = (clm ts)(c := bot)

goal (1 subgoal):
 1. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> Abs_traffic ts'
[PROOF STEP]
using ts'_def ts'_type create_reservation_def
        ts'_def disj re_geq_one re_leq_two cl_leq_one add_leq_two
        fst_conv snd_conv rep_eq sp_eq res_eq dyn_eq clm_eq
        Rep_traffic clm_def res_def clm_def dyn_def physical_size_def braking_distance_def
[PROOF STATE]
proof (prove)
using this:
clm (Abs_traffic ts') = (clm ts)(c := bot)
ts' = (pos ts, (res ts)(c := res ts c \<squnion> clm ts c), (clm ts)(c := bot), dyn ts, physical_size ts, braking_distance ts)
ts' \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}
?ts \<^bold>\<midarrow>r( ?c ) \<^bold>\<rightarrow> ?ts' \<equiv> pos ?ts' = pos ?ts \<and> res ?ts' = (res ?ts)(?c := res ?ts ?c \<squnion> clm ?ts ?c) \<and> dyn ?ts' = dyn ?ts \<and> clm ?ts' = (clm ?ts)(?c := bot) \<and> physical_size ?ts' = physical_size ?ts \<and> braking_distance ?ts' = braking_distance ?ts
ts' = (pos ts, (res ts)(c := res ts c \<squnion> clm ts c), (clm ts)(c := bot), dyn ts, physical_size ts, braking_distance ts)
\<forall>c. fst (snd ts') c \<sqinter> fst (snd (snd ts')) c = bot
\<forall>d. 1 \<le> |fst (snd ts') d|
\<forall>c. |fst (snd ts') c| \<le> 2
\<forall>c. |fst (snd (snd ts')) c| \<le> 1
\<forall>c. |fst (snd ts') c| + |fst (snd (snd ts')) c| \<le> 2
fst (?x1.0, ?x2.0) = ?x1.0
snd (?x1.0, ?x2.0) = ?x2.0
Rep_traffic (Abs_traffic ts') = ts'
pos (Abs_traffic ts') = pos ts
res (Abs_traffic ts') = (res ts)(c := res ts c \<squnion> clm ts c)
dyn (Abs_traffic ts') = dyn ts
clm (Abs_traffic ts') = (clm ts)(c := bot)
Rep_traffic ?x \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}
clm ?ts \<equiv> fst (snd (snd (Rep_traffic ?ts)))
res ?ts \<equiv> fst (snd (Rep_traffic ?ts))
clm ?ts \<equiv> fst (snd (snd (Rep_traffic ?ts)))
dyn ?ts \<equiv> fst (snd (snd (snd (Rep_traffic ?ts))))
physical_size ?ts \<equiv> fst (snd (snd (snd (snd (Rep_traffic ?ts)))))
braking_distance ?ts \<equiv> snd (snd (snd (snd (snd (Rep_traffic ?ts)))))

goal (1 subgoal):
 1. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> Abs_traffic ts'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> Abs_traffic ts'

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> Abs_traffic ts'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> Abs_traffic ts'

goal (1 subgoal):
 1. \<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ts'. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma create_clm_eq_res:"(ts \<^bold>\<midarrow>c(d,n)\<^bold>\<rightarrow> ts')  \<longrightarrow> res ts c = res ts' c "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts \<^bold>\<midarrow>c( d, n ) \<^bold>\<rightarrow> ts' \<longrightarrow> res ts c = res ts' c
[PROOF STEP]
using create_claim_def
[PROOF STATE]
proof (prove)
using this:
?ts \<^bold>\<midarrow>c( ?c, ?n ) \<^bold>\<rightarrow> ?ts' \<equiv> pos ?ts' = pos ?ts \<and> res ?ts' = res ?ts \<and> dyn ?ts' = dyn ?ts \<and> physical_size ?ts' = physical_size ?ts \<and> braking_distance ?ts' = braking_distance ?ts \<and> |clm ?ts ?c| = 0 \<and> |res ?ts ?c| = 1 \<and> (?n + 1 \<^bold>\<in> res ?ts ?c \<or> ?n - 1 \<^bold>\<in> res ?ts ?c) \<and> clm ?ts' = (clm ?ts)(?c := Abs_nat_int {?n})

goal (1 subgoal):
 1. ts \<^bold>\<midarrow>c( d, n ) \<^bold>\<rightarrow> ts' \<longrightarrow> res ts c = res ts' c
[PROOF STEP]
by auto


[STATEMENT]
lemma withdraw_clm_eq_res:"(ts \<^bold>\<midarrow>wdc(d)\<^bold>\<rightarrow> ts') \<longrightarrow> res ts c= res ts' c "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts \<^bold>\<midarrow>wdc( d ) \<^bold>\<rightarrow> ts' \<longrightarrow> res ts c = res ts' c
[PROOF STEP]
using withdraw_claim_def
[PROOF STATE]
proof (prove)
using this:
?ts \<^bold>\<midarrow>wdc( ?c ) \<^bold>\<rightarrow> ?ts' \<equiv> pos ?ts' = pos ?ts \<and> res ?ts' = res ?ts \<and> dyn ?ts' = dyn ?ts \<and> physical_size ?ts' = physical_size ?ts \<and> braking_distance ?ts' = braking_distance ?ts \<and> clm ?ts' = (clm ?ts)(?c := bot)

goal (1 subgoal):
 1. ts \<^bold>\<midarrow>wdc( d ) \<^bold>\<rightarrow> ts' \<longrightarrow> res ts c = res ts' c
[PROOF STEP]
by auto


[STATEMENT]
lemma withdraw_res_subseteq:"(ts \<^bold>\<midarrow>wdr(d,n)\<^bold>\<rightarrow> ts') \<longrightarrow> res ts' c \<sqsubseteq> res ts c "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts \<^bold>\<midarrow>wdr( d, n ) \<^bold>\<rightarrow> ts' \<longrightarrow> res ts' c \<le> res ts c
[PROOF STEP]
using withdraw_reservation_def order_refl less_eq_nat_int.rep_eq nat_int.el.rep_eq
    nat_int.in_refl nat_int.in_singleton  fun_upd_apply subset_eq
[PROOF STATE]
proof (prove)
using this:
?ts \<^bold>\<midarrow>wdr( ?c, ?n ) \<^bold>\<rightarrow> ?ts' \<equiv> pos ?ts' = pos ?ts \<and> res ?ts' = (res ?ts)(?c := Abs_nat_int {?n}) \<and> dyn ?ts' = dyn ?ts \<and> clm ?ts' = clm ?ts \<and> physical_size ?ts' = physical_size ?ts \<and> braking_distance ?ts' = braking_distance ?ts \<and> ?n \<^bold>\<in> res ?ts ?c \<and> |res ?ts ?c| = 2
?x \<le> ?x
(?x \<le> ?xa) = (Rep_nat_int ?x \<subseteq> Rep_nat_int ?xa)
(?x \<^bold>\<in> ?xa) = (?x \<in> Rep_nat_int ?xa)
?n \<^bold>\<in> Abs_nat_int {?n}
?m \<^bold>\<in> Abs_nat_int {?n} \<longrightarrow> ?m = ?n
(?f(?x := ?y)) ?z = (if ?z = ?x then ?y else ?f ?z)
(?A \<subseteq> ?B) = (\<forall>x\<in>?A. x \<in> ?B)

goal (1 subgoal):
 1. ts \<^bold>\<midarrow>wdr( d, n ) \<^bold>\<rightarrow> ts' \<longrightarrow> res ts' c \<le> res ts c
[PROOF STEP]
by fastforce


[STATEMENT]
lemma sep_disj_prod_commute[simp]: "(ps, 0) ## (0, n)"   "(0, n) ## (ps, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ps, 0::'b) ## (0::'a, n) &&& (0::'a, n) ## (ps, 0::'b)
[PROOF STEP]
unfolding sep_disj_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (ps, 0::'b) ## fst (0::'a, n) \<and> snd (ps, 0::'b) ## snd (0::'a, n) &&& fst (0::'a, n) ## fst (ps, 0::'b) \<and> snd (0::'a, n) ## snd (ps, 0::'b)
[PROOF STEP]
by auto


[STATEMENT]
lemma sep_disj_prod_conv[simp]: "(a, x) ## (b, y) = (a##b \<and> x##y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, x) ## (b, y) = (a ## b \<and> x ## y)
[PROOF STEP]
unfolding sep_disj_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst (a, x) ## fst (b, y) \<and> snd (a, x) ## snd (b, y)) = (a ## b \<and> x ## y)
[PROOF STEP]
by auto


[STATEMENT]
lemma sep_plus_prod_conv[simp]: "(ps, n) + (ps', n') = (ps + ps', n + n')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ps, n) + (ps', n') = (ps + ps', n + n')
[PROOF STEP]
unfolding plus_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst (ps, n) + fst (ps', n'), snd (ps, n) + snd (ps', n')) = (ps + ps', n + n')
[PROOF STEP]
by auto


[STATEMENT]
lemma if_zero_one [simp]:
  "(if P then 1 else 0) = (0::nat) \<longleftrightarrow> \<not> P"
  "(0::nat) < (if P then 1 else 0) = P"
  "(if P then 0 else 1) = (if \<not>P then 1 else (0::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if P then 1 else 0) = 0) = (\<not> P) &&& (0 < (if P then 1 else 0)) = P &&& (if P then 0 else 1) = (if \<not> P then 1 else 0)
[PROOF STEP]
by (simp_all)


[STATEMENT]
lemma nth:
  "(x # xs) ! 0 = x"
  "(x # y # xs) ! 1 = y"
  "(x # y # z # xs) ! 2 = z"
  "(x # y # z # u # xs) ! 3 = u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x # xs) ! 0 = x &&& (x # y # xs) ! 1 = y) &&& (x # y # z # xs) ! 2 = z &&& (x # y # z # u # xs) ! 3 = u
[PROOF STEP]
by (simp_all)


[STATEMENT]
lemma setprod_atMost_Suc[simp]:
  "(\<Prod>i \<le> Suc n. f i) = (\<Prod>i \<le> n. f i) * f(Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod f {..Suc n} = prod f {..n} * f (Suc n)
[PROOF STEP]
by(simp add:atMost_Suc mult_ac)


[STATEMENT]
lemma setprod_lessThan_Suc[simp]:
  "(\<Prod>i < Suc n. f i) = (\<Prod>i < n. f i) * f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod f {..<Suc n} = prod f {..<n} * f n
[PROOF STEP]
by (simp add:lessThan_Suc mult_ac)


[STATEMENT]
lemma setsum_add_nat_ivl2: "n \<le> p  \<Longrightarrow>
  sum f {..<n} + sum f {n..p} = sum f {..p::nat}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> p \<Longrightarrow> sum f {..<n} + sum f {n..p} = sum f {..p}
[PROOF STEP]
apply(subst sum.union_disjoint[symmetric])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. n \<le> p \<Longrightarrow> finite {..<n}
 2. n \<le> p \<Longrightarrow> finite {n..p}
 3. n \<le> p \<Longrightarrow> {..<n} \<inter> {n..p} = {}
 4. n \<le> p \<Longrightarrow> sum f ({..<n} \<union> {n..p}) = sum f {..p}
[PROOF STEP]
apply(auto simp add: ivl_disj_un_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma setsum_eq_zero [simp]:
  fixes f::"nat \<Rightarrow> nat"
  shows "(\<Sum>i < n. f i) = 0 \<longleftrightarrow> (\<forall>i < n. f i = 0)"
    "(\<Sum>i \<le> n. f i) = 0 \<longleftrightarrow> (\<forall>i \<le> n. f i = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sum f {..<n} = 0) = (\<forall>i<n. f i = 0) &&& (sum f {..n} = 0) = (\<forall>i\<le>n. f i = 0)
[PROOF STEP]
by (auto)


[STATEMENT]
lemma setprod_eq_zero [simp]:
  fixes f::"nat \<Rightarrow> nat"
  shows "(\<Prod>i < n. f i) = 0 \<longleftrightarrow> (\<exists>i < n. f i = 0)"
    "(\<Prod>i \<le> n. f i) = 0 \<longleftrightarrow> (\<exists>i \<le> n. f i = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (prod f {..<n} = 0) = (\<exists>i<n. f i = 0) &&& (prod f {..n} = 0) = (\<exists>i\<le>n. f i = 0)
[PROOF STEP]
by (auto)


[STATEMENT]
lemma setsum_one_less:
  fixes n::nat
  assumes "\<forall>i < n. f i \<le> 1"
  shows "(\<Sum>i < n. f i) \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..<n} \<le> n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>i<n. f i \<le> 1

goal (1 subgoal):
 1. sum f {..<n} \<le> n
[PROOF STEP]
by (induct n) (auto)


[STATEMENT]
lemma setsum_one_le:
  fixes n::nat
  assumes "\<forall>i \<le> n. f i \<le> 1"
  shows "(\<Sum>i \<le> n. f i) \<le> Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..n} \<le> Suc n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<le>n. f i \<le> 1

goal (1 subgoal):
 1. sum f {..n} \<le> Suc n
[PROOF STEP]
by (induct n) (auto)


[STATEMENT]
lemma setsum_eq_one_le:
  fixes n::nat
  assumes "\<forall>i \<le> n. f i = 1"
  shows "(\<Sum>i \<le> n. f i) = Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..n} = Suc n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<le>n. f i = 1

goal (1 subgoal):
 1. sum f {..n} = Suc n
[PROOF STEP]
by (induct n) (auto)


[STATEMENT]
lemma setsum_least_eq:
  fixes f::"nat \<Rightarrow> nat"
  assumes h0: "p \<le> n"
  assumes h1: "\<forall>i \<in> {..<p}. f i = 1"
  assumes h2: "\<forall>i \<in> {p..n}. f i = 0"
  shows "(\<Sum>i \<le> n. f i) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..n} = p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum f {..n} = p
[PROOF STEP]
have eq_p: "(\<Sum>i \<in> {..<p}. f i) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..<p} = p
[PROOF STEP]
using h1
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{..<p}. f i = 1

goal (1 subgoal):
 1. sum f {..<p} = p
[PROOF STEP]
by (induct p) (simp_all)
[PROOF STATE]
proof (state)
this:
sum f {..<p} = p

goal (1 subgoal):
 1. sum f {..n} = p
[PROOF STEP]
have eq_zero: "(\<Sum>i \<in> {p..n}. f i) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {p..n} = 0
[PROOF STEP]
using h2
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{p..n}. f i = 0

goal (1 subgoal):
 1. sum f {p..n} = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum f {p..n} = 0

goal (1 subgoal):
 1. sum f {..n} = p
[PROOF STEP]
have "(\<Sum>i \<le> n. f i) = (\<Sum>i \<in> {..<p}. f i) + (\<Sum>i \<in> {p..n}. f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..n} = sum f {..<p} + sum f {p..n}
[PROOF STEP]
using h0
[PROOF STATE]
proof (prove)
using this:
p \<le> n

goal (1 subgoal):
 1. sum f {..n} = sum f {..<p} + sum f {p..n}
[PROOF STEP]
by (simp add: setsum_add_nat_ivl2)
[PROOF STATE]
proof (state)
this:
sum f {..n} = sum f {..<p} + sum f {p..n}

goal (1 subgoal):
 1. sum f {..n} = p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum f {..n} = sum f {..<p} + sum f {p..n}

goal (1 subgoal):
 1. sum f {..n} = p
[PROOF STEP]
have "... = (\<Sum>i \<in> {..<p}. f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..<p} + sum f {p..n} = sum f {..<p}
[PROOF STEP]
using eq_zero
[PROOF STATE]
proof (prove)
using this:
sum f {p..n} = 0

goal (1 subgoal):
 1. sum f {..<p} + sum f {p..n} = sum f {..<p}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum f {..<p} + sum f {p..n} = sum f {..<p}

goal (1 subgoal):
 1. sum f {..n} = p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum f {..n} = sum f {..<p}
[PROOF STEP]
show "(\<Sum>i \<le> n. f i) = p"
[PROOF STATE]
proof (prove)
using this:
sum f {..n} = sum f {..<p}

goal (1 subgoal):
 1. sum f {..n} = p
[PROOF STEP]
using eq_p
[PROOF STATE]
proof (prove)
using this:
sum f {..n} = sum f {..<p}
sum f {..<p} = p

goal (1 subgoal):
 1. sum f {..n} = p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum f {..n} = p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nat_mult_le_one:
  fixes m n::nat
  assumes "m \<le> 1" "n \<le> 1"
  shows "m * n \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m * n \<le> 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m \<le> 1
n \<le> 1

goal (1 subgoal):
 1. m * n \<le> 1
[PROOF STEP]
by (induct n) (auto)


[STATEMENT]
lemma setprod_one_le:
  fixes f::"nat \<Rightarrow> nat"
  assumes "\<forall>i \<le> n. f i \<le> 1"
  shows "(\<Prod>i \<le> n. f i) \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod f {..n} \<le> 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<le>n. f i \<le> 1

goal (1 subgoal):
 1. prod f {..n} \<le> 1
[PROOF STEP]
by (induct n) (auto intro: nat_mult_le_one)


[STATEMENT]
lemma setprod_greater_zero:
  fixes f::"nat \<Rightarrow> nat"
  assumes "\<forall>i \<le> n. f i \<ge> 0"
  shows "(\<Prod>i \<le> n. f i) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> prod f {..n}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<le>n. 0 \<le> f i

goal (1 subgoal):
 1. 0 \<le> prod f {..n}
[PROOF STEP]
by (induct n) (auto)


[STATEMENT]
lemma setprod_eq_one:
  fixes f::"nat \<Rightarrow> nat"
  assumes "\<forall>i \<le> n. f i = Suc 0"
  shows "(\<Prod>i \<le> n. f i) = Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod f {..n} = Suc 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<le>n. f i = Suc 0

goal (1 subgoal):
 1. prod f {..n} = Suc 0
[PROOF STEP]
by (induct n) (auto)


[STATEMENT]
lemma setsum_cut_off_less:
  fixes f::"nat \<Rightarrow> nat"
  assumes h1: "m \<le> n"
    and     h2: "\<forall>i \<in> {m..<n}. f i = 0"
  shows "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..<n} = sum f {..<m}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum f {..<n} = sum f {..<m}
[PROOF STEP]
have eq_zero: "(\<Sum>i \<in> {m..<n}. f i) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {m..<n} = 0
[PROOF STEP]
using h2
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{m..<n}. f i = 0

goal (1 subgoal):
 1. sum f {m..<n} = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum f {m..<n} = 0

goal (1 subgoal):
 1. sum f {..<n} = sum f {..<m}
[PROOF STEP]
have "(\<Sum>i < n. f i) = (\<Sum>i \<in> {..<m}. f i) + (\<Sum>i \<in> {m..<n}. f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..<n} = sum f {..<m} + sum f {m..<n}
[PROOF STEP]
using h1
[PROOF STATE]
proof (prove)
using this:
m \<le> n

goal (1 subgoal):
 1. sum f {..<n} = sum f {..<m} + sum f {m..<n}
[PROOF STEP]
by (metis atLeast0LessThan le0 sum.atLeastLessThan_concat)
[PROOF STATE]
proof (state)
this:
sum f {..<n} = sum f {..<m} + sum f {m..<n}

goal (1 subgoal):
 1. sum f {..<n} = sum f {..<m}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum f {..<n} = sum f {..<m} + sum f {m..<n}

goal (1 subgoal):
 1. sum f {..<n} = sum f {..<m}
[PROOF STEP]
have "... = (\<Sum>i \<in> {..<m}. f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..<m} + sum f {m..<n} = sum f {..<m}
[PROOF STEP]
using eq_zero
[PROOF STATE]
proof (prove)
using this:
sum f {m..<n} = 0

goal (1 subgoal):
 1. sum f {..<m} + sum f {m..<n} = sum f {..<m}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum f {..<m} + sum f {m..<n} = sum f {..<m}

goal (1 subgoal):
 1. sum f {..<n} = sum f {..<m}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum f {..<n} = sum f {..<m}
[PROOF STEP]
show "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)"
[PROOF STATE]
proof (prove)
using this:
sum f {..<n} = sum f {..<m}

goal (1 subgoal):
 1. sum f {..<n} = sum f {..<m}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum f {..<n} = sum f {..<m}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma setsum_cut_off_le:
  fixes f::"nat \<Rightarrow> nat"
  assumes h1: "m \<le> n"
    and     h2: "\<forall>i \<in> {m..n}. f i = 0"
  shows "(\<Sum>i \<le> n. f i) = (\<Sum>i < m. f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..n} = sum f {..<m}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum f {..n} = sum f {..<m}
[PROOF STEP]
have eq_zero: "(\<Sum>i \<in> {m..n}. f i) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {m..n} = 0
[PROOF STEP]
using h2
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{m..n}. f i = 0

goal (1 subgoal):
 1. sum f {m..n} = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum f {m..n} = 0

goal (1 subgoal):
 1. sum f {..n} = sum f {..<m}
[PROOF STEP]
have "(\<Sum>i \<le> n. f i) = (\<Sum>i \<in> {..<m}. f i) + (\<Sum>i \<in> {m..n}. f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..n} = sum f {..<m} + sum f {m..n}
[PROOF STEP]
using h1
[PROOF STATE]
proof (prove)
using this:
m \<le> n

goal (1 subgoal):
 1. sum f {..n} = sum f {..<m} + sum f {m..n}
[PROOF STEP]
by (simp add: setsum_add_nat_ivl2)
[PROOF STATE]
proof (state)
this:
sum f {..n} = sum f {..<m} + sum f {m..n}

goal (1 subgoal):
 1. sum f {..n} = sum f {..<m}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum f {..n} = sum f {..<m} + sum f {m..n}

goal (1 subgoal):
 1. sum f {..n} = sum f {..<m}
[PROOF STEP]
have "... = (\<Sum>i \<in> {..<m}. f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..<m} + sum f {m..n} = sum f {..<m}
[PROOF STEP]
using eq_zero
[PROOF STATE]
proof (prove)
using this:
sum f {m..n} = 0

goal (1 subgoal):
 1. sum f {..<m} + sum f {m..n} = sum f {..<m}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum f {..<m} + sum f {m..n} = sum f {..<m}

goal (1 subgoal):
 1. sum f {..n} = sum f {..<m}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum f {..n} = sum f {..<m}
[PROOF STEP]
show "(\<Sum>i \<le> n. f i) = (\<Sum>i < m. f i)"
[PROOF STATE]
proof (prove)
using this:
sum f {..n} = sum f {..<m}

goal (1 subgoal):
 1. sum f {..n} = sum f {..<m}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum f {..n} = sum f {..<m}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma setprod_one [simp]:
  fixes n::nat
  shows "(\<Prod>i < n. Suc 0) = Suc 0"
    "(\<Prod>i \<le> n. Suc 0) = Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>i<n. Suc 0) = Suc 0 &&& (\<Prod>i\<le>n. Suc 0) = Suc 0
[PROOF STEP]
by (induct n) (simp_all)


[STATEMENT]
lemma constn_lemma [simp]:
  "rec_eval (constn n) xs = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval (constn n) xs = n
[PROOF STEP]
by (induct n) (simp_all)


[STATEMENT]
lemma swap_lemma [simp]:
  "rec_eval (rec_swap f) [x, y] = rec_eval f [y, x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval (rec_swap f) [x, y] = rec_eval f [y, x]
[PROOF STEP]
by (simp add: rec_swap_def)


[STATEMENT]
lemma add_lemma [simp]:
  "rec_eval rec_add [x, y] =  x + y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_add [x, y] = x + y
[PROOF STEP]
by (induct x) (simp_all add: rec_add_def)


[STATEMENT]
lemma mult_lemma [simp]:
  "rec_eval rec_mult [x, y] = x * y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_mult [x, y] = x * y
[PROOF STEP]
by (induct x) (simp_all add: rec_mult_def)


[STATEMENT]
lemma power_lemma [simp]:
  "rec_eval rec_power [x, y] = x ^ y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_power [x, y] = x ^ y
[PROOF STEP]
by (induct y) (simp_all add: rec_power_def)


[STATEMENT]
lemma fact_aux_lemma [simp]:
  "rec_eval rec_fact_aux [x, y] = fact x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_fact_aux [x, y] = fact x
[PROOF STEP]
by (induct x) (simp_all add: rec_fact_aux_def)


[STATEMENT]
lemma fact_lemma [simp]:
  "rec_eval rec_fact [x] = fact x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_fact [x] = fact x
[PROOF STEP]
by (simp add: rec_fact_def)


[STATEMENT]
lemma pred_lemma [simp]:
  "rec_eval rec_predecessor [x] =  x - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_predecessor [x] = x - 1
[PROOF STEP]
by (induct x) (simp_all add: rec_predecessor_def)


[STATEMENT]
lemma minus_lemma [simp]:
  "rec_eval rec_minus [x, y] = x - y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_minus [x, y] = x - y
[PROOF STEP]
by (induct y) (simp_all add: rec_minus_def)


[STATEMENT]
lemma sign_lemma [simp]:
  "rec_eval rec_sign [x] = (if x = 0 then 0 else 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_sign [x] = (if x = 0 then 0 else 1)
[PROOF STEP]
by (simp add: rec_sign_def)


[STATEMENT]
lemma not_lemma [simp]:
  "rec_eval rec_not [x] = (if x = 0 then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_not [x] = (if x = 0 then 1 else 0)
[PROOF STEP]
by (simp add: rec_not_def)


[STATEMENT]
lemma eq_lemma [simp]:
  "rec_eval rec_eq [x, y] = (if x = y then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_eq [x, y] = (if x = y then 1 else 0)
[PROOF STEP]
by (simp add: rec_eq_def)


[STATEMENT]
lemma noteq_lemma [simp]:
  "rec_eval rec_noteq [x, y] = (if x \<noteq> y then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_noteq [x, y] = (if x \<noteq> y then 1 else 0)
[PROOF STEP]
by (simp add: rec_noteq_def)


[STATEMENT]
lemma conj_lemma [simp]:
  "rec_eval rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 else 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 else 1)
[PROOF STEP]
by (simp add: rec_conj_def)


[STATEMENT]
lemma disj_lemma [simp]:
  "rec_eval rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0 else 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0 else 1)
[PROOF STEP]
by (simp add: rec_disj_def)


[STATEMENT]
lemma imp_lemma [simp]:
  "rec_eval rec_imp [x, y] = (if 0 < x \<and> y = 0 then 0 else 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_imp [x, y] = (if 0 < x \<and> y = 0 then 0 else 1)
[PROOF STEP]
by (simp add: rec_imp_def)


[STATEMENT]
lemma ifz_lemma [simp]:
  "rec_eval rec_ifz [z, x, y] = (if z = 0 then x else y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_ifz [z, x, y] = (if z = 0 then x else y)
[PROOF STEP]
by (cases z) (simp_all add: rec_ifz_def)


[STATEMENT]
lemma if_lemma [simp]:
  "rec_eval rec_if [z, x, y] = (if 0 < z then x else y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_if [z, x, y] = (if 0 < z then x else y)
[PROOF STEP]
by (simp add: rec_if_def)


[STATEMENT]
lemma less_lemma [simp]:
  "rec_eval rec_less [x, y] = (if x < y then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_less [x, y] = (if x < y then 1 else 0)
[PROOF STEP]
by (simp add: rec_less_def)


[STATEMENT]
lemma le_lemma [simp]:
  "rec_eval rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_le [x, y] = (if x \<le> y then 1 else 0)
[PROOF STEP]
by(simp add: rec_le_def)


[STATEMENT]
lemma sigma1_lemma [simp]:
  shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. rec_eval f [z, y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval (rec_sigma1 f) [x, y] = (\<Sum>z\<le>x. rec_eval f [z, y])
[PROOF STEP]
by (induct x) (simp_all add: rec_sigma1_def)


[STATEMENT]
lemma sigma2_lemma [simp]:
  shows "rec_eval (rec_sigma2 f) [x, y1, y2] = (\<Sum> z \<le> x. rec_eval f  [z, y1, y2])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval (rec_sigma2 f) [x, y1, y2] = (\<Sum>z\<le>x. rec_eval f [z, y1, y2])
[PROOF STEP]
by (induct x) (simp_all add: rec_sigma2_def)


[STATEMENT]
lemma accum1_lemma [simp]:
  shows "rec_eval (rec_accum1 f) [x, y] = (\<Prod> z \<le> x. rec_eval f  [z, y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval (rec_accum1 f) [x, y] = (\<Prod>z\<le>x. rec_eval f [z, y])
[PROOF STEP]
by (induct x) (simp_all add: rec_accum1_def)


[STATEMENT]
lemma accum2_lemma [simp]:
  shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. rec_eval f  [z, y1, y2])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod>z\<le>x. rec_eval f [z, y1, y2])
[PROOF STEP]
by (induct x) (simp_all add: rec_accum2_def)


[STATEMENT]
lemma accum3_lemma [simp]:
  shows "rec_eval (rec_accum3 f) [x, y1, y2, y3] = (\<Prod> z \<le> x. (rec_eval f)  [z, y1, y2, y3])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval (rec_accum3 f) [x, y1, y2, y3] = (\<Prod>z\<le>x. rec_eval f [z, y1, y2, y3])
[PROOF STEP]
by (induct x) (simp_all add: rec_accum3_def)


[STATEMENT]
lemma ex1_lemma [simp]:
  "rec_eval (rec_ex1 f) [x, y] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval (rec_ex1 f) [x, y] = (if \<exists>z\<le>x. 0 < rec_eval f [z, y] then 1 else 0)
[PROOF STEP]
by (simp add: rec_ex1_def)


[STATEMENT]
lemma ex2_lemma [simp]:
  "rec_eval (rec_ex2 f) [x, y1, y2] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval (rec_ex2 f) [x, y1, y2] = (if \<exists>z\<le>x. 0 < rec_eval f [z, y1, y2] then 1 else 0)
[PROOF STEP]
by (simp add: rec_ex2_def)


[STATEMENT]
lemma all1_lemma [simp]:
  "rec_eval (rec_all1 f) [x, y] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval (rec_all1 f) [x, y] = (if \<forall>z\<le>x. 0 < rec_eval f [z, y] then 1 else 0)
[PROOF STEP]
by (simp add: rec_all1_def)


[STATEMENT]
lemma all2_lemma [simp]:
  "rec_eval (rec_all2 f) [x, y1, y2] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval (rec_all2 f) [x, y1, y2] = (if \<forall>z\<le>x. 0 < rec_eval f [z, y1, y2] then 1 else 0)
[PROOF STEP]
by (simp add: rec_all2_def)


[STATEMENT]
lemma all3_lemma [simp]:
  "rec_eval (rec_all3 f) [x, y1, y2, y3] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2, y3]) then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval (rec_all3 f) [x, y1, y2, y3] = (if \<forall>z\<le>x. 0 < rec_eval f [z, y1, y2, y3] then 1 else 0)
[PROOF STEP]
by (simp add: rec_all3_def)


[STATEMENT]
lemma all1_less_lemma [simp]:
  "rec_eval (rec_all1_less f) [x, y] = (if (\<forall>z < x. 0 < rec_eval f [z, y]) then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval (rec_all1_less f) [x, y] = (if \<forall>z<x. 0 < rec_eval f [z, y] then 1 else 0)
[PROOF STEP]
apply(auto simp add: Let_def rec_all1_less_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>\<forall>z\<le>x. z = x \<or> 0 < rec_eval f [z, y]; z < x; rec_eval f [z, y] = 0\<rbrakk> \<Longrightarrow> \<exists>z\<le>x. z \<noteq> x \<and> rec_eval f [z, y] = 0
 2. \<And>z. \<lbrakk>z \<le> x; z \<noteq> x; rec_eval f [z, y] = 0\<rbrakk> \<Longrightarrow> \<exists>z<x. rec_eval f [z, y] = 0
[PROOF STEP]
apply (metis nat_less_le)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma all2_less_lemma [simp]:
  "rec_eval (rec_all2_less f) [x, y1, y2] = (if (\<forall>z < x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval (rec_all2_less f) [x, y1, y2] = (if \<forall>z<x. 0 < rec_eval f [z, y1, y2] then 1 else 0)
[PROOF STEP]
apply(auto simp add: Let_def rec_all2_less_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>\<forall>z\<le>x. z = x \<or> 0 < rec_eval f [z, y1, y2]; z < x; rec_eval f [z, y1, y2] = 0\<rbrakk> \<Longrightarrow> \<exists>z\<le>x. z \<noteq> x \<and> rec_eval f [z, y1, y2] = 0
 2. \<And>z. \<lbrakk>z \<le> x; z \<noteq> x; rec_eval f [z, y1, y2] = 0\<rbrakk> \<Longrightarrow> \<exists>z<x. rec_eval f [z, y1, y2] = 0
[PROOF STEP]
apply(metis nat_less_le)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Quo0:
  shows "Quo 0 y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Quo 0 y = 0
[PROOF STEP]
by (induct y) (auto)


[STATEMENT]
lemma Quo1:
  "x * (Quo x y) \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * Quo x y \<le> y
[PROOF STEP]
by (induct y) (simp_all)


[STATEMENT]
lemma Quo2:
  "b * (Quo b a) + a mod b = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b * Quo b a + a mod b = a
[PROOF STEP]
by (induct a) (auto simp add: mod_Suc)


[STATEMENT]
lemma Quo3:
  "n * (Quo n m) = m - m mod n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n * Quo n m = m - m mod n
[PROOF STEP]
using Quo2[of n m]
[PROOF STATE]
proof (prove)
using this:
n * Quo n m + m mod n = m

goal (1 subgoal):
 1. n * Quo n m = m - m mod n
[PROOF STEP]
by (auto)


[STATEMENT]
lemma Quo4:
  assumes h: "0 < x"
  shows "y < x + x * Quo x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y < x + x * Quo x y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y < x + x * Quo x y
[PROOF STEP]
have "x - (y mod x) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < x - y mod x
[PROOF STEP]
using mod_less_divisor assms
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> ?m mod ?n < ?n
0 < x

goal (1 subgoal):
 1. 0 < x - y mod x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < x - y mod x

goal (1 subgoal):
 1. y < x + x * Quo x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < x - y mod x
[PROOF STEP]
have "y < y + (x - (y mod x))"
[PROOF STATE]
proof (prove)
using this:
0 < x - y mod x

goal (1 subgoal):
 1. y < y + (x - y mod x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y < y + (x - y mod x)

goal (1 subgoal):
 1. y < x + x * Quo x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y < y + (x - y mod x)
[PROOF STEP]
have "y < x + (y - (y mod x))"
[PROOF STATE]
proof (prove)
using this:
y < y + (x - y mod x)

goal (1 subgoal):
 1. y < x + (y - y mod x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y < x + (y - y mod x)

goal (1 subgoal):
 1. y < x + x * Quo x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y < x + (y - y mod x)
[PROOF STEP]
show "y < x + x * (Quo x y)"
[PROOF STATE]
proof (prove)
using this:
y < x + (y - y mod x)

goal (1 subgoal):
 1. y < x + x * Quo x y
[PROOF STEP]
by (simp add: Quo3)
[PROOF STATE]
proof (state)
this:
y < x + x * Quo x y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Quo_div:
  shows "Quo x y = y div x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Quo x y = y div x
[PROOF STEP]
by (metis Quo0 Quo1 Quo4 div_by_0 div_nat_eqI mult_Suc_right neq0_conv)


[STATEMENT]
lemma Quo_rec_quo:
  shows "rec_eval rec_quo [y, x] = Quo x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_quo [y, x] = Quo x y
[PROOF STEP]
by (induct y) (simp_all add: rec_quo_def)


[STATEMENT]
lemma quo_lemma [simp]:
  shows "rec_eval rec_quo [y, x] = y div x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_quo [y, x] = y div x
[PROOF STEP]
by (simp add: Quo_div Quo_rec_quo)


[STATEMENT]
lemma Iter_comm:
  "(Iter f n) (f x) = f ((Iter f n) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Iter f n (f x) = f (Iter f n x)
[PROOF STEP]
by (induct n) (simp_all)


[STATEMENT]
lemma iter_lemma [simp]:
  "rec_eval (rec_iter f) [n, x] =  Iter (\<lambda>x. rec_eval f [x]) n x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval (rec_iter f) [n, x] = Iter (\<lambda>x. rec_eval f [x]) n x
[PROOF STEP]
by (induct n) (simp_all add: rec_iter_def)


[STATEMENT]
lemma BMax_rec_eq1:
  "BMax_rec R x = (GREATEST z. (R z \<and> z \<le> x) \<or> z = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BMax_rec R x = (GREATEST z. R z \<and> z \<le> x \<or> z = 0)
[PROOF STEP]
apply(induct x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. BMax_rec R 0 = (GREATEST z. R z \<and> z \<le> 0 \<or> z = 0)
 2. \<And>x. BMax_rec R x = (GREATEST z. R z \<and> z \<le> x \<or> z = 0) \<Longrightarrow> BMax_rec R (Suc x) = (GREATEST z. R z \<and> z \<le> Suc x \<or> z = 0)
[PROOF STEP]
apply(auto intro: Greatest_equality Greatest_equality[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>BMax_rec R x = (GREATEST z. R z \<and> z \<le> x \<or> z = 0); \<not> R (Suc x)\<rbrakk> \<Longrightarrow> (GREATEST z. R z \<and> z \<le> x \<or> z = 0) = (GREATEST z. R z \<and> z \<le> Suc x \<or> z = 0)
[PROOF STEP]
apply(simp add: le_Suc_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>BMax_rec R x = (GREATEST z. R z \<and> z \<le> x \<or> z = 0); \<not> R (Suc x)\<rbrakk> \<Longrightarrow> (GREATEST z. R z \<and> z \<le> x \<or> z = 0) = (GREATEST z. R z \<and> (z \<le> x \<or> z = Suc x) \<or> z = 0)
[PROOF STEP]
by metis


[STATEMENT]
lemma BMax_rec_eq2:
  "BMax_rec R x = Max ({z. z \<le> x \<and> R z} \<union> {0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BMax_rec R x = Max ({z. z \<le> x \<and> R z} \<union> {0})
[PROOF STEP]
apply(induct x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. BMax_rec R 0 = Max ({z. z \<le> 0 \<and> R z} \<union> {0})
 2. \<And>x. BMax_rec R x = Max ({z. z \<le> x \<and> R z} \<union> {0}) \<Longrightarrow> BMax_rec R (Suc x) = Max ({z. z \<le> Suc x \<and> R z} \<union> {0})
[PROOF STEP]
apply(auto intro: Max_eqI Max_eqI[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>BMax_rec R x = Max (insert 0 {z. z \<le> x \<and> R z}); \<not> R (Suc x)\<rbrakk> \<Longrightarrow> Max (insert 0 {z. z \<le> x \<and> R z}) = Max (insert 0 {z. z \<le> Suc x \<and> R z})
[PROOF STEP]
apply(simp add: le_Suc_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>BMax_rec R x = Max (insert 0 {z. z \<le> x \<and> R z}); \<not> R (Suc x)\<rbrakk> \<Longrightarrow> Max (insert 0 {z. z \<le> x \<and> R z}) = Max (insert 0 {z. (z \<le> x \<or> z = Suc x) \<and> R z})
[PROOF STEP]
by metis


[STATEMENT]
lemma BMax_rec_eq3:
  "BMax_rec R x = Max (Set.filter (\<lambda>z. R z) {..x} \<union> {0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BMax_rec R x = Max (Set.filter R {..x} \<union> {0})
[PROOF STEP]
by (simp add: BMax_rec_eq2 Set.filter_def)


[STATEMENT]
lemma max1_lemma [simp]:
  "rec_eval (rec_max1 f) [x, y] = BMax_rec (\<lambda>u. rec_eval f [u, y] = 0) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval (rec_max1 f) [x, y] = BMax_rec (\<lambda>u. rec_eval f [u, y] = 0) x
[PROOF STEP]
by (induct x) (simp_all add: rec_max1_def)


[STATEMENT]
lemma max2_lemma [simp]:
  "rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x
[PROOF STEP]
by (induct x) (simp_all add: rec_max2_def)


[STATEMENT]
lemma fst_prod_decode:
  "pdec1 z = z - triangle (Max_triangle z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pdec1 z = z - triangle (Max_triangle z)
[PROOF STEP]
by (subst (3) prod_decode_inverse[symmetric])
    (simp add: prod_encode_def prod_decode_def split: prod.split)


[STATEMENT]
lemma snd_prod_decode:
  "pdec2 z = Max_triangle z - pdec1 z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pdec2 z = Max_triangle z - pdec1 z
[PROOF STEP]
by (simp only: prod_decode_def)


[STATEMENT]
lemma le_triangle:
  "m \<le> triangle (n + m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> triangle (n + m)
[PROOF STEP]
by (induct m) (simp_all)


[STATEMENT]
lemma Max_triangle_triangle_le:
  "triangle (Max_triangle z) \<le> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triangle (Max_triangle z) \<le> z
[PROOF STEP]
by (subst (9) prod_decode_inverse[symmetric])
    (simp add: prod_decode_def prod_encode_def split: prod.split)


[STATEMENT]
lemma Max_triangle_le:
  "Max_triangle z \<le> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max_triangle z \<le> z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Max_triangle z \<le> z
[PROOF STEP]
have "Max_triangle z \<le> triangle (Max_triangle z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max_triangle z \<le> triangle (Max_triangle z)
[PROOF STEP]
using le_triangle[of _ 0, simplified]
[PROOF STATE]
proof (prove)
using this:
?m \<le> triangle ?m

goal (1 subgoal):
 1. Max_triangle z \<le> triangle (Max_triangle z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Max_triangle z \<le> triangle (Max_triangle z)

goal (1 subgoal):
 1. Max_triangle z \<le> z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Max_triangle z \<le> triangle (Max_triangle z)

goal (1 subgoal):
 1. Max_triangle z \<le> z
[PROOF STEP]
have "... \<le> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triangle (Max_triangle z) \<le> z
[PROOF STEP]
by (rule Max_triangle_triangle_le)
[PROOF STATE]
proof (state)
this:
triangle (Max_triangle z) \<le> z

goal (1 subgoal):
 1. Max_triangle z \<le> z
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Max_triangle z \<le> z
[PROOF STEP]
show "Max_triangle z \<le> z"
[PROOF STATE]
proof (prove)
using this:
Max_triangle z \<le> z

goal (1 subgoal):
 1. Max_triangle z \<le> z
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Max_triangle z \<le> z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma w_aux:
  "Max_triangle (triangle k + m) = Max_triangle_aux k m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max_triangle (triangle k + m) = Max_triangle_aux k m
[PROOF STEP]
by (simp add: prod_decode_def[symmetric] prod_decode_triangle_add)


[STATEMENT]
lemma y_aux: "y \<le> Max_triangle_aux y k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> Max_triangle_aux y k
[PROOF STEP]
apply(induct k arbitrary: y rule: nat_less_induct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n y. \<forall>m<n. \<forall>x. x \<le> Max_triangle_aux x m \<Longrightarrow> y \<le> Max_triangle_aux y n
[PROOF STEP]
apply(subst (1 2) prod_decode_aux.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n y. \<forall>m<n. \<forall>x. x \<le> Max_triangle_aux x m \<Longrightarrow> y \<le> fst (if n \<le> y then (n, y - n) else prod_decode_aux (Suc y) (n - Suc y)) + snd (if n \<le> y then (n, y - n) else prod_decode_aux (Suc y) (n - Suc y))
[PROOF STEP]
by(auto dest!:spec mp elim:Suc_leD)


[STATEMENT]
lemma Max_triangle_greatest:
  "Max_triangle z = (GREATEST k. (triangle k \<le> z \<and> k \<le> z) \<or> k = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max_triangle z = (GREATEST k. triangle k \<le> z \<and> k \<le> z \<or> k = 0)
[PROOF STEP]
apply(rule Greatest_equality[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. triangle (Max_triangle z) \<le> z \<and> Max_triangle z \<le> z \<or> Max_triangle z = 0
 2. \<And>y. triangle y \<le> z \<and> y \<le> z \<or> y = 0 \<Longrightarrow> y \<le> Max_triangle z
[PROOF STEP]
apply(rule disjI1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. triangle (Max_triangle z) \<le> z \<and> Max_triangle z \<le> z
 2. \<And>y. triangle y \<le> z \<and> y \<le> z \<or> y = 0 \<Longrightarrow> y \<le> Max_triangle z
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. triangle (Max_triangle z) \<le> z
 2. Max_triangle z \<le> z
 3. \<And>y. triangle y \<le> z \<and> y \<le> z \<or> y = 0 \<Longrightarrow> y \<le> Max_triangle z
[PROOF STEP]
apply(rule Max_triangle_triangle_le)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Max_triangle z \<le> z
 2. \<And>y. triangle y \<le> z \<and> y \<le> z \<or> y = 0 \<Longrightarrow> y \<le> Max_triangle z
[PROOF STEP]
apply(rule Max_triangle_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. triangle y \<le> z \<and> y \<le> z \<or> y = 0 \<Longrightarrow> y \<le> Max_triangle z
[PROOF STEP]
apply(erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y. triangle y \<le> z \<and> y \<le> z \<Longrightarrow> y \<le> Max_triangle z
 2. \<And>y. y = 0 \<Longrightarrow> y \<le> Max_triangle z
[PROOF STEP]
apply(erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>triangle y \<le> z; y \<le> z\<rbrakk> \<Longrightarrow> y \<le> Max_triangle z
 2. \<And>y. y = 0 \<Longrightarrow> y \<le> Max_triangle z
[PROOF STEP]
apply(subst (asm) (1) le_iff_add)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>\<exists>c. z = triangle y + c; y \<le> z\<rbrakk> \<Longrightarrow> y \<le> Max_triangle z
 2. \<And>y. y = 0 \<Longrightarrow> y \<le> Max_triangle z
[PROOF STEP]
apply(erule exE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y c. \<lbrakk>y \<le> z; z = triangle y + c\<rbrakk> \<Longrightarrow> y \<le> Max_triangle z
 2. \<And>y. y = 0 \<Longrightarrow> y \<le> Max_triangle z
[PROOF STEP]
apply(clarify)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y c. \<lbrakk>y \<le> triangle y + c; z = triangle y + c\<rbrakk> \<Longrightarrow> y \<le> Max_triangle (triangle y + c)
 2. \<And>y. y = 0 \<Longrightarrow> y \<le> Max_triangle z
[PROOF STEP]
apply(simp only: w_aux)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y c. \<lbrakk>y \<le> triangle y + c; z = triangle y + c\<rbrakk> \<Longrightarrow> y \<le> Max_triangle_aux y c
 2. \<And>y. y = 0 \<Longrightarrow> y \<le> Max_triangle z
[PROOF STEP]
apply(rule y_aux)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y = 0 \<Longrightarrow> y \<le> Max_triangle z
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma triangle_lemma [simp]:
  "rec_eval rec_triangle [x] = triangle x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_triangle [x] = triangle x
[PROOF STEP]
by (simp add: rec_triangle_def triangle_def)


[STATEMENT]
lemma max_triangle_lemma [simp]:
  "rec_eval rec_max_triangle [x] = Max_triangle x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_max_triangle [x] = Max_triangle x
[PROOF STEP]
by (simp add: Max_triangle_greatest rec_max_triangle_def Let_def BMax_rec_eq1)


[STATEMENT]
lemma pdec1_lemma [simp]:
  "rec_eval rec_pdec1 [z] = pdec1 z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_pdec1 [z] = pdec1 z
[PROOF STEP]
by (simp add: rec_pdec1_def fst_prod_decode)


[STATEMENT]
lemma pdec2_lemma [simp]:
  "rec_eval rec_pdec2 [z] = pdec2 z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_pdec2 [z] = pdec2 z
[PROOF STEP]
by (simp add: rec_pdec2_def snd_prod_decode)


[STATEMENT]
lemma penc_lemma [simp]:
  "rec_eval rec_penc [m, n] = penc m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_penc [m, n] = penc m n
[PROOF STEP]
by (simp add: rec_penc_def prod_encode_def)


[STATEMENT]
lemma pdec_zero_simps [simp]:
  "pdec1 0 = 0"
  "pdec2 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pdec1 0 = 0 &&& pdec2 0 = 0
[PROOF STEP]
by (simp_all add: prod_decode_def prod_decode_aux.simps)


[STATEMENT]
lemma ldec_zero:
  "ldec 0 n = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ldec 0 n = 0
[PROOF STEP]
by (induct n) (simp_all add: prod_decode_def prod_decode_aux.simps)


[STATEMENT]
lemma list_encode_inverse:
  "ldec (lenc xs) n = (if n < length xs then xs ! n else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ldec (lenc xs) n = (if n < length xs then xs ! n else 0)
[PROOF STEP]
by (induct xs arbitrary: n rule: lenc.induct)
    (auto simp add: ldec_zero nth_Cons split: nat.splits)


[STATEMENT]
lemma lenc_length_le:
  "length xs \<le> lenc xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs \<le> lenc xs
[PROOF STEP]
by (induct xs) (simp_all add: prod_encode_def)


[STATEMENT]
lemma inside_False [simp]:
  "inside 0 n = False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inside 0 n = False
[PROOF STEP]
by (induct n) (simp_all)


[STATEMENT]
lemma inside_length [simp]:
  "inside (lenc xs) s = (s < length xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inside (lenc xs) s = (s < length xs)
[PROOF STEP]
proof(induct s arbitrary: xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs. inside (lenc xs) 0 = (0 < length xs)
 2. \<And>s xs. (\<And>xs. inside (lenc xs) s = (s < length xs)) \<Longrightarrow> inside (lenc xs) (Suc s) = (Suc s < length xs)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>xs. inside (lenc xs) 0 = (0 < length xs)
 2. \<And>s xs. (\<And>xs. inside (lenc xs) s = (s < length xs)) \<Longrightarrow> inside (lenc xs) (Suc s) = (Suc s < length xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inside (lenc xs) 0 = (0 < length xs)
[PROOF STEP]
by (cases xs) (simp_all add: prod_encode_def)
[PROOF STATE]
proof (state)
this:
inside (lenc xs) 0 = (0 < length xs)

goal (1 subgoal):
 1. \<And>s xs. (\<And>xs. inside (lenc xs) s = (s < length xs)) \<Longrightarrow> inside (lenc xs) (Suc s) = (Suc s < length xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s xs. (\<And>xs. inside (lenc xs) s = (s < length xs)) \<Longrightarrow> inside (lenc xs) (Suc s) = (Suc s < length xs)
[PROOF STEP]
case (Suc s)
[PROOF STATE]
proof (state)
this:
inside (lenc ?xs) s = (s < length ?xs)

goal (1 subgoal):
 1. \<And>s xs. (\<And>xs. inside (lenc xs) s = (s < length xs)) \<Longrightarrow> inside (lenc xs) (Suc s) = (Suc s < length xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inside (lenc ?xs) s = (s < length ?xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
inside (lenc ?xs) s = (s < length ?xs)

goal (1 subgoal):
 1. inside (lenc xs) (Suc s) = (Suc s < length xs)
[PROOF STEP]
by (cases xs;auto)
[PROOF STATE]
proof (state)
this:
inside (lenc xs) (Suc s) = (Suc s < length xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma enclen_length [simp]:
  "enclen (lenc xs) = length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enclen (lenc xs) = length xs
[PROOF STEP]
unfolding enclen_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BMax_rec (\<lambda>x. inside (lenc xs) (x - 1)) (lenc xs) = length xs
[PROOF STEP]
apply(simp add: BMax_rec_eq1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST z. z - 1 < length xs \<and> z \<le> lenc xs \<or> z = 0) = length xs
[PROOF STEP]
apply(rule Greatest_equality)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length xs - 1 < length xs \<and> length xs \<le> lenc xs \<or> length xs = 0
 2. \<And>y. y - 1 < length xs \<and> y \<le> lenc xs \<or> y = 0 \<Longrightarrow> y \<le> length xs
[PROOF STEP]
apply(auto simp add: lenc_length_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma enclen_penc [simp]:
  "enclen (penc (Suc x) (lenc xs)) = Suc (enclen (lenc xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enclen (penc (Suc x) (lenc xs)) = Suc (enclen (lenc xs))
[PROOF STEP]
by (simp only: lenc.simps[symmetric] enclen_length) (simp)


[STATEMENT]
lemma enclen_zero [simp]:
  "enclen 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enclen 0 = 0
[PROOF STEP]
by (simp add: enclen_def)


[STATEMENT]
lemma ldec_iter:
  "ldec z n = pdec1 (Iter pdec2 n z) - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ldec z n = pdec1 (Iter pdec2 n z) - 1
[PROOF STEP]
by (induct n arbitrary: z) (simp | subst Iter_comm)+


[STATEMENT]
lemma inside_iter:
  "inside z n = (0 < Iter pdec2 n z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inside z n = (0 < Iter pdec2 n z)
[PROOF STEP]
by (induct n arbitrary: z) (simp | subst Iter_comm)+


[STATEMENT]
lemma lenc_lemma [simp]:
  "rec_eval (rec_lenc fs) xs = lenc (map (\<lambda>f. rec_eval f xs) fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval (rec_lenc fs) xs = lenc (map (\<lambda>f. rec_eval f xs) fs)
[PROOF STEP]
by (induct fs) (simp_all)


[STATEMENT]
lemma ldec_lemma [simp]:
  "rec_eval rec_ldec [z, n] = ldec z n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_ldec [z, n] = ldec z n
[PROOF STEP]
by (simp add: ldec_iter rec_ldec_def)


[STATEMENT]
lemma inside_lemma [simp]:
  "rec_eval rec_inside [z, n] = (if inside z n then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_inside [z, n] = (if inside z n then 1 else 0)
[PROOF STEP]
by (simp add: inside_iter rec_inside_def)


[STATEMENT]
lemma enclen_lemma [simp]:
  "rec_eval rec_enclen [z] = enclen z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_eval rec_enclen [z] = enclen z
[PROOF STEP]
by (simp add: rec_enclen_def enclen_def)