Theory Normalized_Zone_Semantics_Impl_Extra

theory Normalized_Zone_Semantics_Impl_Extra
  imports Normalized_Zone_Semantics_Impl
begin

context Regions
begin

lemma steps_z_norm'_induct[consumes 1, case_names refl step]:
  assumes "A ⊢ ⟨l⇩0, D⇩0⟩ ↝⇩𝒩* ⟨l', D'⟩"
  assumes "P l⇩0 D⇩0"
  assumes "⋀l D l' D' l'' D'' a. A ⊢ ⟨l⇩0, D⇩0⟩ ↝⇩𝒩* ⟨l, D⟩ ⟹ P l D
  ⟹ A ⊢ ⟨l, D⟩ ↝⇘v,n,τ⇙ ⟨l', D'⟩ ⟹ A ⊢ ⟨l', D'⟩ ↝⇘𝒩(↿a)⇙ ⟨l'', D''⟩ ⟹ P l'' D''"
  shows "P l' D'"
  using assms
  apply (induction "(l', D')" arbitrary: l' D' rule: rtranclp_induct)
  apply clarsimp+
  apply (fastforce simp: step_z_norm''_def)
  done

end

context Reachability_Problem
begin

lemma step_z_norm''_cong[cong]:
  "⋀a b c d e f. step_z_norm'' a b c d e f ≡ step_z_norm'' a b c d e f" .

lemma step_z_norm'_cong[cong]:
  "⋀a b c d e f. step_z_norm' a b c d e f ≡ step_z_norm' a b c d e f" .

no_notation comp3  (infixl "∘∘∘" 55)

lemma step_impl_sound'':
  assumes step: "A ⊢⇩I ⟨l,D⟩ ↝⇘n,a⇙ ⟨l',D'⟩"
    and     reachable: "E⇧*⇧* a⇩0 (l, D)"
  shows
    "∃ M'. step_z_norm' (conv_A A) l (curry (conv_M D)) a l' M'
    ∧ [curry (conv_M (FW' (norm_upd D' (k' l') n) n))]⇘v,n⇙ = [M']⇘v,n⇙"
  apply -
  apply (rule step_impl_norm_sound[OF step])
  using canonical_reachable reachable apply (simp only: check_diag_def neutral; blast)
  using valid_dbm_reachable reachable diag_reachable' by auto

lemma reachable_sound:
  assumes "E⇧*⇧* a⇩0 (l', D')"
  shows
    "∃ M'. steps_z_norm' (conv_A A) l⇩0 (curry init_dbm) l' M' ∧ [curry (conv_M D')]⇘v,n⇙ = [M']⇘v,n⇙"
  using assms unfolding E_closure
proof (induction l ≡ "l⇩0" Z ≡ "init_dbm :: int DBM'" _ _ _ _ rule: steps_impl_induct)
  case refl
  show ?case
    apply (rule exI[where x = "curry init_dbm"])
    apply standard
     apply blast
    using RI_zone_equiv[symmetric] RI_init_dbm by fastforce
next
  case (step l' M' l'' M'' a l''' M''')
  from step have reachable: "E⇧*⇧* a⇩0 (l', M')" unfolding E_closure by auto
  note valid = valid_dbm_reachable[OF reachable]
  from step.hyps(2) obtain D' where D':
    "steps_z_norm' (conv_A A) l⇩0 (curry init_dbm) l' D'" "[curry (conv_M M')]⇘v,n⇙ = [D']⇘v,n⇙"
    by auto
  from step_impl_sound'[OF step(3)] canonical_reachable diag_reachable' valid reachable
  obtain D'' where D'':
    "(conv_A A) ⊢ ⟨l', curry (conv_M M')⟩ ↝⇘v,n,τ⇙ ⟨l'', D''⟩" "[curry (conv_M M'')]⇘v,n⇙ = [D'']⇘v,n⇙"
    unfolding check_diag_def neutral by auto
  from valid diag_reachable' canonical_reachable reachable have valid_M'':
    "valid_dbm (curry (conv_M M''))"
    apply -
    apply (rule step_impl_valid_dbm)
       apply (rule step(3))
      apply assumption+
    by auto
  with canonical_reachable diag_reachable' valid reachable
  obtain D''' where D''':
    "step_z_norm' (conv_A A) l'' (curry (conv_M M'')) (↿a) l''' D'''"
    "[curry (conv_M (FW' (norm_upd M''' (k' l''') n) n))]⇘v,n⇙ = [D''']⇘v,n⇙"
    using reachable_wf_dbm step.hyps(3) step_impl_wf_dbm wf_dbm_D
    by (atomize_elim, intro step_impl_norm_sound[OF step(4)]) auto
  from step_z_dbm_equiv'[OF D''(1) D'(2)] obtain M2 where M2:
    "conv_A A ⊢ ⟨l', D'⟩ ↝⇘v,n,τ⇙ ⟨l'', M2⟩" "[D'']⇘v,n⇙ = [M2]⇘v,n⇙"
    by blast
  have "valid_dbm D'" using D'(1) steps_z_norm'_valid_dbm_preservation by blast
  then have valid_M2: "valid_dbm M2" by (rule step_z_valid_dbm'[OF M2(1)])
  from M2 D''(2) have "[curry (conv_M M'')]⇘v,n⇙ = [M2]⇘v,n⇙" by simp
  from step_z_norm_equiv'[OF D'''(1) valid_M'' valid_M2 this] obtain M3 where
    "step_z_norm' (conv_A A) l'' M2 (↿a) l''' M3" "[D''']⇘v,n⇙ = [M3]⇘v,n⇙"
    by blast
  with M2(1) D'(1) D'''(2) show ?case
    by (fastforce simp: step_z_dbm_delay_loc step_z_norm''_def elim: rtranclp.rtrancl_into_rtrancl)
qed

lemma step_impl_complete2:
  assumes step: "conv_A A ⊢ ⟨l, curry (conv_M M)⟩ ↝⇘v,n,a⇙ ⟨l', D⟩"
    and wf_dbm: "wf_dbm M"
  shows "∃ M'. A ⊢⇩I ⟨l, M⟩ ↝⇘n,a⇙ ⟨l', M'⟩ ∧ [curry (conv_M M')]⇘v,n⇙ ⊇ [D]⇘v,n⇙"
  using assms(1) wf_dbm_D[OF assms(2)] by (metis step_impl_complete''_improved subsetI wf_dbm)

lemma reachable_complete:
  assumes "steps_z_norm' (conv_A A) l⇩0 (curry init_dbm) l' M'"
  shows
    "∃ D'. E⇧*⇧* a⇩0 (l', D') ∧ [M']⇘v,n⇙ ⊆ [curry (conv_M D')]⇘v,n⇙"
  using assms unfolding E_closure
proof (induction rule: steps_z_norm'_induct)
  case refl
  show ?case
    by (intro exI conjI) (rule steps_impl.refl, auto)
next
  case (step l' M' l'' M'' l''' M''' a)
  then obtain D' where D':
    "A ⊢⇩I ⟨l⇩0, init_dbm⟩ ↝⇘k',n⇙* ⟨l', D'⟩" "[M']⇘v,n⇙ ⊆ [curry (conv_M D')]⇘v,n⇙"
    by fast
  from step_z_dbm_mono[OF step(2) D'(2)] obtain D'' where D'':
    "conv_A A ⊢ ⟨l', curry (conv_M D')⟩ ↝⇘v,n,τ⇙ ⟨l'', D''⟩"
    "[M'']⇘v,n⇙ ⊆ [D'']⇘v,n⇙"
    by auto
  from step have reachable: "E⇧*⇧* a⇩0 (l', D')" using D'(1) E_closure by blast (* s/h *)
  from step_impl_complete2[OF D''(1) reachable_wf_dbm[OF this]] step obtain D2 where D2:
    "A ⊢⇩I ⟨l', D'⟩ ↝⇘n,τ⇙ ⟨l'', D2⟩" "[D'']⇘v,n⇙ ⊆ [curry (conv_M D2)]⇘v,n⇙"
    by auto
  have "valid_dbm M''" (* s/h *)
    using step(1,2) step_z_valid_dbm' steps_z_norm'_valid_dbm_preservation valid_init_dbm by blast
  have valid3:"valid_dbm (curry (conv_M D2))"
    apply (rule step_impl_valid_dbm[OF D2(1)])
    using valid_dbm_reachable canonical_reachable reachable
    using diag_reachable[OF reachable] diag_conv by (auto intro!: canonical_reachable)
  from step_z_norm_mono'[OF step(3) ‹valid_dbm M''› valid3] D''(2) D2(2) obtain M3 where M3:
    "step_z_norm' (conv_A A) l'' (curry (conv_M D2)) (↿a) l''' M3" "[M''']⇘v,n⇙ ⊆ [M3]⇘v,n⇙"
    by auto
  have canonical: "canonical (curry (conv_M D2)) n ∨ check_diag n D2"
    using step_impl_canonical[OF D2(1) diag_reachable[OF reachable]]
    unfolding check_diag_def neutral by auto
  have diag: "∀i≤n. conv_M D2 (i, i) ≤ 0"
    using step_impl_diag_preservation[OF D2(1) diag_reachable[OF reachable]] diag_conv by auto
  from step_impl_norm_complete''[OF M3(1) valid3 canonical diag] obtain D3 where
    "A ⊢⇩I ⟨l'', D2⟩ ↝⇘n,↿a⇙ ⟨l''', D3⟩ "
    "[M3]⇘v,n⇙ ⊆ [curry (conv_M (FW' (norm_upd D3 (k' l''') n) n))]⇘v,n⇙"
    by auto
  with D'(1) D2 M3(2) show ?case
     by (blast intro: steps_impl.step)
qed

lemma step_impl_mono_reachable:
    assumes "A ⊢⇩I ⟨l,D⟩ ↝⇘n,a⇙ ⟨l',D'⟩"
    and     "wf_dbm D" "wf_dbm M"
    and "[curry (conv_M D)]⇘v,n⇙ ⊆ [curry (conv_M M)]⇘v,n⇙"
  shows "∃ M'. A ⊢⇩I ⟨l, M⟩ ↝⇘n,a⇙ ⟨l', M'⟩ ∧ [curry (conv_M D')]⇘v,n⇙ ⊆ [curry (conv_M M')]⇘v,n⇙"
  proof -
    note prems_D = wf_dbm_D[OF assms(2)]
    note prems_M = wf_dbm_D[OF assms(3)]
    from step_impl_sound'[OF assms(1) prems_D] diag_conv obtain M' where
      "conv_A A ⊢ ⟨l, curry (conv_M D)⟩ ↝⇘v,n,a⇙ ⟨l', M'⟩"
      "[curry (conv_M D')]⇘v,n⇙ = [M']⇘v,n⇙"
      unfolding check_diag_def neutral by auto
    with step_impl_complete2[OF _ assms(3)] step_z_dbm_mono[OF _ assms(4)] show ?thesis by force
  qed

lemma step_impl_norm_mono_reachable:
    assumes "A ⊢⇩I ⟨l,D⟩ ↝⇘n,a⇙ ⟨l',D'⟩"
        and prems_D: "wf_dbm D"
        and prems_M: "wf_dbm M"
    and subs: "[curry (conv_M D)]⇘v,n⇙ ⊆ [curry (conv_M M)]⇘v,n⇙"
    shows
      "∃ M'. A ⊢⇩I ⟨l, M⟩ ↝⇘n,a⇙ ⟨l', M'⟩
      ∧ [curry (conv_M (FW' (norm_upd D' (k' l') n) n))]⇘v,n⇙
      ⊆ [curry (conv_M (FW' (norm_upd M' (k' l') n) n))]⇘v,n⇙"
  proof -
    note prems_D = wf_dbm_D[OF prems_D]
    note prems_M = wf_dbm_D[OF prems_M]
    from step_impl_norm_sound[OF assms(1) prems_D] obtain M' where M':
      "step_z_norm' (conv_A A) l (curry (conv_M D)) a l' M'"
      "[curry (conv_M (FW' (norm_upd D' (k' l') n) n))]⇘v,n⇙ = [M']⇘v,n⇙"
      by auto
    from
      step_z_norm_mono'[OF this(1) prems_D(3) prems_M(3) subs]
      step_impl_norm_complete''[OF _ prems_M(3,1,2)] M'(2)
    show ?thesis by fast
  qed

lemma step_impl_mono_reachable':
    assumes step:
      "A ⊢⇩I ⟨l, D⟩ ↝⇘n,τ⇙ ⟨l', D'⟩"
      "A ⊢⇩I ⟨l', D'⟩ ↝⇘n,↿a⇙ ⟨l'', D''⟩"
      "D''' = FW' (norm_upd D'' (k' l'') n) n"
    and wf_dbm: "wf_dbm D" "wf_dbm M"
    and subset: "dbm_subset n D M"
    shows
      "∃ M' M'' M'''. A ⊢⇩I ⟨l, M⟩ ↝⇘n,τ⇙ ⟨l', M'⟩ ∧ A ⊢⇩I ⟨l', M'⟩ ↝⇘n,↿a⇙ ⟨l'', M''⟩
       ∧ M''' = FW' (norm_upd M'' (k' l'') n) n ∧ dbm_subset n D''' M'''"
  proof -
    from dbm_subset_correct''[OF wf_dbm] subset[THEN dbm_subset_conv] have
      "([curry (conv_M D)]⇘v,n⇙ ⊆ [curry (conv_M M)]⇘v,n⇙)"
      by simp
    from step_impl_mono_reachable[OF step(1) wf_dbm this] obtain M' where M':
      "A ⊢⇩I ⟨l, M⟩ ↝⇘n,τ⇙ ⟨l', M'⟩" "[curry (conv_M D')]⇘v,n⇙ ⊆ [curry (conv_M M')]⇘v,n⇙"
      by auto
    from step_impl_wf_dbm[OF step(1) wf_dbm(1)] step_impl_wf_dbm[OF M'(1) wf_dbm(2)] have wf_dbm':
      "wf_dbm D'" "wf_dbm M'" by auto
    from step_impl_norm_mono_reachable[OF step(2) wf_dbm' M'(2)] obtain M'' where M'':
      "A ⊢⇩I ⟨l', M'⟩ ↝⇘n,↿a⇙ ⟨l'', M''⟩"
      "[curry (conv_M (FW' (norm_upd D'' (k' l'') n) n))]⇘v,n⇙
      ⊆ [curry (conv_M (FW' (norm_upd M'' (k' l'') n) n))]⇘v,n⇙"
      using diag_conv by auto
    from step_impl_wf_dbm[OF step(2)] step_impl_wf_dbm[OF M''(1)] wf_dbm' have
      "wf_dbm D''" "wf_dbm M''"
      by auto
    from norm_step_wf_dbm[OF this(1)] norm_step_wf_dbm[OF this(2)] have
      "wf_dbm (FW' (norm_upd D'' (k' l'') n) n)" "wf_dbm (FW' (norm_upd M'' (k' l'') n) n)"
      by auto
    from M'(1) dbm_subset_correct''[OF this] M''(2) dbm_subset_conv_rev have
      "dbm_subset n (FW' (norm_upd D'' (k' l'') n) n) (FW' (norm_upd M'' (k' l'') n) n)"
      by auto
    with M'(1) M''(1) show ?thesis unfolding ‹D''' = _› by auto
  qed

lemma step_impl_mono_reachable'':
    assumes step:
      "A ⊢⇩I ⟨l, D⟩ ↝⇘n,τ⇙ ⟨l', D'⟩"
      "A ⊢⇩I ⟨l', D'⟩ ↝⇘n,↿a⇙ ⟨l'', D''⟩"
      "D''' = FW' (norm_upd D'' (k' l'') n) n"
    and wf_dbm: "wf_dbm D" "wf_dbm M"
    and subset: "[curry (conv_M D)]⇘v,n⇙ ⊆ [curry (conv_M M)]⇘v,n⇙"
    shows
      "∃ M' M'' M'''. A ⊢⇩I ⟨l, M⟩ ↝⇘n,τ⇙ ⟨l', M'⟩ ∧ A ⊢⇩I ⟨l', M'⟩ ↝⇘n,↿a⇙ ⟨l'', M''⟩
       ∧ M''' = FW' (norm_upd M'' (k' l'') n) n
       ∧ [curry (conv_M D')]⇘v,n⇙ ⊆ [curry (conv_M M')]⇘v,n⇙
       ∧ [curry (conv_M D''')]⇘v,n⇙ ⊆ [curry (conv_M M''')]⇘v,n⇙"
  proof -
    from step_impl_mono_reachable[OF step(1) wf_dbm subset] obtain M' where M':
      "A ⊢⇩I ⟨l, M⟩ ↝⇘n,τ⇙ ⟨l', M'⟩" "[curry (conv_M D')]⇘v,n⇙ ⊆ [curry (conv_M M')]⇘v,n⇙"
      by auto
    from step_impl_wf_dbm[OF step(1) wf_dbm(1)] step_impl_wf_dbm[OF M'(1) wf_dbm(2)] have wf_dbm':
      "wf_dbm D'" "wf_dbm M'" by auto
    from step_impl_norm_mono_reachable[OF step(2) wf_dbm' M'(2)] obtain M'' where M'':
      "A ⊢⇩I ⟨l', M'⟩ ↝⇘n,↿a⇙ ⟨l'', M''⟩"
      "[curry (conv_M (FW' (norm_upd D'' (k' l'') n) n))]⇘v,n⇙
      ⊆ [curry (conv_M (FW' (norm_upd M'' (k' l'') n) n))]⇘v,n⇙"
      using diag_conv by auto
    with M' M''(1) show ?thesis unfolding ‹D''' = _› by auto
  qed

lemma step_impl_mono_reachable__:
  assumes step:
    "A ⊢⇩I ⟨l, D⟩ ↝⇘n,τ⇙ ⟨l', D'⟩"
    "A ⊢⇩I ⟨l', D'⟩ ↝⇘n,↿a⇙ ⟨l'', D''⟩"
    "D''' = FW' (norm_upd D'' (k' l'') n) n"
    and wf_dbm: "wf_dbm D" "wf_dbm M"
    and subset: "dbm_subset n D M"
  shows
    "∃ M' M'' M'''. A ⊢⇩I ⟨l, M⟩ ↝⇘n,τ⇙ ⟨l', M'⟩ ∧ A ⊢⇩I ⟨l', M'⟩ ↝⇘n,↿a⇙ ⟨l'', M''⟩
     ∧ M''' = FW' (norm_upd M'' (k' l'') n) n ∧ dbm_subset n D''' M'''"
proof -
  from dbm_subset_correct''[OF wf_dbm] subset[THEN dbm_subset_conv] have
    "([curry (conv_M D)]⇘v,n⇙ ⊆ [curry (conv_M M)]⇘v,n⇙)"
    by simp
  from step_impl_mono_reachable[OF step(1) wf_dbm this] obtain M' where M':
    "A ⊢⇩I ⟨l, M⟩ ↝⇘n,τ⇙ ⟨l', M'⟩" "[curry (conv_M D')]⇘v,n⇙ ⊆ [curry (conv_M M')]⇘v,n⇙"
    by auto
  from step_impl_wf_dbm[OF step(1) wf_dbm(1)] step_impl_wf_dbm[OF M'(1) wf_dbm(2)] have wf_dbm':
    "wf_dbm D'" "wf_dbm M'" by auto
  from step_impl_norm_mono_reachable[OF step(2) wf_dbm' M'(2)] obtain M'' where M'':
    "A ⊢⇩I ⟨l', M'⟩ ↝⇘n,↿a⇙ ⟨l'', M''⟩"
    "[curry (conv_M (FW' (norm_upd D'' (k' l'') n) n))]⇘v,n⇙
    ⊆ [curry (conv_M (FW' (norm_upd M'' (k' l'') n) n))]⇘v,n⇙"
    using diag_conv by auto
  from step_impl_wf_dbm[OF step(2)] step_impl_wf_dbm[OF M''(1)] wf_dbm' have
    "wf_dbm D''" "wf_dbm M''"
    by auto
  from norm_step_wf_dbm[OF this(1)] norm_step_wf_dbm[OF this(2)] have
    "wf_dbm (FW' (norm_upd D'' (k' l'') n) n)" "wf_dbm (FW' (norm_upd M'' (k' l'') n) n)"
    by auto
  from M'(1) dbm_subset_correct''[OF this] M''(2) dbm_subset_conv_rev have
    "dbm_subset n (FW' (norm_upd D'' (k' l'') n) n) (FW' (norm_upd M'' (k' l'') n) n)"
    by auto
  with M'(1) M''(1) show ?thesis unfolding ‹D''' = _› by auto
qed

end

end