theory JBC_Expressiveness
imports JBC_VCG_Completeness
begin

consts Expressiveness::"('a \<Rightarrow> (('b \<times> 'c) \<times> 'b \<times> 'c) set)
      \<Rightarrow> 'd \<Rightarrow> 'd \<Rightarrow> ('d list \<Rightarrow> 'd)
                  \<Rightarrow> ('d \<Rightarrow> 'd \<Rightarrow> 'd)
                    \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'c \<Rightarrow> 'd \<Rightarrow> bool)
                      \<Rightarrow> ('a \<Rightarrow> 'b list)
                        \<Rightarrow> ('a \<Rightarrow> 'b)
                          \<Rightarrow> ('a \<Rightarrow> 'b \<rightharpoonup> 'd)
                            \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'b ~~> 'd)
                              \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'd \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b \<rightharpoonup> 'd) \<Rightarrow> bool"

defs Expressiveness_def [simp]:
"Expressiveness \<equiv> exprSL"

lemma succsTyF_wpFcorrect:
assumes wf_Pi: "wf \<Pi>"
assumes p'_B_succsTyF: "(p',B) \<in> set (succsTyF \<Pi> p)"
assumes p_B: "\<Pi>,(p,\<sigma>,e) \<Turnstile> B"
assumes p_p'_effS: "((p,\<sigma>,e),(p',\<sigma>',e')) \<in> effS \<Pi>"
assumes p_wpF: "\<Pi>,(p,\<sigma>,e) \<Turnstile> wpF \<Pi> p p' Q"
shows "\<Pi>,(p',\<sigma>',e') \<Turnstile> Q"
(*<*)
proof -

obtain s where s_def: "s = (p,\<sigma>,e)"
 by fastsimp

obtain s' where s'_def: "s' = (p',\<sigma>',e')"
 by fastsimp

from p'_B_succsTyF p_B s_def
  have s_inv_Ty: "\<Pi>,s \<Turnstile> inv_Ty \<Pi> p"
    apply -
    apply (simp add: upg_def succsTyF_def split_def split del: option.split_asm)
    apply (erule imageE)
    apply simp
    done

  from p'_B_succsTyF p_B s_def
  have s_inv_ExTys: "\<Pi>,s \<Turnstile> inv_ExTys \<Pi> p"
    apply -
    apply (simp add: upg_def succsTyF_def succsExTysF_def split_def split del: option.split_asm)
    apply (erule imageE)+
    apply simp
    done

  from p'_B_succsTyF p_B s_def
  have s_inv_FrNr: "\<Pi>,s \<Turnstile> inv_FrNr \<Pi> p"
    apply -
    apply (simp add: upg_def succsTyF_def succsExTysF_def succsFrNrF_def split_def split del: option.split_asm)
    apply (erule imageE)+
    apply simp
    done

  from p'_B_succsTyF p_B s_def
  have s_inv_Pos: "\<Pi>,s \<Turnstile> inv_Pos \<Pi> p" 
    apply -
    apply (simp add: upg_def addPos_def succsTyF_def succsExTysF_def 
        succsFrNrF_def succsF_def split del: option.split_asm)
    apply (erule disjE)
    apply (erule imageE)+
    apply (simp add: split_def inv_Pos_def)
    apply (erule imageE)+
    apply (simp add: split_def inv_Pos_def)
    done



  from p'_B_succsTyF  p_B s_def
  obtain B' where p'_B'_succsF: "(p',B') \<in> set (succsF \<Pi> p)" and s_B': "\<Pi>,s \<Turnstile> B'"
    apply -
    apply (simp add: upg_def addPos_def succsTyF_def succsExTysF_def 
        succsFrNrF_def split del: option.split_asm)
    apply (erule imageE)+
    apply (simp add: split_def)
    apply fastsimp
    done

  from wf_Pi s_def s'_def s_inv_Pos s_inv_Ty s_inv_ExTys p'_B'_succsF s_B' p_p'_effS 
  have evalE_wpF: "evalE \<Pi> (p, \<sigma>, e) (wpF \<Pi> p p' Q) = evalE \<Pi> (p',\<sigma>',e') Q"
    apply -
    apply (subgoal_tac "\<forall> I. evalE \<Pi> (p, \<sigma>, e\<lparr>lv:= I\<rparr>) (wpF \<Pi> p p' Q) = evalE \<Pi> (p',\<sigma>',e'\<lparr>lv:= I\<rparr>) Q")
     prefer 2
     apply (rule_tac s="s" and s'="s'" in effS_wpF)
     apply (simp)+
    apply (erule_tac x="lv e" in allE)
    apply (subgoal_tac "e\<lparr>lv:= (lv e)\<rparr> = e")
     prefer 2
     apply simp
     apply (simp only:)
    apply (frule effS_lv_inv)
    apply (subgoal_tac "e'\<lparr>lv:= (lv e')\<rparr> = e'")
     prefer 2
     apply simp
    apply (simp only:)
    done

  from p_wpF evalE_wpF show ?thesis
    by simp
qed
(*>*)

constdefs finals::"jbc_prog \<Rightarrow> pos set"
"finals \<Pi> \<equiv> {p. p \<in> set (domC \<Pi>) \<and> \<not> (\<exists> p' B. (p',B) \<in> set (succsTyF \<Pi> p))}"

constdefs specF:: "jbc_prog \<Rightarrow> pos \<Rightarrow> expr option"
"specF \<Pi> p \<equiv>  (if p=ipc \<Pi> then Some (initF \<Pi>) 
               else (if (p \<in> finals \<Pi>) then Some (aF \<Pi> p)
                     else None))"

lemma specFpos:
"\<forall> \<Pi> p. p \<in> {ipc \<Pi>}\<union>finals \<Pi> = (specF \<Pi> p \<noteq> None)"
(*<*)
apply (rule allI)+
apply (rule iffI)
apply simp
apply (erule disjE)
apply (simp add: specF_def)
apply (simp add: specF_def)

apply (rule classical)
apply (simp add: specF_def)
done
(*>*)

lemma wf_ipc_succsF:
"wf \<Pi> \<Longrightarrow> p \<in> set (domC \<Pi>) \<Longrightarrow> ipc \<Pi> \<notin> set (map fst (succsF \<Pi> p))"
(*<*)
apply (simp add: in_set_conv_decomp)
apply (erule exE)+
apply (simp add: wf_def checkPos_split split add: split_if_asm)
apply (rule classical)
apply (simp add: succsF_def)
apply (erule imageE)
apply (simp add: addPos_append addPos_def)
apply (erule disjE)
apply (erule imageE)
apply (simp add: in_set_conv_decomp)
apply (erule exE)+
apply (simp add: split_def)

apply (erule imageE)
apply (simp add: in_set_conv_decomp)
apply (erule exE)+
apply (simp add: split_def)
done
(*>*)

lemma  wf_ipc_succsTyF:
"wf \<Pi> \<Longrightarrow> p \<in> set (domC \<Pi>) \<Longrightarrow> ipc \<Pi> \<notin> set (map fst (succsTyF \<Pi> p))"
(*<*)
apply (drule wf_ipc_succsF)
apply assumption

apply (rule classical)
apply simp
apply (erule imageE)
apply (simp add: succsTyF_def upg_def)
apply (erule imageE)
apply (simp add: succsExTysF_def upg_def)
apply (erule imageE)
apply (simp add: succsFrNrF_def upg_def)
apply (erule imageE)
apply (simp add: split_def)
done
(*>*)

lemma ExpressivenessIns: "Expressiveness effS TT FF And Imp valid domC ipc anF succsTyF wf initF wpF specF"
(*<*)
apply (simp only: Expressiveness_def)
apply (rule VCG_Completeness.exprSL.intro)
--{* SafetyLogic *} 
apply (rule SafetyLogicIns)
--{* CFG *}
apply (rule CFG_axioms_succsTyF)
--{* AbsSem *}
apply (cut_tac AbsSemIns)
apply (simp only: AbsSem_def)
--{* completeVCG *}
apply (cut_tac completeVCG_Ins_Ty)
apply (simp add: completeVCG_def)
--{* Expressiveness axioms *}
apply (simp only: exprSL_axioms_def)
apply (rule conjI)
apply (rule allI | rule impI)+
apply (subgoal_tac "\<exists> \<sigma> e. m = (\<sigma>,e)")
 prefer 2
 apply fastsimp
apply (subgoal_tac "\<exists> \<sigma>' e'. m' = (\<sigma>',e')")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (simp only: )
apply (rule_tac B="B" and \<sigma>'="\<sigma>'" and e'="e'" in succsTyF_wpFcorrect)
apply simp
apply simp
apply simp
apply simp
apply simp

--{* specFpos *}
apply (rule conjI)
apply (cut_tac specFpos)
apply (simp add: finals_def)

--{* specFipc *}
apply (rule conjI)
apply (simp add: specF_def)

--{* succsFipc *}
apply (rule allI | rule impI)+
apply (case_tac "p \<in> set (domC \<Pi>)")
apply (rule wf_ipc_succsTyF)
apply simp
apply simp

apply (rule classical)
apply simp
apply (erule imageE)
apply (subgoal_tac "\<exists> p' B. x = (p',B)")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (simp add: succsTyF_domC)
done
(*>*)

end