[STATEMENT]
lemma cil_assoc1: "!!wl w1 w2 w3. \<lbrakk> w\<in>wl\<otimes>\<^bsub>\<alpha>\<^esub>w3; wl\<in>w1\<otimes>\<^bsub>\<alpha>\<^esub>w2 \<rbrakk>
  \<Longrightarrow> \<exists>wr. w\<in>w1\<otimes>\<^bsub>\<alpha>\<^esub>wr \<and> wr\<in>w2\<otimes>\<^bsub>\<alpha>\<^esub>w3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>wl w1 w2 w3. \<lbrakk>w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3; wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2\<rbrakk> \<Longrightarrow> \<exists>wr. w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
proof (induct w rule: length_compl_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>wl w1 w2 w3. \<lbrakk>[] \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3; wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2\<rbrakk> \<Longrightarrow> \<exists>wr. [] \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
 2. \<And>e l wl w1 w2 w3. \<lbrakk>\<And>ll wl w1 w2 w3. \<lbrakk>length ll \<le> length l; ll \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3; wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2\<rbrakk> \<Longrightarrow> \<exists>wr. ll \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3; e # l \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3; wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2\<rbrakk> \<Longrightarrow> \<exists>wr. e # l \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
[] \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3
wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2

goal (2 subgoals):
 1. \<And>wl w1 w2 w3. \<lbrakk>[] \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3; wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2\<rbrakk> \<Longrightarrow> \<exists>wr. [] \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
 2. \<And>e l wl w1 w2 w3. \<lbrakk>\<And>ll wl w1 w2 w3. \<lbrakk>length ll \<le> length l; ll \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3; wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2\<rbrakk> \<Longrightarrow> \<exists>wr. ll \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3; e # l \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3; wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2\<rbrakk> \<Longrightarrow> \<exists>wr. e # l \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
[] \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3
wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2

goal (1 subgoal):
 1. \<exists>wr. [] \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>wr. [] \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3

goal (1 subgoal):
 1. \<And>e l wl w1 w2 w3. \<lbrakk>\<And>ll wl w1 w2 w3. \<lbrakk>length ll \<le> length l; ll \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3; wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2\<rbrakk> \<Longrightarrow> \<exists>wr. ll \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3; e # l \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3; wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2\<rbrakk> \<Longrightarrow> \<exists>wr. e # l \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e l wl w1 w2 w3. \<lbrakk>\<And>ll wl w1 w2 w3. \<lbrakk>length ll \<le> length l; ll \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3; wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2\<rbrakk> \<Longrightarrow> \<exists>wr. ll \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3; e # l \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3; wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2\<rbrakk> \<Longrightarrow> \<exists>wr. e # l \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
case (Cons e w)
[PROOF STATE]
proof (state)
this:
\<lbrakk>length ?ll \<le> length w; ?ll \<in> ?wl \<otimes>\<^bsub>\<alpha>\<^esub> ?w3.0; ?wl \<in> ?w1.0 \<otimes>\<^bsub>\<alpha>\<^esub> ?w2.0\<rbrakk> \<Longrightarrow> \<exists>wr. ?ll \<in> ?w1.0 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> ?w2.0 \<otimes>\<^bsub>\<alpha>\<^esub> ?w3.0
e # w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3
wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2

goal (1 subgoal):
 1. \<And>e l wl w1 w2 w3. \<lbrakk>\<And>ll wl w1 w2 w3. \<lbrakk>length ll \<le> length l; ll \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3; wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2\<rbrakk> \<Longrightarrow> \<exists>wr. ll \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3; e # l \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3; wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2\<rbrakk> \<Longrightarrow> \<exists>wr. e # l \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
from Cons.prems(1)
[PROOF STATE]
proof (chain)
picking this:
e # w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
e # w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3

goal (1 subgoal):
 1. \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
proof (cases rule: cil_cons_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>w1'. \<lbrakk>wl = e # w1'; w \<in> w1' \<otimes>\<^bsub>\<alpha>\<^esub> w3; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w3) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
 2. \<And>w2'. \<lbrakk>w3 = e # w2'; w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wl) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
case (left wl')
[PROOF STATE]
proof (state)
this:
wl = e # wl'
w \<in> wl' \<otimes>\<^bsub>\<alpha>\<^esub> w3
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w3) = {}

goal (2 subgoals):
 1. \<And>w1'. \<lbrakk>wl = e # w1'; w \<in> w1' \<otimes>\<^bsub>\<alpha>\<^esub> w3; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w3) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
 2. \<And>w2'. \<lbrakk>w3 = e # w2'; w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wl) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
with Cons.prems(2)
[PROOF STATE]
proof (chain)
picking this:
wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2
wl = e # wl'
w \<in> wl' \<otimes>\<^bsub>\<alpha>\<^esub> w3
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w3) = {}
[PROOF STEP]
have "e#wl' \<in> w1\<otimes>\<^bsub>\<alpha>\<^esub>w2"
[PROOF STATE]
proof (prove)
using this:
wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2
wl = e # wl'
w \<in> wl' \<otimes>\<^bsub>\<alpha>\<^esub> w3
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w3) = {}

goal (1 subgoal):
 1. e # wl' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
e # wl' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2

goal (2 subgoals):
 1. \<And>w1'. \<lbrakk>wl = e # w1'; w \<in> w1' \<otimes>\<^bsub>\<alpha>\<^esub> w3; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w3) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
 2. \<And>w2'. \<lbrakk>w3 = e # w2'; w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wl) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
e # wl' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2

goal (1 subgoal):
 1. \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
proof (cases rule: cil_cons_cases[case_names left' right'])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>w1'. \<lbrakk>w1 = e # w1'; wl' \<in> w1' \<otimes>\<^bsub>\<alpha>\<^esub> w2; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w2) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
 2. \<And>w2'. \<lbrakk>w2 = e # w2'; wl' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
case (left' w1')
[PROOF STATE]
proof (state)
this:
w1 = e # w1'
wl' \<in> w1' \<otimes>\<^bsub>\<alpha>\<^esub> w2
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w2) = {}

goal (2 subgoals):
 1. \<And>w1'. \<lbrakk>w1 = e # w1'; wl' \<in> w1' \<otimes>\<^bsub>\<alpha>\<^esub> w2; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w2) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
 2. \<And>w2'. \<lbrakk>w2 = e # w2'; wl' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
from Cons.hyps[OF _ left(2) left'(2)]
[PROOF STATE]
proof (chain)
picking this:
length w \<le> length w \<Longrightarrow> \<exists>wr. w \<in> w1' \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
obtain wr where IHAPP: "w \<in> w1' \<otimes>\<^bsub>\<alpha>\<^esub> wr" "wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3"
[PROOF STATE]
proof (prove)
using this:
length w \<le> length w \<Longrightarrow> \<exists>wr. w \<in> w1' \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3

goal (1 subgoal):
 1. (\<And>wr. \<lbrakk>w \<in> w1' \<otimes>\<^bsub>\<alpha>\<^esub> wr; wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
w \<in> w1' \<otimes>\<^bsub>\<alpha>\<^esub> wr
wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3

goal (2 subgoals):
 1. \<And>w1'. \<lbrakk>w1 = e # w1'; wl' \<in> w1' \<otimes>\<^bsub>\<alpha>\<^esub> w2; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w2) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
 2. \<And>w2'. \<lbrakk>w2 = e # w2'; wl' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
have "e#w\<in>e#w1'\<otimes>\<^bsub>\<alpha>\<^esub>wr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e # w \<in> e # w1' \<otimes>\<^bsub>\<alpha>\<^esub> wr
[PROOF STEP]
proof (rule cil_cons1[OF IHAPP(1)])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wr) = {}
[PROOF STEP]
from left left' cil_mon_pl[OF IHAPP(2)]
[PROOF STATE]
proof (chain)
picking this:
wl = e # wl'
w \<in> wl' \<otimes>\<^bsub>\<alpha>\<^esub> w3
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w3) = {}
w1 = e # w1'
wl' \<in> w1' \<otimes>\<^bsub>\<alpha>\<^esub> w2
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w2) = {}
mon_pl (map \<alpha> wr) = mon_pl (map \<alpha> w2) \<union> mon_pl (map \<alpha> w3)
[PROOF STEP]
show "fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wr) = {}"
[PROOF STATE]
proof (prove)
using this:
wl = e # wl'
w \<in> wl' \<otimes>\<^bsub>\<alpha>\<^esub> w3
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w3) = {}
w1 = e # w1'
wl' \<in> w1' \<otimes>\<^bsub>\<alpha>\<^esub> w2
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w2) = {}
mon_pl (map \<alpha> wr) = mon_pl (map \<alpha> w2) \<union> mon_pl (map \<alpha> w3)

goal (1 subgoal):
 1. fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wr) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wr) = {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
e # w \<in> e # w1' \<otimes>\<^bsub>\<alpha>\<^esub> wr

goal (2 subgoals):
 1. \<And>w1'. \<lbrakk>w1 = e # w1'; wl' \<in> w1' \<otimes>\<^bsub>\<alpha>\<^esub> w2; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w2) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
 2. \<And>w2'. \<lbrakk>w2 = e # w2'; wl' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
e # w \<in> e # w1' \<otimes>\<^bsub>\<alpha>\<^esub> wr

goal (1 subgoal):
 1. \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
using IHAPP(2) left'
[PROOF STATE]
proof (prove)
using this:
e # w \<in> e # w1' \<otimes>\<^bsub>\<alpha>\<^esub> wr
wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
w1 = e # w1'
wl' \<in> w1' \<otimes>\<^bsub>\<alpha>\<^esub> w2
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w2) = {}

goal (1 subgoal):
 1. \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3

goal (1 subgoal):
 1. \<And>w2'. \<lbrakk>w2 = e # w2'; wl' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w2'. \<lbrakk>w2 = e # w2'; wl' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
case (right' w2')
[PROOF STATE]
proof (state)
this:
w2 = e # w2'
wl' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2'
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {}

goal (1 subgoal):
 1. \<And>w2'. \<lbrakk>w2 = e # w2'; wl' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
from Cons.hyps[OF _ left(2) right'(2)]
[PROOF STATE]
proof (chain)
picking this:
length w \<le> length w \<Longrightarrow> \<exists>wr. w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2' \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
obtain wr where IHAPP: "w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr" "wr \<in> w2' \<otimes>\<^bsub>\<alpha>\<^esub> w3"
[PROOF STATE]
proof (prove)
using this:
length w \<le> length w \<Longrightarrow> \<exists>wr. w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2' \<otimes>\<^bsub>\<alpha>\<^esub> w3

goal (1 subgoal):
 1. (\<And>wr. \<lbrakk>w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr; wr \<in> w2' \<otimes>\<^bsub>\<alpha>\<^esub> w3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr
wr \<in> w2' \<otimes>\<^bsub>\<alpha>\<^esub> w3

goal (1 subgoal):
 1. \<And>w2'. \<lbrakk>w2 = e # w2'; wl' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
from IHAPP(2) left
[PROOF STATE]
proof (chain)
picking this:
wr \<in> w2' \<otimes>\<^bsub>\<alpha>\<^esub> w3
wl = e # wl'
w \<in> wl' \<otimes>\<^bsub>\<alpha>\<^esub> w3
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w3) = {}
[PROOF STEP]
have "e#wr \<in> e#w2' \<otimes>\<^bsub>\<alpha>\<^esub> w3"
[PROOF STATE]
proof (prove)
using this:
wr \<in> w2' \<otimes>\<^bsub>\<alpha>\<^esub> w3
wl = e # wl'
w \<in> wl' \<otimes>\<^bsub>\<alpha>\<^esub> w3
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w3) = {}

goal (1 subgoal):
 1. e # wr \<in> e # w2' \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
by (auto intro: cil_cons1)
[PROOF STATE]
proof (state)
this:
e # wr \<in> e # w2' \<otimes>\<^bsub>\<alpha>\<^esub> w3

goal (1 subgoal):
 1. \<And>w2'. \<lbrakk>w2 = e # w2'; wl' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
e # wr \<in> e # w2' \<otimes>\<^bsub>\<alpha>\<^esub> w3

goal (1 subgoal):
 1. \<And>w2'. \<lbrakk>w2 = e # w2'; wl' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
from right' IHAPP(1)
[PROOF STATE]
proof (chain)
picking this:
w2 = e # w2'
wl' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2'
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {}
w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr
[PROOF STEP]
have "e#w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e#wr"
[PROOF STATE]
proof (prove)
using this:
w2 = e # w2'
wl' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2'
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {}
w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr

goal (1 subgoal):
 1. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e # wr
[PROOF STEP]
by (auto intro: cil_cons2)
[PROOF STATE]
proof (state)
this:
e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e # wr

goal (1 subgoal):
 1. \<And>w2'. \<lbrakk>w2 = e # w2'; wl' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
e # wr \<in> e # w2' \<otimes>\<^bsub>\<alpha>\<^esub> w3
e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e # wr
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
e # wr \<in> e # w2' \<otimes>\<^bsub>\<alpha>\<^esub> w3
e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e # wr

goal (1 subgoal):
 1. \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
using right'
[PROOF STATE]
proof (prove)
using this:
e # wr \<in> e # w2' \<otimes>\<^bsub>\<alpha>\<^esub> w3
e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e # wr
w2 = e # w2'
wl' \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2'
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> w1) = {}

goal (1 subgoal):
 1. \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3

goal (1 subgoal):
 1. \<And>w2'. \<lbrakk>w3 = e # w2'; w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wl) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w2'. \<lbrakk>w3 = e # w2'; w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wl) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
case (right w3')
[PROOF STATE]
proof (state)
this:
w3 = e # w3'
w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3'
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wl) = {}

goal (1 subgoal):
 1. \<And>w2'. \<lbrakk>w3 = e # w2'; w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wl) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
from Cons.hyps[OF _ right(2) Cons.prems(2)]
[PROOF STATE]
proof (chain)
picking this:
length w \<le> length w \<Longrightarrow> \<exists>wr. w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3'
[PROOF STEP]
obtain wr where IHAPP: "w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr" "wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3'"
[PROOF STATE]
proof (prove)
using this:
length w \<le> length w \<Longrightarrow> \<exists>wr. w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3'

goal (1 subgoal):
 1. (\<And>wr. \<lbrakk>w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr; wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr
wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3'

goal (1 subgoal):
 1. \<And>w2'. \<lbrakk>w3 = e # w2'; w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wl) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
from IHAPP(2) right cil_mon_pl[OF Cons.prems(2)]
[PROOF STATE]
proof (chain)
picking this:
wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3'
w3 = e # w3'
w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3'
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wl) = {}
mon_pl (map \<alpha> wl) = mon_pl (map \<alpha> w1) \<union> mon_pl (map \<alpha> w2)
[PROOF STEP]
have "e#wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> e#w3'"
[PROOF STATE]
proof (prove)
using this:
wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3'
w3 = e # w3'
w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3'
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wl) = {}
mon_pl (map \<alpha> wl) = mon_pl (map \<alpha> w1) \<union> mon_pl (map \<alpha> w2)

goal (1 subgoal):
 1. e # wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> e # w3'
[PROOF STEP]
by (auto intro: cil_cons2)
[PROOF STATE]
proof (state)
this:
e # wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> e # w3'

goal (1 subgoal):
 1. \<And>w2'. \<lbrakk>w3 = e # w2'; w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wl) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
e # wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> e # w3'

goal (1 subgoal):
 1. \<And>w2'. \<lbrakk>w3 = e # w2'; w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wl) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
from IHAPP(1) right cil_mon_pl[OF Cons.prems(2)]
[PROOF STATE]
proof (chain)
picking this:
w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr
w3 = e # w3'
w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3'
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wl) = {}
mon_pl (map \<alpha> wl) = mon_pl (map \<alpha> w1) \<union> mon_pl (map \<alpha> w2)
[PROOF STEP]
have "e#w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e#wr"
[PROOF STATE]
proof (prove)
using this:
w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr
w3 = e # w3'
w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3'
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wl) = {}
mon_pl (map \<alpha> wl) = mon_pl (map \<alpha> w1) \<union> mon_pl (map \<alpha> w2)

goal (1 subgoal):
 1. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e # wr
[PROOF STEP]
by (auto intro: cil_cons2)
[PROOF STATE]
proof (state)
this:
e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e # wr

goal (1 subgoal):
 1. \<And>w2'. \<lbrakk>w3 = e # w2'; w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w2'; fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wl) = {}\<rbrakk> \<Longrightarrow> \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
e # wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> e # w3'
e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e # wr
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
e # wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> e # w3'
e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e # wr

goal (1 subgoal):
 1. \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
using right
[PROOF STATE]
proof (prove)
using this:
e # wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> e # w3'
e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> e # wr
w3 = e # w3'
w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3'
fst (\<alpha> e) \<inter> mon_pl (map \<alpha> wl) = {}

goal (1 subgoal):
 1. \<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>wr. e # w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cil_assoc2:
  assumes A: "w\<in>w1\<otimes>\<^bsub>\<alpha>\<^esub>wr" and B: "wr\<in>w2\<otimes>\<^bsub>\<alpha>\<^esub>w3"
  shows "\<exists>wl. w\<in>wl\<otimes>\<^bsub>\<alpha>\<^esub>w3 \<and> wl\<in>w1\<otimes>\<^bsub>\<alpha>\<^esub>w2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>wl. w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3 \<and> wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>wl. w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3 \<and> wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr
[PROOF STEP]
have A': "w\<in>wr\<otimes>\<^bsub>\<alpha>\<^esub>w1"
[PROOF STATE]
proof (prove)
using this:
w \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> wr

goal (1 subgoal):
 1. w \<in> wr \<otimes>\<^bsub>\<alpha>\<^esub> w1
[PROOF STEP]
by (simp add: cil_commute)
[PROOF STATE]
proof (state)
this:
w \<in> wr \<otimes>\<^bsub>\<alpha>\<^esub> w1

goal (1 subgoal):
 1. \<exists>wl. w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3 \<and> wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2
[PROOF STEP]
from B
[PROOF STATE]
proof (chain)
picking this:
wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3
[PROOF STEP]
have B': "wr\<in>w3\<otimes>\<^bsub>\<alpha>\<^esub>w2"
[PROOF STATE]
proof (prove)
using this:
wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w3

goal (1 subgoal):
 1. wr \<in> w3 \<otimes>\<^bsub>\<alpha>\<^esub> w2
[PROOF STEP]
by (simp add: cil_commute)
[PROOF STATE]
proof (state)
this:
wr \<in> w3 \<otimes>\<^bsub>\<alpha>\<^esub> w2

goal (1 subgoal):
 1. \<exists>wl. w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3 \<and> wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2
[PROOF STEP]
from cil_assoc1[OF A' B']
[PROOF STATE]
proof (chain)
picking this:
\<exists>wr. w \<in> w3 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w1
[PROOF STEP]
obtain wl where "w \<in> w3 \<otimes>\<^bsub>\<alpha>\<^esub> wl \<and> wl \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w1"
[PROOF STATE]
proof (prove)
using this:
\<exists>wr. w \<in> w3 \<otimes>\<^bsub>\<alpha>\<^esub> wr \<and> wr \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w1

goal (1 subgoal):
 1. (\<And>wl. w \<in> w3 \<otimes>\<^bsub>\<alpha>\<^esub> wl \<and> wl \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
w \<in> w3 \<otimes>\<^bsub>\<alpha>\<^esub> wl \<and> wl \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w1

goal (1 subgoal):
 1. \<exists>wl. w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3 \<and> wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
w \<in> w3 \<otimes>\<^bsub>\<alpha>\<^esub> wl \<and> wl \<in> w2 \<otimes>\<^bsub>\<alpha>\<^esub> w1

goal (1 subgoal):
 1. \<exists>wl. w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3 \<and> wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2
[PROOF STEP]
by (auto simp add: cil_commute)
[PROOF STATE]
proof (state)
this:
\<exists>wl. w \<in> wl \<otimes>\<^bsub>\<alpha>\<^esub> w3 \<and> wl \<in> w1 \<otimes>\<^bsub>\<alpha>\<^esub> w2

goal:
No subgoals!
[PROOF STEP]
qed

\<comment> \<open>Parts of the abstraction can be moved to the operands\<close>


[STATEMENT]
lemma cil_map: "w\<in>w1 \<otimes>\<^bsub>(\<alpha>\<circ>f)\<^esub> w2 \<Longrightarrow> map f w \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f w2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> w1 \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2 \<Longrightarrow> map f w \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f w2
[PROOF STEP]
proof (induct rule: cil_set_induct_fix\<alpha>)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. map f [] \<in> map f [] \<otimes>\<^bsub>\<alpha>\<^esub> map f []
 2. \<And>e w' w1' w2. \<lbrakk>w' \<in> w1' \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2; fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w2) = {}; map f w' \<in> map f w1' \<otimes>\<^bsub>\<alpha>\<^esub> map f w2\<rbrakk> \<Longrightarrow> map f (e # w') \<in> map f (e # w1') \<otimes>\<^bsub>\<alpha>\<^esub> map f w2
 3. \<And>e w' w2' w1. \<lbrakk>w' \<in> w1 \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2'; fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w1) = {}; map f w' \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f w2'\<rbrakk> \<Longrightarrow> map f (e # w') \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f (e # w2')
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. map f [] \<in> map f [] \<otimes>\<^bsub>\<alpha>\<^esub> map f []
 2. \<And>e w' w1' w2. \<lbrakk>w' \<in> w1' \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2; fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w2) = {}; map f w' \<in> map f w1' \<otimes>\<^bsub>\<alpha>\<^esub> map f w2\<rbrakk> \<Longrightarrow> map f (e # w') \<in> map f (e # w1') \<otimes>\<^bsub>\<alpha>\<^esub> map f w2
 3. \<And>e w' w2' w1. \<lbrakk>w' \<in> w1 \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2'; fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w1) = {}; map f w' \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f w2'\<rbrakk> \<Longrightarrow> map f (e # w') \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f (e # w2')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map f [] \<in> map f [] \<otimes>\<^bsub>\<alpha>\<^esub> map f []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map f [] \<in> map f [] \<otimes>\<^bsub>\<alpha>\<^esub> map f []

goal (2 subgoals):
 1. \<And>e w' w1' w2. \<lbrakk>w' \<in> w1' \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2; fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w2) = {}; map f w' \<in> map f w1' \<otimes>\<^bsub>\<alpha>\<^esub> map f w2\<rbrakk> \<Longrightarrow> map f (e # w') \<in> map f (e # w1') \<otimes>\<^bsub>\<alpha>\<^esub> map f w2
 2. \<And>e w' w2' w1. \<lbrakk>w' \<in> w1 \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2'; fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w1) = {}; map f w' \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f w2'\<rbrakk> \<Longrightarrow> map f (e # w') \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f (e # w2')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>e w' w1' w2. \<lbrakk>w' \<in> w1' \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2; fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w2) = {}; map f w' \<in> map f w1' \<otimes>\<^bsub>\<alpha>\<^esub> map f w2\<rbrakk> \<Longrightarrow> map f (e # w') \<in> map f (e # w1') \<otimes>\<^bsub>\<alpha>\<^esub> map f w2
 2. \<And>e w' w2' w1. \<lbrakk>w' \<in> w1 \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2'; fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w1) = {}; map f w' \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f w2'\<rbrakk> \<Longrightarrow> map f (e # w') \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f (e # w2')
[PROOF STEP]
case (left e w' w1' w2)
[PROOF STATE]
proof (state)
this:
w' \<in> w1' \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2
fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w2) = {}
map f w' \<in> map f w1' \<otimes>\<^bsub>\<alpha>\<^esub> map f w2

goal (2 subgoals):
 1. \<And>e w' w1' w2. \<lbrakk>w' \<in> w1' \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2; fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w2) = {}; map f w' \<in> map f w1' \<otimes>\<^bsub>\<alpha>\<^esub> map f w2\<rbrakk> \<Longrightarrow> map f (e # w') \<in> map f (e # w1') \<otimes>\<^bsub>\<alpha>\<^esub> map f w2
 2. \<And>e w' w2' w1. \<lbrakk>w' \<in> w1 \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2'; fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w1) = {}; map f w' \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f w2'\<rbrakk> \<Longrightarrow> map f (e # w') \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f (e # w2')
[PROOF STEP]
have "f e # map f w' \<in> f e # map f w1' \<otimes>\<^bsub>\<alpha>\<^esub> map f w2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f e # map f w' \<in> f e # map f w1' \<otimes>\<^bsub>\<alpha>\<^esub> map f w2
[PROOF STEP]
proof (rule cil_cons1)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. map f w' \<in> map f w1' \<otimes>\<^bsub>\<alpha>\<^esub> map f w2
 2. fst (\<alpha> (f e)) \<inter> mon_pl (map \<alpha> (map f w2)) = {}
[PROOF STEP]
from left(2)
[PROOF STATE]
proof (chain)
picking this:
fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w2) = {}
[PROOF STEP]
have "fst ((\<alpha>\<circ>f) e) \<inter> mon_pl (map \<alpha> (map f w2)) = {}"
[PROOF STATE]
proof (prove)
using this:
fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w2) = {}

goal (1 subgoal):
 1. fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map \<alpha> (map f w2)) = {}
[PROOF STEP]
by (simp only: map_map[symmetric])
[PROOF STATE]
proof (state)
this:
fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map \<alpha> (map f w2)) = {}

goal (2 subgoals):
 1. map f w' \<in> map f w1' \<otimes>\<^bsub>\<alpha>\<^esub> map f w2
 2. fst (\<alpha> (f e)) \<inter> mon_pl (map \<alpha> (map f w2)) = {}
[PROOF STEP]
thus "fst (\<alpha> (f e)) \<inter> mon_pl (map \<alpha> (map f w2)) = {}"
[PROOF STATE]
proof (prove)
using this:
fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map \<alpha> (map f w2)) = {}

goal (1 subgoal):
 1. fst (\<alpha> (f e)) \<inter> mon_pl (map \<alpha> (map f w2)) = {}
[PROOF STEP]
by (simp only: o_apply)
[PROOF STATE]
proof (state)
this:
fst (\<alpha> (f e)) \<inter> mon_pl (map \<alpha> (map f w2)) = {}

goal (1 subgoal):
 1. map f w' \<in> map f w1' \<otimes>\<^bsub>\<alpha>\<^esub> map f w2
[PROOF STEP]
qed (rule left(3))
[PROOF STATE]
proof (state)
this:
f e # map f w' \<in> f e # map f w1' \<otimes>\<^bsub>\<alpha>\<^esub> map f w2

goal (2 subgoals):
 1. \<And>e w' w1' w2. \<lbrakk>w' \<in> w1' \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2; fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w2) = {}; map f w' \<in> map f w1' \<otimes>\<^bsub>\<alpha>\<^esub> map f w2\<rbrakk> \<Longrightarrow> map f (e # w') \<in> map f (e # w1') \<otimes>\<^bsub>\<alpha>\<^esub> map f w2
 2. \<And>e w' w2' w1. \<lbrakk>w' \<in> w1 \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2'; fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w1) = {}; map f w' \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f w2'\<rbrakk> \<Longrightarrow> map f (e # w') \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f (e # w2')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
f e # map f w' \<in> f e # map f w1' \<otimes>\<^bsub>\<alpha>\<^esub> map f w2

goal (1 subgoal):
 1. map f (e # w') \<in> map f (e # w1') \<otimes>\<^bsub>\<alpha>\<^esub> map f w2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map f (e # w') \<in> map f (e # w1') \<otimes>\<^bsub>\<alpha>\<^esub> map f w2

goal (1 subgoal):
 1. \<And>e w' w2' w1. \<lbrakk>w' \<in> w1 \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2'; fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w1) = {}; map f w' \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f w2'\<rbrakk> \<Longrightarrow> map f (e # w') \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f (e # w2')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e w' w2' w1. \<lbrakk>w' \<in> w1 \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2'; fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w1) = {}; map f w' \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f w2'\<rbrakk> \<Longrightarrow> map f (e # w') \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f (e # w2')
[PROOF STEP]
case (right e w' w2' w1)
[PROOF STATE]
proof (state)
this:
w' \<in> w1 \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2'
fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w1) = {}
map f w' \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f w2'

goal (1 subgoal):
 1. \<And>e w' w2' w1. \<lbrakk>w' \<in> w1 \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2'; fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w1) = {}; map f w' \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f w2'\<rbrakk> \<Longrightarrow> map f (e # w') \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f (e # w2')
[PROOF STEP]
have "f e # map f w' \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> f e # map f w2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f e # map f w' \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> f e # map f w2'
[PROOF STEP]
proof (rule cil_cons2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. map f w' \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f w2'
 2. fst (\<alpha> (f e)) \<inter> mon_pl (map \<alpha> (map f w1)) = {}
[PROOF STEP]
from right(2)
[PROOF STATE]
proof (chain)
picking this:
fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w1) = {}
[PROOF STEP]
have "fst ((\<alpha>\<circ>f) e) \<inter> mon_pl (map \<alpha> (map f w1)) = {}"
[PROOF STATE]
proof (prove)
using this:
fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w1) = {}

goal (1 subgoal):
 1. fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map \<alpha> (map f w1)) = {}
[PROOF STEP]
by (simp only: map_map[symmetric])
[PROOF STATE]
proof (state)
this:
fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map \<alpha> (map f w1)) = {}

goal (2 subgoals):
 1. map f w' \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f w2'
 2. fst (\<alpha> (f e)) \<inter> mon_pl (map \<alpha> (map f w1)) = {}
[PROOF STEP]
thus "fst (\<alpha> (f e)) \<inter> mon_pl (map \<alpha> (map f w1)) = {}"
[PROOF STATE]
proof (prove)
using this:
fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map \<alpha> (map f w1)) = {}

goal (1 subgoal):
 1. fst (\<alpha> (f e)) \<inter> mon_pl (map \<alpha> (map f w1)) = {}
[PROOF STEP]
by (simp only: o_apply)
[PROOF STATE]
proof (state)
this:
fst (\<alpha> (f e)) \<inter> mon_pl (map \<alpha> (map f w1)) = {}

goal (1 subgoal):
 1. map f w' \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f w2'
[PROOF STEP]
qed (rule right(3))
[PROOF STATE]
proof (state)
this:
f e # map f w' \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> f e # map f w2'

goal (1 subgoal):
 1. \<And>e w' w2' w1. \<lbrakk>w' \<in> w1 \<otimes>\<^bsub>(\<alpha> \<circ> f)\<^esub> w2'; fst ((\<alpha> \<circ> f) e) \<inter> mon_pl (map (\<alpha> \<circ> f) w1) = {}; map f w' \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f w2'\<rbrakk> \<Longrightarrow> map f (e # w') \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f (e # w2')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
f e # map f w' \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> f e # map f w2'

goal (1 subgoal):
 1. map f (e # w') \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f (e # w2')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map f (e # w') \<in> map f w1 \<otimes>\<^bsub>\<alpha>\<^esub> map f (e # w2')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fac_strict[simp]: "fac\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fac\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma fac_body_strict[simp]: "fac_body\<cdot>r\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fac_body\<cdot>r\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
unfolding fac_body_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> r n. If n =\<^sub>B 0 then 1 else n * r\<cdot>(n - 1))\<cdot>r\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by simp


[STATEMENT]
lemma fac_fac_body_eq: "fac = fix\<cdot>fac_body"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fac = fix\<cdot>fac_body
[PROOF STEP]
unfolding fac_body_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fac = (\<mu> r. \<Lambda> n. If n =\<^sub>B 0 then 1 else n * r\<cdot>(n - 1))
[PROOF STEP]
by (rule cfun_eqI, subst fac_def, simp)


[STATEMENT]
lemma wrapB_unwrapB_body:
  assumes strictF: "f\<cdot>\<bottom> = \<bottom>"
  shows "(wrapB oo unwrapB)\<cdot>f = f" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (wrapB oo unwrapB)\<cdot>f = f
[PROOF STEP]
proof(rule cfun_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (wrapB oo unwrapB)\<cdot>f\<cdot>x = f\<cdot>x
[PROOF STEP]
fix x :: Nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (wrapB oo unwrapB)\<cdot>f\<cdot>x = f\<cdot>x
[PROOF STEP]
have "?lhs\<cdot>x = unbox\<cdot>x >>= (\<Lambda> x'. unwrapB\<cdot>f\<cdot>x' >>= box)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (wrapB oo unwrapB)\<cdot>f\<cdot>x = unbox\<cdot>x >>= (\<Lambda> x'. unwrapB\<cdot>f\<cdot>x' >>= box)
[PROOF STEP]
unfolding wrapB_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<Lambda> f x. unbox\<cdot>x >>= f >>= box) oo unwrapB)\<cdot>f\<cdot>x = unbox\<cdot>x >>= (\<Lambda> x'. unwrapB\<cdot>f\<cdot>x' >>= box)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(wrapB oo unwrapB)\<cdot>f\<cdot>x = unbox\<cdot>x >>= (\<Lambda> x'. unwrapB\<cdot>f\<cdot>x' >>= box)

goal (1 subgoal):
 1. \<And>x. (wrapB oo unwrapB)\<cdot>f\<cdot>x = f\<cdot>x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(wrapB oo unwrapB)\<cdot>f\<cdot>x = unbox\<cdot>x >>= (\<Lambda> x'. unwrapB\<cdot>f\<cdot>x' >>= box)

goal (1 subgoal):
 1. \<And>x. (wrapB oo unwrapB)\<cdot>f\<cdot>x = f\<cdot>x
[PROOF STEP]
have "\<dots> = unbox\<cdot>x >>= (\<Lambda> x'. unbox\<cdot>(f\<cdot>(box\<cdot>x')) >>= box)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unbox\<cdot>x >>= (\<Lambda> x'. unwrapB\<cdot>f\<cdot>x' >>= box) = unbox\<cdot>x >>= (\<Lambda> x'. unbox\<cdot>(f\<cdot>(box\<cdot>x')) >>= box)
[PROOF STEP]
unfolding unwrapB_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unbox\<cdot>x >>= (\<Lambda> x'. (\<Lambda> f. unbox oo f oo box)\<cdot>f\<cdot>x' >>= box) = unbox\<cdot>x >>= (\<Lambda> x'. unbox\<cdot>(f\<cdot>(box\<cdot>x')) >>= box)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
unbox\<cdot>x >>= (\<Lambda> x'. unwrapB\<cdot>f\<cdot>x' >>= box) = unbox\<cdot>x >>= (\<Lambda> x'. unbox\<cdot>(f\<cdot>(box\<cdot>x')) >>= box)

goal (1 subgoal):
 1. \<And>x. (wrapB oo unwrapB)\<cdot>f\<cdot>x = f\<cdot>x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
unbox\<cdot>x >>= (\<Lambda> x'. unwrapB\<cdot>f\<cdot>x' >>= box) = unbox\<cdot>x >>= (\<Lambda> x'. unbox\<cdot>(f\<cdot>(box\<cdot>x')) >>= box)

goal (1 subgoal):
 1. \<And>x. (wrapB oo unwrapB)\<cdot>f\<cdot>x = f\<cdot>x
[PROOF STEP]
from strictF
[PROOF STATE]
proof (chain)
picking this:
f\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
have "\<dots> = f\<cdot>x"
[PROOF STATE]
proof (prove)
using this:
f\<cdot>\<bottom> = \<bottom>

goal (1 subgoal):
 1. unbox\<cdot>x >>= (\<Lambda> x'. unbox\<cdot>(f\<cdot>(box\<cdot>x')) >>= box) = f\<cdot>x
[PROOF STEP]
by (cases x, simp_all)
[PROOF STATE]
proof (state)
this:
unbox\<cdot>x >>= (\<Lambda> x'. unbox\<cdot>(f\<cdot>(box\<cdot>x')) >>= box) = f\<cdot>x

goal (1 subgoal):
 1. \<And>x. (wrapB oo unwrapB)\<cdot>f\<cdot>x = f\<cdot>x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(wrapB oo unwrapB)\<cdot>f\<cdot>x = f\<cdot>x
[PROOF STEP]
show "?lhs\<cdot>x = ?rhs\<cdot>x"
[PROOF STATE]
proof (prove)
using this:
(wrapB oo unwrapB)\<cdot>f\<cdot>x = f\<cdot>x

goal (1 subgoal):
 1. (wrapB oo unwrapB)\<cdot>f\<cdot>x = f\<cdot>x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(wrapB oo unwrapB)\<cdot>f\<cdot>x = f\<cdot>x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fac_fac_ww_eq: "fac = fac_wrap" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fac = fac_wrap
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fac = fac_wrap
[PROOF STEP]
have "wrapB oo unwrapB oo fac_body = fac_body"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrapB oo unwrapB oo fac_body = fac_body
[PROOF STEP]
using wrapB_unwrapB_body[OF fac_body_strict]
[PROOF STATE]
proof (prove)
using this:
(wrapB oo unwrapB)\<cdot>(fac_body\<cdot>?r1) = fac_body\<cdot>?r1

goal (1 subgoal):
 1. wrapB oo unwrapB oo fac_body = fac_body
[PROOF STEP]
by - (rule cfun_eqI, simp)
[PROOF STATE]
proof (state)
this:
wrapB oo unwrapB oo fac_body = fac_body

goal (1 subgoal):
 1. fac = fac_wrap
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
wrapB oo unwrapB oo fac_body = fac_body

goal (1 subgoal):
 1. fac = fac_wrap
[PROOF STEP]
using worker_wrapper_body[where computation=fac and body=fac_body and wrap=wrapB and unwrap=unwrapB]
[PROOF STATE]
proof (prove)
using this:
wrapB oo unwrapB oo fac_body = fac_body
\<lbrakk>wrapB oo unwrapB oo fac_body = fac_body; fac = fix\<cdot>fac_body\<rbrakk> \<Longrightarrow> fac = wrapB\<cdot>(fix\<cdot>(unwrapB oo fac_body oo wrapB))

goal (1 subgoal):
 1. fac = fac_wrap
[PROOF STEP]
unfolding fac_work_def fac_wrap_def
[PROOF STATE]
proof (prove)
using this:
wrapB oo unwrapB oo fac_body = fac_body
\<lbrakk>wrapB oo unwrapB oo fac_body = fac_body; fac = fix\<cdot>fac_body\<rbrakk> \<Longrightarrow> fac = wrapB\<cdot>(fix\<cdot>(unwrapB oo fac_body oo wrapB))

goal (1 subgoal):
 1. fac = wrapB\<cdot>(fix\<cdot>(unwrapB oo fac_body oo wrapB))
[PROOF STEP]
by (simp add: fac_fac_body_eq)
[PROOF STATE]
proof (state)
this:
fac = fac_wrap

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fac_body_final_fac_body': "fac_body_final = fac_body'" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fac_body_final = fac_body'
[PROOF STEP]
proof(rule cfun_eqI)+
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. fac_body_final\<cdot>x\<cdot>xa = fac_body'\<cdot>x\<cdot>xa
[PROOF STEP]
fix r x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. fac_body_final\<cdot>x\<cdot>xa = fac_body'\<cdot>x\<cdot>xa
[PROOF STEP]
show "?lhs\<cdot>r\<cdot>x = ?rhs\<cdot>r\<cdot>x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fac_body_final\<cdot>r\<cdot>x = fac_body'\<cdot>r\<cdot>x
[PROOF STEP]
using bbind_case_distr_strict[where f="unbox" and g="r\<cdot>(x -\<^sub># 1)" and h="(\<Lambda> b. box\<cdot>(x *\<^sub># b))"]
[PROOF STATE]
proof (prove)
using this:
unbox\<cdot>\<bottom> = \<bottom> \<Longrightarrow> unbox\<cdot>(r\<cdot>(x -\<^sub># 1) >>= (\<Lambda> b. box\<cdot>(x *\<^sub># b))) = r\<cdot>(x -\<^sub># 1) >>= (\<Lambda> xa. unbox\<cdot>((\<Lambda> b. box\<cdot>(x *\<^sub># b))\<cdot>xa))

goal (1 subgoal):
 1. fac_body_final\<cdot>r\<cdot>x = fac_body'\<cdot>r\<cdot>x
[PROOF STEP]
unfolding fac_body_final_def fac_body'_def uMinus_def uMult_def zero_Nat_def one_Nat_def
[PROOF STATE]
proof (prove)
using this:
unbox\<cdot>\<bottom> = \<bottom> \<Longrightarrow> unbox\<cdot>(r\<cdot>((\<Lambda> x y. Discr (undiscr x - undiscr y))\<cdot>x\<cdot>1) >>= (\<Lambda> b. box\<cdot>((\<Lambda> x y. Discr (undiscr x * undiscr y))\<cdot>x\<cdot>b))) = r\<cdot>((\<Lambda> x y. Discr (undiscr x - undiscr y))\<cdot>x\<cdot>1) >>= (\<Lambda> xa. unbox\<cdot>((\<Lambda> b. box\<cdot>((\<Lambda> x y. Discr (undiscr x * undiscr y))\<cdot>x\<cdot>b))\<cdot>xa))

goal (1 subgoal):
 1. (\<Lambda> r n. if n = 0 then up\<cdot>1 else r\<cdot>((\<Lambda> x y. Discr (undiscr x - undiscr y))\<cdot>n\<cdot>1) >>= (\<Lambda> b. up\<cdot>((\<Lambda> x y. Discr (undiscr x * undiscr y))\<cdot>n\<cdot>b)))\<cdot>r\<cdot>x = (\<Lambda> r n. unbox\<cdot>(If box\<cdot>n =\<^sub>B box\<cdot>0 then box\<cdot>1 else unbox\<cdot>(box\<cdot>n - box\<cdot>1) >>= r >>= (\<Lambda> b. box\<cdot>n * box\<cdot>b)))\<cdot>r\<cdot>x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fac_body_final\<cdot>r\<cdot>x = fac_body'\<cdot>r\<cdot>x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fac_fac_final: "fac = fac_final" (is "?lhs=?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fac = fac_final
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fac = fac_final
[PROOF STEP]
have "?lhs = fac_wrap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fac = fac_wrap
[PROOF STEP]
by (rule fac_fac_ww_eq)
[PROOF STATE]
proof (state)
this:
fac = fac_wrap

goal (1 subgoal):
 1. fac = fac_final
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fac = fac_wrap

goal (1 subgoal):
 1. fac = fac_final
[PROOF STEP]
have "\<dots> = wrapB\<cdot>fac_work"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fac_wrap = wrapB\<cdot>fac_work
[PROOF STEP]
by (simp only: fac_wrap_def)
[PROOF STATE]
proof (state)
this:
fac_wrap = wrapB\<cdot>fac_work

goal (1 subgoal):
 1. fac = fac_final
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fac_wrap = wrapB\<cdot>fac_work

goal (1 subgoal):
 1. fac = fac_final
[PROOF STEP]
have "\<dots> = wrapB\<cdot>(fix\<cdot>(unwrapB oo fac_body oo wrapB))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrapB\<cdot>fac_work = wrapB\<cdot>(fix\<cdot>(unwrapB oo fac_body oo wrapB))
[PROOF STEP]
by (simp only: fac_work_def)
[PROOF STATE]
proof (state)
this:
wrapB\<cdot>fac_work = wrapB\<cdot>(fix\<cdot>(unwrapB oo fac_body oo wrapB))

goal (1 subgoal):
 1. fac = fac_final
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wrapB\<cdot>fac_work = wrapB\<cdot>(fix\<cdot>(unwrapB oo fac_body oo wrapB))

goal (1 subgoal):
 1. fac = fac_final
[PROOF STEP]
have "\<dots> = wrapB\<cdot>(fix\<cdot>fac_body')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrapB\<cdot>(fix\<cdot>(unwrapB oo fac_body oo wrapB)) = wrapB\<cdot>(fix\<cdot>fac_body')
[PROOF STEP]
by (simp only: fac_body'_fac_body)
[PROOF STATE]
proof (state)
this:
wrapB\<cdot>(fix\<cdot>(unwrapB oo fac_body oo wrapB)) = wrapB\<cdot>(fix\<cdot>fac_body')

goal (1 subgoal):
 1. fac = fac_final
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wrapB\<cdot>(fix\<cdot>(unwrapB oo fac_body oo wrapB)) = wrapB\<cdot>(fix\<cdot>fac_body')

goal (1 subgoal):
 1. fac = fac_final
[PROOF STEP]
have "\<dots> = wrapB\<cdot>fac_work_final"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrapB\<cdot>(fix\<cdot>fac_body') = wrapB\<cdot>fac_work_final
[PROOF STEP]
by (simp only: fac_body_final_fac_body' fac_work_final_def)
[PROOF STATE]
proof (state)
this:
wrapB\<cdot>(fix\<cdot>fac_body') = wrapB\<cdot>fac_work_final

goal (1 subgoal):
 1. fac = fac_final
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wrapB\<cdot>(fix\<cdot>fac_body') = wrapB\<cdot>fac_work_final

goal (1 subgoal):
 1. fac = fac_final
[PROOF STEP]
have "\<dots> = fac_final"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrapB\<cdot>fac_work_final = fac_final
[PROOF STEP]
by (simp add: fac_final_def wrapB_def)
[PROOF STATE]
proof (state)
this:
wrapB\<cdot>fac_work_final = fac_final

goal (1 subgoal):
 1. fac = fac_final
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
fac = fac_final
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fac = fac_final

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a2n_strict[simp]: "a2n\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a2n\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
unfolding a2n_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> a. a\<cdot>1)\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by simp


[STATEMENT]
lemma a2n_n2a: "a2n\<cdot>(n2a\<cdot>u) = up\<cdot>u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a2n\<cdot>(n2a\<cdot>u) = up\<cdot>u
[PROOF STEP]
unfolding a2n_def n2a_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> a. a\<cdot>1)\<cdot>((\<Lambda> m n. up\<cdot>(m *\<^sub># n))\<cdot>u) = up\<cdot>u
[PROOF STEP]
by (simp add: uMult_arithmetic)


[STATEMENT]
lemma A_hom_mult: "n2a\<cdot>(x *\<^sub># y) = (n2a\<cdot>x >=> n2a\<cdot>y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n2a\<cdot>(x *\<^sub># y) = n2a\<cdot>x >=> n2a\<cdot>y
[PROOF STEP]
unfolding n2a_def bKleisli_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> m n. up\<cdot>(m *\<^sub># n))\<cdot>(x *\<^sub># y) = (\<Lambda> f g x. f\<cdot>x >>= g)\<cdot>((\<Lambda> m n. up\<cdot>(m *\<^sub># n))\<cdot>x)\<cdot>((\<Lambda> m n. up\<cdot>(m *\<^sub># n))\<cdot>y)
[PROOF STEP]
by (simp add: uMult_arithmetic)


[STATEMENT]
lemma unwrapA_strict[simp]: "unwrapA\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unwrapA\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
unfolding unwrapA_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> f n. f\<cdot>n >>= n2a)\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by (rule cfun_eqI) simp


[STATEMENT]
lemma wrapA_unwrapA_id: "wrapA oo unwrapA = ID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wrapA oo unwrapA = ID
[PROOF STEP]
unfolding wrapA_def unwrapA_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_cfun ((oo) a2n) oo (\<Lambda> f n. f\<cdot>n >>= n2a) = ID
[PROOF STEP]
apply (rule cfun_eqI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. (Abs_cfun ((oo) a2n) oo (\<Lambda> f n. f\<cdot>n >>= n2a))\<cdot>x\<cdot>xa = ID\<cdot>x\<cdot>xa
[PROOF STEP]
apply (case_tac "x\<cdot>xa")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. x\<cdot>xa = \<bottom> \<Longrightarrow> (Abs_cfun ((oo) a2n) oo (\<Lambda> f n. f\<cdot>n >>= n2a))\<cdot>x\<cdot>xa = ID\<cdot>x\<cdot>xa
 2. \<And>x xa xb. x\<cdot>xa = up\<cdot>xb \<Longrightarrow> (Abs_cfun ((oo) a2n) oo (\<Lambda> f n. f\<cdot>n >>= n2a))\<cdot>x\<cdot>xa = ID\<cdot>x\<cdot>xa
[PROOF STEP]
apply (simp_all add: a2n_n2a)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fac_acc_body1_fac_body_final_eq: "fac_acc_body1 = unwrapA oo fac_body_final oo wrapA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fac_acc_body1 = unwrapA oo fac_body_final oo wrapA
[PROOF STEP]
unfolding fac_acc_body1_def fac_body_final_def wrapA_def unwrapA_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> r n. if n = 0 then n2a\<cdot>1 else Abs_cfun ((oo) a2n)\<cdot>r\<cdot>(n -\<^sub># 1) >>= (\<Lambda> res. n2a\<cdot>(n *\<^sub># res))) = (\<Lambda> f n. f\<cdot>n >>= n2a) oo (\<Lambda> r n. if n = 0 then up\<cdot>1 else r\<cdot>(n -\<^sub># 1) >>= (\<Lambda> b. up\<cdot>(n *\<^sub># b))) oo Abs_cfun ((oo) a2n)
[PROOF STEP]
by (rule cfun_eqI)+ simp


[STATEMENT]
lemma fac_acc_body2_body1_eq: "fac_acc_body2 = fac_acc_body1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fac_acc_body2 = fac_acc_body1
[PROOF STEP]
unfolding fac_acc_body1_def fac_acc_body2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> r n. if n = 0 then n2a\<cdot>1 else wrapA\<cdot>r\<cdot>(n -\<^sub># 1) >>= (\<Lambda> res. n2a\<cdot>n >=> n2a\<cdot>res)) = (\<Lambda> r n. if n = 0 then n2a\<cdot>1 else wrapA\<cdot>r\<cdot>(n -\<^sub># 1) >>= (\<Lambda> res. n2a\<cdot>(n *\<^sub># res)))
[PROOF STEP]
by (rule cfun_eqI)+ (simp add: A_hom_mult)


[STATEMENT]
lemma fac_acc_body3_body2: "fac_acc_body3 oo (unwrapA oo wrapA) = fac_acc_body2" (is "?lhs=?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fac_acc_body3 oo unwrapA oo wrapA = fac_acc_body2
[PROOF STEP]
proof(rule cfun_eqI)+
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa xb. (fac_acc_body3 oo unwrapA oo wrapA)\<cdot>x\<cdot>xa\<cdot>xb = fac_acc_body2\<cdot>x\<cdot>xa\<cdot>xb
[PROOF STEP]
fix r n acc
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa xb. (fac_acc_body3 oo unwrapA oo wrapA)\<cdot>x\<cdot>xa\<cdot>xb = fac_acc_body2\<cdot>x\<cdot>xa\<cdot>xb
[PROOF STEP]
show "((fac_acc_body3 oo (unwrapA oo wrapA))\<cdot>r\<cdot>n\<cdot>acc) = fac_acc_body2\<cdot>r\<cdot>n\<cdot>acc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fac_acc_body3 oo unwrapA oo wrapA)\<cdot>r\<cdot>n\<cdot>acc = fac_acc_body2\<cdot>r\<cdot>n\<cdot>acc
[PROOF STEP]
unfolding fac_acc_body2_def fac_acc_body3_def unwrapA_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<Lambda> r n. if n = 0 then n2a\<cdot>1 else n2a\<cdot>n >=> r\<cdot>(n -\<^sub># 1)) oo (\<Lambda> f n. f\<cdot>n >>= n2a) oo wrapA)\<cdot>r\<cdot>n\<cdot>acc = (\<Lambda> r n. if n = 0 then n2a\<cdot>1 else wrapA\<cdot>r\<cdot>(n -\<^sub># 1) >>= (\<Lambda> res. n2a\<cdot>n >=> n2a\<cdot>res))\<cdot>r\<cdot>n\<cdot>acc
[PROOF STEP]
using bbind_case_distr_strict[where f="\<Lambda> y. n2a\<cdot>n >=> y" and h="n2a", symmetric]
[PROOF STATE]
proof (prove)
using this:
Abs_cfun ((>=>) (n2a\<cdot>n))\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ?g >>= (\<Lambda> x. Abs_cfun ((>=>) (n2a\<cdot>n))\<cdot>(n2a\<cdot>x)) = Abs_cfun ((>=>) (n2a\<cdot>n))\<cdot>(?g >>= n2a)

goal (1 subgoal):
 1. ((\<Lambda> r n. if n = 0 then n2a\<cdot>1 else n2a\<cdot>n >=> r\<cdot>(n -\<^sub># 1)) oo (\<Lambda> f n. f\<cdot>n >>= n2a) oo wrapA)\<cdot>r\<cdot>n\<cdot>acc = (\<Lambda> r n. if n = 0 then n2a\<cdot>1 else wrapA\<cdot>r\<cdot>(n -\<^sub># 1) >>= (\<Lambda> res. n2a\<cdot>n >=> n2a\<cdot>res))\<cdot>r\<cdot>n\<cdot>acc
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(fac_acc_body3 oo unwrapA oo wrapA)\<cdot>r\<cdot>n\<cdot>acc = fac_acc_body2\<cdot>r\<cdot>n\<cdot>acc

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fac_work_final_body3_eq: "fac_work_final = wrapA\<cdot>(fix\<cdot>fac_acc_body3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fac_work_final = wrapA\<cdot>(fix\<cdot>fac_acc_body3)
[PROOF STEP]
unfolding fac_work_final_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fix\<cdot>fac_body_final = wrapA\<cdot>(fix\<cdot>fac_acc_body3)
[PROOF STEP]
by (rule worker_wrapper_fusion_new[OF wrapA_unwrapA_id unwrapA_strict])
     (simp add: fac_acc_body3_body2 fac_acc_body2_body1_eq fac_acc_body1_fac_body_final_eq)


[STATEMENT]
lemma fac_acc_work_final_fac_acc_work3_eq: "fac_acc_body_final = fac_acc_body3" (is "?lhs=?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fac_acc_body_final = fac_acc_body3
[PROOF STEP]
unfolding fac_acc_body3_def fac_acc_body_final_def n2a_def bKleisli_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> r n acc. if n = 0 then up\<cdot>acc else r\<cdot>(n -\<^sub># 1)\<cdot>(n *\<^sub># acc)) = (\<Lambda> r n. if n = 0 then (\<Lambda> m n. up\<cdot>(m *\<^sub># n))\<cdot>1 else (\<Lambda> f g x. f\<cdot>x >>= g)\<cdot>((\<Lambda> m n. up\<cdot>(m *\<^sub># n))\<cdot>n)\<cdot>(r\<cdot>(n -\<^sub># 1)))
[PROOF STEP]
by (rule cfun_eqI)+
     (simp add: uMult_arithmetic)


[STATEMENT]
lemma extract_IPSets_generic0_length: "length (extract_IPSets_generic0 sel rs) = length rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (extract_IPSets_generic0 sel rs) = length rs
[PROOF STEP]
by(induction rs rule: extract_IPSets_generic0.induct) (simp_all)


[STATEMENT]
lemma "mergesort_remdups [(1::ipv4addr, 2::nat), (8,0), (8,1), (2,2), (2,4), (1,2), (2,2)] =
        [(1, 2), (2, 2), (2, 4), (8, 0), (8, 1)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mergesort_remdups [(1, 2), (8, 0), (8, 1), (2, 2), (2, 4), (1, 2), (2, 2)] = [(1, 2), (2, 2), (2, 4), (8, 0), (8, 1)]
[PROOF STEP]
by eval


[STATEMENT]
lemma extract_src_dst_ips_length: "length (extract_src_dst_ips rs acc) = 2*length rs + length acc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (extract_src_dst_ips rs acc) = 2 * length rs + length acc
[PROOF STEP]
proof(induction rs arbitrary: acc)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>acc. length (extract_src_dst_ips [] acc) = 2 * length [] + length acc
 2. \<And>a rs acc. (\<And>acc. length (extract_src_dst_ips rs acc) = 2 * length rs + length acc) \<Longrightarrow> length (extract_src_dst_ips (a # rs) acc) = 2 * length (a # rs) + length acc
[PROOF STEP]
case (Cons r rs)
[PROOF STATE]
proof (state)
this:
length (extract_src_dst_ips rs ?acc) = 2 * length rs + length ?acc

goal (2 subgoals):
 1. \<And>acc. length (extract_src_dst_ips [] acc) = 2 * length [] + length acc
 2. \<And>a rs acc. (\<And>acc. length (extract_src_dst_ips rs acc) = 2 * length rs + length acc) \<Longrightarrow> length (extract_src_dst_ips (a # rs) acc) = 2 * length (a # rs) + length acc
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
length (extract_src_dst_ips rs ?acc) = 2 * length rs + length ?acc

goal (1 subgoal):
 1. length (extract_src_dst_ips (r # rs) acc) = 2 * length (r # rs) + length acc
[PROOF STEP]
by(cases r, simp)
[PROOF STATE]
proof (state)
this:
length (extract_src_dst_ips (r # rs) acc) = 2 * length (r # rs) + length acc

goal (1 subgoal):
 1. \<And>acc. length (extract_src_dst_ips [] acc) = 2 * length [] + length acc
[PROOF STEP]
qed(simp)


[STATEMENT]
lemma extract_IPSets:
  "set (extract_IPSets rs) = set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (extract_IPSets rs) = set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (extract_IPSets rs) = set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (extract_IPSets rs) = set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs)
[PROOF STEP]
fix acc
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (extract_IPSets rs) = set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs)
[PROOF STEP]
have "ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips rs acc) =
            ipcidr_tuple_to_wordinterval ` set acc \<union> set (extract_IPSets_generic0 src rs) \<union>
            set (extract_IPSets_generic0 dst rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips rs acc) = ipcidr_tuple_to_wordinterval ` set acc \<union> set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs)
[PROOF STEP]
proof(induction rs arbitrary: acc)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>acc. ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips [] acc) = ipcidr_tuple_to_wordinterval ` set acc \<union> set (extract_IPSets_generic0 src []) \<union> set (extract_IPSets_generic0 dst [])
 2. \<And>a rs acc. (\<And>acc. ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips rs acc) = ipcidr_tuple_to_wordinterval ` set acc \<union> set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs)) \<Longrightarrow> ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips (a # rs) acc) = ipcidr_tuple_to_wordinterval ` set acc \<union> set (extract_IPSets_generic0 src (a # rs)) \<union> set (extract_IPSets_generic0 dst (a # rs))
[PROOF STEP]
case (Cons r rs )
[PROOF STATE]
proof (state)
this:
ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips rs ?acc) = ipcidr_tuple_to_wordinterval ` set ?acc \<union> set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs)

goal (2 subgoals):
 1. \<And>acc. ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips [] acc) = ipcidr_tuple_to_wordinterval ` set acc \<union> set (extract_IPSets_generic0 src []) \<union> set (extract_IPSets_generic0 dst [])
 2. \<And>a rs acc. (\<And>acc. ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips rs acc) = ipcidr_tuple_to_wordinterval ` set acc \<union> set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs)) \<Longrightarrow> ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips (a # rs) acc) = ipcidr_tuple_to_wordinterval ` set acc \<union> set (extract_IPSets_generic0 src (a # rs)) \<union> set (extract_IPSets_generic0 dst (a # rs))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips rs ?acc) = ipcidr_tuple_to_wordinterval ` set ?acc \<union> set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs)

goal (1 subgoal):
 1. ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips (r # rs) acc) = ipcidr_tuple_to_wordinterval ` set acc \<union> set (extract_IPSets_generic0 src (r # rs)) \<union> set (extract_IPSets_generic0 dst (r # rs))
[PROOF STEP]
apply(cases r)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<And>acc. ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips rs acc) = ipcidr_tuple_to_wordinterval ` set acc \<union> set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs); r = SimpleRule x1 x2\<rbrakk> \<Longrightarrow> ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips (r # rs) acc) = ipcidr_tuple_to_wordinterval ` set acc \<union> set (extract_IPSets_generic0 src (r # rs)) \<union> set (extract_IPSets_generic0 dst (r # rs))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<And>acc. ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips rs acc) = ipcidr_tuple_to_wordinterval ` set acc \<union> set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs); r = SimpleRule x1 x2\<rbrakk> \<Longrightarrow> insert (ipcidr_tuple_to_wordinterval (src x1)) (insert (ipcidr_tuple_to_wordinterval (dst x1)) (ipcidr_tuple_to_wordinterval ` set acc \<union> set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs))) = insert (ipcidr_tuple_to_wordinterval (dst x1)) (insert (ipcidr_tuple_to_wordinterval (src x1)) (ipcidr_tuple_to_wordinterval ` set acc \<union> set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs)))
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips (r # rs) acc) = ipcidr_tuple_to_wordinterval ` set acc \<union> set (extract_IPSets_generic0 src (r # rs)) \<union> set (extract_IPSets_generic0 dst (r # rs))

goal (1 subgoal):
 1. \<And>acc. ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips [] acc) = ipcidr_tuple_to_wordinterval ` set acc \<union> set (extract_IPSets_generic0 src []) \<union> set (extract_IPSets_generic0 dst [])
[PROOF STEP]
qed(simp)
[PROOF STATE]
proof (state)
this:
ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips rs acc) = ipcidr_tuple_to_wordinterval ` set acc \<union> set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs)

goal (1 subgoal):
 1. set (extract_IPSets rs) = set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips rs ?acc2) = ipcidr_tuple_to_wordinterval ` set ?acc2 \<union> set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs)

goal (1 subgoal):
 1. set (extract_IPSets rs) = set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips rs ?acc2) = ipcidr_tuple_to_wordinterval ` set ?acc2 \<union> set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs)

goal (1 subgoal):
 1. set (extract_IPSets rs) = set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs)
[PROOF STEP]
unfolding extract_IPSets_def
[PROOF STATE]
proof (prove)
using this:
ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips rs ?acc2) = ipcidr_tuple_to_wordinterval ` set ?acc2 \<union> set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs)

goal (1 subgoal):
 1. set (map ipcidr_tuple_to_wordinterval (mergesort_remdups (extract_src_dst_ips rs []))) = set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs)
[PROOF STEP]
by(simp_all add: extract_IPSets_def mergesort_remdups_correct)
[PROOF STATE]
proof (state)
this:
set (extract_IPSets rs) = set (extract_IPSets_generic0 src rs) \<union> set (extract_IPSets_generic0 dst rs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "(a::nat) div 2 + a mod 2 \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a div 2 + a mod 2 \<le> a
[PROOF STEP]
by fastforce


[STATEMENT]
lemma merge_length: "length (merge l1 l2) \<le> length l1 + length l2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (merge l1 l2) \<le> length l1 + length l2
[PROOF STEP]
by(induction l1 l2 rule: merge.induct) auto


[STATEMENT]
lemma merge_list_length: "length (merge_list as ls) \<le> length (concat (as @ ls))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (merge_list as ls) \<le> length (concat (as @ ls))
[PROOF STEP]
proof(induction as ls rule: merge_list.induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. length (merge_list [] []) \<le> length (concat ([] @ []))
 2. \<And>l. length (merge_list [] [l]) \<le> length (concat ([] @ [l]))
 3. \<And>la acc2. length (merge_list [] (la # acc2)) \<le> length (concat ([] @ la # acc2)) \<Longrightarrow> length (merge_list (la # acc2) []) \<le> length (concat ((la # acc2) @ []))
 4. \<And>la acc2 l. length (merge_list [] (l # la # acc2)) \<le> length (concat ([] @ l # la # acc2)) \<Longrightarrow> length (merge_list (la # acc2) [l]) \<le> length (concat ((la # acc2) @ [l]))
 5. \<And>acc2 l1 l2 ls. length (merge_list (merge l1 l2 # acc2) ls) \<le> length (concat ((merge l1 l2 # acc2) @ ls)) \<Longrightarrow> length (merge_list acc2 (l1 # l2 # ls)) \<le> length (concat (acc2 @ l1 # l2 # ls))
[PROOF STEP]
case (5 l1 l2 acc2 ls)
[PROOF STATE]
proof (state)
this:
length (merge_list (merge l2 acc2 # l1) ls) \<le> length (concat ((merge l2 acc2 # l1) @ ls))

goal (5 subgoals):
 1. length (merge_list [] []) \<le> length (concat ([] @ []))
 2. \<And>l. length (merge_list [] [l]) \<le> length (concat ([] @ [l]))
 3. \<And>la acc2. length (merge_list [] (la # acc2)) \<le> length (concat ([] @ la # acc2)) \<Longrightarrow> length (merge_list (la # acc2) []) \<le> length (concat ((la # acc2) @ []))
 4. \<And>la acc2 l. length (merge_list [] (l # la # acc2)) \<le> length (concat ([] @ l # la # acc2)) \<Longrightarrow> length (merge_list (la # acc2) [l]) \<le> length (concat ((la # acc2) @ [l]))
 5. \<And>acc2 l1 l2 ls. length (merge_list (merge l1 l2 # acc2) ls) \<le> length (concat ((merge l1 l2 # acc2) @ ls)) \<Longrightarrow> length (merge_list acc2 (l1 # l2 # ls)) \<le> length (concat (acc2 @ l1 # l2 # ls))
[PROOF STEP]
have "length (merge l2 acc2) \<le> length l2 + length acc2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (merge l2 acc2) \<le> length l2 + length acc2
[PROOF STEP]
using merge_length
[PROOF STATE]
proof (prove)
using this:
length (merge ?l1.0 ?l2.0) \<le> length ?l1.0 + length ?l2.0

goal (1 subgoal):
 1. length (merge l2 acc2) \<le> length l2 + length acc2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length (merge l2 acc2) \<le> length l2 + length acc2

goal (5 subgoals):
 1. length (merge_list [] []) \<le> length (concat ([] @ []))
 2. \<And>l. length (merge_list [] [l]) \<le> length (concat ([] @ [l]))
 3. \<And>la acc2. length (merge_list [] (la # acc2)) \<le> length (concat ([] @ la # acc2)) \<Longrightarrow> length (merge_list (la # acc2) []) \<le> length (concat ((la # acc2) @ []))
 4. \<And>la acc2 l. length (merge_list [] (l # la # acc2)) \<le> length (concat ([] @ l # la # acc2)) \<Longrightarrow> length (merge_list (la # acc2) [l]) \<le> length (concat ((la # acc2) @ [l]))
 5. \<And>acc2 l1 l2 ls. length (merge_list (merge l1 l2 # acc2) ls) \<le> length (concat ((merge l1 l2 # acc2) @ ls)) \<Longrightarrow> length (merge_list acc2 (l1 # l2 # ls)) \<le> length (concat (acc2 @ l1 # l2 # ls))
[PROOF STEP]
with 5
[PROOF STATE]
proof (chain)
picking this:
length (merge_list (merge l2 acc2 # l1) ls) \<le> length (concat ((merge l2 acc2 # l1) @ ls))
length (merge l2 acc2) \<le> length l2 + length acc2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length (merge_list (merge l2 acc2 # l1) ls) \<le> length (concat ((merge l2 acc2 # l1) @ ls))
length (merge l2 acc2) \<le> length l2 + length acc2

goal (1 subgoal):
 1. length (merge_list l1 (l2 # acc2 # ls)) \<le> length (concat (l1 @ l2 # acc2 # ls))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (merge_list l1 (l2 # acc2 # ls)) \<le> length (concat (l1 @ l2 # acc2 # ls))

goal (4 subgoals):
 1. length (merge_list [] []) \<le> length (concat ([] @ []))
 2. \<And>l. length (merge_list [] [l]) \<le> length (concat ([] @ [l]))
 3. \<And>la acc2. length (merge_list [] (la # acc2)) \<le> length (concat ([] @ la # acc2)) \<Longrightarrow> length (merge_list (la # acc2) []) \<le> length (concat ((la # acc2) @ []))
 4. \<And>la acc2 l. length (merge_list [] (l # la # acc2)) \<le> length (concat ([] @ l # la # acc2)) \<Longrightarrow> length (merge_list (la # acc2) [l]) \<le> length (concat ((la # acc2) @ [l]))
[PROOF STEP]
qed(simp_all)


[STATEMENT]
lemma mergesort_remdups_length: "length (mergesort_remdups as) \<le> length as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (mergesort_remdups as) \<le> length as
[PROOF STEP]
unfolding mergesort_remdups_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (merge_list [] (map (\<lambda>x. [x]) as)) \<le> length as
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (merge_list [] (map (\<lambda>x. [x]) as)) \<le> length as
[PROOF STEP]
have "concat ([] @ (map (\<lambda>x. [x]) as)) = as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concat ([] @ map (\<lambda>x. [x]) as) = as
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
concat ([] @ map (\<lambda>x. [x]) as) = as

goal (1 subgoal):
 1. length (merge_list [] (map (\<lambda>x. [x]) as)) \<le> length as
[PROOF STEP]
with merge_list_length
[PROOF STATE]
proof (chain)
picking this:
length (merge_list ?as ?ls) \<le> length (concat (?as @ ?ls))
concat ([] @ map (\<lambda>x. [x]) as) = as
[PROOF STEP]
show "length (merge_list [] (map (\<lambda>x. [x]) as)) \<le> length as"
[PROOF STATE]
proof (prove)
using this:
length (merge_list ?as ?ls) \<le> length (concat (?as @ ?ls))
concat ([] @ map (\<lambda>x. [x]) as) = as

goal (1 subgoal):
 1. length (merge_list [] (map (\<lambda>x. [x]) as)) \<le> length as
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
length (merge_list [] (map (\<lambda>x. [x]) as)) \<le> length as

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma extract_IPSets_length: "length (extract_IPSets rs) \<le> 2 * length rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (extract_IPSets rs) \<le> 2 * length rs
[PROOF STEP]
apply(simp add: extract_IPSets_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (mergesort_remdups (extract_src_dst_ips rs [])) \<le> 2 * length rs
[PROOF STEP]
using extract_src_dst_ips_length mergesort_remdups_length
[PROOF STATE]
proof (prove)
using this:
length (extract_src_dst_ips ?rs ?acc) = 2 * length ?rs + length ?acc
length (mergesort_remdups ?as) \<le> length ?as

goal (1 subgoal):
 1. length (mergesort_remdups (extract_src_dst_ips rs [])) \<le> 2 * length rs
[PROOF STEP]
by (metis add.right_neutral list.size(3))


[STATEMENT]
lemma extract_equi0:
  "set (map wordinterval_to_set (extract_IPSets_generic0 sel rs)) =
    (\<lambda>(base,len). ipset_from_cidr base len) ` sel ` match_sel ` set rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map wordinterval_to_set (extract_IPSets_generic0 sel rs)) = (\<lambda>(base, len). ipset_from_cidr base len) ` sel ` match_sel ` set rs
[PROOF STEP]
proof(induction rs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set (map wordinterval_to_set (extract_IPSets_generic0 sel [])) = (\<lambda>a. case a of (base, len) \<Rightarrow> ipset_from_cidr base len) ` sel ` match_sel ` set []
 2. \<And>a rs. set (map wordinterval_to_set (extract_IPSets_generic0 sel rs)) = (\<lambda>a. case a of (base, len) \<Rightarrow> ipset_from_cidr base len) ` sel ` match_sel ` set rs \<Longrightarrow> set (map wordinterval_to_set (extract_IPSets_generic0 sel (a # rs))) = (\<lambda>a. case a of (base, len) \<Rightarrow> ipset_from_cidr base len) ` sel ` match_sel ` set (a # rs)
[PROOF STEP]
case (Cons r rs)
[PROOF STATE]
proof (state)
this:
set (map wordinterval_to_set (extract_IPSets_generic0 sel rs)) = (\<lambda>a. case a of (base, len) \<Rightarrow> ipset_from_cidr base len) ` sel ` match_sel ` set rs

goal (2 subgoals):
 1. set (map wordinterval_to_set (extract_IPSets_generic0 sel [])) = (\<lambda>a. case a of (base, len) \<Rightarrow> ipset_from_cidr base len) ` sel ` match_sel ` set []
 2. \<And>a rs. set (map wordinterval_to_set (extract_IPSets_generic0 sel rs)) = (\<lambda>a. case a of (base, len) \<Rightarrow> ipset_from_cidr base len) ` sel ` match_sel ` set rs \<Longrightarrow> set (map wordinterval_to_set (extract_IPSets_generic0 sel (a # rs))) = (\<lambda>a. case a of (base, len) \<Rightarrow> ipset_from_cidr base len) ` sel ` match_sel ` set (a # rs)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
set (map wordinterval_to_set (extract_IPSets_generic0 sel rs)) = (\<lambda>a. case a of (base, len) \<Rightarrow> ipset_from_cidr base len) ` sel ` match_sel ` set rs

goal (1 subgoal):
 1. set (map wordinterval_to_set (extract_IPSets_generic0 sel (r # rs))) = (\<lambda>a. case a of (base, len) \<Rightarrow> ipset_from_cidr base len) ` sel ` match_sel ` set (r # rs)
[PROOF STEP]
apply(cases r, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>wordinterval_to_set ` set (extract_IPSets_generic0 sel rs) = (\<lambda>a. case a of (base, len) \<Rightarrow> ipset_from_cidr base len) ` sel ` match_sel ` set rs; r = SimpleRule x1 x2\<rbrakk> \<Longrightarrow> insert (wordinterval_to_set (ipcidr_tuple_to_wordinterval (sel x1))) ((\<lambda>x. case x of (x, xa) \<Rightarrow> ipset_from_cidr x xa) ` sel ` match_sel ` set rs) = insert (case sel x1 of (x, xa) \<Rightarrow> ipset_from_cidr x xa) ((\<lambda>x. case x of (x, xa) \<Rightarrow> ipset_from_cidr x xa) ` sel ` match_sel ` set rs)
[PROOF STEP]
using wordinterval_to_set_ipcidr_tuple_to_wordinterval
[PROOF STATE]
proof (prove)
using this:
wordinterval_to_set (ipcidr_tuple_to_wordinterval (?b, ?m)) = ipset_from_cidr ?b ?m

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>wordinterval_to_set ` set (extract_IPSets_generic0 sel rs) = (\<lambda>a. case a of (base, len) \<Rightarrow> ipset_from_cidr base len) ` sel ` match_sel ` set rs; r = SimpleRule x1 x2\<rbrakk> \<Longrightarrow> insert (wordinterval_to_set (ipcidr_tuple_to_wordinterval (sel x1))) ((\<lambda>x. case x of (x, xa) \<Rightarrow> ipset_from_cidr x xa) ` sel ` match_sel ` set rs) = insert (case sel x1 of (x, xa) \<Rightarrow> ipset_from_cidr x xa) ((\<lambda>x. case x of (x, xa) \<Rightarrow> ipset_from_cidr x xa) ` sel ` match_sel ` set rs)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
set (map wordinterval_to_set (extract_IPSets_generic0 sel (r # rs))) = (\<lambda>a. case a of (base, len) \<Rightarrow> ipset_from_cidr base len) ` sel ` match_sel ` set (r # rs)

goal (1 subgoal):
 1. set (map wordinterval_to_set (extract_IPSets_generic0 sel [])) = (\<lambda>a. case a of (base, len) \<Rightarrow> ipset_from_cidr base len) ` sel ` match_sel ` set []
[PROOF STEP]
qed(simp)