header {* 
  \isaheader{VCG Completeness} 
*}

theory VCG_Completeness = VCG:

--{* In completeVCG we show that verification conditions are tautologies. If the safety logic is complete, this means
     they are provable. *}

locale completeVCG = VCG +

fixes Starters::"'program \<Rightarrow> ('pos \<times> 'mem) set"
defines "Starters \<Pi> \<equiv> {s. \<Pi>,s \<Turnstile> initF \<Pi> \<or> (\<exists> A. anF \<Pi> (fst s) = Some A \<and> \<Pi>,s \<Turnstile> A \<and> \<Pi>,s \<Turnstile> safeF \<Pi> (fst s))}"

fixes branch ::  "'program \<Rightarrow> (('pos \<times> 'mem) \<times> ('pos \<times> 'mem)) set"
defines "branch \<Pi> \<equiv> {(s,s'). \<exists>B. (fst s',B) \<in> set (succsF \<Pi> (fst s)) \<and> \<Pi>,s \<Turnstile> B}"

fixes effS\<^isub>B:: "'program \<Rightarrow> (('pos \<times> 'mem) \<times> ('pos \<times> 'mem)) set"
defines "effS\<^isub>B \<Pi> \<equiv> (effS \<Pi>) \<inter> (branch \<Pi>)"

fixes strongAn:: "'program \<Rightarrow> bool"
defines "strongAn \<Pi> \<equiv> (\<forall>s \<in> ReachableFrom (effS\<^isub>B \<Pi>) (Starters \<Pi>). \<Pi>,s \<Turnstile> aF \<Pi> (fst s) \<and> \<Pi>,s \<Turnstile> safeF \<Pi> (fst s))" 

assumes semImpI: "\<lbrakk> wf \<Pi>; \<Pi>,s \<Turnstile> f \<Longrightarrow> \<Pi>,s \<Turnstile> f' \<rbrakk> \<Longrightarrow> \<Pi>,s \<Turnstile> f \<Impl> f'"


assumes succsFprogress: "\<lbrakk> wf \<Pi>; \<Pi>,(p,m) \<Turnstile> B; 
                           (p',B) \<in> set (succsF \<Pi> p'') \<rbrakk> 
                         \<Longrightarrow> p=p'' \<and> (\<exists> m'. ((p,m),(p',m')) \<in> (effS \<Pi>))"

assumes completeWpF: "\<lbrakk> wf \<Pi>;  
                        (p',B) \<in> set (succsF \<Pi> p);  \<Pi>,(p,m) \<Turnstile> B;
                         ((p,m),(p',m')) \<in> (effS \<Pi>); 
                        \<Pi>,(p',m') \<Turnstile> Q \<rbrakk> \<Longrightarrow> \<Pi>,(p,m) \<Turnstile> wpF \<Pi> p p' Q"


assumes ipc_domC:
"wf \<Pi> \<Longrightarrow> ipc \<Pi> \<in> set (domC \<Pi>)"

assumes succsF_domC:
"\<lbrakk> wf \<Pi>; (p',B) \<in> set (succsF \<Pi> p) \<rbrakk> \<Longrightarrow> (p \<in> set (domC \<Pi>)) \<and> (p' \<in> set (domC \<Pi>))"

lemma (in completeVCG) ReachableFrom_isafeF_aux: "\<And> S. \<lbrakk> wf \<Pi>; strongAn \<Pi> \<rbrakk> \<Longrightarrow> 
(\<forall> s \<in> ReachableFrom (effS\<^isub>B \<Pi>) (Starters \<Pi>). 
 ((\<exists> V. noAnn V (anF \<Pi>) \<and> set V \<union> set S = set (domC \<Pi>) \<and> set V \<inter> set S = {} \<and> (V \<noteq> [] \<longrightarrow> V@[fst s] \<in> (paths (succsF \<Pi>)))) 
\<longrightarrow> ((fst s \<in> set (domC \<Pi>)) \<longrightarrow> (\<Pi>,s \<Turnstile> isafeF \<Pi> (fst s)))))"
--{* S contains positions not yet visited by isafeF. It decreases as isafeF expands. *}
(*<*)
apply (subgoal_tac "\<exists> k. length S = k")
 prefer 2
 apply simp
apply (erule exE)
apply (erule rev_mp)+
apply (simp only: atomize_all)
apply (rule forall_switch2)
apply (rule allI)
apply (rule_tac n="k" in nat_less_induct)

apply (rule allI | rule impI | rule ballI | simp add: Let_def split_def)+
apply (erule exE | erule conjE)+
apply (subgoal_tac "\<Pi>,s \<Turnstile> safeF \<Pi> (fst s) \<and> \<Pi>,s \<Turnstile> aF \<Pi> (fst s)")
 prefer 2
 apply (simp add: strongAn_def)
apply (erule conjE)+
apply (subgoal_tac "fst s \<in> set (domC \<Pi>)")
 prefer 2
 apply assumption
apply (case_tac "anF \<Pi> (fst s)")
prefer 2
--{* anF Pi (fst s) = Some a *}
apply (simp add: isafeFdef semConj aF_def)

--{* anF Pi (fst s) = None *}
apply (subgoal_tac "\<exists> p m. s = (p,m)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (case_tac "p \<in> set S")
--{* p in set S *}
apply (erule_tac x="length [q \<in> S. q \<noteq> p]" in allE)
apply (subgoal_tac "length [q \<in> S. q \<noteq> p] < length S")
 prefer 2
 apply (rule AuxBox.length_filter_less)
 apply (simp add: set_mem_eq)
apply simp
apply (erule_tac x="[q \<in> S. q \<noteq> p]" in allE)
apply simp
apply (simplesubst isafeFdef)
apply assumption
apply (simp add: semConj)
apply (rule ballI)
apply (subgoal_tac "\<exists> p' B. x = (p',B)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (simp only: split_def snd_conv)
apply (rule semImpI)
apply assumption
apply (subgoal_tac "p = p \<and> (\<exists> m'. ((p,m),(p',m')) \<in> (effS \<Pi>))")
 prefer 2
 apply (rule_tac B="B" in succsFprogress)
 apply assumption
 apply simp
 apply simp
 apply simp
apply (erule conjE | erule exE)+
apply (subgoal_tac "(p',m') \<in>  ReachableFrom (effS\<^isub>B \<Pi>) (Starters \<Pi>)")
 prefer 2
 apply (rule_tac a="(p,m)" in ReachableFrom.step)
 apply simp
 apply (simp add: effS\<^isub>B_def branch_def)
 apply fastsimp
apply (erule_tac x="(p',m')" in ballE)
prefer 2
apply simp

apply (subgoal_tac "\<Pi>,(p',m') \<Turnstile> isafeF \<Pi> p'")
 prefer 2
 apply (subgoal_tac "(\<exists>V. noAnn V (anF \<Pi>) \<and>
             set V \<union> {x \<in> set S. x \<noteq> fst s} = set (domC \<Pi>) \<and> set V \<inter> {x \<in> set S. x \<noteq> fst s} = {} \<and> (V \<noteq> [] \<longrightarrow> V @ [fst (p', m')] \<in> paths (succsF \<Pi>)))")
  prefer 2
  apply (rule_tac x="V@[p]" in exI)
  apply (rule conjI)
  apply (rule noAnn_ext)
  apply simp+
  apply (rule conjI)
  apply (simplesubst insert_union_right)
  apply (simplesubst insert_set_filter)
  apply (subgoal_tac "insert p (set S) = set S")
   prefer 2
   apply (simp add: set_mem_eq insert_absorb)
  apply (simp only:)

  apply (rule conjI)
  apply (subgoal_tac "set V \<inter> {x. x \<in> set S \<and> x \<noteq> p} \<subseteq>  set V \<inter> set S")
   prefer 2
   apply (rule intersect_mono)
  apply simp
 
  apply (case_tac "V")
  apply simp
  apply (rule paths.start)
  apply simp

  apply simp
  apply (subgoal_tac "(a # list) @ [p] @ [p'] \<in>  paths (succsF \<Pi>)")
   prefer 2
   apply (rule paths.step)
   apply simp
   apply simp
  apply simp
 apply simp
apply (subgoal_tac "p' \<in> set (domC \<Pi>)")
 prefer 2
 apply (rule succsF_domC[THEN conjE])
 apply simp
 apply simp
 apply simp
apply (drule mp, assumption)
apply assumption

apply (subgoal_tac "\<Pi>,(p, m) \<Turnstile> wpF \<Pi> p p' (isafeF \<Pi> p')")
 prefer 2
 apply (rule_tac B="B" in completeWpF)
 apply assumption
 apply assumption
 apply assumption
 apply assumption
 apply assumption
 apply assumption
apply simp


--{* fst notin set S *}
apply (subgoal_tac "noAnn (V@[p]) (anF \<Pi>)")
 prefer 2
 apply (rule noAnn_ext)
 apply simp
 apply simp
apply (subgoal_tac "p \<in> set V")
 prefer 2
 apply (drule_tac t="set (domC \<Pi>)" in sym)
 apply simp
--{* p in V and noAnn V@[p] contradicts wf Pi, which enforces loop annotations. *}
apply (frule wf_anF)
apply (unfold enoughAn_def)
apply (simp only: in_set_conv_decomp)
apply (erule exE | erule conjE)+
apply (erule_tac x="p # zsa @ [p]" in allE)
apply (simp add: isCycle_def)
apply (subgoal_tac "p # zsa @ [p] \<in> (paths (succsF \<Pi>))")
 prefer 2
 apply (rule_tac ps="ysa" in paths_append)
 apply simp
 apply (case_tac "ysa")
 apply simp

 apply simp

 apply simp
apply simp

apply (simp add:noAnn_def)
done
(*>*)

theorem (in completeVCG) ReachableFrom_isafeF:
"\<lbrakk> wf \<Pi>; strongAn \<Pi> \<rbrakk> \<Longrightarrow> (\<forall>s \<in> ReachableFrom (effS\<^isub>B \<Pi>) (Starters \<Pi>). (fst s \<in> set (domC \<Pi>)) \<longrightarrow> \<Pi>,s \<Turnstile> isafeF \<Pi> (fst s))"
(*<*)
apply (drule_tac S="domC \<Pi>" in ReachableFrom_isafeF_aux)
apply assumption

apply (rule ballI)
apply (erule_tac x="s" in ballE)
prefer 2
apply simp

apply (subgoal_tac "(\<exists>V. noAnn V (anF \<Pi>) \<and> set V \<union> set (domC \<Pi>) = set (domC \<Pi>) 
                         \<and> set V \<inter> set (domC \<Pi>) = {} \<and> (V \<noteq> [] \<longrightarrow> V @ [fst s] \<in> paths (succsF \<Pi>)))")
 prefer 2
 apply (rule_tac x="[]" in exI)
 apply (simp add: noAnn_def)
apply simp
done
(*>*)

theorem (in completeVCG) vcg_tautology: 
assumes wf_Pi: "wf \<Pi>"
assumes strongAn: "strongAn \<Pi>"
shows "\<Pi>,s \<Turnstile> vcg \<Pi>"
(*<*)
proof -
  from wf_Pi 
  have initial_vc: "\<Pi>,s \<Turnstile> (initF \<Pi>) \<Impl> (isafeF \<Pi> (ipc \<Pi>))"
  proof (rule semImpI)
    {
      assume s_initF: "\<Pi>,s \<Turnstile> initF \<Pi>"
      show s_isafeF: "\<Pi>,s \<Turnstile> isafeF \<Pi> (ipc \<Pi>)"
	proof -
	from wf_Pi s_initF 
	have s_ipc: "fst s = ipc \<Pi>"
	  by (rule_tac s="s" in initF_ipc,simp+)

	from s_initF have s_ReachableFrom: "s \<in> ReachableFrom (effS\<^isub>B \<Pi>) (Starters \<Pi>)"
	  apply -
	  apply (rule ReachableFrom.init)
	  apply (simp add: Starters_def)
	  done

	from wf_Pi s_ipc have s_domC: "fst s \<in> set (domC \<Pi>)"
	  apply -
	  apply (drule ipc_domC)
	  apply simp
	  done

	from wf_Pi s_domC strongAn s_ReachableFrom 
	have s_isafeF: "\<Pi>,s \<Turnstile> (isafeF \<Pi> (fst s))"
	  apply -
	  apply (drule ReachableFrom_isafeF)
	  apply simp
	  apply simp
	  done

	from s_isafeF s_ipc show ?thesis
	  by simp
      qed
    } 
  qed

  have vc_sections: "\<Pi>,s \<Turnstile> \<Conj> (map (\<lambda> p. (\<Conj> 
                     (map (\<lambda> (p',B). (\<Conj> [isafeF \<Pi> p,B]) \<Impl> (wpF \<Pi> p p' (isafeF \<Pi> p'))) (succsF \<Pi> p))
                                               )) (domA \<Pi>))"
    proof -
      have vc_single_section: "\<forall> p \<in> set (domC \<Pi>). \<forall> A. anF \<Pi> p = Some A \<longrightarrow> (\<forall> p' B. (p',B) \<in> set (succsF \<Pi> p) \<longrightarrow>
                               (\<Pi>,s \<Turnstile> isafeF \<Pi> p \<and> \<Pi>,s \<Turnstile> B) \<longrightarrow> (\<Pi>,s \<Turnstile> wpF \<Pi> p p' (isafeF \<Pi> p')))"
	proof (intro allI ballI impI, elim conjE)
	    fix p A p' B
	    assume p_domC: "p \<in> set (domC \<Pi>)"
	    assume anF_p: "anF \<Pi> p = Some A"
	    assume succsF_p: "(p',B) \<in> set (succsF \<Pi> p)"
	    assume s_isafeF: "\<Pi>,s \<Turnstile> isafeF \<Pi> p"
	    assume s_B:"\<Pi>,s \<Turnstile> B"
	    show "\<Pi>,s \<Turnstile> wpF \<Pi> p p' (isafeF \<Pi> p')"
	      proof -
		obtain sp sm where s_def: "s = (sp,sm)"
		  by fastsimp

		from s_isafeF anF_p s_def wf_Pi p_domC
		have s_A: "\<Pi>,s \<Turnstile> A"
		  by (simp add: isafeFdef semConj)

		from s_isafeF anF_p s_def wf_Pi p_domC
		have s_safeF: "\<Pi>,s \<Turnstile> safeF \<Pi> p"
		  by (simp add: isafeFdef semConj)

		from wf_Pi anF_p s_A succsF_p s_B s_def
		obtain m' where sp_p: "sp = p" and s_s'_effS:"((sp,sm),(p',m')) \<in> (effS \<Pi>)"
		  apply -
		  apply (subgoal_tac "sp = p \<and> (\<exists>  m'. ((sp,sm),(p',m')) \<in> (effS \<Pi>))")
		   prefer 2
		   apply (rule_tac B="B" in succsFprogress)
		   apply (simp add: aF_def)+
		  apply fastsimp
		  done
		from s_def sp_p s_A anF_p s_safeF s_s'_effS s_B succsF_p
		have s'_ReachableFrom: "(p',m') \<in> ReachableFrom (effS\<^isub>B \<Pi>) (Starters \<Pi>)"
		  apply -
		  apply (rule_tac a="s" in ReachableFrom.step)
		  apply (rule ReachableFrom.init)
		  apply (simp add: Starters_def)

		  apply (simp add: effS\<^isub>B_def branch_def)
		  apply fastsimp
		  done

		from wf_Pi succsF_p have p'_domC: "p' \<in> set (domC \<Pi>)"
		  apply -
		  apply (rule succsF_domC[THEN conjE])
		  apply simp
		  apply simp
		  apply simp
		  done

		from wf_Pi strongAn p'_domC s'_ReachableFrom 
		have s'_isafeF: "\<Pi>,(p',m') \<Turnstile> isafeF \<Pi> p'"
		  apply -
		  apply (drule ReachableFrom_isafeF)
		  apply simp
		  apply (erule_tac x="(p',m')" in ballE)
		  apply simp
		  apply simp
		  done

		from wf_Pi anF_p s_A sp_p succsF_p s_B s_s'_effS s'_isafeF s_def
		show ?thesis
		  apply -
		  apply (simp only:)
		  apply (rule completeWpF)
		  apply (simp add: aF_def)+
		  done
	  qed
	qed
	from wf_Pi vc_single_section show ?thesis
	  apply -
	  apply (simp add: semConj domA_def)
	  apply (rule allI | rule impI | rule ballI)+
	  apply (erule_tac x="x" in ballE)
	  prefer 2
	  apply simp

	  apply simp
	  apply (erule_tac x="fst xa" in allE)
	  apply (erule_tac x="snd xa" in allE)
	  apply (simp add: split_def semConj)
	  apply (rule semImpI)
	  apply assumption

	  apply (simp add: semConj)
	  done
      qed

      from wf_Pi initial_vc vc_sections show ?thesis
	by (simp add: vcgdef semConj)
qed
(*>*)

theorem (in completeVCG) vcg_completeness:
"\<lbrakk> wf \<Pi>; strongAn \<Pi>; (\<forall> s. \<Pi>,s \<Turnstile> vcg \<Pi>) \<longrightarrow> \<Pi> \<turnstile> vcg \<Pi> \<rbrakk> \<Longrightarrow> \<Pi> \<turnstile> vcg \<Pi>"
(*<*)
apply (subgoal_tac "\<forall> s. \<Pi>,s \<Turnstile> vcg \<Pi>")
 prefer 2
 apply (rule allI)
 apply (rule vcg_tautology)
 apply assumption+
apply simp
done
(*>*)









lemma ReachableFrom_trans:
"\<lbrakk> a \<in> ReachableFrom R S; b \<in> ReachableFrom R {a} \<rbrakk> \<Longrightarrow> b \<in> ReachableFrom R S"
apply (simp add: ReachableFrom_conv)
apply fastsimp
done

consts ReachableFrom_k:: "('a \<times> 'a) set \<Rightarrow> 'a set \<Rightarrow> (nat \<times> 'a) set"
inductive "ReachableFrom_k R S"
intros
init: "a \<in> S \<Longrightarrow> (0,a) \<in> ReachableFrom_k R S"
step: "(k,a) \<in> ReachableFrom_k R S \<Longrightarrow> (a,b) \<in> R \<Longrightarrow> (k+1,b) \<in> ReachableFrom_k R S"


constdefs ReachableFromIn:: "('a \<times> 'a) set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set"
"ReachableFromIn R S k \<equiv> {a. (k,a) \<in> ReachableFrom_k R S}"

lemma k_init: "a \<in> S \<Longrightarrow> a \<in> ReachableFromIn R S 0"
apply (simp add: ReachableFromIn_def)
apply (rule init)
apply simp
done

lemma k_step: "a \<in> ReachableFromIn R S k \<Longrightarrow> (a,b) \<in> R \<Longrightarrow> b \<in> ReachableFromIn R S (k+1)"
apply (simp add: ReachableFromIn_def)
apply (drule step)
apply simp
apply simp
done

consts
ispecFe:: "('program \<times> 'pos \<times> nat \<times> ('program \<Rightarrow> 'pos \<Rightarrow> 'form option) \<times> 'form \<times> ('form list \<Rightarrow> 'form) \<times> ('form \<Rightarrow> 'form \<Rightarrow> 'form) \<times>  
        ( 'program  \<Rightarrow> 'pos \<Rightarrow> 'form) \<times> ('program  \<Rightarrow> 'pos \<Rightarrow> ('pos \<times> 'form) list) \<times> ('program  \<Rightarrow> 'pos \<Rightarrow> 'pos \<Rightarrow> 'form \<Rightarrow> 'form)) \<Rightarrow> 'form"

recdef 
ispecFe  "measure (\<lambda> a. (fst (snd (snd a))))"
"ispecFe (\<Pi>,p,k,specF,TrueF,Conj,Impl,safeF,succsF,wpF) = 
  (case specF \<Pi> p 
        of Some Q \<Rightarrow> Q
        | None \<Rightarrow> (case k 
                   of 0 \<Rightarrow> TrueF 
                   | Suc k' \<Rightarrow> Conj (map (\<lambda>(p',B). Impl B (wpF \<Pi> p p' (Conj [safeF \<Pi> p', ispecFe (\<Pi>,p',k',specF,TrueF,Conj,Impl,safeF,succsF,wpF)]))) (succsF \<Pi> p))))"

locale exprSL = completeVCG +

fixes finals:: "'program \<Rightarrow> 'pos set"
defines
"finals \<Pi> == {p. p \<in> set (domC \<Pi>) \<and> \<not> (\<exists>p' B. (p',B) \<in> set (succsF \<Pi> p))}"

fixes specF::  "'program \<Rightarrow> 'pos \<Rightarrow> 'form option"

fixes ispecF:: "'program \<Rightarrow> 'pos \<Rightarrow> nat \<Rightarrow> 'form" 
defines "ispecF \<equiv> \<lambda>\<Pi> p k. ispecFe (\<Pi>,p,k,specF,TrueF,Conj,Impl,safeF,succsF,wpF)"

assumes correctWpF:
"\<lbrakk> wf \<Pi>;  (p',B) \<in> set (succsF \<Pi> p);  \<Pi>,(p,m) \<Turnstile> B; ((p,m),(p',m')) \<in> (effS \<Pi>); 
   \<Pi>,(p,m) \<Turnstile> wpF \<Pi> p p' Q \<rbrakk>\<Longrightarrow> \<Pi>,(p',m') \<Turnstile> Q"

assumes specF_pos: "\<forall>p. p \<in> {ipc \<Pi>}\<union>(finals \<Pi>) = (specF \<Pi> p \<noteq> None)" 

assumes specF_ipc: "specF \<Pi> (ipc \<Pi>) = Some (initF \<Pi>)"

assumes ipc_not_succsF: "wf \<Pi> \<Longrightarrow> \<forall>p. ipc \<Pi> \<notin> set (map fst (succsF \<Pi> p))"  

lemma (in exprSL) ispecFe_def: 
"ispecFe (\<Pi>, p, k, specF, TrueF, Conj, Impl, safeF, succsF, wpF) =
(case specF \<Pi> p of
 None \<Rightarrow> case k of 0 \<Rightarrow> TrueF
        | Suc k' \<Rightarrow>
            Conj (map (\<lambda>(p', B). Impl B (wpF \<Pi> p p' (Conj [safeF \<Pi> p', ispecFe (\<Pi>, p', k', specF, TrueF, Conj, Impl, safeF, succsF, wpF)])))
                   (succsF \<Pi> p))
 | Some Q \<Rightarrow> Q)"
apply (subst ispecFe.simps)
apply simp
done

lemma (in exprSL) ispecF_def:
"\<And> p. ispecF \<Pi> p k = (case specF \<Pi> p 
              of Some Q \<Rightarrow> Q
              | None \<Rightarrow> (case k of 0 \<Rightarrow> \<TrueF> 
                         | Suc k' \<Rightarrow> \<Conj> (map (\<lambda>(p',B). B \<Impl> (wpF \<Pi> p p' (\<Conj> [safeF \<Pi> p', ispecF \<Pi> p' k'])))) (succsF \<Pi> p)))"
apply (induct_tac "k")
apply (simp add: ispecF_def)
apply (case_tac "specF \<Pi> p")
apply simp

apply simp

apply (case_tac "specF \<Pi> p")
apply (simp add: ispecF_def)

apply (simp add: ispecF_def)
done

lemma ReachableFromIn_elims:
"\<lbrakk> s \<in> ReachableFromIn R S k; \<lbrakk> k = 0; s \<in> S \<rbrakk> \<Longrightarrow> P; 
  \<And>s' k'. \<lbrakk>k = Suc k';  s' \<in> ReachableFromIn R S k'; (s', s) \<in> R\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
apply (simp add: ReachableFromIn_def)
apply (erule ReachableFrom_k.elims)
apply simp

apply simp
done

lemma ReachableFrom_ReachableFromIn:
"s \<in> ReachableFrom R S \<Longrightarrow> \<exists> k. s \<in> ReachableFromIn R S k"
apply (erule ReachableFrom.induct)
apply (drule_tac R="R" in k_init)
apply fastsimp

apply (erule exE)
apply (rule_tac x="k+1" in exI)
apply (rule k_step)
apply simp
apply simp
done

lemma ReachableFromIn_ReachableFrom:
"s \<in> ReachableFromIn R S k  \<Longrightarrow> s \<in> ReachableFrom R S"
apply (simp add: ReachableFromIn_def)
apply (erule ReachableFrom_k.induct)
apply (rule ReachableFrom.init)
apply simp

apply (rule ReachableFrom.step)
apply simp
apply simp
done

lemma k_lstep:
"\<lbrakk> s' \<in> ReachableFromIn R S k \<rbrakk> \<Longrightarrow> k > 0 \<longrightarrow> (\<exists> s s''. s \<in> S \<and> (s,s'') \<in> R \<and> s' \<in> ReachableFromIn R {s''} (k - 1))"
apply (simp add: ReachableFromIn_def)
apply (erule ReachableFrom_k.induct)
apply simp
apply (rule impI | erule conjE)+
apply (case_tac "k")
apply simp
apply (erule ReachableFrom_k.elims)
apply simp
apply (rule_tac x="aa" in exI)
apply simp
apply (rule_tac x="b" in exI)
apply simp
apply (rule ReachableFrom_k.init)
apply simp

apply simp


apply simp
apply (erule conjE | erule exE)+
apply (rule_tac x="s" in exI)
apply simp

apply (rule_tac x="s''" in exI)
apply simp
apply (drule_tac k="nat" and a="a" in ReachableFrom_k.step)
apply simp

apply simp
done


theorem (in exprSL) strongAn_exist:
assumes wf_Pi: "wf \<Pi>"
and bounded_diam: "\<forall>s s'. s' \<in> ReachableFrom (effS\<^isub>B \<Pi>) {s} \<longrightarrow> (\<exists>r. r \<le> d \<and> s' \<in> ReachableFromIn (effS\<^isub>B \<Pi>) {s} r)"
and isSafe: "\<forall>s \<in> ReachableFrom (effS\<^isub>B \<Pi>) {s. \<Pi>,s \<Turnstile> initF \<Pi>}. \<Pi>,s \<Turnstile> safeF \<Pi> (fst s)"
and correct_specF: "\<forall>s \<in> ReachableFrom (effS\<^isub>B \<Pi>) {s. \<Pi>,s \<Turnstile> initF \<Pi>}. (\<forall>Q. specF \<Pi> (fst s) = Some Q \<longrightarrow> \<Pi>,s \<Turnstile> Q)"
and anF_ispecF: "\<forall>p. anF \<Pi> p = Some (ispecF \<Pi> p d)"
shows "strongAn \<Pi>"
proof -


have ispecF_safeF_ReachableFromIn: "\<And>k s. \<Pi>,s \<Turnstile> ispecF \<Pi> (fst s) k \<Longrightarrow> \<Pi>,s \<Turnstile> safeF \<Pi> (fst s) \<Longrightarrow> fst s \<noteq> ipc \<Pi> \<Longrightarrow> (\<forall>l. l\<le>k \<longrightarrow> (\<forall>s' \<in> ReachableFromIn (effS\<^isub>B \<Pi>) {s} l. \<Pi>,s' \<Turnstile> ispecF \<Pi> (fst s') (k-l) \<and> \<Pi>,s' \<Turnstile> safeF \<Pi> (fst s')))" (is "\<And> z. PROP ?P z")
  proof -
  fix z
  show "PROP ?P z"
  proof (induct "z" rule: nat_less_induct, intro allI impI ballI)
      fix k s l s'
      assume hyp: "\<forall>k'<k. \<forall>s. \<Pi>,s \<Turnstile> ispecF \<Pi> (fst s) k' \<longrightarrow> \<Pi>,s \<Turnstile> safeF \<Pi> (fst s) \<longrightarrow> fst s \<noteq> ipc \<Pi> \<longrightarrow> (\<forall>l\<le>k'. (\<forall>s'\<in>ReachableFromIn (effS\<^isub>B \<Pi>) {s} l. \<Pi>,s' \<Turnstile> ispecF \<Pi> (fst s') (k' - l) \<and> \<Pi>,s' \<Turnstile> safeF \<Pi> (fst s')))"
      assume s_ispecF_k: "\<Pi>,s \<Turnstile> ispecF \<Pi> (fst s) k"
      assume s_safeF: "\<Pi>,s \<Turnstile> safeF \<Pi> (fst s)"
      assume s_not_ipc: "fst s \<noteq> ipc \<Pi>"
      assume l_k: "l \<le> k"
      assume s'_ReachableFromIn_l: "s' \<in> ReachableFromIn (effS\<^isub>B \<Pi>) {s} l"
      show "\<Pi>,s' \<Turnstile> ispecF \<Pi> (fst s') (k - l) \<and> \<Pi>,s' \<Turnstile> safeF \<Pi> (fst s')" (is ?s'_ispecF)
	proof (cases "l")
	  case 0 
	  from 0 s'_ReachableFromIn_l
	  have s_eq_s': "s = s'"
	    apply -
	    apply (erule ReachableFromIn_elims)
	    apply simp
	    apply simp
	    done
	  from 0 s_eq_s' s_ispecF_k s_safeF show "?s'_ispecF"
	    by simp
	next
	  case (Suc l')

	  from Suc have l'_l: "l = Suc l'"
	    by simp

	  from l'_l s'_ReachableFromIn_l
	  obtain s'' where s'_ReachableFromIn_l': "s' \<in> ReachableFromIn (effS\<^isub>B \<Pi>) {s''} l'"
            and s_s''_effSB: "(s,s'') \<in> (effS\<^isub>B \<Pi>)"
	    apply -
	    apply (drule k_lstep)
	    apply fastsimp
	    done
	
	    from l'_l l_k have l'_k: "l' < k"
	    by arith

	    from l'_k
	    obtain k' where k'_k: "k = Suc k'"
	      apply -
	      apply (case_tac "k::nat")
	      by arith

	    from k'_k l'_k have l'_k': "l' \<le> k'"
	      by arith

	  from k'_k l'_l have k_l_k'_l': "k - l = (k' - l')"
	    by arith

	  obtain p m where s_def: "s = (p,m)"
	    by fastsimp

	  obtain p' m' where s'_def: "s' = (p',m')"
	    by fastsimp
	  
	  obtain p'' m'' where s''_def: "s'' = (p'',m'')"
	    by fastsimp

	  from s_s''_effSB s_def s''_def
	  obtain B where p''_B_succsF_p: "(p'',B) \<in> set (succsF \<Pi> p)" 
          and s_B: "\<Pi>,s \<Turnstile> B" and s_s''_effS: "(s,s'') \<in> effS \<Pi>"
	    apply -
	    apply (simp add: effS\<^isub>B_def branch_def)
	    apply fastsimp
	    done

	  from p''_B_succsF_p
	  have p_not_final: "p \<notin> finals \<Pi>"
	    by (fastsimp simp add: finals_def)

	  from s_not_ipc s_def p_not_final specF_pos
	  have p_specF: "specF \<Pi> p = None"
	    by fastsimp

	  from s_ispecF_k k'_k have s''_safeF_ispecF: "\<Pi>,s'' \<Turnstile> \<Conj> [safeF \<Pi> p'', ispecF \<Pi> p'' k']"
	    proof -

	      from s_ispecF_k p_specF s_def k'_k p''_B_succsF_p s''_def
	      have s_B_Imp_wpF: "\<Pi>,s \<Turnstile> B \<Impl> wpF \<Pi> p p'' (\<Conj> [safeF \<Pi> p'', ispecF \<Pi> p'' k'])"
		apply -
		apply (drule_tac P="\<lambda> ispecF. \<Pi>,s \<Turnstile> ispecF" in subst[OF ispecF_def])
		apply (simp add: semConj)
		apply (erule_tac x="(p'',B)" in ballE)
		apply (simp add: split_def)
		apply simp
		done

	      from s_B s_B_Imp_wpF
	      have s_wpF: "\<Pi>,s \<Turnstile> wpF \<Pi> p p'' (\<Conj> [safeF \<Pi> p'', ispecF \<Pi> p'' k'])"
		apply -
		apply (drule semImpE)
		apply simp
		done

	      from wf_Pi s_wpF s_B p''_B_succsF_p s_def s''_def s_s''_effS s_wpF
	      show "?thesis"
		apply -
		apply (simp only:)
		apply (rule correctWpF)
		apply simp+
		done
	    qed

	  from s''_safeF_ispecF s''_def
	  have s''_ispecF: "\<Pi>,s'' \<Turnstile> ispecF \<Pi> (fst s'') k'"
	    by (simp add: semConj)

	  from s''_safeF_ispecF s''_def
	  have s''_safeF: "\<Pi>,s'' \<Turnstile> safeF \<Pi> (fst s'')"
	    by (simp add: semConj)

	  from p''_B_succsF_p wf_Pi ipc_not_succsF[where \<Pi>="\<Pi>"] have p''_not_ipc: "p'' \<noteq> ipc \<Pi>"
	    apply -
	    apply simp
	    apply (erule_tac x="p" in allE)
	    apply clarsimp
	    apply (simp add: in_set_conv_decomp)
	    apply (erule exE | erule conjE)+
	    apply simp
	    done
	    
	  from k'_k have k'_less_k: "k' < k"
	    by arith
	  
	  from hyp s''_ispecF s''_safeF k'_less_k p''_not_ipc l'_k' s'_ReachableFromIn_l' s''_def
	  have s'_ispecF_k'_l'_safeF: "\<Pi>,s' \<Turnstile> ispecF \<Pi> (fst s') (k' - l') \<and> \<Pi>,s' \<Turnstile> safeF \<Pi> (fst s')"
	    by fastsimp

	 from s'_ispecF_k'_l'_safeF k_l_k'_l' 
	 show "?s'_ispecF"  
	   by simp
       qed
     qed
   qed

have ReachableFromIn_ispecF: "\<And>k s. (\<forall>l. l\<le>k \<longrightarrow> (\<forall>s' \<in> ReachableFromIn (effS\<^isub>B \<Pi>) {s} l. \<Pi>,s' \<Turnstile> ispecF \<Pi> (fst s') (k-l))) \<Longrightarrow> fst s \<noteq> ipc \<Pi> \<Longrightarrow> \<Pi>,s \<Turnstile> ispecF \<Pi> (fst s) k"
  proof -
    fix k s
    assume l_k_ReachableFromIn_ispecF: "\<forall>l\<le>k. \<forall>s'\<in>ReachableFromIn (effS\<^isub>B \<Pi>) {s} l. \<Pi>,s' \<Turnstile> ispecF \<Pi> (fst s') (k - l)"
    assume s_not_ipc: "fst s \<noteq> ipc \<Pi>"
    have s_ReachableFromIn_0: "s \<in> ReachableFromIn (effS\<^isub>B \<Pi>) {s} 0"
      apply -
      apply (rule k_init)
      by simp

    from l_k_ReachableFromIn_ispecF s_ReachableFromIn_0
    show "\<Pi>,s \<Turnstile> ispecF \<Pi> (fst s) k"
      by fastsimp
  qed
      

have ispecF_d_inc: "\<And> s. \<Pi>,s \<Turnstile> safeF \<Pi> (fst s) \<Longrightarrow> \<Pi>,s \<Turnstile> ispecF \<Pi> (fst s) d \<Longrightarrow> \<Pi>,s \<Turnstile> ispecF \<Pi> (fst s) (d+1)"
proof -
  fix s
  assume s_safeF: "\<Pi>,s \<Turnstile> safeF \<Pi> (fst s)"
  assume s_ispecF_d: "\<Pi>,s \<Turnstile> ispecF \<Pi> (fst s) d"
  show "\<Pi>,s \<Turnstile> ispecF \<Pi> (fst s) (d+1)"
  proof (cases "specF \<Pi> (fst s)")
    case (Some Q)
    from Some s_ispecF_d show "?thesis"
      by (simp add: ispecF_def)
  next
    case None
    
    obtain p m where s_def: "s = (p,m)"
      by fastsimp

    from None s_def specF_pos[where \<Pi>="\<Pi>"] 
    have p_not_ipc: "p \<noteq> ipc \<Pi>"
      apply -
      apply (erule_tac x="p" in allE)
      apply simp
      done
    
    from None s_def specF_pos[where \<Pi>="\<Pi>"] 
    have p_not_final: "p \<notin> finals \<Pi>"
      apply -
      apply (erule_tac x="p" in allE)
      apply simp
      done

    from s_ispecF_d s_safeF s_def p_not_ipc
    have ReachableFromIn_ispecF_d: "\<forall>l \<le> d. \<forall>s' \<in> ReachableFromIn (effS\<^isub>B \<Pi>) {s} l. \<Pi>,s' \<Turnstile> ispecF \<Pi> (fst s') (d - l) 
                                                                               \<and> \<Pi>,s' \<Turnstile> safeF \<Pi> (fst s')"
      apply -
      apply (drule ispecF_safeF_ReachableFromIn)
      apply simp
      apply simp
      apply simp
      done

    have ReachableFromIn_ispecF_inc_d: 
    "\<And> k l s'. k = (d + 1) - l \<longrightarrow> l \<le> d + 1 \<longrightarrow> s' \<in> ReachableFromIn (effS\<^isub>B \<Pi>) {s} l \<longrightarrow> 
               \<Pi>,s' \<Turnstile> ispecF \<Pi> (fst s') ((d + 1) - l) \<and> \<Pi>,s' \<Turnstile> safeF \<Pi> (fst s')" (is "\<And> k. PROP ?P k")
      proof -
      fix z
      show "PROP ?P z"
	proof (induct "z" rule: nat_less_induct, intro impI)
	  fix k l s'
	  assume Hyp: "\<forall>k'<k. \<forall>l' s'. k' = d + 1 - l' \<longrightarrow>
          l' \<le> d + 1 \<longrightarrow> s' \<in> ReachableFromIn (effS\<^isub>B \<Pi>) {s} l' \<longrightarrow> \<Pi>,s' \<Turnstile> ispecF \<Pi> (fst s') (d + 1 - l') \<and> \<Pi>,s' \<Turnstile> safeF \<Pi> (fst s')"
	  assume k_d_l: "k = (d + 1) - l"
	  assume l_d: "l \<le> (d + 1)"
	  assume s'_ReachableFromIn_l: "s' \<in> ReachableFromIn (effS\<^isub>B \<Pi>) {s} l"
	  show "\<Pi>,s' \<Turnstile> ispecF \<Pi> (fst s') (d + 1 - l) \<and> \<Pi>,s' \<Turnstile> safeF \<Pi> (fst s')" (is "?s'_ispecF")
	    proof (cases k)
	      case 0
	      from 0 k_d_l have l_gr_d: "l > d"
		by arith

	      from s'_ReachableFromIn_l
	      have s'_ReachableFrom_s: "s' \<in> ReachableFrom (effS\<^isub>B \<Pi>) {s}"
		by (rule ReachableFromIn_ReachableFrom)

	      from bounded_diam s'_ReachableFrom_s
	      obtain r where r_le_d: "r \<le> d" 
              and s'_ReachableFromIn_r: "s' \<in> ReachableFromIn (effS\<^isub>B \<Pi>) {s} r"
		by fastsimp

	      from ReachableFromIn_ispecF_d r_le_d s'_ReachableFromIn_r
	      have s'_ispecF_d_r_safeF: "\<Pi>,s' \<Turnstile> ispecF \<Pi> (fst s') (d - r) \<and> \<Pi>,s' \<Turnstile> safeF \<Pi> (fst s')"
		by fastsimp

	      show "?s'_ispecF"
		proof (cases "specF \<Pi> (fst s')")
		  case (Some Q)
		  from Some s'_ispecF_d_r_safeF
		  show "?s'_ispecF"
		    by (simp add: ispecF_def)
		next
		  case None
		  from None 0 k_d_l[THEN sym] s'_ispecF_d_r_safeF show "?s'_ispecF"
		    by (simp add: ispecF_def semTrue)
		qed
	      next
		case (Suc k')
		from Suc have k'_k: "k = Suc k'"
		  by simp

		show "?s'_ispecF"
		  proof (cases "l")
		    case 0
		    from 0 s'_ReachableFromIn_l 
		    have s'_eq_s: "s' = s"
		      apply -
		      apply (erule ReachableFromIn_elims)
		      apply simp
		      apply simp
		      done

		    obtain p' m' where s'_def: "s' = (p',m')"
		      by fastsimp

		    from wf_Pi
		    have s'_B_wpF: "\<forall> (p'',B'') \<in> set (succsF \<Pi> p'). \<Pi>,s' \<Turnstile> B'' \<Impl> wpF \<Pi> p' p'' (\<Conj> [safeF \<Pi> p'', ispecF \<Pi> p'' k'])"
		      proof (intro ballI, simp add: split_paired_all s'_def, intro semImpI, assumption)
			fix p'' B''
			assume p''_B''_succsF_p': "(p'',B'') \<in> set (succsF \<Pi> p')"
			assume s'_B'': "\<Pi>,(p',m') \<Turnstile> B''"

			from wf_Pi p''_B''_succsF_p' s'_B'' s'_def
			obtain m'' where s'_s''_effS: "((p',m'),(p'',m'')) \<in> effS \<Pi>"
			  apply -
			  apply (drule succsFprogress)
			  apply simp+
			  apply (erule exE)
			  apply fastsimp
			  done

			obtain s'' where s''_def: "s'' = (p'',m'')"
			  by fastsimp

			have s''_ispecF_safeF: "\<Pi>,(p'',m'') \<Turnstile> ispecF \<Pi> p'' k' \<and> \<Pi>,(p'',m'') \<Turnstile> safeF \<Pi> p''"
			  proof -

			    from s'_s''_effS s'_def s''_def  s'_B'' p''_B''_succsF_p'
			    have s'_s''_effSB: "(s',s'') \<in> effS\<^isub>B \<Pi>"			  
			      by (fastsimp simp add: effS\<^isub>B_def branch_def)
			    
			    from 0 s'_eq_s s'_ReachableFromIn_l s'_s''_effSB
			    have s''_ReachableFromIn_1: "s'' \<in> ReachableFromIn (effS\<^isub>B \<Pi>) {s} 1"
			      apply -
			      apply (drule k_step)
			      apply simp
			      apply simp
			      done

			    from k'_k have k'_less_k: "k' < k"
			      by arith

			    from Hyp 0 k_d_l[THEN sym] k'_less_k k'_k s''_ReachableFromIn_1 s''_def
			    show s''_ispecF_safeF: "\<Pi>,(p'',m'') \<Turnstile> ispecF \<Pi> p'' k' \<and> \<Pi>,(p'',m'') \<Turnstile> safeF \<Pi> p''"
			      apply -
			      apply (erule_tac x="k'" in allE)
			      apply (drule mp, assumption)
			      apply (erule_tac x="1" in allE)
			      apply (erule_tac x="s''" in allE)
			      by fastsimp
			  qed

			  from s''_ispecF_safeF s''_def
			  have s''_safeF_ispecF: "\<Pi>,(p'',m'') \<Turnstile> \<Conj>[safeF \<Pi> p'', ispecF \<Pi> p'' k']"
			    by (simp add: semConj) 
			      
			from wf_Pi p''_B''_succsF_p' s'_B'' s_def s'_def s''_safeF_ispecF s'_s''_effS
			show "\<Pi>,(p',m') \<Turnstile> wpF \<Pi> p' p'' \<Conj>[safeF \<Pi> p'', ispecF \<Pi> p'' k']"
			  apply -
			  apply (rule completeWpF)
			  apply simp+
			  done
		      qed

		    from 0 s'_ReachableFromIn_l ReachableFromIn_ispecF_d  
		    have s'_safeF: "\<Pi>,s' \<Turnstile> safeF \<Pi> (fst s')"
		      by fastsimp

		    from None s'_eq_s k_d_l[THEN sym] k'_k s'_B_wpF s_def s'_def s'_safeF
		    show "?s'_ispecF"
		      apply -
		      apply (subst ispecF_def)
		      apply (simp add: semConj split_def)
		      done

		    next

		      case (Suc l')

		      from Suc have l'_l: "l = Suc l'"
			by simp

		      from k'_k k_d_l have l_le_d: "l \<le> d"
			by arith

		      from ReachableFromIn_ispecF_d l_le_d s'_ReachableFromIn_l
		      have s'_ispecF_d_safeF: "\<Pi>,s' \<Turnstile> ispecF \<Pi> (fst s') (d - l) \<and> \<Pi>,s' \<Turnstile> safeF \<Pi> (fst s')"
			by fastsimp

		      show "?s'_ispecF"
			proof (cases "specF \<Pi> (fst s')")
			  case (Some Q)
			  from Some s'_ispecF_d_safeF show "?s'_ispecF"
			    by (simp add: ispecF_def)
			next
			  case None

			  obtain p' m' where s'_def: "s' = (p',m')"
			    by fastsimp
			  
			  from wf_Pi
			  have s'_B_wpF: "\<forall> (p'',B'') \<in> set (succsF \<Pi> p'). \<Pi>,s' \<Turnstile> B'' \<Impl> wpF \<Pi> p' p'' (\<Conj> [safeF \<Pi> p'', ispecF \<Pi> p'' k'])"
			  proof (intro ballI, simp add: split_paired_all s'_def, intro semImpI, assumption)
			    fix p'' B''
			    assume p''_B''_succsF_p': "(p'',B'') \<in> set (succsF \<Pi> p')"
			    assume s'_B'': "\<Pi>,(p',m') \<Turnstile> B''"

			    from wf_Pi p''_B''_succsF_p' s'_B'' s'_def
			    obtain m'' where s'_s''_effS: "((p',m'),(p'',m'')) \<in> effS \<Pi>"
			      apply -
			      apply (drule succsFprogress)
			      apply simp+
			      apply (erule exE)
			      apply fastsimp
			      done

			    obtain s'' where s''_def: "s'' = (p'',m'')"
			      by fastsimp

			    have s''_ispecF_safeF: "\<Pi>,(p'',m'') \<Turnstile> ispecF \<Pi> p'' k' \<and> \<Pi>,(p'',m'') \<Turnstile> safeF \<Pi> p''"
			    proof -
			    
			    from s'_s''_effS s'_def s''_def  s'_B'' p''_B''_succsF_p'
			    have s'_s''_effSB: "(s',s'') \<in> effS\<^isub>B \<Pi>"			  
			      by (fastsimp simp add: effS\<^isub>B_def branch_def)
			    
			    have s'_ReachableFromIn_0: "s' \<in> ReachableFromIn (effS\<^isub>B \<Pi>) {s'} 0"
			      apply -
			      apply (rule k_init)
			      by simp

			    from s'_ReachableFromIn_l s'_s''_effSB
			    have s''_ReachableFromIn_inc_l: "s'' \<in> ReachableFromIn (effS\<^isub>B \<Pi>) {s} (l+1)"
			      apply -
			      apply (drule k_step)
			      apply simp
			      apply simp
			      done

			    from k'_k have k'_less_k: "k' < k"
			      by arith

			    from k'_k k_d_l have k'_d_l: "k' = d - l"
			      by arith

			    from Hyp k_d_l[THEN sym] k'_less_k k'_k k'_d_l l_le_d s''_ReachableFromIn_inc_l s''_def
			    show s''_ispecF_safeF: "\<Pi>,(p'',m'') \<Turnstile> ispecF \<Pi> p'' k' \<and> \<Pi>,(p'',m'') \<Turnstile> safeF \<Pi> p''"
			      apply -
			      apply (erule_tac x="k'" in allE)
			      apply (drule mp, assumption)
			      apply (erule_tac x="l + 1" in allE)
			      apply (erule_tac x="s''" in allE)
			      apply simp
			      done
			  qed

			  from s''_ispecF_safeF s''_def
			  have s''_safeF_ispecF: "\<Pi>,(p'',m'') \<Turnstile> \<Conj>[safeF \<Pi> p'', ispecF \<Pi> p'' k']"
			    by (simp add: semConj) 
			      
			from wf_Pi p''_B''_succsF_p' s'_B'' s_def s'_def s''_safeF_ispecF s'_s''_effS
			show "\<Pi>,(p',m') \<Turnstile> wpF \<Pi> p' p'' \<Conj>[safeF \<Pi> p'', ispecF \<Pi> p'' k']"
			  apply -
			  apply (rule completeWpF)
			  apply simp+
			  done
		      qed

		      from None s'_def s'_B_wpF k_d_l[THEN sym] k'_k s'_ispecF_d_safeF
		      show "?s'_ispecF"
			apply -
			apply (subst ispecF_def)
			apply (simp add: semConj split_def)
			done
		    qed
			
			
		    qed
		  qed
		qed
	      qed

		     
    have s_ReachableFromIn_0: "s \<in> ReachableFromIn  (effS\<^isub>B \<Pi>) {s} 0"
      apply -
      apply (rule k_init)
      by simp

    from s_ReachableFromIn_0 ReachableFromIn_ispecF_inc_d[where k="d + 1" and l="0"]
    show "?thesis"
      by simp
  qed
qed  
 

have correct_Starters: "\<And> s. s \<in> Starters \<Pi> \<Longrightarrow>  \<Pi>,s \<Turnstile> aF \<Pi> (fst s) \<and> \<Pi>,s \<Turnstile> safeF \<Pi> (fst s)"
 proof -
   fix s
   assume s_Starters: "s \<in> Starters \<Pi>"
   show "\<Pi>,s \<Turnstile> aF \<Pi> (fst s) \<and> \<Pi>,s \<Turnstile> safeF \<Pi> (fst s)"       
     proof (cases "\<Pi>,s \<Turnstile> initF \<Pi>")
      case True
      from True have s_initF: "\<Pi>,s \<Turnstile> initF \<Pi>"
	by assumption

      from s_initF have s_ReachableFrom: "s \<in> ReachableFrom (effS\<^isub>B \<Pi>) {s. \<Pi>,s \<Turnstile> initF \<Pi>}"
	apply -
	apply (rule ReachableFrom.init)
	by simp
	
      	
      from s_ReachableFrom isSafe
      have s_safeF: "\<Pi>,s \<Turnstile> safeF \<Pi> (fst s)"
	by fastsimp

      from wf_Pi s_initF have s_ipc: "fst s = (ipc \<Pi>)"
	by (rule initF_ipc)

      from s_ipc specF_pos
      obtain Q where Q_def: "specF \<Pi> (fst s) = Some Q"
	by fastsimp
      
      from Q_def anF_ispecF
      have aF_Q: "aF \<Pi> (fst s) = Q"
	apply -
	apply (simp add: aF_def ispecF_def)
	done
	

      from s_ReachableFrom correct_specF Q_def aF_Q
      have s_aF: "\<Pi>,s \<Turnstile> aF \<Pi> (fst s)"
	by fastsimp

      from s_safeF s_aF 
      show "\<Pi>,s \<Turnstile> aF \<Pi> (fst s) \<and> \<Pi>,s \<Turnstile> safeF \<Pi> (fst s)" 
	by simp
    next
      case False
      from False have s_not_initF: "\<not> \<Pi>,s \<Turnstile> initF \<Pi>"
	by assumption
      from s_not_initF s_Starters 
      obtain A where A_def: "anF \<Pi> (fst s) = Some A" and s_A: "\<Pi>,s \<Turnstile> A" and s_safeF: "\<Pi>,s \<Turnstile> safeF \<Pi> (fst s)"
	apply -
	apply (simp add: Starters_def)
	apply fastsimp
	done

      from A_def s_A s_safeF
      show "\<Pi>,s \<Turnstile> aF \<Pi> (fst s) \<and> \<Pi>,s \<Turnstile> safeF \<Pi> (fst s)" 
	by (simp add: aF_def)
    qed
  qed

from anF_ispecF
have in_Starters: "\<And>s. \<Pi>,s \<Turnstile> aF \<Pi> (fst s) \<Longrightarrow> \<Pi>,s \<Turnstile> safeF \<Pi> (fst s) \<Longrightarrow> s \<in> Starters \<Pi>"
  by (simp add: aF_def Starters_def)


have G1: "\<forall>s \<in> ReachableFrom (effS\<^isub>B \<Pi>) (Starters \<Pi>). \<Pi>,s \<Turnstile> aF \<Pi> (fst s) \<and> \<Pi>,s \<Turnstile> safeF \<Pi> (fst s)" (is ?G1)
 proof -
   have G2: "\<And>r. \<forall>s \<in> ReachableFromIn (effS\<^isub>B \<Pi>) (Starters \<Pi>) r. \<Pi>,s \<Turnstile> aF \<Pi> (fst s) \<and> \<Pi>,s \<Turnstile> safeF \<Pi> (fst s)" (is "\<And>r. PROP ?P r")
     proof -
       fix r
       show "PROP ?P r"
       proof (induct "r" rule: nat_less_induct)
	 case (1 n)
	 assume Hyp: "\<forall>m<n. \<forall>s\<in>ReachableFromIn (effS\<^isub>B \<Pi>) (Starters \<Pi>) m. \<Pi>,s \<Turnstile> aF \<Pi> (fst s) \<and> \<Pi>,s \<Turnstile> safeF \<Pi> (fst s)"
	 show "\<forall>s\<in>ReachableFromIn (effS\<^isub>B \<Pi>) (Starters \<Pi>) n. \<Pi>,s \<Turnstile> aF \<Pi> (fst s) \<and> \<Pi>,s \<Turnstile> safeF \<Pi> (fst s)"
	   proof (intro ballI impI)
	     fix s
	     assume s_ReachableFromIn_n: "s \<in> ReachableFromIn (effS\<^isub>B \<Pi>) (Starters \<Pi>) n" 
	     from s_ReachableFromIn_n 
	     have s_ReachableFrom: "s \<in> ReachableFrom (effS\<^isub>B \<Pi>) (Starters \<Pi>)"
	       by (rule ReachableFromIn_ReachableFrom)

	     show "\<Pi>,s \<Turnstile> aF \<Pi> (fst s) \<and> \<Pi>,s \<Turnstile> safeF \<Pi> (fst s)" (is ?G2')
	       proof (rule ReachableFromIn_elims[OF s_ReachableFromIn_n])
		 assume n_0: "n = 0"
		 assume s_Starters: "s \<in> Starters \<Pi>"
                 show "?G2'"
		   by (rule correct_Starters)
	       next
		 fix s' k'
		 assume n_k': "n = Suc k'"
		 assume s'_ReachableFromIn_k': "s' \<in> ReachableFromIn (effS\<^isub>B \<Pi>) (Starters \<Pi>) k'"
		 assume s'_s_effSB: "(s', s) \<in> effS\<^isub>B \<Pi>"
		 show "?G2'"
		   proof -

		     from Hyp n_k' s'_ReachableFromIn_k'
		     have s'_aF_safeF: "\<Pi>,s' \<Turnstile> aF \<Pi> (fst s') \<and> \<Pi>,s' \<Turnstile> safeF \<Pi> (fst s')"
		       by fastsimp

		     from s'_aF_safeF have s'_Starters: "s' \<in> Starters \<Pi>"
		       apply -
		       apply (rule in_Starters)
		       apply simp
		       apply simp
		       done
		     
		     from s'_s_effSB
		     obtain B where s'_s_succsF: "(fst s,B) \<in> set (succsF \<Pi> (fst s'))" and s'_B: "\<Pi>,s' \<Turnstile> B" and s'_s_effS: "(s',s) \<in> effS \<Pi>"
		       apply -
		       apply (simp add: effS\<^isub>B_def branch_def)
		       apply fastsimp
		       done

		     from s'_s_succsF 
		     have s'_not_final: "fst s' \<notin> finals \<Pi>"
		       apply -
		       apply (simp add: finals_def)
		       apply fastsimp
		       done
		       
		     from s'_aF_safeF anF_ispecF
		     have s'_ispecF: "\<Pi>,s' \<Turnstile> ispecF \<Pi> (fst s') (d+1)"
		       apply -
		       apply (rule ispecF_d_inc)
		       apply simp
		       apply (simp add: aF_def)
		       done 

		     show "?G2'"
		       proof (cases "fst s' = ipc \<Pi>")
			 case False
			 from False s'_not_final specF_pos
			 have s'_specF_None: "specF \<Pi> (fst s') = None"
			   by fastsimp

			 from s'_ispecF s'_specF_None s'_s_succsF
			 have s'_wp_ispecF: "\<Pi>,s' \<Turnstile> B \<Impl> wpF \<Pi> (fst s') (fst s) (\<Conj> [safeF \<Pi> (fst s),ispecF \<Pi> (fst s) d])"
			   apply -
			   apply (drule_tac P="\<lambda> ispecF. \<Pi>,s' \<Turnstile> ispecF" in subst[OF ispecF_def])
			   apply (simp add: semConj)
			   apply (erule_tac x="(fst s,B)" in ballE)
			   apply simp

			   apply simp
			   done

			 obtain p m where s_def: "s = (p,m)"
			   by fastsimp
			 
			 obtain p' m' where s'_def: "s' = (p',m')"
			   by fastsimp

			 from wf_Pi s'_s_effS s'_B s'_s_succsF s'_wp_ispecF s_def s'_def
			 have s_safeF_ispecF: "\<Pi>,s \<Turnstile> \<Conj> [safeF \<Pi> (fst s), ispecF \<Pi> (fst s) d]"
			   apply -
			   apply (simp only: fst_conv snd_conv)
			   apply (drule semImpE)
			   apply (rule correctWpF)
			   apply simp+
			   done

			 from s_safeF_ispecF anF_ispecF show "?G2'"
			   apply -
			   apply (simp add: aF_def semConj)
			   done

			 next

			   case True
			   from True have s'_ipc: "fst s' = ipc \<Pi>"
			     by assumption

			   from s'_ipc specF_ipc
			   have specF_s': "specF \<Pi> (fst s') = Some (initF \<Pi>)"
			     by simp


			   from specF_s' s'_ispecF
			   have s'_initF: "\<Pi>,s' \<Turnstile> (initF \<Pi>)"
			     by (simp add: ispecF_def)

			   from s'_initF
			   have s'_ReachableFrom: "s' \<in> ReachableFrom  (effS\<^isub>B \<Pi>) {s. \<Pi>,s \<Turnstile> initF \<Pi>}"
			     apply -
			     apply (rule ReachableFrom.init)
			     apply simp
			     done

			   from s'_initF s'_s_effSB s'_ReachableFrom
			   have s_ReachableFrom: "s \<in> ReachableFrom (effS\<^isub>B \<Pi>) {s. \<Pi>,s \<Turnstile> initF \<Pi>}"
			     apply -
			     apply (rule ReachableFrom.step)
			     apply simp
			     apply simp
			     done

			   from s_ReachableFrom isSafe
			   have s_safeF: "\<Pi>,s \<Turnstile> safeF \<Pi> (fst s)"
			     by fastsimp

			   have ispecF_trans: "\<And> k. \<forall> l. k = d -l \<longrightarrow> (\<forall> s''\<in> ReachableFromIn (effS\<^isub>B \<Pi>) {s} l. \<Pi>,s'' \<Turnstile> ispecF \<Pi> (fst s'') (d - l))" (is "\<And> k. PROP ?P k")
			     proof -
			     fix k
			     show "PROP ?P k"
			       proof (induct "k" rule: nat_less_induct, intro allI impI ballI)
				 fix n l s''
				 assume hyp: "\<forall>m<n. \<forall>l. m = d - l \<longrightarrow> (\<forall>s''\<in>ReachableFromIn (effS\<^isub>B \<Pi>) {s} l. \<Pi>,s'' \<Turnstile> ispecF \<Pi> (fst s'') (d - l))"
				 assume n_d_l: "n = d - l"
                                 assume s''_ReachableFromIn_l: "s'' \<in> ReachableFromIn (effS\<^isub>B \<Pi>) {s} l"
				 show "\<Pi>,s'' \<Turnstile> ispecF \<Pi> (fst s'') (d - l)" (is ?G2'')
				   proof (cases "specF \<Pi> (fst s'')")
				     case (Some Q)
				     from Some have ispecF_Q: "ispecF \<Pi> (fst s'') (d - l) = Q"
				       by (simp add: ispecF_def)
				    
				   

				     from s''_ReachableFromIn_l 
				     have s''_ReachableFrom_s: "s'' \<in> ReachableFrom (effS\<^isub>B \<Pi>) {s}"
				       by (rule ReachableFromIn_ReachableFrom)

				     from s_ReachableFrom s''_ReachableFrom_s
				     have s''_ReachableFrom: "s'' \<in> ReachableFrom (effS\<^isub>B \<Pi>) {s. \<Pi>,s \<Turnstile> initF \<Pi>}"
				       apply (rule ReachableFrom_trans)
				       done

				     from correct_specF s''_ReachableFrom Some ispecF_Q
				     show "?G2''"
				       by fastsimp
				   next
				     case None
				     from None have specF_s'': "specF \<Pi> (fst s'') = None"
				       by assumption

				     show "?G2''"
				       proof (cases "d - l")
					 case 0
					 from specF_s'' 0 show "?G2''"
					   apply -
					   apply (simp add:ispecF_def)
					   apply (rule semTrue)
					   done

				       next

					 case (Suc n')
					 have s''_wpF_ispecF: "\<Pi>,s'' \<Turnstile> \<Conj> (map (\<lambda>(p',B). B \<Impl> 
                                              (wpF \<Pi> (fst s'') p' (\<Conj> [safeF \<Pi> p',ispecF \<Pi> p' ((d - l) - 1)]))) (succsF \<Pi> (fst s'')))"
					   proof -
					     have s''_wpF_ispecF_p'_B: "\<And> p' B. (p',B) \<in> set (succsF \<Pi> (fst s'')) \<Longrightarrow> \<Pi>,s'' \<Turnstile>  B \<Impl> 
                                              (wpF \<Pi> (fst s'') p' (\<Conj> [safeF \<Pi> p',ispecF \<Pi> p' ((d - l) - 1)]))"
					       proof (intro semImpI wf_Pi)
						 fix p''' B'
						 assume p'''_B'_succsF: "(p''',B') \<in> set (succsF \<Pi> (fst s''))"
						 assume s''_B': "\<Pi>,s'' \<Turnstile> B'"
						 show "\<Pi>,s'' \<Turnstile> wpF \<Pi> (fst s'') p''' \<Conj>[safeF \<Pi> p''', ispecF \<Pi> p''' (d - l - 1)]" (is ?wpG)
						   proof -
						     obtain p'' m'' where s''_def: "s'' = (p'',m'')"
						       by fastsimp

						     from wf_Pi s''_B' p'''_B'_succsF s''_def
						     obtain m''' where s''_s'''_effS: "((p'',m''),(p''',m''')) \<in> (effS \<Pi>)"
						       apply -
						       apply (drule succsFprogress)
						       apply simp+
						       apply fastsimp
						       done

						     obtain s''' where s'''_def: "s''' = (p''',m''')"
						       by fastsimp

						     from s''_def s'''_def s''_s'''_effS s''_B' p'''_B'_succsF
						     have s''_s'''_effSB: "(s'',s''') \<in> (effS\<^isub>B \<Pi>)"
						       apply -
						       apply (simp add: effS\<^isub>B_def branch_def)
						       apply fastsimp
						       done

						     from s''_ReachableFromIn_l s''_s'''_effSB
						     have s'''_ReachableFromIn_l': "s''' \<in> ReachableFromIn (effS\<^isub>B \<Pi>) {s} (l+1)"
						       apply -
						       apply (rule k_step)
						       apply simp+
						       done

						     from s'''_ReachableFromIn_l' 
						     have s'''_ReachableFrom_s: "s''' \<in> ReachableFrom (effS\<^isub>B \<Pi>) {s}"
						       by (rule ReachableFromIn_ReachableFrom)

						     from  s'''_ReachableFrom_s s_ReachableFrom
						     have s'''_ReachableFrom: "s''' \<in> ReachableFrom (effS\<^isub>B \<Pi>) {s. \<Pi>,s \<Turnstile> initF \<Pi>}"
						       apply -
						       apply (rule ReachableFrom_trans)
						       apply simp
						       apply simp
						       done
						       

						     from s'''_ReachableFrom isSafe
						     have s'''_safeF: "\<Pi>,s''' \<Turnstile> safeF \<Pi> (fst s''')"
						       by fastsimp
						       

						     from hyp s'''_ReachableFromIn_l' Suc n_d_l
						     have s'''_ispecF: "\<Pi>,s''' \<Turnstile> ispecF \<Pi> (fst s''') (d - (l+1))"
						       apply -
						       apply (erule_tac x="d - (l+1)" in allE)
						       apply simp
						       apply (subgoal_tac "d - Suc l < d - l")
						        prefer 2
							apply arith
						       apply simp
						       done

						     from s'''_ispecF s'''_safeF s'''_def 
						     have s'''_safeF_ispecF: "\<Pi>, s''' \<Turnstile> \<Conj> [safeF \<Pi> p''',ispecF \<Pi> p''' (d - l - 1)]"
						       apply -
						       apply (simp add: semConj)
						       done

						    from wf_Pi p'''_B'_succsF s''_B' s''_s'''_effS s'''_safeF_ispecF s''_def s'''_def
						    show "?wpG"
						      apply -
						      apply (simp only: fst_conv snd_conv)
						      apply (rule completeWpF)
						      apply simp+
						      done
						  qed
						qed
						    
					
					     from s''_wpF_ispecF_p'_B
					     show ?thesis
					       apply -
					       apply (simp add: semConj split_def)
					       done
					   qed

					 from Suc s''_wpF_ispecF specF_s''
					 show "?G2''"
					   apply -
					   apply (simp add: ispecF_def)
					   done
				       qed
				     qed
				   qed
				 qed
				 
				 have s_ReachableFromIn_s: "s \<in> ReachableFromIn (effS\<^isub>B \<Pi>) {s} 0"
				   apply -
				   apply (rule k_init)
				   by simp
				   
				   

				 from s_ReachableFromIn_s ispecF_trans[where k=d]
				 have s_ispecF: "\<Pi>,s \<Turnstile> ispecF \<Pi> (fst s) d"
				   apply -
				   apply (erule_tac x="0" in allE)
				   apply simp
				   done

				 from s_safeF s_ispecF anF_ispecF
				 show "?G2'"
				   by (simp add: aF_def)
	       qed
	   qed
       qed
     qed
   qed
 qed
    
   show "?G1"
   proof (intro ballI impI)
     fix s
     assume s_ReachableFrom: "s \<in> ReachableFrom (effS\<^isub>B \<Pi>) (Starters \<Pi>)"
     show "\<Pi>,s \<Turnstile> aF \<Pi> (fst s) \<and> \<Pi>,s \<Turnstile> safeF \<Pi> (fst s)" (is ?G1')
       proof -
	 from s_ReachableFrom 
         obtain r where s_ReachableFromIn: "s \<in> ReachableFromIn (effS\<^isub>B \<Pi>) (Starters \<Pi>) r"
	   apply -
	   apply (drule ReachableFrom_ReachableFromIn)
	   apply fastsimp
	   done

	 from G2 s_ReachableFromIn
	 show "?G1'"
	   by fastsimp
       qed
     qed
   qed

from G1 show "strongAn \<Pi>"
  by (simp add: strongAn_def)
qed



end