[STATEMENT]
lemma mult_apx_left_isotone_2:
  assumes "x \<sqsubseteq> y"
    shows "x * z \<sqsubseteq> y * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * z \<sqsubseteq> y * z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * z \<sqsubseteq> y * z
[PROOF STEP]
have "x * z \<le> y * z \<squnion> L * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * z \<le> y * z \<squnion> L * z
[PROOF STEP]
by (metis assms apx_def mult_left_isotone mult_right_dist_sup)
[PROOF STATE]
proof (state)
this:
x * z \<le> y * z \<squnion> L * z

goal (1 subgoal):
 1. x * z \<sqsubseteq> y * z
[PROOF STEP]
hence 1: "x * z \<le> y * z \<squnion> L"
[PROOF STATE]
proof (prove)
using this:
x * z \<le> y * z \<squnion> L * z

goal (1 subgoal):
 1. x * z \<le> y * z \<squnion> L
[PROOF STEP]
using n_L_below_L order_lesseq_imp semiring.add_left_mono
[PROOF STATE]
proof (prove)
using this:
x * z \<le> y * z \<squnion> L * z
L * ?x \<le> L
(\<forall>z\<ge>?x. ?y \<le> z) = (?y \<le> ?x)
?a \<le> ?b \<Longrightarrow> ?c \<squnion> ?a \<le> ?c \<squnion> ?b

goal (1 subgoal):
 1. x * z \<le> y * z \<squnion> L
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x * z \<le> y * z \<squnion> L

goal (1 subgoal):
 1. x * z \<sqsubseteq> y * z
[PROOF STEP]
have "y * z \<le> x * z \<squnion> n(x) * top * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y * z \<le> x * z \<squnion> n x * top * z
[PROOF STEP]
by (metis assms apx_def mult_left_isotone mult_right_dist_sup)
[PROOF STATE]
proof (state)
this:
y * z \<le> x * z \<squnion> n x * top * z

goal (1 subgoal):
 1. x * z \<sqsubseteq> y * z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
y * z \<le> x * z \<squnion> n x * top * z

goal (1 subgoal):
 1. x * z \<sqsubseteq> y * z
[PROOF STEP]
have "... \<le> x * z \<squnion> n(x * z) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * z \<squnion> n x * top * z \<le> x * z \<squnion> n (x * z) * top
[PROOF STEP]
by (simp add: n_top_split)
[PROOF STATE]
proof (state)
this:
x * z \<squnion> n x * top * z \<le> x * z \<squnion> n (x * z) * top

goal (1 subgoal):
 1. x * z \<sqsubseteq> y * z
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
y * z \<le> x * z \<squnion> n (x * z) * top
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y * z \<le> x * z \<squnion> n (x * z) * top

goal (1 subgoal):
 1. x * z \<sqsubseteq> y * z
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
y * z \<le> x * z \<squnion> n (x * z) * top
x * z \<le> y * z \<squnion> L

goal (1 subgoal):
 1. x * z \<sqsubseteq> y * z
[PROOF STEP]
by (simp add: apx_def)
[PROOF STATE]
proof (state)
this:
x * z \<sqsubseteq> y * z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_apx_right_isotone_2:
  assumes "x \<sqsubseteq> y"
    shows "z * x \<sqsubseteq> z * y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
have "z * x \<le> z * y \<squnion> z * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z * x \<le> z * y \<squnion> z * L
[PROOF STEP]
by (metis assms apx_def mult_left_dist_sup mult_right_isotone)
[PROOF STATE]
proof (state)
this:
z * x \<le> z * y \<squnion> z * L

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
z * x \<le> z * y \<squnion> z * L

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
have "... \<le> z * y \<squnion> z * bot \<squnion> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z * y \<squnion> z * L \<le> z * y \<squnion> z * bot \<squnion> L
[PROOF STEP]
using n_L_split_L semiring.add_left_mono sup_assoc
[PROOF STATE]
proof (prove)
using this:
?x * L \<le> ?x * bot \<squnion> L
?a \<le> ?b \<Longrightarrow> ?c \<squnion> ?a \<le> ?c \<squnion> ?b
?x \<squnion> ?y \<squnion> ?z = ?x \<squnion> (?y \<squnion> ?z)

goal (1 subgoal):
 1. z * y \<squnion> z * L \<le> z * y \<squnion> z * bot \<squnion> L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z * y \<squnion> z * L \<le> z * y \<squnion> z * bot \<squnion> L

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
z * x \<le> z * y \<squnion> z * bot \<squnion> L
[PROOF STEP]
have 1: "z * x \<le> z * y \<squnion> L"
[PROOF STATE]
proof (prove)
using this:
z * x \<le> z * y \<squnion> z * bot \<squnion> L

goal (1 subgoal):
 1. z * x \<le> z * y \<squnion> L
[PROOF STEP]
using mult_right_isotone sup.absorb_iff1
[PROOF STATE]
proof (prove)
using this:
z * x \<le> z * y \<squnion> z * bot \<squnion> L
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y
(?b \<le> ?a) = (?a \<squnion> ?b = ?a)

goal (1 subgoal):
 1. z * x \<le> z * y \<squnion> L
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
z * x \<le> z * y \<squnion> L

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
have "z * y \<le> z * (x \<squnion> n(x) * top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z * y \<le> z * (x \<squnion> n x * top)
[PROOF STEP]
using assms apx_def mult_right_isotone
[PROOF STATE]
proof (prove)
using this:
x \<sqsubseteq> y
(?x \<sqsubseteq> ?y) = (?x \<le> ?y \<squnion> L \<and> ?y \<le> ?x \<squnion> n ?x * top)
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y

goal (1 subgoal):
 1. z * y \<le> z * (x \<squnion> n x * top)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z * y \<le> z * (x \<squnion> n x * top)

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
z * y \<le> z * (x \<squnion> n x * top)

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
have "... = z * x \<squnion> z * n(x) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z * (x \<squnion> n x * top) = z * x \<squnion> z * n x * top
[PROOF STEP]
by (simp add: mult_left_dist_sup mult_assoc)
[PROOF STATE]
proof (state)
this:
z * (x \<squnion> n x * top) = z * x \<squnion> z * n x * top

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
z * (x \<squnion> n x * top) = z * x \<squnion> z * n x * top

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
have "... \<le> z * x \<squnion> n(z * x) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z * x \<squnion> z * n x * top \<le> z * x \<squnion> n (z * x) * top
[PROOF STEP]
by (simp add: n_split_top)
[PROOF STATE]
proof (state)
this:
z * x \<squnion> z * n x * top \<le> z * x \<squnion> n (z * x) * top

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
z * y \<le> z * x \<squnion> n (z * x) * top
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
z * y \<le> z * x \<squnion> n (z * x) * top

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
z * y \<le> z * x \<squnion> n (z * x) * top
z * x \<le> z * y \<squnion> L

goal (1 subgoal):
 1. z * x \<sqsubseteq> z * y
[PROOF STEP]
by (simp add: apx_def)
[PROOF STATE]
proof (state)
this:
z * x \<sqsubseteq> z * y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_int_t_exists:
  assumes "is_int_t t"
  shows "t = T_i32 \<or> t = T_i64"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = T_i32 \<or> t = T_i64
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_int_t t

goal (1 subgoal):
 1. t = T_i32 \<or> t = T_i64
[PROOF STEP]
by (cases t) (auto simp add: is_int_t_def)


[STATEMENT]
lemma is_float_t_exists:
  assumes "is_float_t t"
  shows "t = T_f32 \<or> t = T_f64"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = T_f32 \<or> t = T_f64
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_float_t t

goal (1 subgoal):
 1. t = T_f32 \<or> t = T_f64
[PROOF STEP]
by (cases t) (auto simp add: is_float_t_def)


[STATEMENT]
lemma int_float_disjoint: "is_int_t t = -(is_float_t t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_int_t t = - is_float_t t
[PROOF STEP]
by simp (metis is_float_t_def is_int_t_def t.exhaust t.simps(13-16))


[STATEMENT]
lemma stab_unfold:
  assumes "stab s i j = Some cl"
  shows "\<exists>k. inst.tab ((inst s)!i) = Some k \<and> length ((tab s)!k) > j \<and>((tab s)!k)!j = Some cl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. inst.tab (inst s ! i) = Some k \<and> j < length (s.tab s ! k) \<and> s.tab s ! k ! j = Some cl
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k. inst.tab (inst s ! i) = Some k \<and> j < length (s.tab s ! k) \<and> s.tab s ! k ! j = Some cl
[PROOF STEP]
obtain k where have_k:"(inst.tab ((inst s)!i)) = Some k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. inst.tab (inst s ! i) = Some k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
stab s i j = Some cl

goal (1 subgoal):
 1. (\<And>k. inst.tab (inst s ! i) = Some k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding stab_def
[PROOF STATE]
proof (prove)
using this:
(case inst.tab (inst s ! i) of None \<Rightarrow> None | Some k \<Rightarrow> stab_s s k j) = Some cl

goal (1 subgoal):
 1. (\<And>k. inst.tab (inst s ! i) = Some k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
inst.tab (inst s ! i) = Some k

goal (1 subgoal):
 1. \<exists>k. inst.tab (inst s ! i) = Some k \<and> j < length (s.tab s ! k) \<and> s.tab s ! k ! j = Some cl
[PROOF STEP]
hence s_o:"stab s i j = stab_s s k j"
[PROOF STATE]
proof (prove)
using this:
inst.tab (inst s ! i) = Some k

goal (1 subgoal):
 1. stab s i j = stab_s s k j
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
inst.tab (inst s ! i) = Some k
stab s i j = Some cl

goal (1 subgoal):
 1. stab s i j = stab_s s k j
[PROOF STEP]
unfolding stab_def
[PROOF STATE]
proof (prove)
using this:
inst.tab (inst s ! i) = Some k
(case inst.tab (inst s ! i) of None \<Rightarrow> None | Some k \<Rightarrow> stab_s s k j) = Some cl

goal (1 subgoal):
 1. (case inst.tab (inst s ! i) of None \<Rightarrow> None | Some k \<Rightarrow> stab_s s k j) = stab_s s k j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stab s i j = stab_s s k j

goal (1 subgoal):
 1. \<exists>k. inst.tab (inst s ! i) = Some k \<and> j < length (s.tab s ! k) \<and> s.tab s ! k ! j = Some cl
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
stab s i j = stab_s s k j
[PROOF STEP]
obtain stabinst where stabinst_def:"stabinst = ((tab s)!k)"
[PROOF STATE]
proof (prove)
using this:
stab s i j = stab_s s k j

goal (1 subgoal):
 1. (\<And>stabinst. stabinst = s.tab s ! k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
stabinst = s.tab s ! k

goal (1 subgoal):
 1. \<exists>k. inst.tab (inst s ! i) = Some k \<and> j < length (s.tab s ! k) \<and> s.tab s ! k ! j = Some cl
[PROOF STEP]
hence "stab_s s k j = (stabinst!j) \<and> (length stabinst > j)"
[PROOF STATE]
proof (prove)
using this:
stabinst = s.tab s ! k

goal (1 subgoal):
 1. stab_s s k j = stabinst ! j \<and> j < length stabinst
[PROOF STEP]
using assms s_o
[PROOF STATE]
proof (prove)
using this:
stabinst = s.tab s ! k
stab s i j = Some cl
stab s i j = stab_s s k j

goal (1 subgoal):
 1. stab_s s k j = stabinst ! j \<and> j < length stabinst
[PROOF STEP]
unfolding stab_s_def
[PROOF STATE]
proof (prove)
using this:
stabinst = s.tab s ! k
stab s i j = Some cl
stab s i j = (let stabinst = s.tab s ! k in if j < length stabinst then stabinst ! j else None)

goal (1 subgoal):
 1. (let stabinst = s.tab s ! k in if j < length stabinst then stabinst ! j else None) = stabinst ! j \<and> j < length stabinst
[PROOF STEP]
by (cases "(length stabinst > j)", auto)
[PROOF STATE]
proof (state)
this:
stab_s s k j = stabinst ! j \<and> j < length stabinst

goal (1 subgoal):
 1. \<exists>k. inst.tab (inst s ! i) = Some k \<and> j < length (s.tab s ! k) \<and> s.tab s ! k ! j = Some cl
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
stab_s s k j = stabinst ! j \<and> j < length stabinst

goal (1 subgoal):
 1. \<exists>k. inst.tab (inst s ! i) = Some k \<and> j < length (s.tab s ! k) \<and> s.tab s ! k ! j = Some cl
[PROOF STEP]
using have_k stabinst_def assms s_o
[PROOF STATE]
proof (prove)
using this:
stab_s s k j = stabinst ! j \<and> j < length stabinst
inst.tab (inst s ! i) = Some k
stabinst = s.tab s ! k
stab s i j = Some cl
stab s i j = stab_s s k j

goal (1 subgoal):
 1. \<exists>k. inst.tab (inst s ! i) = Some k \<and> j < length (s.tab s ! k) \<and> s.tab s ! k ! j = Some cl
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k. inst.tab (inst s ! i) = Some k \<and> j < length (s.tab s ! k) \<and> s.tab s ! k ! j = Some cl

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_basic: "inj Basic"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj Basic
[PROOF STEP]
by (meson e.inject(1) injI)


[STATEMENT]
lemma inj_basic_econst: "inj (\<lambda>v. $C v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (\<lambda>v. $C v)
[PROOF STEP]
by (meson b_e.inject(16) e.inject(1) injI)


[STATEMENT]
lemma to_e_list_1:"[$ a] = $* [a]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [$a] = $* [a]
[PROOF STEP]
by simp


[STATEMENT]
lemma to_e_list_2:"[$ a, $ b] = $* [a, b]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [$a, $b] = $* [a, b]
[PROOF STEP]
by simp


[STATEMENT]
lemma to_e_list_3:"[$ a, $ b, $ c] = $* [a, b, c]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [$a, $b, $c] = $* [a, b, c]
[PROOF STEP]
by simp


[STATEMENT]
lemma v_exists_b_e:"\<exists>ves. ($$*vs) = ($*ves)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ves. $$* vs = $* ves
[PROOF STEP]
proof (induction vs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>ves. $$* [] = $* ves
 2. \<And>a vs. \<exists>ves. $$* vs = $* ves \<Longrightarrow> \<exists>ves. $$* a # vs = $* ves
[PROOF STEP]
case (Cons a vs)
[PROOF STATE]
proof (state)
this:
\<exists>ves. $$* vs = $* ves

goal (2 subgoals):
 1. \<exists>ves. $$* [] = $* ves
 2. \<And>a vs. \<exists>ves. $$* vs = $* ves \<Longrightarrow> \<exists>ves. $$* a # vs = $* ves
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>ves. $$* vs = $* ves

goal (1 subgoal):
 1. \<exists>ves. $$* a # vs = $* ves
[PROOF STEP]
by (metis list.simps(9))
[PROOF STATE]
proof (state)
this:
\<exists>ves. $$* a # vs = $* ves

goal (1 subgoal):
 1. \<exists>ves. $$* [] = $* ves
[PROOF STEP]
qed auto


[STATEMENT]
lemma Lfilled_exact_imp_Lfilled:
  assumes "Lfilled_exact n lholed es LI"
  shows "Lfilled n lholed es LI"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Lfilled n lholed es LI
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Lfilled_exact n lholed es LI

goal (1 subgoal):
 1. Lfilled n lholed es LI
[PROOF STEP]
proof (induction rule: Lfilled_exact.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>lholed es. lholed = LBase [] [] \<Longrightarrow> Lfilled 0 lholed es es
 2. \<And>vs lholed n es' l es'' k es lfilledk. \<lbrakk>const_list vs; lholed = LRec vs n es' l es''; Lfilled_exact k l es lfilledk; Lfilled k l es lfilledk\<rbrakk> \<Longrightarrow> Lfilled (k + 1) lholed es (vs @ [Label n es' lfilledk] @ es'')
[PROOF STEP]
case (L0 lholed es)
[PROOF STATE]
proof (state)
this:
lholed = LBase [] []

goal (2 subgoals):
 1. \<And>lholed es. lholed = LBase [] [] \<Longrightarrow> Lfilled 0 lholed es es
 2. \<And>vs lholed n es' l es'' k es lfilledk. \<lbrakk>const_list vs; lholed = LRec vs n es' l es''; Lfilled_exact k l es lfilledk; Lfilled k l es lfilledk\<rbrakk> \<Longrightarrow> Lfilled (k + 1) lholed es (vs @ [Label n es' lfilledk] @ es'')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
lholed = LBase [] []

goal (1 subgoal):
 1. Lfilled 0 lholed es es
[PROOF STEP]
using const_list_def Lfilled.intros(1)
[PROOF STATE]
proof (prove)
using this:
lholed = LBase [] []
const_list ?xs = list_all is_const ?xs
\<lbrakk>const_list ?vs; ?lholed = LBase ?vs ?es'\<rbrakk> \<Longrightarrow> Lfilled 0 ?lholed ?es (?vs @ ?es @ ?es')

goal (1 subgoal):
 1. Lfilled 0 lholed es es
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Lfilled 0 lholed es es

goal (1 subgoal):
 1. \<And>vs lholed n es' l es'' k es lfilledk. \<lbrakk>const_list vs; lholed = LRec vs n es' l es''; Lfilled_exact k l es lfilledk; Lfilled k l es lfilledk\<rbrakk> \<Longrightarrow> Lfilled (k + 1) lholed es (vs @ [Label n es' lfilledk] @ es'')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>vs lholed n es' l es'' k es lfilledk. \<lbrakk>const_list vs; lholed = LRec vs n es' l es''; Lfilled_exact k l es lfilledk; Lfilled k l es lfilledk\<rbrakk> \<Longrightarrow> Lfilled (k + 1) lholed es (vs @ [Label n es' lfilledk] @ es'')
[PROOF STEP]
case (LN vs lholed n es' l es'' k es lfilledk)
[PROOF STATE]
proof (state)
this:
const_list vs
lholed = LRec vs n es' l es''
Lfilled_exact k l es lfilledk
Lfilled k l es lfilledk

goal (1 subgoal):
 1. \<And>vs lholed n es' l es'' k es lfilledk. \<lbrakk>const_list vs; lholed = LRec vs n es' l es''; Lfilled_exact k l es lfilledk; Lfilled k l es lfilledk\<rbrakk> \<Longrightarrow> Lfilled (k + 1) lholed es (vs @ [Label n es' lfilledk] @ es'')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
const_list vs
lholed = LRec vs n es' l es''
Lfilled_exact k l es lfilledk
Lfilled k l es lfilledk

goal (1 subgoal):
 1. Lfilled (k + 1) lholed es (vs @ [Label n es' lfilledk] @ es'')
[PROOF STEP]
using Lfilled.intros(2)
[PROOF STATE]
proof (prove)
using this:
const_list vs
lholed = LRec vs n es' l es''
Lfilled_exact k l es lfilledk
Lfilled k l es lfilledk
\<lbrakk>const_list ?vs; ?lholed = LRec ?vs ?n ?es' ?l ?es''; Lfilled ?k ?l ?es ?lfilledk\<rbrakk> \<Longrightarrow> Lfilled (?k + 1) ?lholed ?es (?vs @ [Label ?n ?es' ?lfilledk] @ ?es'')

goal (1 subgoal):
 1. Lfilled (k + 1) lholed es (vs @ [Label n es' lfilledk] @ es'')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Lfilled (k + 1) lholed es (vs @ [Label n es' lfilledk] @ es'')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Lfilled_exact_app_imp_exists_Lfilled:
  assumes "const_list ves"
          "Lfilled_exact n lholed (ves@es) LI"
  shows "\<exists>lholed'. Lfilled n lholed' es LI"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>lholed'. Lfilled n lholed' es LI
[PROOF STEP]
using assms(2,1)
[PROOF STATE]
proof (prove)
using this:
Lfilled_exact n lholed (ves @ es) LI
const_list ves

goal (1 subgoal):
 1. \<exists>lholed'. Lfilled n lholed' es LI
[PROOF STEP]
proof (induction "(ves@es)" LI rule: Lfilled_exact.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>lholed. \<lbrakk>lholed = LBase [] []; const_list ves\<rbrakk> \<Longrightarrow> \<exists>lholed'. Lfilled 0 lholed' es (ves @ es)
 2. \<And>vs lholed n es' l es'' k lfilledk. \<lbrakk>const_list vs; lholed = LRec vs n es' l es''; Lfilled_exact k l (ves @ es) lfilledk; const_list ves \<Longrightarrow> \<exists>lholed'. Lfilled k lholed' es lfilledk; const_list ves\<rbrakk> \<Longrightarrow> \<exists>lholed'. Lfilled (k + 1) lholed' es (vs @ [Label n es' lfilledk] @ es'')
[PROOF STEP]
case (L0 lholed)
[PROOF STATE]
proof (state)
this:
lholed = LBase [] []
const_list ves

goal (2 subgoals):
 1. \<And>lholed. \<lbrakk>lholed = LBase [] []; const_list ves\<rbrakk> \<Longrightarrow> \<exists>lholed'. Lfilled 0 lholed' es (ves @ es)
 2. \<And>vs lholed n es' l es'' k lfilledk. \<lbrakk>const_list vs; lholed = LRec vs n es' l es''; Lfilled_exact k l (ves @ es) lfilledk; const_list ves \<Longrightarrow> \<exists>lholed'. Lfilled k lholed' es lfilledk; const_list ves\<rbrakk> \<Longrightarrow> \<exists>lholed'. Lfilled (k + 1) lholed' es (vs @ [Label n es' lfilledk] @ es'')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>lholed'. Lfilled 0 lholed' es (ves @ es)
[PROOF STEP]
using Lfilled.intros(1)[OF L0(2), of _ "[]"]
[PROOF STATE]
proof (prove)
using this:
?lholed = LBase ves [] \<Longrightarrow> Lfilled 0 ?lholed ?es (ves @ ?es @ [])

goal (1 subgoal):
 1. \<exists>lholed'. Lfilled 0 lholed' es (ves @ es)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>lholed'. Lfilled 0 lholed' es (ves @ es)

goal (1 subgoal):
 1. \<And>vs lholed n es' l es'' k lfilledk. \<lbrakk>const_list vs; lholed = LRec vs n es' l es''; Lfilled_exact k l (ves @ es) lfilledk; const_list ves \<Longrightarrow> \<exists>lholed'. Lfilled k lholed' es lfilledk; const_list ves\<rbrakk> \<Longrightarrow> \<exists>lholed'. Lfilled (k + 1) lholed' es (vs @ [Label n es' lfilledk] @ es'')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>vs lholed n es' l es'' k lfilledk. \<lbrakk>const_list vs; lholed = LRec vs n es' l es''; Lfilled_exact k l (ves @ es) lfilledk; const_list ves \<Longrightarrow> \<exists>lholed'. Lfilled k lholed' es lfilledk; const_list ves\<rbrakk> \<Longrightarrow> \<exists>lholed'. Lfilled (k + 1) lholed' es (vs @ [Label n es' lfilledk] @ es'')
[PROOF STEP]
case (LN vs lholed n es' l es'' k lfilledk)
[PROOF STATE]
proof (state)
this:
const_list vs
lholed = LRec vs n es' l es''
Lfilled_exact k l (ves @ es) lfilledk
const_list ves \<Longrightarrow> \<exists>lholed'. Lfilled k lholed' es lfilledk
const_list ves

goal (1 subgoal):
 1. \<And>vs lholed n es' l es'' k lfilledk. \<lbrakk>const_list vs; lholed = LRec vs n es' l es''; Lfilled_exact k l (ves @ es) lfilledk; const_list ves \<Longrightarrow> \<exists>lholed'. Lfilled k lholed' es lfilledk; const_list ves\<rbrakk> \<Longrightarrow> \<exists>lholed'. Lfilled (k + 1) lholed' es (vs @ [Label n es' lfilledk] @ es'')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
const_list vs
lholed = LRec vs n es' l es''
Lfilled_exact k l (ves @ es) lfilledk
const_list ves \<Longrightarrow> \<exists>lholed'. Lfilled k lholed' es lfilledk
const_list ves

goal (1 subgoal):
 1. \<exists>lholed'. Lfilled (k + 1) lholed' es (vs @ [Label n es' lfilledk] @ es'')
[PROOF STEP]
using Lfilled.intros(2)
[PROOF STATE]
proof (prove)
using this:
const_list vs
lholed = LRec vs n es' l es''
Lfilled_exact k l (ves @ es) lfilledk
const_list ves \<Longrightarrow> \<exists>lholed'. Lfilled k lholed' es lfilledk
const_list ves
\<lbrakk>const_list ?vs; ?lholed = LRec ?vs ?n ?es' ?l ?es''; Lfilled ?k ?l ?es ?lfilledk\<rbrakk> \<Longrightarrow> Lfilled (?k + 1) ?lholed ?es (?vs @ [Label ?n ?es' ?lfilledk] @ ?es'')

goal (1 subgoal):
 1. \<exists>lholed'. Lfilled (k + 1) lholed' es (vs @ [Label n es' lfilledk] @ es'')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>lholed'. Lfilled (k + 1) lholed' es (vs @ [Label n es' lfilledk] @ es'')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Lfilled_imp_exists_Lfilled_exact:
  assumes "Lfilled n lholed es LI"
  shows "\<exists>lholed' ves es_c. const_list ves \<and> Lfilled_exact n lholed' (ves@es@es_c) LI"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>lholed' ves es_c. const_list ves \<and> Lfilled_exact n lholed' (ves @ es @ es_c) LI
[PROOF STEP]
using assms Lfilled_exact.intros
[PROOF STATE]
proof (prove)
using this:
Lfilled n lholed es LI
?lholed = LBase [] [] \<Longrightarrow> Lfilled_exact 0 ?lholed ?es ?es
\<lbrakk>const_list ?vs; ?lholed = LRec ?vs ?n ?es' ?l ?es''; Lfilled_exact ?k ?l ?es ?lfilledk\<rbrakk> \<Longrightarrow> Lfilled_exact (?k + 1) ?lholed ?es (?vs @ [Label ?n ?es' ?lfilledk] @ ?es'')

goal (1 subgoal):
 1. \<exists>lholed' ves es_c. const_list ves \<and> Lfilled_exact n lholed' (ves @ es @ es_c) LI
[PROOF STEP]
by (induction rule: Lfilled.induct) fastforce+


[STATEMENT]
lemma n_zeros_typeof:
  "n_zeros ts = vs \<Longrightarrow> (ts = map typeof vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n_zeros ts = vs \<Longrightarrow> ts = map typeof vs
[PROOF STEP]
proof (induction ts arbitrary: vs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>vs. n_zeros [] = vs \<Longrightarrow> [] = map typeof vs
 2. \<And>a ts vs. \<lbrakk>\<And>vs. n_zeros ts = vs \<Longrightarrow> ts = map typeof vs; n_zeros (a # ts) = vs\<rbrakk> \<Longrightarrow> a # ts = map typeof vs
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
n_zeros [] = vs

goal (2 subgoals):
 1. \<And>vs. n_zeros [] = vs \<Longrightarrow> [] = map typeof vs
 2. \<And>a ts vs. \<lbrakk>\<And>vs. n_zeros ts = vs \<Longrightarrow> ts = map typeof vs; n_zeros (a # ts) = vs\<rbrakk> \<Longrightarrow> a # ts = map typeof vs
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n_zeros [] = vs

goal (1 subgoal):
 1. [] = map typeof vs
[PROOF STEP]
unfolding n_zeros_def
[PROOF STATE]
proof (prove)
using this:
map bitzero [] = vs

goal (1 subgoal):
 1. [] = map typeof vs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[] = map typeof vs

goal (1 subgoal):
 1. \<And>a ts vs. \<lbrakk>\<And>vs. n_zeros ts = vs \<Longrightarrow> ts = map typeof vs; n_zeros (a # ts) = vs\<rbrakk> \<Longrightarrow> a # ts = map typeof vs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ts vs. \<lbrakk>\<And>vs. n_zeros ts = vs \<Longrightarrow> ts = map typeof vs; n_zeros (a # ts) = vs\<rbrakk> \<Longrightarrow> a # ts = map typeof vs
[PROOF STEP]
case (Cons t ts)
[PROOF STATE]
proof (state)
this:
n_zeros ts = ?vs \<Longrightarrow> ts = map typeof ?vs
n_zeros (t # ts) = vs

goal (1 subgoal):
 1. \<And>a ts vs. \<lbrakk>\<And>vs. n_zeros ts = vs \<Longrightarrow> ts = map typeof vs; n_zeros (a # ts) = vs\<rbrakk> \<Longrightarrow> a # ts = map typeof vs
[PROOF STEP]
obtain vs' where "n_zeros ts = vs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>vs'. n_zeros ts = vs' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using n_zeros_def
[PROOF STATE]
proof (prove)
using this:
n_zeros ?ts = map bitzero ?ts

goal (1 subgoal):
 1. (\<And>vs'. n_zeros ts = vs' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n_zeros ts = vs'

goal (1 subgoal):
 1. \<And>a ts vs. \<lbrakk>\<And>vs. n_zeros ts = vs \<Longrightarrow> ts = map typeof vs; n_zeros (a # ts) = vs\<rbrakk> \<Longrightarrow> a # ts = map typeof vs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n_zeros ts = vs'

goal (1 subgoal):
 1. \<And>a ts vs. \<lbrakk>\<And>vs. n_zeros ts = vs \<Longrightarrow> ts = map typeof vs; n_zeros (a # ts) = vs\<rbrakk> \<Longrightarrow> a # ts = map typeof vs
[PROOF STEP]
have "typeof (bitzero t) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. typeof (bitzero t) = t
[PROOF STEP]
unfolding typeof_def bitzero_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case case t of T_i32 \<Rightarrow> ConstInt32 0 | T_i64 \<Rightarrow> ConstInt64 0 | T_f32 \<Rightarrow> ConstFloat32 0 | T_f64 \<Rightarrow> ConstFloat64 0 of ConstInt32 x \<Rightarrow> T_i32 | ConstInt64 x \<Rightarrow> T_i64 | ConstFloat32 x \<Rightarrow> T_f32 | ConstFloat64 x \<Rightarrow> T_f64) = t
[PROOF STEP]
by (cases t, simp_all)
[PROOF STATE]
proof (state)
this:
typeof (bitzero t) = t

goal (1 subgoal):
 1. \<And>a ts vs. \<lbrakk>\<And>vs. n_zeros ts = vs \<Longrightarrow> ts = map typeof vs; n_zeros (a # ts) = vs\<rbrakk> \<Longrightarrow> a # ts = map typeof vs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n_zeros ts = vs'
typeof (bitzero t) = t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n_zeros ts = vs'
typeof (bitzero t) = t

goal (1 subgoal):
 1. t # ts = map typeof vs
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
n_zeros ts = vs'
typeof (bitzero t) = t
n_zeros ts = ?vs \<Longrightarrow> ts = map typeof ?vs
n_zeros (t # ts) = vs

goal (1 subgoal):
 1. t # ts = map typeof vs
[PROOF STEP]
unfolding n_zeros_def
[PROOF STATE]
proof (prove)
using this:
map bitzero ts = vs'
typeof (bitzero t) = t
map bitzero ts = ?vs \<Longrightarrow> ts = map typeof ?vs
map bitzero (t # ts) = vs

goal (1 subgoal):
 1. t # ts = map typeof vs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t # ts = map typeof vs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Iface_single:
    "matches (\<beta>, \<alpha>) (Match (IIface X)) a p \<longleftrightarrow> match_iface X (p_iiface p)"
    "matches (\<beta>, \<alpha>) (Match (OIface X)) a p \<longleftrightarrow> match_iface X (p_oiface p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (Match (IIface X)) a p = match_iface X (p_iiface p) &&& matches (\<beta>, \<alpha>) (Match (OIface X)) a p = match_iface X (p_oiface p)
[PROOF STEP]
by(simp_all add: IIface OIface match_raw_ternary bool_to_ternary_simps
               split: ternaryvalue.split)


[STATEMENT]
lemma Iface_single_not:
    "matches (\<beta>, \<alpha>) (MatchNot (Match (IIface X))) a p \<longleftrightarrow> \<not> match_iface X (p_iiface p)"
    "matches (\<beta>, \<alpha>) (MatchNot (Match (OIface X))) a p \<longleftrightarrow> \<not> match_iface X (p_oiface p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (MatchNot (Match (IIface X))) a p = (\<not> match_iface X (p_iiface p)) &&& matches (\<beta>, \<alpha>) (MatchNot (Match (OIface X))) a p = (\<not> match_iface X (p_oiface p))
[PROOF STEP]
by(simp_all add: IIface OIface matches_case_ternaryvalue_tuple bool_to_ternary_simps
          split: ternaryvalue.split)


[STATEMENT]
lemma Prot_single:
    "matches (\<beta>, \<alpha>) (Match (Prot X)) a p \<longleftrightarrow> match_proto X (p_proto p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (Match (Prot X)) a p = match_proto X (p_proto p)
[PROOF STEP]
by(simp add: Prot match_raw_ternary bool_to_ternary_simps split: ternaryvalue.split)


[STATEMENT]
lemma Prot_single_not:
    "matches (\<beta>, \<alpha>) (MatchNot (Match (Prot X))) a p \<longleftrightarrow> \<not> match_proto X (p_proto p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (MatchNot (Match (Prot X))) a p = (\<not> match_proto X (p_proto p))
[PROOF STEP]
by(simp add: Prot matches_case_ternaryvalue_tuple bool_to_ternary_simps split: ternaryvalue.split)


[STATEMENT]
lemma Ports_single:
    "matches (\<beta>, \<alpha>) (Match (Src_Ports (L4Ports proto ps))) a p \<longleftrightarrow> proto = p_proto p \<and> p_sport p \<in> ports_to_set ps"
    "matches (\<beta>, \<alpha>) (Match (Dst_Ports (L4Ports proto ps))) a p \<longleftrightarrow> proto = p_proto p \<and> p_dport p \<in> ports_to_set ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (Match (Src_Ports (L4Ports proto ps))) a p = (proto = p_proto p \<and> p_sport p \<in> ports_to_set ps) &&& matches (\<beta>, \<alpha>) (Match (Dst_Ports (L4Ports proto ps))) a p = (proto = p_proto p \<and> p_dport p \<in> ports_to_set ps)
[PROOF STEP]
by(simp_all add: Src_Ports Dst_Ports match_raw_ternary bool_to_ternary_simps
               split: ternaryvalue.split)


[STATEMENT]
lemma Ports_single_not:
    "matches (\<beta>, \<alpha>) (MatchNot (Match (Src_Ports (L4Ports proto ps)))) a p \<longleftrightarrow> proto \<noteq> p_proto p \<or> p_sport p \<notin> ports_to_set ps"
    "matches (\<beta>, \<alpha>) (MatchNot (Match (Dst_Ports (L4Ports proto ps)))) a p \<longleftrightarrow> proto \<noteq> p_proto p \<or> p_dport p \<notin> ports_to_set ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (MatchNot (Match (Src_Ports (L4Ports proto ps)))) a p = (proto \<noteq> p_proto p \<or> p_sport p \<notin> ports_to_set ps) &&& matches (\<beta>, \<alpha>) (MatchNot (Match (Dst_Ports (L4Ports proto ps)))) a p = (proto \<noteq> p_proto p \<or> p_dport p \<notin> ports_to_set ps)
[PROOF STEP]
by(simp_all add: Src_Ports Dst_Ports matches_case_ternaryvalue_tuple bool_to_ternary_simps
               split: ternaryvalue.split)


[STATEMENT]
lemma Ports_single_rewrite_Prot:
    "matches (\<beta>, \<alpha>) (Match (Src_Ports (L4Ports proto ps))) a p \<longleftrightarrow>
      matches (\<beta>, \<alpha>) (Match (Prot (Proto proto))) a p \<and> p_sport p \<in> ports_to_set ps"
    "matches (\<beta>, \<alpha>) (MatchNot (Match (Src_Ports (L4Ports proto ps)))) a p \<longleftrightarrow>
      matches (\<beta>, \<alpha>) (MatchNot (Match (Prot (Proto proto)))) a p \<or> p_sport p \<notin> ports_to_set ps"
    "matches (\<beta>, \<alpha>) (Match (Dst_Ports (L4Ports proto ps))) a p \<longleftrightarrow>
      matches (\<beta>, \<alpha>) (Match (Prot (Proto proto))) a p \<and> p_dport p \<in> ports_to_set ps"
    "matches (\<beta>, \<alpha>) (MatchNot (Match (Dst_Ports (L4Ports proto ps)))) a p \<longleftrightarrow>
      matches (\<beta>, \<alpha>) (MatchNot (Match (Prot (Proto proto)))) a p \<or> p_dport p \<notin> ports_to_set ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (matches (\<beta>, \<alpha>) (Match (Src_Ports (L4Ports proto ps))) a p = (matches (\<beta>, \<alpha>) (Match (Prot (Proto proto))) a p \<and> p_sport p \<in> ports_to_set ps) &&& matches (\<beta>, \<alpha>) (MatchNot (Match (Src_Ports (L4Ports proto ps)))) a p = (matches (\<beta>, \<alpha>) (MatchNot (Match (Prot (Proto proto)))) a p \<or> p_sport p \<notin> ports_to_set ps)) &&& matches (\<beta>, \<alpha>) (Match (Dst_Ports (L4Ports proto ps))) a p = (matches (\<beta>, \<alpha>) (Match (Prot (Proto proto))) a p \<and> p_dport p \<in> ports_to_set ps) &&& matches (\<beta>, \<alpha>) (MatchNot (Match (Dst_Ports (L4Ports proto ps)))) a p = (matches (\<beta>, \<alpha>) (MatchNot (Match (Prot (Proto proto)))) a p \<or> p_dport p \<notin> ports_to_set ps)
[PROOF STEP]
by(auto simp add: Ports_single_not Ports_single Prot_single_not Prot_single)


[STATEMENT]
lemma multiports_disjuction:
        "(\<exists>rg\<in>set spts. matches (\<beta>, \<alpha>) (Match (Src_Ports (L4Ports proto [rg]))) a p) \<longleftrightarrow> matches (\<beta>, \<alpha>) (Match (Src_Ports (L4Ports proto spts))) a p"
        "(\<exists>rg\<in>set dpts. matches (\<beta>, \<alpha>) (Match (Dst_Ports (L4Ports proto [rg]))) a p) \<longleftrightarrow> matches (\<beta>, \<alpha>) (Match (Dst_Ports (L4Ports proto dpts))) a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>rg\<in>set spts. matches (\<beta>, \<alpha>) (Match (Src_Ports (L4Ports proto [rg]))) a p) = matches (\<beta>, \<alpha>) (Match (Src_Ports (L4Ports proto spts))) a p &&& (\<exists>rg\<in>set dpts. matches (\<beta>, \<alpha>) (Match (Dst_Ports (L4Ports proto [rg]))) a p) = matches (\<beta>, \<alpha>) (Match (Dst_Ports (L4Ports proto dpts))) a p
[PROOF STEP]
by(auto simp add: Src_Ports Dst_Ports match_raw_ternary bool_to_ternary_simps ports_to_set
                   split: ternaryvalue.split)


[STATEMENT]
lemma MultiportPorts_single_rewrite:
    "matches (\<beta>, \<alpha>) (Match (MultiportPorts ports)) a p \<longleftrightarrow>
      matches (\<beta>, \<alpha>) (Match (Src_Ports ports)) a p \<or> matches (\<beta>, \<alpha>) (Match (Dst_Ports ports)) a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (Match (MultiportPorts ports)) a p = (matches (\<beta>, \<alpha>) (Match (Src_Ports ports)) a p \<or> matches (\<beta>, \<alpha>) (Match (Dst_Ports ports)) a p)
[PROOF STEP]
apply(cases ports)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. ports = L4Ports x1 x2 \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (MultiportPorts ports)) a p = (matches (\<beta>, \<alpha>) (Match (Src_Ports ports)) a p \<or> matches (\<beta>, \<alpha>) (Match (Dst_Ports ports)) a p)
[PROOF STEP]
apply(simp add: Ports_single)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. ports = L4Ports x1 x2 \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (MultiportPorts (L4Ports x1 x2))) a p = (x1 = p_proto p \<and> p_sport p \<in> ports_to_set x2 \<or> x1 = p_proto p \<and> p_dport p \<in> ports_to_set x2)
[PROOF STEP]
by(simp add: MultiportsPorts match_raw_ternary bool_to_ternary_simps
            split: ternaryvalue.split)


[STATEMENT]
lemma MultiportPorts_single_rewrite_MatchOr:
    "matches (\<beta>, \<alpha>) (Match (MultiportPorts ports)) a p \<longleftrightarrow>
      matches (\<beta>, \<alpha>) (MatchOr (Match (Src_Ports ports)) (Match (Dst_Ports ports))) a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (Match (MultiportPorts ports)) a p = matches (\<beta>, \<alpha>) (MatchOr (Match (Src_Ports ports)) (Match (Dst_Ports ports))) a p
[PROOF STEP]
apply(cases ports)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. ports = L4Ports x1 x2 \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (MultiportPorts ports)) a p = matches (\<beta>, \<alpha>) (MatchOr (Match (Src_Ports ports)) (Match (Dst_Ports ports))) a p
[PROOF STEP]
by(simp add: MatchOr MultiportPorts_single_rewrite)


[STATEMENT]
lemma MultiportPorts_single_not_rewrite_MatchAnd:
    "matches (\<beta>, \<alpha>) (MatchNot (Match (MultiportPorts ports))) a p \<longleftrightarrow>
      matches (\<beta>, \<alpha>) (MatchAnd (MatchNot (Match (Src_Ports ports))) (MatchNot (Match (Dst_Ports ports)))) a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (MatchNot (Match (MultiportPorts ports))) a p = matches (\<beta>, \<alpha>) (MatchAnd (MatchNot (Match (Src_Ports ports))) (MatchNot (Match (Dst_Ports ports)))) a p
[PROOF STEP]
apply(cases ports)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. ports = L4Ports x1 x2 \<Longrightarrow> matches (\<beta>, \<alpha>) (MatchNot (Match (MultiportPorts ports))) a p = matches (\<beta>, \<alpha>) (MatchAnd (MatchNot (Match (Src_Ports ports))) (MatchNot (Match (Dst_Ports ports)))) a p
[PROOF STEP]
apply(simp add: Ports_single_not bunch_of_lemmata_about_matches)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. ports = L4Ports x1 x2 \<Longrightarrow> matches (\<beta>, \<alpha>) (MatchNot (Match (MultiportPorts (L4Ports x1 x2)))) a p = ((x1 = p_proto p \<longrightarrow> p_sport p \<notin> ports_to_set x2) \<and> (x1 = p_proto p \<longrightarrow> p_dport p \<notin> ports_to_set x2))
[PROOF STEP]
by(simp add: MultiportsPorts matches_case_ternaryvalue_tuple bool_to_ternary_simps
            split: ternaryvalue.split)


[STATEMENT]
lemma MultiportPorts_single_not_rewrite:
    "matches (\<beta>, \<alpha>) (MatchNot (Match (MultiportPorts ports))) a p \<longleftrightarrow>
      \<not> matches (\<beta>, \<alpha>) (Match (Src_Ports ports)) a p \<and> \<not> matches (\<beta>, \<alpha>) (Match (Dst_Ports ports)) a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (MatchNot (Match (MultiportPorts ports))) a p = (\<not> matches (\<beta>, \<alpha>) (Match (Src_Ports ports)) a p \<and> \<not> matches (\<beta>, \<alpha>) (Match (Dst_Ports ports)) a p)
[PROOF STEP]
apply(cases ports)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. ports = L4Ports x1 x2 \<Longrightarrow> matches (\<beta>, \<alpha>) (MatchNot (Match (MultiportPorts ports))) a p = (\<not> matches (\<beta>, \<alpha>) (Match (Src_Ports ports)) a p \<and> \<not> matches (\<beta>, \<alpha>) (Match (Dst_Ports ports)) a p)
[PROOF STEP]
by(simp add: MultiportPorts_single_not_rewrite_MatchAnd bunch_of_lemmata_about_matches
                 Ports_single_not Ports_single)


[STATEMENT]
lemma Extra_single:
    "matches (\<beta>, \<alpha>) (Match (Extra str)) a p \<longleftrightarrow> \<alpha> a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (Match (Extra str)) a p = \<alpha> a p
[PROOF STEP]
by(simp add: Extra match_raw_ternary)


[STATEMENT]
lemma Extra_single_not:  \<comment> \<open>ternary logic, @{text "\<not> unknown = unknown"}\<close>
    "matches (\<beta>, \<alpha>) (MatchNot (Match (Extra str))) a p \<longleftrightarrow> \<alpha> a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (MatchNot (Match (Extra str))) a p = \<alpha> a p
[PROOF STEP]
by(simp add: Extra matches_case_ternaryvalue_tuple)


[STATEMENT]
lemma compress_extra_correct_matchexpr:
    fixes \<beta>::"('i::len common_primitive, ('i::len, 'a) tagged_packet_scheme) exact_match_tac"
    assumes generic: "primitive_matcher_generic \<beta>"
    shows "matches (\<beta>, \<alpha>) m = matches (\<beta>, \<alpha>) (compress_extra m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) m = matches (\<beta>, \<alpha>) (compress_extra m)
[PROOF STEP]
proof(simp add: fun_eq_iff, clarify, rename_tac a p)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p. matches (\<beta>, \<alpha>) m a p = matches (\<beta>, \<alpha>) (compress_extra m) a p
[PROOF STEP]
fix a and p :: "('i, 'a) tagged_packet_scheme"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p. matches (\<beta>, \<alpha>) m a p = matches (\<beta>, \<alpha>) (compress_extra m) a p
[PROOF STEP]
from generic
[PROOF STATE]
proof (chain)
picking this:
primitive_matcher_generic \<beta>
[PROOF STEP]
have "\<beta> (Extra e) p = TernaryUnknown" for e
[PROOF STATE]
proof (prove)
using this:
primitive_matcher_generic \<beta>

goal (1 subgoal):
 1. \<beta> (Extra e) p = TernaryUnknown
[PROOF STEP]
by(simp add: primitive_matcher_generic.Extra)
[PROOF STATE]
proof (state)
this:
\<beta> (Extra ?e) p = TernaryUnknown

goal (1 subgoal):
 1. \<And>a p. matches (\<beta>, \<alpha>) m a p = matches (\<beta>, \<alpha>) (compress_extra m) a p
[PROOF STEP]
hence "ternary_ternary_eval (map_match_tac \<beta> p m) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra m))"
[PROOF STATE]
proof (prove)
using this:
\<beta> (Extra ?e) p = TernaryUnknown

goal (1 subgoal):
 1. ternary_ternary_eval (map_match_tac \<beta> p m) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra m))
[PROOF STEP]
proof(induction m rule: compress_extra.induct)
[PROOF STATE]
proof (state)
goal (30 subgoals):
 1. \<And>x. (\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match x)) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match x)))
 2. \<And>e. (\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (Extra e)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (Extra e)))))
 3. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (Src va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (Src va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (Src va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (Src va)))))
 4. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (Dst va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (Dst va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (Dst va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (Dst va)))))
 5. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (IIface va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (IIface va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (IIface va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (IIface va)))))
 6. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (OIface va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (OIface va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (OIface va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (OIface va)))))
 7. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (Prot va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (Prot va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (Prot va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (Prot va)))))
 8. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (Src_Ports va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (Src_Ports va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (Src_Ports va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (Src_Ports va)))))
 9. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (Dst_Ports va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (Dst_Ports va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (Dst_Ports va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (Dst_Ports va)))))
 10. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (MultiportPorts va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (MultiportPorts va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (MultiportPorts va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (MultiportPorts va)))))
A total of 30 subgoals...
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:
(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p m2_) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra m2_))
\<beta> (Extra ?e) p = TernaryUnknown

goal (30 subgoals):
 1. \<And>x. (\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match x)) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match x)))
 2. \<And>e. (\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (Extra e)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (Extra e)))))
 3. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (Src va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (Src va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (Src va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (Src va)))))
 4. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (Dst va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (Dst va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (Dst va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (Dst va)))))
 5. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (IIface va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (IIface va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (IIface va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (IIface va)))))
 6. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (OIface va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (OIface va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (OIface va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (OIface va)))))
 7. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (Prot va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (Prot va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (Prot va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (Prot va)))))
 8. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (Src_Ports va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (Src_Ports va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (Src_Ports va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (Src_Ports va)))))
 9. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (Dst_Ports va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (Dst_Ports va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (Dst_Ports va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (Dst_Ports va)))))
 10. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (MultiportPorts va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (MultiportPorts va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (MultiportPorts va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (MultiportPorts va)))))
A total of 30 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p m2_) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra m2_))
\<beta> (Extra ?e) p = TernaryUnknown

goal (1 subgoal):
 1. ternary_ternary_eval (map_match_tac \<beta> p (MatchAnd (Match (Extra e1_)) m2_)) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchAnd (Match (Extra e1_)) m2_)))
[PROOF STEP]
by(simp_all split: match_expr.split match_expr.split_asm common_primitive.split)
[PROOF STATE]
proof (state)
this:
ternary_ternary_eval (map_match_tac \<beta> p (MatchAnd (Match (Extra e1_)) m2_)) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchAnd (Match (Extra e1_)) m2_)))

goal (29 subgoals):
 1. \<And>x. (\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match x)) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match x)))
 2. \<And>e. (\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (Extra e)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (Extra e)))))
 3. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (Src va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (Src va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (Src va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (Src va)))))
 4. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (Dst va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (Dst va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (Dst va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (Dst va)))))
 5. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (IIface va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (IIface va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (IIface va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (IIface va)))))
 6. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (OIface va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (OIface va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (OIface va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (OIface va)))))
 7. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (Prot va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (Prot va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (Prot va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (Prot va)))))
 8. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (Src_Ports va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (Src_Ports va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (Src_Ports va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (Src_Ports va)))))
 9. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (Dst_Ports va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (Dst_Ports va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (Dst_Ports va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (Dst_Ports va)))))
 10. \<And>va. \<lbrakk>(\<And>e. \<beta> (Extra e) p = TernaryUnknown) \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (Match (MultiportPorts va))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (Match (MultiportPorts va)))); \<And>e. \<beta> (Extra e) p = TernaryUnknown\<rbrakk> \<Longrightarrow> ternary_ternary_eval (map_match_tac \<beta> p (MatchNot (Match (MultiportPorts va)))) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra (MatchNot (Match (MultiportPorts va)))))
A total of 29 subgoals...
[PROOF STEP]
qed (simp_all)
[PROOF STATE]
proof (state)
this:
ternary_ternary_eval (map_match_tac \<beta> p m) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra m))

goal (1 subgoal):
 1. \<And>a p. matches (\<beta>, \<alpha>) m a p = matches (\<beta>, \<alpha>) (compress_extra m) a p
[PROOF STEP]
thus "matches (\<beta>, \<alpha>) m a p = matches (\<beta>, \<alpha>) (compress_extra m) a p"
[PROOF STATE]
proof (prove)
using this:
ternary_ternary_eval (map_match_tac \<beta> p m) = ternary_ternary_eval (map_match_tac \<beta> p (compress_extra m))

goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) m a p = matches (\<beta>, \<alpha>) (compress_extra m) a p
[PROOF STEP]
by(rule matches_iff_apply_f)
[PROOF STATE]
proof (state)
this:
matches (\<beta>, \<alpha>) m a p = matches (\<beta>, \<alpha>) (compress_extra m) a p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma resComm:
  fixes P :: pi

  shows "<\<nu>a><\<nu>b>P \<approx>\<^sup>s <\<nu>b><\<nu>a>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<nu>a><\<nu>b>P \<approx>\<^sup>s <\<nu>b><\<nu>a>P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. <\<nu>a><\<nu>b>P \<approx>\<^sup>s <\<nu>b><\<nu>a>P
[PROOF STEP]
have "<\<nu>a><\<nu>b>P \<sim>\<^sup>s <\<nu>b><\<nu>a>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<nu>a><\<nu>b>P \<sim>\<^sup>s <\<nu>b><\<nu>a>P
[PROOF STEP]
by(rule Strong_Late_Bisim_Subst_SC.resComm)
[PROOF STATE]
proof (state)
this:
<\<nu>a><\<nu>b>P \<sim>\<^sup>s <\<nu>b><\<nu>a>P

goal (1 subgoal):
 1. <\<nu>a><\<nu>b>P \<approx>\<^sup>s <\<nu>b><\<nu>a>P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
<\<nu>a><\<nu>b>P \<sim>\<^sup>s <\<nu>b><\<nu>a>P

goal (1 subgoal):
 1. <\<nu>a><\<nu>b>P \<approx>\<^sup>s <\<nu>b><\<nu>a>P
[PROOF STEP]
by(rule strongBisimWeakBisim)
[PROOF STATE]
proof (state)
this:
<\<nu>a><\<nu>b>P \<approx>\<^sup>s <\<nu>b><\<nu>a>P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matchId:
  fixes a :: name
  and   P :: pi

  shows "[a\<frown>a]P \<approx>\<^sup>s P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a\<frown>a]P \<approx>\<^sup>s P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [a\<frown>a]P \<approx>\<^sup>s P
[PROOF STEP]
have "[a\<frown>a]P \<sim>\<^sup>s P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a\<frown>a]P \<sim>\<^sup>s P
[PROOF STEP]
by(rule Strong_Late_Bisim_Subst_SC.matchId)
[PROOF STATE]
proof (state)
this:
[a\<frown>a]P \<sim>\<^sup>s P

goal (1 subgoal):
 1. [a\<frown>a]P \<approx>\<^sup>s P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[a\<frown>a]P \<sim>\<^sup>s P

goal (1 subgoal):
 1. [a\<frown>a]P \<approx>\<^sup>s P
[PROOF STEP]
by(rule strongBisimWeakBisim)
[PROOF STATE]
proof (state)
this:
[a\<frown>a]P \<approx>\<^sup>s P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mismatchNil:
  fixes a :: name
  and   P :: pi

  shows "[a\<noteq>a]P \<approx>\<^sup>s \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a\<noteq>a]P \<approx>\<^sup>s \<zero>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [a\<noteq>a]P \<approx>\<^sup>s \<zero>
[PROOF STEP]
have "[a\<noteq>a]P \<sim>\<^sup>s \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a\<noteq>a]P \<sim>\<^sup>s \<zero>
[PROOF STEP]
by(rule Strong_Late_Bisim_Subst_SC.mismatchNil)
[PROOF STATE]
proof (state)
this:
[a\<noteq>a]P \<sim>\<^sup>s \<zero>

goal (1 subgoal):
 1. [a\<noteq>a]P \<approx>\<^sup>s \<zero>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[a\<noteq>a]P \<sim>\<^sup>s \<zero>

goal (1 subgoal):
 1. [a\<noteq>a]P \<approx>\<^sup>s \<zero>
[PROOF STEP]
by(rule strongBisimWeakBisim)
[PROOF STATE]
proof (state)
this:
[a\<noteq>a]P \<approx>\<^sup>s \<zero>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sumSym:
  fixes P :: pi
  and   Q :: pi

  shows "P \<oplus> Q \<approx>\<^sup>s Q \<oplus> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<oplus> Q \<approx>\<^sup>s Q \<oplus> P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<oplus> Q \<approx>\<^sup>s Q \<oplus> P
[PROOF STEP]
have "P \<oplus> Q \<sim>\<^sup>s Q \<oplus> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<oplus> Q \<sim>\<^sup>s Q \<oplus> P
[PROOF STEP]
by(rule Strong_Late_Bisim_Subst_SC.sumSym)
[PROOF STATE]
proof (state)
this:
P \<oplus> Q \<sim>\<^sup>s Q \<oplus> P

goal (1 subgoal):
 1. P \<oplus> Q \<approx>\<^sup>s Q \<oplus> P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
P \<oplus> Q \<sim>\<^sup>s Q \<oplus> P

goal (1 subgoal):
 1. P \<oplus> Q \<approx>\<^sup>s Q \<oplus> P
[PROOF STEP]
by(rule strongBisimWeakBisim)
[PROOF STATE]
proof (state)
this:
P \<oplus> Q \<approx>\<^sup>s Q \<oplus> P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sumAssoc:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi

  shows "(P \<oplus> Q) \<oplus> R \<approx>\<^sup>s P \<oplus> (Q \<oplus> R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<oplus> Q) \<oplus> R \<approx>\<^sup>s P \<oplus> Q \<oplus> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (P \<oplus> Q) \<oplus> R \<approx>\<^sup>s P \<oplus> Q \<oplus> R
[PROOF STEP]
have "(P \<oplus> Q) \<oplus> R \<sim>\<^sup>s P \<oplus> (Q \<oplus> R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<oplus> Q) \<oplus> R \<sim>\<^sup>s P \<oplus> Q \<oplus> R
[PROOF STEP]
by(rule Strong_Late_Bisim_Subst_SC.sumAssoc)
[PROOF STATE]
proof (state)
this:
(P \<oplus> Q) \<oplus> R \<sim>\<^sup>s P \<oplus> Q \<oplus> R

goal (1 subgoal):
 1. (P \<oplus> Q) \<oplus> R \<approx>\<^sup>s P \<oplus> Q \<oplus> R
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(P \<oplus> Q) \<oplus> R \<sim>\<^sup>s P \<oplus> Q \<oplus> R

goal (1 subgoal):
 1. (P \<oplus> Q) \<oplus> R \<approx>\<^sup>s P \<oplus> Q \<oplus> R
[PROOF STEP]
by(rule strongBisimWeakBisim)
[PROOF STATE]
proof (state)
this:
(P \<oplus> Q) \<oplus> R \<approx>\<^sup>s P \<oplus> Q \<oplus> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sumZero:
  fixes P :: pi

  shows "P \<oplus> \<zero> \<approx>\<^sup>s P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<oplus> \<zero> \<approx>\<^sup>s P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<oplus> \<zero> \<approx>\<^sup>s P
[PROOF STEP]
have "P \<oplus> \<zero> \<sim>\<^sup>s P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<oplus> \<zero> \<sim>\<^sup>s P
[PROOF STEP]
by(rule Strong_Late_Bisim_Subst_SC.sumZero)
[PROOF STATE]
proof (state)
this:
P \<oplus> \<zero> \<sim>\<^sup>s P

goal (1 subgoal):
 1. P \<oplus> \<zero> \<approx>\<^sup>s P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
P \<oplus> \<zero> \<sim>\<^sup>s P

goal (1 subgoal):
 1. P \<oplus> \<zero> \<approx>\<^sup>s P
[PROOF STEP]
by(rule strongBisimWeakBisim)
[PROOF STATE]
proof (state)
this:
P \<oplus> \<zero> \<approx>\<^sup>s P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma parZero:
  fixes P :: pi

  shows "P \<parallel> \<zero> \<approx>\<^sup>s P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> \<zero> \<approx>\<^sup>s P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<parallel> \<zero> \<approx>\<^sup>s P
[PROOF STEP]
have "P \<parallel> \<zero> \<sim>\<^sup>s P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> \<zero> \<sim>\<^sup>s P
[PROOF STEP]
by(rule Strong_Late_Bisim_Subst_SC.parZero)
[PROOF STATE]
proof (state)
this:
P \<parallel> \<zero> \<sim>\<^sup>s P

goal (1 subgoal):
 1. P \<parallel> \<zero> \<approx>\<^sup>s P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
P \<parallel> \<zero> \<sim>\<^sup>s P

goal (1 subgoal):
 1. P \<parallel> \<zero> \<approx>\<^sup>s P
[PROOF STEP]
by(rule strongBisimWeakBisim)
[PROOF STATE]
proof (state)
this:
P \<parallel> \<zero> \<approx>\<^sup>s P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma parSym:
  fixes P :: pi
  and   Q :: pi

  shows "P \<parallel> Q \<approx>\<^sup>s Q \<parallel> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> Q \<approx>\<^sup>s Q \<parallel> P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<parallel> Q \<approx>\<^sup>s Q \<parallel> P
[PROOF STEP]
have "P \<parallel> Q \<sim>\<^sup>s Q \<parallel> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> Q \<sim>\<^sup>s Q \<parallel> P
[PROOF STEP]
by(rule Strong_Late_Bisim_Subst_SC.parSym)
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<sim>\<^sup>s Q \<parallel> P

goal (1 subgoal):
 1. P \<parallel> Q \<approx>\<^sup>s Q \<parallel> P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
P \<parallel> Q \<sim>\<^sup>s Q \<parallel> P

goal (1 subgoal):
 1. P \<parallel> Q \<approx>\<^sup>s Q \<parallel> P
[PROOF STEP]
by(rule strongBisimWeakBisim)
[PROOF STATE]
proof (state)
this:
P \<parallel> Q \<approx>\<^sup>s Q \<parallel> P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma scopeExtPar:
  fixes P :: pi
  and   Q :: pi
  and   x :: name

  assumes "x \<sharp> P"

  shows "<\<nu>x>(P \<parallel> Q) \<approx>\<^sup>s P \<parallel> <\<nu>x>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<nu>x>(P \<parallel> Q) \<approx>\<^sup>s P \<parallel> <\<nu>x>Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. <\<nu>x>(P \<parallel> Q) \<approx>\<^sup>s P \<parallel> <\<nu>x>Q
[PROOF STEP]
from \<open>x \<sharp> P\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<sharp> P
[PROOF STEP]
have "<\<nu>x>(P \<parallel> Q) \<sim>\<^sup>s P \<parallel> <\<nu>x>Q"
[PROOF STATE]
proof (prove)
using this:
x \<sharp> P

goal (1 subgoal):
 1. <\<nu>x>(P \<parallel> Q) \<sim>\<^sup>s P \<parallel> <\<nu>x>Q
[PROOF STEP]
by(rule Strong_Late_Bisim_Subst_SC.scopeExtPar)
[PROOF STATE]
proof (state)
this:
<\<nu>x>(P \<parallel> Q) \<sim>\<^sup>s P \<parallel> <\<nu>x>Q

goal (1 subgoal):
 1. <\<nu>x>(P \<parallel> Q) \<approx>\<^sup>s P \<parallel> <\<nu>x>Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
<\<nu>x>(P \<parallel> Q) \<sim>\<^sup>s P \<parallel> <\<nu>x>Q

goal (1 subgoal):
 1. <\<nu>x>(P \<parallel> Q) \<approx>\<^sup>s P \<parallel> <\<nu>x>Q
[PROOF STEP]
by(rule strongBisimWeakBisim)
[PROOF STATE]
proof (state)
this:
<\<nu>x>(P \<parallel> Q) \<approx>\<^sup>s P \<parallel> <\<nu>x>Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma scopeExtPar':
  fixes P :: pi
  and   Q :: pi
  and   x :: name

  assumes "x \<sharp> Q"

  shows "<\<nu>x>(P \<parallel> Q) \<approx>\<^sup>s (<\<nu>x>P) \<parallel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<nu>x>(P \<parallel> Q) \<approx>\<^sup>s <\<nu>x>P \<parallel> Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. <\<nu>x>(P \<parallel> Q) \<approx>\<^sup>s <\<nu>x>P \<parallel> Q
[PROOF STEP]
from \<open>x \<sharp> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<sharp> Q
[PROOF STEP]
have "<\<nu>x>(P \<parallel> Q) \<sim>\<^sup>s (<\<nu>x>P) \<parallel> Q"
[PROOF STATE]
proof (prove)
using this:
x \<sharp> Q

goal (1 subgoal):
 1. <\<nu>x>(P \<parallel> Q) \<sim>\<^sup>s <\<nu>x>P \<parallel> Q
[PROOF STEP]
by(rule Strong_Late_Bisim_Subst_SC.scopeExtPar')
[PROOF STATE]
proof (state)
this:
<\<nu>x>(P \<parallel> Q) \<sim>\<^sup>s <\<nu>x>P \<parallel> Q

goal (1 subgoal):
 1. <\<nu>x>(P \<parallel> Q) \<approx>\<^sup>s <\<nu>x>P \<parallel> Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
<\<nu>x>(P \<parallel> Q) \<sim>\<^sup>s <\<nu>x>P \<parallel> Q

goal (1 subgoal):
 1. <\<nu>x>(P \<parallel> Q) \<approx>\<^sup>s <\<nu>x>P \<parallel> Q
[PROOF STEP]
by(rule strongBisimWeakBisim)
[PROOF STATE]
proof (state)
this:
<\<nu>x>(P \<parallel> Q) \<approx>\<^sup>s <\<nu>x>P \<parallel> Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma parAssoc:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi

  shows "(P \<parallel> Q) \<parallel> R \<approx>\<^sup>s P \<parallel> (Q \<parallel> R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<parallel> Q) \<parallel> R \<approx>\<^sup>s P \<parallel> Q \<parallel> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (P \<parallel> Q) \<parallel> R \<approx>\<^sup>s P \<parallel> Q \<parallel> R
[PROOF STEP]
have "(P \<parallel> Q) \<parallel> R \<sim>\<^sup>s P \<parallel> (Q \<parallel> R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<parallel> Q) \<parallel> R \<sim>\<^sup>s P \<parallel> Q \<parallel> R
[PROOF STEP]
by(rule Strong_Late_Bisim_Subst_SC.parAssoc)
[PROOF STATE]
proof (state)
this:
(P \<parallel> Q) \<parallel> R \<sim>\<^sup>s P \<parallel> Q \<parallel> R

goal (1 subgoal):
 1. (P \<parallel> Q) \<parallel> R \<approx>\<^sup>s P \<parallel> Q \<parallel> R
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(P \<parallel> Q) \<parallel> R \<sim>\<^sup>s P \<parallel> Q \<parallel> R

goal (1 subgoal):
 1. (P \<parallel> Q) \<parallel> R \<approx>\<^sup>s P \<parallel> Q \<parallel> R
[PROOF STEP]
by(rule strongBisimWeakBisim)
[PROOF STATE]
proof (state)
this:
(P \<parallel> Q) \<parallel> R \<approx>\<^sup>s P \<parallel> Q \<parallel> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma freshRes:
  fixes P :: pi
  and   a :: name

  assumes "a \<sharp> P"

  shows "<\<nu>a>P \<approx>\<^sup>s P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<nu>a>P \<approx>\<^sup>s P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<sharp> P

goal (1 subgoal):
 1. <\<nu>a>P \<approx>\<^sup>s P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<sharp> P \<Longrightarrow> <\<nu>a>P \<approx>\<^sup>s P
[PROOF STEP]
from \<open>a \<sharp> P\<close>
[PROOF STATE]
proof (chain)
picking this:
a \<sharp> P
[PROOF STEP]
have "<\<nu>a>P \<sim>\<^sup>s P"
[PROOF STATE]
proof (prove)
using this:
a \<sharp> P

goal (1 subgoal):
 1. <\<nu>a>P \<sim>\<^sup>s P
[PROOF STEP]
by(rule Strong_Late_Bisim_Subst_SC.scopeFresh)
[PROOF STATE]
proof (state)
this:
<\<nu>a>P \<sim>\<^sup>s P

goal (1 subgoal):
 1. a \<sharp> P \<Longrightarrow> <\<nu>a>P \<approx>\<^sup>s P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
<\<nu>a>P \<sim>\<^sup>s P

goal (1 subgoal):
 1. <\<nu>a>P \<approx>\<^sup>s P
[PROOF STEP]
by(rule strongBisimWeakBisim)
[PROOF STATE]
proof (state)
this:
<\<nu>a>P \<approx>\<^sup>s P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma scopeExtSum:
  fixes P :: pi
  and   Q :: pi
  and   x :: name

  assumes "x \<sharp> P"

  shows "<\<nu>x>(P \<oplus> Q) \<approx>\<^sup>s P \<oplus> <\<nu>x>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<nu>x>(P \<oplus> Q) \<approx>\<^sup>s P \<oplus> <\<nu>x>Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. <\<nu>x>(P \<oplus> Q) \<approx>\<^sup>s P \<oplus> <\<nu>x>Q
[PROOF STEP]
from \<open>x \<sharp> P\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<sharp> P
[PROOF STEP]
have "<\<nu>x>(P \<oplus> Q) \<sim>\<^sup>s P \<oplus> <\<nu>x>Q"
[PROOF STATE]
proof (prove)
using this:
x \<sharp> P

goal (1 subgoal):
 1. <\<nu>x>(P \<oplus> Q) \<sim>\<^sup>s P \<oplus> <\<nu>x>Q
[PROOF STEP]
by(rule Strong_Late_Bisim_Subst_SC.scopeExtSum)
[PROOF STATE]
proof (state)
this:
<\<nu>x>(P \<oplus> Q) \<sim>\<^sup>s P \<oplus> <\<nu>x>Q

goal (1 subgoal):
 1. <\<nu>x>(P \<oplus> Q) \<approx>\<^sup>s P \<oplus> <\<nu>x>Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
<\<nu>x>(P \<oplus> Q) \<sim>\<^sup>s P \<oplus> <\<nu>x>Q

goal (1 subgoal):
 1. <\<nu>x>(P \<oplus> Q) \<approx>\<^sup>s P \<oplus> <\<nu>x>Q
[PROOF STEP]
by(rule strongBisimWeakBisim)
[PROOF STATE]
proof (state)
this:
<\<nu>x>(P \<oplus> Q) \<approx>\<^sup>s P \<oplus> <\<nu>x>Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bangSC:
  fixes P

  shows "!P \<approx>\<^sup>s P \<parallel> !P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. !P \<approx>\<^sup>s P \<parallel> !P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. !P \<approx>\<^sup>s P \<parallel> !P
[PROOF STEP]
have "!P \<sim>\<^sup>s P \<parallel> !P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. !P \<sim>\<^sup>s P \<parallel> !P
[PROOF STEP]
by(rule Strong_Late_Bisim_Subst_SC.bangSC)
[PROOF STATE]
proof (state)
this:
!P \<sim>\<^sup>s P \<parallel> !P

goal (1 subgoal):
 1. !P \<approx>\<^sup>s P \<parallel> !P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
!P \<sim>\<^sup>s P \<parallel> !P

goal (1 subgoal):
 1. !P \<approx>\<^sup>s P \<parallel> !P
[PROOF STEP]
by(rule strongBisimWeakBisim)
[PROOF STATE]
proof (state)
this:
!P \<approx>\<^sup>s P \<parallel> !P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma length_interpret_floatariths[simp]: "length (interpret_floatariths fas xs) = length fas"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (interpret_floatariths fas xs) = length fas
[PROOF STEP]
by (induction fas) auto


[STATEMENT]
lemma interpret_floatariths_nth[simp]:
  "interpret_floatariths fas xs ! n = interpret_floatarith (fas ! n) xs"
  if "n < length fas"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatariths fas xs ! n = interpret_floatarith (fas ! n) xs
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
n < length fas

goal (1 subgoal):
 1. interpret_floatariths fas xs ! n = interpret_floatarith (fas ! n) xs
[PROOF STEP]
by (induction fas arbitrary: n) (auto simp: nth_Cons split: nat.splits)


[STATEMENT]
lemma interpret_floatarith_uminus[simp]:
  "interpret_floatarith (- f) xs = - interpret_floatarith f xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (- f) xs = - interpret_floatarith f xs
[PROOF STEP]
by (auto simp: uminus_floatarith_def)


[STATEMENT]
lemma interpret_floatarith_plus[simp]:
  "interpret_floatarith (f + g) xs = interpret_floatarith f xs + interpret_floatarith g xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (f + g) xs = interpret_floatarith f xs + interpret_floatarith g xs
[PROOF STEP]
by (auto simp: plus_floatarith_def)


[STATEMENT]
lemma interpret_floatarith_minus[simp]:
  "interpret_floatarith (f - g) xs = interpret_floatarith f xs - interpret_floatarith g xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (f - g) xs = interpret_floatarith f xs - interpret_floatarith g xs
[PROOF STEP]
by (auto simp: minus_floatarith_def)


[STATEMENT]
lemma interpret_floatarith_inverse[simp]:
  "interpret_floatarith (inverse f) xs = inverse (interpret_floatarith f xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (inverse f) xs = inverse (interpret_floatarith f xs)
[PROOF STEP]
by (auto simp: inverse_floatarith_def)


[STATEMENT]
lemma interpret_floatarith_times[simp]:
  "interpret_floatarith (f * g) xs = interpret_floatarith f xs * interpret_floatarith g xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (f * g) xs = interpret_floatarith f xs * interpret_floatarith g xs
[PROOF STEP]
by (auto simp: times_floatarith_def)


[STATEMENT]
lemma interpret_floatarith_divide[simp]:
  "interpret_floatarith (f div g) xs = interpret_floatarith f xs / interpret_floatarith g xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (f div g) xs = interpret_floatarith f xs / interpret_floatarith g xs
[PROOF STEP]
by (auto simp: divide_floatarith_def inverse_eq_divide)


[STATEMENT]
lemma interpret_floatarith_one[simp]:
  "interpret_floatarith 1 xs = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith 1 xs = 1
[PROOF STEP]
by (auto simp: one_floatarith_def)


[STATEMENT]
lemma interpret_floatarith_zero[simp]:
  "interpret_floatarith 0 xs = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith 0 xs = 0
[PROOF STEP]
by (auto simp: zero_floatarith_def)


[STATEMENT]
lemma interpret_R\<^sub>e[simp]: "interpret_floatarith (R\<^sub>e x) xs = real_of_rat x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (R\<^sub>e x) xs = real_of_rat x
[PROOF STEP]
by (auto simp: R\<^sub>e_def of_rat_divide dest!: quotient_of_div split: prod.splits)


[STATEMENT]
lemma interpret_floatarith_Sin[simp]:
  "interpret_floatarith (Sin x) vs = sin (interpret_floatarith x vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (Sin x) vs = sin (interpret_floatarith x vs)
[PROOF STEP]
by (auto simp: Sin_def approximation_preproc_floatarith(11))


[STATEMENT]
lemma interpret_Half[simp]: "interpret_floatarith (Half x) xs = interpret_floatarith x xs / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (Half x) xs = interpret_floatarith x xs / 2
[PROOF STEP]
by (auto simp: Half_def)


[STATEMENT]
lemma interpret_floatarith_Tan[simp]:
  "interpret_floatarith (Tan x) vs = tan (interpret_floatarith x vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (Tan x) vs = tan (interpret_floatarith x vs)
[PROOF STEP]
by (auto simp: Tan_def approximation_preproc_floatarith(12) inverse_eq_divide)


[STATEMENT]
lemma interpret_floatarith_Sum\<^sub>e[simp]:
  "interpret_floatarith (Sum\<^sub>e f x) vs = (\<Sum>i\<leftarrow>x. interpret_floatarith (f i) vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (Sum\<^sub>e f x) vs = (\<Sum>i\<leftarrow>x. interpret_floatarith (f i) vs)
[PROOF STEP]
by (induction x) auto


[STATEMENT]
lemma fold_const_fa[simp]: "interpret_floatarith (fold_const_fa fa) xs = interpret_floatarith fa xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (fold_const_fa fa) xs = interpret_floatarith fa xs
[PROOF STEP]
by (induction fa) (auto split!: prod.splits floatarith.splits option.splits
      elim!: dest_Num_fa_None dest_Num_fa_Some
      simp: max_def min_def floor_fl_def)


[STATEMENT]
lemma Max_Image_distrib:
  includes no_floatarith_notation
  assumes "finite X" "X \<noteq> {}"
  shows "Max ((\<lambda>x. max (f1 x) (f2 x)) ` X) = max (Max (f1 ` X)) (Max (f2 ` X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (MAX x\<in>X. max (f1 x) (f2 x)) = max (Max (f1 ` X)) (Max (f2 ` X))
[PROOF STEP]
apply (rule Max_eqI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite ((\<lambda>x. max (f1 x) (f2 x)) ` X)
 2. \<And>y. y \<in> (\<lambda>x. max (f1 x) (f2 x)) ` X \<Longrightarrow> y \<le> max (Max (f1 ` X)) (Max (f2 ` X))
 3. max (Max (f1 ` X)) (Max (f2 ` X)) \<in> (\<lambda>x. max (f1 x) (f2 x)) ` X
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ((\<lambda>x. max (f1 x) (f2 x)) ` X)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite X
X \<noteq> {}

goal (1 subgoal):
 1. finite ((\<lambda>x. max (f1 x) (f2 x)) ` X)
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y. y \<in> (\<lambda>x. max (f1 x) (f2 x)) ` X \<Longrightarrow> y \<le> max (Max (f1 ` X)) (Max (f2 ` X))
 2. max (Max (f1 ` X)) (Max (f2 ` X)) \<in> (\<lambda>x. max (f1 x) (f2 x)) ` X
[PROOF STEP]
subgoal for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> (\<lambda>x. max (f1 x) (f2 x)) ` X \<Longrightarrow> y \<le> max (Max (f1 ` X)) (Max (f2 ` X))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite X
X \<noteq> {}

goal (1 subgoal):
 1. y \<in> (\<lambda>x. max (f1 x) (f2 x)) ` X \<Longrightarrow> y \<le> max (Max (f1 ` X)) (Max (f2 ` X))
[PROOF STEP]
by (force intro: max.coboundedI1 max.coboundedI2 Max_ge)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (Max (f1 ` X)) (Max (f2 ` X)) \<in> (\<lambda>x. max (f1 x) (f2 x)) ` X
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (Max (f1 ` X)) (Max (f2 ` X)) \<in> (\<lambda>x. max (f1 x) (f2 x)) ` X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max (Max (f1 ` X)) (Max (f2 ` X)) \<in> (\<lambda>x. max (f1 x) (f2 x)) ` X
[PROOF STEP]
have "Max (f1 ` X) \<in> f1 ` X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (f1 ` X) \<in> f1 ` X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite X
X \<noteq> {}

goal (1 subgoal):
 1. Max (f1 ` X) \<in> f1 ` X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Max (f1 ` X) \<in> f1 ` X

goal (1 subgoal):
 1. max (Max (f1 ` X)) (Max (f2 ` X)) \<in> (\<lambda>x. max (f1 x) (f2 x)) ` X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Max (f1 ` X) \<in> f1 ` X
[PROOF STEP]
obtain x1 where x1: "x1 \<in> X" "Max (f1 ` X) = f1 x1"
[PROOF STATE]
proof (prove)
using this:
Max (f1 ` X) \<in> f1 ` X

goal (1 subgoal):
 1. (\<And>x1. \<lbrakk>x1 \<in> X; Max (f1 ` X) = f1 x1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x1 \<in> X
Max (f1 ` X) = f1 x1

goal (1 subgoal):
 1. max (Max (f1 ` X)) (Max (f2 ` X)) \<in> (\<lambda>x. max (f1 x) (f2 x)) ` X
[PROOF STEP]
have "Max (f2 ` X) \<in> f2 ` X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (f2 ` X) \<in> f2 ` X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite X
X \<noteq> {}

goal (1 subgoal):
 1. Max (f2 ` X) \<in> f2 ` X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Max (f2 ` X) \<in> f2 ` X

goal (1 subgoal):
 1. max (Max (f1 ` X)) (Max (f2 ` X)) \<in> (\<lambda>x. max (f1 x) (f2 x)) ` X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Max (f2 ` X) \<in> f2 ` X
[PROOF STEP]
obtain x2 where x2: "x2 \<in> X" "Max (f2 ` X) = f2 x2"
[PROOF STATE]
proof (prove)
using this:
Max (f2 ` X) \<in> f2 ` X

goal (1 subgoal):
 1. (\<And>x2. \<lbrakk>x2 \<in> X; Max (f2 ` X) = f2 x2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x2 \<in> X
Max (f2 ` X) = f2 x2

goal (1 subgoal):
 1. max (Max (f1 ` X)) (Max (f2 ` X)) \<in> (\<lambda>x. max (f1 x) (f2 x)) ` X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (Max (f1 ` X)) (Max (f2 ` X)) \<in> (\<lambda>x. max (f1 x) (f2 x)) ` X
[PROOF STEP]
apply (rule image_eqI[where x="if f1 x1 \<le> f2 x2 then x2 else x1"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. max (Max (f1 ` X)) (Max (f2 ` X)) = max (f1 (if f1 x1 \<le> f2 x2 then x2 else x1)) (f2 (if f1 x1 \<le> f2 x2 then x2 else x1))
 2. (if f1 x1 \<le> f2 x2 then x2 else x1) \<in> X
[PROOF STEP]
using x1 x2 assms
[PROOF STATE]
proof (prove)
using this:
x1 \<in> X
Max (f1 ` X) = f1 x1
x2 \<in> X
Max (f2 ` X) = f2 x2
finite X
X \<noteq> {}

goal (2 subgoals):
 1. max (Max (f1 ` X)) (Max (f2 ` X)) = max (f1 (if f1 x1 \<le> f2 x2 then x2 else x1)) (f2 (if f1 x1 \<le> f2 x2 then x2 else x1))
 2. (if f1 x1 \<le> f2 x2 then x2 else x1) \<in> X
[PROOF STEP]
apply (auto simp: max_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x1 \<in> X; Max (f1 ` X) = f1 x1; x2 \<in> X; Max (f2 ` X) = f2 x2; finite X; x \<in> X; f1 x1 \<le> f2 x2; \<not> f1 x2 \<le> f2 x2\<rbrakk> \<Longrightarrow> f2 x2 = f1 x2
 2. \<And>x. \<lbrakk>x1 \<in> X; Max (f1 ` X) = f1 x1; x2 \<in> X; Max (f2 ` X) = f2 x2; finite X; x \<in> X; \<not> f1 x1 \<le> f2 x2; f1 x1 \<le> f2 x1\<rbrakk> \<Longrightarrow> f1 x1 = f2 x1
[PROOF STEP]
apply (metis Max_ge dual_order.trans finite_imageI image_eqI assms(1))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x1 \<in> X; Max (f1 ` X) = f1 x1; x2 \<in> X; Max (f2 ` X) = f2 x2; finite X; x \<in> X; \<not> f1 x1 \<le> f2 x2; f1 x1 \<le> f2 x1\<rbrakk> \<Longrightarrow> f1 x1 = f2 x1
[PROOF STEP]
apply (metis Max_ge dual_order.trans finite_imageI image_eqI assms(1))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
max (Max (f1 ` X)) (Max (f2 ` X)) \<in> (\<lambda>x. max (f1 x) (f2 x)) ` X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma max_Var_floatarith_simps[simp]:
  "max_Var_floatarith (a / b) = max (max_Var_floatarith a) (max_Var_floatarith b)"
  "max_Var_floatarith (a * b) = max (max_Var_floatarith a) (max_Var_floatarith b)"
  "max_Var_floatarith (a + b) = max (max_Var_floatarith a) (max_Var_floatarith b)"
  "max_Var_floatarith (a - b) = max (max_Var_floatarith a) (max_Var_floatarith b)"
  "max_Var_floatarith (- b) = (max_Var_floatarith b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (max_Var_floatarith (a / b) = max (max_Var_floatarith a) (max_Var_floatarith b) &&& max_Var_floatarith (a * b) = max (max_Var_floatarith a) (max_Var_floatarith b)) &&& max_Var_floatarith (a + b) = max (max_Var_floatarith a) (max_Var_floatarith b) &&& max_Var_floatarith (a - b) = max (max_Var_floatarith a) (max_Var_floatarith b) &&& max_Var_floatarith (- b) = max_Var_floatarith b
[PROOF STEP]
by (auto simp: divide_floatarith_def times_floatarith_def plus_floatarith_def minus_floatarith_def
      uminus_floatarith_def)


[STATEMENT]
lemma max_Var_floatariths_Max:
  "max_Var_floatariths xs = (if set xs = {} then 0 else linorder_class.Max (max_Var_floatarith ` set xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatariths xs = (if set xs = {} then 0 else Max (max_Var_floatarith ` set xs))
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma max_Var_floatariths_map_plus[simp]:
  "max_Var_floatariths (map (\<lambda>i. fa1 i + fa2 i) xs) = max (max_Var_floatariths (map fa1 xs)) (max_Var_floatariths (map fa2 xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatariths (map (\<lambda>i. fa1 i + fa2 i) xs) = max (max_Var_floatariths (map fa1 xs)) (max_Var_floatariths (map fa2 xs))
[PROOF STEP]
by (auto simp: max_Var_floatariths_Max image_image Max_Image_distrib)


[STATEMENT]
lemma max_Var_floatariths_map_times[simp]:
  "max_Var_floatariths (map (\<lambda>i. fa1 i * fa2 i) xs) = max (max_Var_floatariths (map fa1 xs)) (max_Var_floatariths (map fa2 xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatariths (map (\<lambda>i. fa1 i * fa2 i) xs) = max (max_Var_floatariths (map fa1 xs)) (max_Var_floatariths (map fa2 xs))
[PROOF STEP]
by (auto simp: max_Var_floatariths_Max image_image Max_Image_distrib)


[STATEMENT]
lemma max_Var_floatariths_map_divide[simp]:
  "max_Var_floatariths (map (\<lambda>i. fa1 i / fa2 i) xs) = max (max_Var_floatariths (map fa1 xs)) (max_Var_floatariths (map fa2 xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatariths (map (\<lambda>i. fa1 i / fa2 i) xs) = max (max_Var_floatariths (map fa1 xs)) (max_Var_floatariths (map fa2 xs))
[PROOF STEP]
by (auto simp: max_Var_floatariths_Max image_image Max_Image_distrib)


[STATEMENT]
lemma max_Var_floatariths_map_const[simp]:
  "max_Var_floatariths (map (\<lambda>i. fa) xs) = (if xs = [] then 0 else max_Var_floatarith fa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatariths (map (\<lambda>i. fa) xs) = (if xs = [] then 0 else max_Var_floatarith fa)
[PROOF STEP]
by (auto simp: max_Var_floatariths_Max image_image image_constant_conv)


[STATEMENT]
lemma max_Var_floatariths_map_minus[simp]:
  "max_Var_floatariths (map (\<lambda>i. fa1 i - fa2 i) xs) = max (max_Var_floatariths (map fa1 xs)) (max_Var_floatariths (map fa2 xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatariths (map (\<lambda>i. fa1 i - fa2 i) xs) = max (max_Var_floatariths (map fa1 xs)) (max_Var_floatariths (map fa2 xs))
[PROOF STEP]
by (auto simp: max_Var_floatariths_Max image_image Max_Image_distrib)


[STATEMENT]
lemma fresh_floatarith_subst:
  fixes v::float
  assumes "fresh_floatarith e x"
  assumes "x < length vs"
  shows "interpret_floatarith e (vs[x:=v]) = interpret_floatarith e vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith e (map real_of_float (vs[x := v])) = interpret_floatarith e (map real_of_float vs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
fresh_floatarith e x
x < length vs

goal (1 subgoal):
 1. interpret_floatarith e (map real_of_float (vs[x := v])) = interpret_floatarith e (map real_of_float vs)
[PROOF STEP]
by (induction e) (auto simp: map_update)


[STATEMENT]
lemma fresh_floatarith_max_Var:
  assumes "max_Var_floatarith ea \<le> i"
  shows "fresh_floatarith ea i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fresh_floatarith ea i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
max_Var_floatarith ea \<le> i

goal (1 subgoal):
 1. fresh_floatarith ea i
[PROOF STEP]
by (induction ea) auto


[STATEMENT]
lemma fresh_floatariths_max_Var:
  assumes "max_Var_floatariths ea \<le> i"
  shows "fresh_floatariths ea i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fresh_floatariths ea i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
max_Var_floatariths ea \<le> i

goal (1 subgoal):
 1. fresh_floatariths ea i
[PROOF STEP]
by (induction ea) (auto simp: fresh_floatarith_max_Var)


[STATEMENT]
lemma max_Var_floatarith_le_max_Var_floatariths:
  "fa \<in> set fas \<Longrightarrow> max_Var_floatarith fa \<le> max_Var_floatariths fas"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fa \<in> set fas \<Longrightarrow> max_Var_floatarith fa \<le> max_Var_floatariths fas
[PROOF STEP]
by (induction fas) (auto simp: nth_Cons max_def split: nat.splits)


[STATEMENT]
lemma max_Var_floatarith_le_max_Var_floatariths_nth:
  "n < length fas \<Longrightarrow> max_Var_floatarith (fas ! n) \<le> max_Var_floatariths fas"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < length fas \<Longrightarrow> max_Var_floatarith (fas ! n) \<le> max_Var_floatariths fas
[PROOF STEP]
by (rule max_Var_floatarith_le_max_Var_floatariths) auto


[STATEMENT]
lemma max_Var_floatariths_leI:
  assumes "\<And>i. i < length xs \<Longrightarrow> max_Var_floatarith (xs ! i) \<le> F"
  shows "max_Var_floatariths xs \<le> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatariths xs \<le> F
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?i < length xs \<Longrightarrow> max_Var_floatarith (xs ! ?i) \<le> F

goal (1 subgoal):
 1. max_Var_floatariths xs \<le> F
[PROOF STEP]
by (auto simp: max_Var_floatariths_Max in_set_conv_nth)


[STATEMENT]
lemma fresh_floatariths_map_Var[simp]:
  "fresh_floatariths (map floatarith.Var xs) i \<longleftrightarrow> i \<notin> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fresh_floatariths (map Var xs) i = (i \<notin> set xs)
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma max_Var_floatarith_fold_const_fa:
  "max_Var_floatarith (fold_const_fa fa) \<le> max_Var_floatarith fa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatarith (fold_const_fa fa) \<le> max_Var_floatarith fa
[PROOF STEP]
by (induction fa) (auto simp: fold_const_fa.simps split!: option.splits floatarith.splits)


[STATEMENT]
lemma max_Var_floatariths_fold_const_fa:
  "max_Var_floatariths (map fold_const_fa xs) \<le> max_Var_floatariths xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatariths (map fold_const_fa xs) \<le> max_Var_floatariths xs
[PROOF STEP]
by (auto simp: intro!: max_Var_floatariths_leI max_Var_floatarith_le_max_Var_floatariths_nth
      max_Var_floatarith_fold_const_fa[THEN order_trans])


[STATEMENT]
lemma interpret_form_max_Var_cong:
  assumes "\<And>i. i < max_Var_form f \<Longrightarrow> xs ! i = ys ! i"
  shows "interpret_form f xs = interpret_form f ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_form f xs = interpret_form f ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?i < max_Var_form f \<Longrightarrow> xs ! ?i = ys ! ?i

goal (1 subgoal):
 1. interpret_form f xs = interpret_form f ys
[PROOF STEP]
by (induction f) (auto simp: interpret_floatarith_max_Var_cong[where xs=xs and ys=ys])


[STATEMENT]
lemma interpret_floatariths_max_Var_cong:
  assumes "\<And>i. i < max_Var_floatariths f \<Longrightarrow> xs ! i = ys ! i"
  shows "interpret_floatariths f ys = interpret_floatariths f xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatariths f ys = interpret_floatariths f xs
[PROOF STEP]
by (auto intro!: nth_equalityI interpret_floatarith_max_Var_cong assms max_Var_floatariths_lessI)


[STATEMENT]
lemma max_Var_floatarithimage_Var[simp]: "max_Var_floatarith ` Var ` X = Suc ` X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatarith ` Var ` X = Suc ` X
[PROOF STEP]
by force


[STATEMENT]
lemma max_Var_floatariths_map_Var[simp]:
  "max_Var_floatariths (map Var xs) = (if xs = [] then 0 else Suc (linorder_class.Max (set xs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatariths (map Var xs) = (if xs = [] then 0 else Suc (Max (set xs)))
[PROOF STEP]
by (auto simp: max_Var_floatariths_Max hom_Max_commute split: if_splits)


[STATEMENT]
lemma Max_atLeastLessThan_nat[simp]: "a < b \<Longrightarrow> linorder_class.Max {a..<b} = b - 1" for a b::nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < b \<Longrightarrow> Max {a..<b} = b - 1
[PROOF STEP]
by (auto intro!: Max_eqI)


[STATEMENT]
lemma isDERIV_Power_iff: "isDERIV j (Power fa n) xs = (if n = 0 then True else isDERIV j fa xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDERIV j (fa ^\<^sub>e n) xs = (if n = 0 then True else isDERIV j fa xs)
[PROOF STEP]
by (cases n) auto