|
|
|
|
Impressum IFC.thy
Sprache: Isabelle
|
|
section ‹Definitions›
text ‹
section contains all necessary definitions of this development. Section~\ref{sec:pm} contains
structural definition of our program model which includes the security specification as well
abstractions of control flow and data. Executions of our program model are defined in
~\ref{sec:ex}. Additional well-formedness properties are defined in section~\ref{sec:wf}.
security property is defined in section~\ref{sec:sec}. Our characterisation of how information
propagated by executions of our program model is defined in section~\ref{sec:char-cp}, for which
correctness result can be found in section~\ref{sec:cor-cp}. Section~\ref{sec:char-scp} contains
additional approximation of this characterisation whose correctness result can be found in
~\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.
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
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
‹σ = snd ((step^^k) (entry,σ))›
text ‹A predicate asserting that a sequence of nodes is a valid program path according to the
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"›
to as indistinguishable security. In order to do so we require notions of observations made
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 (σ)) | 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
are comparable and if the execution for an input state terminates then the observation sequence
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
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
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
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
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,
the index reads a variable written by the earlier index and the variable in question has not
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
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
is critical.›
‹[σ =L σ';
cs σ n = cs σ' n';
h ∈ reads(path σ n);
(σ) h ≠ (σ'') 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
to a pair of matching indices where the variable diverges, the later pair of indices is critical.›
‹[((σ,k),(σ',k')) ∈ cp;
n dd σ,v→ k;
n' dd σ',v→ k';
cs σ n = cs σ' n';
(σ) v ≠ (σ'') v
] ==> ((σ,n),(σ',n')) ∈ cp› |
― ‹If from a pair of critical indices the executions take different branches and one of the critical
is a control dependency of an index that is data dependency of a matched index where diverging
is read and the variable in question is not written by the other execution after the executions
reached matching indices again, then the later matching pair of indices is critical.›
‹[((σ,k),(σ',k')) ∈ cp;
n dd σ,v→ l;
l cd σ→ k;
cs σ n = cs σ' n';
path σ (Suc k) ≠ path σ' (Suc k');
(σ) v ≠ (σ'') v;
∀j'∈{(LEAST i'. k' < i' ∧ (∃i. cs σ i = cs σ' 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
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 σ→ 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 ‹c› 50) where
‹[csπ' k' ≺ csπ k ; π = path σ; π' = path σ' ; π (Suc (π🚫csπ' k')) ≠ π' (Suc k')] ==> (σ', k') c (σ, k)›|
‹[csπ' k' = csπ k ; π = path σ; π' = path σ' ; σ 🛇 (reads (π k)) ≠ σ'' 🛇 (reads (π k))] ==> (σ',k') c (σ,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]: ‹π @ π' = (λn.(if n ≤ m then π n else π' (n-m)))›
definition eq_up_to :: ‹(nat → 'n) → nat → (nat → 'n) → bool› (‹_ = _› [55,55,55] 50) where
‹π = π' = (∀ 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 (π @ π')›
unfolding is_path_def proof(rule,cases)
fix n assume ‹m < n› thus ‹((π @ π') n, (π @ π') (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 ‹((π @ π') n, (π @ π') (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: ‹(π @ π') = π› unfolding eq_up_to_def by auto
lemma eq_up_to_le: assumes ‹k ≤ n› ‹π = π'› shows ‹π = π'› using assms unfolding eq_up_to_def by auto
lemma eq_up_to_refl: shows ‹π = π› unfolding eq_up_to_def by auto
lemma eq_up_to_sym: assumes ‹π = π'› shows ‹π' = π› using assms unfolding eq_up_to_def by auto
lemma eq_up_to_apply: assumes ‹π = π'› ‹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 π'› ‹π = π'› ‹π' 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 ‹π = (π@ π')› by (metis eq_up_to_sym path_append_eq_up_to)
moreover
have ‹is_path (π@ π')› using assms * path_cons by metis
moreover
have ‹(π@ π') (k + n) = return› using * by auto
ultimately
show ‹thesis› using that by blast
qed
lemma path_suc: ‹path σ (Suc k) = fst (step (path σ k, σ))› by (induction ‹k›, auto simp: path_def kth_state_def)
lemma kth_state_suc: ‹σ k = snd (step (path σ 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-1›
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-1› 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 (π @ π')› using path_cons[OF path path'] kx \<pi>'0 by auto
have \<pi>''0: \<open>(\<pi> @\<^bsup>k\<^esup> \<pi>') 0 = z\<close> using \<pi>0 by simp
have \<pi>''n: \<open>(\<pi> @\<^bsup>k\<^esup> \<pi>') (k+n') = return\<close> using \<pi>'n' kx \<pi>'0 by auto
obtain k' where k': \<open>k' \<le> k + n'\<close> \<open>(\<pi> @\<^bsup>k\<^esup> \<pi>') k' = y\<close> using yz path'' \<pi>''0 \<pi>''n unfolding is_pd_def by blast
have **: \<open>k \<le> k'\<close> proof (rule ccontr)
assume \<open>\<not> k \<le> k'\<close>
hence \<open>k' < k\<close> by simp
moreover
hence \<open>\<pi> k' = y\<close> using k' by auto
ultimately
show \<open>False\<close> using k_min by force
qed
hence \<open>\<pi>' (k' - k) = y\<close> using k' \<pi>'0 kx by auto
moreover
have \<open>(k' - k) \<le> n'\<close> using k' by auto
ultimately
have \<open>\<exists> k\<le> n'. \<pi>' k = y\<close> by auto
}
hence \<open>y pd\<rightarrow> x\<close> using kx path_nodes path unfolding is_pd_def by auto
thus \<open>?thesis\<close> ..
next \<comment> \<open>This is analogous argument\<close>
assume kx: \<open>\<pi> k \<noteq> x\<close>
hence ky: \<open>\<pi> k = y\<close> using \<pi>k by auto
have k_min: \<open>\<And> k'. \<pi> k' = x \<Longrightarrow> k \<le> k'\<close> using k_le unfolding k by auto
{
fix \<pi>'
and n' :: \<open>nat\<close>
assume path': \<open>is_path \<pi>'\<close> and \<pi>'0: \<open>\<pi>' 0 = y\<close> and \<pi>'n': \<open>\<pi>' n' = return\<close>
have path'': \<open>is_path (\<pi> @\<^bsup>k\<^esup> \<pi>')\<close> using path_cons[OF path path'] ky \<pi>'0 by auto
have \<pi>''0: \<open>(\<pi> @\<^bsup>k\<^esup> \<pi>') 0 = z\<close> using \<pi>0 by simp
have \<pi>''n: \<open>(\<pi> @\<^bsup>k\<^esup> \<pi>') (k+n') = return\<close> using \<pi>'n' ky \<pi>'0 by auto
obtain k' where k': \<open>k' \<le> k + n'\<close> \<open>(\<pi> @\<^bsup>k\<^esup> \<pi>') k' = x\<close> using xz path'' \<pi>''0 \<pi>''n unfolding is_pd_def by blast
have **: \<open>k \<le> k'\<close> proof (rule ccontr)
assume \<open>\<not> k \<le> k'\<close>
hence \<open>k' < k\<close> by simp
moreover
hence \<open>\<pi> k' = x\<close> using k' by auto
ultimately
show \<open>False\<close> using k_min by force
qed
hence \<open>\<pi>' (k' - k) = x\<close> using k' \<pi>'0 ky by auto
moreover
have \<open>(k' - k) \<le> n'\<close> using k' by auto
ultimately
have \<open>\<exists> k\<le> n'. \<pi>' k = x\<close> by auto
}
hence \<open>x pd\<rightarrow> y\<close> using ky path_nodes path unfolding is_pd_def by auto
thus \<open>?thesis\<close> ..
qed
qed
lemma pds_finite: \<open>finite {y . (x,y) \<in> pdt}\<close> proof cases
assume \<open>x \<in> nodes\<close>
then obtain \<pi> n where \<pi>:\<open>is_path \<pi>\<close> \<open>\<pi> 0 = x\<close> \<open>\<pi> n = return\<close> using reaching_ret by blast
have *: \<open>\<forall> y \<in> {y. (x,y)\<in> pdt}. y pd\<rightarrow> x\<close> using pdt_def by auto
have \<open>\<forall> y \<in> {y. (x,y)\<in> pdt}. \<exists> k \<le> n. \<pi> k = y\<close> using * \<pi> is_pd_def by blast
hence \<open>{y. (x,y)\<in> pdt} \<subseteq> \<pi> ` {..n}\<close> by auto
then show \<open>?thesis\<close> using finite_surj by blast
next
assume \<open>\<not> x\<in> nodes\<close>
hence \<open>{y. (x,y)\<in>pdt} = {}\<close> unfolding pdt_def is_pd_def using path_nodes reaching_ret by fastforce
then show \<open>?thesis\<close> by simp
qed
lemma ipd_exists: assumes node: \<open>x \<in> nodes\<close> and not_ret: \<open>x\<noteq>return\<close> shows \<open>\<exists>y. y ipd\<rightarrow> x\<close>
proof -
let \<open>?Q\<close> = \<open>{y. x\<noteq>y \<and> y pd\<rightarrow> x}\<close>
have *: \<open>return \<in> ?Q\<close> using assms return_pd by simp
hence **: \<open>\<exists> x. x\<in> ?Q\<close> by auto
have fin: \<open>finite ?Q\<close> using pds_finite unfolding pdt_def by auto
have tot: \<open>\<forall> y z. y\<in>?Q \<and> z \<in> ?Q \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z\<close> using pd_total by auto
obtain y where ymax: \<open>y\<in> ?Q\<close> \<open>\<forall> z\<in>?Q. z = y \<or> z pd\<rightarrow> y\<close> using fin ** tot proof (induct)
case empty
then show \<open>?case\<close> by auto
next
case (insert x F) show \<open>thesis\<close> proof (cases \<open>F = {}\<close>)
assume \<open>F = {}\<close>
thus \<open>thesis\<close> using insert(4)[of \<open>x\<close>] by auto
next
assume \<open>F \<noteq> {}\<close>
hence \<open>\<exists> x. x\<in> F\<close> by auto
have \<open>\<And>y. y \<in> F \<Longrightarrow> \<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y \<Longrightarrow> thesis\<close> proof -
fix y assume a: \<open>y \<in> F\<close> \<open>\<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y\<close>
have \<open>x \<noteq> y\<close> using insert a by auto
have \<open>x pd\<rightarrow> y \<or> y pd\<rightarrow> x\<close> using insert(6) a(1) by auto
thus \<open>thesis\<close> proof
assume \<open>x pd\<rightarrow> y\<close>
hence \<open>\<forall>z\<in>insert x F. z = y \<or> z pd\<rightarrow> y\<close> using a(2) by blast
thus \<open>thesis\<close> using a(1) insert(4) by blast
next
assume \<open>y pd\<rightarrow> x\<close>
have \<open>\<forall>z\<in>insert x F. z = x \<or> z pd\<rightarrow> x\<close> proof
fix z assume \<open>z\<in> insert x F\<close> thus \<open>z = x \<or> z pd\<rightarrow> x\<close> proof(rule,simp)
assume \<open>z\<in>F\<close>
hence \<open>z = y \<or> z pd\<rightarrow> y\<close> using a(2) by auto
thus \<open>z = x \<or> z pd\<rightarrow> x\<close> proof(rule,simp add: \<open>y pd\<rightarrow> x\<close>)
assume \<open>z pd\<rightarrow> y\<close>
show \<open>z = x \<or> z pd\<rightarrow> x\<close> using \<open>y pd\<rightarrow> x\<close> \<open>z pd\<rightarrow> y\<close> pd_trans by blast
qed
qed
qed
then show \<open>thesis\<close> using insert by blast
qed
qed
then show \<open>thesis\<close> using insert by blast
qed
qed
hence ***: \<open>y pd\<rightarrow> x\<close> \<open>x\<noteq>y\<close> by auto
have \<open>\<forall> z. z \<noteq> x \<and> z pd\<rightarrow> x \<longrightarrow> z pd\<rightarrow> y\<close> proof (rule,rule)
fix z
assume a: \<open> z \<noteq> x \<and> z pd\<rightarrow> x\<close>
hence b: \<open>z \<in> ?Q\<close> by auto
have \<open>y pd\<rightarrow> z \<or> z pd\<rightarrow> y\<close> using pd_total ***(1) a by auto
thus \<open>z pd\<rightarrow> y\<close> proof
assume c: \<open>y pd\<rightarrow> z\<close>
hence \<open>y = z\<close> using b ymax pdt_def pd_antisym by auto
thus \<open>z pd\<rightarrow> y\<close> using c by simp
qed simp
qed
with *** have \<open>y ipd\<rightarrow> x\<close> unfolding is_ipd_def by simp
thus \<open>?thesis\<close> by blast
qed
lemma ipd_unique: assumes yipd: \<open>y ipd\<rightarrow> x\<close> and y'ipd: \<open>y' ipd\<rightarrow> x\<close> shows \<open>y = y'\<close>
proof -
have 1: \<open>y pd\<rightarrow> y'\<close> and 2: \<open>y' pd\<rightarrow> y\<close> using yipd y'ipd unfolding is_ipd_def by auto
show \<open>?thesis\<close> using pd_antisym[OF 1 2] .
qed
lemma ipd_is_ipd: assumes \<open>x \<in> nodes\<close> and \<open>x\<noteq>return\<close> shows \<open>ipd x ipd\<rightarrow> x\<close> proof -
from assms obtain y where \<open>y ipd\<rightarrow> x\<close> using ipd_exists by auto
moreover
hence \<open>\<And> z. z ipd\<rightarrow>x \<Longrightarrow> z = y\<close> using ipd_unique by simp
ultimately show \<open>?thesis\<close> unfolding ipd_def by (auto intro: theI2)
qed
lemma is_ipd_in_pdt: \<open>y ipd\<rightarrow> x \<Longrightarrow> (x,y) \<in> pdt\<close> unfolding is_ipd_def pdt_def by auto
lemma ipd_in_pdt: \<open>x \<in> nodes \<Longrightarrow> x\<noteq>return \<Longrightarrow> (x,ipd x) \<in> pdt\<close> by (metis ipd_is_ipd is_ipd_in_pdt)
lemma no_pd_path: assumes \<open>x \<in> nodes\<close> and \<open>\<not> y pd\<rightarrow> x\<close>
obtains \<pi> n where \<open>is_path \<pi>\<close> and \<open>\<pi> 0 = x\<close> and \<open>\<pi> n = return\<close> and \<open>\<forall> k \<le> n. \<pi> k \<noteq> y\<close>
proof (rule ccontr)
assume \<open>\<not> thesis\<close>
hence \<open>\<forall> \<pi> n. is_path \<pi> \<and> \<pi> 0 = x \<and> \<pi> n = return \<longrightarrow> (\<exists> k\<le>n . \<pi> k = y)\<close> using that by force
thus \<open>False\<close> using assms unfolding is_pd_def by auto
qed
lemma pd_pd_ipd: assumes \<open>x \<in> nodes\<close> \<open>x\<noteq>return\<close> \<open>y\<noteq>x\<close> \<open>y pd\<rightarrow> x\<close> shows \<open>y pd\<rightarrow> ipd x\<close>
proof -
have \<open>ipd x pd\<rightarrow> x\<close> by (metis assms(1,2) ipd_is_ipd is_ipd_def)
hence \<open>y pd\<rightarrow> ipd x \<or> ipd x pd\<rightarrow> y\<close> by (metis assms(4) pd_total)
thus \<open>?thesis\<close> proof
have 1: \<open>ipd x ipd\<rightarrow> x\<close> by (metis assms(1,2) ipd_is_ipd)
moreover
assume \<open>ipd x pd\<rightarrow> y\<close>
ultimately
show \<open>y pd\<rightarrow> ipd x\<close> unfolding is_ipd_def using assms(3,4) by auto
qed auto
qed
lemma pd_nodes: assumes \<open>y pd\<rightarrow> x\<close> shows pd_node1: \<open>y \<in> nodes\<close> and pd_node2: \<open>x \<in> nodes\<close>
proof -
obtain \<pi> k where \<open>is_path \<pi>\<close> \<open>\<pi> k = y\<close> using assms unfolding is_pd_def using reaching_ret by force
thus \<open>y \<in> nodes\<close> using path_nodes by auto
show \<open>x \<in> nodes\<close> using assms unfolding is_pd_def by simp
qed
lemma pd_ret_is_ret: \<open>x pd\<rightarrow> return \<Longrightarrow> x = return\<close> by (metis pd_antisym pd_node1 return_pd)
lemma ret_path_none_pd: assumes \<open>x \<in> nodes\<close> \<open>x\<noteq>return\<close>
obtains \<pi> n where \<open>is_path \<pi>\<close> \<open>\<pi> 0 = x\<close> \<open>\<pi> n = return\<close> \<open>\<forall> i>0. \<not> x pd\<rightarrow> \<pi> i\<close>
proof(rule ccontr)
assume \<open>\<not>thesis\<close>
hence *: \<open>\<And> \<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = return\<rbrakk> \<Longrightarrow> \<exists>i>0. x pd\<rightarrow> \<pi> i\<close> using that by blast
obtain \<pi> n where **: \<open>is_path \<pi>\<close> \<open>\<pi> 0 = x\<close> \<open>\<pi> n = return\<close> \<open>\<forall> i>0. \<pi> i \<noteq> x\<close> using direct_path_return[OF assms] by metis
then obtain i where ***: \<open>i>0\<close> \<open>x pd\<rightarrow> \<pi> i\<close> using * by blast
hence \<open>\<pi> i \<noteq> return\<close> using pd_ret_is_ret assms(2) by auto
hence \<open>i < n\<close> using assms(2) term_path_stable ** by (metis linorder_neqE_nat less_imp_le)
hence \<open>(\<pi>\<guillemotleft>i)(n-i) = return\<close> using **(3) by auto
moreover
have \<open>(\<pi>\<guillemotleft>i) (0) = \<pi> i\<close> by simp
moreover
have \<open>is_path (\<pi>\<guillemotleft>i)\<close> using **(1) path_path_shift by metis
ultimately
obtain k where \<open>(\<pi>\<guillemotleft>i) k = x\<close> using ***(2) unfolding is_pd_def by metis
hence \<open>\<pi> (i + k) = x\<close> by auto
thus \<open>False\<close> using **(4) \<open>i>0\<close> by auto
qed
lemma path_pd_ipd0': assumes \<open>is_path \<pi>\<close> and \<open>\<pi> n \<noteq> return\<close> \<open>\<pi> n \<noteq> \<pi> 0\<close> and \<open>\<pi> n pd\<rightarrow> \<pi> 0\<close>
obtains k where \<open>k \<le> n\<close> and \<open>\<pi> k = ipd(\<pi> 0)\<close>
proof(rule ccontr)
have *: \<open>\<pi> n pd\<rightarrow> ipd (\<pi> 0)\<close> by (metis is_pd_def assms(3,4) pd_pd_ipd pd_ret_is_ret)
obtain \<pi>' n' where **: \<open>is_path \<pi>'\<close> \<open>\<pi>' 0 = \<pi> n\<close> \<open>\<pi>' n' = return\<close> \<open>\<forall> i>0. \<not> \<pi> n pd\<rightarrow> \<pi>' i\<close> by (metis assms(2) assms(4) pd_node1 ret_path_none_pd)
hence \<open>\<forall> i>0. \<pi>' i \<noteq> ipd (\<pi> 0)\<close> using * by metis
moreover
assume \<open>\<not> thesis\<close>
hence \<open>\<forall> k\<le>n. \<pi> k \<noteq> ipd (\<pi> 0)\<close> using that by blast
ultimately
have \<open>\<forall> i. (\<pi>@\<^bsup>n\<^esup> \<pi>') i \<noteq>
moreover
have \<open>(\<pi>@\<^bsup>n\<^esup> \<pi>') (n + n') = return\<close>
by (metis #include"."
moreover
<(<i@<bsup>n\^sup \pi>' 0 = \pi>0<> (etis path_append_defjava.lang.StringIndexOutOfBoundsException: Index 98 out of bounds for length 98
moreover
have \<open>is_path (\<pi>@\<^bsup>n\<^esup> \< * Returns: size in bytes of the encoded integer - at
moreover
unsig =java.lang.StringIndexOutOfBoundsException: Range [31, 30) out of bounds for length 40
have \<open>\<pi> 0 \<in> nodes\<close> by (metis assms( *@: varint
ultimately
False< by blast
qed
d0 \open>\pi>c> \<pen>>0 \noteq \close>\open\pi>n \<noteq>\pi 0\close>and<><> n \> \<pi> 0<>java.lang.StringIndexOutOfBoundsException: Index 191 out of bounds for length 191
kwhere <>\le>n\close>and\open\p>k =ipd\pi> 0)<lose
proof cases
assume *: \<open>\<pi> n = return\<close>
have \<open>ipd (\<pi> 0) pd\<rightarrow> (\<pi> 0)\<close> by (metis is_ipd_def is_pd_def assms(2,4) ipd_is_ipd)
with assms(1,2,3) * show \<open>thesis\<close> unfolding is_pd_def by (metis that)
next
java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
from java.lang.StringIndexOutOfBoundsException: Index 15 out of bounds for length 14
qed
lemma path_pd_ipd: * @out: on success, decoded
obtains l where \<open>k < l\<close> and \<open>l \<le> n\<close> and \<open>\<pi> l = ipd(\<pi> k)\<close>
proof -
have \<open>is_path (\<pi> \<guillemotleft> k)\<close> \<open>(\<pi> \<guillemotleft> k) 0 \<noteq> return\<close> \<open>(\<pi> \<guillemotleft> k) (n - k) \<noteq> (\<pi> \<guillemotleft> k) 0\<close> \<open>(\<pi> \<guillemotleft> k) (n - k) pd\<rightarrow> (\<pi> \<guillemotleft *@end (e stillreturnanerrorifthevarint extends past@nd).
usingassmspath_path_shift auto
-;
v get_unaligned_le64+in;
}
moreover
hence \<open>\<pi> (k + ka) ipd\<rightarrow> \<pi> k\<close> by (metis assms(1) assms(2) ipd_is_ipd path_nodes)
hence \<open>k < k + ka\<close> unfolding is_ipd_def by (metis nat_neq_iff not_add_less1)
ultimately
show \<open>thesis\<close> using that[of \<open>k+ka\<close>] by auto
qed
lemma path_ret_ipd: assumes \<open>is_path \<pi>\<close> and \<open>\<pi> k \<noteq> return\<close> \<open>\<pi> n = return\<close>
obtains l where \<open>k < l\<close> and \<open>l \<le> n\<close> and \<open>\<pi> l = ipd(\<pi> k)\<close>
proof -
have \<open>\<pi> n \<noteq> \<pi> k\<close> using assms by auto
moreover
have \<open>k \<le> n\<close> apply (rule ccontr) using term_path_stable assms by auto
hence \<open>k < n\<close> by (metis assms(2,3) dual_order.order_iff_strict)
moreover
have \<open>\<pi> n pd\<rightarrow> \<pi> k\<close> by (metis assms(1,3) path_nodes return_pd)
ultimately
obtain l where \<open>k < l\<close> \<open>l \<le> n\<close> \<open>\<pi> l = ipd (\<pi> k)\<close> using assms path_pd_ipd by blast
thus \<open>thesis\<close> using that by auto
qed
lemma pd_intro: assumes \<open>l pd\<rightarrow> k\<close> \<open>is_path \<pi>\<close> \<open>\<pi> 0 = k\<close> \<open>\<pi> n = return\<close>
obtains i where \<open>i \<le> n\<close> \<open>\<pi> i = l\<close> using assms unfolding is_pd_def by metis
lemma path_pd_pd0: assumes path: \<open>is_path \<pi>\<close> and lpdn: \<open>\<pi> l pd\<rightarrow> n\<close> and npd0: \<open>n pd\<rightarrow> \<pi> 0\<close>
obtains k where \<open>k \<le> l\<close> \<open>\<pi> k = n\<close>
proof (rule ccontr)
assume \<open>\<not> thesis\<close>
hence notn: \<open>\<And> k. k \<le> l \<Longrightarrow> \<pi> k \<noteq> n\<close> using that by blast
have nret: \<open>\<pi> l \<noteq> return\<close> by (metis is_pd_def assms(1,3) notn)
obtain \<pi>' n' where path': \<open>is_path \<pi>'\<close> and \<pi>0': \<open>\<pi>' 0 = \<pi> l\<close> and \<pi>n': \<open>\<pi>' n' = return\<close> and nonepd: \<open>\<forall> i>0. \<not> \<pi> l pd\<rightarrow> \<pi>' i\<close>
using nret path path_nodes ret_path_none_pd by metis
have \<open>\<pi> l \<noteq> n\<close> using notn by simp
hence \<open>\<forall> i. \<pi>' i \<noteq> n\<close> using nonepd \<pi>0' lpdn by (metis neq0_conv)
hence notn': \<open>\<forall> i. (\<pi>@\<^bsup>l\<^esup> \<pi>') i \<noteq> n\<close> using notn \<pi>0' by auto
have \<open>is_path (\<pi>@\<^bsup>l\<^esup> \<pi>')\<close> using path path' by (metis \<pi>0' path_cons)
moreover
have \<open>(\<pi>@\<^bsup>l\<^esup> \<pi>') 0 = \<pi> 0\<close> by simp
moreover
have \<open>(\<pi>@\<^bsup>l\<^esup> \<pi>') (n' + l) = return\<close> using \<pi>0' \<pi>n' by auto
ultimately
show \<open>False\<close> using notn' npd0 unfolding is_pd_def by blast
qed
subsection \<open>Facts about Control Dependencies\<close>
lemma icd_imp_cd: \<open>n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> by (metis is_icdi_def)
lemma ipd_impl_not_cd: assumes \<open>j \<in> {k..i}\<close> and \<open>\<pi> j = ipd (\<pi> k)\<close> shows \<open>\<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
by (metis assms(1) assms(2) is_cdi_def)
lemma cd_not_ret: assumes \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<close> shows \<open>\<pi> k \<noteq> return\<close> by (metis is_cdi_def assms nat_less_le term_path_stable)
lemma cd_path_shift: assumes \<open>j \<le> k\<close> \<open>is_path \<pi> \<close> shows \<open>(i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - j cd\<^bsup>\<pi>\<guillemotleft>j\<^esup>\<rightarrow> k-j)\<close> proof
assume a: \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
hence b: \<open>k < i\<close> by (metis is_cdi_def)
hence \<open>is_path (\<pi> \<guillemotleft> j)\<close> \<open>k - j < i - j\<close> using assms apply (metis path_path_shift)
by (metis assms(1) b diff_less_mono)
moreover
have c: \<open>\<forall> j \<in> {k..i}. \<pi> j \<noteq> ipd (\<pi> k)\<close> by (metis a ipd_impl_not_cd)
hence \<open>\<forall> ja \<in> {k - j..i - j}. (\<pi> \<guillemotleft> j) ja \<noteq> ipd ((\<pi> \<guillemotleft> j) (k - j))\<close> using b assms by auto fastforce
moreover
have \<open>j < i\<close> using assms(1) b by auto
hence \<open>(\<pi>\<guillemotleft>j) (i - j) \<noteq> return\<close> using a unfolding is_cdi_def by auto
ultimately
show \<open>i - j cd\<^bsup>\<pi>\<guillemotleft>j\<^esup>\<rightarrow> k-j\<close> unfolding is_cdi_def by simp
next
assume a: \<open>i - j cd\<^bsup>\<pi>\<guillemotleft>j\<^esup>\<rightarrow> k-j\<close>
hence b: \<open>k - j < i-j\<close> by (metis is_cdi_def)
moreover
have c: \<open>\<forall> ja \<in> {k - j..i - j}. (\<pi> \<guillemotleft> j) ja \<noteq> ipd ((\<pi> \<guillemotleft> j) (k - j))\<close> by (metis a ipd_impl_not_cd)
have \<open>\<forall> j \<in> {k..i}. \<pi> j \<noteq> ipd (\<pi> k)\<close> proof (rule,goal_cases) case (1 n)
hence \<open>n-j \<in> {k-j..i-j}\<close> using assms by auto
hence \<open>\<pi> (j + (n-j)) \<noteq> ipd(\<pi> (j + (k-j)))\<close> by (metis c path_shift_def)
thus \<open>?case\<close> using 1 assms(1) by auto
qed
moreover
have \<open>j < i\<close> using assms(1) b by auto
hence \<open>\<pi> i \<noteq> return\<close> using a unfolding is_cdi_def by auto
ultimately
show \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow>k\<close> 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 \<open>is_path \<pi>\<close> shows \<open>(i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i-k cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow>0)\<close>
using cd_path_shift[OF _ assms] by (metis diff_self_eq_0 le_refl)
lemma icd_path_shift: assumes \<open>l \<le> k\<close> \<open>is_path \<pi>\<close> shows \<open>(i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - l icd\<^bsup>\<pi>\<guillemotleft>l\<^esup>\<rightarrow> k - l)\<close>
proof -
have \<open>is_path (\<pi>\<guillemotleft>l)\<close> using path_path_shift assms(2) by auto
moreover
have \<open>(i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - l cd\<^bsup>\<pi>\<guillemotleft>l\<^esup>\<rightarrow> k - l)\<close> using assms cd_path_shift by auto
moreover
have \<open>(\<forall> m \<in> {k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall> m \<in> {k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)\<close>
proof -
{fix m assume *: \<open>\<forall> m \<in> {k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m\<close> \<open>m \<in> {k<..<i}\<close>
hence \<open>m-l \<in> {k-l<..<i-l}\<close> using assms(1) by auto
hence \<open>\<not> i - l cd\<^bsup>\<pi>\<guillemotleft>l\<^esup>\<rightarrow>(m-l)\<close> using * by blast
moreover
have \<open>l \<le> m\<close> using * assms by auto
ultimately have \<open>\<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow>m\<close> using assms(2) cd_path_shift by blast
}
moreover
{fix m assume *: \<open>\<forall> m \<in> {k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> \<open>m-l \<in> {k-l<..<i-l}\<close>
hence \<open>m \<in> {k<..<i}\<close> using assms(1) by auto
hence \<open>\<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow>m\<close> using * by blast
moreover
have \<open>l \<le> m\<close> using * assms by auto
ultimately have \<open>\<not> i - l cd\<^bsup>\<pi>\<guillemotleft>l\<^esup>\<rightarrow>(m-l)\<close> using assms(2) cd_path_shift by blast
}
ultimately show \<open>?thesis\<close> by auto (metis diff_add_inverse)
qed
ultimately
show \<open>?thesis\<close> unfolding is_icdi_def using assms by blast
qed
lemma icd_path_shift0: assumes \<open>is_path \<pi>\<close> shows \<open>(i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i-k icd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow>0)\<close>
using icd_path_shift[OF _ assms] by (metis diff_self_eq_0 le_refl)
lemma cdi_path_swap: assumes \<open>is_path \<pi>'\<close> \<open>j cd\<^bsup>\<pi>\<^esup>\<rightarrow>k\<close> \<open>\<pi> =\<^bsub>j\<^esub> \<pi>'\<close> shows \<open>j cd\<^bsup>\<pi>'\<^esup>\<rightarrow>k\<close> using assms unfolding eq_up_to_def is_cdi_def by auto
lemma cdi_path_swap_le: assumes \<open>is_path \<pi>'\<close> \<open>j cd\<^bsup>\<pi>\<^esup>\<rightarrow>k\<close> \<open>\<pi> =\<^bsub>n\<^esub> \<pi>'\<close> \<open>j \<le> n\<close> shows \<open>j cd\<^bsup>\<pi>'\<^esup>\<rightarrow>k\<close> by (metis assms cdi_path_swap eq_up_to_le)
lemma not_cd_impl_ipd: assumes \<open>is_path \<pi>\<close> and \<open>k < i\<close> and \<open>\<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> and \<open>\<pi> i \<noteq> return\<close> obtains j where \<open>j \<in> {k..i}\<close> and \<open>\<pi> j = ipd (\<pi> k)\<close>
by (metis assms(1) assms(2) assms(3) assms(4) is_cdi_def)
lemma icd_is_the_icd: assumes \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> shows \<open>k = (THE k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)\<close> using assms icd_uniq
by (metis the1_equality)
lemma all_ipd_imp_ret: assumes \<open>is_path \<pi>\<close> and \<open>\<forall> i. \<pi> i \<noteq> return \<longrightarrow> (\<exists> j>i. \<pi> j = ipd (\<pi> i))\<close> shows \<open>\<exists>j. \<pi> j = return\<close>
proof -
{ fix x assume *: \<open>\<pi> 0 = x\<close>
have \<open>?thesis\<close> using wf_pdt_inv * assms
proof(induction \<open>x\<close> arbitrary: \<open>\<pi>\<close> rule: wf_induct_rule )
case (less x \<pi>) show \<open>?case\<close> proof (cases \<open>x = return\<close>)
case True thus \<open>?thesis\<close> using less(2) by auto
next
assume not_ret: \<open>x \<noteq> return\<close>
moreover
then obtain k where k_ipd: \<open>\<pi> k = ipd x\<close> using less(2,4) by auto
moreover
have \<open>x \<in> nodes\<close> using less(2,3) by (metis path_nodes)
ultimately
have \<open>(x, \<pi> k) \<in> pdt\<close> by (metis ipd_in_pdt)
hence a: \<open>(\<pi> k, x) \<in> pdt_inv\<close> unfolding pdt_inv_def by simp
have b: \<open>is_path (\<pi> \<guillemotleft> k)\<close> by (metis less.prems(2) path_path_shift)
have c: \<open>\<forall> i. (\<pi>\<guillemotleft>k) i \<noteq> return \<longrightarrow> (\<exists>j>i. (\<pi>\<guillemotleft>k) j = ipd ((\<pi>\<guillemotleft>k) i))\<close> using less(4) apply auto
by (metis (full_types) ab_semigroup_add_class.add_ac(1) less_add_same_cancel1 less_imp_add_positive)
from less(1)[OF a _ b c]
have \<open>\<exists>j. (\<pi>\<guillemotleft>k) j = return\<close> by auto
thus \<open>\<exists>j. \<pi> j = return\<close> by auto
qed
qed
}
thus \<open>?thesis\<close> by simp
qed
lemma loop_has_cd: assumes \<open>is_path \<pi>\<close> \<open>0 < i\<close> \<open>\<pi> i = \<pi> 0\<close> \<open>\<pi> 0 \<noteq> return\<close> shows \<open>\<exists> k < i. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> proof (rule ccontr)
let \<open>?\<pi>\<close> = \<open>(\<lambda> n. \<pi> (n mod i))\<close>
assume \<open>\<not> (\<exists>k<i. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k)\<close>
hence \<open>\<forall> k <i. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> by blast
hence *: \<open>\<forall> k<i. (\<exists>j \<in> {k..i}. \<pi> j = ipd (\<pi> k))\<close> using assms(1,3,4) not_cd_impl_ipd by metis
have \<open>\<forall> k. (\<exists> j > k. ?\<pi> j = ipd (?\<pi> k))\<close> proof
fix k
have \<open>k mod i < i\<close> using assms(2) by auto
with * obtain j where \<open>j \<in> {(k mod i)..i}\<close> \<open>\<pi> j = ipd (\<pi> (k mod i))\<close> by auto
then obtain j' where 1: \<open>j' < i\<close> \<open>\<pi> j' = ipd (\<pi> (k mod i))\<close>
by (cases \<open>j = i\<close>, auto ,metis assms(2) assms(3),metis le_neq_implies_less)
then obtain j'' where 2: \<open>j'' > k\<close> \<open>j'' mod i = j'\<close> by (metis mod_bound_instance)
hence \<open>?\<pi> j'' = ipd (?\<pi> k)\<close> using 1 by auto
with 2(1)
show \<open>\<exists> j > k. ?\<pi> j = ipd (?\<pi> k)\<close> by auto
qed
moreover
have \<open>is_path ?\<pi>\<close> by (metis assms(1) assms(2) assms(3) is_path_loop)
ultimately
obtain k where \<open>?\<pi> k = return\<close> by (metis (lifting) all_ipd_imp_ret)
moreover
have \<open>k mod i < i\<close> by (simp add: assms(2))
ultimately
have \<open>\<pi> i = return\<close> by (metis assms(1) term_path_stable less_imp_le)
thus \<open>False\<close> by (metis assms(3) assms(4))
qed
lemma loop_has_cd': assumes \<open>is_path \<pi>\<close> \<open>j < i\<close> \<open>\<pi> i = \<pi> j\<close> \<open>\<pi> j \<noteq> return\<close> shows \<open>\<exists> k \<in> {j..<i}. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
proof -
have \<open>\<exists> k'< i-j. i-j cd\<^bsup>\<pi>\<guillemotleft>j\<^esup>\<rightarrow>k'\<close>
apply(rule loop_has_cd)
apply (metis assms(1) path_path_shift)
apply (auto simp add: assms less_imp_le)
done
then obtain k where k: \<open>k<i-j\<close> \<open>i-j cd\<^bsup>\<pi>\<guillemotleft>j\<^esup>\<rightarrow>k\<close> by auto
hence k': \<open>(k+j) < i\<close> \<open>i-j cd\<^bsup>\<pi>\<guillemotleft>j\<^esup>\<rightarrow> (k+j)-j\<close> by auto
note cd_path_shift[OF _ assms(1)]
hence \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k+j\<close> using k'(2) by (metis le_add1 add.commute)
with k'(1) show \<open>?thesis\<close> by force
qed
lemma claim'': assumes path\<pi>: \<open>is_path \<pi>\<close> and path\<pi>': \<open>is_path \<pi>'\<close>
and \<pi>i: \<open>\<pi> i = \<pi>' i'\<close> and \<pi>j: \<open>\<pi> j = \<pi>' j'\<close>
and not_cd: \<open>\<forall> k. \<not> j cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> \<open>\<forall> k. \<not> i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k\<close>
and nret: \<open>\<pi> i \<noteq> return\<close>
and ilj: \<open>i < j\<close>
shows \<open>i' < j'\<close> proof (rule ccontr)
assume \<open>\<not> i' < j'\<close>
hence jlei: \<open>j' \<le> i'\<close> by auto
show \<open>False\<close> proof (cases)
assume j'li': \<open>j' < i'\<close>
define \<pi>'' where \<open>\<pi>'' \<equiv> (\<pi>@\<^bsup>j\<^esup>(\<pi>'\<guillemotleft>j'))\<guillemotleft>i\<close>
note \<pi>''_def[simp]
have \<open>\<pi> j = (\<pi>' \<guillemotleft> j') 0\<close> by (metis path_shift_def Nat.add_0_right \<pi>j)
hence \<open>is_path \<pi>''\<close> using path\<pi> path\<pi>' \<pi>''_def path_path_shift path_cons by presburger
moreover
have \<open>\<pi>'' (j-i+(i'-j')) = \<pi>'' 0\<close> using ilj jlei \<pi>i \<pi>j
by (auto, metis add_diff_cancel_left' le_antisym le_diff_conv le_eq_less_or_eq)
moreover
have \<open>\<pi>'' 0 \<noteq> return\<close> by (simp add: ilj less_or_eq_imp_le nret)
moreover
have \<open>0 < j-i+(i'-j')\<close> by (metis add_is_0 ilj neq0_conv zero_less_diff)
ultimately obtain k where k: \<open>k < j-i+(i'-j')\<close> \<open>j-i+(i'-j') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k\<close> by (metis loop_has_cd)
hence *: \<open>\<forall> l \<in> {k..j-i+(i'-j')}. \<pi>'' l \<noteq> ipd (\<pi>'' k)\<close> by (metis is_cdi_def)
show \<open>False\<close> proof (cases \<open>k < j-i\<close>)
assume a: \<open>k < j - i\<close>
hence b: \<open>\<pi>'' k = \<pi> (i + k)\<close> by auto
have \<open>\<forall> l \<in> {i+k..j}. \<pi> l \<noteq> ipd (\<pi> (i+k))\<close> proof
fix l assume l: \<open>l \<in> {i + k..j}\<close>
hence \<open>\<pi> l = \<pi>'' (l - i)\<close> by auto
moreover
from a l have \<open>l-i \<in> {k .. j-i + (i'-j')}\<close> by force
ultimately show \<open>\<pi> l \<noteq> ipd (\<pi> (i + k))\<close> using * b by auto
qed
moreover
have \<open>i + k < j\<close> using a by simp
moreover
have \<open>\<pi> j \<noteq> return\<close> by (metis \<pi>i \<pi>j j'li' nret path\<pi>' term_path_stable less_imp_le)
ultimately
have \<open>j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i+k\<close> by (metis not_cd_impl_ipd path\<pi>)
thus \<open>False\<close> by (metis not_cd(1))
next
assume \<open>\<not> k < j - i\<close>
hence a: \<open>j - i \<le> k\<close> by simp
hence b: \<open>\<pi>'' k = \<pi>' (j' + (i + k) - j)\<close> unfolding \<pi>''_def path_shift_def path_append_def using ilj
by(auto,metis \<pi>j add_diff_cancel_left' le_antisym le_diff_conv add.commute)
have \<open>\<forall> l \<in> {j' + (i+k) - j..i'}. \<pi>' l \<noteq> ipd (\<pi>' (j' + (i+k) - j))\<close> proof
fix l assume l: \<open>l \<in> {j' + (i+k) - j..i'}\<close>
hence \<open>\<pi>' l = \<pi>'' (j + l - i - j')\<close> unfolding \<pi>''_def path_shift_def path_append_def using ilj
by (auto, metis Nat.diff_add_assoc \<pi>j a add.commute add_diff_cancel_left' add_leD1 le_antisym le_diff_conv)
moreover
from a l have \<open>j + l - i - j' \<in> {k .. j-i + (i'-j')}\<close> by force
ultimately show \<open>\<pi>' l \<noteq> ipd (\<pi>' (j' + (i + k) - j))\<close> using * b by auto
qed
moreover
have \<open>j' + (i+k) - j < i'\<close> using a j'li' ilj k(1) by linarith
moreover
have \<open>\<pi>' i' \<noteq> return\<close> by (metis \<pi>i nret)
ultimately
have \<open>i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> j' + (i+k) - j\<close> by (metis not_cd_impl_ipd path\<pi>')
thus \<open>False\<close> by (metis not_cd(2))
qed
next
assume \<open>\<not> j' < i'\<close>
hence \<open>j' = i'\<close> by (metis \<open>\<not> i' < j'\<close> linorder_cases)
hence \<open>\<pi> i = \<pi> j\<close> by (metis \<pi>i \<pi>j)
thus \<open>False\<close> by (metis ilj loop_has_cd' not_cd(1) nret path\<pi>)
qed
qed
lemma other_claim': assumes path: \<open>is_path \<pi>\<close> and eq: \<open>\<pi> i = \<pi> j\<close> and \<open>\<pi> i \<noteq> return\<close>
and icd: \<open>\<forall> k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> and \<open>\<forall> k. \<not> j cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> shows \<open>i = j\<close>
proof (rule ccontr,cases)
assume \<open>i < j\<close> thus \<open>False\<close> using assms claim'' by blast
next
assume \<open>\<not> i < j\<close> \<open>i \<noteq> j\<close>
hence \<open>j < i\<close> by auto
thus \<open>False\<close> using assms claim'' by (metis loop_has_cd')
qed
lemma icd_no_cd_path_shift: assumes \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<close> shows \<open>(\<forall> k. \<not> i - 1 cd\<^bsup>\<pi>\<guillemotleft>1\<^esup>\<rightarrow> k)\<close>
proof (rule,rule ccontr,goal_cases)
case (1 k)
hence *: \<open>i - 1 cd\<^bsup>\<pi> \<guillemotleft> 1\<^esup>\<rightarrow> k\<close> by simp
have **: \<open>1 \<le> k + 1\<close> by simp
have ***: \<open>is_path \<pi>\<close> by (metis assms is_icdi_def)
hence \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k+1\<close> using cd_path_shift[OF ** ***] * by auto
moreover
hence \<open>k+1 < i\<close> unfolding is_cdi_def by simp
moreover
have \<open>0 < k + 1\<close> by simp
ultimately show \<open>False\<close> using assms[unfolded is_icdi_def] by auto
qed
lemma claim': assumes path\<pi>: \<open>is_path \<pi>\<close> and path\<pi>': \<open>is_path \<pi>'\<close> and
\<pi>i: \<open>\<pi> i = \<pi>' i'\<close> and \<pi>j: \<open>\<pi> j = \<pi>' j'\<close> and not_cd:
\<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<close> \<open>j icd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<close>
\<open>i' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> 0\<close> \<open>j' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> 0\<close>
and ilj: \<open>i < j\<close>
and nret: \<open>\<pi> i \<noteq> return\<close>
shows \<open>i' < j'\<close>
proof -
have g0: \<open>0 < i\<close> \<open>0 < j\<close> \<open>0 < i'\<close> \<open>0 < j'\<close>using not_cd[unfolded is_icdi_def is_cdi_def] by auto
have \<open>(\<pi> \<guillemotleft> 1) (i - 1) = (\<pi>' \<guillemotleft> 1) (i' - 1)\<close> \<open>(\<pi> \<guillemotleft> 1) (j - 1) = (\<pi>' \<guillemotleft> 1) (j' - 1)\<close> using \<pi>i \<pi>j g0 by auto
moreover
have \<open>\<forall> k. \<not> (j - 1) cd\<^bsup>\<pi>\<guillemotleft>1\<^esup>\<rightarrow> k\<close> \<open>\<forall> k. \<not> (i' - 1) cd\<^bsup>\<pi>'\<guillemotleft>1\<^esup>\<rightarrow> k\<close>
by (metis icd_no_cd_path_shift not_cd(2)) (metis icd_no_cd_path_shift not_cd(3))
moreover
have \<open>is_path (\<pi>\<guillemotleft>1)\<close> \<open>is_path (\<pi>'\<guillemotleft>1)\<close> using path\<pi> path\<pi>' path_path_shift by blast+
moreover
have \<open>(\<pi>\<guillemotleft>1) (i - 1) \<noteq> return\<close> using g0 nret by auto
moreover
have \<open>i - 1 < j - 1\<close> using g0 ilj by auto
ultimately have \<open>i' - 1 < j' - 1\<close> using claim'' by blast
thus \<open>i'<j'\<close> by auto
qed
lemma other_claim: assumes path: \<open>is_path \<pi>\<close> and eq: \<open>\<pi> i = \<pi> j\<close> and \<open>\<pi> i \<noteq> return\<close>
and icd: \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<close> and \<open>j icd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<close> shows \<open>i = j\<close> proof (rule ccontr,cases)
assume \<open>i < j\<close> thus \<open>False\<close> using assms claim' by blast
next
assume \<open>\<not> i < j\<close> \<open>i \<noteq> j\<close>
hence \<open>j < i\<close> by auto
thus \<open>False\<close> using assms claim' by (metis less_not_refl)
qed
lemma cd_trans0: assumes \<open>j cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<close> and \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow>j\<close> shows \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<close> proof (rule ccontr)
have path: \<open>is_path \<pi>\<close> and ij: \<open>0 < j\<close> and jk: \<open>j < k\<close>
and nret: \<open>\<pi> j \<noteq> return\<close> \<open>\<pi> k \<noteq> return\<close>
and noipdi: \<open>\<forall> l \<in> {0..j}. \<pi> l \<noteq> ipd (\<pi> 0)\<close>
and noipdj: \<open>\<forall> l \<in> {j..k}. \<pi> l \<noteq> ipd (\<pi> j)\<close>
using assms unfolding is_cdi_def by auto
assume \<open>\<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<close>
hence \<open>\<exists>l \<in> {0..k}. \<pi> l = ipd (\<pi> 0)\<close> unfolding is_cdi_def using path ij jk nret by force
then obtain l where \<open>l \<in> {0..k}\<close> and l: \<open>\<pi> l = ipd (\<pi> 0)\<close> by auto
hence jl: \<open>j<l\<close> and lk: \<open>l\<le>k\<close> using noipdi ij by auto
have pdj: \<open>ipd (\<pi> 0) pd\<rightarrow> \<pi> j\<close> proof (rule ccontr)
have \<open>\<pi> j \<in> nodes\<close> using path by (metis path_nodes)
moreover
assume \<open>\<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> j\<close>
ultimately
obtain \<pi>' n where *: \<open>is_path \<pi>'\<close> \<open>\<pi>' 0 = \<pi> j\<close> \<open>\<pi>' n = return\<close> \<open>\<forall> k\<le>n. \<pi>' k \<noteq> ipd(\<pi> 0)\<close> using no_pd_path by metis
hence path': \<open>is_path (\<pi> @\<^bsup>j\<^esup> \<pi>')\<close> by (metis path path_cons)
moreover
have \<open>\<forall> k \<le> j + n. (\<pi>@\<^bsup>j\<^esup> \<pi>') k \<noteq> ipd (\<pi> 0)\<close> using noipdi *(4) by auto
moreover
have \<open>(\<pi>@\<^bsup>j\<^esup> \<pi>') 0 = \<pi> 0\<close> by auto
moreover
have \<open>(\<pi>@\<^bsup>j\<^esup> \<pi>') (j + n) = return\<close> using *(2,3) by auto
ultimately
have \<open>\<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> 0\<close> unfolding is_pd_def by metis
thus \<open>False\<close> by (metis is_ipd_def ij ipd_is_ipd nret(1) path path_nodes term_path_stable less_imp_le)
qed
hence \<open>(\<pi>\<guillemotleft>j) (l-j) pd\<rightarrow> (\<pi>\<guillemotleft>j) 0\<close> using jl l by auto
moreover
have \<open>is_path (\<pi>\<guillemotleft>j)\<close> by (metis path path_path_shift)
moreover
have \<open>\<pi> l \<noteq> return\<close> by (metis lk nret(2) path term_path_stable)
hence \<open>(\<pi>\<guillemotleft>j) (l-j) \<noteq> return\<close> using jl by auto
moreover
have \<open>\<pi> j \<noteq> ipd (\<pi> 0)\<close> using noipdi by force
hence \<open>(\<pi>\<guillemotleft>j) (l-j) \<noteq> (\<pi>\<guillemotleft>j) 0\<close> using jl l by auto
ultimately
obtain k' where \<open>k' \<le> l-j\<close> and \<open>(\<pi>\<guillemotleft>j) k' = ipd ((\<pi>\<guillemotleft>j) 0)\<close> using path_pd_ipd0' by blast
hence \<open>j + k' \<in> {j..k}\<close> \<open>\<pi> (j+k') = ipd (\<pi> j)\<close> using jl lk by auto
thus \<open>False\<close> using noipdj by auto
qed
lemma cd_trans: assumes \<open>j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<close> and \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow>j\<close> shows \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<close> proof -
have path: \<open>is_path \<pi>\<close> using assms is_cdi_def by auto
have ij: \<open>i<j\<close> using assms is_cdi_def by auto
let \<open>?\<pi>\<close> = \<open>\<pi>\<guillemotleft>i\<close>
have \<open>j-i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> 0\<close> using assms(1) cd_path_shift0 path by auto
moreover
have \<open>k-i cd\<^bsup>?\<pi>\<^esup>\<rightarrow>j-i\<close> by (metis assms(2) cd_path_shift is_cdi_def ij less_imp_le_nat)
ultimately
have \<open>k-i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> 0\<close> using cd_trans0 by auto
thus \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<close> using path cd_path_shift0 by auto
qed
lemma excd_impl_exicd: assumes \<open>\<exists> k. i cd\<^bsup>\<pi>\<^esup>\<rightarrow>k\<close> shows \<open>\<exists> k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow>k\<close>
using assms proof(induction \<open>i\<close> arbitrary: \<open>\<pi>\<close> rule: less_induct)
case (less i)
then obtain k where k: \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow>k\<close> by auto
hence ip: \<open>is_path \<pi>\<close> unfolding is_cdi_def by auto
show \<open>?case\<close> proof (cases)
assume *: \<open>\<forall> m \<in> {k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close>
hence \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow>k\<close> using k ip unfolding is_icdi_def by auto
thus \<open>?case\<close> by auto
next
assume \<open>\<not> (\<forall> m \<in> {k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m)\<close>
then obtain m where m: \<open>m \<in> {k<..<i}\<close> \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> by blast
hence \<open>i - m cd\<^bsup>\<pi>\<guillemotleft>m\<^esup>\<rightarrow> 0\<close> by (metis cd_path_shift0 is_cdi_def)
moreover
have \<open>i - m < i\<close> using m by auto
ultimately
obtain k' where k': \<open>i - m icd\<^bsup>\<pi>\<guillemotleft>m\<^esup>\<rightarrow> k'\<close> using less(1) by blast
hence \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k' + m\<close> using ip
by (metis add.commute add_diff_cancel_right' icd_path_shift le_add1)
thus \<open>?case\<close> by auto
qed
qed
lemma cd_split: assumes \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> and \<open>\<not> i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> obtains m where \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> and \<open>m cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
proof -
have ki: \<open>k < i\<close> using assms is_cdi_def by auto
obtain m where m: \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> using assms(1) by (metis excd_impl_exicd)
hence \<open>k \<le> m\<close> unfolding is_icdi_def using ki assms(1) by force
hence km: \<open>k < m\<close>using m assms(2) by (metis le_eq_less_or_eq)
moreover have \<open>\<pi> m \<noteq> return\<close> using m unfolding is_icdi_def is_cdi_def by (simp, metis term_path_stable less_imp_le)
moreover have \<open>m<i\<close> using m unfolding is_cdi_def is_icdi_def by auto
ultimately
have \<open>m cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> using assms(1) unfolding is_cdi_def by auto
with m that show \<open>thesis\<close> by auto
qed
lemma cd_induct[consumes 1, case_names base IS]: assumes prem: \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> and base: \<open>\<And> i. i icd\<^bsup>\<pi>\<^esup>\<rightarrow>k \<Longrightarrow> P i\<close>
and IH: \<open>\<And> k' i'. k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> P k' \<Longrightarrow> i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k' \<Longrightarrow> P i'\<close> shows \<open>P i\<close>
using prem IH proof (induction \<open>i\<close> rule: less_induct,cases)
case (less i)
assume \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
thus \<open>P i\<close> using base by simp
next
case (less i')
assume \<open>\<not> i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
then obtain k' where k': \<open> i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<close> \<open>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> using less cd_split by blast
hence icdk: \<open>i' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<close> using is_icdi_def by auto
note ih=less(3)[OF k'(2) _ k'(1)]
have ki: \<open>k' < i'\<close> using k' is_icdi_def is_cdi_def by auto
have \<open>P k'\<close> using less(1)[OF ki k'(2) ] less(3) by auto
thus \<open>P i'\<close> using ih by simp
qed
lemma cdi_prefix: \<open>n cd\<^bsup>\<pi>\<^esup>\<rightarrow> m \<Longrightarrow> m < n' \<Longrightarrow> n' \<le> n \<Longrightarrow> n' cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> unfolding is_cdi_def
by (simp, metis term_path_stable)
lemma cr_wn': assumes 1: \<open>n cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> and nc: \<open>\<not> m' cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> and 3: \<open>m < m'\<close> shows \<open>n < m'\<close>
proof (rule ccontr)
assume \<open>\<not> n < m'\<close>
hence \<open>m' \<le> n\<close> by simp
hence \<open>m' cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> by (metis 1 3 cdi_prefix)
thus \<open>False\<close> using nc by simp
qed
lemma cr_wn'': assumes \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> and \<open>j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n\<close> and \<open>\<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> n\<close> and \<open>i \<le> j\<close> shows \<open>m \<le> n\<close> proof (rule ccontr)
assume \<open>\<not>m\<le>n\<close>
hence nm: \<open>n < m\<close> by auto
moreover
have \<open>m<j\<close> using assms(1) assms(4) unfolding is_cdi_def by auto
ultimately
have \<open>m cd\<^bsup>\<pi>\<^esup>\<rightarrow> n\<close> using assms(2) cdi_prefix by auto
thus \<open>False\<close> using assms(3) by auto
qed
lemma ret_no_cd: assumes \<open>\<pi> n = return\<close> shows \<open>\<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> by (metis assms is_cdi_def)
lemma ipd_not_self: assumes \<open>x \<in> nodes\<close> \<open>x\<noteq> return\<close> shows \<open>x \<noteq> ipd x\<close> by (metis is_ipd_def assms ipd_is_ipd)
lemma icd_cs: assumes \<open>l icd\<^bsup>\<pi>\<^esup>\<rightarrow>k\<close> shows \<open>cs\<^bsup>\<pi>\<^esup> l = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> l]\<close>
proof -
from assms have \<open>k = (THE k. l icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)\<close> by (metis icd_is_the_icd)
with assms show \<open>?thesis\<close> by auto
qed
lemma cd_not_pd: assumes \<open>l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> \<open>\<pi> l \<noteq> \<pi> k\<close> shows \<open>\<not> \<pi> l pd\<rightarrow> \<pi> k\<close> proof
assume pd: \<open>\<pi> l pd\<rightarrow> \<pi> k\<close>
have nret: \<open>\<pi> k \<noteq> return\<close> by (metis assms(1) pd pd_ret_is_ret ret_no_cd)
have kl: \<open>k < l\<close> by (metis is_cdi_def assms(1))
have path: \<open>is_path \<pi>\<close> by (metis is_cdi_def assms(1))
from path_pd_ipd[OF path nret assms(2) pd kl]
obtain n where \<open>k < n\<close> \<open>n \<le> l\<close> \<open>\<pi> n = ipd (\<pi> k)\<close> .
thus \<open>False\<close> using assms(1) unfolding is_cdi_def by auto
qed
lemma cd_ipd_is_cd: assumes \<open>k<m\<close> \<open>\<pi> m = ipd (\<pi> k)\<close> \<open>\<forall> n \<in> {k..<m}. \<pi> n \<noteq> ipd (\<pi> k)\<close> and mcdj: \<open>m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close> shows \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close> proof cases
assume \<open>j < k\<close> thus \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close> by (metis mcdj assms(1) cdi_prefix less_imp_le_nat)
next
assume \<open>\<not> j < k\<close>
hence kj: \<open>k \<le> j\<close> by simp
have \<open>k < j\<close> apply (rule ccontr) using kj assms mcdj by (auto, metis is_cdi_def is_ipd_def cd_not_pd ipd_is_ipd path_nodes term_path_stable less_imp_le)
moreover
have \<open>j < m\<close> using mcdj is_cdi_def by auto
hence \<open>\<forall> n \<in> {k..j}. \<pi> n \<noteq> ipd(\<pi> k)\<close> using assms(3) by force
ultimately
have \<open>j cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> by (metis mcdj is_cdi_def term_path_stable less_imp_le)
hence \<open>m cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> by (metis mcdj cd_trans)
hence \<open>False\<close> by (metis is_cdi_def is_ipd_def assms(2) cd_not_pd ipd_is_ipd path_nodes term_path_stable less_imp_le)
thus \<open>?thesis\<close> by simp
qed
lemma ipd_pd_cd0: assumes lcd: \<open>n cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<close> shows \<open>ipd (\<pi> 0) pd\<rightarrow> (\<pi> n)\<close>
proof -
obtain k l where \<pi>0: \<open>\<pi> 0 = k\<close> and \<pi>n: \<open>\<pi> n = l\<close> and cdi: \<open>n cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<close> using lcd unfolding is_cdi_def by blast
have nret: \<open>k \<noteq> return\<close> by (metis is_cdi_def \<pi>0 cdi term_path_stable less_imp_le)
have path: \<open>is_path \<pi>\<close> and ipd: \<open>\<forall> i\<le>n. \<pi> i \<noteq> ipd k\<close> using cdi unfolding is_cdi_def \<pi>0 by auto
{
fix \<pi>' n'
assume path': \<open>is_path \<pi>'\<close>
and \<pi>'0: \<open>\<pi>' 0 = l\<close>
and ret: \<open>\<pi>' n' = return\<close>
have \<open>is_path (\<pi> @\<^bsup>n\<^esup> \<pi>')\<close> using path path' \<pi>n \<pi>'0 by (metis path_cons)
moreover
have \<open>(\<pi> @\<^bsup>n\<^esup> \<pi>') (n+n') = return\<close> using ret \<pi>n \<pi>'0 by auto
moreover
have \<open>(\<pi> @\<^bsup>n\<^esup> \<pi>') 0 = k\<close> using \<pi>0 by auto
moreover
have \<open>ipd k pd\<rightarrow> k\<close> by (metis is_ipd_def path \<pi>0 ipd_is_ipd nret path_nodes)
ultimately
obtain k' where k': \<open>k' \<le> n+n'\<close> \<open>(\<pi> @\<^bsup>n\<^esup> \<pi>') k' = ipd k\<close> by (metis pd_intro)
have \<open>\<not> k'\<le> n\<close> proof
assume \<open>k' \<le> n\<close>
hence \<open>(\<pi> @\<^bsup>n\<^esup> \<pi>') k' = \<pi> k'\<close> by auto
thus \<open>False\<close> using k'(2) ipd by (metis \<open>k' \<le> n\<close>)
qed
hence \<open>(\<pi> @\<^bsup>n\<^esup> \<pi>') k' = \<pi>' (k' - n)\<close> by auto
moreover
have \<open>(k' - n) \<le> n'\<close> using k' by simp
ultimately
have \<open>\<exists> k'\<le>n'. \<pi>' k' = ipd k\<close> unfolding k' by auto
}
moreover
have \<open>l \<in> nodes\<close> by (metis \<pi>n path path_nodes)
ultimately show \<open>ipd (\<pi> 0) pd\<rightarrow> (\<pi> n)\<close> unfolding is_pd_def by (simp add: \<pi>0 \<pi>n)
qed
lemma ipd_pd_cd: assumes lcd: \<open>l cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> shows \<open>ipd (\<pi> k) pd\<rightarrow> (\<pi> l)\<close>
proof -
have \<open>l-k cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow>0\<close> using lcd cd_path_shift0 is_cdi_def by blast
moreover
note ipd_pd_cd0[OF this]
moreover
have \<open>(\<pi> \<guillemotleft> k) 0 = \<pi> k\<close> by auto
moreover
have \<open>k < l\<close> using lcd unfolding is_cdi_def by simp
then have \<open>(\<pi> \<guillemotleft> k) (l - k) = \<pi> l\<close> by simp
ultimately show \<open>?thesis\<close> by simp
qed
lemma cd_is_cd_ipd: assumes km: \<open>k<m\<close> and ipd: \<open>\<pi> m = ipd (\<pi> k)\<close> \<open>\<forall> n \<in> {k..<m}. \<pi> n \<noteq> ipd (\<pi> k)\<close> and cdj: \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close> and nipdj: \<open>ipd (\<pi> j) \<noteq> \<pi> m\<close> shows \<open>m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close> proof -
have path: \<open>is_path \<pi>\<close>
and jk: \<open>j < k\<close>
and nretj: \<open>\<pi> k \<noteq> return\<close>
and nipd: \<open>\<forall> l \<in> {j..k}. \<pi> l \<noteq> ipd (\<pi> j)\<close> using cdj is_cdi_def by auto
have pd: \<open>ipd (\<pi> j) pd\<rightarrow> \<pi> m\<close> by (metis atLeastAtMost_iff cdj ipd(1) ipd_pd_cd jk le_refl less_imp_le nipd nretj path path_nodes pd_pd_ipd)
have nretm: \<open>\<pi> m \<noteq> return\<close> by (metis nipdj pd pd_ret_is_ret)
have jm: \<open>j < m\<close> using jk km by simp
show \<open>m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close> proof (rule ccontr)
assume ncdj: \<open>\<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close>
hence \<open>\<exists> l \<in> {j..m}. \<pi> l = ipd (\<pi> j)\<close> unfolding is_cdi_def by (metis jm nretm path)
then obtain l
where jl: \<open>j \<le> l\<close> and \<open>l \<le> m\<close>
and lipd: \<open>\<pi> l = ipd (\<pi> j)\<close> by force
hence lm: \<open>l < m\<close> using nipdj by (metis le_eq_less_or_eq)
have npd: \<open>\<not> ipd (\<pi> k) pd\<rightarrow> \<pi> l\<close> by (metis ipd(1) lipd nipdj pd pd_antisym)
have nd: \<open>\<pi> l \<in> nodes\<close> using path path_nodes by simp
from no_pd_path[OF nd npd]
obtain \<pi>' n where path': \<open>is_path \<pi>'\<close> and \<pi>'0: \<open>\<pi>' 0 = \<pi> l\<close> and \<pi>'n: \<open>\<pi>' n = return\<close> and nipd: \<open>\<forall> ka\<le>n. \<pi>' ka \<noteq> ipd (\<pi> k)\<close> .
let \<open>?\<pi>\<close> = \<open>(\<pi>@\<^bsup>l\<^esup> \<pi>') \<guillemotleft> k\<close>
have path'': \<open>is_path ?\<pi>\<close> by (metis \<pi>'0 path path' path_cons path_path_shift)
moreover
have kl: \<open>k < l\<close> using lipd cdj jl unfolding is_cdi_def by fastforce
have \<open>?\<pi> 0 = \<pi> k\<close> using kl by auto
moreover
have \<open>?\<pi> (l + n - k) = return\<close> using \<pi>'n \<pi>'0 kl by auto
moreover
have \<open>ipd (\<pi> k) pd\<rightarrow> \<pi> k\<close> by (metis is_ipd_def ipd_is_ipd nretj path path_nodes)
ultimately
obtain l' where l': \<open>l' \<le> (l + n - k)\<close> \<open>?\<pi> l' = ipd (\<pi> k)\<close> unfolding is_pd_def by blast
show \<open>False\<close> proof (cases )
assume *: \<open>k + l' \<le> l\<close>
hence \<open>\<pi> (k + l') = ipd (\<pi> k)\<close> using l' by auto
moreover
have \<open>k + l' < m\<close> by (metis "*" dual_order.strict_trans2 lm)
ultimately
show \<open>False\<close> using ipd(2) by simp
next
assume \<open>\<not> k + l' \<le> l\<close>
hence \<open>\<pi>' (k + l' - l) = ipd (\<pi> k)\<close> using l' by auto
moreover
have \<open>k + l' - l \<le> n\<close> using l' kl by linarith
ultimately
show \<open>False\<close> using nipd by auto
qed
qed
qed
lemma ipd_icd_greatest_cd_not_ipd: assumes ipd: \<open>\<pi> m = ipd (\<pi> k)\<close> \<open>\<forall> n \<in> {k..<m}. \<pi> n \<noteq> ipd (\<pi> k)\<close>
and km: \<open>k < m\<close> and icdj: \<open>m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close> shows \<open>j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)\<close>
proof -
let \<open>?j\<close> = \<open>GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m\<close>
have kcdj: \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close> using assms cd_ipd_is_cd is_icdi_def by blast
have nipd: \<open>ipd (\<pi> j) \<noteq> \<pi> m\<close> using icdj unfolding is_icdi_def is_cdi_def by auto
have bound: \<open>\<And> j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m \<Longrightarrow> j \<le> k\<close> unfolding is_cdi_def by simp
have exists: \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m\<close> (is \<open>?P j\<close>) using kcdj nipd by auto
note GreatestI_nat[of \<open>?P\<close> _ \<open>k\<close>, OF exists] Greatest_le_nat[of \<open>?P\<close> \<open>j\<close> \<open>k\<close>, OF exists]
hence kcdj': \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j\<close> and ipd': \<open>ipd (\<pi> ?j) \<noteq> \<pi> m\<close> and jj: \<open>j \<le> ?j\<close> using bound by auto
hence mcdj': \<open>m cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j\<close> using ipd km cd_is_cd_ipd by auto
show \<open>j = ?j\<close> proof (rule ccontr)
assume \<open>j \<noteq> ?j\<close>
hence jlj: \<open>j < ?j\<close> using jj by simp
moreover
have \<open>?j < m\<close> using kcdj' km unfolding is_cdi_def by auto
ultimately
show \<open>False\<close> using icdj mcdj' unfolding is_icdi_def by auto
qed
qed
lemma cd_impl_icd_cd: assumes \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<close> and \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> and \<open>\<not> i icd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<close> shows \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<close>
using assms cd_split icd_uniq by metis
lemma cdi_is_cd_icdi: assumes \<open>k icd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close> shows \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<longleftrightarrow> j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> i = j\<close>
by (metis assms cd_impl_icd_cd cd_trans icd_imp_cd icd_uniq)
lemma same_ipd_stable: assumes \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<close> \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close> \<open>i<j\<close> \<open>ipd (\<pi> i) = ipd (\<pi> k)\<close> shows \<open>ipd (\<pi> j) = ipd (\<pi> k)\<close>
proof -
have jcdi: \<open>j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<close> by (metis is_cdi_def assms(1,2,3) cr_wn' le_antisym less_imp_le_nat)
have 1: \<open>ipd (\<pi> j) pd\<rightarrow> \<pi> k \<close> by (metis assms(2) ipd_pd_cd)
have 2: \<open>ipd (\<pi> k) pd\<rightarrow> \<pi> j \<close> by (metis assms(4) ipd_pd_cd jcdi)
have 3: \<open>ipd (\<pi> k) pd\<rightarrow> (ipd (\<pi> j))\<close> by (metis 2 IFC_def.is_cdi_def assms(1,2,4) atLeastAtMost_iff jcdi less_imp_le pd_node2 pd_pd_ipd)
have 4: \<open>ipd (\<pi> j) pd\<rightarrow> (ipd (\<pi> k))\<close> by (metis 1 2 IFC_def.is_ipd_def assms(2) cd_not_pd ipd_is_ipd jcdi pd_node2 ret_no_cd)
show \<open>?thesis\<close> using 3 4 pd_antisym by simp
qed
lemma icd_pd_intermediate': assumes icd: \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> and j: \<open>k < j\<close> \<open>j < i\<close> shows \<open>\<pi> i pd\<rightarrow> (\<pi> j)\<close>
using j proof (induction \<open>i - j\<close> arbitrary: \<open>j\<close> rule: less_induct)
case (less j)
have \<open>\<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close> using less.prems icd unfolding is_icdi_def by force
moreover
have \<open>is_path \<pi>\<close> using icd by (metis is_icdi_def)
moreover
have \<open>\<pi> i \<noteq> return\<close> using icd by (metis is_icdi_def ret_no_cd)
ultimately
have \<open>\<exists> l. j \<le> l \<and> l \<le> i \<and> \<pi> l = ipd (\<pi> j)\<close> unfolding is_cdi_def using less.prems by auto
then obtain l where l: \<open>j \<le> l\<close> \<open>l \<le> i\<close> \<open>\<pi> l = ipd (\<pi> j)\<close> by blast
hence lpd: \<open>\<pi> l pd\<rightarrow> (\<pi> j)\<close> by (metis is_ipd_def \<open>\<pi> i \<noteq> return\<close> \<open>is_path \<pi>\<close> ipd_is_ipd path_nodes term_path_stable)
show \<open>?case\<close> proof (cases)
assume \<open>l = i\<close>
thus \<open>?case\<close> using lpd by auto
next
assume \<open>l \<noteq> i\<close>
hence \<open>l < i\<close> using l by simp
moreover
have \<open>j \<noteq> l\<close> using l by (metis is_ipd_def \<open>\<pi> i \<noteq> return\<close> \<open>is_path \<pi>\<close> ipd_is_ipd path_nodes term_path_stable)
hence \<open>j < l\<close> using l by simp
moreover
hence \<open>i - l < i - j\<close> by (metis diff_less_mono2 less.prems(2))
moreover
have \<open>k < l\<close> by (metis l(1) less.prems(1) linorder_neqE_nat not_le order.strict_trans)
ultimately
have \<open>\<pi> i pd\<rightarrow> (\<pi> l)\<close> using less.hyps by auto
thus \<open>?case\<close> using lpd by (metis pd_trans)
qed
qed
lemma icd_pd_intermediate: assumes icd: \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> and j: \<open>k < j\<close> \<open>j \<le> i\<close> shows \<open>\<pi> i pd\<rightarrow> (\<pi> j)\<close>
using assms icd_pd_intermediate'[OF assms(1,2)] apply (cases \<open>j < i\<close>,metis) by (metis is_icdi_def le_neq_trans path_nodes pd_refl)
lemma no_icd_pd: assumes path: \<open>is_path \<pi>\<close> and noicd: \<open>\<forall> l\<ge>n. \<not> k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<close> and nk: \<open>n \<le> k\<close> shows \<open>\<pi> k pd\<rightarrow> \<pi> n\<close>
proof cases
assume \<open>\<pi> k = return\<close> thus \<open>?thesis\<close> by (metis path path_nodes return_pd)
next
assume nret: \<open>\<pi> k \<noteq> return\<close>
have nocd: \<open>\<And> l. n\<le>l \<Longrightarrow> \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<close> proof
fix l assume kcd: \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<close> and nl: \<open>n \<le> l\<close>
hence \<open>(k - n) cd\<^bsup>\<pi>\<guillemotleft>n\<^esup>\<rightarrow> (l - n)\<close> using cd_path_shift[OF nl path] by simp
hence \<open>\<exists> l. (k - n) icd\<^bsup>\<pi>\<guillemotleft>n\<^esup>\<rightarrow> l\<close> using excd_impl_exicd by blast
then obtain l' where "k - n icd\<^bsup>\<pi> \<guillemotleft> n\<^esup>\<rightarrow> l'" ..
hence \<open>k icd\<^bsup>\<pi>\<^esup>\<rightarrow> (l' + n)\<close> using icd_path_shift[of \<open>n\<close> \<open>l' + n\<close> \<open>\<pi>\<close> \<open>k\<close>] path by auto
thus \<open>False\<close> using noicd by auto
qed
hence \<open>\<And>l. n \<le> l \<Longrightarrow> l<k \<Longrightarrow> \<exists> j \<in> {l..k}. \<pi> j = ipd (\<pi> l)\<close> using path nret unfolding is_cdi_def by auto
thus \<open>?thesis\<close> using nk proof (induction \<open>k - n\<close> arbitrary: \<open>n\<close> rule: less_induct,cases)
case (less n)
assume \<open>n = k\<close>
thus \<open>?case\<close> using pd_refl path path_nodes by auto
next
case (less n)
assume \<open>n \<noteq> k\<close>
hence nk: \<open>n < k\<close> using less(3) by auto
with less(2) obtain j where jnk: \<open>j \<in> {n..k}\<close> and ipdj: \<open>\<pi> j = ipd (\<pi> n)\<close> by blast
have nretn: \<open>\<pi> n \<noteq> return\<close> using nk nret term_path_stable path by auto
with ipd_is_ipd path path_nodes is_ipd_def ipdj
have jpdn: \<open>\<pi> j pd\<rightarrow> \<pi> n\<close> by auto
show \<open>?case\<close> proof cases
assume \<open>j = k\<close> thus \<open>?case\<close> using jpdn by simp
next
assume \<open>j \<noteq> k\<close>
hence jk: \<open>j < k\<close> using jnk by auto
have \<open>j \<noteq> n\<close> using ipdj by (metis ipd_not_self nretn path path_nodes)
hence nj: \<open>n < j\<close> using jnk by auto
have *: \<open>k - j < k - n\<close> using jk nj by auto
with less(1)[OF *] less(2) jk nj
have \<open>\<pi> k pd\<rightarrow> \<pi> j\<close> by auto
thus \<open>?thesis\<close> using jpdn pd_trans by metis
qed
qed
qed
lemma first_pd_no_cd: assumes path: \<open>is_path \<pi>\<close> and pd: \<open>\<pi> n pd\<rightarrow> \<pi> 0\<close> and first: \<open>\<forall> l < n. \<pi> l \<noteq> \<pi> n\<close> shows \<open>\<forall> l. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<close>
proof (rule ccontr, goal_cases)
case 1
then obtain l where ncdl: \<open>n cd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<close> by blast
hence ln: \<open>l < n\<close> using is_cdi_def by auto
have \<open>\<not> \<pi> n pd\<rightarrow> \<pi> l\<close> using ncdl cd_not_pd by (metis ln first)
then obtain \<pi>' n' where path': \<open>is_path \<pi>'\<close> and \<pi>0: \<open>\<pi>' 0 = \<pi> l\<close> and \<pi>n: \<open>\<pi>' n' = return\<close> and not\<pi>n: \<open>\<forall> j\<le> n'. \<pi>' j \<noteq> \<pi> n\<close> unfolding is_pd_def using path path_nodes by auto
let \<open>?\<pi>\<close> = \<open>\<pi>@\<^bsup>l\<^esup> \<pi>'\<close>
have \<open>is_path ?\<pi>\<close> by (metis \<pi>0 path path' path_cons)
moreover
have \<open>?\<pi> 0 = \<pi> 0\<close> by auto
moreover
have \<open>?\<pi> (n' + l) = return\<close> using \<pi>0 \<pi>n by auto
ultimately
obtain j where j: \<open>j \<le> n' + l\<close> and jn: \<open>?\<pi> j = \<pi> n\<close> using pd unfolding is_pd_def by blast
show \<open>False\<close> proof cases
assume \<open>j \<le> l\<close> thus \<open>False\<close> using jn first ln by auto
next
assume \<open>\<not> j \<le> l\<close> thus \<open>False\<close> using j jn not\<pi>n by auto
qed
qed
lemma first_pd_no_icd: assumes path: \<open>is_path \<pi>\<close> and pd: \<open>\<pi> n pd\<rightarrow> \<pi> 0\<close> and first: \<open>\<forall> l < n. \<pi> l \<noteq> \<pi> n\<close> shows \<open>\<forall> l. \<not> n icd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<close>
by (metis first first_pd_no_cd icd_imp_cd path pd)
lemma path_nret_ex_nipd: assumes \<open>is_path \<pi>\<close> \<open>\<forall> i. \<pi> i \<noteq> return\<close> shows \<open>\<forall> i. (\<exists> j\<ge>i. (\<forall> k>j. \<pi> k \<noteq> ipd (\<pi> j)))\<close> proof(rule, rule ccontr)
fix i
assume \<open>\<not> (\<exists>j\<ge>i. \<forall> k>j. \<pi> k \<noteq> ipd (\<pi> j))\<close>
hence *: \<open>\<forall> j\<ge>i. (\<exists>k>j. \<pi> k = ipd (\<pi> j))\<close> by blast
have \<open>\<forall> j. (\<exists>k>j. (\<pi>\<guillemotleft>i) k = ipd ((\<pi>\<guillemotleft>i) j))\<close> proof
fix j
have \<open>i + j \<ge> i\<close> by auto
then obtain k where k: \<open>k>i+j\<close> \<open>\<pi> k = ipd (\<pi> (i+j))\<close> using * by blast
hence \<open>(\<pi>\<guillemotleft>i) (k - i) = ipd ((\<pi>\<guillemotleft>i) j)\<close> by auto
moreover
have \<open>k - i > j\<close> using k by auto
ultimately
show \<open>\<exists>k>j. (\<pi>\<guillemotleft>i) k = ipd ((\<pi>\<guillemotleft>i) j)\<close> by auto
qed
moreover
have \<open>is_path (\<pi>\<guillemotleft>i)\<close> using assms(1) path_path_shift by simp
ultimately
obtain k where \<open>(\<pi>\<guillemotleft>i) k = return\<close> using all_ipd_imp_ret by blast
thus \<open>False\<close> using assms(2) by auto
qed
lemma path_nret_ex_all_cd: assumes \<open>is_path \<pi>\<close> \<open>\<forall> i. \<pi> i \<noteq> return\<close> shows \<open>\<forall> i. (\<exists> j\<ge>i. (\<forall> k>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j))\<close>
unfolding is_cdi_def using assms path_nret_ex_nipd[OF assms] by (metis atLeastAtMost_iff ipd_not_self linorder_neqE_nat not_le path_nodes)
lemma path_nret_inf_all_cd: assumes \<open>is_path \<pi>\<close> \<open>\<forall> i. \<pi> i \<noteq> return\<close> shows \<open>\<not> finite {j. \<forall> k>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j}\<close>
using unbounded_nat_set_infinite path_nret_ex_all_cd[OF assms] by auto
lemma path_nret_inf_icd_seq: assumes path: \<open>is_path \<pi>\<close> and nret: \<open>\<forall> i. \<pi> i \<noteq> return\<close>
obtains f where \<open>\<forall> i. f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i\<close> \<open>range f = {i. \<forall> j>i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}\<close> \<open>\<not> (\<exists>i. f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> i)\<close>
proof -
note path_nret_inf_all_cd[OF assms]
then obtain f where ran: \<open>range f = {j. \<forall> k>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j}\<close> and asc: \<open>\<forall> i. f i < f (Suc i)\<close> using infinite_ascending by blast
have mono: \<open>\<forall> i j. i < j \<longrightarrow> f i < f j\<close> using asc by (metis lift_Suc_mono_less)
{
fix i
have cd: \<open>f (Suc i) cd\<^bsup>\<pi>\<^esup>\<rightarrow> f i\<close> using ran asc by auto
have \<open>f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i\<close> proof (rule ccontr)
assume \<open>\<not> f (Suc i) icd\<^bsup>\<pi>\<^esup>\<rightarrow> f i\<close>
then obtain m where im: \<open>f i < m\<close> and mi: \<open> m < f (Suc i)\<close> and cdm: \<open>f (Suc i) cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> unfolding is_icdi_def using assms(1) cd by auto
have \<open>\<forall> k>m. k cd\<^bsup>\<pi>\<^esup>\<rightarrow>m\<close> proof (rule,rule,cases)
fix k assume \<open>f (Suc i) < k\<close>
hence \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> f (Suc i)\<close> using ran by auto
thus \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> using cdm cd_trans by metis
next
fix k assume mk: \<open>m < k\<close> and \<open>\<not> f (Suc i) < k\<close>
hence ik: \<open>k \<le> f (Suc i)\<close> by simp
thus \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> using cdm by (metis cdi_prefix mk)
qed
hence \<open>m \<in> range f\<close> using ran by blast
then obtain j where m: \<open>m = f j\<close> by blast
show \<open>False\<close> using im mi mono unfolding m by (metis Suc_lessI le_less not_le)
qed
}
moreover
{
fix m
assume cdm: \<open>f 0 cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close>
have \<open>\<forall> k>m. k cd\<^bsup>\<pi>\<^esup>\<rightarrow>m\<close> proof (rule,rule,cases)
fix k assume \<open>f 0 < k\<close>
hence \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> f 0\<close> using ran by auto
thus \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> using cdm cd_trans by metis
next
fix k assume mk: \<open>m < k\<close> and \<open>\<not> f 0 < k\<close>
hence ik: \<open>k \<le> f 0\<close> by simp
thus \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> using cdm by (metis cdi_prefix mk)
qed
hence \<open>m \<in> range f\<close> using ran by blast
then obtain j where m: \<open>m = f j\<close> by blast
hence fj0: \<open>f j < f 0\<close> using cdm m is_cdi_def by auto
hence \<open>0 < j\<close> by (metis less_irrefl neq0_conv)
hence \<open>False\<close> using fj0 mono by fastforce
}
ultimately show \<open>thesis\<close> using that ran by blast
qed
lemma cdi_iff_no_strict_pd: \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<longleftrightarrow> is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> return \<and> (\<forall> j \<in> {k..i}. \<not> (\<pi> k, \<pi> j) \<in> pdt)\<close>
proof
assume cd:\<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
have 1: \<open>is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> return\<close> using cd unfolding is_cdi_def by auto
have 2: \<open>\<forall> j \<in> {k..i}. \<not> (\<pi> k, \<pi> j) \<in> pdt\<close> proof (rule ccontr)
assume \<open> \<not> (\<forall>j\<in>{k..i}. (\<pi> k, \<pi> j) \<notin> pdt)\<close>
then obtain j where \<open>j \<in> {k..i}\<close> and \<open>(\<pi> k, \<pi> j) \<in> pdt\<close> by auto
hence \<open>\<pi> j \<noteq> \<pi> k\<close> and \<open>\<pi> j pd\<rightarrow> \<pi> k\<close> unfolding pdt_def by auto
thus \<open>False\<close> using path_pd_ipd by (metis \<open>j \<in> {k..i}\<close> atLeastAtMost_iff cd cd_not_pd cdi_prefix le_eq_less_or_eq)
qed
show \<open>is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> return \<and> (\<forall> j \<in> {k..i}. \<not> (\<pi> k, \<pi> j) \<in> pdt)\<close> using 1 2 by simp
next
assume \<open>is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> return \<and> (\<forall> j \<in> {k..i}. \<not> (\<pi> k, \<pi> j) \<in> pdt)\<close>
thus \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> by (metis ipd_in_pdt term_path_stable less_or_eq_imp_le not_cd_impl_ipd path_nodes)
qed
subsection \<open>Facts about Control Slices\<close>
lemma last_cs: \<open>last (cs\<^bsup>\<pi>\<^esup> i) = \<pi> i\<close> by auto
lemma cs_not_nil: \<open>cs\<^bsup>\<pi>\<^esup> n \<noteq> []\<close> by (auto)
lemma cs_return: assumes \<open>\<pi> n = return\<close> shows \<open>cs\<^bsup>\<pi>\<^esup> n = [\<pi> n]\<close> by (metis assms cs.elims icd_imp_cd ret_no_cd)
lemma cs_0[simp]: \<open>cs\<^bsup>\<pi>\<^esup> 0 = [\<pi> 0]\<close> using is_icdi_def is_cdi_def by auto
lemma cs_inj: assumes \<open>is_path \<pi>\<close> \<open>\<pi> n \<noteq> return\<close> \<open>cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'\<close> shows \<open>n = n'\<close>
using assms proof (induction \<open>cs\<^bsup>\<pi>\<^esup> n\<close> arbitrary: \<open>\<pi>\<close> \<open>n\<close> \<open>n'\<close> rule:rev_induct)
case Nil hence \<open>False\<close> using cs_not_nil by metis thus \<open>?case\<close> by simp
next
case (snoc x xs \<pi> n n') show \<open>?case\<close> proof (cases \<open>xs\<close>)
case Nil
hence *: \<open>\<not> (\<exists> k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow>k)\<close> using snoc(2) cs_not_nil
by (auto,metis append1_eq_conv append_Nil cs_not_nil)
moreover
have \<open>[x] = cs\<^bsup>\<pi>\<^esup> n'\<close> using Nil snoc by auto
hence **: \<open>\<not> (\<exists> k. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow>k)\<close> using cs_not_nil
by (auto,metis append1_eq_conv append_Nil cs_not_nil)
ultimately
have \<open>\<forall> k. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> \<open>\<forall> k. \<not> n' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> using excd_impl_exicd by auto blast+
moreover
hence \<open>\<pi> n = \<pi> n'\<close> using snoc(5,2) by auto (metis * ** list.inject)
ultimately
show \<open>n = n'\<close> using other_claim' snoc by blast
next
case (Cons y ys)
hence *: \<open>\<exists> k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow>k\<close> using snoc(2) by auto (metis append_is_Nil_conv list.distinct(1) list.inject)
then obtain k where k: \<open>n icd\<^bsup>\<pi>\<^esup>\<rightarrow>k\<close> by auto
have \<open>k = (THE k . n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)\<close> using k by (metis icd_is_the_icd)
hence xsk: \<open>xs = cs\<^bsup>\<pi>\<^esup> k\<close> using * k snoc(2) unfolding cs.simps[of \<open>\<pi>\<close> \<open>n\<close>] by | | |