header {* 
  \isaheader{Annotated Control Flow Paths} 
*}

theory CFG = SafetyPolicy + AuxBox:

section {* Annotated Control Flow Graphs *}

consts enoughAn::"('prog \<Rightarrow> 'pos \<Rightarrow> ('pos\<times>'form) list) \<Rightarrow> 'prog \<Rightarrow> ('prog \<Rightarrow> 'pos \<Rightarrow> 'form option) \<Rightarrow> bool"

locale CFG = SafetyPolicy +

fixes domC:: "'prog \<Rightarrow> 'pos list"
fixes ipc::  "'prog \<Rightarrow> 'pos"

fixes anF:: "'prog \<Rightarrow> ('pos \<Rightarrow> 'form option)"
fixes aF::"'prog \<Rightarrow> 'pos \<Rightarrow> 'form"
defines "aF \<equiv> \<lambda> \<Pi> p. (case anF \<Pi> p of None \<Rightarrow> \<TrueF> | Some An \<Rightarrow> An)"
fixes domA:: "'prog \<Rightarrow> 'pos list"
defines "domA \<equiv> \<lambda> \<Pi>. [pc\<in> domC \<Pi>. (anF \<Pi> pc) \<noteq> None]"

fixes succsF:: "'prog  \<Rightarrow> 'pos \<Rightarrow> ('pos \<times> 'form) list"

fixes wf::" 'prog \<Rightarrow> bool"

assumes wf_anF:
"wf \<Pi> \<Longrightarrow> enoughAn succsF \<Pi> anF" 

fixes correctAn::"'prog \<Rightarrow> bool"
defines "correctAn \<equiv> \<lambda> \<Pi>. \<forall>s \<in> Reachables \<Pi>. \<Pi>,s \<Turnstile> aF \<Pi> (fst s)"

fixes saF::"'prog \<Rightarrow> 'pos \<Rightarrow> 'form"
defines
"saF \<equiv> \<lambda> \<Pi> p. \<Conj> [safeF \<Pi> p, aF \<Pi> p]"


section {* Auxiliary definitions *}

text {* This theory defines notions for paths and loops in a program. These are required to state the wellformedness condition wf Pi, 
which checks wether a program has at least one annotation per loop. *}

subsection {* Index of list elements *}

consts 
idx::"'a list \<Rightarrow> 'a \<Rightarrow> nat"

primrec 
"idx [] a = 0"
"idx (l#ls) a = (if l=a 
                 then 0
                 else Suc (idx ls a)
                )"

subsection {* Paths *}

text {* The set of all control flow paths of a given program *}

consts 
paths::"('a \<Rightarrow> ('a \<times> 'b) list) \<Rightarrow> ('a list) set"
inductive "(paths sc)"
intros
start: "\<lbrakk> (p',B) \<in> set (sc p) \<rbrakk> \<Longrightarrow> [p,p'] \<in> (paths sc)"
step: "\<lbrakk> l@[p] \<in> (paths sc); (p',B) \<in> set (sc p) \<rbrakk> \<Longrightarrow> l@[p]@[p'] \<in> (paths sc)"

(* deprecated
consts 
paths::" 'prog  \<Rightarrow> ( 'prog  \<Rightarrow> 'pos \<Rightarrow> ('pos \<times> 'form) list) \<Rightarrow> ('pos list) set"
inductive "(paths \<Pi> succsF')"
intros
start: "\<lbrakk> (pc',B) \<in> set (succsF' \<Pi> pc) \<rbrakk> \<Longrightarrow> [pc,pc'] \<in> (paths \<Pi> succsF')"
step: "\<lbrakk> l@[pc]\<in> (paths \<Pi> succsF') ; (pc',B) \<in> set (succsF' \<Pi> pc) \<rbrakk> \<Longrightarrow> l@[pc]@[pc'] \<in> (paths \<Pi> succsF')"
*)

subsection {* Cycles *}

text {* A path is a cycle if the first position equals the last position. *}

constdefs 
isCycle::"('prog \<Rightarrow> 'pos \<Rightarrow> ('pos\<times>'form) list) \<Rightarrow>  'prog  \<Rightarrow> ('pos list) \<Rightarrow> bool"
"isCycle succsF \<Pi> l \<equiv> (l\<in> paths (succsF \<Pi>) \<and> (hd l = last l))"


constdefs noAnn::"'pos list \<Rightarrow> ('pos \<Rightarrow> 'form option) \<Rightarrow> bool"
"noAnn l pan \<equiv> (\<forall> p. p\<in> set l \<longrightarrow> pan p = None)"

defs enoughAn_def:
"enoughAn succsF \<Pi> an \<equiv> (\<forall> l. isCycle succsF \<Pi> l \<longrightarrow> \<not> (noAnn l (an \<Pi>)))"


constdefs noAnnOnWay::"('prog \<Rightarrow> 'pos \<Rightarrow> ('pos\<times>'form) list) \<Rightarrow> 
('prog \<Rightarrow> 'pos \<Rightarrow> 'form option) \<Rightarrow> 'prog  \<Rightarrow> 'pos \<Rightarrow> 'pos \<Rightarrow> bool"
"noAnnOnWay succsF an \<Pi> pc pc' \<equiv> \<exists> l. ((pc#l)@[pc'])\<in>(paths (succsF \<Pi>)) \<and> (noAnn (pc#l) (an \<Pi>))"


section {* Lemmas *}

lemma idx_nth:
"a\<in> set l \<Longrightarrow> l!(idx l a) = a"
by (induct l, auto)

lemma idx_not_nth:
"a \<notin> set l \<Longrightarrow> idx l a = length l"
by (induct l, auto)

lemma paths_append:
"\<lbrakk> ps@(p#ps') \<in> paths (succsF \<Pi>); ps \<noteq> []; ps' \<noteq> [] \<rbrakk> \<Longrightarrow> (p#ps') \<in> (paths (succsF \<Pi>))"
(*<*)
apply (induct ps' rule: rev_induct)
apply simp
apply atomize
apply (erule paths.elims)
apply simp
apply (case_tac "ps")
apply simp
apply simp

apply simp
apply (case_tac "xs")
apply simp
apply (rule paths.start)
apply simp

apply simp
apply (rule_tac xs="list" in rev_cases)
apply simp
apply (subgoal_tac "([p]@[pa]@[p']) \<in> paths (succsF \<Pi>)")
 prefer 2
 apply (rule paths.step)
 apply simp
 apply simp
apply simp

apply simp
apply (subgoal_tac "(p # a # ys) @ [pa] @ [p'] \<in> paths (succsF \<Pi>)")
 prefer 2
 apply (rule paths.step)
 apply simp
 apply simp
apply simp
done
(*>*)

lemma path_succsF:
"\<lbrakk> l \<in> paths (succsF \<Pi>); k+1<length l \<rbrakk> \<Longrightarrow> \<exists>B. (l!(k+1),B) \<in> set (succsF \<Pi> (l!k))"
(*<*)
apply (rotate_tac 1)
apply (erule rev_mp)
apply (rule_tac  sc="succsF  \<Pi>" in paths.induct)
apply assumption
apply simp
apply (rule impI)
apply (rule_tac x="B" in exI)
apply assumption

apply (case_tac "k= length (la)")
apply simp
apply (rule_tac x="B" in exI)
apply (simp add: nth_append)

apply (case_tac "k + 1 = length la")
apply (simp add: nth_append)
apply (simp add: nth_append)
done 
(*>*)

lemma less_chain_simp:
"\<lbrakk> \<forall>k. length l <= k+1 \<or> idx L (l!k) < idx L (l!(k+1)); 1 < length (l::'pos  list) \<rbrakk> \<Longrightarrow> idx L (hd l) < idx L (last l)"
(*<*)
apply (erule rev_mp)
apply (erule rev_mp)
apply (induct l)
apply simp
apply (case_tac l)
apply simp
apply (case_tac list)
apply simp
apply (rule impI)
apply (erule_tac x="0" in allE)
apply simp
apply (rule impI)
apply (rule impI)
apply hypsubst
apply simp
apply (rule conjI)
apply (rule impI)
apply simp
apply (frule_tac x="0" and P="\<lambda> k. Suc (Suc 0) <= k \<or> (?Q k)" in spec)
apply (frule_tac x="1" and P="\<lambda> k. Suc (Suc 0) <= k \<or> (?Q k)" in spec)
apply simp

apply (frule_tac x="0" and P="\<lambda> k. Suc (Suc (length lista)) <= k \<or> (?Q k)" in spec)
apply simp
apply (rule impI)
apply simp
apply (subgoal_tac "(\<forall>k. Suc (length lista) \<le> k \<or> idx L ((aa # ab # lista) ! k) < idx L ((ab # lista) ! k))")
 prefer 2
 apply (rule allI)
 apply (case_tac "Suc (length lista) \<le> k")
 apply simp
 apply (erule_tac x="Suc k" in allE)
 apply simp
apply simp
done 
(*>*)

lemma path_length:
"\<lbrakk> l \<in> paths (succsF \<Pi>) \<rbrakk> \<Longrightarrow> 1 < length l"
(*<*)
apply (rule_tac sc="succsF \<Pi>" in paths.induct)
apply assumption
apply simp
apply simp
done
(*>*)

lemma loop_has_back_jump:
"\<lbrakk> l \<in> paths (succsF \<Pi>); hd l = last l \<rbrakk> \<Longrightarrow> \<exists>k. (k+1)<length l \<and> idx L (l!(k+1)) <= idx L (l!k)"
(*<*)
apply (frule path_length)
apply (rule classical)
apply (simp only: not_ex)
apply (simp only: de_Morgan_conj)
apply (simp only: linorder_not_less linorder_not_le)
apply (drule less_chain_simp)
apply simp
apply simp
done
(*>*)

(*<*)
lemma noAnn_ext:
"\<lbrakk> noAnn l pan; pan p = None \<rbrakk> \<Longrightarrow> noAnn (l@[p]) pan"
apply (unfold noAnn_def)
apply (rule allI)
apply (rule impI)
apply (simp only: set_append)
apply (case_tac "pa \<in> set l")
apply (erule_tac x="pa" in  allE)
apply (drule mp)
apply assumption
apply assumption
apply simp
done
(*>*)

(*<*)
lemma noAnn_conv:
"noAnn V aF = (\<forall> p \<in> set V. aF p = None)"
apply (simp add: noAnn_def)
apply blast
done
(*>*)

end