[STATEMENT]
lemma out_next_subseqs:
  assumes inv: "invariant base elements n state"
      and nxt: "next_subseqs state = (out, state')"
  shows "set out = S base elements (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set out = S base elements (Suc n)
[PROOF STEP]
proof (cases state)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c. state = (a, b, c) \<Longrightarrow> set out = S base elements (Suc n)
[PROOF STEP]
case state: (fields head tail prevs)
[PROOF STATE]
proof (state)
this:
state = (head, tail, prevs)

goal (1 subgoal):
 1. \<And>a b c. state = (a, b, c) \<Longrightarrow> set out = S base elements (Suc n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set out = S base elements (Suc n)
[PROOF STEP]
proof(cases "elements = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. elements = [] \<Longrightarrow> set out = S base elements (Suc n)
 2. elements \<noteq> [] \<Longrightarrow> set out = S base elements (Suc n)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
elements = []

goal (2 subgoals):
 1. elements = [] \<Longrightarrow> set out = S base elements (Suc n)
 2. elements \<noteq> [] \<Longrightarrow> set out = S base elements (Suc n)
[PROOF STEP]
with inv nxt
[PROOF STATE]
proof (chain)
picking this:
invariant base elements n state
local.next_subseqs state = (out, state')
elements = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
invariant base elements n state
local.next_subseqs state = (out, state')
elements = []

goal (1 subgoal):
 1. set out = S base elements (Suc n)
[PROOF STEP]
by (auto simp: state S_def)
[PROOF STATE]
proof (state)
this:
set out = S base elements (Suc n)

goal (1 subgoal):
 1. elements \<noteq> [] \<Longrightarrow> set out = S base elements (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. elements \<noteq> [] \<Longrightarrow> set out = S base elements (Suc n)
[PROOF STEP]
case elements: False
[PROOF STATE]
proof (state)
this:
elements \<noteq> []

goal (1 subgoal):
 1. elements \<noteq> [] \<Longrightarrow> set out = S base elements (Suc n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set out = S base elements (Suc n)
[PROOF STEP]
proof(cases state')
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c. state' = (a, b, c) \<Longrightarrow> set out = S base elements (Suc n)
[PROOF STEP]
case state': (fields head' tail' prevs')
[PROOF STATE]
proof (state)
this:
state' = (head', tail', prevs')

goal (1 subgoal):
 1. \<And>a b c. state' = (a, b, c) \<Longrightarrow> set out = S base elements (Suc n)
[PROOF STEP]
from elements inv[unfolded state,simplified]
[PROOF STATE]
proof (chain)
picking this:
elements \<noteq> []
if elements = [] then prevs = [] else head = hd elements \<and> tail = IArray (tl elements) \<and> set prevs = set_prevs base (tl elements) n
[PROOF STEP]
have "head = hd elements"
       and "tail = IArray (tl elements)"
       and prevs: "set prevs = set_prevs base (tl elements) n"
[PROOF STATE]
proof (prove)
using this:
elements \<noteq> []
if elements = [] then prevs = [] else head = hd elements \<and> tail = IArray (tl elements) \<and> set prevs = set_prevs base (tl elements) n

goal (1 subgoal):
 1. head = hd elements &&& tail = IArray (tl elements) &&& set prevs = set_prevs base (tl elements) n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
head = hd elements
tail = IArray (tl elements)
set prevs = set_prevs base (tl elements) n

goal (1 subgoal):
 1. \<And>a b c. state' = (a, b, c) \<Longrightarrow> set out = S base elements (Suc n)
[PROOF STEP]
with elements
[PROOF STATE]
proof (chain)
picking this:
elements \<noteq> []
head = hd elements
tail = IArray (tl elements)
set prevs = set_prevs base (tl elements) n
[PROOF STEP]
have elements2: "elements = head # IArray.list_of tail"
[PROOF STATE]
proof (prove)
using this:
elements \<noteq> []
head = hd elements
tail = IArray (tl elements)
set prevs = set_prevs base (tl elements) n

goal (1 subgoal):
 1. elements = head # IArray.list_of tail
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
elements = head # IArray.list_of tail

goal (1 subgoal):
 1. \<And>a b c. state' = (a, b, c) \<Longrightarrow> set out = S base elements (Suc n)
[PROOF STEP]
let ?f = "\<lambda>as. (foldr f as base)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c. state' = (a, b, c) \<Longrightarrow> set out = S base elements (Suc n)
[PROOF STEP]
have "set out = ?f ` {ys. subseq_of_length (Suc n) elements ys}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set out = (\<lambda>as. foldr f as base) ` {ys. subseq_of_length (Suc n) elements ys}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set out = (\<lambda>as. foldr f as base) ` {ys. subseq_of_length (Suc n) elements ys}
[PROOF STEP]
from invariant_next_subseqs[OF inv nxt, unfolded state' invariant.simps if_not_P[OF elements]]
[PROOF STATE]
proof (chain)
picking this:
head' = hd elements \<and> tail' = IArray (tl elements) \<and> set prevs' = set_prevs base (tl elements) (Suc n)
[PROOF STEP]
have tail': "tail' = IArray (tl elements)"
         and prevs': "set prevs' = set_prevs base (tl elements) (Suc n)"
[PROOF STATE]
proof (prove)
using this:
head' = hd elements \<and> tail' = IArray (tl elements) \<and> set prevs' = set_prevs base (tl elements) (Suc n)

goal (1 subgoal):
 1. tail' = IArray (tl elements) &&& set prevs' = set_prevs base (tl elements) (Suc n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tail' = IArray (tl elements)
set prevs' = set_prevs base (tl elements) (Suc n)

goal (1 subgoal):
 1. set out = (\<lambda>as. foldr f as base) ` {ys. subseq_of_length (Suc n) elements ys}
[PROOF STEP]
note next_subseqs_spec(2)[OF nxt[unfolded state state'], unfolded this]
[PROOF STATE]
proof (state)
this:
set out = (f head \<circ> snd) ` set prevs \<union> snd ` set_prevs base (tl elements) (Suc n)

goal (1 subgoal):
 1. set out = (\<lambda>as. foldr f as base) ` {ys. subseq_of_length (Suc n) elements ys}
[PROOF STEP]
note this[folded image_comp, unfolded snd_set_prevs]
[PROOF STATE]
proof (state)
this:
set out = f head ` snd ` set prevs \<union> (\<lambda>as. foldr f as base) ` Collect (subseq_of_length (Suc n) (tl elements))

goal (1 subgoal):
 1. set out = (\<lambda>as. foldr f as base) ` {ys. subseq_of_length (Suc n) elements ys}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set out = f head ` snd ` set prevs \<union> (\<lambda>as. foldr f as base) ` Collect (subseq_of_length (Suc n) (tl elements))

goal (1 subgoal):
 1. set out = (\<lambda>as. foldr f as base) ` {ys. subseq_of_length (Suc n) elements ys}
[PROOF STEP]
note prevs
[PROOF STATE]
proof (state)
this:
set prevs = set_prevs base (tl elements) n

goal (1 subgoal):
 1. set out = (\<lambda>as. foldr f as base) ` {ys. subseq_of_length (Suc n) elements ys}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set prevs = set_prevs base (tl elements) n

goal (1 subgoal):
 1. set out = (\<lambda>as. foldr f as base) ` {ys. subseq_of_length (Suc n) elements ys}
[PROOF STEP]
note snd_set_prevs
[PROOF STATE]
proof (state)
this:
snd ` set_prevs ?base ?tail ?n = (\<lambda>as. foldr f as ?base) ` {as. subseq_of_length ?n ?tail as}

goal (1 subgoal):
 1. set out = (\<lambda>as. foldr f as base) ` {ys. subseq_of_length (Suc n) elements ys}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
snd ` set_prevs ?base ?tail ?n = (\<lambda>as. foldr f as ?base) ` {as. subseq_of_length ?n ?tail as}

goal (1 subgoal):
 1. set out = (\<lambda>as. foldr f as base) ` {ys. subseq_of_length (Suc n) elements ys}
[PROOF STEP]
have "f head ` ?f ` { as. subseq_of_length n (tl elements) as } =
          ?f ` Cons head ` { as. subseq_of_length n (tl elements) as }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f head ` (\<lambda>as. foldr f as base) ` {as. subseq_of_length n (tl elements) as} = (\<lambda>as. foldr f as base) ` (#) head ` {as. subseq_of_length n (tl elements) as}
[PROOF STEP]
by (auto simp: image_def)
[PROOF STATE]
proof (state)
this:
f head ` (\<lambda>as. foldr f as base) ` {as. subseq_of_length n (tl elements) as} = (\<lambda>as. foldr f as base) ` (#) head ` {as. subseq_of_length n (tl elements) as}

goal (1 subgoal):
 1. set out = (\<lambda>as. foldr f as base) ` {ys. subseq_of_length (Suc n) elements ys}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f head ` (\<lambda>as. foldr f as base) ` {as. subseq_of_length n (tl elements) as} = (\<lambda>as. foldr f as base) ` (#) head ` {as. subseq_of_length n (tl elements) as}

goal (1 subgoal):
 1. set out = (\<lambda>as. foldr f as base) ` {ys. subseq_of_length (Suc n) elements ys}
[PROOF STEP]
note image_Un[symmetric]
[PROOF STATE]
proof (state)
this:
?f ` ?A \<union> ?f ` ?B = ?f ` (?A \<union> ?B)

goal (1 subgoal):
 1. set out = (\<lambda>as. foldr f as base) ` {ys. subseq_of_length (Suc n) elements ys}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
?f ` ?A \<union> ?f ` ?B = ?f ` (?A \<union> ?B)

goal (1 subgoal):
 1. set out = (\<lambda>as. foldr f as base) ` {ys. subseq_of_length (Suc n) elements ys}
[PROOF STEP]
have
          "((#) head ` {as. subseq_of_length n (tl elements) as} \<union>
           {as. subseq_of_length (Suc n) (tl elements) as}) =
           {as. subseq_of_length (Suc n) elements as}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (#) head ` {as. subseq_of_length n (tl elements) as} \<union> {as. subseq_of_length (Suc n) (tl elements) as} = {as. subseq_of_length (Suc n) elements as}
[PROOF STEP]
by (unfold subseqs_of_length_Suc_Cons elements2, auto)
[PROOF STATE]
proof (state)
this:
(#) head ` {as. subseq_of_length n (tl elements) as} \<union> {as. subseq_of_length (Suc n) (tl elements) as} = {as. subseq_of_length (Suc n) elements as}

goal (1 subgoal):
 1. set out = (\<lambda>as. foldr f as base) ` {ys. subseq_of_length (Suc n) elements ys}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set out = (\<lambda>as. foldr f as base) ` {as. subseq_of_length (Suc n) elements as}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set out = (\<lambda>as. foldr f as base) ` {as. subseq_of_length (Suc n) elements as}

goal (1 subgoal):
 1. set out = (\<lambda>as. foldr f as base) ` {ys. subseq_of_length (Suc n) elements ys}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set out = (\<lambda>as. foldr f as base) ` {ys. subseq_of_length (Suc n) elements ys}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set out = (\<lambda>as. foldr f as base) ` {ys. subseq_of_length (Suc n) elements ys}

goal (1 subgoal):
 1. \<And>a b c. state' = (a, b, c) \<Longrightarrow> set out = S base elements (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set out = (\<lambda>as. foldr f as base) ` {ys. subseq_of_length (Suc n) elements ys}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set out = (\<lambda>as. foldr f as base) ` {ys. subseq_of_length (Suc n) elements ys}

goal (1 subgoal):
 1. set out = S base elements (Suc n)
[PROOF STEP]
by (auto simp: S_def)
[PROOF STATE]
proof (state)
this:
set out = S base elements (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set out = S base elements (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set out = S base elements (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma create_subseqs:
  "create_subseqs base elements n = (out, state) \<Longrightarrow>
   invariant base elements n state \<and> set out = S base elements n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.create_subseqs base elements n = (out, state) \<Longrightarrow> invariant base elements n state \<and> set out = S base elements n
[PROOF STEP]
proof(induct n arbitrary: out state)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>out state. local.create_subseqs base elements 0 = (out, state) \<Longrightarrow> invariant base elements 0 state \<and> set out = S base elements 0
 2. \<And>n out state. \<lbrakk>\<And>out state. local.create_subseqs base elements n = (out, state) \<Longrightarrow> invariant base elements n state \<and> set out = S base elements n; local.create_subseqs base elements (Suc n) = (out, state)\<rbrakk> \<Longrightarrow> invariant base elements (Suc n) state \<and> set out = S base elements (Suc n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
local.create_subseqs base elements 0 = (out, state)

goal (2 subgoals):
 1. \<And>out state. local.create_subseqs base elements 0 = (out, state) \<Longrightarrow> invariant base elements 0 state \<and> set out = S base elements 0
 2. \<And>n out state. \<lbrakk>\<And>out state. local.create_subseqs base elements n = (out, state) \<Longrightarrow> invariant base elements n state \<and> set out = S base elements n; local.create_subseqs base elements (Suc n) = (out, state)\<rbrakk> \<Longrightarrow> invariant base elements (Suc n) state \<and> set out = S base elements (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.create_subseqs base elements 0 = (out, state)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
local.create_subseqs base elements 0 = (out, state)

goal (1 subgoal):
 1. invariant base elements 0 state \<and> set out = S base elements 0
[PROOF STEP]
by (cases "elements", cases state, auto simp: S_def Let_def set_prevs_def)
[PROOF STATE]
proof (state)
this:
invariant base elements 0 state \<and> set out = S base elements 0

goal (1 subgoal):
 1. \<And>n out state. \<lbrakk>\<And>out state. local.create_subseqs base elements n = (out, state) \<Longrightarrow> invariant base elements n state \<and> set out = S base elements n; local.create_subseqs base elements (Suc n) = (out, state)\<rbrakk> \<Longrightarrow> invariant base elements (Suc n) state \<and> set out = S base elements (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n out state. \<lbrakk>\<And>out state. local.create_subseqs base elements n = (out, state) \<Longrightarrow> invariant base elements n state \<and> set out = S base elements n; local.create_subseqs base elements (Suc n) = (out, state)\<rbrakk> \<Longrightarrow> invariant base elements (Suc n) state \<and> set out = S base elements (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
local.create_subseqs base elements n = (?out10, ?state10) \<Longrightarrow> invariant base elements n ?state10 \<and> set ?out10 = S base elements n
local.create_subseqs base elements (Suc n) = (out, state)

goal (1 subgoal):
 1. \<And>n out state. \<lbrakk>\<And>out state. local.create_subseqs base elements n = (out, state) \<Longrightarrow> invariant base elements n state \<and> set out = S base elements n; local.create_subseqs base elements (Suc n) = (out, state)\<rbrakk> \<Longrightarrow> invariant base elements (Suc n) state \<and> set out = S base elements (Suc n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invariant base elements (Suc n) state \<and> set out = S base elements (Suc n)
[PROOF STEP]
proof (cases "create_subseqs base elements n")
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c d. local.create_subseqs base elements n = (a, b, c, d) \<Longrightarrow> invariant base elements (Suc n) state \<and> set out = S base elements (Suc n)
[PROOF STEP]
case 1: (fields out'' head tail prevs)
[PROOF STATE]
proof (state)
this:
local.create_subseqs base elements n = (out'', head, tail, prevs)

goal (1 subgoal):
 1. \<And>a b c d. local.create_subseqs base elements n = (a, b, c, d) \<Longrightarrow> invariant base elements (Suc n) state \<and> set out = S base elements (Suc n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invariant base elements (Suc n) state \<and> set out = S base elements (Suc n)
[PROOF STEP]
proof (cases "next_subseqs (head, tail, prevs)")
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c d. local.next_subseqs (head, tail, prevs) = (a, b, c, d) \<Longrightarrow> invariant base elements (Suc n) state \<and> set out = S base elements (Suc n)
[PROOF STEP]
case (fields out' head' tail' prevs')
[PROOF STATE]
proof (state)
this:
local.next_subseqs (head, tail, prevs) = (out', head', tail', prevs')

goal (1 subgoal):
 1. \<And>a b c d. local.next_subseqs (head, tail, prevs) = (a, b, c, d) \<Longrightarrow> invariant base elements (Suc n) state \<and> set out = S base elements (Suc n)
[PROOF STEP]
note 2 = this[unfolded next_subseq_preserve[OF this]]
[PROOF STATE]
proof (state)
this:
local.next_subseqs (head, tail, prevs) = (out', head, tail, prevs')

goal (1 subgoal):
 1. \<And>a b c d. local.next_subseqs (head, tail, prevs) = (a, b, c, d) \<Longrightarrow> invariant base elements (Suc n) state \<and> set out = S base elements (Suc n)
[PROOF STEP]
from Suc(2)[unfolded create_subseqs.simps 1 snd_conv 2]
[PROOF STATE]
proof (chain)
picking this:
(out', head, tail, prevs') = (out, state)
[PROOF STEP]
have 3: "out' = out" "state = (head,tail,prevs')"
[PROOF STATE]
proof (prove)
using this:
(out', head, tail, prevs') = (out, state)

goal (1 subgoal):
 1. out' = out &&& state = (head, tail, prevs')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
out' = out
state = (head, tail, prevs')

goal (1 subgoal):
 1. \<And>a b c d. local.next_subseqs (head, tail, prevs) = (a, b, c, d) \<Longrightarrow> invariant base elements (Suc n) state \<and> set out = S base elements (Suc n)
[PROOF STEP]
from Suc(1)[OF 1]
[PROOF STATE]
proof (chain)
picking this:
invariant base elements n (head, tail, prevs) \<and> set out'' = S base elements n
[PROOF STEP]
have inv: "invariant base elements n (head, tail, prevs)"
[PROOF STATE]
proof (prove)
using this:
invariant base elements n (head, tail, prevs) \<and> set out'' = S base elements n

goal (1 subgoal):
 1. invariant base elements n (head, tail, prevs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invariant base elements n (head, tail, prevs)

goal (1 subgoal):
 1. \<And>a b c d. local.next_subseqs (head, tail, prevs) = (a, b, c, d) \<Longrightarrow> invariant base elements (Suc n) state \<and> set out = S base elements (Suc n)
[PROOF STEP]
from out_next_subseqs[OF inv 2] invariant_next_subseqs[OF inv 2]
[PROOF STATE]
proof (chain)
picking this:
set out' = S base elements (Suc n)
invariant base elements (Suc n) (head, tail, prevs')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set out' = S base elements (Suc n)
invariant base elements (Suc n) (head, tail, prevs')

goal (1 subgoal):
 1. invariant base elements (Suc n) state \<and> set out = S base elements (Suc n)
[PROOF STEP]
by (auto simp: 3)
[PROOF STATE]
proof (state)
this:
invariant base elements (Suc n) state \<and> set out = S base elements (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invariant base elements (Suc n) state \<and> set out = S base elements (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invariant base elements (Suc n) state \<and> set out = S base elements (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma impl_correct: "correct_subseqs_foldr_impl f impl invariant"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. correct_subseqs_foldr_impl f impl invariant
[PROOF STEP]
..


[STATEMENT]
lemma auth_seg0_non_empty [simp, intro!]: "auth_seg0 \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. auth_seg0 \<noteq> {}
[PROOF STEP]
by auto


[STATEMENT]
lemma auth_seg0_non_empty_frag [simp, intro!]: "\<exists> info . pfragment info [] auth_seg0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>info. pfragment info [] auth_seg0
[PROOF STEP]
apply(auto simp add: pfragment_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>info zs1 zs2. (info, zs1 @ zs2) \<in> auth_seg0
[PROOF STEP]
by (metis append_Nil2 ASM_empty)


[STATEMENT]
lemma extend_pfragment0:
  assumes "pfragment ainfo (hf2#xs) auth_seg0"
  assumes "ASID hf1 \<in> bad"
  assumes "ASID hf2 \<in> bad"
  shows "pfragment ainfo (hf1#hf2#xs) auth_seg0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pfragment ainfo (hf1 # hf2 # xs) auth_seg0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
pfragment ainfo (hf2 # xs) auth_seg0
ASID hf1 \<in> bad
ASID hf2 \<in> bad

goal (1 subgoal):
 1. pfragment ainfo (hf1 # hf2 # xs) auth_seg0
[PROOF STEP]
by(auto intro!: pfragmentI[of _ "[]" _ _] elim!: pfragmentE intro: ASM_cutoff intro!: ASM_extension)


[STATEMENT]
lemma "\<lbrakk>\<And>hf. hf \<in> set hfs \<Longrightarrow> ASID hf \<in> bad\<rbrakk> \<Longrightarrow> (info, hfs) \<in> auth_seg0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>hf. hf \<in> set hfs \<Longrightarrow> ASID hf \<in> bad) \<Longrightarrow> (info, hfs) \<in> auth_seg0
[PROOF STEP]
apply(induction hfs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<And>hf. hf \<in> set [] \<Longrightarrow> ASID hf \<in> bad) \<Longrightarrow> (info, []) \<in> auth_seg0
 2. \<And>a hfs. \<lbrakk>(\<And>hf. hf \<in> set hfs \<Longrightarrow> ASID hf \<in> bad) \<Longrightarrow> (info, hfs) \<in> auth_seg0; \<And>hf. hf \<in> set (a # hfs) \<Longrightarrow> ASID hf \<in> bad\<rbrakk> \<Longrightarrow> (info, a # hfs) \<in> auth_seg0
[PROOF STEP]
using ASM_empty
[PROOF STATE]
proof (prove)
using this:
(?info, []) \<in> auth_seg0

goal (2 subgoals):
 1. (\<And>hf. hf \<in> set [] \<Longrightarrow> ASID hf \<in> bad) \<Longrightarrow> (info, []) \<in> auth_seg0
 2. \<And>a hfs. \<lbrakk>(\<And>hf. hf \<in> set hfs \<Longrightarrow> ASID hf \<in> bad) \<Longrightarrow> (info, hfs) \<in> auth_seg0; \<And>hf. hf \<in> set (a # hfs) \<Longrightarrow> ASID hf \<in> bad\<rbrakk> \<Longrightarrow> (info, a # hfs) \<in> auth_seg0
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a hfs. \<lbrakk>(\<And>hf. hf \<in> set hfs \<Longrightarrow> ASID hf \<in> bad) \<Longrightarrow> (info, hfs) \<in> auth_seg0; \<And>hf. hf \<in> set (a # hfs) \<Longrightarrow> ASID hf \<in> bad\<rbrakk> \<Longrightarrow> (info, a # hfs) \<in> auth_seg0
[PROOF STEP]
subgoal for a hfs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<And>hf. hf \<in> set hfs \<Longrightarrow> ASID hf \<in> bad) \<Longrightarrow> (info, hfs) \<in> auth_seg0; \<And>hf. hf \<in> set (a # hfs) \<Longrightarrow> ASID hf \<in> bad\<rbrakk> \<Longrightarrow> (info, a # hfs) \<in> auth_seg0
[PROOF STEP]
apply(cases hfs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<And>hf. hf \<in> set hfs \<Longrightarrow> ASID hf \<in> bad) \<Longrightarrow> (info, hfs) \<in> auth_seg0; \<And>hf. hf \<in> set (a # hfs) \<Longrightarrow> ASID hf \<in> bad; hfs = []\<rbrakk> \<Longrightarrow> (info, a # hfs) \<in> auth_seg0
 2. \<And>aa list. \<lbrakk>(\<And>hf. hf \<in> set hfs \<Longrightarrow> ASID hf \<in> bad) \<Longrightarrow> (info, hfs) \<in> auth_seg0; \<And>hf. hf \<in> set (a # hfs) \<Longrightarrow> ASID hf \<in> bad; hfs = aa # list\<rbrakk> \<Longrightarrow> (info, a # hfs) \<in> auth_seg0
[PROOF STEP]
by(auto intro!: ASM_singleton ASM_extension)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma weak_integer_composition_enum_length:
  "xs \<in> set (weak_integer_composition_enum i l) \<Longrightarrow> length xs = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> set (weak_integer_composition_enum i l) \<Longrightarrow> length xs = l
[PROOF STEP]
proof(induct l arbitrary: xs i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs i. xs \<in> set (weak_integer_composition_enum i 0) \<Longrightarrow> length xs = 0
 2. \<And>l xs i. \<lbrakk>\<And>xs i. xs \<in> set (weak_integer_composition_enum i l) \<Longrightarrow> length xs = l; xs \<in> set (weak_integer_composition_enum i (Suc l))\<rbrakk> \<Longrightarrow> length xs = Suc l
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
xs \<in> set (weak_integer_composition_enum i 0)

goal (2 subgoals):
 1. \<And>xs i. xs \<in> set (weak_integer_composition_enum i 0) \<Longrightarrow> length xs = 0
 2. \<And>l xs i. \<lbrakk>\<And>xs i. xs \<in> set (weak_integer_composition_enum i l) \<Longrightarrow> length xs = l; xs \<in> set (weak_integer_composition_enum i (Suc l))\<rbrakk> \<Longrightarrow> length xs = Suc l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<in> set (weak_integer_composition_enum i 0)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
xs \<in> set (weak_integer_composition_enum i 0)

goal (1 subgoal):
 1. length xs = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length xs = 0

goal (1 subgoal):
 1. \<And>l xs i. \<lbrakk>\<And>xs i. xs \<in> set (weak_integer_composition_enum i l) \<Longrightarrow> length xs = l; xs \<in> set (weak_integer_composition_enum i (Suc l))\<rbrakk> \<Longrightarrow> length xs = Suc l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l xs i. \<lbrakk>\<And>xs i. xs \<in> set (weak_integer_composition_enum i l) \<Longrightarrow> length xs = l; xs \<in> set (weak_integer_composition_enum i (Suc l))\<rbrakk> \<Longrightarrow> length xs = Suc l
[PROOF STEP]
case (Suc l)
[PROOF STATE]
proof (state)
this:
?xs \<in> set (weak_integer_composition_enum ?i l) \<Longrightarrow> length ?xs = l
xs \<in> set (weak_integer_composition_enum i (Suc l))

goal (1 subgoal):
 1. \<And>l xs i. \<lbrakk>\<And>xs i. xs \<in> set (weak_integer_composition_enum i l) \<Longrightarrow> length xs = l; xs \<in> set (weak_integer_composition_enum i (Suc l))\<rbrakk> \<Longrightarrow> length xs = Suc l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?xs \<in> set (weak_integer_composition_enum ?i l) \<Longrightarrow> length ?xs = l
xs \<in> set (weak_integer_composition_enum i (Suc l))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?xs \<in> set (weak_integer_composition_enum ?i l) \<Longrightarrow> length ?xs = l
xs \<in> set (weak_integer_composition_enum i (Suc l))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weak_integer_composition_enum_sum_list:
  "xs \<in> set (weak_integer_composition_enum i l) \<Longrightarrow> sum_list xs = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> set (weak_integer_composition_enum i l) \<Longrightarrow> sum_list xs = i
[PROOF STEP]
proof(induct l arbitrary: xs i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs i. xs \<in> set (weak_integer_composition_enum i 0) \<Longrightarrow> sum_list xs = i
 2. \<And>l xs i. \<lbrakk>\<And>xs i. xs \<in> set (weak_integer_composition_enum i l) \<Longrightarrow> sum_list xs = i; xs \<in> set (weak_integer_composition_enum i (Suc l))\<rbrakk> \<Longrightarrow> sum_list xs = i
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
xs \<in> set (weak_integer_composition_enum i 0)

goal (2 subgoals):
 1. \<And>xs i. xs \<in> set (weak_integer_composition_enum i 0) \<Longrightarrow> sum_list xs = i
 2. \<And>l xs i. \<lbrakk>\<And>xs i. xs \<in> set (weak_integer_composition_enum i l) \<Longrightarrow> sum_list xs = i; xs \<in> set (weak_integer_composition_enum i (Suc l))\<rbrakk> \<Longrightarrow> sum_list xs = i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<in> set (weak_integer_composition_enum i 0)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
xs \<in> set (weak_integer_composition_enum i 0)

goal (1 subgoal):
 1. sum_list xs = i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum_list xs = i

goal (1 subgoal):
 1. \<And>l xs i. \<lbrakk>\<And>xs i. xs \<in> set (weak_integer_composition_enum i l) \<Longrightarrow> sum_list xs = i; xs \<in> set (weak_integer_composition_enum i (Suc l))\<rbrakk> \<Longrightarrow> sum_list xs = i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l xs i. \<lbrakk>\<And>xs i. xs \<in> set (weak_integer_composition_enum i l) \<Longrightarrow> sum_list xs = i; xs \<in> set (weak_integer_composition_enum i (Suc l))\<rbrakk> \<Longrightarrow> sum_list xs = i
[PROOF STEP]
case (Suc l)
[PROOF STATE]
proof (state)
this:
?xs \<in> set (weak_integer_composition_enum ?i l) \<Longrightarrow> sum_list ?xs = ?i
xs \<in> set (weak_integer_composition_enum i (Suc l))

goal (1 subgoal):
 1. \<And>l xs i. \<lbrakk>\<And>xs i. xs \<in> set (weak_integer_composition_enum i l) \<Longrightarrow> sum_list xs = i; xs \<in> set (weak_integer_composition_enum i (Suc l))\<rbrakk> \<Longrightarrow> sum_list xs = i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?xs \<in> set (weak_integer_composition_enum ?i l) \<Longrightarrow> sum_list ?xs = ?i
xs \<in> set (weak_integer_composition_enum i (Suc l))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?xs \<in> set (weak_integer_composition_enum ?i l) \<Longrightarrow> sum_list ?xs = ?i
xs \<in> set (weak_integer_composition_enum i (Suc l))

goal (1 subgoal):
 1. sum_list xs = i
[PROOF STEP]
by(cases l) auto
[PROOF STATE]
proof (state)
this:
sum_list xs = i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weak_integer_composition_enum_head:
  assumes "xs \<in> set (weak_integer_composition_enum (sum_list xs) (length xs))"
  shows "x # xs \<in> set (weak_integer_composition_enum (x + sum_list xs) (Suc (length xs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x # xs \<in> set (weak_integer_composition_enum (x + sum_list xs) (Suc (length xs)))
[PROOF STEP]
proof(cases "length xs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length xs = 0 \<Longrightarrow> x # xs \<in> set (weak_integer_composition_enum (x + sum_list xs) (Suc (length xs)))
 2. \<And>nat. length xs = Suc nat \<Longrightarrow> x # xs \<in> set (weak_integer_composition_enum (x + sum_list xs) (Suc (length xs)))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
length xs = 0

goal (2 subgoals):
 1. length xs = 0 \<Longrightarrow> x # xs \<in> set (weak_integer_composition_enum (x + sum_list xs) (Suc (length xs)))
 2. \<And>nat. length xs = Suc nat \<Longrightarrow> x # xs \<in> set (weak_integer_composition_enum (x + sum_list xs) (Suc (length xs)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length xs = 0

goal (1 subgoal):
 1. x # xs \<in> set (weak_integer_composition_enum (x + sum_list xs) (Suc (length xs)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x # xs \<in> set (weak_integer_composition_enum (x + sum_list xs) (Suc (length xs)))

goal (1 subgoal):
 1. \<And>nat. length xs = Suc nat \<Longrightarrow> x # xs \<in> set (weak_integer_composition_enum (x + sum_list xs) (Suc (length xs)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. length xs = Suc nat \<Longrightarrow> x # xs \<in> set (weak_integer_composition_enum (x + sum_list xs) (Suc (length xs)))
[PROOF STEP]
case (Suc y)
[PROOF STATE]
proof (state)
this:
length xs = Suc y

goal (1 subgoal):
 1. \<And>nat. length xs = Suc nat \<Longrightarrow> x # xs \<in> set (weak_integer_composition_enum (x + sum_list xs) (Suc (length xs)))
[PROOF STEP]
(*maybe this should be proven elsewhere*)
[PROOF STATE]
proof (state)
this:
length xs = Suc y

goal (1 subgoal):
 1. \<And>nat. length xs = Suc nat \<Longrightarrow> x # xs \<in> set (weak_integer_composition_enum (x + sum_list xs) (Suc (length xs)))
[PROOF STEP]
have 1: "\<lbrakk>n \<in> set xs; 0 < n\<rbrakk> \<Longrightarrow> 0 < sum_list xs" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<in> set xs; 0 < n\<rbrakk> \<Longrightarrow> 0 < sum_list xs
[PROOF STEP]
using sum_list_eq_0_iff
[PROOF STATE]
proof (prove)
using this:
(sum_list ?ns = (0::?'a)) = (\<forall>n\<in>set ?ns. n = (0::?'a))

goal (1 subgoal):
 1. \<lbrakk>n \<in> set xs; 0 < n\<rbrakk> \<Longrightarrow> 0 < sum_list xs
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<lbrakk>?n \<in> set xs; 0 < ?n\<rbrakk> \<Longrightarrow> 0 < sum_list xs

goal (1 subgoal):
 1. \<And>nat. length xs = Suc nat \<Longrightarrow> x # xs \<in> set (weak_integer_composition_enum (x + sum_list xs) (Suc (length xs)))
[PROOF STEP]
have 2: "xs \<notin> set (weak_integer_composition_enum 0 (Suc y)) \<Longrightarrow> 0 < sum_list xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<notin> set (weak_integer_composition_enum 0 (Suc y)) \<Longrightarrow> 0 < sum_list xs
[PROOF STEP]
using Suc assms not_gr0
[PROOF STATE]
proof (prove)
using this:
length xs = Suc y
xs \<in> set (weak_integer_composition_enum (sum_list xs) (length xs))
(\<not> 0 < ?n) = (?n = 0)

goal (1 subgoal):
 1. xs \<notin> set (weak_integer_composition_enum 0 (Suc y)) \<Longrightarrow> 0 < sum_list xs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
xs \<notin> set (weak_integer_composition_enum 0 (Suc y)) \<Longrightarrow> 0 < sum_list xs

goal (1 subgoal):
 1. \<And>nat. length xs = Suc nat \<Longrightarrow> x # xs \<in> set (weak_integer_composition_enum (x + sum_list xs) (Suc (length xs)))
[PROOF STEP]
have "x # xs \<notin> (#) (x + sum_list xs) ` set (weak_integer_composition_enum 0 (Suc y))
    \<Longrightarrow> \<exists>xa\<in>{0..<x + sum_list xs}. x # xs \<in> (#) xa ` set (weak_integer_composition_enum (x + sum_list xs - xa) (Suc y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x # xs \<notin> (#) (x + sum_list xs) ` set (weak_integer_composition_enum 0 (Suc y)) \<Longrightarrow> \<exists>xa\<in>{0..<x + sum_list xs}. x # xs \<in> (#) xa ` set (weak_integer_composition_enum (x + sum_list xs - xa) (Suc y))
[PROOF STEP]
unfolding image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x # xs \<notin> {ya. \<exists>xa\<in>set (weak_integer_composition_enum 0 (Suc y)). ya = (x + sum_list xs) # xa} \<Longrightarrow> \<exists>xa\<in>{0..<x + sum_list xs}. x # xs \<in> {ya. \<exists>x\<in>set (weak_integer_composition_enum (x + sum_list xs - xa) (Suc y)). ya = xa # x}
[PROOF STEP]
using Suc assms 1 2
[PROOF STATE]
proof (prove)
using this:
length xs = Suc y
xs \<in> set (weak_integer_composition_enum (sum_list xs) (length xs))
\<lbrakk>?n \<in> set xs; 0 < ?n\<rbrakk> \<Longrightarrow> 0 < sum_list xs
xs \<notin> set (weak_integer_composition_enum 0 (Suc y)) \<Longrightarrow> 0 < sum_list xs

goal (1 subgoal):
 1. x # xs \<notin> {ya. \<exists>xa\<in>set (weak_integer_composition_enum 0 (Suc y)). ya = (x + sum_list xs) # xa} \<Longrightarrow> \<exists>xa\<in>{0..<x + sum_list xs}. x # xs \<in> {ya. \<exists>x\<in>set (weak_integer_composition_enum (x + sum_list xs - xa) (Suc y)). ya = xa # x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x # xs \<notin> (#) (x + sum_list xs) ` set (weak_integer_composition_enum 0 (Suc y)) \<Longrightarrow> \<exists>xa\<in>{0..<x + sum_list xs}. x # xs \<in> (#) xa ` set (weak_integer_composition_enum (x + sum_list xs - xa) (Suc y))

goal (1 subgoal):
 1. \<And>nat. length xs = Suc nat \<Longrightarrow> x # xs \<in> set (weak_integer_composition_enum (x + sum_list xs) (Suc (length xs)))
[PROOF STEP]
from Suc this
[PROOF STATE]
proof (chain)
picking this:
length xs = Suc y
x # xs \<notin> (#) (x + sum_list xs) ` set (weak_integer_composition_enum 0 (Suc y)) \<Longrightarrow> \<exists>xa\<in>{0..<x + sum_list xs}. x # xs \<in> (#) xa ` set (weak_integer_composition_enum (x + sum_list xs - xa) (Suc y))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length xs = Suc y
x # xs \<notin> (#) (x + sum_list xs) ` set (weak_integer_composition_enum 0 (Suc y)) \<Longrightarrow> \<exists>xa\<in>{0..<x + sum_list xs}. x # xs \<in> (#) xa ` set (weak_integer_composition_enum (x + sum_list xs - xa) (Suc y))

goal (1 subgoal):
 1. x # xs \<in> set (weak_integer_composition_enum (x + sum_list xs) (Suc (length xs)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x # xs \<in> set (weak_integer_composition_enum (x + sum_list xs) (Suc (length xs)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weak_integer_composition_enum_correct_aux:
  "xs \<in> set (weak_integer_composition_enum (sum_list xs) (length xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> set (weak_integer_composition_enum (sum_list xs) (length xs))
[PROOF STEP]
by (induct xs) (auto simp: weak_integer_composition_enum_head)


[STATEMENT]
theorem weak_integer_composition_enum_correct:
  "set (weak_integer_composition_enum i l) = weak_integer_compositions i l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (weak_integer_composition_enum i l) = weak_integer_compositions i l
[PROOF STEP]
proof standard
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set (weak_integer_composition_enum i l) \<subseteq> weak_integer_compositions i l
 2. weak_integer_compositions i l \<subseteq> set (weak_integer_composition_enum i l)
[PROOF STEP]
show "set (weak_integer_composition_enum i l) \<subseteq> weak_integer_compositions i l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (weak_integer_composition_enum i l) \<subseteq> weak_integer_compositions i l
[PROOF STEP]
unfolding weak_integer_compositions_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (weak_integer_composition_enum i l) \<subseteq> {xs. length xs = l \<and> sum_list xs = i}
[PROOF STEP]
using weak_integer_composition_enum_length weak_integer_composition_enum_sum_list
[PROOF STATE]
proof (prove)
using this:
?xs \<in> set (weak_integer_composition_enum ?i ?l) \<Longrightarrow> length ?xs = ?l
?xs \<in> set (weak_integer_composition_enum ?i ?l) \<Longrightarrow> sum_list ?xs = ?i

goal (1 subgoal):
 1. set (weak_integer_composition_enum i l) \<subseteq> {xs. length xs = l \<and> sum_list xs = i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (weak_integer_composition_enum i l) \<subseteq> weak_integer_compositions i l

goal (1 subgoal):
 1. weak_integer_compositions i l \<subseteq> set (weak_integer_composition_enum i l)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. weak_integer_compositions i l \<subseteq> set (weak_integer_composition_enum i l)
[PROOF STEP]
show "weak_integer_compositions i l \<subseteq> set (weak_integer_composition_enum i l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weak_integer_compositions i l \<subseteq> set (weak_integer_composition_enum i l)
[PROOF STEP]
unfolding weak_integer_compositions_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {xs. length xs = l \<and> sum_list xs = i} \<subseteq> set (weak_integer_composition_enum i l)
[PROOF STEP]
using weak_integer_composition_enum_correct_aux
[PROOF STATE]
proof (prove)
using this:
?xs \<in> set (weak_integer_composition_enum (sum_list ?xs) (length ?xs))

goal (1 subgoal):
 1. {xs. length xs = l \<and> sum_list xs = i} \<subseteq> set (weak_integer_composition_enum i l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
weak_integer_compositions i l \<subseteq> set (weak_integer_composition_enum i l)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem weak_integer_composition_enum_distinct: "distinct (weak_integer_composition_enum i l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (weak_integer_composition_enum i l)
[PROOF STEP]
proof(induct rule: weak_integer_composition_enum.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i. distinct (weak_integer_composition_enum i 0)
 2. \<And>i. distinct (weak_integer_composition_enum i (Suc 0))
 3. \<And>i va. (\<And>x. x \<in> set [0..<Suc i] \<Longrightarrow> distinct (weak_integer_composition_enum (i - x) (Suc (Suc va) - 1))) \<Longrightarrow> distinct (weak_integer_composition_enum i (Suc (Suc va)))
[PROOF STEP]
case (1 i)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>i. distinct (weak_integer_composition_enum i 0)
 2. \<And>i. distinct (weak_integer_composition_enum i (Suc 0))
 3. \<And>i va. (\<And>x. x \<in> set [0..<Suc i] \<Longrightarrow> distinct (weak_integer_composition_enum (i - x) (Suc (Suc va) - 1))) \<Longrightarrow> distinct (weak_integer_composition_enum i (Suc (Suc va)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (weak_integer_composition_enum i 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (weak_integer_composition_enum i 0)

goal (2 subgoals):
 1. \<And>i. distinct (weak_integer_composition_enum i (Suc 0))
 2. \<And>i va. (\<And>x. x \<in> set [0..<Suc i] \<Longrightarrow> distinct (weak_integer_composition_enum (i - x) (Suc (Suc va) - 1))) \<Longrightarrow> distinct (weak_integer_composition_enum i (Suc (Suc va)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. distinct (weak_integer_composition_enum i (Suc 0))
 2. \<And>i va. (\<And>x. x \<in> set [0..<Suc i] \<Longrightarrow> distinct (weak_integer_composition_enum (i - x) (Suc (Suc va) - 1))) \<Longrightarrow> distinct (weak_integer_composition_enum i (Suc (Suc va)))
[PROOF STEP]
case (2 i)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>i. distinct (weak_integer_composition_enum i (Suc 0))
 2. \<And>i va. (\<And>x. x \<in> set [0..<Suc i] \<Longrightarrow> distinct (weak_integer_composition_enum (i - x) (Suc (Suc va) - 1))) \<Longrightarrow> distinct (weak_integer_composition_enum i (Suc (Suc va)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (weak_integer_composition_enum i (Suc 0))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (weak_integer_composition_enum i (Suc 0))

goal (1 subgoal):
 1. \<And>i va. (\<And>x. x \<in> set [0..<Suc i] \<Longrightarrow> distinct (weak_integer_composition_enum (i - x) (Suc (Suc va) - 1))) \<Longrightarrow> distinct (weak_integer_composition_enum i (Suc (Suc va)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i va. (\<And>x. x \<in> set [0..<Suc i] \<Longrightarrow> distinct (weak_integer_composition_enum (i - x) (Suc (Suc va) - 1))) \<Longrightarrow> distinct (weak_integer_composition_enum i (Suc (Suc va)))
[PROOF STEP]
case (3 i l)
[PROOF STATE]
proof (state)
this:
?x \<in> set [0..<Suc i] \<Longrightarrow> distinct (weak_integer_composition_enum (i - ?x) (Suc (Suc l) - 1))

goal (1 subgoal):
 1. \<And>i va. (\<And>x. x \<in> set [0..<Suc i] \<Longrightarrow> distinct (weak_integer_composition_enum (i - x) (Suc (Suc va) - 1))) \<Longrightarrow> distinct (weak_integer_composition_enum i (Suc (Suc va)))
[PROOF STEP]
have "distinct [h#r . h \<leftarrow> [0..< Suc i], r \<leftarrow> weak_integer_composition_enum (i-h) (Suc l)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (concat (map (\<lambda>h. map ((#) h) (weak_integer_composition_enum (i - h) (Suc l))) [0..<Suc i]))
[PROOF STEP]
apply(subst Cons_distinct_concat_map_function)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<forall>x\<in>set [0..<Suc i]. distinct (weak_integer_composition_enum (i - x) (Suc l))
 2. distinct [0..<Suc i]
 3. True
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
?x \<in> set [0..<Suc i] \<Longrightarrow> distinct (weak_integer_composition_enum (i - ?x) (Suc (Suc l) - 1))

goal (3 subgoals):
 1. \<forall>x\<in>set [0..<Suc i]. distinct (weak_integer_composition_enum (i - x) (Suc l))
 2. distinct [0..<Suc i]
 3. True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (concat (map (\<lambda>h. map ((#) h) (weak_integer_composition_enum (i - h) (Suc l))) [0..<Suc i]))

goal (1 subgoal):
 1. \<And>i va. (\<And>x. x \<in> set [0..<Suc i] \<Longrightarrow> distinct (weak_integer_composition_enum (i - x) (Suc (Suc va) - 1))) \<Longrightarrow> distinct (weak_integer_composition_enum i (Suc (Suc va)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (concat (map (\<lambda>h. map ((#) h) (weak_integer_composition_enum (i - h) (Suc l))) [0..<Suc i]))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
distinct (concat (map (\<lambda>h. map ((#) h) (weak_integer_composition_enum (i - h) (Suc l))) [0..<Suc i]))

goal (1 subgoal):
 1. distinct (weak_integer_composition_enum i (Suc (Suc l)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (weak_integer_composition_enum i (Suc (Suc l)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weak_integer_composition_enum_zero: "length (weak_integer_composition_enum 0 (Suc n)) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (weak_integer_composition_enum 0 (Suc n)) = 1
[PROOF STEP]
by(induct n) auto


[STATEMENT]
lemma a_choose_equivalence: "Suc (\<Sum>x\<leftarrow>[0..<k]. n + (k - x) choose (k - x)) = Suc (n + k) choose k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (\<Sum>x\<leftarrow>[0..<k]. n + (k - x) choose (k - x)) = Suc (n + k) choose k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc (\<Sum>x\<leftarrow>[0..<k]. n + (k - x) choose (k - x)) = Suc (n + k) choose k
[PROOF STEP]
have "m \<ge> k \<Longrightarrow> (\<Sum>x\<leftarrow>[0..< Suc k]. m - x choose (k - x)) = Suc m choose k" for m
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> m \<Longrightarrow> (\<Sum>x\<leftarrow>[0..<Suc k]. m - x choose (k - x)) = Suc m choose k
[PROOF STEP]
using sum_choose_diagonal leq_sum_to_sum_list
[PROOF STATE]
proof (prove)
using this:
?m \<le> ?n \<Longrightarrow> (\<Sum>k\<le>?m. ?n - k choose (?m - k)) = Suc ?n choose ?m
sum ?f {..?n} = sum_list (map ?f [0..<Suc ?n])

goal (1 subgoal):
 1. k \<le> m \<Longrightarrow> (\<Sum>x\<leftarrow>[0..<Suc k]. m - x choose (k - x)) = Suc m choose k
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
k \<le> ?m \<Longrightarrow> (\<Sum>x\<leftarrow>[0..<Suc k]. ?m - x choose (k - x)) = Suc ?m choose k

goal (1 subgoal):
 1. Suc (\<Sum>x\<leftarrow>[0..<k]. n + (k - x) choose (k - x)) = Suc (n + k) choose k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<le> ?m \<Longrightarrow> (\<Sum>x\<leftarrow>[0..<Suc k]. ?m - x choose (k - x)) = Suc ?m choose k
[PROOF STEP]
have 1: "Suc (\<Sum>x\<leftarrow>[0..<k]. (n + k) - x choose (k - x)) = Suc (n + k) choose k"
[PROOF STATE]
proof (prove)
using this:
k \<le> ?m \<Longrightarrow> (\<Sum>x\<leftarrow>[0..<Suc k]. ?m - x choose (k - x)) = Suc ?m choose k

goal (1 subgoal):
 1. Suc (\<Sum>x\<leftarrow>[0..<k]. n + k - x choose (k - x)) = Suc (n + k) choose k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (\<Sum>x\<leftarrow>[0..<k]. n + k - x choose (k - x)) = Suc (n + k) choose k

goal (1 subgoal):
 1. Suc (\<Sum>x\<leftarrow>[0..<k]. n + (k - x) choose (k - x)) = Suc (n + k) choose k
[PROOF STEP]
have "Suc (\<Sum>x\<leftarrow>[0..<k]. (n + k) - x choose (k - x)) = Suc (\<Sum>x\<leftarrow>[0..<k]. n + (k - x) choose (k - x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (\<Sum>x\<leftarrow>[0..<k]. n + k - x choose (k - x)) = Suc (\<Sum>x\<leftarrow>[0..<k]. n + (k - x) choose (k - x))
[PROOF STEP]
by (metis (no_types, opaque_lifting) Nat.diff_add_assoc2 add.commute binomial_n_0 diff_is_0_eq' nle_le)
[PROOF STATE]
proof (state)
this:
Suc (\<Sum>x\<leftarrow>[0..<k]. n + k - x choose (k - x)) = Suc (\<Sum>x\<leftarrow>[0..<k]. n + (k - x) choose (k - x))

goal (1 subgoal):
 1. Suc (\<Sum>x\<leftarrow>[0..<k]. n + (k - x) choose (k - x)) = Suc (n + k) choose k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Suc (\<Sum>x\<leftarrow>[0..<k]. n + k - x choose (k - x)) = Suc (\<Sum>x\<leftarrow>[0..<k]. n + (k - x) choose (k - x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Suc (\<Sum>x\<leftarrow>[0..<k]. n + k - x choose (k - x)) = Suc (\<Sum>x\<leftarrow>[0..<k]. n + (k - x) choose (k - x))

goal (1 subgoal):
 1. Suc (\<Sum>x\<leftarrow>[0..<k]. n + (k - x) choose (k - x)) = Suc (n + k) choose k
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
Suc (\<Sum>x\<leftarrow>[0..<k]. n + k - x choose (k - x)) = Suc (\<Sum>x\<leftarrow>[0..<k]. n + (k - x) choose (k - x))
Suc (\<Sum>x\<leftarrow>[0..<k]. n + k - x choose (k - x)) = Suc (n + k) choose k

goal (1 subgoal):
 1. Suc (\<Sum>x\<leftarrow>[0..<k]. n + (k - x) choose (k - x)) = Suc (n + k) choose k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (\<Sum>x\<leftarrow>[0..<k]. n + (k - x) choose (k - x)) = Suc (n + k) choose k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma composition_enum_length: "length (weak_integer_composition_enum i n) = n multichoose i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (weak_integer_composition_enum i n) = n multichoose i
[PROOF STEP]
unfolding multichoose_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (weak_integer_composition_enum i n) = n + i - 1 choose i
[PROOF STEP]
proof(induct i n rule: weak_integer_composition_enum.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i. length (weak_integer_composition_enum i 0) = 0 + i - 1 choose i
 2. \<And>i. length (weak_integer_composition_enum i (Suc 0)) = Suc 0 + i - 1 choose i
 3. \<And>i va. (\<And>x. x \<in> set [0..<Suc i] \<Longrightarrow> length (weak_integer_composition_enum (i - x) (Suc (Suc va) - 1)) = Suc (Suc va) - 1 + (i - x) - 1 choose (i - x)) \<Longrightarrow> length (weak_integer_composition_enum i (Suc (Suc va))) = Suc (Suc va) + i - 1 choose i
[PROOF STEP]
case (1 i)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>i. length (weak_integer_composition_enum i 0) = 0 + i - 1 choose i
 2. \<And>i. length (weak_integer_composition_enum i (Suc 0)) = Suc 0 + i - 1 choose i
 3. \<And>i va. (\<And>x. x \<in> set [0..<Suc i] \<Longrightarrow> length (weak_integer_composition_enum (i - x) (Suc (Suc va) - 1)) = Suc (Suc va) - 1 + (i - x) - 1 choose (i - x)) \<Longrightarrow> length (weak_integer_composition_enum i (Suc (Suc va))) = Suc (Suc va) + i - 1 choose i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (weak_integer_composition_enum i 0) = 0 + i - 1 choose i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (weak_integer_composition_enum i 0) = 0 + i - 1 choose i

goal (2 subgoals):
 1. \<And>i. length (weak_integer_composition_enum i (Suc 0)) = Suc 0 + i - 1 choose i
 2. \<And>i va. (\<And>x. x \<in> set [0..<Suc i] \<Longrightarrow> length (weak_integer_composition_enum (i - x) (Suc (Suc va) - 1)) = Suc (Suc va) - 1 + (i - x) - 1 choose (i - x)) \<Longrightarrow> length (weak_integer_composition_enum i (Suc (Suc va))) = Suc (Suc va) + i - 1 choose i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. length (weak_integer_composition_enum i (Suc 0)) = Suc 0 + i - 1 choose i
 2. \<And>i va. (\<And>x. x \<in> set [0..<Suc i] \<Longrightarrow> length (weak_integer_composition_enum (i - x) (Suc (Suc va) - 1)) = Suc (Suc va) - 1 + (i - x) - 1 choose (i - x)) \<Longrightarrow> length (weak_integer_composition_enum i (Suc (Suc va))) = Suc (Suc va) + i - 1 choose i
[PROOF STEP]
case (2 i)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>i. length (weak_integer_composition_enum i (Suc 0)) = Suc 0 + i - 1 choose i
 2. \<And>i va. (\<And>x. x \<in> set [0..<Suc i] \<Longrightarrow> length (weak_integer_composition_enum (i - x) (Suc (Suc va) - 1)) = Suc (Suc va) - 1 + (i - x) - 1 choose (i - x)) \<Longrightarrow> length (weak_integer_composition_enum i (Suc (Suc va))) = Suc (Suc va) + i - 1 choose i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (weak_integer_composition_enum i (Suc 0)) = Suc 0 + i - 1 choose i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (weak_integer_composition_enum i (Suc 0)) = Suc 0 + i - 1 choose i

goal (1 subgoal):
 1. \<And>i va. (\<And>x. x \<in> set [0..<Suc i] \<Longrightarrow> length (weak_integer_composition_enum (i - x) (Suc (Suc va) - 1)) = Suc (Suc va) - 1 + (i - x) - 1 choose (i - x)) \<Longrightarrow> length (weak_integer_composition_enum i (Suc (Suc va))) = Suc (Suc va) + i - 1 choose i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i va. (\<And>x. x \<in> set [0..<Suc i] \<Longrightarrow> length (weak_integer_composition_enum (i - x) (Suc (Suc va) - 1)) = Suc (Suc va) - 1 + (i - x) - 1 choose (i - x)) \<Longrightarrow> length (weak_integer_composition_enum i (Suc (Suc va))) = Suc (Suc va) + i - 1 choose i
[PROOF STEP]
case (3 i n)
[PROOF STATE]
proof (state)
this:
?x \<in> set [0..<Suc i] \<Longrightarrow> length (weak_integer_composition_enum (i - ?x) (Suc (Suc n) - 1)) = Suc (Suc n) - 1 + (i - ?x) - 1 choose (i - ?x)

goal (1 subgoal):
 1. \<And>i va. (\<And>x. x \<in> set [0..<Suc i] \<Longrightarrow> length (weak_integer_composition_enum (i - x) (Suc (Suc va) - 1)) = Suc (Suc va) - 1 + (i - x) - 1 choose (i - x)) \<Longrightarrow> length (weak_integer_composition_enum i (Suc (Suc va))) = Suc (Suc va) + i - 1 choose i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> set [0..<Suc i] \<Longrightarrow> length (weak_integer_composition_enum (i - ?x) (Suc (Suc n) - 1)) = Suc (Suc n) - 1 + (i - ?x) - 1 choose (i - ?x)
[PROOF STEP]
have "x \<in> set [0..< i] \<Longrightarrow>
    length (weak_integer_composition_enum (i - x) (Suc n)) = n + (i - x) choose (i - x)" for x
[PROOF STATE]
proof (prove)
using this:
?x \<in> set [0..<Suc i] \<Longrightarrow> length (weak_integer_composition_enum (i - ?x) (Suc (Suc n) - 1)) = Suc (Suc n) - 1 + (i - ?x) - 1 choose (i - ?x)

goal (1 subgoal):
 1. x \<in> set [0..<i] \<Longrightarrow> length (weak_integer_composition_enum (i - x) (Suc n)) = n + (i - x) choose (i - x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?x \<in> set [0..<i] \<Longrightarrow> length (weak_integer_composition_enum (i - ?x) (Suc n)) = n + (i - ?x) choose (i - ?x)

goal (1 subgoal):
 1. \<And>i va. (\<And>x. x \<in> set [0..<Suc i] \<Longrightarrow> length (weak_integer_composition_enum (i - x) (Suc (Suc va) - 1)) = Suc (Suc va) - 1 + (i - x) - 1 choose (i - x)) \<Longrightarrow> length (weak_integer_composition_enum i (Suc (Suc va))) = Suc (Suc va) + i - 1 choose i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> set [0..<i] \<Longrightarrow> length (weak_integer_composition_enum (i - ?x) (Suc n)) = n + (i - ?x) choose (i - ?x)
[PROOF STEP]
have ev: "length [h#r . h \<leftarrow> [0..< i], r \<leftarrow> weak_integer_composition_enum (i-h) (Suc n)] =
     (\<Sum>x\<leftarrow>[0..< i]. n + (i - x) choose (i - x))"
[PROOF STATE]
proof (prove)
using this:
?x \<in> set [0..<i] \<Longrightarrow> length (weak_integer_composition_enum (i - ?x) (Suc n)) = n + (i - ?x) choose (i - ?x)

goal (1 subgoal):
 1. length (concat (map (\<lambda>h. map ((#) h) (weak_integer_composition_enum (i - h) (Suc n))) [0..<i])) = (\<Sum>x\<leftarrow>[0..<i]. n + (i - x) choose (i - x))
[PROOF STEP]
using length_concat_map_function_sum_list [of
      "[0..< i]"
      "\<lambda>x. (weak_integer_composition_enum (i-x) (Suc n))"
      "\<lambda>x. n + (i-x) choose (i-x)"
      "\<lambda>h r. h#r"
      ]
[PROOF STATE]
proof (prove)
using this:
?x \<in> set [0..<i] \<Longrightarrow> length (weak_integer_composition_enum (i - ?x) (Suc n)) = n + (i - ?x) choose (i - ?x)
(\<And>x. x \<in> set [0..<i] \<Longrightarrow> length (weak_integer_composition_enum (i - x) (Suc n)) = n + (i - x) choose (i - x)) \<Longrightarrow> length (concat (map (\<lambda>x. map ((#) x) (weak_integer_composition_enum (i - x) (Suc n))) [0..<i])) = (\<Sum>x\<leftarrow>[0..<i]. n + (i - x) choose (i - x))

goal (1 subgoal):
 1. length (concat (map (\<lambda>h. map ((#) h) (weak_integer_composition_enum (i - h) (Suc n))) [0..<i])) = (\<Sum>x\<leftarrow>[0..<i]. n + (i - x) choose (i - x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (concat (map (\<lambda>h. map ((#) h) (weak_integer_composition_enum (i - h) (Suc n))) [0..<i])) = (\<Sum>x\<leftarrow>[0..<i]. n + (i - x) choose (i - x))

goal (1 subgoal):
 1. \<And>i va. (\<And>x. x \<in> set [0..<Suc i] \<Longrightarrow> length (weak_integer_composition_enum (i - x) (Suc (Suc va) - 1)) = Suc (Suc va) - 1 + (i - x) - 1 choose (i - x)) \<Longrightarrow> length (weak_integer_composition_enum i (Suc (Suc va))) = Suc (Suc va) + i - 1 choose i
[PROOF STEP]
have "Suc (\<Sum>x\<leftarrow>[0..<i]. n + (i - x) choose (i - x)) = Suc (n + i) choose i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (\<Sum>x\<leftarrow>[0..<i]. n + (i - x) choose (i - x)) = Suc (n + i) choose i
[PROOF STEP]
using a_choose_equivalence
[PROOF STATE]
proof (prove)
using this:
Suc (\<Sum>x\<leftarrow>[0..<?k]. ?n + (?k - x) choose (?k - x)) = Suc (?n + ?k) choose ?k

goal (1 subgoal):
 1. Suc (\<Sum>x\<leftarrow>[0..<i]. n + (i - x) choose (i - x)) = Suc (n + i) choose i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (\<Sum>x\<leftarrow>[0..<i]. n + (i - x) choose (i - x)) = Suc (n + i) choose i

goal (1 subgoal):
 1. \<And>i va. (\<And>x. x \<in> set [0..<Suc i] \<Longrightarrow> length (weak_integer_composition_enum (i - x) (Suc (Suc va) - 1)) = Suc (Suc va) - 1 + (i - x) - 1 choose (i - x)) \<Longrightarrow> length (weak_integer_composition_enum i (Suc (Suc va))) = Suc (Suc va) + i - 1 choose i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Suc (\<Sum>x\<leftarrow>[0..<i]. n + (i - x) choose (i - x)) = Suc (n + i) choose i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Suc (\<Sum>x\<leftarrow>[0..<i]. n + (i - x) choose (i - x)) = Suc (n + i) choose i

goal (1 subgoal):
 1. length (weak_integer_composition_enum i (Suc (Suc n))) = Suc (Suc n) + i - 1 choose i
[PROOF STEP]
using weak_integer_composition_enum_zero ev
[PROOF STATE]
proof (prove)
using this:
Suc (\<Sum>x\<leftarrow>[0..<i]. n + (i - x) choose (i - x)) = Suc (n + i) choose i
length (weak_integer_composition_enum 0 (Suc ?n)) = 1
length (concat (map (\<lambda>h. map ((#) h) (weak_integer_composition_enum (i - h) (Suc n))) [0..<i])) = (\<Sum>x\<leftarrow>[0..<i]. n + (i - x) choose (i - x))

goal (1 subgoal):
 1. length (weak_integer_composition_enum i (Suc (Suc n))) = Suc (Suc n) + i - 1 choose i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (weak_integer_composition_enum i (Suc (Suc n))) = Suc (Suc n) + i - 1 choose i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem weak_integer_compositions_cardinality: "card (weak_integer_compositions n k) = k multichoose n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (weak_integer_compositions n k) = k multichoose n
[PROOF STEP]
using weak_integer_composition_enum_correct weak_integer_composition_enum_distinct composition_enum_length
  distinct_card
[PROOF STATE]
proof (prove)
using this:
set (weak_integer_composition_enum ?i ?l) = weak_integer_compositions ?i ?l
distinct (weak_integer_composition_enum ?i ?l)
length (weak_integer_composition_enum ?i ?n) = ?n multichoose ?i
distinct ?xs \<Longrightarrow> card (set ?xs) = length ?xs

goal (1 subgoal):
 1. card (weak_integer_compositions n k) = k multichoose n
[PROOF STEP]
by metis


[STATEMENT]
lemma wfI_domi:
  assumes "\<Theta> ; \<Gamma> \<turnstile> i"
  shows "fst ` toSet \<Gamma> \<subseteq> dom i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` toSet \<Gamma> \<subseteq> dom i
[PROOF STEP]
using wfI_def toSet.simps assms
[PROOF STATE]
proof (prove)
using this:
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i = (\<forall>(x, b, c)\<in>toSet ?\<Gamma>. \<exists>s. Some s = ?i x \<and>  ?\<Theta>  \<turnstile> s : b)
toSet GNil = {}
toSet (?xbc #\<^sub>\<Gamma> ?G) = {?xbc} \<union> toSet ?G
 \<Theta> ; \<Gamma> \<turnstile> i

goal (1 subgoal):
 1. fst ` toSet \<Gamma> \<subseteq> dom i
[PROOF STEP]
by fastforce


[STATEMENT]
lemma wfI_lookup:
  fixes G::\<Gamma> and b::b
  assumes "Some (b,c) = lookup G x" and "P ; G \<turnstile> i" and "Some s = i x" and "P ; B \<turnstile>\<^sub>w\<^sub>f G"
  shows "P \<turnstile> s : b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  P  \<turnstile> s : b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  P  \<turnstile> s : b
[PROOF STEP]
have "(x,b,c) \<in> toSet G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, b, c) \<in> toSet G
[PROOF STEP]
using lookup.simps assms
[PROOF STATE]
proof (prove)
using this:
lookup GNil ?x = None
lookup ((?x, ?b, ?c) #\<^sub>\<Gamma> ?G) ?y = (if ?x = ?y then Some (?b, ?c) else lookup ?G ?y)
Some (b, c) = lookup G x
 P ; G \<turnstile> i
Some s = i x
 P ; B  \<turnstile>\<^sub>w\<^sub>f G

goal (1 subgoal):
 1. (x, b, c) \<in> toSet G
[PROOF STEP]
using lookup_in_g
[PROOF STATE]
proof (prove)
using this:
lookup GNil ?x = None
lookup ((?x, ?b, ?c) #\<^sub>\<Gamma> ?G) ?y = (if ?x = ?y then Some (?b, ?c) else lookup ?G ?y)
Some (b, c) = lookup G x
 P ; G \<turnstile> i
Some s = i x
 P ; B  \<turnstile>\<^sub>w\<^sub>f G
Some (?b, ?c) = lookup ?\<Gamma> ?x \<Longrightarrow> (?x, ?b, ?c) \<in> toSet ?\<Gamma>

goal (1 subgoal):
 1. (x, b, c) \<in> toSet G
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(x, b, c) \<in> toSet G

goal (1 subgoal):
 1.  P  \<turnstile> s : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, b, c) \<in> toSet G
[PROOF STEP]
obtain s' where *:"Some s' = i x \<and> wfRCV P s' b"
[PROOF STATE]
proof (prove)
using this:
(x, b, c) \<in> toSet G

goal (1 subgoal):
 1. (\<And>s'. Some s' = i x \<and>  P  \<turnstile> s' : b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wfI_def assms
[PROOF STATE]
proof (prove)
using this:
(x, b, c) \<in> toSet G
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i = (\<forall>(x, b, c)\<in>toSet ?\<Gamma>. \<exists>s. Some s = ?i x \<and>  ?\<Theta>  \<turnstile> s : b)
Some (b, c) = lookup G x
 P ; G \<turnstile> i
Some s = i x
 P ; B  \<turnstile>\<^sub>w\<^sub>f G

goal (1 subgoal):
 1. (\<And>s'. Some s' = i x \<and>  P  \<turnstile> s' : b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Some s' = i x \<and>  P  \<turnstile> s' : b

goal (1 subgoal):
 1.  P  \<turnstile> s : b
[PROOF STEP]
hence "s' = s"
[PROOF STATE]
proof (prove)
using this:
Some s' = i x \<and>  P  \<turnstile> s' : b

goal (1 subgoal):
 1. s' = s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Some s' = i x \<and>  P  \<turnstile> s' : b
Some (b, c) = lookup G x
 P ; G \<turnstile> i
Some s = i x
 P ; B  \<turnstile>\<^sub>w\<^sub>f G

goal (1 subgoal):
 1. s' = s
[PROOF STEP]
by (metis option.inject)
[PROOF STATE]
proof (state)
this:
s' = s

goal (1 subgoal):
 1.  P  \<turnstile> s : b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s' = s

goal (1 subgoal):
 1.  P  \<turnstile> s : b
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
s' = s
Some s' = i x \<and>  P  \<turnstile> s' : b

goal (1 subgoal):
 1.  P  \<turnstile> s : b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 P  \<turnstile> s : b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wfI_restrict_weakening:
  assumes "wfI \<Theta> \<Gamma>' i'" and "i =  restrict_map i' (fst `toSet \<Gamma>)" and "toSet \<Gamma> \<subseteq> toSet \<Gamma>'"
  shows  "\<Theta> ; \<Gamma> \<turnstile> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i
[PROOF STEP]
assume "x \<in> toSet \<Gamma>"
[PROOF STATE]
proof (state)
this:
x \<in> toSet \<Gamma>

goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i
[PROOF STEP]
have "case x of (x, b, c) \<Rightarrow> \<exists>s. Some s = i x \<and> \<Theta> \<turnstile> s : b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case x of (x, b, c) \<Rightarrow> \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
using assms wfI_def
[PROOF STATE]
proof (prove)
using this:
 \<Theta> ; \<Gamma>' \<turnstile> i'
i = i' |` (fst ` toSet \<Gamma>)
toSet \<Gamma> \<subseteq> toSet \<Gamma>'
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i = (\<forall>(x, b, c)\<in>toSet ?\<Gamma>. \<exists>s. Some s = ?i x \<and>  ?\<Theta>  \<turnstile> s : b)

goal (1 subgoal):
 1. case x of (x, b, c) \<Rightarrow> \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk> \<Theta> ; \<Gamma>' \<turnstile> i'; i = i' |` (fst ` toSet \<Gamma>); toSet \<Gamma> \<subseteq> toSet \<Gamma>'; \<And>\<Theta> \<Gamma> i.  \<Theta> ; \<Gamma> \<turnstile> i = (\<forall>(x, b, c)\<in>toSet \<Gamma>. \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b)\<rbrakk> \<Longrightarrow> case x of (x, b, c) \<Rightarrow> \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
have "case x of (x, b, c) \<Rightarrow> \<exists>s. Some s = i' x \<and> \<Theta> \<turnstile> s : b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case x of (x, b, c) \<Rightarrow> \<exists>s. Some s = i' x \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
using \<open>x \<in> toSet \<Gamma>\<close>  assms wfI_def
[PROOF STATE]
proof (prove)
using this:
x \<in> toSet \<Gamma>
 \<Theta> ; \<Gamma>' \<turnstile> i'
i = i' |` (fst ` toSet \<Gamma>)
toSet \<Gamma> \<subseteq> toSet \<Gamma>'
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i = (\<forall>(x, b, c)\<in>toSet ?\<Gamma>. \<exists>s. Some s = ?i x \<and>  ?\<Theta>  \<turnstile> s : b)

goal (1 subgoal):
 1. case x of (x, b, c) \<Rightarrow> \<exists>s. Some s = i' x \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
case x of (x, b, c) \<Rightarrow> \<exists>s. Some s = i' x \<and>  \<Theta>  \<turnstile> s : b

goal (1 subgoal):
 1. \<lbrakk> \<Theta> ; \<Gamma>' \<turnstile> i'; i = i' |` (fst ` toSet \<Gamma>); toSet \<Gamma> \<subseteq> toSet \<Gamma>'; \<And>\<Theta> \<Gamma> i.  \<Theta> ; \<Gamma> \<turnstile> i = (\<forall>(x, b, c)\<in>toSet \<Gamma>. \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b)\<rbrakk> \<Longrightarrow> case x of (x, b, c) \<Rightarrow> \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
case x of (x, b, c) \<Rightarrow> \<exists>s. Some s = i' x \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
have "\<exists>s. Some s = i (fst x) \<and> wfRCV \<Theta> s (fst (snd x))"
[PROOF STATE]
proof (prove)
using this:
case x of (x, b, c) \<Rightarrow> \<exists>s. Some s = i' x \<and>  \<Theta>  \<turnstile> s : b

goal (1 subgoal):
 1. \<exists>s. Some s = i (fst x) \<and>  \<Theta>  \<turnstile> s : fst (snd x)
[PROOF STEP]
by (simp add: \<open>x \<in> toSet \<Gamma>\<close> assms(2) case_prod_unfold)
[PROOF STATE]
proof (state)
this:
\<exists>s. Some s = i (fst x) \<and>  \<Theta>  \<turnstile> s : fst (snd x)

goal (1 subgoal):
 1. \<lbrakk> \<Theta> ; \<Gamma>' \<turnstile> i'; i = i' |` (fst ` toSet \<Gamma>); toSet \<Gamma> \<subseteq> toSet \<Gamma>'; \<And>\<Theta> \<Gamma> i.  \<Theta> ; \<Gamma> \<turnstile> i = (\<forall>(x, b, c)\<in>toSet \<Gamma>. \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b)\<rbrakk> \<Longrightarrow> case x of (x, b, c) \<Rightarrow> \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s. Some s = i (fst x) \<and>  \<Theta>  \<turnstile> s : fst (snd x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>s. Some s = i (fst x) \<and>  \<Theta>  \<turnstile> s : fst (snd x)

goal (1 subgoal):
 1. case x of (x, b, c) \<Rightarrow> \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b
[PROOF STEP]
by (simp add: case_prod_unfold)
[PROOF STATE]
proof (state)
this:
case x of (x, b, c) \<Rightarrow> \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
case x of (x, b, c) \<Rightarrow> \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b

goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> toSet \<Gamma> \<Longrightarrow> case ?x2 of (x, b, c) \<Rightarrow> \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b

goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> toSet \<Gamma> \<Longrightarrow> case ?x2 of (x, b, c) \<Rightarrow> \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b

goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i
[PROOF STEP]
using wfI_def assms
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> toSet \<Gamma> \<Longrightarrow> case ?x2 of (x, b, c) \<Rightarrow> \<exists>s. Some s = i x \<and>  \<Theta>  \<turnstile> s : b
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i = (\<forall>(x, b, c)\<in>toSet ?\<Gamma>. \<exists>s. Some s = ?i x \<and>  ?\<Theta>  \<turnstile> s : b)
 \<Theta> ; \<Gamma>' \<turnstile> i'
i = i' |` (fst ` toSet \<Gamma>)
toSet \<Gamma> \<subseteq> toSet \<Gamma>'

goal (1 subgoal):
 1.  \<Theta> ; \<Gamma> \<turnstile> i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 \<Theta> ; \<Gamma> \<turnstile> i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wfI_suffix:
  fixes G::\<Gamma>
  assumes "wfI P (G'@G) i" and "P ; B \<turnstile>\<^sub>w\<^sub>f G"
  shows "P ; G \<turnstile> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  P ; G \<turnstile> i
[PROOF STEP]
using wfI_def append_g.simps assms toSet.simps
[PROOF STATE]
proof (prove)
using this:
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i = (\<forall>(x, b, c)\<in>toSet ?\<Gamma>. \<exists>s. Some s = ?i x \<and>  ?\<Theta>  \<turnstile> s : b)
GNil @ ?g = ?g
(?xbc #\<^sub>\<Gamma> ?g1.0) @ ?g2.0 = ?xbc #\<^sub>\<Gamma> ?g1.0 @ ?g2.0
 P ; G' @ G \<turnstile> i
 P ; B  \<turnstile>\<^sub>w\<^sub>f G
toSet GNil = {}
toSet (?xbc #\<^sub>\<Gamma> ?G) = {?xbc} \<union> toSet ?G

goal (1 subgoal):
 1.  P ; G \<turnstile> i
[PROOF STEP]
by simp


[STATEMENT]
lemma wfI_replace_inside:
  assumes "wfI \<Theta> (\<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>) i"
  shows  "wfI \<Theta> (\<Gamma>' @ (x, b, c') #\<^sub>\<Gamma> \<Gamma>) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<Gamma>' @ (x, b, c') #\<^sub>\<Gamma> \<Gamma> \<turnstile> i
[PROOF STEP]
using wfI_def toSet_splitP assms
[PROOF STATE]
proof (prove)
using this:
 ?\<Theta> ; ?\<Gamma> \<turnstile> ?i = (\<forall>(x, b, c)\<in>toSet ?\<Gamma>. \<exists>s. Some s = ?i x \<and>  ?\<Theta>  \<turnstile> s : b)
(\<forall>(x', b', c')\<in>toSet (?\<Gamma>' @ (?x, ?b, ?c) #\<^sub>\<Gamma> ?\<Gamma>). ?P x' b' c') = ((\<forall>(x', b', c')\<in>toSet ?\<Gamma>'. ?P x' b' c') \<and> ?P ?x ?b ?c \<and> (\<forall>(x', b', c')\<in>toSet ?\<Gamma>. ?P x' b' c'))
 \<Theta> ; \<Gamma>' @ (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i

goal (1 subgoal):
 1.  \<Theta> ; \<Gamma>' @ (x, b, c') #\<^sub>\<Gamma> \<Gamma> \<turnstile> i
[PROOF STEP]
by simp


[STATEMENT]
lemma eval_l_base:
  "\<Theta> \<turnstile> \<lbrakk> l \<rbrakk>  : (base_for_lit l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta>  \<turnstile> \<lbrakk> l \<rbrakk>  : base_for_lit l
[PROOF STEP]
apply(nominal_induct l rule:l.strong_induct)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x.  \<Theta>  \<turnstile> \<lbrakk> L_num x \<rbrakk>  : base_for_lit (L_num x)
 2.  \<Theta>  \<turnstile> \<lbrakk> L_true \<rbrakk>  : base_for_lit L_true
 3.  \<Theta>  \<turnstile> \<lbrakk> L_false \<rbrakk>  : base_for_lit L_false
 4.  \<Theta>  \<turnstile> \<lbrakk> L_unit \<rbrakk>  : base_for_lit L_unit
 5. \<And>x.  \<Theta>  \<turnstile> \<lbrakk> L_bitvec x \<rbrakk>  : base_for_lit (L_bitvec x)
[PROOF STEP]
using wfRCV.intros eval_l.simps  base_for_lit.simps
[PROOF STATE]
proof (prove)
using this:
 ?P  \<turnstile> SBitvec ?bv : B_bitvec
 ?P  \<turnstile> SNum ?n : B_int
 ?P  \<turnstile> SBool ?b : B_bool
\<lbrakk> ?P  \<turnstile> ?s1.0 : ?b1.0;  ?P  \<turnstile> ?s2.0 : ?b2.0\<rbrakk> \<Longrightarrow>  ?P  \<turnstile> SPair ?s1.0 ?s2.0 : [ ?b1.0 , ?b2.0 ]\<^sup>b
\<lbrakk>AF_typedef ?s ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist;  ?\<Theta>  \<turnstile> ?s1.0 : ?b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SCons ?s ?dc ?s1.0 : B_id ?s
\<lbrakk>AF_typedef_poly ?s ?bv ?dclist \<in> set ?\<Theta>; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; atom ?bv \<sharp> (?\<Theta>, SConsp ?s ?dc ?b' ?s1.0, B_app ?s ?b');  ?\<Theta>  \<turnstile> ?s1.0 : ?b[?bv::=?b']\<^sub>b\<^sub>b\<rbrakk> \<Longrightarrow>  ?\<Theta>  \<turnstile> SConsp ?s ?dc ?b' ?s1.0 : B_app ?s ?b'
 ?P  \<turnstile> SUnit : B_unit
 ?P  \<turnstile> SUt ?n : B_var ?bv
\<lbrakk> L_true \<rbrakk>  = SBool True
\<lbrakk> L_false \<rbrakk>  = SBool False
\<lbrakk> L_num ?n \<rbrakk>  = SNum ?n
\<lbrakk> L_unit \<rbrakk>  = SUnit
\<lbrakk> L_bitvec ?n \<rbrakk>  = SBitvec ?n
base_for_lit L_true = B_bool
base_for_lit L_false = B_bool
base_for_lit (L_num ?n) = B_int
base_for_lit L_unit = B_unit
base_for_lit (L_bitvec ?v) = B_bitvec

goal (5 subgoals):
 1. \<And>x.  \<Theta>  \<turnstile> \<lbrakk> L_num x \<rbrakk>  : base_for_lit (L_num x)
 2.  \<Theta>  \<turnstile> \<lbrakk> L_true \<rbrakk>  : base_for_lit L_true
 3.  \<Theta>  \<turnstile> \<lbrakk> L_false \<rbrakk>  : base_for_lit L_false
 4.  \<Theta>  \<turnstile> \<lbrakk> L_unit \<rbrakk>  : base_for_lit L_unit
 5. \<And>x.  \<Theta>  \<turnstile> \<lbrakk> L_bitvec x \<rbrakk>  : base_for_lit (L_bitvec x)
[PROOF STEP]
by auto+


[STATEMENT]
lemma obtain_fresh_bv_dclist:
  fixes tm::"'a::fs"
  assumes "(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist"
  obtains bv1::bv and dclist1 x1 b1 c1 where "AF_typedef_poly tyid bv dclist =  AF_typedef_poly tyid bv1 dclist1
      \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> tm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>bv1 dclist1 x1 b1 c1. AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> tm \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>bv1 dclist1 x1 b1 c1. AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> tm \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain bv1 dclist1 where "AF_typedef_poly tyid bv dclist =  AF_typedef_poly tyid bv1 dclist1 \<and> atom bv1 \<sharp> tm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>bv1 dclist1. AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> atom bv1 \<sharp> tm \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obtain_fresh_bv
[PROOF STATE]
proof (prove)
using this:
(\<And>bva2 dclist2. AF_typedef_poly ?tyid ?bva ?dclist = AF_typedef_poly ?tyid bva2 dclist2 \<and> atom bva2 \<sharp> ?tm \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>bv1 dclist1. AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> atom bv1 \<sharp> tm \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> atom bv1 \<sharp> tm

goal (1 subgoal):
 1. (\<And>bv1 dclist1 x1 b1 c1. AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> tm \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> atom bv1 \<sharp> tm

goal (1 subgoal):
 1. (\<And>bv1 dclist1 x1 b1 c1. AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> tm \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "[[atom bv]]lst. dclist = [[atom bv1]]lst. dclist1"
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> atom bv1 \<sharp> tm

goal (1 subgoal):
 1. [[atom bv]]lst. dclist = [[atom bv1]]lst. dclist1
[PROOF STEP]
using type_def.eq_iff
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> atom bv1 \<sharp> tm
(AF_typedef ?list1.0 ?list2.0 = AF_typedef ?list1a ?list2a) = (?list1.0 = ?list1a \<and> ?list2.0 = ?list2a)
(AF_typedef_poly ?list1.0 ?bv ?list2.0 = AF_typedef_poly ?list1a ?bva ?list2a) = ([[atom ?bv]]lst. ?list2.0 = [[atom ?bva]]lst. ?list2a \<and> ?list1.0 = ?list1a)

goal (1 subgoal):
 1. [[atom bv]]lst. dclist = [[atom bv1]]lst. dclist1
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
[[atom bv]]lst. dclist = [[atom bv1]]lst. dclist1

goal (1 subgoal):
 1. (\<And>bv1 dclist1 x1 b1 c1. AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> tm \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[[atom bv]]lst. dclist = [[atom bv1]]lst. dclist1

goal (1 subgoal):
 1. (\<And>bv1 dclist1 x1 b1 c1. AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> tm \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[[atom bv]]lst. dclist = [[atom bv1]]lst. dclist1
[PROOF STEP]
obtain x1 b1 c1 where "(dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1"
[PROOF STATE]
proof (prove)
using this:
[[atom bv]]lst. dclist = [[atom bv1]]lst. dclist1

goal (1 subgoal):
 1. (\<And>x1 b1 c1. (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using td_lookup_eq_iff assms
[PROOF STATE]
proof (prove)
using this:
[[atom bv]]lst. dclist = [[atom bv1]]lst. dclist1
\<lbrakk>[[atom ?bva1.0]]lst. ?dclist1.0 = [[atom ?bva2.0]]lst. ?dclist2.0; (?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist1.0\<rbrakk> \<Longrightarrow> \<exists>x2 b2 c2. (?dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set ?dclist2.0
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist

goal (1 subgoal):
 1. (\<And>x1 b1 c1. (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1

goal (1 subgoal):
 1. (\<And>bv1 dclist1 x1 b1 c1. AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> tm \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> atom bv1 \<sharp> tm
[[atom bv]]lst. dclist = [[atom bv1]]lst. dclist1
(dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> atom bv1 \<sharp> tm
[[atom bv]]lst. dclist = [[atom bv1]]lst. dclist1
(dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> atom bv1 \<sharp> tm
[[atom bv]]lst. dclist = [[atom bv1]]lst. dclist1
(dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid ?bv1.0 ?dclist1.0 \<and> (dc, \<lbrace> ?x1.0 : ?b1.0  | ?c1.0 \<rbrace>) \<in> set ?dclist1.0 \<and> atom ?bv1.0 \<sharp> tm \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma obtain_fresh_bv_dclist_b_iff:
  fixes tm::"'a::fs"
  assumes "(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist" and "AF_typedef_poly tyid bv dclist \<in> set P" and "\<turnstile>\<^sub>w\<^sub>f P"
  obtains bv1::bv and dclist1 x1 b1 c1 where "AF_typedef_poly tyid bv dclist =  AF_typedef_poly tyid bv1 dclist1
      \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> tm \<and> b[bv::=b']\<^sub>b\<^sub>b=b1[bv1::=b']\<^sub>b\<^sub>b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>bv1 dclist1 x1 b1 c1. AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> tm \<and> b[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>bv1 dclist1 x1 b1 c1. AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> tm \<and> b[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain bv1 dclist1 x1 b1 c1 where *:"AF_typedef_poly tyid bv dclist =  AF_typedef_poly tyid bv1 dclist1 \<and> atom bv1 \<sharp> tm
    \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>bv1 dclist1 x1 b1 c1. AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> atom bv1 \<sharp> tm \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obtain_fresh_bv_dclist assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?dc, \<lbrace> ?x : ?b  | ?c \<rbrace>) \<in> set ?dclist; \<And>bv1 dclist1 x1 b1 c1. AF_typedef_poly ?tyid ?bv ?dclist = AF_typedef_poly ?tyid bv1 dclist1 \<and> (?dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> ?tm \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
AF_typedef_poly tyid bv dclist \<in> set P
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1. (\<And>bv1 dclist1 x1 b1 c1. AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> atom bv1 \<sharp> tm \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> atom bv1 \<sharp> tm \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1

goal (1 subgoal):
 1. (\<And>bv1 dclist1 x1 b1 c1. AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> tm \<and> b[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "AF_typedef_poly tyid bv1 dclist1 \<in> set P"
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> atom bv1 \<sharp> tm \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1

goal (1 subgoal):
 1. AF_typedef_poly tyid bv1 dclist1 \<in> set P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> atom bv1 \<sharp> tm \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1
(dc, \<lbrace> x : b  | c \<rbrace>) \<in> set dclist
AF_typedef_poly tyid bv dclist \<in> set P
   \<turnstile>\<^sub>w\<^sub>f P

goal (1 subgoal):
 1. AF_typedef_poly tyid bv1 dclist1 \<in> set P
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
AF_typedef_poly tyid bv1 dclist1 \<in> set P

goal (1 subgoal):
 1. (\<And>bv1 dclist1 x1 b1 c1. AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> tm \<and> b[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "b[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b"
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bv1 dclist1 \<in> set P

goal (1 subgoal):
 1. b[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b
[PROOF STEP]
using  wfTh_typedef_poly_b_eq_iff[OF assms(2) assms(1) _ _ assms(3),of bv1 dclist1 x1 b1 c1 b']  *
[PROOF STATE]
proof (prove)
using this:
AF_typedef_poly tyid bv1 dclist1 \<in> set P
\<lbrakk>AF_typedef_poly tyid bv1 dclist1 \<in> set P; (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1\<rbrakk> \<Longrightarrow> b[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> atom bv1 \<sharp> tm \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1

goal (1 subgoal):
 1. b[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
b[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b

goal (1 subgoal):
 1. (\<And>bv1 dclist1 x1 b1 c1. AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1 \<and> atom bv1 \<sharp> tm \<and> b[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from this that
[PROOF STATE]
proof (chain)
picking this:
b[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid ?bv1.0 ?dclist1.0 \<and> (dc, \<lbrace> ?x1.0 : ?b1.0  | ?c1.0 \<rbrace>) \<in> set ?dclist1.0 \<and> atom ?bv1.0 \<sharp> tm \<and> b[bv::=b']\<^sub>b\<^sub>b = ?b1.0[?bv1.0::=b']\<^sub>b\<^sub>b \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid ?bv1.0 ?dclist1.0 \<and> (dc, \<lbrace> ?x1.0 : ?b1.0  | ?c1.0 \<rbrace>) \<in> set ?dclist1.0 \<and> atom ?bv1.0 \<sharp> tm \<and> b[bv::=b']\<^sub>b\<^sub>b = ?b1.0[?bv1.0::=b']\<^sub>b\<^sub>b \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
b[bv::=b']\<^sub>b\<^sub>b = b1[bv1::=b']\<^sub>b\<^sub>b
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid ?bv1.0 ?dclist1.0 \<and> (dc, \<lbrace> ?x1.0 : ?b1.0  | ?c1.0 \<rbrace>) \<in> set ?dclist1.0 \<and> atom ?bv1.0 \<sharp> tm \<and> b[bv::=b']\<^sub>b\<^sub>b = ?b1.0[?bv1.0::=b']\<^sub>b\<^sub>b \<Longrightarrow> thesis
AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 \<and> atom bv1 \<sharp> tm \<and> (dc, \<lbrace> x1 : b1  | c1 \<rbrace>) \<in> set dclist1

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

goal:
No subgoals!
[PROOF STEP]
qed