Theory Eg1RefinementTrivial

theory Eg1RefinementTrivial
imports Eg1
        "../CompositionalRefinement"
        Dependent_SIFUM_Type_Systems.TypeSystem
begin

sublocale sifum_example ⊆
    sifum_refinement_same_mem dma 𝒞_vars 𝒞 evalw evalw
      by(unfold_locales)

context sifum_example begin

text ‹This predicate can be used to express arbitrary relational invariants for
  compiler-specific features, but for this trivial case the vacuous one is fine.
›
definition P_true :: "('a × 'a) set"
where
  "P_true  ≡ UNIV"

lemma Id_secure_refinement:
  "secure_refinement R Id P_true"
  unfolding secure_refinement_def
  proof(safe)
    show "closed_others Id"
    unfolding closed_others_def Id_def by blast
  next
    show "preserves_modes_mem Id"
    unfolding preserves_modes_mem_def Id_def by blast
  next
    fix c1A mds mem1 c1C c1C' mds' mem1'
    assume step: "(⟨c1C, mds, mem1⟩C, ⟨c1C', mds', mem1'⟩C) ∈ evalw"
    show
      "∃n c1A'.
          neval ⟨c1C, mds, mem1⟩C n ⟨c1A', mds', mem1'⟩C ∧
          (⟨c1A', mds', mem1'⟩C, ⟨c1C', mds', mem1'⟩C) ∈ Id ∧
          (∀c2A mem2 c2C c2A' mem2'.
              (⟨c1C, mds, mem1⟩C, ⟨c2A, mds, mem2⟩C) ∈ R ∧
              (⟨c2A, mds, mem2⟩C, ⟨c2C, mds, mem2⟩C) ∈ Id ∧
              (⟨c1C, mds, mem1⟩C, ⟨c2C, mds, mem2⟩C) ∈ P_true ∧
              neval ⟨c2A, mds, mem2⟩C n ⟨c2A', mds', mem2'⟩C ⟶
              (∃c2C'.
                  (⟨c2C, mds, mem2⟩C, ⟨c2C', mds', mem2'⟩C)
                  ∈ evalw ∧
                  (⟨c2A', mds', mem2'⟩C, ⟨c2C', mds', mem2'⟩C) ∈ Id ∧
                  (⟨c1C', mds', mem1'⟩C, ⟨c2C', mds', mem2'⟩C) ∈ P_true))"
    proof -
      let ?n = "Suc 0"
      let ?c1A' = c1C'
      from step have "neval ⟨c1C, mds, mem1⟩C ?n ⟨?c1A', mds', mem1'⟩C"
        by simp
      moreover have "(⟨?c1A', mds', mem1'⟩C, ⟨c1C', mds', mem1'⟩C) ∈ Id"
        by simp
      moreover have "(∀c2A mem2 c2C c2A' mem2'.
              (⟨c1C, mds, mem1⟩C, ⟨c2A, mds, mem2⟩C) ∈ R ∧
              (⟨c2A, mds, mem2⟩C, ⟨c2C, mds, mem2⟩C) ∈ Id ∧
              (⟨c1C, mds, mem1⟩C, ⟨c2C, mds, mem2⟩C) ∈ P_true ∧
              neval ⟨c2A, mds, mem2⟩C ?n ⟨c2A', mds', mem2'⟩C ⟶
              (∃c2C'.
                  (⟨c2C, mds, mem2⟩C, ⟨c2C', mds', mem2'⟩C)
                  ∈ evalw ∧
                  (⟨c2A', mds', mem2'⟩C, ⟨c2C', mds', mem2'⟩C) ∈ Id ∧
                  (⟨c1C', mds', mem1'⟩C, ⟨c2C', mds', mem2'⟩C) ∈ P_true))"
        using step
        unfolding P_true_def
        by clarsimp
      ultimately show ?thesis by blast
    qed
  next
    show "closed_glob_consistent P_true"
      by(auto simp: closed_glob_consistent_def P_true_def)
  qed

text ‹
  This doesn't really mean much, but shows the lemmas in action.
  (I suspect that @{term "RC_of R Id"} is equivalent to @{term R}. But who cares?)
›
lemma "strong_low_bisim_mm (gen_refine.RC_of (ℛ Γ 𝒮 P) Id P_true)"
  apply(rule RC_of_strong_low_bisim_mm)
   apply(rule ℛ_bisim)
  apply(rule Id_secure_refinement)
  unfolding P_true_def sym_def apply blast
  done

end

end