Theory Invariants_To_Assertions

theory Invariants_To_Assertions
  imports 
    Cooperation_Program
begin

context lts
begin

definition change_assertion where
  "change_assertion P A = ⦇ lts.initial = lts.initial P, transition_rules = transition_rules P, assertion = A ⦈"

lemma invariants_to_assertion_reachable_states:
  assumes inv: "invariants P Φ"
  and A: "⋀ l. assertion P l ∧⇩f Φ l ⟹⇩f A l" "⋀ l. formula (A l)"
  shows "reachable_states P ⊆ reachable_states (change_assertion P A)" (is "?l ⊆ ?r")
proof(intro subsetI)
  note inv = invariantD[OF invariantsD[OF inv]]
  fix s assume "s ∈ ?l"
  then obtain n where "s ∈ ((transition P)^^n) `` initial_states P" by fast
  then show "s ∈ ?r"
  proof (induct n arbitrary: s)
    case 0
    then have reach: "s ∈ reachable_states P" by auto
    obtain l α where s[simp]: "s = State α l" by (cases s, auto)
    with 0 have "l ∈ lts.initial P" "α ⊨ assertion P l" and α: "assignment α" by (auto simp: initial_states_def)
    with impliesD[OF A(1) α, of l] inv[OF reach[unfolded s]] A(2)
    have "s ∈ initial_states (change_assertion P A)" by (auto simp: change_assertion_def initial_states_def)
    then show ?case by (auto simp: change_assertion_def initial_states_def)
  next
    case (Suc n)
    then obtain t where tPn: "t ∈ ((transition P)^^n) `` initial_states P" and tsP: "(t,s) ∈ transition P" by auto
    obtain l α where t: "t = State α l" by (cases t, auto)
    obtain r β where s: "s = State β r" by (cases s, auto)
    from tPn have tP: "t ∈ ?l" by (auto simp: rtrancl_is_UN_relpow)
    from reachable_state[OF tP] t have Pl: "α ⊨ assertion P l" and α: "assignment α" by auto
    from inv[OF tP[unfolded t]] impliesD[OF A(1) α, of l] tP Pl have Al: "α ⊨ A l" by auto
    from rtrancl_image_advance[OF tP tsP] have sP: "s ∈ ?l".
    from reachable_state[OF sP] s have Pr: "β ⊨ assertion P r" and β: "assignment β" by auto
    from inv[OF sP[unfolded s]] impliesD[OF A(1) β, of r] sP Pr have Ar: "β ⊨ A r" by auto
    from tsP obtain τ where "τ ∈ transition_rules P" "(t,s) ∈ transition_step_lts P τ" by (auto simp: transition_def)
    with α β Al Ar have "(t,s) ∈ transition (change_assertion P A)" by (auto simp: change_assertion_def s t)
    with rtrancl_image_advance[OF Suc(1)[OF tPn]]
    show ?case by auto
  qed
qed

lemma invariants_to_assertion: assumes inv: "invariants P Φ"
  and SN: "cooperation_SN Q"
  and J: "⋀ l. assertion P l ∧⇩f Φ l ⟹⇩f Ψ l" "⋀ l. formula (Ψ l)" 
  and Q: "Q = ⦇ lts.initial = lts.initial P, transition_rules = transition_rules P, assertion = Ψ ⦈" (is "_ = ?Q")
shows "cooperation_SN P"
proof -
  have "flat_transitions_of P ∪ sharp_transitions_of P = transition_rules P" 
    by auto
  then have id: "(⋃ (transition_step_lts P ` (flat_transitions_of P ∪ sharp_transitions_of P)))⇧* `` initial_states P
    = reachable_states P" 
    unfolding transition_def by simp
  {
    fix s
    assume reach: "s ∈ reachable_states P"
    obtain l α where s: "s = State α l" by (cases s, auto)
    from reachable_state[OF reach]
    have al: "α ⊨ assertion P l" and aP: "valuation s ⊨ assertion P (location s)" 
      and v: "assignment (valuation s)" 
      by (auto simp: s)
    from inv reach[unfolded s] s
    have "valuation s ⊨ Φ (location s)" by auto
    from impliesD[OF J(1) v] this aP J(2)[of "location s"]
    have "valuation s ⊨ Ψ (location s)" "formula (Ψ (location s))" by auto
  } note J = this
  {
    fix g
    let ?PS = "{ τ ∈ transition_rules P. g τ }" 
    let ?QS = "{ τ ∈ transition_rules ?Q. g τ }" 
    fix a b1 b2
    assume a: "a ∈ ?PS" and step: "(b1, b2) ∈ transition_step_lts P a" 
      and reach: "b1 ∈ reachable_states P" "b2 ∈ reachable_states P"
    note J = J[OF reach(1)] J[OF reach(2)]
    from J step 
    have "(b1, b2) ∈ transition_step (λs. state s ∧ valuation s ⊨ Ψ (location s)) a" by (cases b1; cases b2, cases a, auto)
    with a have "a ∈ ?QS ∧ (b1, b2) ∈ transition_step_lts ?Q a" by auto
  } note main = this
  {
    fix s
    assume s: "s ∈ initial_states P" 
    then have "s ∈ reachable_states P" by auto
    from J[OF this] s have "s ∈ initial_states ?Q" unfolding initial_states_def by auto
  }
  then have init:  "(λx. x) ` initial_states P ⊆ initial_states ?Q" by auto
  show "cooperation_SN P" 
    by (rule cooperation_SN_on_simulation[OF _ _ _ SN[unfolded Q], of "λ x. x" _ _ _ _ "λ x. x"], 
    unfold id, rule init, (rule main, auto)[1], (rule main, auto)[1])
qed

lemma invariants_to_assertion_lts: assumes inv: "invariants P Φ"
  and SN: "lts_termination Q"
  and J: "⋀ l. assertion P l ∧⇩f Φ l ⟹⇩f J l" "⋀ l. formula (J l)" 
  and Q: "Q = ⦇ lts.initial = lts.initial P, transition_rules = transition_rules P, assertion = J ⦈" (is "_ = ?Q")
shows "lts_termination P"
proof 
  {
    fix s
    assume reach: "s ∈ reachable_states P"
    obtain l α where s: "s = State α l" by (cases s, auto)
    from reachable_state[OF reach]
    have al: "α ⊨ assertion P l" and aP: "valuation s ⊨ assertion P (location s)" 
      and v: "assignment (valuation s)" 
      by (auto simp: s)
    from inv reach[unfolded s] s
    have "valuation s ⊨ Φ (location s)" by auto
    from impliesD[OF J(1) v] this aP J(2)[of "location s"]
    have "valuation s ⊨ J (location s)" "formula (J (location s))" by auto
  } note J = this
  {
    fix s
    assume s: "s ∈ initial_states P" 
    then have "s ∈ reachable_states P" by auto
    from J[OF this] s have "s ∈ initial_states ?Q" unfolding initial_states_def by auto
  } note init = this
  fix f
  assume nSN: "f 0 ∈ initial_states P" "∀ i. (f i, f (Suc i)) ∈ transition P" 
  from init[OF nSN(1)] have init: "f 0 ∈ initial_states Q" unfolding Q .
  have *: "(f 0, f i) ∈ (transition P)^*" for i 
  proof (induct i)
    case (Suc i)
    from Suc nSN(2)[rule_format, of i] show ?case by auto
  qed auto
  from nSN(1) have reach: "f i ∈ reachable_states P" for i using *[of i] by auto
  {
    fix i
    from nSN(2)[rule_format, of i, unfolded transition_def]
    obtain r where r: "r ∈ transition_rules P" and step: "(f i, f (Suc i)) ∈ transition_step_lts P r" by auto
    from r have r: "r ∈ transition_rules Q" unfolding Q by auto
    from step have step: "(f i, f (Suc i)) ∈ transition_step_lts Q r" using J[OF reach[of i]] J[OF reach[of "Suc i"]]
      unfolding Q by auto
    with r have "(f i, f (Suc i)) ∈ transition Q" unfolding transition_def by auto
  }
  with init SN show False by auto
qed

definition fix_invariants :: "('f,'v,'t,'l :: showl,'tr :: showl) lts_impl ⇒ ('l ⇒ ('f,'v,'t) exp formula)
  ⇒ showsl + ('f,'v,'t,'l,'tr) lts_impl" where 
  "fix_invariants P Φ = do {
      let ls = nodes_lts_impl P;
      let old = assertion_of P;
      return 
       (Lts_Impl 
         (initial P) 
         (transitions_impl P) 
         (map (λ l. (l, Φ l)) ls))
    } <+? (λ s. showsl_lit (STR ''problem when fixing invariants as assertions⏎'') o s)"

lemma fix_invariants:
  assumes res: "fix_invariants P A = return Q"
  defines "A' ≡ (λl. if l ∈ set (nodes_lts_impl P) then A l else True⇩f)"
  shows "lts_of Q = change_assertion (lts_of P) A'"
proof-
  note res = res[unfolded fix_invariants_def Let_def, simplified]
  define f where "f = (λl. (l, A l))"
  define fm where "fm = map f (nodes_lts_impl P)"
  note res = res[folded f_def fm_def]
  from res have Q: "Q = Lts_Impl (lts_impl.initial P) (transitions_impl P) fm" by auto
  have PQ: "lts_of Q = ⦇lts.initial = lts.initial (lts_of P), transition_rules = transition_rules (lts_of P),
       assertion = map_of_default form_True fm⦈" unfolding Q by (simp add: assertion_of_def)
  also have "map_of_default form_True fm = A'"
    by (rule ext, rule map_of_defaultI2, auto simp: A'_def fm_def f_def)
  finally show ?thesis by (auto simp: change_assertion_def)
qed

lemma fix_invariants_cooperation_SN:
  assumes res: "fix_invariants P Φ = return Q"
      and inv: "invariants (lts_of P) Φ"
      and SN: "cooperation_SN_impl Q"
  shows "cooperation_SN_impl P"
proof
  assume lts: "lts_impl P"
  from lts_impl[OF lts, unfolded lts_def] have lc: "formula (assertion_of P l)" for l by auto
  note res = res[unfolded fix_invariants_def Let_def, simplified]
  define f where "f = (λl. (l, Φ l))"
  from inv have "formula (Φ l)" for l by auto
  then have form: "formula (snd (f l))" for l unfolding f_def
    using lc[of l] lts_impl[OF lts]
    by (auto simp: lts_def)
  have form': "(a,g) = f l ⟹ formula g" for a g l using form[of l] by (cases "f l", auto)
  define fm where "fm = map f (nodes_lts_impl P)"
  note res = res[folded f_def fm_def]
  from res have Q: "Q = Lts_Impl (lts_impl.initial P) (transitions_impl P) fm" by auto
  have PQ: "lts_of Q = ⦇lts.initial = lts.initial (lts_of P), transition_rules = transition_rules (lts_of P),
       assertion = map_of_default form_True fm⦈" unfolding Q by (simp add: assertion_of_def)
  from lts form' have lts: "lts_impl Q" by (auto simp: Q fm_def f_def elim: lts_implE)
  show "indexed_rewriting.cooperation_SN_on (transition_step_lts (lts_of P)) (flat_transitions_of (lts_of P)) (sharp_transitions_of (lts_of P)) (initial_states (lts_of P))"      
  proof (rule invariants_to_assertion[OF inv _ _ _ PQ])
    show "cooperation_SN (lts_of Q)" using SN lts by auto
    fix l
    let ?f = "map_of_default True⇩f fm l" 
    let ?P = "λ f. f = True⇩f ∨ (l ∈ set (nodes_lts_impl P) ∧ f = Φ l)"
    note d = map_of_default_def lookup_default_def lookup_of_alist
    have choice: "?P ?f" 
    proof (cases "map_of fm l")
      case (Some f)
      with map_of_SomeD[OF this]
      show ?thesis unfolding d by (auto simp: fm_def f_def)
    qed (auto simp: d)
    from inv have Il: "formula (Φ l)" by auto
    from choice show "formula (map_of_default True⇩f fm l)"
      by (auto simp: lc Il)
    show "assertion (lts_of P) l ∧⇩f Φ l ⟹⇩f map_of_default True⇩f fm l" 
      using choice by auto
  qed
qed 

lemma fix_invariants_lts:
  assumes res: "fix_invariants P Φ = return Q"
      and inv: "invariants (lts_of P) Φ"
      and SN: "lts_impl Q ⟹ lts_termination (lts_of Q)"
  shows "lts_impl P ⟹ lts_termination (lts_of P)"
proof -
  assume lts: "lts_impl P"
  from lts_impl[OF lts, unfolded lts_def] have lc: "formula (assertion_of P l)" for l by auto
  note res = res[unfolded fix_invariants_def Let_def, simplified]
  define f where "f = (λl. (l, Φ l))"
  from inv have "formula (Φ l)" for l by auto
  then have form: "formula (snd (f l))" for l unfolding f_def
    using lc[of l] lts_impl[OF lts]
    by (auto simp: lts_def)
  have form': "(a,g) = f l ⟹ formula g" for a g l using form[of l] by (cases "f l", auto)
  define fm where "fm = map f (nodes_lts_impl P)"
  note res = res[folded f_def fm_def]
  from res have Q: "Q = Lts_Impl (lts_impl.initial P) (transitions_impl P) fm" by auto
  have PQ: "lts_of Q = ⦇lts.initial = lts.initial (lts_of P), transition_rules = transition_rules (lts_of P),
       assertion = map_of_default form_True fm⦈" unfolding Q by (simp add: assertion_of_def)
  from lts form' have lts: "lts_impl Q" by (auto simp: Q fm_def f_def elim: lts_implE)
  show "lts_termination (lts_of P)" 
  proof (rule invariants_to_assertion_lts[OF inv _ _ _ PQ])
    show "lts_termination (lts_of Q)" using SN lts by auto
    fix l
    let ?f = "map_of_default True⇩f fm l" 
    let ?P = "λ f. f = True⇩f ∨ (l ∈ set (nodes_lts_impl P) ∧ f = Φ l)"
    note d = map_of_default_def lookup_default_def lookup_of_alist
    have choice: "?P ?f" 
    proof (cases "map_of fm l")
      case (Some f)
      with map_of_SomeD[OF this]
      show ?thesis unfolding d by (auto simp: fm_def f_def)
    qed (auto simp: d)
    from inv have Il: "formula (Φ l)" by auto
    from choice show "formula (map_of_default True⇩f fm l)"
      by (auto simp: lc Il)
    show "assertion (lts_of P) l ∧⇩f Φ l ⟹⇩f map_of_default True⇩f fm l" 
      using choice by auto
  qed
qed

lemma fix_invariants_safety:
  assumes res: "fix_invariants P Φ = return Q"
      and inv: "invariants (lts_of P) Φ"
      and safe: "lts_impl Q ⟹ lts_safe (lts_of Q) errs"
  shows "lts_impl P ⟹ lts_safe (lts_of P) errs"
proof(unfold lts_safe_def, intro allI impI)
  assume lts: "lts_impl P"
  from lts_impl[OF lts, unfolded lts_def] have lc: "formula (assertion_of P l)" for l by auto
  note res2 = res[unfolded fix_invariants_def Let_def, simplified]
  define f where "f = (λl. (l, Φ l))"
  from inv have "formula (Φ l)" for l by auto
  then have form: "formula (snd (f l))" for l unfolding f_def
    using lc[of l] lts_impl[OF lts]
    by (auto simp: lts_def)
  have form': "(a,g) = f l ⟹ formula g" for a g l using form[of l] by (cases "f l", auto)
  define fm where "fm = map f (nodes_lts_impl P)"
  note res2 = res2[folded f_def fm_def]
  from res2 have Q: "Q = Lts_Impl (lts_impl.initial P) (transitions_impl P) fm" by auto
  have PQ: "lts_of Q = ⦇lts.initial = lts.initial (lts_of P), transition_rules = transition_rules (lts_of P),
       assertion = map_of_default form_True fm⦈" unfolding Q by (simp add: assertion_of_def)
  from lts form' have "lts_impl Q" by (auto simp: Q fm_def f_def elim: lts_implE)
  note safe = safe[OF this]

  fix l α assume "l ∈ errs"
  with safe[unfolded lts_safe_def] have "State α l ∉ reachable_states (lts_of Q)" by auto
  moreover have "reachable_states (lts_of P) ⊆ reachable_states (lts_of Q)"
    unfolding fix_invariants[OF res]
    apply (rule invariants_to_assertion_reachable_states[OF inv])
    using inv lts by (auto intro: lts_impl_formula_assertion_of)
  ultimately show "State α l ∉ reachable_states (lts_of P)" by auto
qed

end


declare lts.fix_invariants_def[code]

  
end