Theory ArityAnalysisCorrDenotational

theory ArityAnalysisCorrDenotational
imports ArityAnalysisSpec "Denotational" ArityTransform
begin

context ArityAnalysisLetSafe
begin

inductive eq :: "Arity ⇒ Value ⇒ Value ⇒ bool" where
   "eq 0 v v"
 |  "(⋀ v. eq n (v1 ↓Fn v) (v2 ↓Fn v)) ⟹ eq (inc⋅n) v1 v2"

lemma [simp]: "eq 0 v v' ⟷ v = v'"
  by (auto elim: eq.cases intro: eq.intros)

lemma eq_inc_simp:
  "eq (inc⋅n) v1 v2 ⟷ (∀ v . eq n (v1 ↓Fn v) (v2 ↓Fn v))"
  by (auto elim: eq.cases intro: eq.intros)

lemma eq_FnI:
  "(⋀ v. eq (pred⋅n) (f1⋅v) (f2⋅v)) ⟹ eq n (Fn⋅f1) (Fn⋅f2)"
  by (induction n rule: Arity_ind) (auto intro: eq.intros cfun_eqI)

lemma eq_refl[simp]: "eq a v v"
  by (induction a arbitrary: v rule: Arity_ind) (auto intro!: eq.intros)

lemma eq_trans[trans]: "eq a v1 v2 ⟹ eq a v2 v3 ⟹ eq a v1 v3"
  apply (induction a arbitrary: v1 v2 v3 rule: Arity_ind)
  apply (auto elim!: eq.cases intro!: eq.intros)
  apply blast
  done

lemma eq_Fn: "eq a v1 v2 ⟹ eq (pred⋅a) (v1 ↓Fn v) (v2 ↓Fn v)"
apply (induction a  rule: Arity_ind[case_names 0 inc])
apply (auto simp add: eq_inc_simp)
done

lemma eq_inc_same: "eq a v1 v2 ⟹ eq (inc⋅a) v1 v2"
by (induction a  arbitrary: v1 v2 rule: Arity_ind[case_names 0 inc])  (auto simp add: eq_inc_simp)

lemma eq_mono: "a ⊑ a' ⟹ eq a' v1 v2 ⟹ eq a v1 v2"
proof (induction a  rule: Arity_ind[case_names 0 inc])
  case 0 thus ?case by auto
next
  case (inc a)
  show "eq (inc⋅a) v1 v2"
  proof (cases "inc⋅a = a'")
    case True with inc show ?thesis by simp
  next
    case False with `inc⋅a ⊑ a'` have "a ⊑ a'" 
      by (simp add: inc_def)(transfer, simp)
    from this inc.prems(2)
    have "eq a v1 v2" by (rule inc.IH)
    thus ?thesis by (rule eq_inc_same)
  qed
qed

lemma eq_join[simp]: "eq (a ⊔ a') v1 v2 ⟷ eq a v1 v2 ∧ eq a' v1 v2"
  using Arity_total[of a a']
  apply (auto elim!: eq_mono[OF join_above1] eq_mono[OF join_above2])
  apply (metis join_self_below(2))
  apply (metis join_self_below(1))
  done

lemma eq_adm: "cont f ⟹ cont g ⟹ adm (λ x. eq a (f x) (g x))"
proof (induction a arbitrary: f g rule: Arity_ind[case_names 0 inc])
  case 0 thus ?case by simp
next
  case inc
  show ?case
  apply (subst eq_inc_simp)
  apply (rule adm_all)
  apply (rule inc)
  apply (intro cont2cont inc(2,3))+
  done
qed

inductive eqρ :: "AEnv ⇒ (var ⇒ Value) ⇒ (var ⇒ Value) ⇒ bool" where
 eqρI: "(⋀ x a. ae x = up⋅a ⟹ eq a (ρ1 x) (ρ2 x)) ⟹ eqρ ae ρ1 ρ2"

lemma eqρE: "eqρ ae ρ1 ρ2 ⟹ ae x = up⋅a ⟹ eq a (ρ1 x) (ρ2 x)"
  by (auto simp add: eqρ.simps) 

lemma eqρ_refl[simp]: "eqρ ae ρ ρ"
  by (simp add: eqρ.simps) 

lemma eq_esing_up[simp]: "eqρ (esing x⋅(up⋅a)) ρ1 ρ2 ⟷ eq a (ρ1 x) (ρ2 x)"
  by (auto simp add: eqρ.simps) 
 
lemma eqρ_mono:
  assumes "ae ⊑ ae'"
  assumes "eqρ ae' ρ1 ρ2"
  shows "eqρ ae ρ1 ρ2"
proof (rule eqρI)
  fix x a
  assume "ae x = up⋅a"
  with `ae ⊑ ae'` have "up⋅a ⊑ ae' x" by (metis fun_belowD)
  then obtain a' where "ae' x = up⋅a'" by (metis Exh_Up below_antisym minimal)
  with `eqρ ae' ρ1 ρ2`
  have "eq a' (ρ1 x) (ρ2 x)" by (auto simp add: eqρ.simps)
  with `up⋅a ⊑ ae' x` and `ae' x = up⋅a'`
  show "eq a (ρ1 x) (ρ2 x)" by (metis eq_mono up_below)
qed

lemma eqρ_adm: "cont f ⟹ cont g ⟹ adm (λ x. eqρ a (f x) (g x))"
  apply (simp add: eqρ.simps)
  apply (intro adm_lemmas eq_adm)
  apply (erule cont2cont_fun)+
  done
 
lemma up_join_eq_up[simp]: "up⋅(n::'a::Finite_Join_cpo) ⊔ up⋅n' = up⋅(n ⊔ n')"
  apply (rule lub_is_join)
  apply (auto simp add: is_lub_def )
  apply (case_tac u)
  apply auto
  done
 
lemma eqρ_join[simp]: "eqρ (ae ⊔ ae') ρ1 ρ2 ⟷ eqρ ae ρ1 ρ2 ∧ eqρ ae' ρ1 ρ2"
  apply (auto elim!: eqρ_mono[OF join_above1] eqρ_mono[OF join_above2])
  apply (auto intro!: eqρI)
  apply (case_tac "ae x", auto elim: eqρE)
  apply (case_tac "ae' x", auto elim: eqρE)
  done

lemma eqρ_override[simp]:
  "eqρ ae (ρ1 ++⇘S⇙ ρ2) (ρ1' ++⇘S⇙ρ2') ⟷ eqρ ae (ρ1 f|` (- S)) (ρ1' f|` (- S)) ∧  eqρ ae (ρ2 f|` S) (ρ2' f|` S)"
  by (auto simp add: lookup_env_restr_eq eqρ.simps lookup_override_on_eq)

lemma Aexp_heap_below_Aheap:
  assumes "(Aheap Γ e⋅a) x = up⋅a'"
  assumes "map_of Γ x = Some e'"
  shows "Aexp e'⋅a' ⊑ Aheap Γ e⋅a ⊔ Aexp (Let Γ e)⋅a"
proof-
  from assms(1)
  have "Aexp e'⋅a' = ABind x e'⋅(Aheap Γ e⋅a)"
    by (simp del: join_comm fun_meet_simp)
  also have "… ⊑ ABinds Γ⋅(Aheap Γ e⋅a)"
    by (rule monofun_cfun_fun[OF ABind_below_ABinds[OF `map_of _ _ = _`]])
  also have "… ⊑ ABinds Γ⋅(Aheap Γ e⋅a) ⊔  Aexp e⋅a"
    by simp
  also note Aexp_Let
  finally
  show ?thesis by this simp_all
qed

lemma Aexp_body_below_Aheap:
  shows "Aexp e⋅a ⊑ Aheap Γ e⋅a ⊔ Aexp (Let Γ e)⋅a"
  by (rule below_trans[OF join_above2 Aexp_Let])


lemma Aexp_correct: "eqρ (Aexp e⋅a) ρ1 ρ2 ⟹ eq a (⟦e⟧⇘ρ1⇙) (⟦e⟧⇘ρ2⇙)"
proof(induction a e arbitrary: ρ1 ρ2 rule: transform.induct[case_names App Lam Var Let Bool IfThenElse])
  case (Var a x)
  from `eqρ (Aexp (Var x)⋅a) ρ1 ρ2` 
  have "eqρ (esing x⋅(up⋅a)) ρ1 ρ2" by (rule eqρ_mono[OF Aexp_Var_singleton])
  thus ?case by simp
next
  case (App a e x)
  from `eqρ (Aexp (App e x)⋅a) ρ1 ρ2` 
  have "eqρ (Aexp e⋅(inc⋅a) ⊔ esing x⋅(up⋅0)) ρ1 ρ2" by (rule eqρ_mono[OF Aexp_App])
  hence "eqρ (Aexp e⋅(inc⋅a)) ρ1 ρ2" and "ρ1 x = ρ2 x" by simp_all
  from App(1)[OF this(1)] this(2)
  show ?case by (auto elim: eq.cases)
next
  case (Lam a x e)
  from  `eqρ (Aexp (Lam [x]. e)⋅a) ρ1 ρ2`
  have "eqρ (env_delete x (Aexp e⋅(pred⋅a))) ρ1 ρ2" by (rule eqρ_mono[OF Aexp_Lam])
  hence "⋀ v. eqρ (Aexp e⋅(pred⋅a)) (ρ1(x := v)) (ρ2(x := v))"  by (auto intro!: eqρI elim!: eqρE)
  from Lam(1)[OF this]
  show ?case by (auto intro: eq_FnI simp del: fun_upd_apply)
next
  case (Bool b)
  show ?case by simp
next
  case (IfThenElse a scrut e⇩1 e⇩2)
  from `eqρ (Aexp (scrut ? e⇩1 : e⇩2)⋅a) ρ1 ρ2`
  have "eqρ (Aexp scrut⋅0 ⊔ Aexp e⇩1⋅a ⊔ Aexp e⇩2⋅a) ρ1 ρ2" by (rule eqρ_mono[OF Aexp_IfThenElse])
  hence "eqρ (Aexp scrut⋅0) ρ1 ρ2"
  and   "eqρ (Aexp e⇩1⋅a) ρ1 ρ2"
  and   "eqρ (Aexp e⇩2⋅a) ρ1 ρ2" by simp_all
  from IfThenElse(1)[OF this(1)] IfThenElse(2)[OF this(2)] IfThenElse(3)[OF this(3)]
  show ?case
    by (cases "⟦ scrut ⟧⇘ρ2⇙") auto
next
  case (Let a Γ e)

  have "eqρ (Aheap Γ e⋅a ⊔ Aexp (Let Γ e)⋅a) (⦃Γ⦄ρ1) (⦃Γ⦄ρ2)"
  proof(induction rule: parallel_HSem_ind[case_names adm bottom step])
    case adm thus ?case by (intro eqρ_adm cont2cont)
  next
    case bottom show ?case by simp
  next
    case (step ρ1' ρ2')
    show ?case
    proof (rule eqρI)
      fix x a'
      assume ass: "(Aheap Γ e⋅a ⊔ Aexp (Let Γ e)⋅a) x = up⋅a'"
      show "eq a' ((ρ1 ++⇘domA Γ⇙ ❙⟦ Γ ❙⟧⇘ρ1'⇙) x) ((ρ2 ++⇘domA Γ⇙ ❙⟦ Γ ❙⟧⇘ρ2'⇙) x)"
      proof(cases "x ∈ domA Γ")
        case [simp]: True
        then obtain e' where [simp]: "map_of Γ x = Some e'" by (metis domA_map_of_Some_the)
        have "(Aheap Γ e⋅a) x = up⋅a'" using ass by simp
        hence "Aexp e'⋅a' ⊑ Aheap Γ e⋅a ⊔ Aexp (Let Γ e)⋅a" using `map_of _ _ = _` by (rule Aexp_heap_below_Aheap)
        hence "eqρ (Aexp e'⋅a') ρ1' ρ2'" using step(1) by (rule eqρ_mono)
        hence "eq a' (⟦ e' ⟧⇘ρ1'⇙) (⟦ e' ⟧⇘ρ2'⇙)"
          by (rule Let(1)[OF map_of_SomeD[OF `map_of _ _ = _`]])
        thus ?thesis by (simp add: lookupEvalHeap')
      next
        case [simp]: False
        with edom_Aheap have "x ∉ edom (Aheap Γ e⋅a)" by blast
        hence "(Aexp (Let Γ e)⋅a) x = up⋅a'" using ass by (simp add: edomIff)
        with `eqρ (Aexp (Let Γ e)⋅a) ρ1 ρ2`
        have "eq a' (ρ1 x) (ρ2 x)" by (auto elim: eqρE)
        thus ?thesis by simp
      qed
    qed
  qed
  hence "eqρ (Aexp e⋅a) (⦃Γ⦄ρ1) (⦃Γ⦄ρ2)" by (rule eqρ_mono[OF Aexp_body_below_Aheap])
  hence "eq a (⟦ e ⟧⇘⦃Γ⦄ρ1⇙) (⟦ e ⟧⇘⦃Γ⦄ρ2⇙)" by (rule Let(2)[simplified])
  thus ?case by simp
qed

lemma ESem_ignores_fresh[simp]: "⟦ e ⟧⇘ρ(fresh_var e := v)⇙ = ⟦ e ⟧⇘ρ⇙"
  by (metis ESem_fresh_cong env_restr_fun_upd_other fresh_var_not_free)

lemma eq_Aeta_expand: "eq a (⟦ Aeta_expand a e ⟧⇘ρ⇙) (⟦e⟧⇘ρ⇙)"
  apply (induction a arbitrary: e ρ  rule: Arity_ind[case_names 0 inc])
  apply simp
  apply (fastforce simp add: eq_inc_simp elim: eq_trans)
  done

lemma Arity_transformation_correct: "eq a (⟦ 𝒯⇘a⇙ e ⟧⇘ρ⇙) (⟦ e ⟧⇘ρ⇙)"
proof(induction a e arbitrary: ρ rule: transform.induct[case_names App Lam Var Let Bool IfThenElse])
  case Var
  show ?case by simp
next
  case (App a e x)
  from this[where ρ =ρ ]
  show ?case
    by (auto elim: eq.cases)
next
  case (Lam x e)
  thus ?case
    by (auto intro: eq_FnI)
next
  case (Bool b)
  show ?case by simp
next
  case (IfThenElse a e e⇩1 e⇩2)
  thus ?case by (cases "⟦ e ⟧⇘ρ⇙") auto
next
  case (Let a Γ e)

  have "eq a (⟦ transform a (Let Γ e) ⟧⇘ρ⇙) (⟦ transform a e ⟧⇘⦃map_transform Aeta_expand (Aheap Γ e⋅a) (map_transform transform (Aheap Γ e⋅a) Γ)⦄ρ⇙)"
    by simp
  also have "eq a … (⟦ e ⟧⇘⦃map_transform Aeta_expand (Aheap Γ e⋅a) (map_transform transform (Aheap Γ e⋅a) Γ)⦄ρ⇙)"
    using Let(2) by simp
  also have "eq a … (⟦ e ⟧⇘⦃Γ⦄ρ⇙)"
  proof (rule Aexp_correct)
    have "eqρ (Aheap Γ e⋅a ⊔ Aexp (Let Γ e)⋅a) (⦃map_transform Aeta_expand (Aheap Γ e⋅a) (map_transform transform (Aheap Γ e⋅a) Γ)⦄ρ) (⦃Γ⦄ρ)"
    proof(induction rule: parallel_HSem_ind[case_names adm bottom step])
      case adm thus ?case by (intro eqρ_adm cont2cont)
    next
      case bottom show ?case by simp
    next
      case (step ρ1 ρ2)
      have "eqρ (Aheap Γ e⋅a ⊔ Aexp (Let Γ e)⋅a) (❙⟦ map_transform Aeta_expand (Aheap Γ e⋅a) (map_transform transform (Aheap Γ e⋅a) Γ) ❙⟧⇘ρ1⇙) (❙⟦Γ❙⟧⇘ρ2⇙)"
      proof(rule eqρI)
        fix x a'
        assume ass: "(Aheap Γ e⋅a ⊔ Aexp (Let Γ e)⋅a) x = up⋅a'"
        show "eq a' ((❙⟦ map_transform Aeta_expand (Aheap Γ e⋅a) (map_transform transform (Aheap Γ e⋅a) Γ) ❙⟧⇘ρ1⇙) x) ((❙⟦Γ❙⟧⇘ρ2⇙) x)"
        proof(cases "x ∈ domA Γ")
          case [simp]: True
          then obtain e' where [simp]: "map_of Γ x = Some e'" by (metis domA_map_of_Some_the)
          from ass have ass': "(Aheap Γ e⋅a) x = up⋅a'" by simp

          have "(❙⟦ map_transform Aeta_expand (Aheap Γ e⋅a) (map_transform transform (Aheap Γ e⋅a) Γ) ❙⟧⇘ρ1⇙) x =
            ⟦Aeta_expand a' (transform a' e')⟧⇘ρ1⇙"
           by (simp add: lookupEvalHeap' map_of_map_transform ass')
          also have "eq a' … (⟦transform a' e'⟧⇘ρ1⇙)"
            by (rule eq_Aeta_expand)
          also have "eq a' … (⟦e'⟧⇘ρ1⇙)"
            by (rule Let(1)[OF map_of_SomeD[OF `map_of _ _ = _`]])
          also have "eq a' … (⟦e'⟧⇘ρ2⇙)"
          proof (rule Aexp_correct)
            from ass' `map_of _ _ = _`
            have "Aexp e'⋅a' ⊑ Aheap Γ e⋅a ⊔ Aexp (Let Γ e)⋅a" by (rule Aexp_heap_below_Aheap)
            thus "eqρ (Aexp e'⋅a') ρ1 ρ2" using step by (rule eqρ_mono)
          qed
          also have "… = (❙⟦Γ❙⟧⇘ρ2⇙) x"
           by (simp add: lookupEvalHeap')
          finally
          show ?thesis.
        next
          case False thus ?thesis by simp
        qed
      qed
      thus ?case
        by (simp add: env_restr_useless  order_trans[OF  edom_evalHeap_subset] del: fun_meet_simp eqρ_join)
    qed
    thus "eqρ (Aexp e⋅a) (⦃map_transform Aeta_expand (Aheap Γ e⋅a) (map_transform transform (Aheap Γ e⋅a) Γ)⦄ρ) (⦃Γ⦄ρ)" 
        by (rule eqρ_mono[OF Aexp_body_below_Aheap])
  qed
  also have "… = ⟦ Let Γ e ⟧⇘ρ⇙"
    by simp
  finally show ?case.
qed

corollary Arity_transformation_correct':
  "⟦ 𝒯⇘0⇙ e ⟧⇘ρ⇙ = ⟦ e ⟧⇘ρ⇙"
  using Arity_transformation_correct[where a = 0] by simp

end
end