Theory Executions

section Executions

text ‹This section contains all definitions required for reasoning about executions in the concurrent
  revisions model. It also contains a number of proofs for inductive variants. One of these
  proves the equivalence of the two definitions of the operational semantics. The others are
  required for proving determinacy.›

theory Executions
  imports OperationalSemantics
begin

context substitution
begin

subsection ‹Generalizing the original transition›

subsubsection Definition

definition steps :: "('r,'l,'v) global_state rel" (‹[↝]›) where
  "steps = { (s,s') | s s'. ∃r. revision_step r s s' }"

abbreviation valid_step :: "('r,'l,'v) global_state ⇒ ('r,'l,'v) global_state ⇒ bool" (infix ‹↝› 60) where
  "s ↝ s' ≡ (s,s') ∈ [↝]"

lemma valid_stepI [intro]:
  "revision_step r s s' ⟹ s ↝ s'"
  using steps_def by auto

lemma valid_stepE [dest]:
  "s ↝ s' ⟹ ∃r. revision_step r s s'"
  by (simp add: steps_def)

subsubsection Closures

abbreviation refl_trans_step_rel :: "('r,'l,'v) global_state ⇒ ('r,'l,'v) global_state ⇒ bool"(infix ‹↝⇧^*› 60) where
  "s ↝⇧^* s' ≡ (s,s') ∈ [↝]⇧^*"

abbreviation refl_step_rel :: "('r,'l,'v) global_state ⇒ ('r,'l,'v) global_state ⇒ bool" (infix ‹↝⇧⁼› 60) where
  "s ↝⇧⁼ s' ≡ (s,s') ∈ [↝]⇧⁼"

lemma refl_rewritesI [intro]: "s ↝ s' ⟹ s ↝⇧⁼ s'" by blast

subsection Properties

abbreviation program_expr :: "('r,'l,'v) expr ⇒ bool" where
  "program_expr e ≡ LID⇩_E e = {} ∧ RID⇩_E e = {}"

abbreviation initializes :: "('r,'l,'v) global_state ⇒ ('r,'l,'v) expr ⇒ bool" where
  "initializes s e ≡ ∃r. s = (ε(r ↦(ε,ε,e))) ∧ program_expr e"

abbreviation initial_state :: "('r,'l,'v) global_state ⇒ bool" where
  "initial_state s ≡ ∃e. initializes s e"

definition execution :: "('r,'l,'v) expr ⇒ ('r,'l,'v) global_state ⇒ ('r,'l,'v) global_state ⇒ bool" where
  "execution e s s' ≡ initializes s e ∧ s ↝⇧^* s'"

definition maximal_execution :: "('r,'l,'v) expr ⇒ ('r,'l,'v) global_state ⇒ ('r,'l,'v) global_state ⇒ bool" where
  "maximal_execution e s s' ≡ execution e s s' ∧ (∄s''. s' ↝ s'')"

definition reachable :: "('r,'l,'v) global_state ⇒ bool" where
  "reachable s ≡ ∃e s'. execution e s' s"

definition terminates_in :: "('r,'l,'v) expr ⇒ ('r,'l,'v) global_state ⇒ bool" (infix ‹↓› 60) where
  "e ↓ s' ≡ ∃s. maximal_execution e s s'"

subsection Invariants

subsubsection ‹Inductive invariance›

definition inductive_invariant :: "(('r,'l,'v) global_state ⇒ bool) ⇒ bool" where
  "inductive_invariant P ≡ (∀s. initial_state s ⟶ P s) ∧ (∀s s'. s ↝ s' ⟶ P s ⟶ P s')"

lemma inductive_invariantI [intro]:
  "(⋀s. initial_state s ⟹ P s) ⟹ (⋀s s'. s ↝ s' ⟹ P s ⟹ P s') ⟹ inductive_invariant P"
  by (auto simp add: inductive_invariant_def)

lemma inductive_invariant_is_execution_invariant: "reachable s ⟹ inductive_invariant P ⟹ P s"
proof -
  assume reach: "reachable s" and ind_inv: "inductive_invariant P"
  then obtain e initial n where initializes: "initializes initial e" and trace: "(initial,s) ∈ [↝]^^n"
    by (metis execution_def reachable_def rtrancl_power)
  thus "P s"
  proof (induct n arbitrary: s)
    case 0
    have "initial = s"   using "0.prems"(2) by auto
    hence "initial_state s" using initializes by blast
    then show ?case using ind_inv inductive_invariant_def by auto
  next
    case (Suc n)
    obtain s' where nfold: "(initial, s') ∈ [↝]^^n" and step: "s' ↝ s" using Suc.prems(2) by auto
    have "P s'" using Suc(1) nfold initializes by blast
    then show ?case using ind_inv step inductive_invariant_def by auto
  qed
qed

subsubsection ‹Subsumption is invariant›

lemma nice_ind_inv_is_inductive_invariant: "inductive_invariant (λs. 𝒮⇩_G s ∧ 𝒜⇩_G s)"
proof (rule inductive_invariantI)
  fix s
  assume "initial_state s"
  then obtain e r where s: "s = ε(r ↦ (ε, ε, e))" and prog_expr_e: "program_expr e" by blast
  show "𝒮⇩_G s ∧ 𝒜⇩_G s"
  proof (rule conjI)
    show "𝒮⇩_G s"
    proof (rule domains_subsume_globallyI)
      fix r' σ' τ' e'
      assume s_r': "s r' = Some (σ',τ',e')"
      have "r' = r" using s s_r' prog_expr_e by (meson domI domIff fun_upd_other)
      hence "LID⇩_L (σ',τ',e') = LID⇩_L (ε, ε, e)" using s s_r' by auto
      also have "... = {}" using prog_expr_e by auto
      also have "... = dom σ' ∪ dom τ'" using ‹r' = r› s s_r' by auto
      finally show "𝒮 (σ', τ', e')" by (simp add: domains_subsume_def)
    qed
    show "𝒜⇩_G s"
    proof (rule subsumes_accessible_globallyI)
      fix r⇩₁ σ⇩₁ τ⇩₁ e⇩₁ r⇩₂ σ⇩₂ τ⇩₂ e⇩₂
      assume s_r1: "s r⇩₁ = Some (σ⇩₁, τ⇩₁, e⇩₁)" and s_r2: "s r⇩₂ = Some (σ⇩₂, τ⇩₂, e⇩₂)"
      have "r⇩₂ = r" using s s_r2 prog_expr_e  by (meson domI domIff fun_upd_other)
      hence "σ⇩₂ = ε" using s s_r2 by auto
      hence "LID⇩_S σ⇩₂ = {}" by auto
      thus "𝒜 r⇩₁ r⇩₂ s" using s_r2 by auto
    qed
  qed
qed (use step_preserves_𝒮⇩_G_and_𝒜⇩_G in auto)

corollary reachable_imp_𝒮⇩_G: "reachable s ⟹ 𝒮⇩_G s"
proof -
  assume reach: "reachable s"
  have "𝒮⇩_G s ∧ 𝒜⇩_G s" by (rule inductive_invariant_is_execution_invariant[OF reach nice_ind_inv_is_inductive_invariant]) 
  thus ?thesis by auto
qed

lemma transition_relations_equivalent: "reachable s ⟹ revision_step r s s' = revision_step_relaxed r s s'"
proof -
  assume reach: "reachable s"
  have doms_sub_local: "𝒮⇩_G s" by (rule reachable_imp_𝒮⇩_G[OF reach])
  show "revision_step r s s' = revision_step_relaxed r s s'"
  proof (rule iffI)
    assume step: "revision_step r s s'"
    show "revision_step_relaxed r s s'"
    proof (use step in ‹induct rule: revision_stepE›)
      case (new σ τ ℰ v l)
      have "revision_step_relaxed r s (s(r ↦ (σ, τ(l ↦ v), ℰ [VE (Loc l)])))"
      proof (rule revision_step_relaxed.new)
        show "l ∉ ⋃ { doms ls | ls. ls ∈ ran s}"
        proof 
          assume "l ∈ ⋃ { doms ls | ls. ls ∈ ran s}"
          then obtain ls where in_ran: "ls ∈ ran s" and in_doms: "l ∈ doms ls" by blast
          from in_doms have "l ∈ LID⇩_L ls" by (cases ls) auto
          have "l ∈ LID⇩_G s"
          proof -
            have "ls ∈ {ls. ∃r. s r = Some ls}" by (metis (full_types) in_ran ran_def)
            then show ?thesis using ‹l ∈ LID⇩_L ls› by blast
          qed
          thus False using new by auto
        qed
      qed (simp add: new.hyps(2))
      thus ?thesis using new.hyps(1) by blast
    qed (use revision_step_relaxed.intros in simp)+
  next
    assume step: "revision_step_relaxed r s s'"
    show "revision_step r s s'"
    proof (use step in ‹induct rule: revision_step_relaxedE›)
      case (new σ τ ℰ v l)
      have "revision_step r s (s(r ↦ (σ, τ(l ↦ v), ℰ [VE (Loc l)])))"
      proof (rule revision_step.new)
        show "s r = Some (σ, τ, ℰ [Ref (VE v)])" by (simp add: new.hyps(2))
        show "l ∉ LID⇩_G s"
        proof
          assume "l ∈ LID⇩_G s"
          then obtain r' σ' τ' e' where s_r': "s r' = Some (σ',τ',e')" and l_in_local: "l ∈ LID⇩_L (σ',τ',e')" by auto
          hence "l ∈ dom σ' ∪ dom τ'"
            by (metis (no_types, lifting) domains_subsume_def domains_subsume_globally_def doms.simps doms_sub_local rev_subsetD)
          thus False by (meson s_r' new.hyps(3) ranI)
        qed
      qed
      then show ?case using new.hyps(1) by blast
    next
      case (get σ τ ℰ l)
      have "revision_step r s (s(r ↦ (σ, τ, ℰ [VE (the ((σ;;τ) l))])))"
      proof 
       show "s r = Some (σ, τ, ℰ [Read (VE (Loc l))])" by (simp add: get.hyps(2))
       show "l ∈ dom (σ;;τ)"
       proof -
         have "l ∈ LID⇩_L (σ, τ, ℰ [Read (VE (Loc l))])"  by simp
         hence "l ∈ dom σ ∪ dom τ"
           using domains_subsume_def domains_subsume_globally_def doms_sub_local get.hyps(2) by fastforce
         thus "l ∈ dom (σ;;τ)" by (simp add: dom_combination_dom_union)
       qed
     qed
     then show ?case using get.hyps(1) by auto
    next
      case (set σ τ ℰ l v)
      have "revision_step r s (s(r ↦ (σ, τ(l ↦ v), ℰ [VE (CV Unit)])))"
      proof 
       show "s r = Some (σ, τ, ℰ [Assign (VE (Loc l)) (VE v)])" by (simp add: set.hyps(2))
       show "l ∈ dom (σ;;τ)"
       proof -
         have "l ∈ LID⇩_L (σ, τ, ℰ [Assign (VE (Loc l)) (VE v)])"  by simp
         hence "l ∈ dom σ ∪ dom τ"
           using domains_subsume_def domains_subsume_globally_def doms_sub_local set.hyps(2) by fastforce
         thus "l ∈ dom (σ;;τ)" by (simp add: dom_combination_dom_union)
       qed
     qed
     then show ?case using set.hyps(1) by blast
    qed (simp add: revision_step.intros)+
  qed
qed

subsubsection ‹Finitude is invariant›

lemma finite_occurrences_val_expr [simp]:
  fixes 
    v :: "('r,'l,'v) val" and
    e :: "('r,'l,'v) expr"
  shows
  "finite (RID⇩_V v)"
  "finite (RID⇩_E e)"
  "finite (LID⇩_V v)"
  "finite (LID⇩_E e)"
proof -
  have "(finite (RID⇩_V v) ∧ finite (LID⇩_V v)) ∧ finite (RID⇩_E e) ∧ finite (LID⇩_E e)"
    by (induct rule: val_expr.induct) auto
  thus  
    "finite (RID⇩_V v)"
    "finite (RID⇩_E e)"
    "finite (LID⇩_V v)"
    "finite (LID⇩_E e)"
    by auto
qed

lemma store_finite_upd [intro]:
  "finite (RID⇩_S τ) ⟹ finite (RID⇩_S (τ(l := None)))" 
  "finite (LID⇩_S τ) ⟹ finite (LID⇩_S (τ(l := None)))"
  apply (meson ID_restricted_store_subset_store(1) finite_subset)
  by (simp add: ID_restricted_store_subset_store(2) rev_finite_subset)

lemma finite_state_imp_restriction_finite [intro]: 
  "finite (RID⇩_G s) ⟹ finite (RID⇩_G (s(r := None)))"
  "finite (LID⇩_G s) ⟹ finite (LID⇩_G (s(r := None)))"
proof -
  assume "finite (RID⇩_G s)"
  thus "finite (RID⇩_G (s(r := None)))" by (meson infinite_super ID_restricted_global_subset_unrestricted)
next
  assume fin: "finite (LID⇩_G s)"
  have "LID⇩_G (s(r := None)) ⊆ LID⇩_G s" by auto
  thus "finite (LID⇩_G (s(r := None)))" using fin finite_subset by auto
qed

lemma local_state_of_finite_restricted_global_state_is_finite [intro]: 
  "s r' = Some ls ⟹ finite (RID⇩_G (s(r := None))) ⟹ r ≠ r' ⟹ finite (RID⇩_L ls)"
  "s r' = Some ls ⟹ finite (LID⇩_G (s(r := None))) ⟹ r ≠ r' ⟹ finite (LID⇩_L ls)"
   apply (metis (no_types, lifting) ID_distr_global(1) finite_Un finite_insert fun_upd_triv fun_upd_twist)
  by (metis ID_distr_global(2) finite_Un fun_upd_triv fun_upd_twist)

lemma empty_map_finite [simp]: 
  "finite (RID⇩_S ε)" 
  "finite (LID⇩_S ε)" 
  "finite (RID⇩_G ε)" 
  "finite (LID⇩_G ε)" 
  by (simp add: RID⇩_S_def LID⇩_S_def RID⇩_G_def LID⇩_G_def)+

lemma finite_combination [intro]:
  "finite (RID⇩_S σ) ⟹ finite (RID⇩_S τ) ⟹ finite (RID⇩_S (σ;;τ))"
  "finite (LID⇩_S σ) ⟹ finite (LID⇩_S τ) ⟹ finite (LID⇩_S (σ;;τ))"
  by (meson finite_UnI rev_finite_subset ID_combination_subset_union)+

lemma RID⇩_G_finite_invariant:
  assumes
    step: "revision_step r s s'" and
    fin: "finite (RID⇩_G s)"
shows
    "finite (RID⇩_G s')"
proof (use step in ‹cases rule: revision_stepE›)
  case (join σ τ ℰ r' σ' τ' v)
  hence "r ≠ r'" by auto
  then show ?thesis 
    by (metis (mono_tags, lifting) ID_distr_global(1) ID_distr_local(2) fin finite_Un finite_combination(1) finite_insert finite_occurrences_val_expr(2) finite_state_imp_restriction_finite(1) join local_state_of_finite_restricted_global_state_is_finite(1))
qed (use fin in ‹auto simp add: ID_distr_global_conditional›)

lemma RID⇩_L_finite_invariant:
  assumes
    step: "revision_step r s s'" and
    fin: "finite (LID⇩_G s)"
shows
    "finite (LID⇩_G s')"
proof (use step in ‹cases rule: revision_stepE›)
  case (join σ τ ℰ r' σ' τ' v)
  hence "r ≠ r'" by auto
  then show ?thesis 
    using join assms
    by (metis (mono_tags, lifting) ID_distr_global(2) ID_distr_local(1) fin finite_Un finite_combination(2) finite_occurrences_val_expr(4) finite_state_imp_restriction_finite(2) join local_state_of_finite_restricted_global_state_is_finite(2))
qed (use fin in ‹auto simp add: ID_distr_global_conditional›)
 
lemma reachable_imp_identifiers_finite:
  assumes reach: "reachable s"
  shows 
    "finite (RID⇩_G s)"
    "finite (LID⇩_G s)"
proof -
  from reach obtain e r where exec: "execution e (ε(r ↦ (ε,ε,e))) s" using reachable_def execution_def by auto
  hence prog_exp: "program_expr e" by (meson execution_def)
  obtain n where n_reachable: "(ε(r ↦ (ε,ε,e)), s) ∈ [↝]^^n" using exec by (meson execution_def rtrancl_imp_relpow)
  hence "finite (RID⇩_G s) ∧ finite (LID⇩_G s)"
  proof (induct n arbitrary: s)
    case 0
    hence s: "s = ε(r ↦ (ε, ε, e))" by auto
    hence rid_dom: "dom s = {r}" by auto
    hence rid_ran: "⋃ (RID⇩_L ` ran s) = {}" using s by (auto simp add: prog_exp)
    have rids: "RID⇩_G s = {r}" by (unfold RID⇩_G_def, use rid_dom rid_ran in auto)
    have lid_ran: "⋃ (LID⇩_L ` ran s) = {}" using s by (auto simp add: prog_exp)
    hence lids: "LID⇩_G s = {}" by (unfold LID⇩_G_def, simp)
    thus ?case using rids lids by simp
  next
    case (Suc n)
    then obtain s' where 
      n_steps: "(ε(r ↦ (ε, ε, e)), s') ∈ [↝]^^n" and 
      step: "s' ↝ s" 
      by (meson relpow_Suc_E)
    have fin_rid: "finite (RID⇩_G s')" using Suc.hyps n_steps by blast
    have fin_lid: "finite (LID⇩_G s')" using Suc.hyps n_steps by blast
    thus ?case by (meson RID⇩_G_finite_invariant RID⇩_L_finite_invariant fin_rid local.step valid_stepE)
  qed
  thus "finite (RID⇩_G s)" "finite (LID⇩_G s)" by auto
qed

lemma reachable_imp_identifiers_available:
  assumes 
    "reachable (s :: ('r,'l,'v) global_state)"
  shows 
    "infinite (UNIV :: 'r set) ⟹ ∃r. r ∉ RID⇩_G s"
    "infinite (UNIV :: 'l set) ⟹ ∃l. l ∉ LID⇩_G s"
  by (simp add: assms ex_new_if_finite reachable_imp_identifiers_finite)+

subsubsection ‹Reachability is invariant›

lemma initial_state_reachable:
  assumes "program_expr e"
  shows "reachable (ε(r ↦ (ε,ε,e)))"
proof -
  have "initializes (ε(r ↦ (ε,ε,e))) e" using assms by auto
  hence "execution e (ε(r ↦ (ε,ε,e))) (ε(r ↦ (ε,ε,e)))" by (simp add: execution_def)
  thus ?thesis using reachable_def by blast
qed

lemma reachability_closed_under_execution_step:
  assumes
    reach: "reachable s" and
    step: "revision_step r s s'"
  shows "reachable s'"
proof -
  obtain init e where exec: "execution e init s" using reach reachable_def by blast
  hence init_s:"init ↝⇧^* s" by (simp add: execution_def)
  have s_s': "s ↝ s'" using step by blast 
  have "init ↝⇧^* s'" using init_s s_s' by auto
  hence "execution e init s'" using exec by (simp add: execution_def)
  thus ?thesis using reachable_def by auto
qed

lemma reachability_closed_under_execution: "reachable s ⟹ s ↝⇧^* s' ⟹ reachable s'"
proof -
  assume reach: "reachable s" and "s ↝⇧^* s'"
  then obtain n where "(s, s') ∈ [↝]^^n" using rtrancl_imp_relpow by blast
  thus "reachable s'"
  proof (induct n arbitrary: s')
    case 0
    thus ?case using reach by auto
  next 
    case (Suc n)
    obtain s'' where "(s,s'') ∈ [↝]^^n" "s'' ↝ s'" using Suc.prems by auto
    have "reachable s''" by (simp add: Suc.hyps ‹(s, s'') ∈ [↝]^^n›)
    then show ?case using ‹s'' ↝ s'› reachability_closed_under_execution_step by blast
  qed
qed

end (* substitution locale *)

end (* theory *)