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  boolwhere
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
fU = (λ 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  (kn. π k = y))

text The immediate post dominance relation.
definition is_ipd (infix ipd→ 50)where
y ipd→ x  x  y  y pd→ x  ( z. zx  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). xy  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. hwrites(path σ k); 
   k'<n'. hwrites(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'}. vwrites (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).  ji. 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:kn. P k
shows GreatestBI: P (GREATEST k. kn  P k) and GreatestB: (GREATEST k. kn  P k)  n 
proof -
  show P (GREATEST k. kn  P k) using GreatestI_ex_nat[OF assms] by auto  
  show (GREATEST k. kn  P k)  n using GreatestI_ex_nat[OF assms] by auto
qed

lemma GreatestB_le:
fixes n :: nat
assumes xn and P x
shows x  (GREATEST k. kn  P k) 
proof -
  have *:  y. yn  P y  y<Suc n by auto
  then show x  (GREATEST k. kn  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 ij
    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 kn. π 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: kn. π k = y using ypdx unfolding is_pd_def by auto
  obtain k where k: k = (GREATEST k. kn  π 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 xz 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.  kn. π k = f i using ***(1) f 0  nodes unfolding is_pd_def by blast
  hence πf: i.  kn. π 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 *:  kn. (π k = x  π k = y) (is  kn. ?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: kn 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: xreturn shows y. y ipd→ x 
proof -
  let ?Q = {y. xy  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  zF. z = y  z pd→ y  thesis proof -
        fix y assume a: y  F zF. 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 zinsert 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 zinsert 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 zF
              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 xy 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 xreturn 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  xreturn  (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  ( kn . π k = y) using that by force
  thus False using assms unfolding is_pd_def by auto
qed

lemma pd_pd_ipd: assumes x  nodes xreturn yx 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 xreturn 
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  kn. π 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)
qed 

lemma cd_path_shift0: assumes is_path π shows (i cd⇗π⇖→ k) = (i-k cd⇗π«k⇖→0)
  using cd_path_shift[OF _ assms] by (metis diff_self_eq_0 le_refl)

lemma icd_path_shift: assumes l  k is_path π shows (i icd⇗π⇖→ k) = (i - l icd⇗π«l⇖→ k - l) 
proof -
  have is_path (π«l) using path_path_shift assms(2) by auto
  moreover
  have (i cd⇗π⇖→ k) = (i - l cd⇗π«l⇖→ k - l) using assms cd_path_shift by auto
  moreover 
  have ( m  {k<..<i}. ¬ i cd⇗π⇖→ m) = ( m  {k - l<..<i - l}. ¬ i - l cd⇗π « l⇖→ m) 
  proof -
    {fix m assume *:  m  {k - l<..<i - l}. ¬ i - l cd⇗π « l⇖→ m m  {k<..<i} 
      hence m-l  {k-l<..<i-l} using assms(1) by auto
      hence ¬ i - l cd⇗π«l⇖→(m-l) using * by blast
      moreover
      have l  m using * assms by auto
      ultimately have ¬ i cd⇗π⇖→m using assms(2) cd_path_shift by blast
    }
    moreover
    {fix m assume *:  m  {k<..<i}. ¬ i cd⇗π⇖→ m m-l  {k-l<..<i-l} 
      hence m  {k<..<i} using assms(1) by auto
      hence ¬ i cd⇗π⇖→m using * by blast
      moreover
      have l  m using * assms by auto
      ultimately have ¬ i - l cd⇗π«l⇖→(m-l) using assms(2) cd_path_shift by blast
    }
    ultimately show ?thesis by auto (metis diff_add_inverse)
  qed
  ultimately
  show ?thesis unfolding is_icdi_def using assms by blast
qed

lemma icd_path_shift0: assumes is_path π shows (i icd⇗π⇖→ k) = (i-k icd⇗π«k⇖→0)
  using icd_path_shift[OF _ assms] by (metis diff_self_eq_0 le_refl)

lemma cdi_path_swap: assumes is_path π' j cd⇗π⇖→k π =⇘jπ' shows j cd⇗π'⇖→k using assms unfolding eq_up_to_def is_cdi_def by auto

lemma cdi_path_swap_le: assumes is_path π' j cd⇗π⇖→k π =⇘nπ' j  n shows j cd⇗