[STATEMENT]
lemma wfT_restrict2:
  fixes \<tau>::\<tau>
  assumes "wfT \<Theta> \<B> ((x, b, c) #\<^sub>\<Gamma> \<Gamma>) \<tau>" and "atom x \<sharp> \<tau>"
  shows "\<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta> ; \<B> ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<tau>
[PROOF STEP]
using wf_restrict1(4)[of \<Theta> \<B> "((x, b, c) #\<^sub>\<Gamma> \<Gamma>)"  \<tau> GNil x "b" "c" \<Gamma>] assms fresh_GNil append_g.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> \<Theta> ; \<B> ; (x, b, c) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<tau> ; (x, b, c) #\<^sub>\<Gamma> \<Gamma> = GNil @ (x, b, c) #\<^sub>\<Gamma> \<Gamma>; atom x \<sharp> \<tau>; atom x \<sharp> GNil\<rbrakk> \<Longrightarrow>  \<Theta> ; \<B> ; GNil @ \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<tau>
 \<Theta> ; \<B> ; (x, b, c) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<tau>
atom x \<sharp> \<tau>
?a \<sharp> GNil
GNil @ ?g = ?g
(?xbc #\<^sub>\<Gamma> ?g1.0) @ ?g2.0 = ?xbc #\<^sub>\<Gamma> ?g1.0 @ ?g2.0

goal (1 subgoal):
 1.  \<Theta> ; \<B> ; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<tau>
[PROOF STEP]
by auto


[STATEMENT]
lemma successive_ends_1:
  "successive P xs \<Longrightarrow> \<not> P x \<Longrightarrow> successive P ys \<Longrightarrow> successive P (xs @ x # ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>successive P xs; \<not> P x; successive P ys\<rbrakk> \<Longrightarrow> successive P (xs @ x # ys)
[PROOF STEP]
by (induction _ xs rule: list_two_induct) (fastforce intro: successive_stepI)+


[STATEMENT]
lemma B_accessible[intro]: "(i, j) \<in> B.acc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i, j) \<in> B.acc
[PROOF STEP]
proof (cases i j rule: linorder_le_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i \<le> j \<Longrightarrow> (i, j) \<in> B.acc
 2. j \<le> i \<Longrightarrow> (i, j) \<in> B.acc
[PROOF STEP]
assume "i \<le> j"
[PROOF STATE]
proof (state)
this:
i \<le> j

goal (2 subgoals):
 1. i \<le> j \<Longrightarrow> (i, j) \<in> B.acc
 2. j \<le> i \<Longrightarrow> (i, j) \<in> B.acc
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<le> j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<le> j

goal (1 subgoal):
 1. (i, j) \<in> B.acc
[PROOF STEP]
by (induct rule: inc_induct) (auto intro: B_E_Suc converse_rtrancl_into_rtrancl)
[PROOF STATE]
proof (state)
this:
(i, j) \<in> B.acc

goal (1 subgoal):
 1. j \<le> i \<Longrightarrow> (i, j) \<in> B.acc
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j \<le> i \<Longrightarrow> (i, j) \<in> B.acc
[PROOF STEP]
assume "j \<le> i"
[PROOF STATE]
proof (state)
this:
j \<le> i

goal (1 subgoal):
 1. j \<le> i \<Longrightarrow> (i, j) \<in> B.acc
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j \<le> i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
j \<le> i

goal (1 subgoal):
 1. (i, j) \<in> B.acc
[PROOF STEP]
by (induct rule: dec_induct) (auto intro: B_E_Suc converse_rtrancl_into_rtrancl)
[PROOF STATE]
proof (state)
this:
(i, j) \<in> B.acc

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqvt:
  shows "eqvt (substClosed weakBisim)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt (substClosed weakBisim)
[PROOF STEP]
by(rule eqvtSubstClosed[OF Weak_Late_Bisim.eqvt])


[STATEMENT]
lemma OK_None_bot [iff]: "OK None \<sqsubseteq>\<^bsub>Err.le (le r)\<^esub> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK None \<sqsubseteq>\<^bsub>Err.le (Opt.le r)\<^esub> x
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK None \<sqsubseteq>\<^bsub>Err.le (Opt.le r)\<^esub> x
[PROOF STEP]
by (simp add: lesub_def Err.le_def le_def split: option.split err.split)


[STATEMENT]
lemma undefg_equiv: "(\<alpha>\<noteq>undefg) = (\<exists>g. \<alpha>=Agame g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<alpha> \<noteq> undefg) = (\<exists>g. \<alpha> = Agame g)
[PROOF STEP]
by simp


[STATEMENT]
lemma adjoint_funcs_skip: "SFuncs \<sigma> f=None \<Longrightarrow> Funcs (adjoint \<sigma> I \<omega>) f = Funcs I f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SFuncs \<sigma> f = undeft \<Longrightarrow> Funcs (USubst.adjoint \<sigma> I \<omega>) f = Funcs I f
[PROOF STEP]
using adjoint_funcs
[PROOF STATE]
proof (prove)
using this:
Funcs (USubst.adjoint ?\<sigma> ?I ?\<omega>) ?f = (case SFuncs ?\<sigma> ?f of None \<Rightarrow> Funcs ?I ?f | Some r \<Rightarrow> \<lambda>d. term_sem (repc ?I dotid d) r ?\<omega>)

goal (1 subgoal):
 1. SFuncs \<sigma> f = undeft \<Longrightarrow> Funcs (USubst.adjoint \<sigma> I \<omega>) f = Funcs I f
[PROOF STEP]
by auto


[STATEMENT]
lemma (in group) prime_order_simple:
  assumes prime:"prime (order G)"
  shows "simple_group G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_group G
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 1 < order G
 2. \<And>H. H \<lhd> G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
from prime
[PROOF STATE]
proof (chain)
picking this:
prime (order G)
[PROOF STEP]
show "1 < order G"
[PROOF STATE]
proof (prove)
using this:
prime (order G)

goal (1 subgoal):
 1. 1 < order G
[PROOF STEP]
unfolding prime_nat_iff
[PROOF STATE]
proof (prove)
using this:
1 < order G \<and> (\<forall>m. m dvd order G \<longrightarrow> m = 1 \<or> m = order G)

goal (1 subgoal):
 1. 1 < order G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 < order G

goal (1 subgoal):
 1. \<And>H. H \<lhd> G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>H. H \<lhd> G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
fix H
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>H. H \<lhd> G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
assume "H \<lhd> G"
[PROOF STATE]
proof (state)
this:
H \<lhd> G

goal (1 subgoal):
 1. \<And>H. H \<lhd> G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
hence HG:"subgroup H G"
[PROOF STATE]
proof (prove)
using this:
H \<lhd> G

goal (1 subgoal):
 1. subgroup H G
[PROOF STEP]
unfolding normal_def
[PROOF STATE]
proof (prove)
using this:
subgroup H G \<and> Group.group G \<and> normal_axioms H G

goal (1 subgoal):
 1. subgroup H G
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
subgroup H G

goal (1 subgoal):
 1. \<And>H. H \<lhd> G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
hence "card H dvd order G"
[PROOF STATE]
proof (prove)
using this:
subgroup H G

goal (1 subgoal):
 1. card H dvd order G
[PROOF STEP]
by (rule card_subgrp_dvd)
[PROOF STATE]
proof (state)
this:
card H dvd order G

goal (1 subgoal):
 1. \<And>H. H \<lhd> G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
with prime
[PROOF STATE]
proof (chain)
picking this:
prime (order G)
card H dvd order G
[PROOF STEP]
have "card H = 1 \<or> card H = order G"
[PROOF STATE]
proof (prove)
using this:
prime (order G)
card H dvd order G

goal (1 subgoal):
 1. card H = 1 \<or> card H = order G
[PROOF STEP]
unfolding prime_nat_iff
[PROOF STATE]
proof (prove)
using this:
1 < order G \<and> (\<forall>m. m dvd order G \<longrightarrow> m = 1 \<or> m = order G)
card H dvd order G

goal (1 subgoal):
 1. card H = 1 \<or> card H = order G
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card H = 1 \<or> card H = order G

goal (1 subgoal):
 1. \<And>H. H \<lhd> G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
thus "H = carrier G \<or> H = {\<one>}"
[PROOF STATE]
proof (prove)
using this:
card H = 1 \<or> card H = order G

goal (1 subgoal):
 1. H = carrier G \<or> H = {\<one>}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. card H = 1 \<Longrightarrow> H = carrier G \<or> H = {\<one>}
 2. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
assume "card H = 1"
[PROOF STATE]
proof (state)
this:
card H = 1

goal (2 subgoals):
 1. card H = 1 \<Longrightarrow> H = carrier G \<or> H = {\<one>}
 2. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card H = 1

goal (2 subgoals):
 1. card H = 1 \<Longrightarrow> H = carrier G \<or> H = {\<one>}
 2. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
from HG
[PROOF STATE]
proof (chain)
picking this:
subgroup H G
[PROOF STEP]
have "\<one> \<in> H"
[PROOF STATE]
proof (prove)
using this:
subgroup H G

goal (1 subgoal):
 1. \<one> \<in> H
[PROOF STEP]
by (metis subgroup.one_closed)
[PROOF STATE]
proof (state)
this:
\<one> \<in> H

goal (2 subgoals):
 1. card H = 1 \<Longrightarrow> H = carrier G \<or> H = {\<one>}
 2. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card H = 1
\<one> \<in> H
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card H = 1
\<one> \<in> H

goal (1 subgoal):
 1. H = carrier G \<or> H = {\<one>}
[PROOF STEP]
by (auto simp: card_Suc_eq)
[PROOF STATE]
proof (state)
this:
H = carrier G \<or> H = {\<one>}

goal (1 subgoal):
 1. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
assume "card H = order G"
[PROOF STATE]
proof (state)
this:
card H = order G

goal (1 subgoal):
 1. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card H = order G

goal (1 subgoal):
 1. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
from HG
[PROOF STATE]
proof (chain)
picking this:
subgroup H G
[PROOF STEP]
have "H \<subseteq> carrier G"
[PROOF STATE]
proof (prove)
using this:
subgroup H G

goal (1 subgoal):
 1. H \<subseteq> carrier G
[PROOF STEP]
unfolding subgroup_def
[PROOF STATE]
proof (prove)
using this:
(H \<subseteq> carrier G \<and> (\<forall>x y. x \<in> H \<longrightarrow> y \<in> H \<longrightarrow> x \<otimes> y \<in> H)) \<and> \<one> \<in> H \<and> (\<forall>x. x \<in> H \<longrightarrow> inv x \<in> H)

goal (1 subgoal):
 1. H \<subseteq> carrier G
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
H \<subseteq> carrier G

goal (1 subgoal):
 1. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
H \<subseteq> carrier G

goal (1 subgoal):
 1. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
from prime
[PROOF STATE]
proof (chain)
picking this:
prime (order G)
[PROOF STEP]
have "card (carrier G) > 1"
[PROOF STATE]
proof (prove)
using this:
prime (order G)

goal (1 subgoal):
 1. 1 < card (carrier G)
[PROOF STEP]
unfolding order_def prime_nat_iff
[PROOF STATE]
proof (prove)
using this:
1 < card (carrier G) \<and> (\<forall>m. m dvd card (carrier G) \<longrightarrow> m = 1 \<or> m = card (carrier G))

goal (1 subgoal):
 1. 1 < card (carrier G)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
1 < card (carrier G)

goal (1 subgoal):
 1. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
hence "finite (carrier G)"
[PROOF STATE]
proof (prove)
using this:
1 < card (carrier G)

goal (1 subgoal):
 1. finite (carrier G)
[PROOF STEP]
by (auto simp:card_ge_0_finite)
[PROOF STATE]
proof (state)
this:
finite (carrier G)

goal (1 subgoal):
 1. card H = order G \<Longrightarrow> H = carrier G \<or> H = {\<one>}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card H = order G
H \<subseteq> carrier G
finite (carrier G)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card H = order G
H \<subseteq> carrier G
finite (carrier G)

goal (1 subgoal):
 1. H = carrier G \<or> H = {\<one>}
[PROOF STEP]
unfolding order_def
[PROOF STATE]
proof (prove)
using this:
card H = card (carrier G)
H \<subseteq> carrier G
finite (carrier G)

goal (1 subgoal):
 1. H = carrier G \<or> H = {\<one>}
[PROOF STEP]
by (metis card_subset_eq)
[PROOF STATE]
proof (state)
this:
H = carrier G \<or> H = {\<one>}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
H = carrier G \<or> H = {\<one>}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma picard_lindeloef_sq_mtx_affine:
  assumes "continuous_on T A" and "continuous_on T B"
    and "t\<^sub>0 \<in> T" "is_interval T" "open T" and "open S"
  shows "picard_lindeloef (\<lambda>t s. A t *\<^sub>V s + B t) T S t\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. picard_lindeloef (\<lambda>t s. A t *\<^sub>V s + B t) T S t\<^sub>0
[PROOF STEP]
apply(unfold_locales, simp_all add: assms, clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. s \<in> S \<Longrightarrow> continuous_on T (\<lambda>t. A t *\<^sub>V s + B t)
 2. local_lipschitz T S (\<lambda>t s. A t *\<^sub>V s + B t)
[PROOF STEP]
using continuous_on_affine assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>continuous_on ?s ?A; continuous_on ?s ?g\<rbrakk> \<Longrightarrow> continuous_on ?s (\<lambda>x. ?A x *\<^sub>V ?sa + ?g x)
continuous_on T A
continuous_on T B
t\<^sub>0 \<in> T
is_interval T
open T
open S

goal (2 subgoals):
 1. \<And>s. s \<in> S \<Longrightarrow> continuous_on T (\<lambda>t. A t *\<^sub>V s + B t)
 2. local_lipschitz T S (\<lambda>t s. A t *\<^sub>V s + B t)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_lipschitz T S (\<lambda>t s. A t *\<^sub>V s + B t)
[PROOF STEP]
by (rule local_lipschitz_sq_mtx_affine, simp_all add: assms)


[STATEMENT]
lemma ss_exps_throw_Val:
 "\<lbrakk> val_of e = \<lfloor>a\<rfloor>; ss_exps (map Val vs @ throw e # es') = \<lfloor>e'\<rfloor> \<rbrakk>
   \<Longrightarrow> e' = throw e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>val_of e = \<lfloor>a\<rfloor>; ss_exps (map Val vs @ throw e # es') = \<lfloor>e'\<rfloor>\<rbrakk> \<Longrightarrow> e' = throw e
[PROOF STEP]
by(induct vs) (auto)


[STATEMENT]
lemma assumes mon_conv: "x\<up>(y::real)"
  and less: "z < y"
  shows real_mon_conv_outgrow: "\<exists>n. \<forall>m. n \<le> m \<longrightarrow> z < x m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
from less
[PROOF STATE]
proof (chain)
picking this:
z < y
[PROOF STEP]
have less': "0 < y-z"
[PROOF STATE]
proof (prove)
using this:
z < y

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

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
have "\<exists>n.\<forall>m. n \<le> m \<longrightarrow> \<bar>x m - y\<bar> < y - z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < y - z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < y - z
[PROOF STEP]
from mon_conv
[PROOF STATE]
proof (chain)
picking this:
x\<up>y
[PROOF STEP]
have aux: "\<And>r. r > 0 \<Longrightarrow> \<exists>n. \<forall>m. n \<le> m \<longrightarrow> \<bar>x m - y\<bar> < r"
[PROOF STATE]
proof (prove)
using this:
x\<up>y

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < r
[PROOF STEP]
unfolding mon_conv_real_def lim_sequentially dist_real_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>n. x n \<le> x (Suc n)) \<and> (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. \<bar>x n - y\<bar> < r)

goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < ?r \<Longrightarrow> \<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < ?r

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < y - z
[PROOF STEP]
with less'
[PROOF STATE]
proof (chain)
picking this:
0 < y - z
0 < ?r \<Longrightarrow> \<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < ?r
[PROOF STEP]
show "\<exists>n. \<forall>m. n \<le> m \<longrightarrow> \<bar>x m - y\<bar> < y - z"
[PROOF STATE]
proof (prove)
using this:
0 < y - z
0 < ?r \<Longrightarrow> \<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < ?r

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < y - z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < y - z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < y - z

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < y - z

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < y - z

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
from mon_conv
[PROOF STATE]
proof (chain)
picking this:
x\<up>y
[PROOF STEP]
have "x m \<le> y"
[PROOF STATE]
proof (prove)
using this:
x\<up>y

goal (1 subgoal):
 1. x m \<le> y
[PROOF STEP]
by (rule real_mon_conv_le)
[PROOF STATE]
proof (state)
this:
x m \<le> y

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
hence "\<bar>x m - y\<bar> = y - x m"
[PROOF STATE]
proof (prove)
using this:
x m \<le> y

goal (1 subgoal):
 1. \<bar>x m - y\<bar> = y - x m
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<bar>x m - y\<bar> = y - x m

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>x m - y\<bar> = y - x m

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
assume "\<bar>x m - y\<bar> < y - z"
[PROOF STATE]
proof (state)
this:
\<bar>x m - y\<bar> < y - z

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>x m - y\<bar> = y - x m
\<bar>x m - y\<bar> < y - z
[PROOF STEP]
have "z < x m"
[PROOF STATE]
proof (prove)
using this:
\<bar>x m - y\<bar> = y - x m
\<bar>x m - y\<bar> < y - z

goal (1 subgoal):
 1. z < x m
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
z < x m

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<bar>x ?m2 - y\<bar> < y - z \<Longrightarrow> z < x ?m2

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < y - z
\<bar>x ?m2 - y\<bar> < y - z \<Longrightarrow> z < x ?m2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>n. \<forall>m\<ge>n. \<bar>x m - y\<bar> < y - z
\<bar>x ?m2 - y\<bar> < y - z \<Longrightarrow> z < x ?m2

goal (1 subgoal):
 1. \<exists>n. \<forall>m\<ge>n. z < x m
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n. \<forall>m\<ge>n. z < x m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma curry_preserves_morphisms:
  assumes "f \<in> X \<Otimes>\<^sub>Q Y \<rightarrow>\<^sub>Q Z"
  shows "curry f \<in> X \<rightarrow>\<^sub>Q exp_qbs Y Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. curry f \<in> X \<rightarrow>\<^sub>Q Y \<Rightarrow>\<^sub>Q Z
[PROOF STEP]
by(rule qbs_morphismE(2)[OF curry_morphism,simplified,OF assms])


[STATEMENT]
lemma sngr_same_false[simp]:
  "p \<mapsto>\<^sub>r x * p \<mapsto>\<^sub>r y = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<mapsto>\<^sub>r x * p \<mapsto>\<^sub>r y = false
[PROOF STEP]
unfolding times_assn_def bot_assn_def sngr_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_assn (times_assn_raw (Rep_assn (Abs_assn (sngr_assn_raw p x))) (Rep_assn (Abs_assn (sngr_assn_raw p y)))) = Abs_assn (\<lambda>_. False)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. False = (h \<Turnstile> Abs_assn (times_assn_raw (Rep_assn (Abs_assn (sngr_assn_raw p x))) (Rep_assn (Abs_assn (sngr_assn_raw p y)))))
[PROOF STEP]
apply (auto simp: Abs_assn_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ent_pure_post_iff_sng[simp]:
  "(P \<Longrightarrow>\<^sub>A \<up>b) \<longleftrightarrow> ((\<forall>h. h\<Turnstile>P \<longrightarrow> b) \<and> (P \<Longrightarrow>\<^sub>A emp))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow>\<^sub>A \<up> b) = ((\<forall>h. h \<Turnstile> P \<longrightarrow> b) \<and> (P \<Longrightarrow>\<^sub>A emp))
[PROOF STEP]
using ent_pure_post_iff[where Q=emp]
[PROOF STATE]
proof (prove)
using this:
(?P \<Longrightarrow>\<^sub>A emp * \<up> ?b) = ((\<forall>h. h \<Turnstile> ?P \<longrightarrow> ?b) \<and> (?P \<Longrightarrow>\<^sub>A emp))

goal (1 subgoal):
 1. (P \<Longrightarrow>\<^sub>A \<up> b) = ((\<forall>h. h \<Turnstile> P \<longrightarrow> b) \<and> (P \<Longrightarrow>\<^sub>A emp))
[PROOF STEP]
by simp


[STATEMENT]
lemma widen_refT: "\<lbrakk> is_refT T; P \<turnstile> U \<le> T \<rbrakk> \<Longrightarrow> is_refT U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_refT T; P \<turnstile> U \<le> T\<rbrakk> \<Longrightarrow> is_refT U
[PROOF STEP]
by(erule refTE)(auto simp add: widen_Class widen_Array)


[STATEMENT]
lemma has_fields_fun:
  assumes "P \<turnstile> C has_fields FDTs" and "P \<turnstile> C has_fields FDTs'"
  shows "FDTs' = FDTs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FDTs' = FDTs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C has_fields FDTs
P \<turnstile> C has_fields FDTs'

goal (1 subgoal):
 1. FDTs' = FDTs
[PROOF STEP]
proof(induction arbitrary: FDTs')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C D fs ms FDTs FDTs' FDTs'a. \<lbrakk>class P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; P \<turnstile> D has_fields FDTs; \<And>FDTs'. P \<turnstile> D has_fields FDTs' \<Longrightarrow> FDTs' = FDTs; FDTs' = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ FDTs; P \<turnstile> C has_fields FDTs'a\<rbrakk> \<Longrightarrow> FDTs'a = FDTs'
 2. \<And>D fs ms FDTs FDTs'. \<lbrakk>class P Object = \<lfloor>(D, fs, ms)\<rfloor>; FDTs = map (\<lambda>(F, T). ((F, Object), T)) fs; P \<turnstile> Object has_fields FDTs'\<rbrakk> \<Longrightarrow> FDTs' = FDTs
[PROOF STEP]
case has_fields_Object
[PROOF STATE]
proof (state)
this:
class P Object = \<lfloor>(D_, fs_, ms_)\<rfloor>
FDTs_ = map (\<lambda>(F, T). ((F, Object), T)) fs_
P \<turnstile> Object has_fields FDTs'

goal (2 subgoals):
 1. \<And>C D fs ms FDTs FDTs' FDTs'a. \<lbrakk>class P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; P \<turnstile> D has_fields FDTs; \<And>FDTs'. P \<turnstile> D has_fields FDTs' \<Longrightarrow> FDTs' = FDTs; FDTs' = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ FDTs; P \<turnstile> C has_fields FDTs'a\<rbrakk> \<Longrightarrow> FDTs'a = FDTs'
 2. \<And>D fs ms FDTs FDTs'. \<lbrakk>class P Object = \<lfloor>(D, fs, ms)\<rfloor>; FDTs = map (\<lambda>(F, T). ((F, Object), T)) fs; P \<turnstile> Object has_fields FDTs'\<rbrakk> \<Longrightarrow> FDTs' = FDTs
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
class P Object = \<lfloor>(D_, fs_, ms_)\<rfloor>
FDTs_ = map (\<lambda>(F, T). ((F, Object), T)) fs_
P \<turnstile> Object has_fields FDTs'

goal (1 subgoal):
 1. FDTs' = FDTs_
[PROOF STEP]
by(auto elim: Fields.cases)
[PROOF STATE]
proof (state)
this:
FDTs' = FDTs_

goal (1 subgoal):
 1. \<And>C D fs ms FDTs FDTs' FDTs'a. \<lbrakk>class P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; P \<turnstile> D has_fields FDTs; \<And>FDTs'. P \<turnstile> D has_fields FDTs' \<Longrightarrow> FDTs' = FDTs; FDTs' = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ FDTs; P \<turnstile> C has_fields FDTs'a\<rbrakk> \<Longrightarrow> FDTs'a = FDTs'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C D fs ms FDTs FDTs' FDTs'a. \<lbrakk>class P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; P \<turnstile> D has_fields FDTs; \<And>FDTs'. P \<turnstile> D has_fields FDTs' \<Longrightarrow> FDTs' = FDTs; FDTs' = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ FDTs; P \<turnstile> C has_fields FDTs'a\<rbrakk> \<Longrightarrow> FDTs'a = FDTs'
[PROOF STEP]
case (has_fields_rec C D fs ms Dres Cres Cres')
[PROOF STATE]
proof (state)
this:
class P C = \<lfloor>(D, fs, ms)\<rfloor>
C \<noteq> Object
P \<turnstile> D has_fields Dres
Cres = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ Dres
P \<turnstile> D has_fields ?FDTs' \<Longrightarrow> ?FDTs' = Dres
P \<turnstile> C has_fields Cres'

goal (1 subgoal):
 1. \<And>C D fs ms FDTs FDTs' FDTs'a. \<lbrakk>class P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; P \<turnstile> D has_fields FDTs; \<And>FDTs'. P \<turnstile> D has_fields FDTs' \<Longrightarrow> FDTs' = FDTs; FDTs' = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ FDTs; P \<turnstile> C has_fields FDTs'a\<rbrakk> \<Longrightarrow> FDTs'a = FDTs'
[PROOF STEP]
from \<open>P \<turnstile> C has_fields Cres'\<close> \<open>C \<noteq> Object\<close> \<open>class P C = Some (D, fs, ms)\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> C has_fields Cres'
C \<noteq> Object
class P C = \<lfloor>(D, fs, ms)\<rfloor>
[PROOF STEP]
obtain Dres' where DFields': "P \<turnstile> D has_fields Dres'"
    and Cres': "Cres' = map (\<lambda>(F,Tm). ((F,C),Tm)) fs @ Dres'"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C has_fields Cres'
C \<noteq> Object
class P C = \<lfloor>(D, fs, ms)\<rfloor>

goal (1 subgoal):
 1. (\<And>Dres'. \<lbrakk>P \<turnstile> D has_fields Dres'; Cres' = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ Dres'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by cases auto
[PROOF STATE]
proof (state)
this:
P \<turnstile> D has_fields Dres'
Cres' = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ Dres'

goal (1 subgoal):
 1. \<And>C D fs ms FDTs FDTs' FDTs'a. \<lbrakk>class P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; P \<turnstile> D has_fields FDTs; \<And>FDTs'. P \<turnstile> D has_fields FDTs' \<Longrightarrow> FDTs' = FDTs; FDTs' = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ FDTs; P \<turnstile> C has_fields FDTs'a\<rbrakk> \<Longrightarrow> FDTs'a = FDTs'
[PROOF STEP]
from has_fields_rec.IH[OF DFields'] \<open>Cres = map (\<lambda>(F,Tm). ((F,C),Tm)) fs @ Dres\<close> Cres'
[PROOF STATE]
proof (chain)
picking this:
Dres' = Dres
Cres = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ Dres
Cres' = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ Dres'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Dres' = Dres
Cres = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ Dres
Cres' = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ Dres'

goal (1 subgoal):
 1. Cres' = Cres
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Cres' = Cres

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma widen_i_i_i_code [code]:
  "widen_i_i_i P T T' = (if P \<turnstile> T \<le> T' then Predicate.single () else bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. widen_i_i_i P T T' = (if P \<turnstile> T \<le> T' then Predicate.single () else bot)
[PROOF STEP]
by(auto intro!: pred_eqI intro: widen_i_i_iI elim: widen_i_i_iE)


[STATEMENT]
lemma "\<lbrakk>\<^bold>\<not> F\<triangleright> \<Gamma> \<turnstile> H; G\<triangleright> \<Gamma> \<turnstile> H\<rbrakk> \<Longrightarrow> F \<^bold>\<rightarrow> G\<triangleright> \<Gamma> \<turnstile> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<^bold>\<not> F \<triangleright> \<Gamma> \<turnstile> H; G \<triangleright> \<Gamma> \<turnstile> H\<rbrakk> \<Longrightarrow> F \<^bold>\<rightarrow> G \<triangleright> \<Gamma> \<turnstile> H
[PROOF STEP]
apply(rule ND_caseDistinction[of F])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<^bold>\<not> F \<triangleright> \<Gamma> \<turnstile> H; G \<triangleright> \<Gamma> \<turnstile> H\<rbrakk> \<Longrightarrow> F \<triangleright> F \<^bold>\<rightarrow> G \<triangleright> \<Gamma> \<turnstile> H
 2. \<lbrakk>\<^bold>\<not> F \<triangleright> \<Gamma> \<turnstile> H; G \<triangleright> \<Gamma> \<turnstile> H\<rbrakk> \<Longrightarrow> \<^bold>\<not> F \<triangleright> F \<^bold>\<rightarrow> G \<triangleright> \<Gamma> \<turnstile> H
[PROOF STEP]
apply (meson ImpE ImpI ND.intros(1) Weaken insertI1 subset_insertI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<^bold>\<not> F \<triangleright> \<Gamma> \<turnstile> H; G \<triangleright> \<Gamma> \<turnstile> H\<rbrakk> \<Longrightarrow> \<^bold>\<not> F \<triangleright> F \<^bold>\<rightarrow> G \<triangleright> \<Gamma> \<turnstile> H
[PROOF STEP]
apply (metis Weaken insert_commute subset_insertI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma aext_imp [alpha]: "(P \<Rightarrow> Q) \<oplus>\<^sub>p x = (P \<oplus>\<^sub>p x \<Rightarrow> Q \<oplus>\<^sub>p x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<Rightarrow> Q) \<oplus>\<^sub>p x = (P \<oplus>\<^sub>p x \<Rightarrow> Q \<oplus>\<^sub>p x)
[PROOF STEP]
by (pred_auto)


[STATEMENT]
lemma reduce_alist_code [code, code_unfold]:
  "reduce (AList_Mapping.Mapping xs) t = reduce_alist xs t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduce (AList_Mapping.Mapping xs) t = reduce_alist xs t
[PROOF STEP]
by (induction t arbitrary: xs)
     (auto simp: AList_Mapping_update split: option.split)


[STATEMENT]
lemma HaddP_SUCC_Ex1:
  assumes "atom i \<sharp> (x,y,z)"
    shows "insert (HaddP (SUCC x) y z) (insert (OrdP x) H)
           \<turnstile> Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (HaddP (SUCC x) y z) (insert (OrdP x) H) \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insert (HaddP (SUCC x) y z) (insert (OrdP x) H) \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))
[PROOF STEP]
have "{ HaddP (SUCC x) y z, OrdP x } \<turnstile> Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {HaddP (SUCC x) y z, OrdP x} \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))
[PROOF STEP]
apply (rule cut_same [OF HaddP_commute [THEN cut2]])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. {HaddP (SUCC x) y z, OrdP x} \<turnstile> HaddP ?x2 ?y2 ?z2
 2. {HaddP (SUCC x) y z, OrdP x} \<turnstile> OrdP ?x2
 3. {HaddP ?y2 ?x2 ?z2, HaddP (SUCC x) y z, OrdP x} \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))
[PROOF STEP]
apply (blast intro: OrdP_SUCC_I)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {HaddP y (SUCC x) z, HaddP (SUCC x) y z, OrdP x} \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))
[PROOF STEP]
apply (rule cut_same [OF HaddP_SUCC_Ex2 [where z'=i]], blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. atom i \<sharp> (y, x, z)
 2. {SyntaxN.Ex i (HaddP y x (Var i) AND z EQ SUCC (Var i)), HaddP y (SUCC x) z, HaddP (SUCC x) y z, OrdP x} \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
atom i \<sharp> (x, y, z)

goal (2 subgoals):
 1. atom i \<sharp> (y, x, z)
 2. {SyntaxN.Ex i (HaddP y x (Var i) AND z EQ SUCC (Var i)), HaddP y (SUCC x) z, HaddP (SUCC x) y z, OrdP x} \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom i \<sharp> (x, y, z) \<Longrightarrow> {HaddP y x (Var i), z EQ SUCC (Var i), HaddP y (SUCC x) z, HaddP (SUCC x) y z, OrdP x} \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))
[PROOF STEP]
apply (auto intro!: Ex_I [where x="Var i"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom i \<sharp> (x, y, z) \<Longrightarrow> {HaddP y x (Var i), z EQ SUCC (Var i), HaddP y (SUCC x) z, HaddP (SUCC x) y z, OrdP x} \<turnstile> HaddP x y (Var i)
[PROOF STEP]
by (metis AssumeH(2) HaddP_commute [THEN cut2] HaddP_imp_OrdP rotate2 thin1)
[PROOF STATE]
proof (state)
this:
{HaddP (SUCC x) y z, OrdP x} \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))

goal (1 subgoal):
 1. insert (HaddP (SUCC x) y z) (insert (OrdP x) H) \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{HaddP (SUCC x) y z, OrdP x} \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))

goal (1 subgoal):
 1. insert (HaddP (SUCC x) y z) (insert (OrdP x) H) \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))
[PROOF STEP]
by (metis Assume AssumeH(2) cut2)
[PROOF STATE]
proof (state)
this:
insert (HaddP (SUCC x) y z) (insert (OrdP x) H) \<turnstile> SyntaxN.Ex i (HaddP x y (Var i) AND z EQ SUCC (Var i))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma index_1_imp_mult_1:
  assumes "\<Lambda> = 1"
  assumes "bl \<in># \<B>"
  assumes "card bl \<ge> 2"
  shows "multiplicity bl = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity bl = 1
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. multiplicity bl \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (multiplicity bl = 1)"
[PROOF STATE]
proof (state)
this:
multiplicity bl \<noteq> 1

goal (1 subgoal):
 1. multiplicity bl \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
multiplicity bl \<noteq> 1
[PROOF STEP]
have "multiplicity bl \<noteq> 1" and "multiplicity bl \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
multiplicity bl \<noteq> 1

goal (1 subgoal):
 1. multiplicity bl \<noteq> 1 &&& multiplicity bl \<noteq> 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
multiplicity bl \<noteq> 1
\<Lambda> = 1
bl \<in># \<B>
2 \<le> card bl

goal (1 subgoal):
 1. multiplicity bl \<noteq> 1 &&& multiplicity bl \<noteq> 0
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
multiplicity bl \<noteq> 1
multiplicity bl \<noteq> 0

goal (1 subgoal):
 1. multiplicity bl \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
multiplicity bl \<noteq> 1
multiplicity bl \<noteq> 0
[PROOF STEP]
have m: "multiplicity bl \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
multiplicity bl \<noteq> 1
multiplicity bl \<noteq> 0

goal (1 subgoal):
 1. 2 \<le> multiplicity bl
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
2 \<le> multiplicity bl

goal (1 subgoal):
 1. multiplicity bl \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
obtain ps where ps: "ps \<subseteq> bl \<and> card ps = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ps. ps \<subseteq> bl \<and> card ps = 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using nat_int_comparison(3) obtain_subset_with_card_n
[PROOF STATE]
proof (prove)
using this:
(?a \<le> ?b) = (int ?a \<le> int ?b)
\<lbrakk>?n \<le> card ?S; \<And>T. \<lbrakk>T \<subseteq> ?S; card T = ?n; finite T\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>ps. ps \<subseteq> bl \<and> card ps = 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis assms(3))
[PROOF STATE]
proof (state)
this:
ps \<subseteq> bl \<and> card ps = 2

goal (1 subgoal):
 1. multiplicity bl \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ps \<subseteq> bl \<and> card ps = 2
[PROOF STEP]
have "\<B> index ps \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
ps \<subseteq> bl \<and> card ps = 2

goal (1 subgoal):
 1. 2 \<le> \<B> index ps
[PROOF STEP]
using m points_index_count_min ps
[PROOF STATE]
proof (prove)
using this:
ps \<subseteq> bl \<and> card ps = 2
2 \<le> multiplicity bl
\<lbrakk>?n \<le> multiplicity ?bl; ?ps \<subseteq> ?bl\<rbrakk> \<Longrightarrow> ?n \<le> \<B> index ?ps
ps \<subseteq> bl \<and> card ps = 2

goal (1 subgoal):
 1. 2 \<le> \<B> index ps
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
2 \<le> \<B> index ps

goal (1 subgoal):
 1. multiplicity bl \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 \<le> \<B> index ps
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
2 \<le> \<B> index ps

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms index_distinct ps antisym_conv2 not_numeral_less_zero
      numeral_le_one_iff points_index_ps_nin semiring_norm(69) zero_neq_numeral
[PROOF STATE]
proof (prove)
using this:
2 \<le> \<B> index ps
\<Lambda> = 1
bl \<in># \<B>
2 \<le> card bl
\<lbrakk>?G1.0 \<in> \<G>; ?G2.0 \<in> \<G>; ?G1.0 \<noteq> ?G2.0; ?x \<in> ?G1.0; ?y \<in> ?G2.0\<rbrakk> \<Longrightarrow> int (\<B> index {?x, ?y}) = \<Lambda>
ps \<subseteq> bl \<and> card ps = 2
?x \<le> ?y \<Longrightarrow> (\<not> ?x < ?y) = (?x = ?y)
\<not> numeral ?n < (0::?'a)
(numeral ?n \<le> (1::?'a)) = (?n \<le> num.One)
\<not> ?ps \<subseteq> \<V> \<Longrightarrow> \<B> index ?ps = 0
(num.Bit0 ?m \<le> num.One) = False
(0::?'a) \<noteq> numeral ?n

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis gdd_index_options int_int_eq int_ops(2))
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma idiv_by_0: "(a::enat) div 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a div 0 = 0
[PROOF STEP]
unfolding div_enat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case a of enat x \<Rightarrow> case 0 of enat y \<Rightarrow> enat (x div y) | \<infinity> \<Rightarrow> 0 | \<infinity> \<Rightarrow> case 0 of enat 0 \<Rightarrow> 0 | enat (Suc n) \<Rightarrow> \<infinity> | \<infinity> \<Rightarrow> \<infinity>) = 0
[PROOF STEP]
by (case_tac a, simp_all)


[STATEMENT]
lemma opt_mru_guard_imp_Quorum:
  "opt_mru_guard vs Q v \<Longrightarrow> Q \<in> Quorum"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. opt_mru_guard vs Q v \<Longrightarrow> Q \<in> Quorum
[PROOF STEP]
by (simp add: opt_mru_guard_def Let_def)


[STATEMENT]
lemma either_contains_arg2: "paths t' \<subseteq> paths (t \<oplus>\<oplus> t')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paths t' \<subseteq> paths (t \<oplus>\<oplus> t')
[PROOF STEP]
by transfer fastforce


[STATEMENT]
lemma ttree_restr_possible2: "possible (ttree_restr S t') x \<Longrightarrow> x \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. possible (ttree_restr S t') x \<Longrightarrow> x \<in> S
[PROOF STEP]
by transfer (auto, metis filter_eq_Cons_iff)


[STATEMENT]
lemma splitAtRec_notRam:
 "\<And> us. ram \<notin>  set vs \<Longrightarrow> splitAtRec ram us vs = (us @ vs, [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>us. ram \<notin> set vs \<Longrightarrow> splitAtRec ram us vs = (us @ vs, [])
[PROOF STEP]
proof (induct vs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>us. ram \<notin> set [] \<Longrightarrow> splitAtRec ram us [] = (us @ [], [])
 2. \<And>a vs us. \<lbrakk>\<And>us. ram \<notin> set vs \<Longrightarrow> splitAtRec ram us vs = (us @ vs, []); ram \<notin> set (a # vs)\<rbrakk> \<Longrightarrow> splitAtRec ram us (a # vs) = (us @ a # vs, [])
[PROOF STEP]
case  Nil
[PROOF STATE]
proof (state)
this:
ram \<notin> set []

goal (2 subgoals):
 1. \<And>us. ram \<notin> set [] \<Longrightarrow> splitAtRec ram us [] = (us @ [], [])
 2. \<And>a vs us. \<lbrakk>\<And>us. ram \<notin> set vs \<Longrightarrow> splitAtRec ram us vs = (us @ vs, []); ram \<notin> set (a # vs)\<rbrakk> \<Longrightarrow> splitAtRec ram us (a # vs) = (us @ a # vs, [])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ram \<notin> set []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ram \<notin> set []

goal (1 subgoal):
 1. splitAtRec ram us [] = (us @ [], [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
splitAtRec ram us [] = (us @ [], [])

goal (1 subgoal):
 1. \<And>a vs us. \<lbrakk>\<And>us. ram \<notin> set vs \<Longrightarrow> splitAtRec ram us vs = (us @ vs, []); ram \<notin> set (a # vs)\<rbrakk> \<Longrightarrow> splitAtRec ram us (a # vs) = (us @ a # vs, [])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a vs us. \<lbrakk>\<And>us. ram \<notin> set vs \<Longrightarrow> splitAtRec ram us vs = (us @ vs, []); ram \<notin> set (a # vs)\<rbrakk> \<Longrightarrow> splitAtRec ram us (a # vs) = (us @ a # vs, [])
[PROOF STEP]
case (Cons v vs)
[PROOF STATE]
proof (state)
this:
ram \<notin> set vs \<Longrightarrow> splitAtRec ram ?us vs = (?us @ vs, [])
ram \<notin> set (v # vs)

goal (1 subgoal):
 1. \<And>a vs us. \<lbrakk>\<And>us. ram \<notin> set vs \<Longrightarrow> splitAtRec ram us vs = (us @ vs, []); ram \<notin> set (a # vs)\<rbrakk> \<Longrightarrow> splitAtRec ram us (a # vs) = (us @ a # vs, [])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ram \<notin> set vs \<Longrightarrow> splitAtRec ram ?us vs = (?us @ vs, [])
ram \<notin> set (v # vs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ram \<notin> set vs \<Longrightarrow> splitAtRec ram ?us vs = (?us @ vs, [])
ram \<notin> set (v # vs)

goal (1 subgoal):
 1. splitAtRec ram us (v # vs) = (us @ v # vs, [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
splitAtRec ram us (v # vs) = (us @ v # vs, [])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma DynCastRedsNull:
  "P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>null,s'\<rangle> \<Longrightarrow> P,E \<turnstile> \<langle>Cast C e,s\<rangle> \<rightarrow>* \<langle>null,s'\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>null,s'\<rangle> \<Longrightarrow> P,E \<turnstile> \<langle>Cast C e,s\<rangle> \<rightarrow>* \<langle>null,s'\<rangle>
[PROOF STEP]
apply(rule rtrancl_into_rtrancl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>null,s'\<rangle> \<Longrightarrow> ((Cast C e, s), ?b) \<in> (Red P E)\<^sup>*
 2. P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>null,s'\<rangle> \<Longrightarrow> (?b, null, s') \<in> Red P E
[PROOF STEP]
apply(erule DynCastReds)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>null,s'\<rangle> \<Longrightarrow> ((Cast C null, s'), null, s') \<in> Red P E
[PROOF STEP]
apply(simp add:RedDynCastNull)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma atMost_Int_atLeast: "{..\<le>\<^sub>an} \<inter> {n\<le>\<^sub>a..} = {n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {..\<le>\<^sub>an} \<inter> {n\<le>\<^sub>a..} = {n}
[PROOF STEP]
unfolding ray_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> UNIV. x \<le>\<^sub>a n} \<inter> {x \<in> UNIV. n \<le>\<^sub>a x} = {n}
[PROOF STEP]
by (auto simp: eq_iff)


[STATEMENT]
lemma TSnopaid: "(snd (fst (snd (rTS initH) is q))) = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (fst (snd (rTS initH) is q)) = []
[PROOF STEP]
unfolding rTS_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (fst (snd (\<lambda>s. initH, TS_step_d) is q)) = []
[PROOF STEP]
by(simp add: TS_step_d_def)


[STATEMENT]
theorem closure_sound_complete:
assumes result: "closure as (r,s) = Some(ws,R)"
and atoms: "set as = atoms r \<union> atoms s"
shows "ws = [] \<longleftrightarrow> lang r = lang s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ws = []) = (lang r = lang s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (ws = []) = (lang r = lang s)
[PROOF STEP]
have leq: "(lang r = lang s) =
  (\<forall>(r',s') \<in> {((r0,s0),(nderiv a r0,nderiv a s0))| r0 s0 a. a : set as}^* `` {(r,s)}.
    nullable r' = nullable s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lang r = lang s) = (\<forall>(r', s')\<in>{((r0, s0), nderiv a r0, nderiv a s0) |r0 s0 a. a \<in> set as}\<^sup>* `` {(r, s)}. nullable r' = nullable s')
[PROOF STEP]
by(simp add: atoms rtrancl_nderiv_nderivs Ball_def lang_eq_ext imp_ex nullable_nderivs
         del:Un_iff)
[PROOF STATE]
proof (state)
this:
(lang r = lang s) = (\<forall>(r', s')\<in>{((r0, s0), nderiv a r0, nderiv a s0) |r0 s0 a. a \<in> set as}\<^sup>* `` {(r, s)}. nullable r' = nullable s')

goal (1 subgoal):
 1. (ws = []) = (lang r = lang s)
[PROOF STEP]
have "{(x,y). y \<in> set ((\<lambda>(p,q). map (\<lambda>a. (nderiv a p, nderiv a q)) as) x)} =
    {((r,s), nderiv a r, nderiv a s) |r s a. a \<in> set as}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). y \<in> set (case x of (p, q) \<Rightarrow> map (\<lambda>a. (nderiv a p, nderiv a q)) as)} = {((r, s), nderiv a r, nderiv a s) |r s a. a \<in> set as}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(x, y). y \<in> set (case x of (p, q) \<Rightarrow> map (\<lambda>a. (nderiv a p, nderiv a q)) as)} = {((r, s), nderiv a r, nderiv a s) |r s a. a \<in> set as}

goal (1 subgoal):
 1. (ws = []) = (lang r = lang s)
[PROOF STEP]
with atoms rtrancl_while_Some[OF result[unfolded closure_def]]
[PROOF STATE]
proof (chain)
picking this:
set as = atoms r \<union> atoms s
if ws = [] then R = {(x, y). y \<in> set (case x of (r, s) \<Rightarrow> map (\<lambda>a. (nderiv a r, nderiv a s)) as)}\<^sup>* `` {(r, s)} \<and> (\<forall>z\<in>R. case z of (r, s) \<Rightarrow> nullable r = nullable s) else \<not> (case hd ws of (r, s) \<Rightarrow> nullable r = nullable s) \<and> hd ws \<in> {(x, y). y \<in> set (case x of (r, s) \<Rightarrow> map (\<lambda>a. (nderiv a r, nderiv a s)) as)}\<^sup>* `` {(r, s)}
{(x, y). y \<in> set (case x of (p, q) \<Rightarrow> map (\<lambda>a. (nderiv a p, nderiv a q)) as)} = {((r, s), nderiv a r, nderiv a s) |r s a. a \<in> set as}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set as = atoms r \<union> atoms s
if ws = [] then R = {(x, y). y \<in> set (case x of (r, s) \<Rightarrow> map (\<lambda>a. (nderiv a r, nderiv a s)) as)}\<^sup>* `` {(r, s)} \<and> (\<forall>z\<in>R. case z of (r, s) \<Rightarrow> nullable r = nullable s) else \<not> (case hd ws of (r, s) \<Rightarrow> nullable r = nullable s) \<and> hd ws \<in> {(x, y). y \<in> set (case x of (r, s) \<Rightarrow> map (\<lambda>a. (nderiv a r, nderiv a s)) as)}\<^sup>* `` {(r, s)}
{(x, y). y \<in> set (case x of (p, q) \<Rightarrow> map (\<lambda>a. (nderiv a p, nderiv a q)) as)} = {((r, s), nderiv a r, nderiv a s) |r s a. a \<in> set as}

goal (1 subgoal):
 1. (ws = []) = (lang r = lang s)
[PROOF STEP]
by (auto simp add: leq Ball_def split: if_splits)
[PROOF STATE]
proof (state)
this:
(ws = []) = (lang r = lang s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma directional_derivative_add[simp]: "directional_derivative k a (x + y) = directional_derivative k a x + directional_derivative k a y"
  and directional_derivative_scaleR[simp]: "directional_derivative k a (c *\<^sub>R x) = c *\<^sub>R directional_derivative k a x"
  if "k \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. directional_derivative k a (x + y) = directional_derivative k a x + directional_derivative k a y &&& directional_derivative k a (c *\<^sub>R x) = c *\<^sub>R directional_derivative k a x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0

goal (1 subgoal):
 1. directional_derivative k a (x + y) = directional_derivative k a x + directional_derivative k a y &&& directional_derivative k a (c *\<^sub>R x) = c *\<^sub>R directional_derivative k a x
[PROOF STEP]
by (auto simp: directional_derivative_def restrict0_def[abs_def] fun_eq_iff
      differentiable_on_def linear_iff that
      dest!: linear_frechet_derivative spec[where x=a] smooth_on_imp_differentiable_on)


[STATEMENT]
lemma sup_less_eq_cases_3:
  "-y \<squnion> -x \<le> -z \<squnion> -x \<Longrightarrow> -y \<squnion> --x \<le> -z \<squnion> --x \<Longrightarrow> -y \<le> -z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>- y \<squnion> - x \<le> - z \<squnion> - x; - y \<squnion> - - x \<le> - z \<squnion> - - x\<rbrakk> \<Longrightarrow> - y \<le> - z
[PROOF STEP]
by (simp add: sup_less_eq_cases_2 sub_commutative)


[STATEMENT]
lemma varMonotone_byFIX: "Monotone (\<lambda> \<Phi> . (\<lambda> (s,t,\<beta>) .(b,\<Phi>,\<beta>,s,t):var))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Monotone (\<lambda>\<Phi> (s, t, \<beta>). (b, \<Phi>, \<beta>, s, t) \<in> var)
[PROOF STEP]
apply (subgoal_tac "Monotone (\<lambda> \<Phi> . PhiWhile b \<Phi>)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Monotone (PhiWhile b) \<Longrightarrow> Monotone (\<lambda>\<Phi> (s, t, \<beta>). (b, \<Phi>, \<beta>, s, t) \<in> var)
 2. Monotone (PhiWhile b)
[PROOF STEP]
apply (simp add: FIXvarFIX)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Monotone (PhiWhile b)
[PROOF STEP]
apply (rule PhiWhileMonotone)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma IfHigh:
 "\<lbrakk> G \<rhd> c: HighSec; G \<rhd> d:HighSec\<rbrakk> \<Longrightarrow> G \<rhd> Iff b c d: HighSec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G \<rhd> c : HighSec; G \<rhd> d : HighSec\<rbrakk> \<Longrightarrow> G \<rhd> Iff b c d : HighSec
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G \<rhd> c : HighSec; G \<rhd> d : HighSec\<rbrakk> \<Longrightarrow> G \<rhd> Iff b c d : HighSec
[PROOF STEP]
apply (rule VDMConseq, rule VDMIff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>G \<rhd> c : HighSec; G \<rhd> d : HighSec\<rbrakk> \<Longrightarrow> G \<rhd> c : ?A3
 2. \<lbrakk>G \<rhd> c : HighSec; G \<rhd> d : HighSec\<rbrakk> \<Longrightarrow> G \<rhd> d : ?B3
 3. \<lbrakk>G \<rhd> c : HighSec; G \<rhd> d : HighSec\<rbrakk> \<Longrightarrow> \<forall>s t. (evalB b (fst s) \<longrightarrow> ?A3 s t) \<and> (\<not> evalB b (fst s) \<longrightarrow> ?B3 s t) \<longrightarrow> HighSec s t
[PROOF STEP]
apply (assumption, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G \<rhd> c : HighSec; G \<rhd> d : HighSec\<rbrakk> \<Longrightarrow> \<forall>s t. (evalB b (fst s) \<longrightarrow> HighSec s t) \<and> (\<not> evalB b (fst s) \<longrightarrow> HighSec s t) \<longrightarrow> HighSec s t
[PROOF STEP]
apply (erule thin_rl, erule thin_rl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s t. (evalB b (fst s) \<longrightarrow> HighSec s t) \<and> (\<not> evalB b (fst s) \<longrightarrow> HighSec s t) \<longrightarrow> HighSec s t
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma \<pi>_subset_elem_trans:
  assumes Y: "Y \<subseteq> \<pi> k T X"
  assumes z: "z \<in> \<pi> k T Y"
  shows "z \<in>  \<pi> k T X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> \<pi> k T X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<in> \<pi> k T X
[PROOF STEP]
from Y
[PROOF STATE]
proof (chain)
picking this:
Y \<subseteq> \<pi> k T X
[PROOF STEP]
have "\<pi> k T Y \<subseteq> \<pi> k T (\<pi> k T X)"
[PROOF STATE]
proof (prove)
using this:
Y \<subseteq> \<pi> k T X

goal (1 subgoal):
 1. \<pi> k T Y \<subseteq> \<pi> k T (\<pi> k T X)
[PROOF STEP]
by (simp add: monoD mono_\<pi>)
[PROOF STATE]
proof (state)
this:
\<pi> k T Y \<subseteq> \<pi> k T (\<pi> k T X)

goal (1 subgoal):
 1. z \<in> \<pi> k T X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<pi> k T Y \<subseteq> \<pi> k T (\<pi> k T X)
[PROOF STEP]
have "\<pi> k T Y \<subseteq> \<pi> k T X"
[PROOF STATE]
proof (prove)
using this:
\<pi> k T Y \<subseteq> \<pi> k T (\<pi> k T X)

goal (1 subgoal):
 1. \<pi> k T Y \<subseteq> \<pi> k T X
[PROOF STEP]
using \<pi>_idempotent
[PROOF STATE]
proof (prove)
using this:
\<pi> k T Y \<subseteq> \<pi> k T (\<pi> k T X)
\<pi> ?k ?T (\<pi> ?k ?T ?I) = \<pi> ?k ?T ?I

goal (1 subgoal):
 1. \<pi> k T Y \<subseteq> \<pi> k T X
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<pi> k T Y \<subseteq> \<pi> k T X

goal (1 subgoal):
 1. z \<in> \<pi> k T X
[PROOF STEP]
with z
[PROOF STATE]
proof (chain)
picking this:
z \<in> \<pi> k T Y
\<pi> k T Y \<subseteq> \<pi> k T X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
z \<in> \<pi> k T Y
\<pi> k T Y \<subseteq> \<pi> k T X

goal (1 subgoal):
 1. z \<in> \<pi> k T X
[PROOF STEP]
using contra_subsetD
[PROOF STATE]
proof (prove)
using this:
z \<in> \<pi> k T Y
\<pi> k T Y \<subseteq> \<pi> k T X
\<lbrakk>?A \<subseteq> ?B; ?c \<notin> ?B\<rbrakk> \<Longrightarrow> ?c \<notin> ?A

goal (1 subgoal):
 1. z \<in> \<pi> k T X
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z \<in> \<pi> k T X

goal:
No subgoals!
[PROOF STEP]
qed


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

  assumes "P \<approx> Q"

  shows "<\<nu>x>P \<approx> <\<nu>x>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<nu>x>P \<approx> <\<nu>x>Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. <\<nu>x>P \<approx> <\<nu>x>Q
[PROOF STEP]
let ?X = "{(<\<nu>x>P, <\<nu>x>Q) | x P Q. P \<approx> Q}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. <\<nu>x>P \<approx> <\<nu>x>Q
[PROOF STEP]
from \<open>P \<approx> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<approx> Q
[PROOF STEP]
have "(<\<nu>x>P, <\<nu>x>Q) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
P \<approx> Q

goal (1 subgoal):
 1. (<\<nu>x>P, <\<nu>x>Q) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(<\<nu>x>P, <\<nu>x>Q) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}

goal (1 subgoal):
 1. <\<nu>x>P \<approx> <\<nu>x>Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(<\<nu>x>P, <\<nu>x>Q) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}

goal (1 subgoal):
 1. <\<nu>x>P \<approx> <\<nu>x>Q
[PROOF STEP]
proof(coinduct rule: weakBisimCoinduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
case(cSim xP xQ)
[PROOF STATE]
proof (state)
this:
(xP, xQ) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(xP, xQ) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
fix P Q x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
assume "P \<approx> Q"
[PROOF STATE]
proof (state)
this:
P \<approx> Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
hence "P \<leadsto><weakBisim> Q"
[PROOF STATE]
proof (prove)
using this:
P \<approx> Q

goal (1 subgoal):
 1. P \<leadsto><weakBisim> Q
[PROOF STEP]
by(rule weakBisimE)
[PROOF STATE]
proof (state)
this:
P \<leadsto><weakBisim> Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<leadsto><weakBisim> Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
have "\<And>P Q x. P \<approx> Q \<Longrightarrow> (<\<nu>x>P, <\<nu>x>Q) \<in> ?X \<union> weakBisim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P Q x. P \<approx> Q \<Longrightarrow> (<\<nu>x>P, <\<nu>x>Q) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?P \<approx> ?Q \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?P \<approx> ?Q \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
have "weakBisim \<subseteq> ?X \<union> weakBisim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weakBisim \<subseteq> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
weakBisim \<subseteq> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
weakBisim \<subseteq> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
have "eqvt weakBisim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt weakBisim
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eqvt weakBisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eqvt weakBisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
have "eqvt (?X \<union> weakBisim)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt ({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)
[PROOF STEP]
by(auto simp add: eqvt_def dest: Weak_Early_Bisim.eqvtI)+
[PROOF STATE]
proof (state)
this:
eqvt ({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto><weakBisim> Q
?P \<approx> ?Q \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim
weakBisim \<subseteq> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim
eqvt weakBisim
eqvt ({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)
[PROOF STEP]
have "<\<nu>x>P \<leadsto><(?X \<union> weakBisim)> <\<nu>x>Q"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto><weakBisim> Q
?P \<approx> ?Q \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim
weakBisim \<subseteq> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim
eqvt weakBisim
eqvt ({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)

goal (1 subgoal):
 1. <\<nu>x>P \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> <\<nu>x>Q
[PROOF STEP]
by(rule Weak_Early_Sim_Pres.resPres)
[PROOF STATE]
proof (state)
this:
<\<nu>x>P \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> <\<nu>x>Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?Pa2 \<approx> ?Qa2 \<Longrightarrow> <\<nu>?xa2>?Pa2 \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> <\<nu>?xa2>?Qa2

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> R \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> S
 2. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
with \<open>(xP, xQ) \<in> ?X\<close>
[PROOF STATE]
proof (chain)
picking this:
(xP, xQ) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
?Pa2 \<approx> ?Qa2 \<Longrightarrow> <\<nu>?xa2>?Pa2 \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> <\<nu>?xa2>?Qa2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(xP, xQ) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
?Pa2 \<approx> ?Qa2 \<Longrightarrow> <\<nu>?xa2>?Pa2 \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> <\<nu>?xa2>?Qa2

goal (1 subgoal):
 1. xP \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> xQ
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xP \<leadsto><({(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<union> weakBisim)> xQ

goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
case(cSym xP xQ)
[PROOF STATE]
proof (state)
this:
(xP, xQ) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}

goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q} \<Longrightarrow> (S, R) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(xP, xQ) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}

goal (1 subgoal):
 1. (xQ, xP) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}
[PROOF STEP]
by(blast dest: Weak_Early_Bisim.symetric)
[PROOF STATE]
proof (state)
this:
(xQ, xP) \<in> {(<\<nu>x>P, <\<nu>x>Q) |x P Q. P \<approx> Q}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
<\<nu>x>P \<approx> <\<nu>x>Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma order_impl_root_order: "\<lbrakk>k > 0; order k t\<rbrakk> \<Longrightarrow> root_order k t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; order k t\<rbrakk> \<Longrightarrow> root_order k t
[PROOF STEP]
apply(cases t)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>0 < k; order k t; t = Leaf x1\<rbrakk> \<Longrightarrow> root_order k t
 2. \<And>x21 x22. \<lbrakk>0 < k; order k t; t = Node x21 x22\<rbrakk> \<Longrightarrow> root_order k t
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma coprime_inv_hom[simp]: "coprime (Hilbert_Choice.inv hom x') y \<longleftrightarrow> coprime x' (hom y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime (inv hom x') y = coprime x' (hom y)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. coprime (inv hom x') y = coprime x' (hom y)
[PROOF STEP]
interpret inv: comm_monoid_mult_isom "Hilbert_Choice.inv hom"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comm_monoid_mult_isom (inv hom)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. coprime (inv hom x') y = coprime x' (hom y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime (inv hom x') y = coprime x' (hom y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coprime (inv hom x') y = coprime x' (hom y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ht_phl_seq: "\<lbrace>p\<rbrace> x \<lbrace>r\<rbrace> \<Longrightarrow> \<lbrace>r\<rbrace> y \<lbrace>q\<rbrace> \<Longrightarrow> \<lbrace>p\<rbrace> x \<cdot> y \<lbrace>q\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>p\<rbrace>x\<lbrace>r\<rbrace>; \<lbrace>r\<rbrace>y\<lbrace>q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>p\<rbrace>x \<cdot> y\<lbrace>q\<rbrace>
[PROOF STEP]
by (fact phl_seq)


[STATEMENT]
lemma the_cat_scospan_Comp_app_\<ff>\<bb>[cat_ss_cs_simps]:
  assumes "g = \<ff>\<^sub>S\<^sub>S" and "f = \<bb>\<^sub>S\<^sub>S"
  shows "g \<circ>\<^sub>A\<^bsub>\<rightarrow>\<bullet>\<leftarrow>\<^sub>C\<^esub> f = g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>\<rightarrow>\<bullet>\<leftarrow>\<^sub>C\<^esub> f = g
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>\<rightarrow>\<bullet>\<leftarrow>\<^sub>C\<^esub> f = g
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
g = \<ff>\<^sub>S\<^sub>S
f = \<bb>\<^sub>S\<^sub>S
[PROOF STEP]
have "[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> cat_scospan_composable"
[PROOF STATE]
proof (prove)
using this:
g = \<ff>\<^sub>S\<^sub>S
f = \<bb>\<^sub>S\<^sub>S

goal (1 subgoal):
 1. [g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> cat_scospan_composable
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> cat_scospan_composable

goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>\<rightarrow>\<bullet>\<leftarrow>\<^sub>C\<^esub> f = g
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> cat_scospan_composable
[PROOF STEP]
show "g \<circ>\<^sub>A\<^bsub>\<rightarrow>\<bullet>\<leftarrow>\<^sub>C\<^esub> f = g"
[PROOF STATE]
proof (prove)
using this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> cat_scospan_composable

goal (1 subgoal):
 1. g \<circ>\<^sub>A\<^bsub>\<rightarrow>\<bullet>\<leftarrow>\<^sub>C\<^esub> f = g
[PROOF STEP]
unfolding the_cat_scospan_components(5) assms
[PROOF STATE]
proof (prove)
using this:
[\<ff>\<^sub>S\<^sub>S, \<bb>\<^sub>S\<^sub>S]\<^sub>\<circ> \<in>\<^sub>\<circ> cat_scospan_composable

goal (1 subgoal):
 1. (\<lambda>gf\<in>\<^sub>\<circ>cat_scospan_composable. if gf = [\<oo>\<^sub>S\<^sub>S, \<gg>\<^sub>S\<^sub>S]\<^sub>\<circ> \<Rightarrow> \<gg>\<^sub>S\<^sub>S | gf = [\<oo>\<^sub>S\<^sub>S, \<ff>\<^sub>S\<^sub>S]\<^sub>\<circ> \<Rightarrow> \<ff>\<^sub>S\<^sub>S | otherwise \<Rightarrow> gf\<lparr>[]\<^sub>\<circ>\<rparr>) \<lparr>\<ff>\<^sub>S\<^sub>S, \<bb>\<^sub>S\<^sub>S\<rparr>\<^sub>\<bullet> = \<ff>\<^sub>S\<^sub>S
[PROOF STEP]
using cat_ss_ineq
[PROOF STATE]
proof (prove)
using this:
[\<ff>\<^sub>S\<^sub>S, \<bb>\<^sub>S\<^sub>S]\<^sub>\<circ> \<in>\<^sub>\<circ> cat_scospan_composable
\<aa>\<^sub>S\<^sub>S \<noteq> \<bb>\<^sub>S\<^sub>S
\<aa>\<^sub>S\<^sub>S \<noteq> \<oo>\<^sub>S\<^sub>S
\<bb>\<^sub>S\<^sub>S \<noteq> \<oo>\<^sub>S\<^sub>S
\<gg>\<^sub>S\<^sub>S \<noteq> \<ff>\<^sub>S\<^sub>S
\<gg>\<^sub>S\<^sub>S \<noteq> \<aa>\<^sub>S\<^sub>S
\<gg>\<^sub>S\<^sub>S \<noteq> \<bb>\<^sub>S\<^sub>S
\<gg>\<^sub>S\<^sub>S \<noteq> \<oo>\<^sub>S\<^sub>S
\<ff>\<^sub>S\<^sub>S \<noteq> \<aa>\<^sub>S\<^sub>S
\<ff>\<^sub>S\<^sub>S \<noteq> \<bb>\<^sub>S\<^sub>S
\<ff>\<^sub>S\<^sub>S \<noteq> \<oo>\<^sub>S\<^sub>S

goal (1 subgoal):
 1. (\<lambda>gf\<in>\<^sub>\<circ>cat_scospan_composable. if gf = [\<oo>\<^sub>S\<^sub>S, \<gg>\<^sub>S\<^sub>S]\<^sub>\<circ> \<Rightarrow> \<gg>\<^sub>S\<^sub>S | gf = [\<oo>\<^sub>S\<^sub>S, \<ff>\<^sub>S\<^sub>S]\<^sub>\<circ> \<Rightarrow> \<ff>\<^sub>S\<^sub>S | otherwise \<Rightarrow> gf\<lparr>[]\<^sub>\<circ>\<rparr>) \<lparr>\<ff>\<^sub>S\<^sub>S, \<bb>\<^sub>S\<^sub>S\<rparr>\<^sub>\<bullet> = \<ff>\<^sub>S\<^sub>S
[PROOF STEP]
by (auto simp: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
g \<circ>\<^sub>A\<^bsub>\<rightarrow>\<bullet>\<leftarrow>\<^sub>C\<^esub> f = g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem post_accountability:
assumes v: "valid tr" and i: "srcOf (hd tr) = istate"
and PIDin: "PID \<in>\<in> postIDs (tgtOf (last tr))"
and PID: "vis (tgtOf (last tr)) PID = VIS"
shows "proper tr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper tr
[PROOF STEP]
proof(cases "VIS = FriendV")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. VIS = FriendV \<Longrightarrow> proper tr
 2. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
VIS = FriendV

goal (2 subgoals):
 1. VIS = FriendV \<Longrightarrow> proper tr
 2. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
VIS = FriendV

goal (1 subgoal):
 1. proper tr
[PROOF STEP]
unfolding proper_def
[PROOF STATE]
proof (prove)
using this:
VIS = FriendV

goal (1 subgoal):
 1. VIS = FriendV \<or> (\<exists>uid tr1 trn tr2 trnn tr3. tr = tr1 @ trn # tr2 @ trnn # tr3 \<and> SNC uid trn \<and> SNVU uid VIS trnn \<and> (\<forall>vis. BD_Security_IO.never (SNVU uid vis) tr3))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proper tr

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
VIS \<noteq> FriendV

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
have "proper2 tr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper2 tr
[PROOF STEP]
using proper2_valid_istate[OF False v i PIDin]
[PROOF STATE]
proof (prove)
using this:
proper2 tr

goal (1 subgoal):
 1. proper2 tr
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
proper2 tr

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
proper2 tr
[PROOF STEP]
obtain uid tr1 trn trr where
  tr: "tr = tr1 @ trn # trr" and SNC: "SNC uid trn"
[PROOF STATE]
proof (prove)
using this:
proper2 tr

goal (1 subgoal):
 1. (\<And>tr1 trn trr uid. \<lbrakk>tr = tr1 @ trn # trr; SNC uid trn\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding proper2_def
[PROOF STATE]
proof (prove)
using this:
\<exists>uid tr1 trn tr2. tr = tr1 @ trn # tr2 \<and> SNC uid trn

goal (1 subgoal):
 1. (\<And>tr1 trn trr uid. \<lbrakk>tr = tr1 @ trn # trr; SNC uid trn\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tr = tr1 @ trn # trr
SNC uid trn

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
hence trn: "validTrans trn" and r: "reach (srcOf trn)"
[PROOF STATE]
proof (prove)
using this:
tr = tr1 @ trn # trr
SNC uid trn

goal (1 subgoal):
 1. validTrans trn &&& reach (srcOf trn)
[PROOF STEP]
using v
[PROOF STATE]
proof (prove)
using this:
tr = tr1 @ trn # trr
SNC uid trn
valid tr

goal (1 subgoal):
 1. validTrans trn &&& reach (srcOf trn)
[PROOF STEP]
unfolding tr
[PROOF STATE]
proof (prove)
using this:
tr1 @ trn # trr = tr1 @ trn # trr
SNC uid trn
valid (tr1 @ trn # trr)

goal (1 subgoal):
 1. validTrans trn &&& reach (srcOf trn)
[PROOF STEP]
apply (metis list.distinct(2) self_append_conv2 valid_ConsE valid_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reach (srcOf trn)
[PROOF STEP]
by (metis (mono_tags, lifting) append_Cons hd_append i list.sel(1) reach.simps tr v valid_append valid_init_reach)
[PROOF STATE]
proof (state)
this:
validTrans trn
reach (srcOf trn)

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
hence N: "PID \<in>\<in> postIDs (tgtOf trn)" "vis (tgtOf trn) PID \<noteq> VIS"
[PROOF STATE]
proof (prove)
using this:
validTrans trn
reach (srcOf trn)

goal (1 subgoal):
 1. PID \<in>\<in> postIDs (tgtOf trn) &&& vis (tgtOf trn) PID \<noteq> VIS
[PROOF STEP]
using SNC_postIDs SNC_visPost False SNC
[PROOF STATE]
proof (prove)
using this:
validTrans trn
reach (srcOf trn)
\<lbrakk>validTrans ?trn; SNC ?uid ?trn\<rbrakk> \<Longrightarrow> PID \<in>\<in> postIDs (tgtOf ?trn)
\<lbrakk>VIS \<noteq> FriendV; validTrans ?trn; SNC ?uid ?trn; reach (srcOf ?trn)\<rbrakk> \<Longrightarrow> vis (tgtOf ?trn) PID \<noteq> VIS
VIS \<noteq> FriendV
SNC uid trn

goal (1 subgoal):
 1. PID \<in>\<in> postIDs (tgtOf trn) &&& vis (tgtOf trn) PID \<noteq> VIS
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
PID \<in>\<in> postIDs (tgtOf trn)
vis (tgtOf trn) PID \<noteq> VIS

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
hence trrNE: "trr \<noteq> []" and 1: "last tr = last trr"
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> postIDs (tgtOf trn)
vis (tgtOf trn) PID \<noteq> VIS

goal (1 subgoal):
 1. trr \<noteq> [] &&& last tr = last trr
[PROOF STEP]
using PID
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> postIDs (tgtOf trn)
vis (tgtOf trn) PID \<noteq> VIS
vis (tgtOf (last tr)) PID = VIS

goal (1 subgoal):
 1. trr \<noteq> [] &&& last tr = last trr
[PROOF STEP]
unfolding tr
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> postIDs (tgtOf trn)
vis (tgtOf trn) PID \<noteq> VIS
vis (tgtOf (last (tr1 @ trn # trr))) PID = VIS

goal (1 subgoal):
 1. trr \<noteq> [] &&& last (tr1 @ trn # trr) = last trr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trr \<noteq> []
last tr = last trr

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
hence trr_v: "valid trr"
[PROOF STATE]
proof (prove)
using this:
trr \<noteq> []
last tr = last trr

goal (1 subgoal):
 1. valid trr
[PROOF STEP]
using v
[PROOF STATE]
proof (prove)
using this:
trr \<noteq> []
last tr = last trr
valid tr

goal (1 subgoal):
 1. valid trr
[PROOF STEP]
unfolding tr
[PROOF STATE]
proof (prove)
using this:
trr \<noteq> []
last (tr1 @ trn # trr) = last trr
valid (tr1 @ trn # trr)

goal (1 subgoal):
 1. valid trr
[PROOF STEP]
by (metis valid_Cons_iff append_self_conv2 list.distinct(1) valid_append)
[PROOF STATE]
proof (state)
this:
valid trr

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
have 0: "tgtOf trn = srcOf (hd trr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tgtOf trn = srcOf (hd trr)
[PROOF STEP]
using v trrNE
[PROOF STATE]
proof (prove)
using this:
valid tr
trr \<noteq> []

goal (1 subgoal):
 1. tgtOf trn = srcOf (hd trr)
[PROOF STEP]
unfolding tr
[PROOF STATE]
proof (prove)
using this:
valid (tr1 @ trn # trr)
trr \<noteq> []

goal (1 subgoal):
 1. tgtOf trn = srcOf (hd trr)
[PROOF STEP]
by (metis valid_append list.distinct(2) self_append_conv2 valid_ConsE)
[PROOF STATE]
proof (state)
this:
tgtOf trn = srcOf (hd trr)

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
have "proper1 trr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper1 trr
[PROOF STEP]
using proper1_valid[OF False trr_v N[unfolded 0] PID[unfolded 1]]
[PROOF STATE]
proof (prove)
using this:
proper1 trr

goal (1 subgoal):
 1. proper1 trr
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
proper1 trr

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
from proper1_never[OF trr_v N(1)[unfolded 0] this PID[unfolded 1]]
[PROOF STATE]
proof (chain)
picking this:
\<exists>tr2 trnn tr3. trr = tr2 @ trnn # tr3 \<and> SNVU (owner (srcOf trnn) PID) VIS trnn \<and> (\<forall>vis. BD_Security_IO.never (SNVU (owner (srcOf trnn) PID) vis) tr3)
[PROOF STEP]
obtain tr2 trnn tr3 where
  trr: "trr = tr2 @ trnn # tr3" and SNVU: "SNVU (owner (srcOf trnn) PID) VIS trnn"
  and vis: "\<forall> vis. never (SNVU (owner (srcOf trnn) PID) vis) tr3"
[PROOF STATE]
proof (prove)
using this:
\<exists>tr2 trnn tr3. trr = tr2 @ trnn # tr3 \<and> SNVU (owner (srcOf trnn) PID) VIS trnn \<and> (\<forall>vis. BD_Security_IO.never (SNVU (owner (srcOf trnn) PID) vis) tr3)

goal (1 subgoal):
 1. (\<And>tr2 trnn tr3. \<lbrakk>trr = tr2 @ trnn # tr3; SNVU (owner (srcOf trnn) PID) VIS trnn; \<forall>vis. BD_Security_IO.never (SNVU (owner (srcOf trnn) PID) vis) tr3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trr = tr2 @ trnn # tr3
SNVU (owner (srcOf trnn) PID) VIS trnn
\<forall>vis. BD_Security_IO.never (SNVU (owner (srcOf trnn) PID) vis) tr3

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
have 00: "srcOf (hd (tr2 @ [trnn])) = tgtOf trn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. srcOf (hd (tr2 ## trnn)) = tgtOf trn
[PROOF STEP]
using v
[PROOF STATE]
proof (prove)
using this:
valid tr

goal (1 subgoal):
 1. srcOf (hd (tr2 ## trnn)) = tgtOf trn
[PROOF STEP]
unfolding tr trr
[PROOF STATE]
proof (prove)
using this:
valid (tr1 @ trn # tr2 @ trnn # tr3)

goal (1 subgoal):
 1. srcOf (hd (tr2 ## trnn)) = tgtOf trn
[PROOF STEP]
by (metis "0" append_self_conv2 hd_append2 list.sel(1) trr)
[PROOF STATE]
proof (state)
this:
srcOf (hd (tr2 ## trnn)) = tgtOf trn

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
have trnn: "validTrans trnn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. validTrans trnn
[PROOF STEP]
using trr_v
[PROOF STATE]
proof (prove)
using this:
valid trr

goal (1 subgoal):
 1. validTrans trnn
[PROOF STEP]
unfolding trr
[PROOF STATE]
proof (prove)
using this:
valid (tr2 @ trnn # tr3)

goal (1 subgoal):
 1. validTrans trnn
[PROOF STEP]
by (metis valid_Cons_iff append_self_conv2 list.distinct(1) valid_append)
[PROOF STATE]
proof (state)
this:
validTrans trnn

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
have vv: "valid (tr2 @ [trnn])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid (tr2 ## trnn)
[PROOF STEP]
using v
[PROOF STATE]
proof (prove)
using this:
valid tr

goal (1 subgoal):
 1. valid (tr2 ## trnn)
[PROOF STEP]
unfolding tr trr
[PROOF STATE]
proof (prove)
using this:
valid (tr1 @ trn # tr2 @ trnn # tr3)

goal (1 subgoal):
 1. valid (tr2 ## trnn)
[PROOF STEP]
by (smt Nil_is_append_conv append_self_conv2 hd_append2 list.distinct(1) list.sel(1)
        valid_Cons_iff valid_append)
[PROOF STATE]
proof (state)
this:
valid (tr2 ## trnn)

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
have "uid = owner (tgtOf trn) PID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uid = owner (tgtOf trn) PID
[PROOF STEP]
using SNC trn SNC_owner
[PROOF STATE]
proof (prove)
using this:
SNC uid trn
validTrans trn
\<lbrakk>validTrans ?trn; SNC ?uid ?trn\<rbrakk> \<Longrightarrow> ?uid = owner (tgtOf ?trn) PID

goal (1 subgoal):
 1. uid = owner (tgtOf trn) PID
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
uid = owner (tgtOf trn) PID

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
uid = owner (tgtOf trn) PID

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
have "... = owner (tgtOf trnn) PID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. owner (tgtOf trn) PID = owner (tgtOf trnn) PID
[PROOF STEP]
using owner_valid[OF vv] N(1)
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> postIDs (srcOf (hd (tr2 ## trnn))) \<Longrightarrow> owner (srcOf (hd (tr2 ## trnn))) PID = owner (tgtOf (last (tr2 ## trnn))) PID
PID \<in>\<in> postIDs (tgtOf trn)

goal (1 subgoal):
 1. owner (tgtOf trn) PID = owner (tgtOf trnn) PID
[PROOF STEP]
unfolding 00
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> postIDs (tgtOf trn) \<Longrightarrow> owner (tgtOf trn) PID = owner (tgtOf (last (tr2 ## trnn))) PID
PID \<in>\<in> postIDs (tgtOf trn)

goal (1 subgoal):
 1. owner (tgtOf trn) PID = owner (tgtOf trnn) PID
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
owner (tgtOf trn) PID = owner (tgtOf trnn) PID

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
owner (tgtOf trn) PID = owner (tgtOf trnn) PID

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
have "... = owner (srcOf trnn) PID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. owner (tgtOf trnn) PID = owner (srcOf trnn) PID
[PROOF STEP]
using SNVU trnn SNVU_postIDs owner_validTrans
[PROOF STATE]
proof (prove)
using this:
SNVU (owner (srcOf trnn) PID) VIS trnn
validTrans trnn
\<lbrakk>validTrans ?trn; SNVU ?uid ?vs ?trn\<rbrakk> \<Longrightarrow> PID \<in>\<in> postIDs (srcOf ?trn)
\<lbrakk>validTrans ?trn; PID \<in>\<in> postIDs (srcOf ?trn)\<rbrakk> \<Longrightarrow> owner (srcOf ?trn) PID = owner (tgtOf ?trn) PID

goal (1 subgoal):
 1. owner (tgtOf trnn) PID = owner (srcOf trnn) PID
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
owner (tgtOf trnn) PID = owner (srcOf trnn) PID

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
uid = owner (srcOf trnn) PID
[PROOF STEP]
have uid: "uid = owner (srcOf trnn) PID"
[PROOF STATE]
proof (prove)
using this:
uid = owner (srcOf trnn) PID

goal (1 subgoal):
 1. uid = owner (srcOf trnn) PID
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
uid = owner (srcOf trnn) PID

goal (1 subgoal):
 1. VIS \<noteq> FriendV \<Longrightarrow> proper tr
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper tr
[PROOF STEP]
unfolding proper_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VIS = FriendV \<or> (\<exists>uid tr1 trn tr2 trnn tr3. tr = tr1 @ trn # tr2 @ trnn # tr3 \<and> SNC uid trn \<and> SNVU uid VIS trnn \<and> (\<forall>vis. BD_Security_IO.never (SNVU uid vis) tr3))
[PROOF STEP]
apply(rule disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>uid tr1 trn tr2 trnn tr3. tr = tr1 @ trn # tr2 @ trnn # tr3 \<and> SNC uid trn \<and> SNVU uid VIS trnn \<and> (\<forall>vis. BD_Security_IO.never (SNVU uid vis) tr3)
[PROOF STEP]
apply(intro exI[of _ uid] exI[of _ tr1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>trn tr2 trnn tr3. tr = tr1 @ trn # tr2 @ trnn # tr3 \<and> SNC uid trn \<and> SNVU uid VIS trnn \<and> (\<forall>vis. BD_Security_IO.never (SNVU uid vis) tr3)
[PROOF STEP]
apply(rule exI[of _ trn], rule exI[of _ tr2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>trnn tr3. tr = tr1 @ trn # tr2 @ trnn # tr3 \<and> SNC uid trn \<and> SNVU uid VIS trnn \<and> (\<forall>vis. BD_Security_IO.never (SNVU uid vis) tr3)
[PROOF STEP]
apply(intro exI[of _ trnn] exI[of _ tr3])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tr = tr1 @ trn # tr2 @ trnn # tr3 \<and> SNC uid trn \<and> SNVU uid VIS trnn \<and> (\<forall>vis. BD_Security_IO.never (SNVU uid vis) tr3)
[PROOF STEP]
using SNC SNVU vis
[PROOF STATE]
proof (prove)
using this:
SNC uid trn
SNVU (owner (srcOf trnn) PID) VIS trnn
\<forall>vis. BD_Security_IO.never (SNVU (owner (srcOf trnn) PID) vis) tr3

goal (1 subgoal):
 1. tr = tr1 @ trn # tr2 @ trnn # tr3 \<and> SNC uid trn \<and> SNVU uid VIS trnn \<and> (\<forall>vis. BD_Security_IO.never (SNVU uid vis) tr3)
[PROOF STEP]
unfolding tr trr uid
[PROOF STATE]
proof (prove)
using this:
SNC (owner (srcOf trnn) PID) trn
SNVU (owner (srcOf trnn) PID) VIS trnn
\<forall>vis. BD_Security_IO.never (SNVU (owner (srcOf trnn) PID) vis) tr3

goal (1 subgoal):
 1. tr1 @ trn # tr2 @ trnn # tr3 = tr1 @ trn # tr2 @ trnn # tr3 \<and> SNC (owner (srcOf trnn) PID) trn \<and> SNVU (owner (srcOf trnn) PID) VIS trnn \<and> (\<forall>vis. BD_Security_IO.never (SNVU (owner (srcOf trnn) PID) vis) tr3)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proper tr

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma absn_cong[intro]: "s \<leftrightarrow> t \<Longrightarrow> (Abs^^n) s \<leftrightarrow> (Abs^^n) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<leftrightarrow> t \<Longrightarrow> (Abs ^^ n) s \<leftrightarrow> (Abs ^^ n) t
[PROOF STEP]
by (induction n) auto


[STATEMENT]
lemma reach_lreach:
assumes "reach s"
obtains "lreach nid (s nid)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lreach nid (s nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (lreach nid (s nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
interpret Node: Transition_System "istate nid" "validTrans nid" "srcOf nid" "tgtOf nid"
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (Node.reach (s nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms that
[PROOF STATE]
proof (chain)
picking this:
reach s
Node.reach (s nid) \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
reach s
Node.reach (s nid) \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof induction
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (Node.reach (istate nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis
 2. \<And>s trn s'. \<lbrakk>reach s; (Node.reach (s nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis; nValidTrans trn; nSrcOf trn = s; nTgtOf trn = s'; Node.reach (s' nid) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case Istate
[PROOF STATE]
proof (state)
this:
Node.reach (istate nid) \<Longrightarrow> thesis

goal (2 subgoals):
 1. (Node.reach (istate nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis
 2. \<And>s trn s'. \<lbrakk>reach s; (Node.reach (s nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis; nValidTrans trn; nSrcOf trn = s; nTgtOf trn = s'; Node.reach (s' nid) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Node.reach (istate nid) \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
Node.reach (istate nid) \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using Node.reach.Istate
[PROOF STATE]
proof (prove)
using this:
Node.reach (istate nid) \<Longrightarrow> thesis
Node.reach (istate nid)

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

goal (1 subgoal):
 1. \<And>s trn s'. \<lbrakk>reach s; (Node.reach (s nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis; nValidTrans trn; nSrcOf trn = s; nTgtOf trn = s'; Node.reach (s' nid) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s trn s'. \<lbrakk>reach s; (Node.reach (s nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis; nValidTrans trn; nSrcOf trn = s; nTgtOf trn = s'; Node.reach (s' nid) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (Step s trn s')
[PROOF STATE]
proof (state)
this:
reach s
nValidTrans trn
nSrcOf trn = s
nTgtOf trn = s'
(Node.reach (s nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis
Node.reach (s' nid) \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<And>s trn s'. \<lbrakk>reach s; (Node.reach (s nid) \<Longrightarrow> thesis) \<Longrightarrow> thesis; nValidTrans trn; nSrcOf trn = s; nTgtOf trn = s'; Node.reach (s' nid) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (rule Step.IH)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Node.reach (s nid) \<Longrightarrow> thesis
[PROOF STEP]
assume "Node.reach (s nid)"
[PROOF STATE]
proof (state)
this:
Node.reach (s nid)

goal (1 subgoal):
 1. Node.reach (s nid) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Node.reach (s nid)
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
Node.reach (s nid)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using Step.hyps Node.reach.Step[of "s nid" _ "s' nid"]
[PROOF STATE]
proof (prove)
using this:
Node.reach (s nid)
reach s
nValidTrans trn
nSrcOf trn = s
nTgtOf trn = s'
\<lbrakk>Node.reach (s nid); validTrans nid ?trn; srcOf nid ?trn = s nid; tgtOf nid ?trn = s' nid\<rbrakk> \<Longrightarrow> Node.reach (s' nid)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (intro Step.prems, cases trn) (auto)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Class_revI [intro, simp]:
  "(a, b) \<in> E \<Longrightarrow> b \<in> Class a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> E \<Longrightarrow> b \<in> Class a
[PROOF STEP]
by (blast intro: symmetric)


[STATEMENT]
lemma
  iNext_iff: "(\<circle> t t0 I. P t) = (\<box> t [\<dots>0] \<oplus> (inext t0 I). P t)" and
  iLast_iff: "(\<ominus> t t0 I. P t) = (\<box> t [\<dots>0] \<oplus> (iprev t0 I). P t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iNext t0 I P = (\<box> t [\<dots>0] \<oplus> inext t0 I. P t) &&& iLast t0 I P = (\<box> t [\<dots>0] \<oplus> iprev t0 I. P t)
[PROOF STEP]
by (fastforce simp: iTL_Next_defs iT_add iIN_0)+