Theory Eg1Eg2

theory Eg1Eg2
imports Eg1
        Eg2
        "../CompositionalRefinement"
begin

locale sifum_refinement_eg1_eg2 =
  A: sifum_example +
  C: sifum_example2

primrec Eg2_var⇩C_of_Eg1 :: "Eg1.var ⇒ Eg2.var⇩C"
where
  "Eg2_var⇩C_of_Eg1 control_var = control_var⇩C" |
  "Eg2_var⇩C_of_Eg1 buffer = buffer⇩C" |
  "Eg2_var⇩C_of_Eg1 high_var = high_var⇩C" |
  "Eg2_var⇩C_of_Eg1 low_var = low_var⇩C" |
  "Eg2_var⇩C_of_Eg1 temp = temp⇩C"

sublocale sifum_refinement_eg1_eg2 ⊆ sifum_refinement dma dma⇩C 𝒞_vars 𝒞_vars⇩C 𝒞 𝒞⇩C A.eval⇩w C.eval⇩w undefined Eg2_var⇩C_of_Eg1
  supply image_cong_simp [cong del] INF_cong_simp [cong] SUP_cong_simp [cong] subst_all [simp del]
  apply(unfold_locales)
           apply(erule C.eval_det, simp)
          apply(rule C.Var_finite)
         apply(simp add:𝒞_vars⇩C_def split:if_splits)
        apply(simp add:𝒞_vars⇩C_def dma⇩C_def)
       apply(simp add:𝒞_vars⇩C_def dma⇩C_def)
      apply(rule inj_onI, simp)
      apply(case_tac x)
          apply(case_tac y, simp+)
         apply(case_tac y, simp+)
        apply(case_tac y, simp+)
       apply(case_tac y, simp+)
      apply(case_tac y, simp+)
     apply(case_tac x⇩A)
         apply(clarsimp simp:dma⇩C_def dma_def dma_control_var_def dma_control_var⇩C_def)+
    apply(case_tac x⇩A)
        apply(clarsimp simp:𝒞_vars⇩C_def 𝒞_vars_def)+
   apply(rule set_eqI, clarsimp)
   apply(case_tac x, clarsimp)
        apply(rule_tac x=control_var in rev_image_eqI, clarsimp+)
       apply(case_tac xa, clarsimp+)
          apply(case_tac xb, clarsimp+)
      apply(case_tac xa, clarsimp+)
         apply(case_tac xb, clarsimp+)
     apply(case_tac xa, clarsimp+)
        apply(case_tac xb, clarsimp+)
    apply(case_tac xa, clarsimp+)
       apply(case_tac xb, clarsimp+)
   apply(case_tac xa, clarsimp+)
  apply(simp add:𝒞⇩C_def)
  done

context sifum_refinement_eg1_eg2
begin


lemma bisim_simple_ℛ:
  "bisim_simple (A.ℛ Γ 𝒮 P)"
  unfolding bisim_simple_def
  apply clarsimp
  apply(drule_tac lc="⟨c⇩1⇩A, mds, mem⇩1⇩A⟩⇩A" and lc'="⟨c⇩2⇩A, mds, mem⇩2⇩A⟩⇩A" in A.bisim_simple_ℛ⇩u)
  by simp

(* Don't know to what extent these helpers can be made generic enough to go into any parent theories.
   Again, mightn't be able to (or bother to) make some generic considering the aexp evaluator
   is going to be specific to each language. *)

lemma conc_only_vars_not_visible_abs:
  "(∀v⇩C. v⇩C ∈ range Eg2_var⇩C_of_Eg1 ⟶ mem⇩C v⇩C = mem⇩C' v⇩C) ⟹ mem⇩A_of mem⇩C = mem⇩A_of mem⇩C'"
  by (simp add: mem⇩A_of_def)

lemma conc_only_var_assign_not_visible_abs:
  "∀v⇩C e. v⇩C ∉ range Eg2_var⇩C_of_Eg1 ⟶ mem⇩A_of mem⇩C = mem⇩A_of (mem⇩C(v⇩C := e))"
  using conc_only_vars_not_visible_abs
  by simp

lemma reg⇩C_is_not_the_var⇩C_of_anything:
  "reg⇩C = Eg2_var⇩C_of_Eg1 x ⟹ False"
  by (induct x, clarsimp+)

lemma reg⇩C_not_visible_abs:
  "reg⇩C ∉ range Eg2_var⇩C_of_Eg1"
  using reg⇩C_is_not_the_var⇩C_of_anything
  by blast

(* This one's pretty specific to this refinement... *)
lemma reg⇩C_the_only_concrete_only_var:
  "v⇩C ∉ range Eg2_var⇩C_of_Eg1 ⟹ v⇩C = reg⇩C"
  apply(case_tac v⇩C)
       apply(erule rev_notE, clarsimp, rule_tac x=control_var in range_eqI, clarsimp)
      apply(erule rev_notE, clarsimp, rule_tac x=buffer in range_eqI, clarsimp)
     apply(erule rev_notE, clarsimp, rule_tac x=high_var in range_eqI, clarsimp)
    apply(erule rev_notE, clarsimp, rule_tac x=low_var in range_eqI, clarsimp)
   apply(erule rev_notE, clarsimp, rule_tac x=temp in range_eqI, clarsimp)
  apply clarsimp
  done

lemma NoRW⇩A_implies_NoRW⇩C:
  "x ∈ mds⇩A_of mds⇩C AsmNoReadOrWrite ⟹
   Eg2_var⇩C_of_Eg1 x ∈ mds⇩C AsmNoReadOrWrite"
  unfolding mds⇩A_of_def
  apply clarsimp
  apply (simp only: Eg2_var⇩C_of_Eg1_def)
  apply clarsimp
  apply (simp add: f_inv_into_f)
  done

lemma NoWrite⇩A_implies_NoWrite⇩C:
  "x ∈ mds⇩A_of mds⇩C AsmNoWrite ⟹
   Eg2_var⇩C_of_Eg1 x ∈ mds⇩C AsmNoWrite"
  unfolding mds⇩A_of_def
  apply clarsimp
  apply (simp only: Eg2_var⇩C_of_Eg1_def)
  apply clarsimp
  apply (simp add: f_inv_into_f)
  done

lemma assign_eval⇩w_load⇩A:
  shows "(⟨x ← Eg1.Load y, mds, mem⟩⇩A, ⟨Stop, mds, mem (x := mem y)⟩⇩A) ∈ A.eval⇩w"
  by (metis A.assign_eval⇩w ev⇩A.simps(2))

lemma assign_eval⇩w_load⇩C:
  shows "(⟨x ← Load y, mds, mem⟩⇩C, ⟨Stop, mds, mem (x := mem y)⟩⇩C) ∈ C.eval⇩w"
  using C.unannotated[OF C.assign, where E="[]", simplified]
  apply(drule_tac x=x in meta_spec)
  apply(drule_tac x="Load y" in meta_spec)
  apply(drule_tac x=mds in meta_spec)
  apply(drule_tac x=mem in meta_spec)
  apply clarsimp
  done

lemma assign_eval⇩w_const⇩A:
  shows "(⟨x ← Eg1.Const c, mds, mem⟩, ⟨Stop, mds, mem (x := c)⟩) ∈ A.eval⇩w"
  by (metis A.assign_eval⇩w ev⇩A.simps(1))

lemma assign_eval⇩w_const⇩C:
  shows "(⟨x ← Const c, mds, mem⟩, ⟨Stop, mds, mem (x := c)⟩) ∈ C.eval⇩w"
  using C.unannotated[OF C.assign, where E="[]", simplified]
  apply(drule_tac x=x in meta_spec)
  apply(drule_tac x="Const c" in meta_spec)
  apply(drule_tac x=mds in meta_spec)
  apply(drule_tac x=mem in meta_spec)
  apply clarsimp
  done

lemma if_seq_eval⇩w_helper⇩A:
  "(⟨If B T E, mds, mem⟩,
    ⟨if ev⇩B mem B then T else E, mds, mem⟩⇩A) ∈ A.eval⇩w
    ⟹
   (⟨If B T E ;; TAIL, mds, mem⟩,
    ⟨if ev⇩B mem B then T ;; TAIL else E ;; TAIL, mds, mem⟩⇩A) ∈ A.eval⇩w"
  using A.eval⇩w.seq
  by auto

lemma if_seq_eval⇩w_helper⇩C:
  "(⟨If B T E, mds, mem⟩,
    ⟨if ev⇩B⇩C mem B then T else E, mds, mem⟩⇩C) ∈ C.eval⇩w
    ⟹
   (⟨If B T E ;; TAIL, mds, mem⟩,
    ⟨if ev⇩B⇩C mem B then T ;; TAIL else E ;; TAIL, mds, mem⟩⇩C) ∈ C.eval⇩w"
  using C.eval⇩w.seq
  by auto

lemma mem_assign_refinement_helper_var:
  "mem⇩A_of (mem⇩C (Eg2_var⇩C_of_Eg1 x := mem⇩C (Eg2_var⇩C_of_Eg1 y)))
       = (mem⇩A_of mem⇩C) (x := (mem⇩A_of mem⇩C) y)"
  apply(clarsimp simp: mem⇩A_of_def)
  apply(rule ext, clarsimp)
  apply(cases x)
      apply(case_tac x⇩A, clarsimp+)+
  done

lemma mem_assign_refinement_helper_const:
  "mem⇩A_of (mem⇩C (Eg2_var⇩C_of_Eg1 x := c))
       = (mem⇩A_of mem⇩C) (x := c)"
  apply(clarsimp simp: mem⇩A_of_def)
  apply(rule ext, clarsimp)
  apply(cases x)
      apply(case_tac x⇩A, clarsimp+)+
  done

lemma if_true_eval⇩w⇩C:
  shows "mem⇩C x = 0 ⟶
     (⟨(If (Eq x 0) c⇩C_then c⇩C_else) ;; c⇩C_tail, mds⇩C, mem⇩C⟩⇩C,
      ⟨(c⇩C_then ;; c⇩C_tail), mds⇩C, mem⇩C⟩⇩C) ∈ C.eval⇩w"
  using C.if_eval⇩w C.eval⇩w.seq ev⇩B⇩C.simps by presburger

lemma if_false_eval⇩w⇩C:
  shows "mem⇩C x ≠ 0 ⟶
     (⟨(If (Eq x 0) c⇩C_then c⇩C_else) ;; c⇩C_tail, mds⇩C, mem⇩C⟩⇩C,
      ⟨(c⇩C_else ;; c⇩C_tail), mds⇩C, mem⇩C⟩⇩C) ∈ C.eval⇩w"
  using C.if_eval⇩w C.eval⇩w.seq ev⇩B⇩C.simps by presburger


end

end