Quelle 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 π'0 by auto
have π''0: ‹(π @ π') 0 = z› using π0 by simp
have π''n: ‹(π @ π') (k+n') = return› using π'n' kx π'0 by auto
obtain k' where k': ‹k' ≤ k + n'› ‹(π @ π') k' = y› using yz path'' π''0 π''n unfolding is_pd_def by blast
have **: ‹k ≤ k'› proof (rule ccontr)
assume ‹¬ k ≤ k'›
hence ‹k' < k› by simp
moreover
hence ‹π k' = y› using k' by auto
ultimately
show ‹False› using k_min by force
qed
hence ‹π' (k' - k) = y› using k' π'0 kx by auto
moreover
have ‹(k' - k) ≤ n'› using k' by auto
ultimately
have ‹∃ k≤ n'. π' k = y› by auto
}
hence ‹y pd→ x› using kx path_nodes path unfolding is_pd_def by auto
thus ‹?thesis› ..
next ― ‹This is analogous argument›
assume kx: ‹π k ≠ x›
hence ky: ‹π k = y› using πk by auto
have k_min: ‹∧ k'. π k' = x ==> k ≤ k'› using k_le unfolding k by auto
{
fix π'
and n' :: ‹nat›
assume path': ‹is_path π'› and π'0: ‹π' 0 = y› and π'n': ‹π' n' = return›
have path'': ‹is_path (π @ π')› using path_cons[OF path path'] ky π'0 by auto
have π''0: ‹(π @ π') 0 = z› using π0 by simp
have π''n: ‹(π @ π') (k+n') = return› using π'n' ky π'0 by auto
obtain k' where k': ‹k' ≤ k + n'› ‹(π @ π') k' = x› using xz path'' π''0 π''n unfolding is_pd_def by blast
have **: ‹k ≤ k'› proof (rule ccontr)
assume ‹¬ k ≤ k'›
hence ‹k' < k› by simp
moreover
hence ‹π k' = x› using k' by auto
ultimately
show ‹False› using k_min by force
qed
hence ‹π' (k' - k) = x› using k' π'0 ky by auto
moreover
have ‹(k' - k) ≤ n'› using k' by auto
ultimately
have ‹∃ k≤ n'. π' k = x› by auto
}
hence ‹x pd→ y› using ky path_nodes path unfolding is_pd_def by auto
thus ‹?thesis› ..
qed
qed
lemma pds_finite: ‹finite {y . (x,y) ∈ pdt}› proof cases
assume ‹x ∈ nodes›
then obtain π n where π:‹is_path π› ‹π 0 = x› ‹π n = return› using reaching_ret by blast
have *: ‹∀ y ∈ {y. (x,y)∈ pdt}. y pd→ x› using pdt_def by auto
have ‹∀ y ∈ {y. (x,y)∈ pdt}. ∃ k ≤ n. π k = y› using * π is_pd_def by blast
hence ‹{y. (x,y)∈ pdt} ⊆ π ` {..n}› by auto
then show ‹?thesis› using finite_surj by blast
next
assume ‹¬ x∈ nodes›
hence ‹{y. (x,y)∈pdt} = {}› unfolding pdt_def is_pd_def using path_nodes reaching_ret by fastforce
then show ‹?thesis› by simp
qed
lemma ipd_exists: assumes node: ‹x ∈ nodes› and not_ret: ‹x≠return› shows ‹∃y. y ipd→ x›
proof -
let ‹?Q› = ‹{y. x≠y ∧ y pd→ x}›
have *: ‹return ∈ ?Q› using assms return_pd by simp
hence **: ‹∃ x. x∈ ?Q› by auto
have fin: ‹finite ?Q› using pds_finite unfolding pdt_def by auto
have tot: ‹∀ y z. y∈?Q ∧ z ∈ ?Q ⟶ z pd→ y ∨ y pd→ z› using pd_total by auto
obtain y where ymax: ‹y∈ ?Q› ‹∀ z∈?Q. z = y ∨ z pd→ y› using fin ** tot proof (induct)
case empty
then show ‹?case› by auto
next
case (insert x F) show ‹thesis› proof (cases ‹F = {}›)
assume ‹F = {}›
thus ‹thesis› using insert(4)[of ‹x›] by auto
next
assume ‹F ≠ {}›
hence ‹∃ x. x∈ F› by auto
have ‹∧y. y ∈ F ==> ∀z∈F. z = y ∨ z pd→ y ==> thesis› proof -
fix y assume a: ‹y ∈ F› ‹∀z∈F. z = y ∨ z pd→ y›
have ‹x ≠ y› using insert a by auto
have ‹x pd→ y ∨ y pd→ x› using insert(6) a(1) by auto
thus ‹thesis› proof
assume ‹x pd→ y›
hence ‹∀z∈insert x F. z = y ∨ z pd→ y› using a(2) by blast
thus ‹thesis› using a(1) insert(4) by blast
next
assume ‹y pd→ x›
have ‹∀z∈insert x F. z = x ∨ z pd→ x› proof
fix z assume ‹z∈ insert x F› thus ‹z = x ∨ z pd→ x› proof(rule,simp)
assume ‹z∈F›
hence ‹z = y ∨ z pd→ y› using a(2) by auto
thus ‹z = x ∨ z pd→ x› proof(rule,simp add: ‹y pd→ x›)
assume ‹z pd→ y›
show ‹z = x ∨ z pd→ x› using ‹y pd→ x› ‹z pd→ y› pd_trans by blast
qed
qed
qed
then show ‹thesis› using insert by blast
qed
qed
then show ‹thesis› using insert by blast
qed
qed
hence ***: ‹y pd→ x› ‹x≠y› by auto
have ‹∀ z. z ≠ x ∧ z pd→ x ⟶ z pd→ y› proof (rule,rule)
fix z
assume a: ‹ z ≠ x ∧ z pd→ x›
hence b: ‹z ∈ ?Q› by auto
have ‹y pd→ z ∨ z pd→ y› using pd_total ***(1) a by auto
thus ‹z pd→ y› proof
assume c: ‹y pd→ z›
hence ‹y = z› using b ymax pdt_def pd_antisym by auto
thus ‹z pd→ y› using c by simp
qed simp
qed
with *** have ‹y ipd→ x› unfolding is_ipd_def by simp
thus ‹?thesis› by blast
qed
lemma ipd_unique: assumes yipd: ‹y ipd→ x› and y'ipd: ‹y' ipd→ x› shows ‹y = y'›
proof -
have 1: ‹y pd→ y'› and 2: ‹y' pd→ y› using yipd y'ipd unfolding is_ipd_def by auto
show ‹?thesis› using pd_antisym[OF 1 2] .
qed
lemma ipd_is_ipd: assumes ‹x ∈ nodes› and ‹x≠return› shows ‹ipd x ipd→ x› proof -
from assms obtain y where ‹y ipd→ x› using ipd_exists by auto
moreover
hence ‹∧ z. z ipd→x ==> z = y› using ipd_unique by simp
ultimately show ‹?thesis› unfolding ipd_def by (auto intro: theI2)
qed
lemma is_ipd_in_pdt: ‹y ipd→ x ==> (x,y) ∈ pdt› unfolding is_ipd_def pdt_def by auto
lemma ipd_in_pdt: ‹x ∈ nodes ==> x≠return ==> (x,ipd x) ∈ pdt› by (metis ipd_is_ipd is_ipd_in_pdt)
lemma no_pd_path: assumes ‹x ∈ nodes› and ‹¬ y pd→ x›
obtains π n where ‹is_path π› and ‹π 0 = x› and ‹π n = return› and ‹∀ k ≤ n. π k ≠ y›
proof (rule ccontr)
assume ‹¬ thesis›
hence ‹∀ π n. is_path π ∧ π 0 = x ∧ π n = return ⟶ (∃ k≤n . π k = y)› using that by force
thus ‹False› using assms unfolding is_pd_def by auto
qed
lemma pd_pd_ipd: assumes ‹x ∈ nodes› ‹x≠return› ‹y≠x› ‹y pd→ x› shows ‹y pd→ ipd x›
proof -
have ‹ipd x pd→ x› by (metis assms(1,2) ipd_is_ipd is_ipd_def)
hence ‹y pd→ ipd x ∨ ipd x pd→ y› by (metis assms(4) pd_total)
thus ‹?thesis› proof
have 1: ‹ipd x ipd→ x› by (metis assms(1,2) ipd_is_ipd)
moreover
assume ‹ipd x pd→ y›
ultimately
show ‹y pd→ ipd x› unfolding is_ipd_def using assms(3,4) by auto
qed auto
qed
lemma pd_nodes: assumes ‹y pd→ x› shows pd_node1: ‹y ∈ nodes› and pd_node2: ‹x ∈ nodes›
proof -
obtain π k where ‹is_path π› ‹π k = y› using assms unfolding is_pd_def using reaching_ret by force
thus ‹y ∈ nodes› using path_nodes by auto
show ‹x ∈ nodes› using assms unfolding is_pd_def by simp
qed
lemma pd_ret_is_ret: ‹x pd→ return ==> x = return› by (metis pd_antisym pd_node1 return_pd)
lemma ret_path_none_pd: assumes ‹x ∈ nodes› ‹x≠return›
obtains π n where ‹is_path π› ‹π 0 = x› ‹π n = return› ‹∀ i>0. ¬ x pd→ π i›
proof(rule ccontr)
assume ‹¬thesis›
hence *: ‹∧ π n. [is_path π; π 0 = x; π n = return] ==> ∃i>0. x pd→ π i› using that by blast
obtain π n where **: ‹is_path π› ‹π 0 = x› ‹π n = return› ‹∀ i>0. π i ≠ x› using direct_path_return[OF assms] by metis
then obtain i where ***: ‹i>0› ‹x pd→ π i› using * by blast
hence ‹π i ≠ return› using pd_ret_is_ret assms(2) by auto
hence ‹i < n› using assms(2) term_path_stable ** by (metis linorder_neqE_nat less_imp_le)
hence ‹(π«i)(n-i) = return› using **(3) by auto
moreover
have ‹(π«i) (0) = π i› by simp
moreover
have ‹is_path (π«i)› using **(1) path_path_shift by metis
ultimately
obtain k where ‹(π«i) k = x› using ***(2) unfolding is_pd_def by metis
hence ‹π (i + k) = x› by auto
thus ‹False› using **(4) ‹i>0› by auto
qed
lemma path_pd_ipd0': assumes ‹is_path π› and ‹π n ≠ return› ‹π n ≠ π 0› and ‹π n pd→ π 0›
obtains k where ‹k ≤ n› and ‹π k = ipd(π 0)›
proof(rule ccontr)
have *: ‹π n pd→ ipd (π 0)› by (metis is_pd_def assms(3,4) pd_pd_ipd pd_ret_is_ret)
obtain π' n' where **: ‹is_path π'› ‹π' 0 = π n› ‹π' n' = return› ‹∀ i>0. ¬ π n pd→ π' i› by (metis assms(2) assms(4) pd_node1 ret_path_none_pd)
hence ‹∀ i>0. π' i ≠ ipd (π 0)› using * by metis
moreover
assume ‹¬ thesis›
hence ‹∀ k≤n. π k ≠ ipd (π 0)› using that by blast
ultimately
have ‹∀ i. (π@ π') i ≠ ipd (π 0)› by (metis diff_is_0_eq neq0_conv path_append_def)
moreover
have ‹(π@ π') (n + n') = return›
by (metis ‹π' 0 = π n› ‹π' n' = return› add_diff_cancel_left' assms(2
moreover
haveopenpi\bsupn<esup le0
moreover
have ‹is_path (π@ π')› by (metis ‹π' 0 = π n› ‹is_path π'› assms(1) path_cons)
moreover
have ‹ipd (π 0) pd→ π 0›
moreover
have ‹
show ‹False› unfolding is_pd_def by blast
path_pd_ipd0: assumes ‹is_path π› and ‹π 0 ≠ return› ‹π n ≠ π 0› and ‹π n pd→ π 0›
k where ‹k ≤ n› and ‹π k = ipd(π 0)›
cases
assume *: ‹π n = return›
have ‹ipd (π 0) pd→ (π 0)› by (metis is_ipd_def is_pd_def assms(2,4) ipd_is_ipd)
with assms(1,2,3) * show ‹thesis› unfolding is_pd_def by (metis that)
assume ‹π n ≠ return›
from path_pd_ipd0' [OF assms(1) this assms(3,4)] that show ‹thesis› by auto
path_pd_ipd: assumes ‹is_path π› and ‹π k ≠ return› ‹π n ≠ π k› and ‹π n pd→ π k› and kn: ‹k < n›
l where ‹k < l› and ‹l ≤ n› and ‹π l = ipd(π k)›
-
have ‹is_path (π « k)› ‹(π « k) 0 ≠ return› ‹(π « k) (n - k) ≠ (π « k) 0› ‹(π « k) (n - k) pd→ (π « k) 0›
using assms path_path_shift by auto
with path_pd_ipd0[of ‹π«k› ‹n-k›]
obtain ka where ‹ka ≤ n - k› ‹(π « k) ka = ipd ((π « k) 0)› .
hence ‹k + ka ≤ n› ‹π (k + ka) = ipd (π k)› using kn by auto
moreover
hence ‹π (k + ka) ipd→ π k› by (metis assms(1) assms(2) ipd_is_ipd path_nodes)
hence ‹k < k + ka› unfolding is_ipd_def by (metis nat_neq_iff not_add_less1)
ultimately
show ‹thesis› using that[of ‹k+ka›] by auto
path_ret_ipd: assumes ‹is_path π› and ‹π k ≠ return› ‹π n = return›
l where ‹k < l› and ‹l ≤ n› and ‹π l = ipd(π k)›
-
have ‹π n ≠ π k› using assms by auto
moreover
have ‹k ≤ n› apply (rule ccontr) using term_path_stable assms by auto
hence ‹k < n› by (metis assms(2,3) dual_order.order_iff_strict)
moreover
have ‹π n pd→ π k› by (metis assms(1,3) path_nodes return_pd)
ultimately
obtain l where ‹k < l› ‹l ≤ n› ‹π l = ipd (π k)› using assms path_pd_ipd by blast
thus ‹thesis› using that by auto
pd_intro: assumes ‹l pd→ k› ‹is_path π› ‹π 0 = k› ‹π n = return›
i where ‹i ≤ n› ‹π i = l› using assms unfolding is_pd_def by metis
path_pd_pd0: assumes path: ‹is_path π› and lpdn: ‹π l pd→ n› and npd0: ‹n pd→ π 0›
k where ‹k ≤ l› ‹π k = n›
(rule ccontr)
assume ‹¬ thesis›
hence notn: ‹∧ k. k ≤ l ==> π k ≠ n› using that by blast
have nret: ‹π l ≠ return› by (metis is_pd_def assms(1,3) notn)
obtain π' n' where path': ‹is_path π'› and π0': ‹π' 0 = π l› and πn': ‹π' n' = return› and nonepd: ‹∀ i>0. ¬ π l pd→ π' i›
using nret path path_nodes ret_path_none_pd by metis
have ‹π l ≠ n› using notn by simp
hence ‹∀ i. π' i ≠ n› using nonepd π0' lpdn by (metis neq0_conv)
hence notn': ‹∀ i. (π@ π') i ≠ n› using notn π0' by auto
have ‹is_path (π@ π')› using path path' by (metis π0' path_cons)
moreover
have ‹(π@ π') 0 = π 0› by simp
moreover
have ‹(π@ π') (n' + l) = return› using π0' πn' by auto
ultimately
show ‹False› using notn' npd0 unfolding is_pd_def by blast
‹Facts about Control Dependencies›
icd_imp_cd: ‹n icdπ→ k ==> n cdπ→ k› by (metis is_icdi_def)
ipd_impl_not_cd: assumes ‹j ∈ {k..i}› and ‹π j = ipd (π k)› shows ‹¬ i cdπ→ k›
by (metis assms(1) assms(2) is_cdi_def)
cd_not_ret: assumes ‹i cdπ→ k › shows ‹π k ≠ return› by (metis is_cdi_def assms nat_less_le term_path_stable)
cd_path_shift: assumes ‹j ≤ k› ‹is_path π › shows ‹(i cdπ→ k) = (i - j cdπ«j→ k-j)› proof
assume a: ‹i cdπ→ k›
hence b: ‹k < i› by (metis is_cdi_def)
hence ‹is_path (π « j)› ‹k - j < i - j› using assms apply (metis path_path_shift)
by (metis assms(1) b diff_less_mono)
moreover
have c: ‹∀ j ∈ {k..i}. π j ≠ ipd (π k)› by (metis a ipd_impl_not_cd)
hence ‹∀ ja ∈ {k - j..i - j}. (π « j) ja ≠ ipd ((π « j) (k - j))› using b assms by auto fastforce
moreover
have ‹j < i› using assms(1) b by auto
hence ‹(π«j) (i - j) ≠ return› using a unfolding is_cdi_def by auto
ultimately
show ‹i - j cdπ«j→ k-j› unfolding is_cdi_def by simp
assume a: ‹i - j cdπ«j→ k-j›
hence b: ‹k - j < i-j› by (metis is_cdi_def)
moreover
have c: ‹∀ ja ∈ {k - j..i - j}. (π « j) ja ≠ ipd ((π « j) (k - j))› by (metis a ipd_impl_not_cd)
have ‹∀ j ∈ {k..i}. π j ≠ ipd (π k)› proof (rule,goal_cases) case (1 n)
hence ‹n-j ∈ {k-j..i-j}› using assms by auto
hence ‹π (j + (n-j)) ≠ ipd(π (j + (k-j)))› by (metis c path_shift_def)
thus ‹?case› using 1 assms(1) by auto
qed
moreover
have ‹j < i› using assms(1) b by auto
hence ‹π i ≠ return› using a unfolding is_cdi_def by auto
ultimately
show ‹i cdπ→k› unfolding is_cdi_def by (metis assms(1) assms(2) diff_is_0_eq' le_diff_iff nat_le_linear nat_less_le)
cd_path_shift0: assumes ‹is_path π› shows ‹(i cdπ→ k) = (i-k cdπ«k→0)›
using cd_path_shift[OF _ assms] by (metis diff_self_eq_0 le_refl)
icd_path_shift: assumes ‹l ≤ k› ‹is_path π› shows ‹(i icdπ→ k) = (i - l icdπ«l→ k - l)›
-
have ‹is_path (π«l)› using path_path_shift assms(2) by auto
moreover
have ‹(i cdπ→ k) = (i - l cdπ«l→ k - l)› using assms cd_path_shift by auto
moreover
have ‹(∀ m ∈ {k<..<i}. ¬ i cdπ→ m) = (∀ m ∈ {k - l<..<i - l}. ¬ i - l cdπ « l→ m)›
proof -
{fix m assume *: ‹∀ m ∈ {k - l<..<i - l}. ¬ i - l cdπ « l→ m› ‹m ∈ {k<..<i}›
hence ‹m-l ∈ {k-l<..<i-l}› using assms(1) by auto
hence ‹¬ i - l cdπ«l→(m-l)› using * by blast
moreover
have ‹l ≤ m› using * assms by auto
ultimately have ‹¬ i cdπ→m› using assms(2) cd_path_shift by blast
}
moreover
{fix m assume *: ‹∀ m ∈ {k<..<i}. ¬ i cdπ→ m› ‹m-l ∈ {k-l<..<i-l}›
hence ‹m ∈ {k<..<i}› using assms(1) by auto
hence ‹¬ i cdπ→m› using * by blast
moreover
have ‹l ≤ m› using * assms by auto
ultimately have ‹¬ i - l cdπ«l→(m-l)› using assms(2) cd_path_shift by blast
}
ultimately show ‹?thesis› by auto (metis diff_add_inverse)
qed
ultimately
show ‹?thesis› unfolding is_icdi_def using assms by blast
icd_path_shift0: assumes ‹is_path π› shows ‹(i icdπ→ k) = (i-k icdπ«k→0)›
using icd_path_shift[OF _ assms] by (metis diff_self_eq_0 le_refl)
cdi_path_swap: assumes ‹is_path π'› ‹j cdπ→k› ‹π = π'› shows ‹j cdπ'→k› using assms unfolding eq_up_to_def is_cdi_def by auto
cdi_path_swap_le: assumes ‹is_path π'› ‹j cdπ→k› ‹π = π'› ‹j ≤ n› shows ‹j cdπ'→k› by (metis assms cdi_path_swap eq_up_to_le)
not_cd_impl_ipd: assumes ‹is_path π› and ‹k < i› and ‹¬ i cdπ→ k› and ‹π i ≠ return› obtains j where ‹j ∈ {k..i}› and ‹π j = ipd (π k)›
(metis assms(1) assms(2) assms(3) assms(4) is_cdi_def)
icd_is_the_icd: assumes ‹i icdπ→ k› shows ‹k = (THE k. i icdπ→ k)› using assms icd_uniq
by (metis the1_equality)
all_ipd_imp_ret: assumes ‹is_path π› and ‹∀ i. π i ≠ return ⟶ (∃ j>i. π j = ipd (π i))› shows ‹∃j. π j = return›
-
{ fix x assume *: ‹π 0 = x›
have ‹?thesis› using wf_pdt_inv * assms
proof(induction ‹x› arbitrary: ‹π› rule: wf_induct_rule )
case (less x π) show ‹?case› proof (cases ‹x = return›)
case True thus ‹?thesis› using less(2) by auto
next
assume not_ret: ‹x ≠ return›
moreover
then obtain k where k_ipd: ‹π k = ipd x› using less(2,4) by auto
moreover
have ‹x ∈ nodes› using less(2,3) by (metis path_nodes)
ultimately
have ‹(x, π k) ∈ pdt› by (metis ipd_in_pdt)
hence a: ‹(π k, x) ∈ pdt_inv› unfolding pdt_inv_def by simp
have b: ‹is_path (π « k)› by (metis less.prems(2) path_path_shift)
have c: ‹∀ i. (π«k) i ≠ return ⟶ (∃j>i. (π«k) j = ipd ((π«k) i))› 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 ‹∃j. (π«k) j = return› by auto
thus ‹∃j. π j = return› by auto
qed
qed
}
thus ‹?thesis› by simp
loop_has_cd: assumes ‹is_path π› ‹0 < i› ‹π i = π 0› ‹π 0 ≠ return› shows ‹∃ k < i. i cdπ→ k› proof (rule ccontr)
let ‹?π› = ‹(λ n. π (n mod i))›
assume ‹¬ (∃k<i. i cdπ→ k)›
hence ‹∀ k <i. ¬ i cdπ→ k› by blast
hence *: ‹∀ k<i. (∃j ∈ {k..i}. π j = ipd (π k))› using assms(1,3,4) not_cd_impl_ipd by metis
have ‹∀ k. (∃ j > k. ?π j = ipd (?π k))› proof
fix k
have ‹k mod i < i› using assms(2) by auto
with * obtain j where ‹j ∈ {(k mod i)..i}› ‹π j = ipd (π (k mod i))› by auto
then obtain j' where 1: ‹j' < i› ‹π j' = ipd (π (k mod i))›
by (cases ‹j = i›, auto ,metis assms(2) assms(3),metis le_neq_implies_less)
then obtain j'' where 2: ‹j'' > k› ‹j'' mod i = j'› by (metis mod_bound_instance)
hence ‹?π j'' = ipd (?π k)› using 1 by auto
with 2(1)
show ‹∃ j > k. ?π j = ipd (?π k)› by auto
qed
moreover
have ‹is_path ?π› by (metis assms(1) assms(2) assms(3) is_path_loop)
ultimately
obtain k where ‹?π k = return› by (metis (lifting) all_ipd_imp_ret)
moreover
have ‹k mod i < i› by (simp add: assms(2))
ultimately
have ‹π i = return› by (metis assms(1) term_path_stable less_imp_le)
thus ‹False› by (metis assms(3) assms(4))
loop_has_cd': assumes ‹is_path π› ‹j < i› ‹π i = π j› ‹π j ≠ return› shows ‹∃ k ∈ {j..<i}. i cdπ→ k›
-
have ‹∃ k'< i-j. i-j cdπ«j→k'›
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: ‹k<i-j› ‹i-j cdπ«j→k› by auto
hence k': ‹(k+j) < i› ‹i-j cdπ«j→ (k+j)-j› by auto
note cd_path_shift[OF _ assms(1)]
hence ‹i cdπ→ k+j› using k'(2) by (metis le_add1 add.commute)
with k'(1) show ‹?thesis› by force
claim'': assumes pathπ: ‹is_path π› and pathπ': ‹is_path π'›
πi: ‹π i = π' i'› and πj: ‹π j = π' j'›
not_cd: ‹∀ k. ¬ j cdπ→ k› ‹∀ k. ¬ i' cdπ'→ k›
nret: ‹π i ≠ return›
ilj: ‹i < j›
‹i' < j'› proof (rule ccontr)
assume ‹¬ i' < j'›
hence jlei: ‹j' ≤ i'› by auto
show ‹False› proof (cases)
assume j'li': ‹j' < i'›
define π'' where ‹π'' ≡ (π@(π'«j'))«i›
note π''_def[simp]
have ‹π j = (π' « j') 0› by (metis path_shift_def Nat.add_0_right πj)
hence ‹is_path π''› using pathπ pathπ' π''_def path_path_shift path_cons by presburger
moreover
have ‹π'' (j-i+(i'-j')) = π'' 0› using ilj jlei πi πj
by (auto, metis add_diff_cancel_left' le_antisym le_diff_conv le_eq_less_or_eq)
moreover
have ‹π'' 0 ≠ return› by (simp add: ilj less_or_eq_imp_le nret)
moreover
have ‹0 < j-i+(i'-j')› by (metis add_is_0 ilj neq0_conv zero_less_diff)
ultimately obtain k where k: ‹k < j-i+(i'-j')› ‹j-i+(i'-j') cdπ''→ k› by (metis loop_has_cd)
hence *: ‹∀ l ∈ {k..j-i+(i'-j')}. π'' l ≠ ipd (π'' k)› by (metis is_cdi_def)
show ‹False› proof (cases ‹k < j-i›)
assume a: ‹k < j - i›
hence b: ‹π'' k = π (i + k)› by auto
have ‹∀ l ∈ {i+k..j}. π l ≠ ipd (π (i+k))› proof
fix l assume l: ‹l ∈ {i + k..j}›
hence ‹π l = π'' (l - i)› by auto
moreover
from a l have ‹l-i ∈ {k .. j-i + (i'-j')}› by force
ultimately show ‹π l ≠ ipd (π (i + k))› using * b by auto
qed
moreover
have ‹i + k < j› using a by simp
moreover
have ‹π j ≠ return› by (metis πi πj j'li' nret pathπ' term_path_stable less_imp_le)
ultimately
have ‹j cdπ→ i+k› by (metis not_cd_impl_ipd pathπ)
thus ‹False› by (metis not_cd(1))
next
assume ‹¬ k < j - i›
hence a: ‹j - i ≤ k› by simp
hence b: ‹π'' k = π' (j' + (i + k) - j)› unfolding π''_def path_shift_def path_append_def using ilj
by(auto,metis πj add_diff_cancel_left' le_antisym le_diff_conv add.commute)
have ‹∀ l ∈ {j' + (i+k) - j..i'}. π' l ≠ ipd (π' (j' + (i+k) - j))› proof
fix l assume l: ‹l ∈ {j' + (i+k) - j..i'}›
hence ‹π' l = π'' (j + l - i - j')› unfolding π''_def path_shift_def path_append_def using ilj
by (auto, metis Nat.diff_add_assoc πj a add.commute add_diff_cancel_left' add_leD1 le_antisym le_diff_conv)
moreover
from a l have ‹j + l - i - j' ∈ {k .. j-i + (i'-j')}› by force
ultimately show ‹π' l ≠ ipd (π' (j' + (i + k) - j))› using * b by auto
qed
moreover
have ‹j' + (i+k) - j < i'› using a j'li' ilj k(1) by linarith
moreover
have ‹π' i' ≠ return› by (metis πi nret)
ultimately
have ‹i' cdπ'→ j' + (i+k) - j› by (metis not_cd_impl_ipd pathπ')
thus ‹False› by (metis not_cd(2))
qed
next
assume ‹¬ j' < i'›
hence ‹j' = i'› by (metis ‹¬ i' < j'› linorder_cases)
hence ‹π i = π j› by (metis πi πj)
thus ‹False› by (metis ilj loop_has_cd' not_cd(1) nret pathπ)
other_claim': assumes path: ‹is_path π› and eq: ‹π i = π j› and ‹π i ≠ return›
icd: ‹∀ k. ¬ i cdπ→ k› and ‹∀ k. ¬ j cdπ→ k› shows ‹i = j›
(rule ccontr,cases)
assume ‹i < j› thus ‹False› using assms claim'' by blast
assume ‹¬ i < j› ‹i ≠ j›
hence ‹j < i› by auto
thus ‹False› using assms claim'' by (metis loop_has_cd')
icd_no_cd_path_shift: assumes ‹i icdπ→ 0› shows ‹(∀ k. ¬ i - 1 cdπ«1→ k)›
(rule,rule ccontr,goal_cases)
case (1 k)
hence *: ‹i - 1 cdπ « 1→ k› by simp
have **: ‹1 ≤ k + 1› by simp
have ***: ‹is_path π› by (metis assms is_icdi_def)
hence ‹i cdπ→ k+1› using cd_path_shift[OF ** ***] * by auto
moreover
hence ‹k+1 < i› unfolding is_cdi_def by simp
moreover
have ‹0 < k + 1› by simp
ultimately show ‹False› using assms[unfolded is_icdi_def] by auto
claim': assumes pathπ: ‹is_path π› and pathπ': ‹is_path π'› and
πi: ‹π i = π' i'› and πj: ‹π j = π' j'› and not_cd:
‹i icdπ→ 0› ‹j icdπ→ 0›
‹i' icdπ'→ 0› ‹j' icdπ'→ 0›
and ilj: ‹i < j›
and nret: ‹π i ≠ return›
shows ‹i' < j'›
-
have g0: ‹0 < i› ‹0 < j› ‹0 < i'› ‹0 < j'›using not_cd[unfolded is_icdi_def is_cdi_def] by auto
have ‹(π « 1) (i - 1) = (π' « 1) (i' - 1)› ‹(π « 1) (j - 1) = (π' « 1) (j' - 1)› using πi πj g0 by auto
moreover
have ‹∀ k. ¬ (j - 1) cdπ«1→ k› ‹∀ k. ¬ (i' - 1) cdπ'«1→ k›
by (metis icd_no_cd_path_shift not_cd(2)) (metis icd_no_cd_path_shift not_cd(3))
moreover
have ‹is_path (π«1)› ‹is_path (π'«1)› using pathπ pathπ' path_path_shift by blast+
moreover
have ‹(π«1) (i - 1) ≠ return› using g0 nret by auto
moreover
have ‹i - 1 < j - 1› using g0 ilj by auto
ultimately have ‹i' - 1 < j' - 1› using claim'' by blast
thus ‹i'<j'› by auto
other_claim: assumes path: ‹is_path π› and eq: ‹π i = π j› and ‹π i ≠ return›
icd: ‹i icdπ→ 0› and ‹j icdπ→ 0› shows ‹i = j› proof (rule ccontr,cases)
assume ‹i < j› thus ‹False› using assms claim' by blast
assume ‹¬ i < j› ‹i ≠ j›
hence ‹j < i› by auto
thus ‹False› using assms claim' by (metis less_not_refl)
cd_trans0: assumes ‹j cdπ→ 0› and ‹k cdπ→j› shows ‹k cdπ→ 0› proof (rule ccontr)
have path: ‹is_path π› and ij: ‹0 < j› and jk: ‹j < k›
and nret: ‹π j ≠ return› ‹π k ≠ return›
and noipdi: ‹∀ l ∈ {0..j}. π l ≠ ipd (π 0)›
and noipdj: ‹∀ l ∈ {j..k}. π l ≠ ipd (π j)›
using assms unfolding is_cdi_def by auto
assume ‹¬ k cdπ→ 0›
hence ‹∃l ∈ {0..k}. π l = ipd (π 0)› unfolding is_cdi_def using path ij jk nret by force
then obtain l where ‹l ∈ {0..k}› and l: ‹π l = ipd (π 0)› by auto
hence jl: ‹j<l\› and lk: ‹l≤k› using noipdi ij by auto
have pdj: ‹ipd (π 0) pd→ π j› proof (rule ccontr)
have ‹π j ∈ nodes› using path by (metis path_nodes)
moreover
assume ‹¬ ipd (π 0) pd→ π j›
ultimately
obtain π' n where *: ‹is_path π'› ‹π' 0 = π j› ‹π' n = return› ‹∀ k≤n. π' k ≠ ipd(π 0)› using no_pd_path by metis
hence path': ‹is_path (π @ π')› by (metis path path_cons)
moreover
have ‹∀ k ≤ j + n. (π@ π') k ≠ ipd (π 0)› using noipdi *(4) by auto
moreover
have ‹(π@ π') 0 = π 0› by auto
moreover
have ‹(π@ π') (j + n) = return› using *(2,3) by auto
ultimately
have ‹¬ ipd (π 0) pd→ π 0› unfolding is_pd_def by metis
thus ‹False› by (metis is_ipd_def ij ipd_is_ipd nret(1) path path_nodes term_path_stable less_imp_le)
qed
hence ‹(π«j) (l-j) pd→ (π«j) 0› using jl l by auto
moreover
have ‹is_path (π«j)› by (metis path path_path_shift)
moreover
have ‹π l ≠ return› by (metis lk nret(2) path term_path_stable)
hence ‹(π«j) (l-j) ≠ return› using jl by auto
moreover
have ‹π j ≠ ipd (π 0)› using noipdi by force
hence ‹(π«j) (l-j) ≠ (π«j) 0› using jl l by auto
ultimately
obtain k' where ‹k' ≤ l-j› and ‹(π«j) k' = ipd ((π«j) 0)› using path_pd_ipd0' by blast
hence ‹j + k' ∈ {j..k}› ‹π (j+k') = ipd (π j)› using jl lk by auto
thus ‹False› using noipdj by auto
cd_trans: assumes ‹j cdπ→ i› and ‹k cdπ→j› shows ‹k cdπ→ i› proof -
have path: ‹is_path π› using assms is_cdi_def by auto
have ij: ‹i<j\› using assms is_cdi_def by auto
let ‹?π› = ‹π«i›
have ‹j-i cdπ→ 0› using assms(1) cd_path_shift0 path by auto
moreover
have ‹k-i cdπ→j-i› by (metis assms(2) cd_path_shift is_cdi_def ij less_imp_le_nat)
ultimately
have ‹k-i cdπ→ 0› using cd_trans0 by auto
thus ‹k cdπ→ i› using path cd_path_shift0 by auto
excd_impl_exicd: assumes ‹∃ k. i cdπ→k› shows ‹∃ k. i icdπ→k›
assms proof(induction ‹i› arbitrary: ‹π› rule: less_induct)
case (less i)
then obtain k where k: ‹i cdπ→k› by auto
hence ip: ‹is_path π› unfolding is_cdi_def by auto
show ‹?case› proof (cases)
assume *: ‹∀ m ∈ {k<..<i}. ¬ i cdπ→ m›
hence ‹i icdπ→k› using k ip unfolding is_icdi_def by auto
thus ‹?case› by auto
next
assume ‹¬ (∀ m ∈ {k<..<i}. ¬ i cdπ→ m)›
then obtain m where m: ‹m ∈ {k<..<i}› ‹i cdπ→ m› by blast
hence ‹i - m cdπ«m→ 0› by (metis cd_path_shift0 is_cdi_def)
moreover
have ‹i - m < i› using m by auto
ultimately
obtain k' where k': ‹i - m icdπ«m→ k'› using less(1) by blast
hence ‹i icdπ→ k' + m› using ip
by (metis add.commute add_diff_cancel_right' icd_path_shift le_add1)
thus ‹?case› by auto
qed
cd_split: assumes ‹i cdπ→ k› and ‹¬ i icdπ→ k› obtains m where ‹i icdπ→ m› and ‹m cdπ→ k›
-
have ki: ‹k < i› using assms is_cdi_def by auto
obtain m where m: ‹i icdπ→ m› using assms(1) by (metis excd_impl_exicd)
hence ‹k ≤ m› unfolding is_icdi_def using ki assms(1) by force
hence km: ‹k < m›using m assms(2) by (metis le_eq_less_or_eq)
moreover have ‹π m ≠ return› using m unfolding is_icdi_def is_cdi_def by (simp, metis term_path_stable less_imp_le)
moreover have ‹m<i\› using m unfolding is_cdi_def is_icdi_def by auto
ultimately
have ‹m cdπ→ k› using assms(1) unfolding is_cdi_def by auto
with m that show ‹thesis› by auto
cd_induct[consumes 1, case_names base IS]: assumes prem: ‹i cdπ→ k› and base: ‹∧ i. i icdπ→k ==> P i›
IH: ‹∧ k' i'. k' cdπ→ k ==> P k' ==> i' icdπ→ k' ==> P i'› shows ‹P i›
prem IH proof (induction ‹i› rule: less_induct,cases)
case (less i)
assume ‹i icdπ→ k›
thus ‹P i› using base by simp
case (less i')
assume ‹¬ i' icdπ→ k›
then obtain k' where k': ‹ i' icdπ→ k'› ‹k' cdπ→ k› using less cd_split by blast
hence icdk: ‹i' cdπ→ k'› using is_icdi_def by auto
note ih=less(3)[OF k'(2) _ k'(1)]
have ki: ‹k' < i'› using k' is_icdi_def is_cdi_def by auto
have ‹P k'› using less(1)[OF ki k'(2) ] less(3) by auto
thus ‹P i'› using ih by simp
cdi_prefix: ‹n cdπ→ m ==> m < n' ==> n' ≤ n ==> n' cdπ→ m› unfolding is_cdi_def
by (simp, metis term_path_stable)
cr_wn': assumes 1: ‹n cdπ→ m› and nc: ‹¬ m' cdπ→ m› and 3: ‹m < m'› shows ‹n < m'›
(rule ccontr)
assume ‹¬ n < m'›
hence ‹m' ≤ n› by simp
hence ‹m' cdπ→ m› by (metis 1 3 cdi_prefix)
thus ‹False› using nc by simp
cr_wn'': assumes ‹i cdπ→ m› and ‹j cdπ→ n› and ‹¬ m cdπ→ n› and ‹i ≤ j› shows ‹m ≤ n› proof (rule ccontr)
assume ‹¬m≤n›
hence nm: ‹n < m› by auto
moreover
have ‹m<j\› using assms(1) assms(4) unfolding is_cdi_def by auto
ultimately
have ‹m cdπ→ n› using assms(2) cdi_prefix by auto
thus ‹False› using assms(3) by auto
ret_no_cd: assumes ‹π n = return› shows ‹¬ n cdπ→ k› by (metis assms is_cdi_def)
ipd_not_self: assumes ‹x ∈ nodes› ‹x≠ return› shows ‹x ≠ ipd x› by (metis is_ipd_def assms ipd_is_ipd)
icd_cs: assumes ‹l icdπ→k› shows ‹csπ l = csπ k @ [π l]›
-
from assms have ‹k = (THE k. l icdπ→ k)› by (metis icd_is_the_icd)
with assms show ‹?thesis› by auto
cd_not_pd: assumes ‹l cdπ→ k› ‹π l ≠ π k› shows ‹¬ π l pd→ π k› proof
assume pd: ‹π l pd→ π k›
have nret: ‹π k ≠ return› by (metis assms(1) pd pd_ret_is_ret ret_no_cd)
have kl: ‹k < l› by (metis is_cdi_def assms(1))
have path: ‹is_path π› by (metis is_cdi_def assms(1))
from path_pd_ipd[OF path nret assms(2) pd kl]
obtain n where ‹k < n› ‹n ≤ l› ‹π n = ipd (π k)› .
thus ‹False› using assms(1) unfolding is_cdi_def by auto
cd_ipd_is_cd: assumes ‹k<m\› ‹π m = ipd (π k)› ‹∀ n ∈ {k..<m}. π n ≠ ipd (π k)› and mcdj: ‹m cdπ→ j› shows ‹k cdπ→ j› proof cases
assume ‹j < k› thus ‹k cdπ→ j› by (metis mcdj assms(1) cdi_prefix less_imp_le_nat)
assume ‹¬ j < k›
hence kj: ‹k ≤ j› by simp
have ‹k < j› 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 ‹j < m› using mcdj is_cdi_def by auto
hence ‹∀ n ∈ {k..j}. π n ≠ ipd(π k)› using assms(3) by force
ultimately
have ‹j cdπ→ k› by (metis mcdj is_cdi_def term_path_stable less_imp_le)
hence ‹m cdπ→ k› by (metis mcdj cd_trans)
hence ‹False› 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 ‹?thesis› by simp
ipd_pd_cd0: assumes lcd: ‹n cdπ→ 0› shows ‹ipd (π 0) pd→ (π n)›
-
obtain k l where π0: ‹π 0 = k› and πn: ‹π n = l› and cdi: ‹n cdπ→ 0› using lcd unfolding is_cdi_def by blast
have nret: ‹k ≠ return› by (metis is_cdi_def π0 cdi term_path_stable less_imp_le)
have path: ‹is_path π› and ipd: ‹∀ i≤n. π i ≠ ipd k› using cdi unfolding is_cdi_def π0 by auto
{
fix π' n'
assume path': ‹is_path π'›
and π'0: ‹π' 0 = l›
and ret: ‹π' n' = return›
have ‹is_path (π @ π')› using path path' πn π'0 by (metis path_cons)
moreover
have ‹(π @ π') (n+n') = return› using ret πn π'0 by auto
moreover
have ‹(π @ π') 0 = k› using π0 by auto
moreover
have ‹ipd k pd→ k› by (metis is_ipd_def path π0 ipd_is_ipd nret path_nodes)
ultimately
obtain k' where k': ‹k' ≤ n+n'› ‹(π @ π') k' = ipd k› by (metis pd_intro)
have ‹¬ k'≤ n› proof
assume ‹k' ≤ n›
hence ‹(π @ π') k' = π k'› by auto
thus ‹False› using k'(2) ipd by (metis ‹k' ≤ n›)
qed
hence ‹(π @ π') k' = π' (k' - n)› by auto
moreover
have ‹(k' - n) ≤ n'› using k' by simp
ultimately
have ‹∃ k'≤n'. π' k' = ipd k› unfolding k' by auto
}
moreover
have ‹l ∈ nodes› by (metis πn path path_nodes)
ultimately show ‹ipd (π 0) pd→ (π n)› unfolding is_pd_def by (simp add: π0 πn)
ipd_pd_cd: assumes lcd: ‹l cdπ→ k› shows ‹ipd (π k) pd→ (π l)›
-
have ‹l-k cdπ«k→0› using lcd cd_path_shift0 is_cdi_def by blast
moreover
note ipd_pd_cd0[OF this]
moreover
have ‹(π « k) 0 = π k› by auto
moreover
have ‹k < l› using lcd unfolding is_cdi_def by simp
then have ‹(π « k) (l - k) = π l› by simp
ultimately show ‹?thesis› by simp
cd_is_cd_ipd: assumes km: ‹k<m\› and ipd: ‹π m = ipd (π k)› ‹∀ n ∈ {k..<m}. π n ≠ ipd (π k)› and cdj: ‹k cdπ→ j› and nipdj: ‹ipd (π j) ≠ π m› shows ‹m cdπ→ j› proof -
have path: ‹is_path π›
and jk: ‹j < k›
and nretj: ‹π k ≠ return›
and nipd: ‹∀ l ∈ {j..k}. π l ≠ ipd (π j)› using cdj is_cdi_def by auto
have pd: ‹ipd (π j) pd→ π m› 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: ‹π m ≠ return› by (metis nipdj pd pd_ret_is_ret)
have jm: ‹j < m› using jk km by simp
show ‹m cdπ→ j› proof (rule ccontr)
assume ncdj: ‹¬ m cdπ→ j›
hence ‹∃ l ∈ {j..m}. π l = ipd (π j)› unfolding is_cdi_def by (metis jm nretm path)
then obtain l
where jl: ‹j ≤ l› and ‹l ≤ m›
and lipd: ‹π l = ipd (π j)› by force
hence lm: ‹l < m› using nipdj by (metis le_eq_less_or_eq)
have npd: ‹¬ ipd (π k) pd→ π l› by (metis ipd(1) lipd nipdj pd pd_antisym)
have nd: ‹π l ∈ nodes› using path path_nodes by simp
from no_pd_path[OF nd npd]
obtain π' n where path': ‹is_path π'› and π'0: ‹π' 0 = π l› and π'n: ‹π' n = return› and nipd: ‹∀ ka≤n. π' ka ≠ ipd (π k)› .
let ‹?π› = ‹(π@ π') « k›
have path'': ‹is_path ?π› by (metis π'0 path path' path_cons path_path_shift)
moreover
have kl: ‹k < l› using lipd cdj jl unfolding is_cdi_def by fastforce
have ‹?π 0 = π k› using kl by auto
moreover
have ‹?π (l + n - k) = return› using π'n π'0 kl by auto
moreover
have ‹ipd (π k) pd→ π k› by (metis is_ipd_def ipd_is_ipd nretj path path_nodes)
ultimately
obtain l' where l': ‹l' ≤ (l + n - k)› ‹?π l' = ipd (π k)› unfolding is_pd_def by blast
show ‹False› proof (cases )
assume *: ‹k + l' ≤ l›
hence ‹π (k + l') = ipd (π k)› using l' by auto
moreover
have ‹k + l' < m› by (metis "*" dual_order.strict_trans2 lm)
ultimately
show ‹False› using ipd(2) by simp
next
assume ‹¬ k + l' ≤ l›
hence ‹π' (k + l' - l) = ipd (π k)› using l' by auto
moreover
have ‹k + l' - l ≤ n› using l' kl by linarith
ultimately
show ‹False› using nipd by auto
qed
qed
ipd_icd_greatest_cd_not_ipd: assumes ipd: ‹π m = ipd (π k)› ‹∀ n ∈ {k..<m}. π n ≠ ipd (π k)›
km: ‹k < m› and icdj: ‹m icdπ→ j› shows ‹j = (GREATEST j. k cdπ→ j ∧ ipd (π j) ≠ π m)›
-
let ‹?j› = ‹GREATEST j. k cdπ→ j ∧ ipd (π j) ≠ π m›
have kcdj: ‹k cdπ→ j› using assms cd_ipd_is_cd is_icdi_def by blast
have nipd: ‹ipd (π j) ≠ π m› using icdj unfolding is_icdi_def is_cdi_def by auto
have bound: ‹∧ j. k cdπ→ j ∧ ipd (π j) ≠ π m ==> j ≤ k› unfolding is_cdi_def by simp
have exists: ‹k cdπ→ j ∧ ipd (π j) ≠ π m› (is ‹?P j›) using kcdj nipd by auto
note GreatestI_nat[of ‹?P› _ ‹k›, OF exists] Greatest_le_nat[of ‹?P› ‹j› ‹k›, OF exists]
hence kcdj': ‹k cdπ→ ?j› and ipd': ‹ipd (π ?j) ≠ π m› and jj: ‹j ≤ ?j› using bound by auto
hence mcdj': ‹m cdπ→ ?j› using ipd km cd_is_cd_ipd by auto
show ‹j = ?j› proof (rule ccontr)
assume ‹j ≠ ?j›
hence jlj: ‹j < ?j› using jj by simp
moreover
have ‹?j < m› using kcdj' km unfolding is_cdi_def by auto
ultimately
show ‹False› using icdj mcdj' unfolding is_icdi_def by auto
qed
cd_impl_icd_cd: assumes ‹i cdπ→ l› and ‹i icdπ→ k› and ‹¬ i icdπ→ l› shows ‹k cdπ→ l›
using assms cd_split icd_uniq by metis
cdi_is_cd_icdi: assumes ‹k icdπ→ j› shows ‹k cdπ→ i ⟷ j cdπ→ i ∨ i = j›
by (metis assms cd_impl_icd_cd cd_trans icd_imp_cd icd_uniq)
same_ipd_stable: assumes ‹k cdπ→ i› ‹k cdπ→ j› ‹i<j\› ‹ipd (π i) = ipd (π k)› shows ‹ipd (π j) = ipd (π k)›
-
have jcdi: ‹j cdπ→ i› by (metis is_cdi_def assms(1,2,3) cr_wn' le_antisym less_imp_le_nat)
have 1: ‹ipd (π j) pd→ π k › by (metis assms(2) ipd_pd_cd)
have 2: ‹ipd (π k) pd→ π j › by (metis assms(4) ipd_pd_cd jcdi)
have 3: ‹ipd (π k) pd→ (ipd (π j))› 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: ‹ipd (π j) pd→ (ipd (π k))› by (metis 1 2 IFC_def.is_ipd_def assms(2) cd_not_pd ipd_is_ipd jcdi pd_node2 ret_no_cd)
show ‹?thesis› using 3 4 pd_antisym by simp
icd_pd_intermediate': assumes icd: ‹i icdπ→ k› and j: ‹k < j› ‹j < i› shows ‹π i pd→ (π j)›
j proof (induction ‹i - j› arbitrary: ‹j› rule: less_induct)
case (less j)
have ‹¬ i cdπ→ j› using less.prems icd unfolding is_icdi_def by force
moreover
have ‹is_path π› using icd by (metis is_icdi_def)
moreover
have ‹π i ≠ return› using icd by (metis is_icdi_def ret_no_cd)
ultimately
have ‹∃ l. j ≤ l ∧ l ≤ i ∧ π l = ipd (π j)› unfolding is_cdi_def using less.prems by auto
then obtain l where l: ‹j ≤ l› ‹l ≤ i› ‹π l = ipd (π j)› by blast
hence lpd: ‹π l pd→ (π j)› by (metis is_ipd_def ‹π i ≠ return› ‹is_path π› ipd_is_ipd path_nodes term_path_stable)
show ‹?case› proof (cases)
assume ‹l = i›
thus ‹?case› using lpd by auto
next
assume ‹l ≠ i›
hence ‹l < i› using l by simp
moreover
have ‹j ≠ l› using l by (metis is_ipd_def ‹π i ≠ return› ‹is_path π› ipd_is_ipd path_nodes term_path_stable)
hence ‹j < l› using l by simp
moreover
hence ‹i - l < i - j› by (metis diff_less_mono2 less.prems(2))
moreover
have ‹k < l› by (metis l(1) less.prems(1) linorder_neqE_nat not_le order.strict_trans)
ultimately
have ‹π i pd→ (π l)› using less.hyps by auto
thus ‹?case› using lpd by (metis pd_trans)
qed
icd_pd_intermediate: assumes icd: ‹i icdπ→ k› and j: ‹k < j› ‹j ≤ i› shows ‹π i pd→ (π j)›
assms icd_pd_intermediate'[OF assms(1,2)] apply (cases ‹j < i›,metis) by (metis is_icdi_def le_neq_trans path_nodes pd_refl)
no_icd_pd: assumes path: ‹is_path π› and noicd: ‹∀ l≥n. ¬ k icdπ→ l› and nk: ‹n ≤ k› shows ‹π k pd→ π n›
cases
assume ‹π k = return› thus ‹?thesis› by (metis path path_nodes return_pd)
assume nret: ‹π k ≠ return›
have nocd: ‹∧ l. n≤l ==> ¬ k cdπ→ l› proof
fix l assume kcd: ‹k cdπ→ l› and nl: ‹n ≤ l›
hence ‹(k - n) cdπ«n→ (l - n)› using cd_path_shift[OF nl path] by simp
hence ‹∃ l. (k - n) icdπ«n→ l› using excd_impl_exicd by blast
then obtain l' where "k - n icdπ « n→ l'" ..
hence ‹k icdπ→ (l' + n)› using icd_path_shift[of ‹n› ‹l' + n› ‹π› ‹k›] path by auto
thus ‹False› using noicd by auto
qed
hence ‹∧l. n ≤ l ==> l<k ==> ∃ j ∈ {l..k}. π j = ipd (π l)› using path nret unfolding is_cdi_def by auto
thus ‹?thesis› using nk proof (induction ‹k - n› arbitrary: ‹n› rule: less_induct,cases)
case (less n)
assume ‹n = k›
thus ‹?case› using pd_refl path path_nodes by auto
next
case (less n)
assume ‹n ≠ k›
hence nk: ‹n < k› using less(3) by auto
with less(2) obtain j where jnk: ‹j ∈ {n..k}› and ipdj: ‹π j = ipd (π n)› by blast
have nretn: ‹π n ≠ return› using nk nret term_path_stable path by auto
with ipd_is_ipd path path_nodes is_ipd_def ipdj
have jpdn: ‹π j pd→ π n› by auto
show ‹?case› proof cases
assume ‹j = k› thus ‹?case› using jpdn by simp
next
assume ‹j ≠ k›
hence jk: ‹j < k› using jnk by auto
have ‹j ≠ n› using ipdj by (metis ipd_not_self nretn path path_nodes)
hence nj: ‹n < j› using jnk by auto
have *: ‹k - j < k - n› using jk nj by auto
with less(1)[OF *] less(2) jk nj
have ‹π k pd→ π j› by auto
thus ‹?thesis› using jpdn pd_trans by metis
qed
qed
first_pd_no_cd: assumes path: ‹is_path π› and pd: ‹π n pd→ π 0› and first: ‹∀ l < n. π l ≠ π n› shows ‹∀ l. ¬ n cdπ→ l›
(rule ccontr, goal_cases)
case 1
then obtain l where ncdl: ‹n cdπ→ l› by blast
hence ln: ‹l < n› using is_cdi_def by auto
have ‹¬ π n pd→ π l› using ncdl cd_not_pd by (metis ln first)
then obtain π' n' where path': ‹is_path π'› and π0: ‹π' 0 = π l› and πn: ‹π' n' = return› and notπn: ‹∀ j≤ n'. π' j ≠ π n› unfolding is_pd_def using path path_nodes by auto
let ‹?π› = ‹π@ π'›
have ‹is_path ?π› by (metis π0 path path' path_cons)
moreover
have ‹?π 0 = π 0› by auto
moreover
have ‹?π (n' + l) = return› using π0 πn by auto
ultimately
obtain j where j: ‹j ≤ n' + l› and jn: ‹?π j = π n› using pd unfolding is_pd_def by blast
show ‹False› proof cases
assume ‹j ≤ l› thus ‹False› using jn first ln by auto
next
assume ‹¬ j ≤ l› thus ‹False› using j jn notπn by auto
qed
first_pd_no_icd: assumes path: ‹is_path π› and pd: ‹π n pd→ π 0› and first: ‹∀ l < n. π l ≠ π n› shows ‹∀ l. ¬ n icdπ→ l›
by (metis first first_pd_no_cd icd_imp_cd path pd)
path_nret_ex_nipd: assumes ‹is_path π› ‹∀ i. π i ≠ return› shows ‹∀ i. (∃ j≥i. (∀ k>j. π k ≠ ipd (π j)))› proof(rule, rule ccontr)
fix i
assume ‹¬ (∃j≥i. ∀ k>j. π k ≠ ipd (π j))›
hence *: ‹∀ j≥i. (∃k>j. π k = ipd (π j))› by blast
have ‹∀ j. (∃k>j. (π«i) k = ipd ((π«i) j))› proof
fix j
have ‹i + j ≥ i› by auto
then obtain k where k: ‹k>i+j› ‹π k = ipd (π (i+j))› using * by blast
hence ‹(π«i) (k - i) = ipd ((π«i) j)› by auto
moreover
have ‹k - i > j› using k by auto
ultimately
show ‹∃k>j. (π«i) k = ipd ((π«i) j)› by auto
qed
moreover
have ‹is_path (π«i)› using assms(1) path_path_shift by simp
ultimately
obtain k where ‹(π«i) k = return› using all_ipd_imp_ret by blast
thus ‹False› using assms(2) by auto
path_nret_ex_all_cd: assumes ‹is_path π› ‹∀ i. π i ≠ return› shows ‹∀ i. (∃ j≥i. (∀ k>j. k cdπ→ j))›
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)
path_nret_inf_all_cd: assumes ‹is_path π› ‹∀ i. π i ≠ return› shows ‹¬ finite {j. ∀ k>j. k cdπ→ j}›
unbounded_nat_set_infinite path_nret_ex_all_cd[OF assms] by auto
path_nret_inf_icd_seq: assumes path: ‹is_path π› and nret: ‹∀ i. π i ≠ return›
f where ‹∀ i. f (Suc i) icdπ→ f i› ‹range f = {i. ∀ j>i. j cdπ→ i}› ‹¬ (∃i. f 0 cdπ→ i)›
-
note path_nret_inf_all_cd[OF assms]
then obtain f where ran: ‹range f = {j. ∀ k>j. k cdπ→ j}› and asc: ‹∀ i. f i < f (Suc i)› using infinite_ascending by blast
have mono: ‹∀ i j. i < j ⟶ f i < f j› using asc by (metis lift_Suc_mono_less)
{
fix i
have cd: ‹f (Suc i) cdπ→ f i› using ran asc by auto
have ‹f (Suc i) icdπ→ f i› proof (rule ccontr)
assume ‹¬ f (Suc i) icdπ→ f i›
then obtain m where im: ‹f i < m› and mi: ‹ m < f (Suc i)› and cdm: ‹f (Suc i) cdπ→ m› unfolding is_icdi_def using assms(1) cd by auto
have ‹∀ k>m. k cdπ→m› proof (rule,rule,cases)
fix k assume ‹f (Suc i) < k›
hence ‹k cdπ→ f (Suc i)› using ran by auto
thus ‹k cdπ→ m› using cdm cd_trans by metis
next
fix k assume mk: ‹m < k› and ‹¬ f (Suc i) < k›
hence ik: ‹k ≤ f (Suc i)› by simp
thus ‹k cdπ→ m› using cdm by (metis cdi_prefix mk)
qed
hence ‹m ∈ range f› using ran by blast
then obtain j where m: ‹m = f j› by blast
show ‹False› using im mi mono unfolding m by (metis Suc_lessI le_less not_le)
qed
}
moreover
{
fix m
assume cdm: ‹f 0 cdπ→ m›
have ‹∀ k>m. k cdπ→m› proof (rule,rule,cases)
fix k assume ‹f 0 < k›
hence ‹k cdπ→ f 0› using ran by auto
thus ‹k cdπ→ m› using cdm cd_trans by metis
next
fix k assume mk: ‹m < k› and ‹¬ f 0 < k›
hence ik: ‹k ≤ f 0› by simp
thus ‹k cdπ→ m› using cdm by (metis cdi_prefix mk)
qed
hence ‹m ∈ range f› using ran by blast
then obtain j where m: ‹m = f j› by blast
hence fj0: ‹f j < f 0› using cdm m is_cdi_def by auto
hence ‹0 < j› by (metis less_irrefl neq0_conv)
hence ‹False› using fj0 mono by fastforce
}
ultimately show ‹thesis› using that ran by blast
cdi_iff_no_strict_pd: ‹i cdπ→ k ⟷ is_path π ∧ k < i ∧ π i ≠ return ∧ (∀ j ∈ {k..i}. ¬ (π k, π j) ∈ pdt)›
assume cd:‹i cdπ→ k›
have 1: ‹is_path π ∧ k < i ∧ π i ≠ return› using cd unfolding is_cdi_def by auto
have 2: ‹∀ j ∈ {k..i}. ¬ (π k, π j) ∈ pdt› proof (rule ccontr)
assume ‹ ¬ (∀j∈{k..i}. (π k, π j) ∉ pdt)›
then obtain j where ‹j ∈ {k..i}› and ‹(π k, π j) ∈ pdt› by auto
hence ‹π j ≠ π k› and ‹π j pd→ π k› unfolding pdt_def by auto
thus ‹False› using path_pd_ipd by (metis ‹j ∈ {k..i}› atLeastAtMost_iff cd cd_not_pd cdi_prefix le_eq_less_or_eq)
qed
show ‹is_path π ∧ k < i ∧ π i ≠ return ∧ (∀ j ∈ {k..i}. ¬ (π k, π j) ∈ pdt)› using 1 2 by simp
assume ‹is_path π ∧ k < i ∧ π i ≠ return ∧ (∀ j ∈ {k..i}. ¬ (π k, π j) ∈ pdt)›
thus ‹i cdπ→ k› by (metis ipd_in_pdt term_path_stable less_or_eq_imp_le not_cd_impl_ipd path_nodes)
‹Facts about Control Slices›
last_cs: ‹last (csπ i) = π i› by auto
cs_not_nil: ‹csπ n ≠ []› by (auto)
cs_return: assumes ‹π n = return› shows ‹csπ n = [π n]› by (metis assms cs.elims icd_imp_cd ret_no_cd)
cs_0[simp]: ‹csπ 0 = [π 0]› using is_icdi_def is_cdi_def by auto
cs_inj: assumes ‹is_path π› ‹π n ≠ return› ‹csπ n = csπ n'› shows ‹n = n'›
assms proof (induction ‹csπ n› arbitrary: ‹π› ‹n› ‹n'› rule:rev_induct)
case Nil hence ‹False› using cs_not_nil by metis thus ‹?case› by simp
case (snoc x xs π n n') show ‹?case› proof (cases ‹xs›)
case Nil
hence *: ‹¬ (∃ k. n icdπ→k)› using snoc(2) cs_not_nil
by (auto,metis append1_eq_conv append_Nil cs_not_nil)
moreover
have ‹[x] = csπ n'› using Nil snoc by auto
hence **: ‹¬ (∃ k. n' icdπ→k)› using cs_not_nil
by (auto,metis append1_eq_conv append_Nil cs_not_nil)
ultimately
have ‹∀ k. ¬ n cdπ→ k› ‹∀ k. ¬ n' cdπ→ k› using excd_impl_exicd by auto blast+
moreover
hence ‹π n = π n'› using snoc(5,2) by auto (metis * ** list.inject)
ultimately
show ‹n = n'› using other_claim' snoc by blast
case (Cons y ys)
hence *: ‹∃ k. n icdπ→k› using snoc(2) by auto (metis append_is_Nil_conv list.distinct(1) list.inject)
then obtain k where k: ‹n icdπ→k› by auto
have ‹k = (THE k . n icdπ→ k)› using k by (metis icd_is_the_icd)
hence xsk: ‹xs = csπ k› using * k snoc(2) unfolding cs.simps[of ‹π› ‹n›] by auto
have **: ‹∃ k. n' icdπ→k› using snoc(2)[unfolded snoc(5)] by auto (metis Cons append1_eq_conv append_Nil list.distinct(1))
then obtain k' where k': ‹n' icdπ→ k'› by auto
hence ‹k' = (THE k . n' icdπ→ k)› using k' by (metis icd_is_the_icd)
hence xsk': ‹xs = csπ k'› using ** k' snoc(5,2) unfolding cs.simps[of ‹π› ‹n'›] by auto
hence ‹csπ k = csπ k'› using xsk by simp
moreover
have kn: ‹k < n› using k by (metis is_icdi_def is_cdi_def)
hence ‹π k ≠ return› using snoc by (metis term_path_stable less_imp_le)
ultimately
have kk'[simp]: ‹k' = k› using snoc(1) xsk snoc(3) by metis
have nk0: ‹n - k icdπ«k→ 0› ‹n' - k icdπ«k→ 0› using k k' icd_path_shift0 snoc(3) by auto
moreover
have nkr: ‹(π«k)(n-k) ≠ return› using snoc(4) kn by auto
moreover
have ‹is_path (π«k)› by (metis path_path_shift snoc.prems(1))
moreover
have kn': ‹k < n'› using k' kk' by (metis is_icdi_def is_cdi_def)
have ‹π n = π n'› using snoc(5) * ** by auto
hence ‹(π«k)(n-k) = (π«k)(n'-k)› using kn kn' by auto
ultimately
have ‹n - k = n' - k› using other_claim by auto
thus ‹n = n'› using kn kn' by auto
cs_cases: fixes π i
(base) ‹csπ i = [π i]› and ‹∀ k. ¬ i cdπ→ k› |
depend) k where ‹csπ i = (csπ k)@[π i]› and ‹i icdπ→ k›
cases
assume *: ‹∃ k. i icdπ→ k›
then obtain k where k: ‹i icdπ→ k› ..
hence ‹k = (THE k. i icdπ→ k)› by (metis icd_is_the_icd)
hence ‹csπ i = (csπ k)@[π i]› using * by auto
with k that show ‹thesis› by simp
assume *: ‹¬ (∃ k. i icdπ→ k)›
hence ‹∀ k. ¬ i cdπ→ k› by (metis excd_impl_exicd)
moreover
have ‹csπ i = [π i]› using * by auto
ultimately
show ‹thesis› using that by simp
cs_length_one: assumes ‹length (csπ i) = 1› shows ‹csπ i = [π i]› and ‹∀ k. ¬ i cdπ→ k›
apply (cases ‹i› ‹π› rule: cs_cases)
using assms cs_not_nil
apply auto
apply (cases ‹i› ‹π› rule: cs_cases)
using assms cs_not_nil
by auto
cs_length_g_one: assumes ‹length (csπ i) ≠ 1› obtains k where ‹csπ i = (csπ k)@[π i]› and ‹i icdπ→ k›
apply (cases ‹i› ‹π› rule: cs_cases)
using assms cs_not_nil by auto
claim: assumes path: ‹is_path π› ‹is_path π'› and ii: ‹csπ i = csπ' i'› and jj: ‹csπ j = csπ' j'›
bl: ‹butlast (csπ i) = butlast (csπ j)› and nret: ‹π i ≠ return› and ilj: ‹i < j›
‹i' < j'›
(cases )
assume *: ‹length (csπ i) = 1›
hence **: ‹length (csπ i) = 1› ‹length (csπ j) = 1› ‹length (csπ' i') = 1› ‹length (csπ' j') = 1›
apply metis
apply (metis "*" bl butlast.simps(2) butlast_snoc cs_length_g_one cs_length_one(1) cs_not_nil)
apply (metis "*" ii)
by (metis "*" bl butlast.simps(2) butlast_snoc cs_length_g_one cs_length_one(1) cs_not_nil jj)
then obtain ‹csπ i = [π i]› ‹csπ j = [π j]› ‹csπ' j' = [π' j']› ‹csπ' i'= [π' i']›
‹∀ k. ¬ j cdπ→ k› ‹∀ k. ¬ i' cdπ'→ k› ‹∀ k. ¬ j' cdπ'→ k›
by (metis cs_length_one ** )
moreover
hence ‹π i = π' i'› ‹π j = π' j'› using assms by auto
ultimately
show ‹i' < j'› using nret ilj path claim'' by blast
assume *: ‹length (csπ i) ≠ 1›
hence **: ‹length (csπ i) ≠ 1› ‹length (csπ j) ≠ 1› ‹length (csπ' i') ≠ 1› ‹length (csπ' j') ≠ 1›
apply metis
apply (metis "*" bl butlast.simps(2) butlast_snoc cs_length_g_one cs_length_one(1) cs_not_nil)
apply (metis "*" ii)
by (metis "*" bl butlast.simps(2) butlast_snoc cs_length_g_one cs_length_one(1) cs_not_nil jj)
obtain k l k' l' where ***:
‹csπ i = (csπ k)@[π i]› ‹csπ j = (csπ l)@[π j]› ‹csπ' i' = (csπ' k')@[π' i']› ‹csπ' j' = (csπ' l')@[π' j']› and
icds: ‹i icdπ→ k› ‹j icdπ→ l› ‹i' icdπ'→ k'› ‹j' icdπ'→ l'›
by (metis ** cs_length_g_one)
hence ‹csπ k = csπ l› ‹csπ' k' = csπ' l'› using assms by auto
moreover
have ‹π k ≠ return› ‹π' k' ≠ return› using nret
apply (metis is_icdi_def icds(1) is_cdi_def term_path_stable less_imp_le)
by (metis is_cdi_def is_icdi_def icds(3) term_path_stable less_imp_le)
ultimately
have lk[simp]: ‹l = k› ‹l' = k'› using path cs_inj by auto
let ‹?π› = ‹π « k›
let ‹?π'› = ‹π'«k'›
have ‹i-k icdπ→ 0› ‹j-k icdπ→ 0› ‹i'-k' icdπ'→ 0› ‹j'-k' icdπ'→ 0› using icd_path_shift0 path icds by auto
moreover
have ki: ‹k < i› using icds by (metis is_icdi_def is_cdi_def)
hence ‹i-k < j-k› by (metis diff_is_0_eq diff_less_mono ilj nat_le_linear order.strict_trans)
moreover
have πi: ‹π i = π' i'› ‹π j = π' j'› using assms *** by auto
have ‹k' < i'› ‹k' < j'› using icds unfolding lk by (metis is_cdi_def is_icdi_def)+
hence ‹?π (i-k) = ?π' (i'-k')› ‹?π (j-k) = ?π' (j'-k')› using πi ki ilj by auto
moreover
have ‹?π (i-k) ≠ return› using nret ki by auto
moreover
have ‹is_path ?π› ‹is_path ?π'› using path path_path_shift by auto
ultimately
have ‹i'-k' < j' - k'› using claim' by blast
thus ‹i' < j'› by (metis diff_is_0_eq diff_less_mono less_nat_zero_code linorder_neqE_nat nat_le_linear)
cs_split': assumes ‹csπ i = xs@[x,x']@ys› shows ‹∃ m. csπ m = xs@[x] ∧ i cdπ→ m›
assms proof (induction ‹ys› arbitrary: ‹i› rule:rev_induct )
case (snoc y ys)
hence ‹length (csπ i) ≠ 1› by auto
then obtain i' where ‹csπ i = (csπ i') @ [π i]› and *: ‹i icdπ→ i'› using cs_length_g_one[of ‹π› ‹i›] by metis
hence ‹csπ i' = xs@[x,x']@ys› using snoc(2) by (metis append1_eq_conv append_assoc)
then obtain m where **: ‹csπ m = xs @ [x]› and ‹i' cdπ→ m› using snoc(1) by blast
hence ‹i cdπ→ m› using * cd_trans by (metis is_icdi_def)
with ** show ‹?case› by blast
case Nil
hence ‹length (csπ i) ≠ 1› by auto
then obtain i' where a: ‹csπ i = (csπ i') @ [π i]› and *: ‹i icdπ→ i'› using cs_length_g_one[of ‹π› ‹i›] by metis
have ‹csπ i = (xs@[x])@[x']› using Nil by auto
hence ‹csπ i' = xs@[x]› using append1_eq_conv a by metis
thus ‹?case› using * unfolding is_icdi_def by blast
cs_split: assumes ‹csπ i = xs@[x]@ys@[π i]› shows ‹∃ m. csπ m = xs@[x] ∧ i cdπ→ m› proof -
obtain x' ys' where ‹ys@[π i] = [x']@ys'› by (metis append_Cons append_Nil neq_Nil_conv)
thus ‹?thesis› using cs_split'[of ‹π› ‹i› ‹xs› ‹x› ‹x'› ‹ys'›] assms by auto
cs_less_split: assumes ‹xs ≺ ys› obtains a as where ‹ys = xs@a#as›
using assms unfolding cs_less.simps apply auto
(metis Cons_nth_drop_Suc append_take_drop_id)
cs_select_is_cs: assumes ‹is_path π› ‹xs ≠ Nil› ‹xs ≺ csπ k› shows ‹csπ (π🍋xs) = xs› ‹k cdπ→ (π🍋xs)›proof -
obtain b bs where b: ‹csπ k = xs@b#bs› using assms cs_less_split by blast
obtain a as where a: ‹xs = as@[a]› using assms by (metis rev_exhaust)
have ‹csπ k = as@[a,b]@bs› using a b by auto
then obtain k' where csk: ‹csπ k' = xs› and is_cd: ‹k cdπ→ k'› using cs_split' a by blast
hence nret: ‹π k' ≠ return› by (metis is_cdi_def term_path_stable less_imp_le)
show a: ‹csπ (π🍋xs) = xs› unfolding cs_select_def using cs_inj[OF assms(1) nret] csk the_equality[of _ ‹k'›]
by (metis (mono_tags))
show ‹k cdπ→ (π🍋xs)› unfolding cs_select_def by (metis a assms(1) cs_inj cs_select_def csk is_cd nret)
cd_in_cs: assumes ‹n cdπ→ m› shows ‹∃ ns. csπ n = (csπ m) @ ns @[π n]›
assms proof (induction rule: cd_induct)
case (base n) thus ‹?case› by (metis append_Nil cs.simps icd_is_the_icd)
case (IS k n)
hence ‹csπ n = csπ k @ [π n]› by (metis cs.simps icd_is_the_icd)
thus ‹?case› using IS by force
butlast_cs_not_cd: assumes ‹butlast (csπ m) = butlast (csπ n)› shows ‹¬ m cdπ→n›
(metis append_Cons append_Nil append_assoc assms cd_in_cs cs_not_nil list.distinct(1) self_append_conv snoc_eq_iff_butlast)
wn_cs_butlast: assumes ‹butlast (csπ m) = butlast (csπ n)› ‹i cdπ→ m› ‹j cdπ→ n› ‹m<n\› shows ‹i<j\›
(rule ccontr)
assume ‹¬ i < j›
moreover
have ‹¬ n cdπ→ m› by (metis assms(1) butlast_cs_not_cd)
ultimately
have ‹n ≤ m› using assms(2,3) cr_wn'' by auto
thus ‹False› using assms(4) by auto
‹This is the central theorem making the control slice suitable for matching indices between executions.›
cs_order: assumes path: ‹is_path π› ‹is_path π'› and csi: ‹csπ i = csπ' i'›
csj: ‹csπ j = csπ' j'› and nret: ‹π i ≠ return› and ilj: ‹i < j›
‹i'<j'›
-
have ‹csπ i ≠ csπ j› using cs_inj[OF path(1) nret] ilj by blast
moreover
have ‹csπ i ≠ Nil› ‹csπ j ≠ Nil› by (metis cs_not_nil)+
ultimately show ‹?thesis› proof (cases rule: list_neq_prefix_cases)
case (diverge xs x x' ys ys')
note csx = ‹csπ i = xs @ [x] @ ys›
note csx' = ‹csπ j = xs @ [x'] @ ys'›
note xx = ‹x ≠ x'›
show ‹i' < j'› proof (cases ‹ys›)
assume ys: ‹ys = Nil›
show ‹?thesis› proof (cases ‹ys'›)
assume ys': ‹ys' = Nil›
have cs: ‹csπ i = xs @ [x]› ‹csπ j = xs @ [x']› by (metis append_Nil2 csx ys, metis append_Nil2 csx' ys')
hence bl: ‹butlast (csπ i) = butlast (csπ j)› by auto
show ‹i' < j'› using claim[OF path csi csj bl nret ilj] .
next
fix y' zs'
assume ys': ‹ys' = y'#zs'›
have cs: ‹csπ i = xs @ [x]› ‹csπ j = xs @ [x',y']@ zs'› by (metis append_Nil2 csx ys, metis append_Cons append_Nil csx' ys')
obtain n where n: ‹csπ n = xs@[x']› and jn: ‹j cdπ→ n› using cs cs_split' by blast
obtain n' where n': ‹csπ' n' = xs@[x']› and jn': ‹j' cdπ'→ n'› using cs cs_split' unfolding csj by blast
have csn : ‹csπ n = csπ' n'› and bl: ‹butlast (csπ i) = butlast (csπ n)› using n n' cs by auto
hence bl': ‹butlast (csπ' i') = butlast (csπ' n')› using csi by auto
have notcd: ‹¬ i cdπ→ n› by (metis butlast_cs_not_cd bl)
have nin: ‹i ≠ n› using cs n xx by auto
have iln: ‹i < n› apply (rule ccontr) using cr_wn'[OF jn notcd] nin ilj by auto
note claim[OF path csi csn bl nret iln]
hence ‹i' < n'› .
thus ‹i' < j'› using jn' unfolding is_cdi_def by auto
qed
next
fix y zs
assume ys: ‹ys = y#zs›
show ‹?thesis› proof (cases ‹ys'›)
assume ys' : ‹ys' = Nil›
have cs: ‹csπ i = xs @ [x,y]@zs› ‹csπ j = xs @ [x']› by (metis append_Cons append_Nil csx ys, metis append_Nil2 csx' ys')
obtain n where n: ‹csπ n = xs@[x]› and jn: ‹i cdπ→ n› using cs cs_split' by blast
obtain n' where n': ‹csπ' n' = xs@[x]› and jn': ‹i' cdπ'→ n'› using cs cs_split' unfolding csi by blast
have csn : ‹csπ n = csπ' n'› and bl: ‹butlast (csπ n) = butlast (csπ j)› using n n' cs by auto
hence bl': ‹butlast (csπ' j') = butlast (csπ' n')› using csj by auto
have notcd: ‹¬ j' cdπ'→ n'› by (metis butlast_cs_not_cd bl')
have nin: ‹n < i› using jn unfolding is_cdi_def by auto
have nlj: ‹n < j› using nin ilj by auto
note claim[OF path csn csj bl _ nlj]
hence nj': ‹n' < j'› using term_path_stable[OF path(1) _] less_imp_le nin nret by auto
show ‹i' < j'› apply(rule ccontr) using cdi_prefix[OF jn' nj'] notcd by auto
next
fix y' zs'
assume ys' : ‹ys' = y'#zs'›
have cs: ‹csπ i = xs@[x,y]@zs› ‹csπ j = xs@[x',y']@zs'› by (metis append_Cons append_Nil csx ys,metis append_Cons append_Nil csx' ys')
have neq: ‹csπ i ≠ csπ j› using cs_inj path nret ilj by blast
obtain m where m: ‹csπ m = xs@[x]› and im: ‹i cdπ→ m› using cs cs_split' by blast
obtain n where n: ‹csπ n = xs@[x']› and jn: ‹j cdπ→ n› using cs cs_split' by blast
obtain m' where m': ‹csπ' m' = xs@[x]› and im': ‹i' cdπ'→ m'› using cs cs_split' unfolding csi by blast
obtain n' where n': ‹csπ' n' = xs@[x']› and jn': ‹j' cdπ'→ n'› using cs cs_split' unfolding csj by blast
have ‹m ≤ n› using ilj m n wn_cs_butlast[OF _ jn im] by force
moreover
have ‹m ≠ n› using m n xx by (metis last_snoc)
ultimately
have mn: ‹m < n› by auto
moreover
have ‹π m ≠ return› by (metis last_cs last_snoc m mn n path(1) term_path_stable xx less_imp_le)
moreover
have ‹butlast (csπ m) = butlast (csπ n)› ‹csπ m = csπ' m'› ‹csπ n = csπ' n'› using m n n' m' by auto
ultimately
have ‹m' < n'› using claim path by blast
thus ‹i' < j'› using m' n' im' jn' wn_cs_butlast by (metis butlast_snoc)
qed
qed
next
case (prefix1 xs)
note pfx = ‹csπ i = csπ j @ xs›
note xs = ‹xs ≠ []›
obtain a as where ‹xs = a#as› using xs by (metis list.exhaust)
moreover
obtain bs b where bj: ‹csπ j = bs@[b]› using cs_not_nil by (metis rev_exhaust)
ultimately
have ‹csπ i = bs@[b,a]@as› using pfx by auto
then obtain m where ‹csπ m = bs@[b]› and cdep: ‹i cdπ→ m› using cs_split' by blast
hence mi: ‹m = j› using bj cs_inj by (metis is_cdi_def term_path_stable less_imp_le)
hence ‹i cdπ→ j› using cdep by auto
hence ‹False› using ilj unfolding is_cdi_def by auto
thus ‹i' < j'› ..
next
case (prefix2 xs)
have pfx : ‹csπ' i' @ xs = csπ' j'› using prefix2 csi csj by auto
note xs = ‹xs ≠ []›
obtain a as where ‹xs = a#as› using xs by (metis list.exhaust)
moreover
obtain bs b where bj: ‹csπ' i' = bs@[b]› using cs_not_nil by (metis rev_exhaust)
ultimately
have ‹csπ' j' = bs@[b,a]@as› using pfx by auto
then obtain m where ‹csπ' m = bs@[b]› and cdep: ‹j' cdπ'→ m› using cs_split' by blast
hence mi: ‹m = i'› using bj cs_inj by (metis is_cdi_def term_path_stable less_imp_le)
hence ‹j' cdπ'→ i'› using cdep by auto
thus ‹i' < j'› unfolding is_cdi_def by auto
qed
cs_order_le: assumes path: ‹is_path π› ‹is_path π'› and csi: ‹csπ i = csπ' i'›
csj: ‹csπ j = csπ' j'› and nret: ‹π i ≠ return› and ilj: ‹i ≤ j›
‹i'≤j'› proof cases
assume ‹i < j› with cs_order[OF assms(1,2,3,4,5)] show ‹?thesis› by simp
assume ‹¬ i < j›
hence ‹i = j› using ilj by simp
hence csij: ‹csπ' i' = csπ' j'› using csi csj by simp
have nret': ‹π' i' ≠ return› using nret last_cs csi by metis
show ‹?thesis› using cs_inj[OF path(2) nret' csij] by simp
cs_induct[case_names cs] = cs.induct
icdi_path_swap: assumes ‹is_path π'› ‹j icdπ→k› ‹π = π'› shows ‹j icdπ'→k› using assms unfolding eq_up_to_def is_icdi_def is_cdi_def by auto
icdi_path_swap_le: assumes ‹is_path π'› ‹j icdπ→k› ‹π = π'› ‹j ≤ n› shows ‹j icdπ'→k› by (metis assms icdi_path_swap eq_up_to_le)
cs_path_swap: assumes ‹is_path π› ‹is_path π'› ‹π = π'› shows ‹csπ k = csπ' k› using assms(1,3) proof (induction ‹π› ‹k› rule:cs_induct,cases)
case (cs π k)
let ‹?l› = ‹(THE l. k icdπ→ l)›
assume *: ‹∃l. k icdπ→ l›
have kicd: ‹k icdπ→ ?l› by (metis "*" icd_is_the_icd)
hence ‹?l < k› unfolding is_cdi_def[of ‹k› ‹π› ‹?l›] is_icdi_def[of ‹k› ‹π› ‹?l›] by auto
hence ‹∀ i≤?l. π i = π' i› using cs(2,3) unfolding eq_up_to_def by auto
hence csl: ‹csπ ?l = csπ' ?l› using cs(1,2) * unfolding eq_up_to_def by auto
have kicd: ‹k icdπ→ ?l› by (metis "*" icd_is_the_icd)
hence csk: ‹csπ k = csπ ?l @ [π k]› using kicd by auto
have kicd': ‹k icdπ'→ ?l› using kicd icdi_path_swap[OF assms(2) _ cs(3)] by simp
hence ‹?l = (THE l. k icdπ'→ l)› by (metis icd_is_the_icd)
hence csk': ‹csπ' k = csπ' ?l @ [π' k]› using kicd' by auto
have ‹π' k = π k› using cs(3) unfolding eq_up_to_def by auto
with csl csk csk'
show ‹?case› by auto
case (cs π k)
assume *: ‹¬ (∃l. k icdπ→ l)›
hence csk: ‹csπ k = [π k]› by auto
have ‹¬ (∃l. k icdπ'→ l)› apply (rule ccontr) using * icdi_path_swap_le[OF cs(2) _, of ‹k› ‹π'›] cs(3) by (metis eq_up_to_sym le_refl)
hence csk': ‹csπ' k = [π' k]› by auto
with csk show ‹?case› using cs(3) eq_up_to_apply by auto
cs_path_swap_le: assumes ‹is_path π› ‹is_path π'› ‹π = π'› ‹k ≤ n› shows ‹csπ k = csπ' k› by (metis assms cs_path_swap eq_up_to_le)
cs_path_swap_cd: assumes ‹is_path π› and ‹is_path π'› and ‹csπ n = csπ' n'› and ‹n cdπ→ k›
k' where ‹n' cdπ'→ k'› and ‹csπ k = csπ' k'›
-
from cd_in_cs[OF assms(4)]
obtain ns where *: ‹csπ n = csπ k @ ns @ [π n]› by blast
obtain xs x where csk: ‹csπ k = xs @ [x]› by (metis cs_not_nil rev_exhaust)
have ‹π n = π' n'› using assms(3) last_cs by metis
hence **: ‹csπ' n' = xs@[x]@ns@[π' n']› using * assms(3) csk by auto
from cs_split[OF **]
obtain k' where ‹csπ' k' = xs @ [x]› ‹n' cdπ'→ k'› by blast
thus ‹thesis› using that csk by auto
path_ipd_swap: assumes ‹is_path π› ‹π k ≠ return› ‹k < n›
π' m where ‹is_path π'› ‹π = π'› ‹k < m› ‹π' m = ipd (π' k)› ‹∀ l ∈ {k..<m}. π' l ≠ ipd (π' k)›
-
obtain π' r where *: ‹π' 0 = π n› ‹is_path π'› ‹π' r = return› by (metis assms(1) path_nodes reaching_ret)
let ‹?π› = ‹π@ π'›
have path: ‹is_path ?π› and ret: ‹?π (n + r) = return› and equpto: ‹?π = π› using assms path_cons * path_append_eq_up_to by auto
have πk: ‹?π k = π k› by (metis assms(3) less_imp_le_nat path_append_def)
obtain j where j: ‹k < j ∧ j ≤ (n + r) ∧ ?π j = ipd (π k)› (is ‹?P j› )by (metis πk assms(2) path path_ret_ipd ret)
define m where m: ‹m ≡ LEAST m . ?P m›
have Pm: ‹?P m› using LeastI[of ‹?P› ‹j›] j m by auto
hence km: ‹k < m› ‹m ≤ (n + r)› ‹?π m = ipd (π k)› by auto
have le: ‹∧l. ?P l ==> m ≤ l› using Least_le[of ‹?P›] m by blast
have πknipd: ‹?π k ≠ ipd (π k)› by (metis πk assms(1) assms(2) ipd_not_self path_nodes)
have nipd': ‹∧l. k < l ==> l < m ==> ?π l ≠ ipd (π k)› apply (rule ccontr) using le km(2) by force
have ‹∀ l ∈ {k..<m}. ?π l ≠ ipd(π k)› using πknipd nipd' by(auto, metis le_eq_less_or_eq,metis le_eq_less_or_eq)
thus ‹thesis› using that by (metis πk eq_up_to_sym km(1) km(3) path path_append_eq_up_to)
cs_sorted_list_of_cd': ‹csπ k = map π (sorted_list_of_set { i . k cdπ→ i}) @ [π k]›
(induction ‹π› ‹k› rule: cs.induct, cases)
case (1 π k)
assume ‹∃ j. k icdπ→ j›
then obtain j where j: "k icdπ→ j" ..
hence csj: ‹csπ j = map π (sorted_list_of_set {i. j cdπ→ i}) @ [π j]› by (metis "1.IH" icd_is_the_icd)
have ‹{i. k cdπ→ i} = insert j {i. j cdπ→ i}› using cdi_is_cd_icdi[OF j] by auto
moreover
have f: ‹finite {i. j cdπ→ i}› unfolding is_cdi_def by auto
moreover
have ‹j ∉ {i. j cdπ→ i}› unfolding is_cdi_def by auto
ultimately
have ‹sorted_list_of_set { i . k cdπ→ i} = insort j (sorted_list_of_set { i . j cdπ→ i})› using sorted_list_of_set_insert by auto
moreover
have ‹∀ x ∈ {i. j cdπ→ i}. x < j› unfolding is_cdi_def by auto
hence ‹∀ x ∈ set (sorted_list_of_set {i. j cdπ→ i}). x < j› by (simp add: f)
ultimately
have ‹sorted_list_of_set { i . k cdπ→ i} = (sorted_list_of_set { i . j cdπ→ i})@[j]› using insort_greater by auto
hence ‹csπ j = map π (sorted_list_of_set { i . k cdπ→ i})› using csj by auto
thus ‹?case› by (metis icd_cs j)
case (1 π k)
assume *: ‹¬ (∃ j. k icdπ→ j)›
hence ‹csπ k = [π k]› by (metis cs_cases)
moreover
have ‹{ i . k cdπ→ i} = {}› by (auto, metis * excd_impl_exicd)
ultimately
show ‹?case› by (metis append_Nil list.simps(8) sorted_list_of_set_empty)
cs_sorted_list_of_cd: ‹csπ k = map π (sorted_list_of_set ({ i . k cdπ→ i} ∪ {k}))› proof -
have le: ‹∀ x ∈ {i. k cdπ→i}.∀ y ∈ {k}. x < y› unfolding is_cdi_def by auto
have fin: ‹finite {i. k cdπ→i}› ‹finite {k}› unfolding is_cdi_def by auto
show ‹?thesis› unfolding cs_sorted_list_of_cd'[of ‹π› ‹k›] sorted_list_of_set_append[OF fin le] by auto
cs_not_ipd: assumes ‹k cdπ→ j ∧ ipd (π j) ≠ ipd (π k)› (is ‹?Q j›)
‹csπ (GREATEST j. k cdπ→ j ∧ ipd (π j) ≠ ipd (π k)) = [n←csπ k . ipd n ≠ ipd (π k)]›
is ‹csπ ?j = filter ?P _›)
-
have csk: ‹csπ k = map π (sorted_list_of_set ({ i . k cdπ→ i } ∪ {k}))› by (metis cs_sorted_list_of_cd)
have csj: ‹csπ ?j = map π (sorted_list_of_set ({i. ?j cdπ→ i } ∪ {?j}))› by (metis cs_sorted_list_of_cd)
have bound: ‹∀ j. k cdπ→ j ∧ ipd (π j) ≠ ipd(π k) ⟶ j ≤ k› unfolding is_cdi_def by simp
have kcdj: ‹k cdπ→ ?j› and ipd': ‹ipd (π ?j) ≠ ipd(π k)› using GreatestI_nat[of ‹?Q› ‹j› ‹k›, OF assms] bound by auto
have greatest: ‹∧ j. k cdπ→ j ==> ipd (π j) ≠ ipd (π k) ==> j ≤ ?j› using Greatest_le_nat[of ‹?Q› _ ‹k›] bound by auto
have less_not_ipdk: ‹∧ j. k cdπ→ j ==> j < ?j ==> ipd (π j) ≠ ipd (π k)› by (metis (lifting) ipd' kcdj same_ipd_stable)
hence le_not_ipdk: ‹∧ j. k cdπ→ j ==> j ≤ ?j ==> ipd (π j) ≠ ipd (π k)› using kcdj ipd' by (case_tac ‹j = ?j›,auto)
have *: ‹{j ∈ {i. k cdπ→i} ∪ {k}. ?P (π j)} = insert ?j { i . ?j cdπ→ i} ›
apply auto
apply (metis (lifting, no_types) greatest cr_wn'' kcdj le_antisym le_refl)
apply (metis kcdj)
apply (metis ipd')
apply (metis (full_types) cd_trans kcdj)
apply (subgoal_tac ‹k cdπ→ x›)
apply (metis (lifting, no_types) is_cdi_def less_not_ipdk)
by (metis (full_types) cd_trans kcdj)
have ‹finite ({i . k cdπ→ i} ∪ {k})› unfolding is_cdi_def by auto
note filter_sorted_list_of_set[OF this, of ‹?P o π›]
hence ‹[n←csπ k . ipd n ≠ ipd(π k)] = map π (sorted_list_of_set {j ∈ {i. k cdπ→i} ∪ {k}. ?P (π j)})› unfolding csk filter_map by auto
also
have ‹… = map π (sorted_list_of_set (insert ?j { i . ?j cdπ→ i}))› unfolding * by auto
also
have ‹… = csπ ?j› using csj by auto
finally
show ‹?thesis› by metis
cs_ipd: assumes ipd: ‹π m = ipd (π k)› ‹∀ n ∈ {k..<m}. π n ≠ ipd (π k)›
km: ‹k < m› shows ‹csπ m = [n←csπ k . ipd n ≠ π m] @ [π m]›
cases
assume ‹∃ j. m icdπ→ j›
then obtain j where jicd: ‹m icdπ→ j› by blast
hence *: ‹csπ m = csπ j @ [π m]› by (metis icd_cs)
have j: ‹j = (GREATEST j. k cdπ→ j ∧ ipd (π j) ≠ π m)› using jicd assms ipd_icd_greatest_cd_not_ipd by blast
moreover
have ‹ipd (π j) ≠ ipd (π k)› by (metis is_cdi_def is_icdi_def is_ipd_def cd_not_pd ipd(1) ipd_is_ipd jicd path_nodes less_imp_le term_path_stable)
moreover
have ‹k cdπ→ j› unfolding j by (metis (lifting, no_types) assms(3) cd_ipd_is_cd icd_imp_cd ipd(1) ipd(2) j jicd)
ultimately
have ‹csπ j = [n←csπ k . ipd n ≠ π m]› using cs_not_ipd[of ‹k› ‹π› ‹j›] ipd(1) by metis
thus ‹?thesis› using * by metis
assume noicd: ‹¬ (∃ j. m icdπ→ j)›
hence csm: ‹csπ m = [π m]› by auto
have ‹∧j. k cdπ→j ==> ipd(π j) = π m› using cd_is_cd_ipd[OF km ipd] by (metis excd_impl_exicd noicd)
hence *: ‹{j ∈ {i. k cdπ→ i} ∪ {k}. ipd (π j) ≠ π m} = {}› using ipd(1) by auto
have **: ‹((λn. ipd n ≠ π m) o π) = (λn. ipd (π n) ≠ π m)› by auto
have fin: ‹finite ({i. k cdπ→ i} ∪ {k})› unfolding is_cdi_def by auto
note csk = cs_sorted_list_of_cd[of ‹π› ‹k›]
hence ‹[n←csπ k . ipd n ≠ π m] = [n← (map π (sorted_list_of_set ({i. k cdπ→ i} ∪ {k}))) . ipd n ≠ π m]› by simp
also
have ‹… = map π [n <- sorted_list_of_set ({i. k cdπ→ i} ∪ {k}). ipd (π n) ≠ π m]› by (auto simp add: filter_map **)
also
have ‹… = []› unfolding * filter_sorted_list_of_set[OF fin, of ‹λn. ipd (π n) ≠ π m›] by auto
finally
show ‹?thesis› using csm by (metis append_Nil)
converged_ipd_same_icd: assumes path: ‹is_path π› ‹is_path π'› and converge: ‹l < m› ‹csπ m = csπ' m'›
csk: ‹csπ k = csπ' k'› and icd: ‹l icdπ→ k› and suc: ‹π (Suc k) = π' (Suc k')›
ipd: ‹π' m' = ipd (π k)› ‹∀ n ∈ {k'..<m'}. π' n ≠ ipd (π k)›
‹∃l'. csπ l = csπ' l'›
cases
assume l: ‹l = Suc k›
hence ‹Suc k cdπ→ k› using icd by (metis is_icdi_def)
hence ‹π (Suc k) ≠ ipd (π k)› unfolding is_cdi_def by auto
hence ‹π' (Suc k') ≠ ipd (π' k')› by (metis csk last_cs suc)
moreover
have ‹π' (Suc k') ≠ return› by (metis ‹Suc k cdπ→ k› ret_no_cd suc)
ultimately
have ‹Suc k' cdπ'→ k'› unfolding is_cdi_def using path(2) apply auto
by (metis ipd_not_self le_Suc_eq le_antisym path_nodes term_path_stable)
hence ‹Suc k' icdπ'→ k'› unfolding is_icdi_def using path(2) by fastforce
hence ‹csπ' (Suc k') = csπ' k' @[π' (Suc k')]› using icd_cs by auto
moreover
have ‹csπ l = csπ k @ [π l]› using icd icd_cs by auto
ultimately
have ‹csπ l = csπ' (Suc k')› by (metis csk l suc)
thus ‹?thesis› by blast
assume nsuck: ‹l ≠ Suc k›
have kk'[simp]: ‹π' k' = π k› by (metis csk last_cs)
have kl: ‹k < l› using icd unfolding is_icdi_def is_cdi_def by auto
open>Suc k < lk
hence lpd: ‹ (uc k\closeusng ic icd_pd_inerediateby uto
have km: ‹
have lcd: ‹I")
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "brackoff" is null
have *: ‹[F]0 & ∀n([F]n → [F]n')›
have nretk: ‹π k ≠I")
have **: ‹ l) pd→ k)›
assume a: ‹ ipd (π
hence ‹ l pd→π k)› by (metis is_ipd_def ‹›h) pthnodspdanisymtempa_saleles_ie
moreover
have ‹
ultimately
show ‹
havea km: ‹'› cs_order[OF path csk converge(2) nretk km] .
π'' n'' where path'': ‹''›0: \openπ k)›''n: \openπ'' n'' = return› and notπl: ‹n''. π> π l›
?π'›(π' @π'') «
>s_path ?π'› by (metis π''0 ipd(1) ) pat' pa(2 ahcnh_pt_sit
moreover
have ‹
moreover
have ‹ uing \pi''n km' \' π''0 ipd(1) by auto
ultimately
obtain AOT_show \<H]u›[G]u› using 0 1 "≡
have l''m: \<open [H]u ≡ [G]u›
let ‹?l'› = ‹[F]u› if ‹ using 0 1 "🚫
?l' ≤ m'› using l''m km' by auto
―
open>π' ?l' = π l› using l'' l''m lm' by auto
have 2: ‹ by simp
?l' < m'›
― ‹
let ‹ = ‹' l' = π k' < l'›
have *: ‹?P ?l'› using 1 2 3 by blast
define l' where l': \<openl
have π
have kl': ‹k' < l'›cets[HN rlif1zer]" OF "-eis:2, ymti]
have lm': ‹'›?P›
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "brackoff" is null
have nipd': ‹∀ j ∈ {k'..l'}. π(rule "→
have lcd': ‹l' cd\\^>π' k'›
have lcd \open' icdπ' k'›
java.lang.NullPointerException
java.lang.NullPointerException
then obtain j' where kj': ‹close>and jl': ‹'›l' cdπ' by force
have jm': ‹
have \<<pi π apply (rule ccontr) using l' kj' jm' jl' Least_le[of ‹j'›] by auto
¬ π' l' pd→ π using cd_not_pd lcdj' πl' by metis
moreover have ‹
ultimately
java.lang.NullPointerException
let ‹ = ‹ π Suc k🚫o∀x([H]x → O!x)›
java.lang.NullPointerException
moreover
have ‹
moreover
have kj': ‹Suc k' ≤ j'› by (metis kj' less_eq_Suc_le)
hence ‹ s,metis<>01)
ultimately
obtain l'' where *: ‹?π'' l'' = π=‹ ([H] ==> [F]))<down\guillemotright>}›
show ‹
assume a: ‹l'' ≤ j' - Suc k'›
hence ‹
moreover
have ‹'› by (metis a jl' add_diff_cancel_right' kj' le_add_diff_inverse less_imp_difes oed_nel_oni_i_las._dfcov2
moreover
have ‹∃c ConceptOf(c,G)›
moreover
have ‹∃I)
ultimately
show ‹
next
assume a: ‹¬x[G]›
hence ‹tsNl-idd:1zro", aeist:",smei]
hence ‹ConceptOf(c,G)› ‹ [G] <Rightarrow[ for: c;
moreover
have ‹Suc (k' + l'') - j' ≤E"(2)] "con-exists:2"[THEN "RA[2]"])
ultimately
False› using nl' by (metis πl')
qed
AOT_theorem "concept-G[concept]": \pen!cG›
thus ‹?thesis› unfolding is_icdi_def using lcd' path(2) by simp
hence ‹-]FccetsOF"oaeit:"
hence ‹ l' = csl›l' csk icd icd_cs)
:\><>< ‹is_path π'› and converge: ‹ ‹π n = cs
csk: ‹ k = cs andcd:‹→ and suc: ‹
‹
have nret \openπ k ≠ return›
have kl: ‹metric rueE"b
have kn: ‹E"(1)] "∀
rompt_ipd_sswapOFpath() net ]
obtain ρ m where pathρ: ‹<>:π =ρ and km: ‹›ρ m = ipd (ρ k)›∀ l ∈ l ≠ .
have csk1: ‹E"(2)]
java.lang.StringIndexOutOfBoundsException: Index 106 out of bounds for length 106
have nret': ‹fE"] "&E"(2))
act2axio_inst, EN \<equivE"(1)] by simp
from path_ipd_swap[OF path(2) nret' kn']
obtain\rho'm' here path\rho' 🚫π' =ρ and km': ‹ and ipd': ‹ ‹ ρ ipd (ρ' k')›
have csk1': ‹ k' = cs using cs_path_swap_le path pathρ' π' kn' by auto
have sucρ^sub>1, THEN "\<equivE
icdρ: ‹l icdρ→ k› icd π] conergeby imp
have lm: ‹ using ipd(1) icdρ km unfolding is_icdi_def is_cdi_def by auto
have csk': ‹\<rho k = csk'›
hence kk': ‹ uing last_c ei
have suc': ‹ρ∀x ([H]x → O!x)›
have mm': ‹ρ[H]x›
from cs_ipd[OF ipd km] cs_ipd[OF ipd' km',unfolded mm', folded csk']
have csm: ‹◻∀ [G]x)›
>G ≡E F¬, simplified] 0 1 2 by fast
from converged_ipd_same_icd[OF pathρ pathρ' lm csm csk' icdρ suc' ipd'[unfolded kk']]
obtain l' where csl: ‹
have cslρ: ‹
have nretl: ‹ccH[G])›
have csn': ‹csρ n = csρ' n'› using converge(2) cs_path_swap path pathρE" by blast
ln': ‹l' < nah<>
': ‹ l' = cs\^ρ' using cs_path_swap_le[OF path(2) path\rho πρ'] ln' by auto
have csl': ‹[λx C!x & ∀ <›
thus ‹
java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
wherecl \open>s>π using cd_in_cs[OF assms] by blast
hence len: ‹
show ‹
cs_select_id: assumes ‹is_path π› ‹
java.lang.NullPointerException
hence \AOT_thus[λz [R]za] = [λz [R]zb]›
thus ‹y [λz [G]x])]↓
cs_single_nocd: assumes ‹π shows ‹k. ¬π k›
have ‹¬ (∃ k. i icd∀x ∀y (∀ [F]y) → ◻ z[λz [G]y]))›
hence ‹¬ (∃ k. i cd"(2), THEN "∀ F ] y at
thus ‹
cs_single_pd_intermed: assumes ‹fI"] "&I" "log-prop-prop:2")
have ‹The assumptions of the theorems above are derivable, if the additional
thus ‹?thesis›
cs_first_pd: assumes path: ‹is_path π› and pd: ‹π n pd→ π 0› and first: ‹∀ l < n. π l ≠ π n› shows ‹csπ n = [π n]›
(metis cs_cases first first_pd_no_cd icd_imp_cd path pd)
converged_pd_cs_single: assumes path: ‹is_path π› ‹is_path π'› and converge: ‹l < m› ‹csπ m = csπ' m'›
π0: ‹π 0 = π' 0› and mpdl: ‹π m pd→ π l› and csl: ‹csπ l = [π l]›
‹∃l'. csπ l = csπ' l'› proof -
have *: ‹π l pd→ π' 0› using cs_single_pd_intermed[OF path(1) csl] π0[symmetric] by auto
have πm: ‹π m = π' m'› by (metis converge(2) last_cs)
hence **: ‹π' m' pd→ π l› using mpdl by metis
obtain l' where lm': ‹l' ≤ m'› and πl: ‹π' l' = π l› (is ‹?P l'›) using path_pd_pd0[OF path(2) ** *] .
let ‹?l› = ‹(LEAST l'. π' l' = π l)›
have πl': ‹π' ?l = π l› using LeastI[of ‹?P›,OF πl] .
moreover
have ‹∀ i <?l. π' i ≠ π l› using Least_le[of ‹?P›] by (metis not_less)
hence ‹∀ i <?l. π' i ≠ π' ?l› using πl' by metis
moreover
have ‹π' ?l pd→ π' 0› using * πl' by metis
ultimately
have ‹csπ' ?l = [π' ?l]› using cs_first_pd[OF path(2)] by metis
thus ‹?thesis› using csl πl' by metis
converged_cs_single: assumes path: ‹is_path π› ‹is_path π'› and converge: ‹l < m› ‹csπ m = csπ' m'›
π0: ‹π 0 = π' 0› and csl: ‹csπ l = [π l]›
‹∃l'. csπ l = csπ' l'› proof cases
assume *: ‹π l = return›
hence ‹π m = return› by (metis converge(1) path(1) term_path_stable less_imp_le)
hence ‹csπ m = [return]› using cs_return by auto
hence ‹csπ' m' = [return]› using converge by simp
moreover
have ‹csπ l = [return]› using * cs_return by auto
ultimately show ‹?thesis› by metis
assume nret: ‹π l ≠ return›
have πm: ‹π m = π' m'› by (metis converge(2) last_cs)
obtain π1 n where path1: ‹is_path π1› and upto: ‹π = π1› and πn: ‹π1 n = return› using path(1) path_swap_ret by blast
obtain π1' n' where path1': ‹is_path π1'› and upto': ‹π' =' π1'› and πn': ‹π1' n' = return› using path(2) path_swap_ret by blast
have π1l: ‹π1 l = π l› using upto converge(1) by (metis eq_up_to_def nat_less_le)
have cs1l: ‹csπ1 l = csπ l› using cs_path_swap_le upto path1 path(1) converge(1) by auto
have csl1: ‹csπ1 l = [π1 l]› by (metis π1l cs1l csl)
have converge1: ‹csπ1 n = csπ1' n'› using πn πn' cs_return by auto
have ln: ‹l < n› using nret πn π1l term_path_stable[OF path1 πn] by (auto, metis linorder_neqE_nat less_imp_le)
have π01: ‹π1 0 = π1' 0› using π0 eq_up_to_apply[OF upto] eq_up_to_apply[OF upto'] by auto
have pd: ‹π1 n pd→ π1 l› using πn by (metis path1 path_nodes return_pd)
obtain l' where csl: ‹csπ1 l = csπ1' l'› using converged_pd_cs_single[OF path1 path1' ln converge1 π01 pd csl1] by blast
have cs1m: ‹csπ1 m = csπ m› using cs_path_swap upto path1 path(1) by auto
have cs1m': ‹csπ1' m' = csπ' m'› using cs_path_swap upto' path1' path(2) by auto
hence converge1: ‹csπ1 m = csπ1' m'› using converge(2) cs1m by metis
have nret1: ‹π1 l ≠ return› using nret π1l by auto
have lm': ‹l' < m'› using cs_order[OF path1 path1' csl converge1 nret1 converge(1)] .
have ‹csπ' l' = csπ1' l'› using cs_path_swap_le[OF path(2) path1' upto'] lm' by auto
moreover
have ‹csπ l = csπ1 l› using cs_path_swap_le[OF path(1) path1 upto] converge(1) by auto
ultimately
have ‹csπ l = csπ' l'› using csl by auto
thus ‹?thesis› by blast
converged_cd_same_suc: assumes path: ‹is_path π› ‹is_path π'› and init: ‹π 0 = π' 0›
cd_suc: ‹∀ k k'. csπ k = csπ' k' ∧ l cdπ→ k ⟶ π (Suc k) = π' (Suc k')› and converge: ‹l < m› ‹csπ m = csπ' m'›
‹∃l'. csπ l = csπ' l'›
path init cd_suc converge proof (induction ‹π› ‹l› rule: cs_induct,cases)
case (cs π l)
assume *: ‹∃k. l icdπ→ k›
let ‹?k› = ‹THE k. l icdπ→ k›
have icd: ‹l icdπ→ ?k› by (metis "*" icd_is_the_icd)
hence lcdk: ‹l cdπ→ ?k› by (metis is_icdi_def)
hence kl: ‹?k<l\› using is_cdi_def by metis
have ‹∧ j. ?k cdπ→ j ==> l cdπ→ j› using icd cd_trans is_icdi_def by fast
hence suc': ‹∀ j j'. csπ j = csπ' j' ∧ ?k cdπ→ j ⟶ π (Suc j) = π' (Suc j')› using cs.prems(4) by blast
from cs.IH[OF * cs(2) path(2) cs(4) suc'] cs.prems kl
have ‹∃k'. csπ (THE k. l icdπ→ k) = csπ' k'› by (metis Suc_lessD less_trans_Suc)
then obtain k' where csk: ‹csπ ?k = csπ' k'› by blast
have suc2: ‹π (Suc ?k) = π' (Suc k')› using cs.prems(4) lcdk csk by auto
have km: ‹?k < m› using kl cs.prems(5) by simp
from converged_same_icd[OF cs(2) path(2) cs.prems(5) cs.prems(6) csk icd suc2]
show ‹?case› .
case (cs π l)
assume ‹¬ (∃k. l icdπ→ k)›
hence ‹csπ l = [π l]› by auto
with cs converged_cs_single
show ‹?case› by metis
converged_cd_diverge:
path: ‹is_path π› ‹is_path π'› and init: ‹π 0 = π' 0› and notin: ‹¬ (∃l'. csπ l = csπ' l')› and converge: ‹l < m› ‹csπ m = csπ' m'›
k k' where ‹csπ k = csπ' k'› ‹l cdπ→ k› ‹π (Suc k) ≠ π' (Suc k')›
assms converged_cd_same_suc by blast
converged_cd_same_suc_return: assumes path: ‹is_path π› ‹is_path π'› and π0: ‹π 0 = π' 0›
cd_suc: ‹∀ k k'. csπ k = csπ' k' ∧ l cdπ→ k ⟶ π (Suc k) = π' (Suc k')› and ret: ‹π' n' = return›
‹∃l'. csπ l = csπ' l'›proof cases
assume ‹π l = return›
hence ‹csπ l = csπ' n'› using ret cs_return by presburger
thus ‹?thesis› by blast
assume nretl: ‹π l ≠ return›
have ‹π l ∈ nodes› using path path_nodes by auto
then obtain πl n where ipl: ‹is_path πl› and πl: ‹π l = πl 0› and retn: ‹πl n = return› and notl: ‹∀ i>0. πl i ≠ π l› by (metis direct_path_return nretl)
hence ip: ‹is_path (π@ πl)› and l: ‹(π@ πl) l = π l› and retl: ‹(π@ πl) (l + n) = return› and nl: ‹∀ i>l. (π@ πl) i ≠ π l› using path_cons[OF path(1) ipl πl] by auto
have π0': ‹(π@ πl) 0 = π' 0› unfolding cs_0 using πl π0 by auto
have csn: ‹csπ@ πl (l+n) = csπ' n'› using ret retl cs_return by metis
have eql: ‹(π@ πl) = π› by (metis path_append_eq_up_to)
have csl': ‹csπ@ πl l = csπ l› using eql cs_path_swap ip path(1) by metis
have ‹0 < n› using nretl[unfolded πl] retn by (metis neq0_conv)
hence ln: ‹l < l + n› by simp
have *: ‹∀ k k'. csπ @ πl k = csπ' k' ∧ l cdπ @ πl→ k ⟶ (π @ πl) (Suc k) = π' (Suc k')› proof (rule,rule,rule)
fix k k' assume *: ‹csπ @ πl k = csπ' k' ∧ l cdπ @ πl→ k›
hence kl: ‹k < l› using is_cdi_def by auto
hence ‹csπ k = csπ' k' ∧ l cdπ→ k› using eql * cs_path_swap_le[OF ip path(1) eql,of ‹k›] cdi_path_swap_le[OF path(1) _ eql,of ‹l› ‹k›] by auto
hence ‹π (Suc k) = π' (Suc k')› using cd_suc by blast
then show ‹(π @ πl) (Suc k) = π' (Suc k')› using cs_path_swap_le[OF ip path(1) eql,of ‹Suc k›] kl by auto
qed
obtain l' where ‹csπ @ πl l = csπ' l'› using converged_cd_same_suc[OF ip path(2) π0' * ln csn] by blast
moreover
have ‹csπ@ πl l = csπ l› using eql by (metis cs_path_swap ip path(1))
ultimately
show ‹?thesis› by metis
converged_cd_diverge_return: assumes path: ‹is_path π› ‹is_path π'› and init: ‹π 0 = π' 0›
notin: ‹¬ (∃l'. csπ l = csπ' l')› and ret: ‹π' m' = return›
k k' where ‹csπ k = csπ' k'› ‹l cdπ→ k› ‹π (Suc k) ≠ π' (Suc k')› using converged_cd_same_suc_return[OF path init _ ret, of ‹l›] notin by blast
returned_missing_cd_or_loop: assumes path: ‹is_path π› ‹is_path π'› and π0: ‹π 0 = π' 0›
notin': ‹¬(∃ k'. csπ k = csπ' k')› and nret: ‹∀ n'. π' n' ≠ return› and ret: ‹π n = return›
i i' where ‹i<k\› ‹csπ i = csπ' i'› ‹π (Suc i) ≠ π' (Suc i')› ‹k cdπ→ i ∨ (∀ j'> i'. j' cdπ'→ i')›
-
obtain f where icdf: ‹∀ i'. f (Suc i') icdπ'→ f i'› and ran: ‹range f = {i'. ∀ j'>i'. j' cdπ'→ i'}› and icdf0: ‹¬ (∃i'. f 0 cdπ'→ i')› using path(2) path_nret_inf_icd_seq nret by blast
show ‹thesis› proof cases
assume ‹∃ j. ¬ (∃ i. csπ i = csπ' (f j))›
then obtain j where niπ: ‹¬ (∃ i. csπ' (f j) = csπ i)› by metis
note converged_cd_diverge_return[OF path(2,1) π0[symmetric] niπ ret] that
then obtain i k' where csk: ‹csπ i = csπ' k'› and cdj: ‹f j cdπ'→ k'› and div: ‹π (Suc i) ≠ π' (Suc k')› by metis
have ‹k' ∈ range f› using cdj proof (induction ‹j›)
case 0 thus ‹?case› using icdf0 by blast
next
case (Suc j)
have icdfj: ‹f (Suc j) icdπ'→ f j› using icdf by auto
show ‹?case› proof cases
assume ‹f (Suc j) icdπ'→ k'›
hence ‹k' = f j› using icdfj by (metis icd_uniq)
thus ‹?case› by auto
next
assume ‹¬ f (Suc j) icdπ'→ k'›
hence ‹f j cdπ'→ k'› using cd_impl_icd_cd[OF Suc.prems icdfj] by auto
thus ‹?case› using Suc.IH by auto
qed
qed
hence alldep: ‹∀ i'>k'. i' cdπ'→ k'› using ran by auto
show ‹thesis› proof cases
assume ‹i < k› with alldep that[OF _ csk div] show ‹thesis› by blast
next
assume ‹¬ i < k›
hence ki: ‹k≤i› by auto
have ‹k ≠ i› using notin' csk by auto
hence ki': ‹k<i\› using ki by auto
obtain ka k' where ‹csπ ka = csπ' k'› ‹k cdπ→ ka› ‹π (Suc ka) ≠ π' (Suc k')›
using converged_cd_diverge[OF path π0 notin' ki' csk] by blast
moreover
hence ‹ka < k› unfolding is_cdi_def by auto
ultimately
show ‹?thesis› using that by blast
qed
next
assume ‹¬(∃ j. ¬ (∃ i. csπ i = csπ' (f j)))›
hence allin: ‹∀ j. (∃ i. csπ i = csπ' (f j))› by blast
define f' where f': ‹f' ≡ λ j. (SOME i. csπ i = csπ' (f j))›
have ‹∀ i. f' i < f' (Suc i)› proof
fix i
have csi: ‹csπ' (f i) = csπ (f' i)› unfolding f' using allin by (metis (mono_tags) someI_ex)
have cssuci: ‹csπ' (f (Suc i)) = csπ (f' (Suc i))› unfolding f' using allin by (metis (mono_tags) someI_ex)
have fi: ‹f i < f (Suc i)› using icdf unfolding is_icdi_def is_cdi_def by auto
have ‹f (Suc i) cdπ'→ f i› using icdf unfolding is_icdi_def by blast
hence nreti: ‹π' (f i) ≠ return› by (metis cd_not_ret)
show ‹f' i < f' (Suc i)› using cs_order[OF path(2,1) csi cssuci nreti fi] .
qed
hence kle: ‹k < f' (Suc k)› using mono_ge_id[of ‹f'› ‹Suc k›] by auto
have cssk: ‹csπ (f' (Suc k)) = csπ' (f (Suc k))› unfolding f' using allin by (metis (mono_tags) someI_ex)
obtain ka k' where ‹csπ ka = csπ' k'› ‹k cdπ→ ka› ‹π (Suc ka) ≠ π' (Suc k')›
using converged_cd_diverge[OF path π0 notin' kle cssk] by blast
moreover
hence ‹ka < k› unfolding is_cdi_def by auto
ultimately
show ‹?thesis› using that by blast
qed
missing_cd_or_loop: assumes path: ‹is_path π› ‹is_path π'› and π0: ‹π 0 = π' 0› and notin': ‹¬(∃ k'. csπ k = csπ' k')›
i i' where ‹i < k› ‹csπ i = csπ' i'› ‹π (Suc i) ≠ π' (Suc i')› ‹k cdπ→ i ∨ (∀ j'> i'. j' cdπ'→ i')›
cases
assume ‹∃ n'. π' n' = return›
then obtain n' where retn: ‹π' n' = return› by blast
note converged_cd_diverge_return[OF path π0 notin' retn]
then obtain ka k' where ‹csπ ka = csπ' k'› ‹k cdπ→ ka› ‹π (Suc ka) ≠ π' (Suc k')› by blast
moreover
hence ‹ka < k› unfolding is_cdi_def by auto
ultimately show ‹thesis› using that by simp
assume ‹¬ (∃ n'. π' n' = return)›
hence notret: ‹∀ n'. π' n' ≠ return› by auto
then obtain πl n where ipl: ‹is_path πl› and πl: ‹π k = πl 0› and retn: ‹πl n = return› using reaching_ret path(1) path_nodes by metis
hence ip: ‹is_path (π@πl)› and l: ‹(π@πl) k = π k› and retl: ‹(π@πl) (k + n) = return› using path_cons[OF path(1) ipl πl] by auto
have π0': ‹(π@πl) 0 = π' 0› unfolding cs_0 using πl π0 by auto
have eql: ‹(π@πl) = π› by (metis path_append_eq_up_to)
have csl': ‹csπ@πl k = csπ k› using eql cs_path_swap ip path(1) by metis
hence notin: ‹¬(∃ k'. csπ@πl k = csπ' k')› using notin' by auto
obtain i i' where *: ‹i < k› and csi: ‹csπ@πl i = csπ' i'› and suci: ‹(π @ πl) (Suc i) ≠ π' (Suc i')› and cdloop: ‹k cdπ@πl→ i ∨ (∀ j'>i'. j' cdπ'→ i')›
using returned_missing_cd_or_loop[OF ip path(2) π0' notin notret retl] by blast
have ‹i ≠ k› using notin csi by auto
hence ik: ‹i < k› using * by auto
hence ‹csπ i = csπ' i'› using csi cs_path_swap_le[OF ip path(1) eql] by auto
moreover
have ‹π (Suc i) ≠ π' (Suc i')› using ik eq_up_to_apply[OF eql, of ‹Suc i›] suci by auto
moreover
have ‹k cdπ→ i ∨ (∀ j'>i'. j' cdπ'→ i')› using cdloop cdi_path_swap_le[OF path(1) _ eql, of ‹k› ‹i›] by auto
ultimately
show ‹thesis› using that[OF *] by blast
path_shift_set_cd: assumes ‹is_path π› shows ‹{k + j| j . n cdπ«k→ j } = {i. (k+n) cdπ→ i ∧ k ≤ i }›
-
{ fix i
assume ‹i∈{k+j | j . n cdπ«k→ j }›
then obtain j where ‹i = k+j› ‹n cdπ«k→ j› by auto
hence ‹k+n cdπ→ i ∧ k ≤ i› using cd_path_shift[OF _ assms, of ‹k› ‹k+j› ‹k+n›] by simp
hence ‹i∈{ i. k+n cdπ→ i ∧ k ≤ i }› by blast
}
moreover
{ fix i
assume ‹i∈{ i. k+n cdπ→ i ∧ k ≤ i }›
hence *: ‹k+n cdπ→ i ∧ k ≤ i› by blast
then obtain j where i: ‹i = k+j› by (metis le_Suc_ex)
hence ‹k+n cdπ→ k+j› using * by auto
hence ‹n cdπ«k→ j› using cd_path_shift[OF _ assms, of ‹k› ‹k+j› ‹k+n›] by simp
hence ‹i∈{k+j | j . n cdπ«k→ j }› using i by simp
}
ultimately show ‹?thesis› by blast
cs_path_shift_set_cd: assumes path: ‹is_path π› shows ‹csπ«k n = map π (sorted_list_of_set {i. k+n cdπ→ i ∧ k ≤ i }) @ [π (k+n)]›
-
have mono:‹∀n m. n < m ⟶ k + n < k + m› by auto
have fin: ‹finite {i. n cdπ « k→ i}› unfolding is_cdi_def by auto
have *: ‹(λ x. k+x)`{i. n cdπ«k→ i} = {k + i | i. n cdπ«k→ i}› by auto
have ‹csπ«k n = map (π«k) (sorted_list_of_set {i. n cdπ«k→ i}) @ [(π«k) n]› using cs_sorted_list_of_cd' by blast
also
have ‹… = map π (map (λ x. k+x) (sorted_list_of_set{i. n cdπ«k→ i})) @ [π (k+n)]› by auto
also
have ‹… = map π (sorted_list_of_set ((λ x. k+x)`{i. n cdπ«k→ i})) @ [π (k+n)]› using sorted_list_of_set_map_mono[OF mono fin] by auto
also
have ‹… = map π (sorted_list_of_set ({k + i | i. n cdπ«k→ i})) @ [π (k+n)]› using * by auto
also
have ‹… = map π (sorted_list_of_set ({i. k+n cdπ→ i ∧ k ≤ i})) @ [π (k+n)]› using path_shift_set_cd[OF path] by auto
finally
show ‹?thesis› .
cs_split_shift_cd: assumes ‹n cdπ→ j› and ‹j < k› and ‹k < n› and ‹∀j'<k. n cdπ→ j' ⟶ j' ≤ j› shows ‹csπ n = csπ j @ csπ«k (n-k)›
-
have path: ‹is_path π› using assms unfolding is_cdi_def by auto
have 1: ‹{i. n cdπ→ i} = {i. n cdπ→ i ∧ i < k} ∪ {i. n cdπ→ i ∧ k ≤ i}› by auto
have le: ‹∀ i∈ {i. n cdπ→ i ∧ i < k}. ∀ j∈ {i. n cdπ→ i ∧ k ≤ i}. i < j› by auto
have 2: ‹{i. n cdπ→ i ∧ i < k} = {i . j cdπ→ i} ∪ {j}› proof -
{ fix i assume ‹i∈{i. n cdπ→ i ∧ i < k}›
hence cd: ‹n cdπ→ i› and ik:‹i < k› by auto
have ‹i∈{i . j cdπ→ i} ∪ {j}› proof cases
assume ‹i < j› hence ‹j cdπ→ i› by (metis is_cdi_def assms(1) cd cdi_prefix nat_less_le)
thus ‹?thesis› by simp
next
assume ‹¬ i < j›
moreover
have ‹i ≤ j› using assms(4) ik cd by auto
ultimately
show ‹?thesis› by auto
qed
}
moreover
{ fix i assume ‹i∈{i . j cdπ→ i} ∪ {j}›
hence ‹j cdπ→ i ∨ i = j› by auto
hence ‹i∈{i. n cdπ→ i ∧ i < k}› using assms(1,2) cd_trans[OF _ assms(1)] apply auto unfolding is_cdi_def
by (metis (poly_guards_query) diff_diff_cancel diff_is_0_eq le_refl le_trans nat_less_le)
}
ultimately show | |