Theory NDET

(*  Title:       Nondeterministic recursive algorithms
    ID:
    Author:      Peter Lammich <peter.lammich@uni-muenster.de>
    Maintainer:  Peter Lammich <peter.lammich@uni-muenster.de>
*)

section ‹ Nondeterministic recursive algorithms ›
theory NDET
imports Main
begin

text ‹
  This theory models nondeterministic, recursive algorithms by means of a step relation.

  An algorithm is modelled as follows: 
  \begin{enumerate}
    \item Start with some state @{text "s"}
    \item If there is no @{text "s'"} with @{text "(s,s')∈R"}, terminate with state @{text "s"}
    \item Else set @{text "s := s'"} and continue with step 2
  \end{enumerate}

  Thus, @{text R} is the step relation, relating the previous with the next state. If the state is not in the domain of @{text R}, the algorithm terminates.
›

text ‹ The relation @{text "A_rel R"} describes the non-reflexive part of the algorithm, that is all possible mappings for non-terminating initial states.
  We will first explore properties of this non-reflexive part, and then transfer them to the whole algorithm, that also specifies how
  terminating initial states are treated.
›

inductive_set A_rel :: "('s×'s) set ⇒ ('s×'s) set" for R
where
  A_rel_base: "⟦(s,s')∈R; s'∉Domain R⟧ ⟹ (s,s')∈A_rel R" |
  A_rel_step: "⟦(s,sh)∈R; (sh,s')∈A_rel R⟧ ⟹ (s,s')∈A_rel R"

subsection ‹ Basic properties ›

text ‹ The algorithm just terminates at terminating states ›
lemma termstate: "(s,s')∈A_rel R ⟹ s'∉Domain R" by (induct rule: A_rel.induct, auto)

lemma dom_subset: "Domain (A_rel R) ⊆ Domain R" by (unfold Domain_def) (auto elim: A_rel.induct) 

text ‹ We can use invariants to reason over properties of the algorithm ›
definition "is_inv R s0 P == P s0 ∧ (∀s s'. (s,s')∈R ∧ P s ⟶ P s')"

lemma inv: "⟦(s0,sf)∈A_rel R; is_inv R s0 P⟧ ⟹ P sf" by (unfold is_inv_def, induct rule: A_rel.induct) blast+
lemma invI: "⟦P s0; !! s s'. ⟦(s,s')∈R; P s⟧ ⟹ P s'⟧ ⟹ is_inv R s0 P" by (unfold is_inv_def, blast)
lemma inv2: "⟦(s0,sf)∈A_rel R; P s0; !! s s'. ⟦(s,s')∈R; P s⟧ ⟹ P s'⟧ ⟹ P sf"
  apply (subgoal_tac "is_inv R s0 P")
  apply (blast intro: inv)
  apply (blast intro: invI)
done

text ‹ To establish new invariants, we can use already existing invariants ›
lemma inv_useI: "⟦P s0; !! s s'. ⟦(s,s')∈R; P s; !!P'. is_inv R s0 P' ⟹ P' s ⟧ ⟹ P s' ⟧ ⟹ is_inv R s0 (λs. P s ∧ (∀P'. is_inv R s0 P' ⟶ P' s))"
  apply (rule invI)
  apply (simp (no_asm) only: is_inv_def, blast)
  apply safe
  apply blast
  apply (subgoal_tac "P' s")
  apply (simp (no_asm_use) only: is_inv_def, blast)
  apply fast
  done  
  
text ‹ If the inverse step relation is well-founded, the algorithm will terminate for every state in @{text "Domain R"} (@{text "⊆"}-direction). The @{text "⊇"}-direction is from @{thm [source] dom_subset} ›
(* TODO: Prove also the other direction of this lemma … *)
lemma wf_dom_eq: "wf (R¯) ⟹ Domain R = Domain (A_rel R)" proof -
  assume WF: "wf (R¯)"
  hence "(∃sf. (s,sf) ∈ A_rel R)" if "(s,s')∈R" for s s' using that
  proof (induction arbitrary: s')
    case (less x)

    {
      assume "s'∉Domain R"
      with less.prems have "(x,s')∈A_rel R" by (blast intro: A_rel_base)
    } moreover {
      assume "s'∈Domain R"
      then obtain st where "(s',st)∈R" by (unfold Domain_def, auto)
      with less.prems less.IH obtain sf where "(s',sf)∈A_rel R" by blast
      with less.prems have "(x,sf)∈A_rel R" by (blast intro: A_rel_step)
      hence "∃sf. (x,sf)∈A_rel R" by blast
    } ultimately show "∃sf. (x,sf)∈A_rel R" by blast
  qed
  hence "Domain R ⊆ Domain (A_rel R)" by (unfold Domain_def, auto)
  with dom_subset show ?thesis by force 
qed
  
subsection ‹ Refinement ›
text ‹
  Refinement is a simulation property between step relations.

  We define refinement w.r.t. an abstraction relation @{text "α"}, that relates abstract to concrete states. The refining step-relation is called more concrete than the refined one.
›

definition refines :: "('s*'s) set ⇒ ('r*'s) set ⇒ ('r*'r) set ⇒ bool" ("_≤⇘_⇙_" [50,50,50] 50) where
  "R ≤⇘α⇙ S == α O R ⊆ S O α ∧ α `` Domain S ⊆ Domain R"

lemma refinesI: "⟦α O R ⊆ S O α; α `` Domain S ⊆ Domain R⟧ ⟹ R≤⇘α⇙S" by (unfold refines_def, auto)
lemma refinesE: "R≤⇘α⇙S ⟹ α O R ⊆ S O α"
  "R≤⇘α⇙S ⟹ α `` Domain S ⊆ Domain R" 
  by (unfold refines_def, auto)

text ‹ Intuitively, the first condition for refinement means, that for each concrete step 
  @{text "(c,c')∈S"} where the start state @{text c} has an abstract counterpart @{text "(a,c)∈α"}, 
  there is also an abstract counterpart of the end state @{text "(a',c')∈α"} and 
  the step can also be done on the abstract counterparts @{text "(a,a')∈R"}.
›
lemma refines_compI:
  assumes A: "!! a c c'.  ⟦ (a,c)∈α; (c,c')∈S  ⟧ ⟹ ∃a'. (a,a')∈R ∧ (a',c')∈α"
  shows "α O S ⊆ R O α" using A by blast

lemma refines_compE: "⟦α O S ⊆ R O α; (a,c)∈α; (c,c')∈S⟧ ⟹ ∃a'. (a,a')∈R ∧ (a',c')∈α" by (auto)

text ‹ Intuitively, the second condition for refinement means, that if there is an abstract step @{text "(a,a')∈R"}, where the start state has a concrete counterpart @{text c},
  then there must also be a concrete step from @{text c}. Note that this concrete step is not required to lead to the concrete counterpart of @{text a'}. In fact, it is only
  important that there is such a concrete step, ensuring that the concrete algorithm will not terminate on states on that the abstract algorithm continues execution.
›
lemma refines_domI: 
  assumes A: "!! a a' c. ⟦(a,c)∈α; (a,a')∈R ⟧ ⟹ c∈Domain S"
  shows "α `` Domain R ⊆ Domain S" using A by auto

lemma refines_domE: "⟦α `` Domain R ⊆ Domain S; (a,c)∈α; (a,a')∈R⟧ ⟹ c∈Domain S" by auto

lemma refinesI2: 
  assumes A: "!! a c c'.  ⟦ (a,c)∈α; (c,c')∈S  ⟧ ⟹ ∃a'. (a,a')∈R ∧ (a',c')∈α"
  assumes B: "!! a a' c. ⟦(a,c)∈α; (a,a')∈R ⟧ ⟹ c∈Domain S"
  shows "S≤⇘α⇙R" by (simp only: refinesI A refines_compI B refines_domI)

lemma refinesE2: 
  "⟦S≤⇘α⇙R; (a,c)∈α; (c,c')∈S⟧ ⟹ ∃a'. (a,a')∈R ∧ (a',c')∈α" 
  "⟦S≤⇘α⇙R; (a,c)∈α; (a,a')∈R⟧ ⟹ c∈Domain S"
  by (blast dest: refinesE refines_compE refines_domE)+

text ‹ Reflexivity of identity refinement›
lemma refines_id_refl[intro!, simp]: "R≤⇘Id⇙R" by (auto intro: refinesI)

text ‹ Transitivity of refinement ›
lemma refines_trans: assumes R: "R ≤⇘α⇙ S"   "S ≤⇘β⇙ T" shows "R≤⇘β O α⇙T"
proof (rule refinesI)
  {
    fix s s' t'
    assume A: "(s,s')∈β O α" "(s',t')∈R"
    then obtain sh where "(s,sh)∈β ∧ (sh,s')∈α" by (blast)
    with A R obtain t th where "(sh,th)∈S ∧ (th,t')∈α ∧ (s,t)∈T ∧ (t,th)∈β" by (blast dest: refinesE)
    hence "(s,t')∈T O (β O α)" by blast
  } thus "(β O α) O R ⊆ T O (β O α)" by blast
next
  {
    fix s s'
    assume A: "s∈Domain T" "(s,s')∈β O α"
    then obtain sh where "(s,sh)∈β ∧ (sh,s')∈α" by blast
    (*with R A have "sh∈Domain S" by (blast dest!: refinesE)*)
    with R A have "s'∈Domain R" by (blast dest!: refinesE)
  } thus "(β O α) `` Domain T ⊆ Domain R" by (unfold Domain_def, blast)
qed

text ‹ Property transfer lemma ›
lemma refines_A_rel[rule_format]:
  assumes R: "R≤⇘α⇙S" and A: "(r,r')∈A_rel R" "(s,r)∈α"
  shows "(∃s'. (s',r')∈α ∧ (s,s')∈A_rel S)"
  using A
proof (induction arbitrary: s)
  case 1: (A_rel_base r r' s)
  assume C: "(r,r')∈R" "r'∉Domain R" "(s,r)∈α"
  with R obtain s' where "(s,s')∈S ∧ (s',r')∈α ∧ s'∉Domain S" by (blast dest: refinesE)
  hence "(s',r')∈α ∧ (s,s')∈A_rel S" by (blast intro: A_rel_base)
  thus "∃s'. (s',r')∈α ∧ (s,s')∈A_rel S" by (blast)
next
  case C: (A_rel_step r rh r')
  assume A: "(r,rh)∈R" "(rh,r')∈A_rel R" "(s,r)∈α"
  with R obtain sh where STEP: "(sh,rh)∈α ∧ (s,sh)∈S" by (blast dest: refinesE)
  with C.IH obtain s' where "(s',r')∈α ∧ (sh,s')∈A_rel S" by blast
  with STEP have "(s', r') ∈ α ∧ (s, s') ∈ A_rel S" by (blast intro: A_rel_step)
  thus "∃s'. (s', r') ∈ α ∧ (s, s') ∈ A_rel S" by (blast)
qed  
  

text ‹ Property transfer lemma for single-valued abstractions (i.e. abstraction functions) ›
lemma refines_A_rel_sv: "⟦R≤⇘α⇙S; (r,r')∈A_rel R; single_valued (α¯); (s,r)∈α; (s',r')∈α⟧ ⟹ (s,s')∈A_rel S" by (blast dest: single_valuedD refines_A_rel)


subsection ‹ Extension to reflexive states ›
text ‹ 
  Up to now we only defined how to relate initial states to terminating states if the algorithm makes at least one step. 
  In this section, we also add the reflexive part: Initial states for that no steps can be made are mapped to themselves.  
›
definition
  "ndet_algo R == (A_rel R) ∪ {(s,s) | s. s∉Domain R}"

lemma ndet_algo_A_rel: "⟦x∈Domain R; (x,y)∈ndet_algo R⟧ ⟹ (x,y)∈A_rel R" by (unfold ndet_algo_def) auto

lemma ndet_algoE: "⟦(s,s')∈ndet_algo R; ⟦(s,s')∈A_rel R⟧ ⟹ P; ⟦ s=s'; s∉Domain R⟧ ⟹ P⟧ ⟹ P" by (unfold ndet_algo_def, auto)
lemma ndet_algoE': "⟦(s,s')∈ndet_algo R; ⟦(s,s')∈A_rel R; s∈Domain R; s'∉Domain R⟧ ⟹ P; ⟦ s=s'; s∉Domain R⟧ ⟹ P⟧ ⟹ P"
  using dom_subset[of R] termstate[of s s' R]
  by (auto elim!: ndet_algoE)

text ‹ @{text "ndet_algo"} is total (i.e. the algorithm is defined for every initial state), if @{text "R¯"} is well founded ›
lemma ndet_algo_total: "wf (R¯) ⟹ Domain (ndet_algo R) = UNIV" 
  by (unfold ndet_algo_def) (auto simp add: wf_dom_eq)

text ‹ The result of the algorithm is always a terminating state ›
lemma termstate_ndet_algo: "(s,s')∈ndet_algo R ⟹ s'∉Domain R" by (unfold ndet_algo_def, auto dest: termstate) 
  
text ‹ Property transfer lemma for @{text ndet_algo} ›
lemma refines_ndet_algo[rule_format]:
  assumes R: "S≤⇘α⇙R" and A: "(c,c')∈ndet_algo S"
  shows "∀a. (a,c)∈α ⟶ (∃a'. (a',c')∈α ∧ (a,a')∈ndet_algo R)"
proof (intro allI impI)
  fix a assume B: "(a,c)∈α"
  { assume CASE: "c∈Domain S"
    with A have "(c,c')∈A_rel S" by (blast elim: ndet_algoE)
    with R B obtain a' where "(a',c')∈α ∧ (a,a')∈A_rel R" by (blast dest: refines_A_rel)
    moreover hence "(a,a')∈ndet_algo R" by (unfold ndet_algo_def, simp)
    ultimately have "∃a'. (a', c') ∈ α ∧ (a, a') ∈ ndet_algo R" by blast
  } moreover {
    assume CASE: "c∉Domain S"
    with A have "c=c'" by (blast elim: ndet_algoE')
    moreover have "a∉Domain R" proof
      assume "a∈Domain R"
      with B R have "c∈Domain S" by (auto elim: refinesE2)
      with CASE show "False" ..
    qed
    ultimately have "∃a'. (a', c') ∈ α ∧ (a, a') ∈ ndet_algo R" using B by (unfold ndet_algo_def, blast)
  } ultimately show "∃a'. (a', c') ∈ α ∧ (a, a') ∈ ndet_algo R" by blast
qed

text ‹ Property transfer lemma for single-valued abstractions (i.e. Abstraction functions) ›
lemma refines_ndet_algo_sv: "⟦S≤⇘α⇙R; (c,c')∈ndet_algo S; single_valued (α¯); (a,c)∈α; (a',c')∈α⟧ ⟹ (a,a')∈ndet_algo R" by (blast dest: single_valuedD refines_ndet_algo)

subsection ‹ Well-foundedness ›

lemma wf_imp_minimal: "⟦wf S; x∈Q⟧ ⟹ ∃z∈Q. (∀x. (x,z)∈S ⟶ x∉Q)" by (auto iff add: wf_eq_minimal)

text ‹ This lemma allows to show well-foundedness of a refining relation by providing a well-founded refined relation for each element
  in the domain of the refining relation.
›
lemma refines_wf:
  assumes A: "!!r. ⟦ r∈Domain R ⟧ ⟹ (s r,r)∈α r ∧ R≤⇘α r ⇙S r ∧ wf ((S r)¯)"
  shows "wf (R¯)"
proof (rule wfI_min)    
  fix Q and e :: 'a
  assume NOTEMPTY: "e∈Q"
  moreover {
    assume "e∉Domain R"
    hence "∀y. (e,y)∈R ⟶ y∉Q" by blast
  } moreover {
    assume C: "e∈Domain R"
    with A have MAP: "(s e,e)∈α e" and REF: "R≤⇘α e⇙ S e" and  WF: "wf ((S e)¯)" by (auto)
    let ?aQ = "((α e)¯) `` Q"
    from MAP NOTEMPTY have "s e∈?aQ" by auto
    with WF wf_imp_minimal[of "(S e)¯", simplified] have "∃z∈?aQ. (∀x. (z,x)∈S e ⟶ x∉?aQ)" by auto
    then obtain z where ZMIN: "z∈?aQ ∧ (∀x. (z,x)∈S e ⟶ x∉?aQ)" by blast 
    then obtain q where QP: "(z,q)∈α e ∧ q∈Q" by blast
    have "∀x. (q,x)∈R ⟶ x∉Q" proof (intro allI impI)
      fix x
      assume "(q,x)∈R"
      with REF QP obtain xt where ZREF: "(z,xt)∈S e ∧ (xt,x)∈α e" by (blast dest: refinesE)
      with ZMIN have "xt∉?aQ" by simp
      moreover from ZREF have "x∈Q ⟹ xt∈?aQ" by blast
      ultimately show "x∉Q" by blast
    qed
    with QP have "∃q∈Q. ∀y. (q,y)∈R ⟶ y∉Q" by blast
  } ultimately show "∃z∈Q. ∀y. (y,z)∈R¯ ⟶ y∉Q" by blast
qed

subsubsection ‹ The relations @{text ">"} and @{text "⊃"} on finite domains ›
definition "greaterN N == {(i,j) . j<i & i≤(N::nat)}"
definition "greaterS S == {(a,b) . b⊂a & a⊆(S::'a set)}"

text ‹ @{text ">"} on initial segment of nat is well founded ›
lemma wf_greaterN: "wf (greaterN N)"
  apply (unfold greaterN_def)
  apply (rule wf_subset[of "measure (λk. (N-k))"], blast)
  apply (clarify, simp add: measure_def inv_image_def)
done

text ‹ Strict version of @{thm [source] card_mono} ›
lemma card_mono_strict: "⟦finite B; A⊂B⟧ ⟹ card A < card B" proof - 
  assume F: "finite B" and S: "A⊂B"
  hence FA: "finite A" by (auto intro: finite_subset)
  from S obtain x where P: "x∈B ∧ x∉A ∧ A-{x}=A ∧ insert x A ⊆ B" by auto
  with FA have "card (insert x A) = Suc (card A)" by (simp)
  moreover from F P have "card (insert x A) ≤ card B" by (fast intro: card_mono)
  ultimately show ?thesis by simp
qed  

text ‹ @{text "⊃"} on finite sets is well founded ›
text ‹ This is shown here by embedding the @{text "⊃"} relation into the @{text ">"} relation, using cardinality ›
lemma wf_greaterS: "finite S ⟹ wf (greaterS S)" proof -
  assume FS: "finite S" ― ‹ For this purpose, we show that we can embed greaterS into the greaterN by the inverse image of cardinality ›
  have "{(a,b) . b⊂a ∧ a ⊆ S} ⊆ inv_image (greaterN (card S)) card" proof -
    { (* Show the necessary per-element proposition *)
      fix a b
      assume A: "b⊂a" "a⊆S"
      with FS have Fab: "finite a" "finite b" by (auto simp add: finite_subset)
      with A FS have "card b < card a & card a ≤ card S" by (fast intro: card_mono card_mono_strict)
    } note R=this
    thus ?thesis by (auto simp add: inv_image_def greaterN_def)
  qed
  thus ?thesis by (unfold greaterS_def, blast intro: wf_greaterN wf_subset)
qed

text ‹ This lemma shows well-foundedness of saturation algorithms, where in each step some set is increased, and this set remains below some finite upper bound ›
lemma sat_wf:
  assumes subset: "!!r r'. (r,r')∈R ⟹ α r ⊂ α r' ∧ α r' ⊆ U"
  assumes finite: "finite U"
  shows "wf (R¯)"
proof -
  have "R¯ ⊆ inv_image (greaterS U) α" by (auto simp add: inv_image_def greaterS_def dest: subset)
  moreover have "wf (inv_image (greaterS U) α)" using finite by (blast intro: wf_greaterS)
  ultimately show ?thesis by (blast intro: wf_subset)
qed

subsection ‹ Implementation ›
text ‹
  The first step to implement a nondeterministic algorithm specified by a relation @{text "R"} is to provide a deterministic refinement w.r.t. the identity abstraction @{text "Id"}. 
  We can describe such a deterministic refinement as the graph of a partial function @{text "sel"}. We call this function a selector function, 
  because it selects the next state from the possible states specified by @{text "R"}.

  In order to get a working implementation, we must prove termination. That is, we have to show that @{text "(graph sel)¯"} is well-founded. 
  If we already know that @{text "R¯"} is well-founded, this property transfers to @{text "(graph sel)¯"}.

  Once obtained well-foundedness, we can use the selector function to implement the following recursive function:

    @{text "algo s = case sel s of None ⇒ s | Some s' ⇒ algo s'"}

  And we can show, that @{text "algo"} is consistent with @{text "ndet_algo R"}, that is @{text "(s,algo s)∈ndet_algo R"}.
›

subsubsection "Graphs of functions"
text ‹ The graph of a (partial) function is the relation of arguments and function values ›
definition "graph f == {(x,x') . f x = Some x'}"

lemma graphI[intro]: "f x = Some x' ⟹ (x,x')∈graph f" by (unfold graph_def, auto)
lemma graphD[dest]: "(x,x')∈graph f ⟹ f x = Some x'" by (unfold graph_def, auto)
lemma graph_dom_iff1: "(x∉Domain (graph f)) = (f x = None)" by (cases "f x") auto
lemma graph_dom_iff2: "(x∈Domain (graph f)) = (f x ≠ None)" by (cases "f x") auto

subsubsection "Deterministic refinement w.r.t. the identity abstraction"
lemma detRef_eq: "(graph sel ≤⇘Id⇙ R) = ((∀s s'. sel s = Some s' ⟶ (s,s')∈R) ∧ (∀s. sel s = None ⟶ s∉Domain R))"
  by (unfold refines_def) (auto iff add: graph_dom_iff2)

lemma detRef_wf_transfer: "⟦wf (R¯); graph sel ≤⇘Id⇙ R ⟧ ⟹ wf ((graph sel)¯)"
  by (rule refines_wf[where s=id and α="λx. Id" and S="λx. R"]) simp

subsubsection "Recursive characterization"

locale detRef_impl =
  fixes algo and sel and R
  assumes detRef: "graph sel ≤⇘Id⇙ R" 
  assumes algo_rec[simp]: "!! s s'. sel s = Some s' ⟹ algo s = algo s'" and algo_term[simp]: "!! s. sel s = None ⟹ algo s = s"
  assumes wf: "wf ((graph sel)¯)"

lemma (in detRef_impl) sel_cons: 
  "sel s = Some s' ⟹ (s,s')∈R"
  "sel s = None ⟹ s∉Domain R"
  "s∈Domain R ⟹ ∃s'. sel s = Some s'"
  "s∉Domain R ⟹ sel s = None"
  using detRef 
  by (simp_all only: detRef_eq) (cases "sel s", blast, blast)+

lemma (in detRef_impl) algo_correct: "(s,algo s)∈ndet_algo R" proof -
  {
    assume C: "s∈Domain R"
    have "!!s. s∈Domain R ⟶ (s,algo s)∈A_rel R" 
    proof (rule wf_induct[OF wf, of "λs. s∈Domain R ⟶ (s,algo s)∈A_rel R"]; intro impI)
      fix s
      assume A: "s ∈ Domain R" and IH: "∀y. (y, s) ∈ (graph sel)¯ ⟶ y ∈ Domain R ⟶ (y, algo y) ∈ A_rel R"
      then obtain sh where SH: "sel s = Some sh ∧ (s,sh)∈R" using sel_cons by blast
      hence AS: "algo s = algo sh" by auto
      {
        assume C: "sh∉Domain R"
        hence "sel sh=None" by (auto dest: sel_cons)
        hence "algo sh=sh" by (auto)
        moreover from SH C have "(s,sh)∈A_rel R" by (blast intro: A_rel_base) 
        ultimately have "(s,algo s)∈A_rel R" using AS by simp
      } moreover {
        assume C: "sh∈Domain R"
        with SH IH AS A have "(sh,algo s)∈A_rel R" by auto
        with SH have "(s,algo s)∈A_rel R" by (blast intro: A_rel_step)
      } ultimately show "(s,algo s)∈A_rel R" by blast
    qed
    with C have "(s,algo s)∈A_rel R" by simp
    hence ?thesis by (unfold ndet_algo_def, auto)
  } moreover {
    assume C: "s∉Domain R"
    hence "s=algo s" by (auto dest: sel_cons)
    with C have ?thesis by (unfold ndet_algo_def, auto)
  } ultimately show ?thesis by blast
qed
   

end