Theory IFC

section ‹Definitions›

text ‹
This section contains all necessary definitions of this development. Section~\ref{sec:pm} contains 
the structural definition of our program model which includes the security specification as well 
as abstractions of control flow and data.  Executions of our program model are defined in 
section~\ref{sec:ex}.  Additional well-formedness properties are defined in section~\ref{sec:wf}. 
Our security property is defined in section~\ref{sec:sec}.  Our characterisation of how information
is propagated by executions of our program model is defined in section~\ref{sec:char-cp}, for which
the correctness result can be found in section~\ref{sec:cor-cp}.  Section~\ref{sec:char-scp} contains
an additional approximation of this characterisation whose correctness result can be found in 
section~\ref{sec:cor-scp}.
›


theory IFC
  imports Main
begin

subsection ‹Program Model›
text_raw ‹\label{sec:pm}›

text ‹Our program model contains all necessary components for the remaining development and consists of:›

record ('n, 'var, 'val, 'obs) ifc_problem =  
― ‹A set of nodes representing program locations:›
  nodes :: ‹'n set›
― ‹An initial node where all executions start:›
  entry :: ‹'n›
― ‹A final node where executions can terminate:›
  return :: ‹'n›
― ‹An abstraction of control flow in the form of an edge relation:›
  edges :: ‹('n × 'n) set›
― ‹An abstraction of variables written at program locations:›
  writes :: ‹'n ⇒ 'var set›
― ‹An abstraction of variables read at program locations:›
  reads :: ‹'n ⇒ 'var set›
― ‹A set of variables containing the confidential information in the initial state:›
  hvars :: ‹'var set›
― ‹A step function on location state pairs:›
  step :: ‹('n × ('var ⇒ 'val)) ⇒ ('n × ('var ⇒ 'val))›
― ‹An attacker model producing observations based on the reached state at certain locations:›
  att :: ‹'n ⇀ (('var ⇒ 'val) ⇒ 'obs)›

text ‹We fix a program in the following in order to define the central concepts.  
The necessary well-formedness assumptions will be made in section~\ref{sec:wf}.›
locale IFC_def =
fixes prob :: ‹('n, 'var, 'val, 'obs) ifc_problem›
begin  

text ‹Some short hands to the components of the program which we will utilise exclusively in the following.›
definition nodes where ‹nodes = ifc_problem.nodes prob›
definition entry where ‹entry = ifc_problem.entry prob›
definition return where ‹return = ifc_problem.return prob›
definition edges where ‹edges = ifc_problem.edges prob›
definition writes where ‹writes = ifc_problem.writes prob›
definition reads where ‹reads = ifc_problem.reads prob›
definition hvars where ‹hvars = ifc_problem.hvars prob›
definition step where ‹step = ifc_problem.step prob›
definition att where ‹att = ifc_problem.att prob›

text ‹The components of the step function for convenience.›
definition suc where ‹suc n σ = fst (step (n, σ))›
definition sem where ‹sem n σ = snd (step (n, σ))›

lemma step_suc_sem: ‹step (n,σ) = (suc n σ, sem n σ)› unfolding suc_def sem_def by auto


subsubsection ‹Executions›
text ‹\label{sec:ex}›
text ‹In order to define what it means for a program to be well-formed, we first require concepts 
of executions and program paths.›

text ‹The sequence of nodes visited by the execution corresponding to an input state.›
definition path where
‹path σ k= fst ((step^^k) (entry,σ))›

text ‹The sequence of states visited by the execution corresponding to an input state.›
definition kth_state ( ‹_⇗_⇖› [111,111] 110) where 
‹σ⇗k⇖ = snd ((step^^k) (entry,σ))›

text ‹A predicate asserting that a sequence of nodes is a valid program path according to the
control flow graph.›

definition is_path where
‹is_path π = (∀ n. (π n, π (Suc n)) ∈ edges)› 
end

subsubsection ‹Well-formed Programs›
text_raw ‹\label{sec:wf}›

text ‹The following assumptions define our notion of valid programs.›
locale IFC = IFC_def ‹prob› for prob:: ‹('n, 'var, 'val, 'out) ifc_problem› +
assumes ret_is_node[simp,intro]: ‹return ∈ nodes›
and entry_is_node[simp,intro]: ‹entry ∈ nodes›
and writes: ‹⋀ v n. (∃σ. σ v ≠ sem n σ v) ⟹ v ∈ writes n›
and writes_return: ‹writes return = {}›
and uses_writes: ‹⋀ n σ σ'. (∀ v ∈ reads n. σ v = σ' v) ⟹ ∀ v ∈ writes n. sem n σ v = sem n σ' v›
and uses_suc: ‹⋀ n σ σ'. (∀ v ∈ reads n. σ v = σ' v) ⟹ suc n σ = suc n σ'›
and uses_att: ‹⋀ n f σ σ'. att n = Some f ⟹ (∀ v ∈ reads n. σ v = σ' v) ⟹ f σ = f σ'›
and edges_complete[intro,simp]: ‹⋀m σ. m ∈ nodes ⟹ (m,suc m σ) ∈ edges›
and edges_return : ‹⋀x. (return,x) ∈ edges ⟹ x = return ›
and edges_nodes: ‹edges ⊆ nodes × nodes›    
and reaching_ret: ‹⋀ x. x ∈ nodes ⟹ ∃ π n. is_path π ∧ π 0 = x ∧ π n = return›


subsection ‹Security›
text_raw ‹\label{sec:sec}›

text ‹We define our notion of security, which corresponds to what Bohannon et al.~\<^cite>‹"Bohannon:2009:RN:1653662.1653673"› 
refer to as indistinguishable security.  In order to do so we require notions of observations made
by the attacker, termination and equivalence of input states.›

context IFC_def
begin

subsubsection ‹Observations›
text_raw ‹\label{sec:obs}›

text ‹The observation made at a given index within an execution.›
definition obsp where
‹obsp σ k = (case att(path σ k) of Some f ⇒ Some (f (σ⇗k⇖)) | None ⇒ None)›

text ‹The indices within a path where an observation is made.›
definition obs_ids :: ‹(nat ⇒ 'n) ⇒ nat set› where
‹obs_ids π = {k. att (π k) ≠ None}›

text ‹A predicate relating an observable index to the number of observations made before.›
definition is_kth_obs :: ‹(nat ⇒ 'n) ⇒ nat ⇒ nat ⇒ bool›where
‹is_kth_obs π k i = (card (obs_ids π ∩ {..<i}) = k ∧ att (π i) ≠  None)›

text ‹The final sequence of observations made for an execution.›
definition obs where
‹obs σ k = (if (∃i. is_kth_obs (path σ) k i) then obsp σ (THE i. is_kth_obs (path σ) k i) else None)›

text ‹Comparability of observations.›
definition obs_prefix :: ‹(nat ⇒ 'obs option) ⇒ (nat ⇒ 'obs option) ⇒ bool› (infix ‹≲› 50) where
‹a ≲ b ≡ ∀ i. a i ≠ None ⟶ a i = b i›

definition obs_comp (infix ‹≈› 50) where
‹a ≈ b ≡ a ≲ b ∨ b ≲ a›

subsubsection ‹Low equivalence of input states›

definition restrict (infix ‹↾› 100 ) where
‹f↾U = (λ n. if n ∈ U then f n else undefined)›

text ‹Two input states are low equivalent if they coincide on the non high variables.›
definition loweq (infix ‹=⇩L› 50) 
where ‹σ =⇩L σ' = (σ↾(-hvars) = σ'↾(-hvars))›

subsubsection ‹Termination›

text ‹An execution terminates iff it reaches the terminal node at any point.›
definition terminates where
‹terminates σ ≡ ∃ i. path σ i = return›


subsubsection ‹Security Property›
text ‹The fixed program is secure if and only if for all pairs of low equivalent inputs the observation
sequences are comparable and if the execution for an input state terminates then the observation sequence 
is not missing any observations.›

definition secure where
‹secure ≡ ∀ σ σ'. σ =⇩L σ' ⟶ (obs σ ≈ obs σ' ∧ (terminates σ ⟶ obs σ' ≲ obs σ))›



subsection ‹Characterisation of Information Flows›
text ‹We now define our characterisation of information flows which tracks data and control dependencies 
within executions. To do so we first require some additional concepts.›

subsubsection ‹Post Dominance›
text ‹We utilise the post dominance relation in order to define control dependence.›

text ‹The basic post dominance relation.›
definition is_pd (infix ‹pd→› 50) where 
‹y pd→ x ⟷ x ∈ nodes ∧ (∀ π n. is_path π ∧ π (0::nat) = x ∧ π n = return ⟶ (∃k≤n. π k = y))›

text ‹The immediate post dominance relation.›
definition is_ipd (infix ‹ipd→› 50)where
‹y ipd→ x ⟷ x ≠ y ∧ y pd→ x ∧ (∀ z. z≠x ∧ z pd→ x ⟶ z pd→ y)›

definition ipd where 
‹ipd x = (THE y. y ipd→ x)›

text ‹The post dominance tree.›
definition pdt where
‹pdt = {(x,y). x≠y ∧ y pd→ x}›


subsubsection ‹Control Dependence›

text ‹An index on an execution path is control dependent upon another if the path does not visit
the immediate post domiator of the node reached by the smaller index.›
definition is_cdi (‹_ cd⇗_⇖→ _› [51,51,51]50) where
‹i cd⇗π⇖→ k ⟷ is_path π ∧ k < i ∧ π i ≠ return ∧ (∀ j ∈ {k..i}. π j ≠ ipd (π k))› 

text ‹The largest control dependency of an index is the immediate control dependency.›
definition is_icdi (‹_ icd⇗_⇖→ _› [51,51,51]50) where
‹n icd⇗π⇖→ n' ⟷ is_path π ∧ n cd⇗π⇖→ n' ∧ (∀ m ∈ {n'<..<n}.¬ n cd⇗π⇖→ m)›

text ‹For the definition of the control slice, which we will define next, we require the uniqueness 
of the immediate control dependency.›

lemma icd_uniq: assumes  ‹m icd⇗π⇖→ n› ‹ m icd⇗π⇖→ n'› shows ‹n = n'›
proof - 
  {
    fix n n' assume *: ‹m icd⇗π⇖→ n› ‹ m icd⇗π⇖→ n'› ‹n < n'›
    have ‹n'<m› using * unfolding is_icdi_def is_cdi_def by auto    
    hence ‹¬ m cd⇗π⇖→ n'› using * unfolding is_icdi_def by auto
    with *(2) have ‹False› unfolding is_icdi_def by auto
  }
  thus ?thesis using assms by (metis linorder_neqE_nat)
qed


subsubsection ‹Control Slice›
text ‹We utilise the control slice, that is the sequence of nodes visited by the control dependencies 
of an index, to match indices between executions.›

function cs:: ‹(nat ⇒ 'n) ⇒ nat ⇒ 'n list› (‹cs⇗_⇖ _› [51,70] 71) where
‹cs⇗π⇖ n = (if (∃ m. n icd⇗π⇖→ m) then (cs π (THE m. n icd⇗π⇖→ m))@[π n] else [π n])› 
by pat_completeness auto  
termination ‹cs› proof
  show ‹wf (measure snd)› by simp
  fix π n  
  define m where ‹m == (The (is_icdi n π))›
  assume ‹Ex (is_icdi n π)› 
  hence ‹n icd⇗π⇖→ m› unfolding m_def by (metis (full_types) icd_uniq theI')
  hence ‹m < n› unfolding is_icdi_def is_cdi_def by simp
  thus ‹((π, The (is_icdi n π)), π, n) ∈ measure snd› by (metis in_measure m_def snd_conv)
qed

inductive cs_less (infix ‹≺› 50) where
‹length xs < length ys ⟹ take (length xs) ys = xs  ⟹ xs ≺ ys›     

definition cs_select (infix ‹¡› 50) where
‹π¡xs = (THE k. cs⇗π⇖ k = xs)›


subsubsection ‹Data Dependence›

text ‹Data dependence is defined straight forward. An index is data dependent upon another, 
if the index reads a variable written by the earlier index and the variable in question has not 
been written by any index in between.›
definition is_ddi (‹_ dd⇗_,_⇖→ _› [51,51,51,51] 50) where
‹n dd⇗π,v⇖→ m ⟷ is_path π ∧ m < n ∧ v ∈ reads (π n) ∩ (writes (π m)) ∧ (∀ l ∈ {m<..<n}. v ∉ writes (π l))›



subsubsection ‹Characterisation via Critical Paths›
text_raw ‹\label{sec:char-cp}›
text ‹With the above we define the set of critical paths which as we will prove characterise the matching
points in executions where diverging data is read.›

inductive_set cp where

― ‹Any pair of low equivalent input states and indices where a diverging high variable is first
read is critical.›

‹⟦σ =⇩L σ'; 
  cs⇗path σ⇖ n = cs⇗path σ'⇖ n'; 
  h ∈ reads(path σ n); 
  (σ⇗n⇖) h ≠ (σ'⇗n'⇖) h; 
  ∀ k<n. h∉writes(path σ k); 
  ∀ k'<n'. h∉writes(path σ' k')
 ⟧ ⟹ ((σ,n),(σ',n')) ∈ cp› |

― ‹If from a pair of critical indices in two executions there exist data dependencies from both
indices to a pair of matching indices where the variable diverges, the later pair of indices is critical.›

‹⟦((σ,k),(σ',k')) ∈ cp; 
  n dd⇗path σ,v⇖→ k;
  n' dd⇗path σ',v⇖→ k'; 
  cs⇗path σ⇖ n = cs⇗path σ'⇖ n'; 
  (σ⇗n⇖) v ≠ (σ'⇗n'⇖) v
 ⟧ ⟹ ((σ,n),(σ',n')) ∈ cp› |

― ‹If from a pair of critical indices the executions take different branches and one of the critical 
indices is a control dependency of an index that is data dependency of a matched index where diverging 
data is read and the variable in question is not written by the other execution after the executions
first reached matching indices again, then the later matching pair of indices is critical.›

‹⟦((σ,k),(σ',k')) ∈ cp; 
  n dd⇗path σ,v⇖→ l; 
  l cd⇗path σ⇖→ k; 
  cs⇗path σ⇖ n = cs⇗path σ'⇖ n'; 
  path σ (Suc k) ≠ path σ' (Suc k'); 
  (σ⇗n⇖) v ≠ (σ'⇗n'⇖) v; 
  ∀j'∈{(LEAST i'. k' < i' ∧ (∃i. cs⇗path σ⇖ i = cs⇗path σ'⇖ i'))..<n'}. v∉writes (path σ' j')
 ⟧ ⟹ ((σ,n),(σ',n')) ∈ cp› | 

― ‹The relation is symmetric.›

‹⟦((σ,k),(σ',k')) ∈ cp⟧ ⟹ ((σ',k'),(σ,k)) ∈ cp›


text ‹Based on the set of critical paths, the critical observable paths are those that either directly 
reach observable nodes or are diverging control dependencies of an observable index.›

inductive_set cop where
‹⟦((σ,n),(σ',n')) ∈ cp;
  path σ n ∈ dom att
 ⟧ ⟹ ((σ,n),(σ',n')) ∈ cop› |

‹⟦((σ,k),(σ',k')) ∈ cp; 
  n cd⇗path σ⇖→ k; 
  path σ (Suc k) ≠ path σ' (Suc k'); 
  path σ n ∈ dom att
 ⟧ ⟹ ((σ,n),(σ',k')) ∈ cop›



subsubsection ‹Approximation via Single Critical Paths›
text_raw ‹\label{sec:char-scp}›

text ‹For applications we also define a single execution approximation.›

definition is_dcdi_via (‹_ dcd⇗_,_⇖→ _ via _ _› [51,51,51,51,51,51] 50) where
‹n dcd⇗π,v⇖→ m via π' m' = (is_path π ∧ m < n ∧ (∃ l' n'. cs⇗π⇖ m = cs⇗π'⇖ m' ∧ cs⇗π⇖ n = cs⇗π'⇖ n' ∧ n' dd⇗π',v⇖→ l' ∧ l' cd⇗π'⇖→ m') ∧ (∀ l ∈ {m..<n}. v∉ writes(π l)))›

inductive_set scp where
‹⟦h ∈ hvars; h ∈ reads (path σ n); (∀ k<n. h∉ writes(path σ k))⟧ ⟹ (path σ,n) ∈ scp› |
‹⟦(π,m) ∈ scp; n cd⇗π⇖→ m⟧ ⟹ (π,n) ∈ scp›|
‹⟦(π,m) ∈ scp; n dd⇗π,v⇖→ m⟧ ⟹ (π,n) ∈ scp›|
‹⟦(π,m) ∈ scp; (π',m') ∈ scp; n dcd⇗π,v⇖→ m via π' m'⟧ ⟹ (π,n) ∈ scp›

inductive_set scop where
‹⟦(π,n) ∈ scp; π n ∈ dom att⟧ ⟹ (π,n) ∈ scop›



subsubsection ‹Further Definitions›
text ‹The following concepts are utilised by the proofs.›

inductive contradicts (infix ‹𝔠› 50) where
‹⟦cs⇗π'⇖ k' ≺ cs⇗π⇖ k ; π = path σ;  π' = path σ' ; π (Suc (π¡cs⇗π'⇖ k')) ≠ π' (Suc k')⟧ ⟹ (σ', k') 𝔠 (σ, k)›|
‹⟦cs⇗π'⇖ k' = cs⇗π⇖ k ; π = path σ;  π' = path σ' ; σ⇗k⇖ ↾ (reads (π k)) ≠ σ'⇗k'⇖ ↾ (reads (π k))⟧ ⟹ (σ',k') 𝔠 (σ,k)›

definition path_shift (infixl ‹«› 51) where 
[simp]: ‹π«m = (λ n. π (m+n))› 

definition path_append :: ‹(nat ⇒ 'n) ⇒ nat ⇒ (nat ⇒ 'n) ⇒ (nat ⇒ 'n)› (‹_ @⇗_⇖ _› [0,0,999] 51) where
[simp]: ‹π @⇗m⇖ π' = (λn.(if n ≤ m then π n else π' (n-m)))› 

definition eq_up_to :: ‹(nat ⇒ 'n) ⇒ nat ⇒ (nat ⇒ 'n) ⇒ bool› (‹_ =⇘_⇙ _› [55,55,55] 50) where
‹π =⇘k⇙ π' = (∀ i ≤ k. π i = π' i)›

end (* End of locale IFC_def *)




section ‹Proofs›
text_raw ‹\label{sec:proofs}›

subsection ‹Miscellaneous Facts›

lemma option_neq_cases: assumes ‹x ≠ y› obtains (none1) a where ‹x = None› ‹y = Some a› | (none2) a where ‹x = Some a› ‹y = None› | (some) a b where ‹x = Some a› ‹y = Some b› ‹a ≠ b› using assms by fastforce

lemmas nat_sym_cases[case_names less sym eq] = linorder_less_wlog

lemma mod_bound_instance: assumes ‹j < (i::nat)› obtains j' where ‹k < j'› and ‹j' mod i = j›  proof -
  have ‹k < Suc k * i + j› using assms less_imp_Suc_add by fastforce
  moreover
  have ‹(Suc k * i + j) mod i = j› by (metis assms mod_less mod_mult_self3) 
  ultimately show ‹thesis› using that by auto
qed

lemma list_neq_prefix_cases: assumes ‹ls ≠ ls'› and ‹ls ≠ Nil› and ‹ls' ≠ Nil›
  obtains (diverge) xs x x' ys ys' where ‹ls = xs@[x]@ys› ‹ls' = xs@[x']@ys'› ‹x ≠ x'› |
   (prefix1) xs where ‹ls = ls'@xs› and ‹xs ≠ Nil› |
   (prefix2) xs where ‹ls@xs = ls'› and ‹xs ≠ Nil› 
using assms proof (induct ‹length ls› arbitrary: ‹ls› ‹ls'› rule: less_induct)
  case (less ls ls')
  obtain z zs z' zs' where
  lz: ‹ls = z#zs› ‹ls' = z'#zs'› by (metis list.exhaust less(6,7))
  show ‹?case› proof cases
    assume zz: ‹z = z'›
    hence zsz: ‹zs ≠ zs'› using less(5) lz by auto
    have lenz: ‹length zs < length ls› using lz by auto    
    show ‹?case› proof(cases ‹zs = Nil›)
      assume zs: ‹zs = Nil›
      hence ‹zs' ≠ Nil› using zsz by auto
      moreover
      have ‹ls@zs' = ls'› using zs lz zz by auto
      ultimately
      show ‹thesis› using less(4) by blast
    next
      assume zs: ‹zs ≠ Nil›
      show ‹thesis› proof (cases ‹zs' = Nil›)
        assume ‹zs' = Nil›
        hence ‹ls = ls'@zs› using lz zz by auto
        thus ‹thesis› using zs less(3) by blast
      next
        assume zs': ‹zs' ≠ Nil›
        { fix xs x ys x' ys' 
          assume ‹zs = xs @ [x] @ ys› ‹zs' = xs @ [x'] @ ys'› and xx: ‹x ≠ x'›
          hence ‹ls = (z#xs) @ [x] @ ys› ‹ls' = (z#xs) @ [x'] @ ys'› using lz zz by auto
          hence ‹thesis› using less(2) xx by blast
        } note * = this
        { fix xs 
          assume ‹zs = zs' @ xs› and xs: ‹xs ≠ []›
          hence ‹ls = ls' @ xs› using lz zz by auto
          hence ‹thesis› using xs less(3) by blast
        } note ** = this
        { fix xs 
          assume ‹zs@xs = zs'› and xs: ‹xs ≠ []›
          hence ‹ls@xs = ls'› using lz zz by auto
          hence ‹thesis› using xs less(4) by blast
        } note *** = this
        have ‹(⋀xs x ys x' ys'. zs = xs @ [x] @ ys ⟹ zs' = xs @ [x'] @ ys' ⟹ x ≠ x' ⟹ thesis) ⟹ 
              (⋀xs. zs = zs' @ xs ⟹ xs ≠ [] ⟹ thesis) ⟹ 
              (⋀xs. zs @ xs = zs' ⟹ xs ≠ [] ⟹ thesis) ⟹ thesis› 
        using less(1)[OF lenz _ _ _ zsz zs zs' ] .
        thus ‹thesis› using * ** *** by blast
      qed
    qed 
  next
    assume ‹z ≠ z'›
    moreover
    have ‹ls = []@[z]@zs› ‹ls' = []@[z']@zs'› using lz by auto
    ultimately show ‹thesis› using less(2) by blast
  qed
qed

lemma three_cases: assumes ‹A ∨ B ∨ C› obtains ‹A› | ‹B› | ‹C› using assms by auto

lemma insort_greater: ‹∀ x ∈ set ls. x < y ⟹ insort y ls = ls@[y]› by (induction ‹ls›,auto) 

lemma insort_append_first: assumes ‹∀ y ∈ set ys. x ≤ y› shows ‹insort x (xs@ys) = insort x xs @ ys› using assms by (induction ‹xs›,auto,metis insort_is_Cons)

lemma sorted_list_of_set_append: assumes ‹finite xs› ‹finite ys› ‹∀ x ∈ xs. ∀ y ∈ ys. x < y› shows ‹sorted_list_of_set (xs ∪ ys) = sorted_list_of_set xs @ (sorted_list_of_set ys)›
using assms(1,3) proof (induction ‹xs›)
  case empty thus ‹?case› by simp
next
  case (insert x xs)
  hence iv: ‹sorted_list_of_set (xs ∪ ys) = sorted_list_of_set xs @ sorted_list_of_set ys› by blast
  have le: ‹∀ y ∈ set (sorted_list_of_set ys). x < y› using insert(4) assms(2) sorted_list_of_set by auto
  have ‹sorted_list_of_set (insert x xs ∪ ys) = sorted_list_of_set (insert x (xs ∪ ys))› by auto
  also 
  have ‹… = insort x (sorted_list_of_set (xs ∪ ys))› by (metis Un_iff assms(2) finite_Un insert.hyps(1) insert.hyps(2) insert.prems insertI1 less_irrefl sorted_list_of_set_insert)
  also 
  have ‹… = insort x (sorted_list_of_set xs @ sorted_list_of_set ys)› using iv by simp
  also
  have ‹… = insort x (sorted_list_of_set xs) @ sorted_list_of_set ys›  by (metis le insort_append_first less_le_not_le)
  also 
  have ‹… = sorted_list_of_set (insert x xs) @ sorted_list_of_set ys› using sorted_list_of_set_insert[OF insert(1),of ‹x›] insert(2) by auto
  finally  
  show ‹?case› .
qed

lemma filter_insort: ‹sorted xs ⟹ filter P (insort x xs) = (if P x then insort x (filter P xs) else filter P xs)› by (induction ‹xs›, simp) (metis filter_insort filter_insort_triv map_ident) 

lemma filter_sorted_list_of_set: assumes ‹finite xs› shows ‹filter P (sorted_list_of_set xs) = sorted_list_of_set {x ∈ xs. P x}› using assms proof(induction ‹xs›)
  case empty thus ‹?case› by simp
next  
  case (insert x xs)
  have *: ‹set (sorted_list_of_set xs) = xs› ‹sorted (sorted_list_of_set xs)› ‹distinct (sorted_list_of_set xs)› by (auto simp add: insert.hyps(1))
  have **: ‹P x ⟹ {y ∈ insert x xs. P y} = insert x {y ∈ xs. P y}› by auto
  have ***: ‹¬ P x ⟹ {y ∈ insert x xs. P y} = {y ∈ xs. P y}› by auto
  note filter_insort[OF *(2),of ‹P› ‹x›] sorted_list_of_set_insert[OF insert(1), of ‹x›] insert(2,3) ** ***  
  thus ‹?case› by (metis (mono_tags) "*"(1) List.finite_set distinct_filter distinct_insort distinct_sorted_list_of_set set_filter sorted_list_of_set_insert)
qed

lemma unbounded_nat_set_infinite: assumes ‹∀ (i::nat). ∃ j≥i. j ∈ A› shows ‹¬ finite A› using assms
by (metis finite_nat_set_iff_bounded_le not_less_eq_eq)

lemma infinite_ascending: assumes nf: ‹¬ finite (A::nat set)› obtains f where ‹range f = A› ‹∀ i. f i < f (Suc i)› proof 
  let ‹?f› = ‹λ i. (LEAST a. a ∈ A ∧ card (A ∩ {..<a}) = i)›
  { fix i 
    obtain a where ‹a ∈ A› ‹card (A ∩ {..<a}) = i› 
    proof (induction ‹i› arbitrary: ‹thesis›)
      case 0
      let ‹?a0› = ‹(LEAST a. a ∈ A)›
      have ‹?a0 ∈ A› by (metis LeastI empty_iff finite.emptyI nf set_eq_iff)      
      moreover
      have ‹⋀b. b ∈ A ⟹ ?a0 ≤ b› by (metis Least_le)
      hence ‹card (A ∩ {..<?a}) = 0› by force
      ultimately
      show ‹?case› using 0 by blast
    next
      case (Suc i)
      obtain a where aa: ‹a ∈ A› and card: ‹card (A ∩ {..<a}) = i› using Suc.IH by metis
      have nf': ‹~ finite (A - {..a})› using nf by auto
      let ‹?b› = ‹LEAST b. b ∈ A - {..a}›
      have bin: ‹?b ∈ A-{..a}› by (metis LeastI empty_iff finite.emptyI nf' set_eq_iff)
      have le: ‹⋀c. c ∈ A-{..a} ⟹ ?b ≤ c› by (metis Least_le)
      have ab: ‹a < ?b› using bin by auto
      have ‹⋀ c. c ∈ A ⟹ c < ?b ⟹ c ≤ a› using le by force
      hence ‹A ∩ {..<?b} = insert a (A ∩ {..<a})› using bin ab aa by force 
      hence ‹card (A ∩{..<?b}) = Suc i› using card by auto
      thus ‹?case› using Suc.prems bin by auto
    qed
    note ‹⋀ thesis. ((⋀a. a ∈ A ⟹ card (A ∩ {..<a}) = i ⟹ thesis) ⟹ thesis)›
  }
  note ex = this
    
  {
    fix i
    obtain a where a: ‹a ∈ A ∧ card (A ∩{..<a}) = i›  using ex by blast
    have ina: ‹?f i ∈ A› and card: ‹card (A ∩{..<?f i}) = i› using LeastI[of ‹λ a. a ∈ A ∧ card (A ∩{..<a}) = i› ‹a›, OF a] by auto    
    obtain b where b: ‹b ∈ A ∧ card (A ∩{..<b}) = Suc i›  using ex by blast
    have inab: ‹?f (Suc i) ∈ A› and cardb: ‹card (A ∩{..<?f (Suc i)}) = Suc i› using LeastI[of ‹λ a. a ∈ A ∧ card (A ∩{..<a}) = Suc i› ‹b›, OF b] by auto
    have ‹?f i < ?f (Suc i)› proof (rule ccontr)
      assume ‹¬ ?f i < ?f (Suc i)›
      hence ‹A ∩{..<?f (Suc i)} ⊆ A ∩{..<?f i}› by auto
      moreover have ‹finite (A ∩{..<?f i})› by auto
      ultimately have ‹card(A ∩{..<?f (Suc i)}) ≤ card (A ∩{..<?f i})› by (metis (erased, lifting) card_mono)
      thus ‹False› using card cardb by auto 
    qed
    note this ina
  }
  note b = this
  thus ‹∀ i. ?f i < ?f (Suc i)› by auto
  have *: ‹range ?f ⊆ A› using b by auto
  moreover
  { 
    fix a assume ina: ‹a ∈ A›
    let ‹?i› = ‹card (A ∩ {..<a})›
    obtain b where b: ‹b ∈ A ∧ card (A ∩{..<b}) = ?i›  using ex by blast
    have inab: ‹?f ?i ∈ A› and cardb: ‹card (A ∩{..<?f ?i}) = ?i› using LeastI[of ‹λ a. a ∈ A ∧ card (A ∩{..<a}) = ?i› ‹b›, OF b] by auto
    have le: ‹?f ?i ≤ a› using Least_le[of ‹λ a. a ∈ A ∧ card (A ∩{..<a}) = ?i› ‹a›] ina by auto    
    have ‹a = ?f ?i› proof (rule ccontr)
      have fin: ‹finite (A ∩ {..<a})› by auto
      assume ‹a ≠ ?f ?i›
      hence ‹?f ?i < a› using le by simp
      hence ‹?f ?i ∈ A ∩ {..<a}› using inab by auto
      moreover
      have ‹A ∩ {..<?f ?i} ⊆ A ∩ {..<a}› using le by auto
      hence ‹A ∩ {..<?f ?i} = A ∩ {..<a}› using cardb card_subset_eq[OF fin] by auto
      ultimately      
      show ‹False› by auto
    qed
    hence ‹a ∈ range ?f› by auto
  }
  hence ‹A ⊆ range ?f› by auto 
  ultimately show ‹range ?f = A› by auto
qed

lemma mono_ge_id: ‹∀ i. f i < f (Suc i) ⟹ i ≤ f i› 
  apply (induction ‹i›,auto) 
  by (metis not_le not_less_eq_eq order_trans)

lemma insort_map_mono: assumes mono: ‹∀ n m. n < m ⟶ f n < f m› shows ‹map f (insort n ns) = insort (f n) (map f ns)›
  apply (induction ‹ns›)
   apply auto
     apply (metis not_less not_less_iff_gr_or_eq mono)
    apply (metis antisym_conv1 less_imp_le mono)
   apply (metis mono not_less)
  by (metis mono not_less)  

lemma sorted_list_of_set_map_mono: assumes mono: ‹∀ n m. n < m ⟶ f n < f m› and fin: ‹finite A›
shows ‹map f (sorted_list_of_set A) = sorted_list_of_set (f`A)›
using fin proof (induction)
  case empty thus ‹?case› by simp
next
  case (insert x A)
  have [simp]:‹sorted_list_of_set (insert x A) = insort x (sorted_list_of_set A)› using insert sorted_list_of_set_insert by simp
  have ‹f ` insert x A = insert (f x) (f ` A)› by auto
  moreover
  have ‹f x ∉ f`A› apply (rule ccontr) using insert(2) mono apply auto by (metis insert.hyps(2) mono neq_iff)
  ultimately
  have ‹sorted_list_of_set (f ` insert x A) = insort (f x) (sorted_list_of_set (f`A))› using insert(1) sorted_list_of_set_insert by simp
  also
  have ‹… = insort (f x) (map f (sorted_list_of_set A))› using insert.IH by auto
  also have ‹… = map f (insort x (sorted_list_of_set A))› using insort_map_mono[OF mono] by auto
  finally  
  show ‹map f (sorted_list_of_set (insert x A)) = sorted_list_of_set (f ` insert x A)› by simp
qed

lemma GreatestIB:
fixes n :: ‹nat› and P
assumes a:‹∃k≤n. P k›
shows GreatestBI: ‹P (GREATEST k. k≤n ∧ P k)› and GreatestB: ‹(GREATEST k. k≤n ∧ P k) ≤ n› 
proof -
  show ‹P (GREATEST k. k≤n ∧ P k)› using GreatestI_ex_nat[OF assms] by auto  
  show ‹(GREATEST k. k≤n ∧ P k) ≤ n› using GreatestI_ex_nat[OF assms] by auto
qed

lemma GreatestB_le:
fixes n :: ‹nat›
assumes ‹x≤n› and ‹P x›
shows ‹x ≤ (GREATEST k. k≤n ∧ P k)› 
proof -
  have *: ‹∀ y. y≤n ∧ P y ⟶ y<Suc n› by auto
  then show ‹x ≤ (GREATEST k. k≤n ∧ P k)› using assms by (blast intro: Greatest_le_nat)
qed

lemma LeastBI_ex: assumes ‹∃k ≤ n. P k› shows ‹P (LEAST k::'c::wellorder. P k)› and ‹(LEAST k. P k) ≤ n› 
proof -
  from assms obtain k where k: "k ≤ n" "P k" by blast
  thus ‹P (LEAST k. P k)› using LeastI[of ‹P› ‹k›] by simp
  show ‹(LEAST k. P k) ≤ n› using Least_le[of ‹P› ‹k›] k by auto
qed

lemma allB_atLeastLessThan_lower:  assumes ‹(i::nat) ≤ j› ‹∀ x∈{i..<n}. P x› shows ‹∀ x∈{j..<n}. P x› proof 
  fix x assume ‹x∈{j..<n}› hence ‹x∈{i..<n}› using assms(1) by simp
  thus ‹P x› using assms(2) by auto
qed


subsection ‹Facts about Paths›

context IFC
begin

lemma path0: ‹path σ 0 = entry› unfolding path_def by auto

lemma path_in_nodes[intro]: ‹path σ k ∈ nodes› proof (induction ‹k›)
  case (Suc k)
  hence ‹⋀ σ'. (path σ k, suc (path σ k) σ') ∈ edges› by auto
  hence ‹(path σ k, path σ (Suc k)) ∈ edges› unfolding path_def 
    by (metis suc_def comp_apply funpow.simps(2) prod.collapse) 
  thus ‹?case› using edges_nodes by force
qed (auto simp add: path_def)

lemma path_is_path[simp]: ‹is_path (path σ)› unfolding is_path_def path_def using step_suc_sem apply auto
by (metis path_def suc_def edges_complete path_in_nodes prod.collapse)

lemma term_path_stable: assumes ‹is_path π› ‹π i = return› and le: ‹i ≤ j› shows ‹π j = return› 
using le proof (induction ‹j›)
  case (Suc j) 
  show ‹?case› proof cases
    assume ‹i≤j›
    hence ‹π j = return› using Suc by simp
    hence ‹(return, π (Suc j)) ∈ edges› using assms(1) unfolding is_path_def by metis
    thus ‹π (Suc j) = return› using edges_return by auto
  next
    assume ‹¬ i ≤ j›
    hence ‹Suc j = i› using Suc by auto
    thus ‹?thesis› using assms(2) by auto
  qed
next
  case 0 thus ‹?case› using assms by simp
qed 

lemma path_path_shift: assumes ‹is_path π› shows ‹is_path (π«m)› 
using assms unfolding is_path_def by simp

lemma path_cons: assumes ‹is_path π› ‹is_path π'› ‹π m = π' 0› shows ‹is_path (π @⇗m⇖ π')› 
unfolding is_path_def proof(rule,cases)
  fix n assume ‹m < n› thus ‹((π @⇗m⇖ π') n, (π @⇗m⇖  π') (Suc n)) ∈ edges› 
    using assms(2) unfolding is_path_def path_append_def
    by (auto,metis Suc_diff_Suc diff_Suc_Suc less_SucI) 
next
  fix n assume *: ‹¬ m < n›  thus ‹((π @⇗m⇖  π') n, (π @⇗m⇖  π') (Suc n)) ∈ edges› proof cases
    assume [simp]: ‹n = m›
    thus ‹?thesis› using assms unfolding is_path_def path_append_def by force
  next
    assume ‹n ≠ m›
    hence ‹Suc n ≤ m› ‹n≤ m› using * by auto
    with assms(1) show ‹?thesis› unfolding is_path_def by auto
  qed
qed

lemma is_path_loop: assumes ‹is_path π› ‹0 < i› ‹π i = π 0› shows ‹is_path (λ n. π (n mod i))› unfolding is_path_def proof (rule,cases)
  fix n
  assume ‹0 < Suc n mod i›
  hence ‹Suc n mod i = Suc (n mod i)› by (metis mod_Suc neq0_conv)
  moreover 
  have ‹(π (n mod i), π (Suc (n mod i))) ∈ edges› using assms(1) unfolding is_path_def by auto
  ultimately
  show ‹(π (n mod i), π (Suc n mod i)) ∈ edges› by simp
  next
  fix n
  assume ‹¬ 0 < Suc n mod i›
  hence ‹Suc n mod i = 0› by auto
  moreover 
  hence ‹n mod i = i - 1› using assms(2) by (metis Zero_neq_Suc diff_Suc_1 mod_Suc)
  ultimately
  show ‹(π(n mod i), π (Suc n mod i)) ∈ edges› using assms(1) unfolding is_path_def by (metis assms(3) mod_Suc)
qed

lemma path_nodes: ‹is_path π ⟹ π k ∈ nodes› unfolding is_path_def using edges_nodes by force 

lemma direct_path_return': assumes ‹is_path π › ‹π 0 = x› ‹x ≠ return› ‹π n = return›
obtains π' n' where ‹is_path π'› ‹π' 0 = x› ‹π' n' = return› ‹∀ i> 0. π' i ≠ x›
using assms proof (induction ‹n› arbitrary: ‹π›  rule: less_induct)
  case (less n π) 
  hence ih: ‹⋀ n' π'. n' < n ⟹ is_path π' ⟹ π' 0 = x ⟹ π' n' = return ⟹ thesis› using assms by auto
  show ‹thesis› proof cases
    assume ‹∀ i>0. π i ≠ x› thus ‹thesis› using less by auto
  next
    assume ‹¬ (∀ i>0. π i ≠ x)›
    then obtain i where ‹0<i› ‹π i = x› by auto
    hence ‹(π«i) 0 = x› by auto
    moreover
    have ‹i < n› using less(3,5,6) ‹π i = x› by (metis linorder_neqE_nat term_path_stable less_imp_le)    
    hence ‹(π«i) (n-i) = return› using less(6) by auto
    moreover
    have ‹is_path (π«i)› using less(3) by (metis path_path_shift)
    moreover
    have ‹n - i < n› using ‹0<i› ‹i < n› by auto    
    ultimately show ‹thesis› using ih by auto
  qed
qed

lemma direct_path_return: assumes  ‹x ∈ nodes› ‹x ≠ return›
obtains π n where ‹is_path π› ‹π 0 = x› ‹π n = return› ‹∀ i> 0. π i ≠ x›
using direct_path_return'[of _ ‹x›] reaching_ret[OF assms(1)] assms(2) by blast

lemma path_append_eq_up_to: ‹(π @⇗k⇖ π') =⇘k⇙ π›  unfolding eq_up_to_def by auto

lemma eq_up_to_le: assumes ‹k ≤ n› ‹π =⇘n⇙  π'› shows ‹π =⇘k⇙ π'› using assms unfolding eq_up_to_def by auto 

lemma eq_up_to_refl: shows ‹π =⇘k⇙ π› unfolding eq_up_to_def by auto 

lemma eq_up_to_sym: assumes ‹π =⇘k⇙ π'› shows ‹π' =⇘k⇙ π› using assms unfolding eq_up_to_def by auto

lemma eq_up_to_apply: assumes ‹π =⇘k⇙ π'› ‹j ≤ k› shows ‹π j = π' j› using assms unfolding eq_up_to_def by auto

lemma path_swap_ret: assumes ‹is_path π› obtains π' n where ‹is_path π'› ‹π =⇘k⇙ π'› ‹π' n = return›
proof -
  have nd: ‹π k ∈ nodes› using assms path_nodes by simp
  obtain π' n where *: ‹is_path π'› ‹π' 0 = π k› ‹π' n = return› using reaching_ret[OF nd] by blast
  have ‹π =⇘k⇙ (π@⇗k⇖ π')› by (metis eq_up_to_sym path_append_eq_up_to)
  moreover
  have ‹is_path (π@⇗k⇖ π')› using assms * path_cons by metis
  moreover
  have ‹(π@⇗k⇖ π') (k + n) = return› using * by auto
  ultimately
  show ‹thesis› using that by blast
qed

lemma path_suc: ‹path σ (Suc k) = fst (step (path σ k, σ⇗k⇖))› by (induction ‹k›, auto simp: path_def kth_state_def)

lemma kth_state_suc: ‹σ⇗Suc k⇖  = snd (step (path σ k, σ⇗k⇖))› by (induction ‹k›, auto simp: path_def kth_state_def)


subsection ‹Facts about Post Dominators›

lemma pd_trans: assumes 1: ‹y pd→ x› and 2: ‹z pd→y› shows ‹z pd→x› 
proof -
  {
    fix π n
    assume 3[simp]: ‹is_path π› ‹π 0 = x› ‹π n = return›
    then obtain k where ‹π k = y› and 7: ‹k ≤ n› using 1 unfolding is_pd_def by blast
    then have ‹(π«k) 0 = y› and ‹(π«k) (n-k) = return› by auto
    moreover have ‹is_path (π«k)› by(metis 3(1) path_path_shift)
    ultimately obtain k' where 8: ‹(π«k) k' = z› and ‹k' ≤ n-k› using 2 unfolding is_pd_def by blast
    hence ‹k+k'≤n› and ‹π (k+ k') = z› using 7 by auto
    hence ‹∃k≤n. π k = z› using path_nodes by auto    
  }
  thus ‹?thesis› using 1 unfolding is_pd_def by blast
qed

lemma pd_path: assumes ‹y pd→ x›
obtains π n k where ‹is_path π› and ‹π 0 = x› and ‹π n = return› and ‹π k = y› and ‹k ≤ n›   
using assms unfolding is_pd_def using reaching_ret[of ‹x›] by blast

lemma pd_antisym: assumes xpdy: ‹x pd→ y› and ypdx: ‹y pd→ x› shows ‹x = y›
proof -
  obtain π n where path: ‹is_path π› and π0: ‹π 0 = x› and πn: ‹π n = return› using pd_path[OF ypdx] by metis
  hence kex: ‹∃k≤n. π k = y› using ypdx unfolding is_pd_def by auto
  obtain k where k: ‹k = (GREATEST k. k≤n ∧ π k = y)› by simp
  have πk: ‹π k = y› and kn: ‹k ≤ n› using k kex by (auto intro: GreatestIB)
  
  have kpath: ‹is_path (π«k)› by (metis path_path_shift path)
  moreover have k0: ‹(π«k) 0 = y› using πk by simp
  moreover have kreturn: ‹(π«k) (n-k) = return› using kn πn by simp
  ultimately have ky': ‹∃k'≤(n-k).(π«k) k' = x› using xpdy unfolding is_pd_def by simp      

  obtain k' where k': ‹k' = (GREATEST k'. k'≤(n-k) ∧ (π«k) k' = x)› by simp

  with ky' have πk': ‹(π«k) k' = x› and kn': ‹k' ≤ (n-k)›  by (auto intro: GreatestIB)
  have k'path: ‹is_path (π«k«k')› using kpath by(metis path_path_shift)
  moreover have k'0: ‹(π«k«k') 0 = x› using πk' by simp
  moreover have k'return: ‹(π«k«k') (n-k-k') = return› using kn' kreturn by (metis path_shift_def le_add_diff_inverse)
  ultimately have ky'': ‹∃k''≤(n-k-k').(π«k«k') k'' = y› using ypdx unfolding is_pd_def by blast

  obtain k'' where k'': ‹k''= (GREATEST k''. k''≤(n-k-k') ∧ (π«k«k') k'' = y)› by simp
  with ky'' have πk'': ‹(π«k«k') k'' = y› and kn'': ‹k'' ≤ (n-k-k')›  by (auto intro: GreatestIB)

  from this(1) have  ‹π (k + k' + k'') = y› by (metis path_shift_def add.commute add.left_commute)
  moreover
  have ‹k + k' +k'' ≤ n› using kn'' kn' kn by simp
  ultimately have ‹k + k' + k''≤ k› using k by(auto simp: GreatestB_le)
  hence ‹k' = 0› by simp
  with k0 πk' show ‹x = y› by simp
qed

lemma pd_refl[simp]: ‹x ∈ nodes ⟹ x pd→ x› unfolding is_pd_def by blast

lemma pdt_trans_in_pdt: ‹(x,y) ∈ pdt⇧+ ⟹ (x,y) ∈ pdt› 
proof (induction rule: trancl_induct)
  case base thus ‹?case› by simp
next
  case (step y z) show ‹?case› unfolding pdt_def proof (simp)
    have *: ‹y pd→ x› ‹z pd→ y› using step unfolding pdt_def by auto
    hence [simp]: ‹z pd→ x› using pd_trans[where x=‹x› and y=‹y› and z=‹z›] by simp
    have ‹x≠z› proof 
      assume ‹x = z›
      hence ‹z pd→ y› ‹y pd→ z› using * by auto
      hence ‹z = y› using pd_antisym by auto
      thus ‹False› using step(2) unfolding pdt_def by simp
    qed
    thus ‹x ≠ z ∧ z pd→ x› by auto
  qed
qed

lemma pdt_trancl_pdt: ‹pdt⇧+ = pdt› using pdt_trans_in_pdt by fast

lemma trans_pdt: ‹trans pdt› by (metis pdt_trancl_pdt trans_trancl)

definition [simp]: ‹pdt_inv = pdt¯›

lemma wf_pdt_inv: ‹wf (pdt_inv)› proof (rule ccontr)
  assume ‹¬ wf (pdt_inv)›
  then obtain f where  ‹∀i. (f (Suc i), f i) ∈ pdt¯› using wf_iff_no_infinite_down_chain by force
  hence *: ‹∀ i. (f i, f (Suc i)) ∈ pdt› by simp
  have **:‹∀ i. ∀ j>i. (f i, f j) ∈ pdt› proof(rule,rule,rule)
    fix i j assume  ‹i < (j::nat)› thus ‹(f i, f j) ∈ pdt› proof (induction ‹j› rule: less_induct)
      case (less k)
      show ‹?case› proof (cases ‹Suc i < k›)
        case True
        hence k:‹k-1 < k› ‹i < k-1› and sk: ‹Suc (k-1) = k› by auto
        show ‹?thesis› using less(1)[OF k] *[rule_format,of ‹k-1›,unfolded sk] trans_pdt[unfolded trans_def] by blast
      next
        case False
        hence ‹Suc i = k› using less(2) by auto
        then show ‹?thesis› using * by auto
      qed
    qed
  qed
  hence ***:‹∀ i. ∀ j > i. f j pd→ f i› ‹∀ i. ∀ j > i. f i ≠  f j› unfolding pdt_def by auto
  hence ****:‹∀ i>0. f i pd→ f 0› by simp
  hence ‹f 0 ∈ nodes›  using * is_pd_def by fastforce
  then obtain π n where π:‹is_path π› ‹π 0 = f 0› ‹π n = return› using reaching_ret by blast  
  hence ‹∀ i>0. ∃ k≤n. π k = f i› using ***(1) ‹f 0 ∈ nodes› unfolding is_pd_def by blast
  hence πf:‹∀ i. ∃ k≤n. π k = f i› using π(2) by (metis le0 not_gr_zero)
  have ‹range f ⊆ π ` {..n}› proof(rule subsetI)
    fix x assume ‹x ∈ range f›
    then obtain i where ‹x = f i› by auto
    then obtain k where ‹x = π k› ‹k ≤ n› using πf by metis
    thus ‹x ∈ π ` {..n}› by simp
  qed
  hence f:‹finite (range f)› using finite_surj by auto
  hence fi:‹∃ i. infinite {j. f j = f i}›  using pigeonhole_infinite[OF _ f] by auto
  obtain i where ‹infinite {j. f j = f i}› using fi ..    
  thus ‹False› 
    by (metis (mono_tags, lifting) "***"(2) bounded_nat_set_is_finite gt_ex mem_Collect_eq nat_neq_iff)
qed

lemma return_pd: assumes ‹x ∈ nodes› shows ‹return pd→ x› unfolding is_pd_def using assms by blast

lemma pd_total: assumes xz: ‹x pd→ z› and yz: ‹y pd→ z› shows ‹x pd→ y ∨ y pd→x› 
proof -
  obtain π n where path: ‹is_path π› and π0: ‹π 0 = z› and πn: ‹π n = return› using xz reaching_ret unfolding is_pd_def by force
  have *: ‹∃ k≤n. (π k = x ∨ π k = y)› (is ‹∃ k≤n. ?P k›) using path π0 πn xz yz unfolding is_pd_def by auto
  obtain k where k: ‹k = (LEAST k. π k = x ∨ π k = y)› by simp
  hence kn: ‹k≤n› and πk: ‹π k = x ∨ π k = y› using LeastBI_ex[OF *] by auto 
  note k_le = Least_le[where P = ‹?P›] 
  show ‹?thesis› proof (cases)
    assume kx: ‹π k = x›
    have k_min: ‹⋀ k'. π k' = y ⟹ k ≤ k'› using k_le unfolding k by auto
    {
      fix π' 
      and n' :: ‹nat›
      assume path': ‹is_path π'› and π'0: ‹π' 0 = x› and π'n': ‹π' n' = return›
      have path'': ‹is_path (π @⇗k⇖ π')› using path_cons[OF path path'] kx π'0 by auto
      have π''0: ‹(π @⇗k⇖ π') 0 = z› using π0 by simp
      have π''n: ‹(π @⇗k⇖ π') (k+n') = return› using π'n' kx π'0 by auto
      obtain k' where k': ‹k' ≤ k + n'› ‹(π @⇗k⇖ π') k' = y› using yz path'' π''0 π''n unfolding is_pd_def by blast
      have **: ‹k ≤ k'› proof (rule ccontr)
        assume ‹¬ k ≤ k'›
        hence ‹k' < k› by simp
        moreover 
        hence ‹π k' = y› using k' by auto
        ultimately
        show ‹False› using k_min by force
     qed
     hence ‹π' (k' - k) = y› using k' π'0 kx  by auto
     moreover
     have ‹(k' - k) ≤ n'› using k' by auto
     ultimately 
     have ‹∃ k≤ n'. π' k = y› by auto
   }
   hence ‹y pd→ x› using kx path_nodes path unfolding is_pd_def by auto
   thus ‹?thesis› ..
 next ― ‹This is analogous argument›
   assume kx: ‹π k ≠ x›
   hence ky: ‹π k = y› using πk by auto
   have k_min: ‹⋀ k'. π k' = x ⟹ k ≤ k'› using k_le unfolding k by auto
    {
      fix π' 
      and n' :: ‹nat›
      assume path': ‹is_path π'› and π'0: ‹π' 0 = y› and π'n': ‹π' n' = return›
      have path'': ‹is_path (π @⇗k⇖ π')› using path_cons[OF path path'] ky π'0 by auto
      have π''0: ‹(π @⇗k⇖ π') 0 = z› using π0 by simp
      have π''n: ‹(π @⇗k⇖ π') (k+n') = return› using π'n' ky π'0 by auto
      obtain k' where k': ‹k' ≤ k + n'› ‹(π @⇗k⇖ π') k' = x› using xz path'' π''0 π''n unfolding is_pd_def by blast
      have **: ‹k ≤ k'› proof (rule ccontr)
        assume ‹¬ k ≤ k'›
        hence ‹k' < k› by simp
        moreover 
        hence ‹π k' = x› using k' by auto
        ultimately
        show ‹False› using k_min by force
     qed
     hence ‹π' (k' - k) = x› using k' π'0 ky  by auto
     moreover
     have ‹(k' - k) ≤ n'› using k' by auto
     ultimately 
     have ‹∃ k≤ n'. π' k = x› by auto
   }
   hence ‹x pd→ y› using ky path_nodes path unfolding is_pd_def by auto
   thus ‹?thesis› ..
  qed
qed    

lemma pds_finite: ‹finite {y . (x,y) ∈ pdt}› proof cases 
  assume ‹x ∈ nodes›
  then obtain π n where π:‹is_path π› ‹π 0 = x› ‹π n = return› using reaching_ret by blast
  have *: ‹∀ y ∈ {y. (x,y)∈ pdt}. y pd→ x› using pdt_def by auto
  have ‹∀ y ∈ {y. (x,y)∈ pdt}. ∃ k ≤ n. π k = y›  using * π is_pd_def by blast
  hence ‹{y. (x,y)∈ pdt} ⊆ π ` {..n}›  by auto
  then show ‹?thesis› using finite_surj by blast
next
  assume ‹¬ x∈ nodes›
  hence ‹{y. (x,y)∈pdt} = {}› unfolding pdt_def is_pd_def using path_nodes reaching_ret by fastforce
  then show ‹?thesis› by simp
qed

lemma ipd_exists: assumes node: ‹x ∈ nodes› and not_ret: ‹x≠return› shows ‹∃y. y ipd→ x› 
proof -
  let ‹?Q› = ‹{y. x≠y ∧ y pd→ x}›
  have *: ‹return ∈ ?Q› using assms return_pd by simp    
  hence **: ‹∃ x. x∈ ?Q› by auto
  have fin: ‹finite ?Q› using pds_finite unfolding pdt_def by auto
  have tot: ‹∀ y z. y∈?Q ∧ z ∈ ?Q ⟶ z pd→ y ∨ y pd→ z› using pd_total by auto
  obtain y where ymax: ‹y∈ ?Q› ‹∀ z∈?Q. z = y ∨ z pd→ y› using fin ** tot proof (induct)
    case empty
    then show ‹?case› by auto
  next
    case (insert x F) show ‹thesis› proof (cases ‹F = {}›)
      assume ‹F = {}›
      thus ‹thesis› using insert(4)[of ‹x›] by auto
    next  
      assume ‹F ≠ {}›
      hence ‹∃ x. x∈ F› by auto
      have ‹⋀y. y ∈ F ⟹ ∀z∈F. z = y ∨ z pd→ y ⟹ thesis› proof -
        fix y assume a: ‹y ∈ F› ‹∀z∈F. z = y ∨ z pd→ y›
        have ‹x ≠ y› using insert a by auto
        have ‹x pd→ y ∨ y pd→ x› using insert(6) a(1) by auto
        thus ‹thesis› proof 
          assume ‹x pd→ y›
          hence ‹∀z∈insert x F. z = y ∨ z pd→ y› using a(2) by blast
          thus ‹thesis› using a(1) insert(4) by blast
        next
          assume ‹y pd→ x›
          have ‹∀z∈insert x F. z = x ∨ z pd→ x› proof
            fix z assume ‹z∈ insert x F› thus ‹z = x ∨ z pd→ x› proof(rule,simp)
              assume ‹z∈F›
              hence ‹z = y ∨ z pd→ y› using a(2) by auto
              thus ‹z = x ∨ z pd→ x› proof(rule,simp add: ‹y pd→ x›)
                assume ‹z pd→ y›
                show ‹z = x ∨ z pd→ x› using ‹y pd→ x› ‹z pd→ y› pd_trans by blast
              qed 
            qed
          qed 
          then show ‹thesis› using insert by blast
        qed
      qed
      then show ‹thesis› using insert by blast
    qed
  qed    
  hence ***: ‹y pd→ x› ‹x≠y› by auto
  have ‹∀ z. z ≠ x ∧ z pd→ x ⟶ z pd→ y› proof (rule,rule)
    fix z 
    assume a: ‹ z ≠ x ∧ z pd→ x›
    hence b: ‹z ∈ ?Q› by auto
    have ‹y pd→ z ∨ z pd→ y› using pd_total ***(1) a by auto
    thus ‹z pd→ y› proof
      assume c: ‹y pd→ z›
      hence ‹y = z› using b ymax pdt_def pd_antisym by auto
      thus ‹z pd→ y› using c by simp
    qed simp
  qed
  with *** have  ‹y ipd→ x› unfolding is_ipd_def by simp
  thus ‹?thesis› by blast
qed

lemma ipd_unique: assumes yipd: ‹y ipd→ x› and y'ipd: ‹y' ipd→ x› shows ‹y = y'› 
proof -  
  have 1: ‹y pd→ y'› and  2: ‹y' pd→ y› using yipd y'ipd unfolding is_ipd_def by auto
  show ‹?thesis› using pd_antisym[OF 1 2] .
qed

lemma ipd_is_ipd: assumes ‹x ∈ nodes› and ‹x≠return› shows ‹ipd x ipd→ x› proof -
  from assms obtain y where ‹y ipd→ x› using ipd_exists by auto
  moreover
  hence ‹⋀ z. z ipd→x ⟹ z = y› using ipd_unique by simp
  ultimately show ‹?thesis› unfolding ipd_def by (auto intro: theI2)
qed

lemma is_ipd_in_pdt: ‹y ipd→ x ⟹ (x,y) ∈ pdt› unfolding is_ipd_def pdt_def by auto

lemma ipd_in_pdt: ‹x ∈ nodes ⟹ x≠return ⟹ (x,ipd x) ∈ pdt› by (metis ipd_is_ipd is_ipd_in_pdt)

lemma no_pd_path: assumes ‹x ∈ nodes› and ‹¬ y pd→ x›
obtains π n where ‹is_path π› and ‹π 0 = x› and ‹π n = return› and ‹∀ k ≤ n. π k ≠ y›
proof (rule ccontr)
  assume ‹¬ thesis›
  hence ‹∀ π n.  is_path π ∧ π 0 = x ∧ π n = return ⟶ (∃ k≤n . π k = y)› using that by force
  thus ‹False› using assms unfolding is_pd_def by auto
qed

lemma pd_pd_ipd: assumes ‹x ∈ nodes› ‹x≠return› ‹y≠x› ‹y pd→ x› shows ‹y pd→ ipd x› 
proof -
  have ‹ipd x pd→ x› by (metis assms(1,2) ipd_is_ipd is_ipd_def)
  hence ‹y pd→ ipd x ∨ ipd x pd→ y› by (metis assms(4) pd_total)
  thus ‹?thesis› proof
    have 1: ‹ipd x ipd→ x› by (metis assms(1,2) ipd_is_ipd)
    moreover
    assume ‹ipd x pd→ y›
    ultimately
    show ‹y pd→ ipd x› unfolding is_ipd_def using assms(3,4) by auto
  qed auto
qed

lemma pd_nodes: assumes ‹y pd→ x› shows pd_node1: ‹y ∈ nodes› and pd_node2: ‹x ∈ nodes›
proof -
  obtain π k where ‹is_path π› ‹π k = y› using assms unfolding is_pd_def using reaching_ret by force
  thus ‹y ∈ nodes› using path_nodes by auto
  show ‹x ∈ nodes› using assms unfolding is_pd_def by simp
qed

lemma pd_ret_is_ret: ‹x pd→ return ⟹ x = return› by (metis pd_antisym pd_node1 return_pd)

lemma ret_path_none_pd: assumes ‹x ∈ nodes› ‹x≠return› 
obtains π n where ‹is_path π›  ‹π 0 = x› ‹π n = return›  ‹∀ i>0. ¬ x pd→ π i›
proof(rule ccontr)
  assume ‹¬thesis›
  hence *: ‹⋀ π n. ⟦is_path π; π 0 = x; π n = return⟧ ⟹ ∃i>0. x pd→ π i› using that by blast
  obtain π n where **: ‹is_path π›  ‹π 0 = x› ‹π n = return› ‹∀ i>0. π i ≠ x› using direct_path_return[OF assms] by metis
  then obtain i where ***: ‹i>0› ‹x pd→ π i› using * by blast
  hence ‹π i ≠ return› using pd_ret_is_ret assms(2) by auto
  hence ‹i < n› using assms(2) term_path_stable ** by (metis linorder_neqE_nat less_imp_le)
  hence ‹(π«i)(n-i) = return› using **(3) by auto
  moreover
  have ‹(π«i) (0) = π i› by simp
  moreover 
  have ‹is_path (π«i)› using **(1) path_path_shift by metis
  ultimately
  obtain k where ‹(π«i) k = x› using ***(2) unfolding is_pd_def by metis
  hence ‹π (i + k) = x› by auto
  thus ‹False› using **(4) ‹i>0› by auto
qed

lemma path_pd_ipd0': assumes ‹is_path π› and ‹π n ≠ return› ‹π n ≠ π 0› and ‹π n pd→ π 0› 
obtains k where ‹k ≤ n› and ‹π k = ipd(π 0)› 
proof(rule ccontr)  
  have *: ‹π n pd→ ipd (π 0)› by (metis is_pd_def assms(3,4) pd_pd_ipd pd_ret_is_ret)  
  obtain π' n' where **: ‹is_path π'› ‹π' 0 = π n› ‹π' n' = return› ‹∀ i>0. ¬ π n pd→ π' i›  by (metis assms(2) assms(4) pd_node1 ret_path_none_pd)
  hence ‹∀ i>0. π' i ≠ ipd (π 0)› using * by metis
  moreover
  assume ‹¬ thesis›
  hence ‹∀ k≤n. π k ≠ ipd (π 0)› using that by blast
  ultimately
  have ‹∀ i. (π@⇗n⇖  π') i ≠ ipd (π 0)› by (metis diff_is_0_eq neq0_conv path_append_def)
  moreover
  have ‹(π@⇗n⇖  π') (n + n') = return› 
    by (metis ‹π' 0 = π n› ‹π' n' = return› add_diff_cancel_left' assms(2) diff_is_0_eq path_append_def)
  moreover
  have ‹(π@⇗n⇖  π') 0 = π 0› by (metis le0 path_append_def)
  moreover
  have ‹is_path (π@⇗n⇖  π')› by (metis ‹π' 0 = π n› ‹is_path π'› assms(1) path_cons)
  moreover  
  have ‹ipd (π 0) pd→ π 0› by (metis **(2,3,4) assms(2) assms(4) ipd_is_ipd is_ipd_def neq0_conv pd_node2)
  moreover
  have ‹π 0 ∈ nodes› by (metis assms(1) path_nodes)
  ultimately
  show ‹False› unfolding is_pd_def by blast
qed

lemma path_pd_ipd0: assumes ‹is_path π› and ‹π 0 ≠ return› ‹π n ≠ π 0› and ‹π n pd→ π 0› 
obtains k where ‹k ≤ n› and ‹π k = ipd(π 0)› 
proof cases 
  assume *: ‹π n = return›
  have ‹ipd (π 0) pd→ (π 0)› by (metis is_ipd_def is_pd_def assms(2,4) ipd_is_ipd)
  with assms(1,2,3) * show ‹thesis› unfolding is_pd_def by (metis that)
next
  assume ‹π n ≠ return› 
  from path_pd_ipd0' [OF assms(1) this assms(3,4)] that show ‹thesis› by auto
qed

lemma path_pd_ipd: assumes ‹is_path π› and ‹π k ≠ return› ‹π n ≠ π k› and ‹π n pd→ π k› and kn: ‹k < n› 
obtains l where ‹k < l› and ‹l ≤ n› and ‹π l = ipd(π k)› 
proof -
  have ‹is_path (π « k)› ‹(π « k) 0 ≠ return› ‹(π « k) (n - k) ≠ (π « k) 0› ‹(π « k) (n - k) pd→ (π « k) 0› 
  using assms path_path_shift by auto 
  with path_pd_ipd0[of ‹π«k› ‹n-k›]
  obtain ka where ‹ka ≤ n - k› ‹(π « k) ka = ipd ((π « k) 0)› .
  hence ‹k + ka ≤ n› ‹π (k + ka) = ipd (π k)› using kn by auto
  moreover 
  hence ‹π (k + ka) ipd→ π k› by (metis assms(1) assms(2) ipd_is_ipd path_nodes)
  hence ‹k < k + ka› unfolding is_ipd_def by (metis nat_neq_iff not_add_less1)
  ultimately
  show ‹thesis› using that[of ‹k+ka›] by auto
qed

lemma path_ret_ipd: assumes ‹is_path π› and ‹π k ≠ return› ‹π n = return› 
obtains l where ‹k < l› and ‹l ≤ n› and ‹π l = ipd(π k)› 
proof -
  have ‹π n ≠ π k› using assms by auto
  moreover
  have ‹k ≤ n› apply (rule ccontr) using term_path_stable assms by auto
  hence ‹k < n› by (metis assms(2,3) dual_order.order_iff_strict)
  moreover
  have ‹π n pd→ π k› by (metis assms(1,3) path_nodes return_pd)
  ultimately
  obtain l where ‹k < l› ‹l ≤ n› ‹π l = ipd (π k)› using assms path_pd_ipd by blast
  thus ‹thesis› using that by auto
qed

lemma pd_intro: assumes ‹l pd→ k› ‹is_path π› ‹π 0 = k› ‹π n = return› 
obtains i where ‹i ≤ n› ‹π i = l› using assms unfolding is_pd_def by metis

lemma path_pd_pd0: assumes path:  ‹is_path π› and lpdn: ‹π l pd→ n› and npd0: ‹n pd→ π 0› 
obtains k where ‹k ≤ l› ‹π k = n›
proof (rule ccontr)
  assume ‹¬ thesis›
  hence notn: ‹⋀ k. k ≤ l ⟹ π k ≠ n› using that by blast
  have nret: ‹π l ≠ return› by (metis is_pd_def assms(1,3) notn)
  
  obtain π' n' where path': ‹is_path π'› and π0': ‹π' 0 = π l› and πn': ‹π' n' = return› and nonepd: ‹∀ i>0. ¬ π l pd→ π' i›
  using nret path path_nodes ret_path_none_pd by metis
  
  have ‹π l ≠ n› using notn by simp
  hence ‹∀ i. π' i ≠ n› using nonepd π0' lpdn by (metis neq0_conv)
  
  hence notn': ‹∀ i. (π@⇗l⇖ π') i ≠ n› using notn π0' by auto

  have ‹is_path (π@⇗l⇖ π')› using path path' by (metis π0' path_cons)
  moreover
  have ‹(π@⇗l⇖ π') 0 = π 0› by simp
  moreover
  have ‹(π@⇗l⇖ π') (n' + l) = return› using π0' πn' by auto
  ultimately
  show ‹False› using notn' npd0 unfolding is_pd_def by blast
qed


subsection ‹Facts about Control Dependencies›

lemma icd_imp_cd: ‹n icd⇗π⇖→ k ⟹ n cd⇗π⇖→ k› by (metis is_icdi_def)

lemma ipd_impl_not_cd:  assumes ‹j ∈ {k..i}› and ‹π j = ipd (π k)› shows ‹¬ i cd⇗π⇖→ k› 
  by (metis assms(1) assms(2) is_cdi_def)

lemma cd_not_ret: assumes ‹i cd⇗π⇖→ k › shows ‹π k ≠ return› by (metis is_cdi_def assms nat_less_le term_path_stable)

lemma cd_path_shift: assumes ‹j ≤ k› ‹is_path π › shows ‹(i cd⇗π⇖→ k) = (i - j cd⇗π«j⇖→ k-j)› proof 
  assume a: ‹i cd⇗π⇖→ k›
  hence b: ‹k < i› by (metis is_cdi_def)
  hence ‹is_path (π « j)› ‹k - j < i - j› using assms apply (metis path_path_shift) 
  by (metis assms(1) b diff_less_mono)  
  moreover 
  have c: ‹∀ j ∈ {k..i}. π j ≠ ipd (π k)› by (metis a ipd_impl_not_cd)
  hence ‹∀ ja ∈ {k - j..i - j}. (π « j) ja ≠ ipd ((π « j) (k - j))› using b assms by auto fastforce
  moreover 
  have ‹j < i› using assms(1) b by auto
  hence ‹(π«j) (i - j) ≠ return› using a unfolding is_cdi_def by auto 
  ultimately
  show ‹i - j cd⇗π«j⇖→ k-j› unfolding is_cdi_def by simp
next
  assume a: ‹i - j cd⇗π«j⇖→ k-j›
  hence b: ‹k - j < i-j› by (metis is_cdi_def)
  moreover
  have c: ‹∀ ja ∈ {k - j..i - j}. (π « j) ja ≠ ipd ((π « j) (k - j))› by (metis a ipd_impl_not_cd)
  have ‹∀ j ∈ {k..i}. π j ≠ ipd (π k)› proof (rule,goal_cases) case (1 n)
    hence ‹n-j ∈ {k-j..i-j}› using assms by auto
    hence ‹π (j + (n-j)) ≠ ipd(π (j + (k-j)))› by (metis c path_shift_def)
    thus ‹?case› using 1 assms(1) by auto
  qed
  moreover
  have ‹j < i› using assms(1) b by auto
  hence ‹π i ≠ return› using a unfolding is_cdi_def by auto
  ultimately
  show ‹i cd⇗π⇖→k› unfolding is_cdi_def by (metis assms(1) assms(2) diff_is_0_eq' le_diff_iff nat_le_linear nat_less_le)<