Theory ArityAnalysisFix

theory ArityAnalysisFix
imports ArityAnalysisSig ArityAnalysisAbinds
begin

context ArityAnalysis
begin

definition Afix ::  "heap ⇒ (AEnv → AEnv)"
  where "Afix Γ = (Λ ae. (μ  ae'. ABinds Γ ⋅ ae' ⊔ ae))"

lemma Afix_eq: "Afix Γ⋅ae = (μ ae'. (ABinds Γ⋅ae') ⊔ ae)"
  unfolding Afix_def by simp

lemma Afix_strict[simp]: "Afix Γ⋅⊥ = ⊥"
  unfolding Afix_eq
  by (rule fix_eqI) auto

lemma Afix_least_below: "ABinds Γ ⋅ ae' ⊑ ae' ⟹ ae ⊑ ae' ⟹ Afix Γ ⋅ ae ⊑ ae'"
  unfolding Afix_eq
  by (auto intro: fix_least_below)

lemma Afix_unroll: "Afix Γ⋅ae = ABinds Γ ⋅ (Afix Γ⋅ae) ⊔ ae"
  unfolding Afix_eq
  apply (subst fix_eq)
  by simp

lemma Abinds_below_Afix: "ABinds Δ ⊑ Afix Δ"
  apply (rule cfun_belowI)
  apply (simp add: Afix_eq)
  apply (subst fix_eq, simp)
  apply (rule below_trans[OF _ join_above2])
  apply (rule monofun_cfun_arg)
  apply (subst fix_eq, simp)
  done

lemma Afix_above_arg: "ae ⊑ Afix Γ ⋅ ae"
  by (subst Afix_unroll) simp

lemma Abinds_Afix_below[simp]: "ABinds Γ⋅(Afix Γ⋅ae) ⊑ Afix Γ⋅ae"
  apply (subst Afix_unroll) back
  apply simp
  done


(*lemma Abinds_Afix[simp]: "ABinds Γ⋅(Afix Γ⋅ae) = Afix Γ⋅ae"
  unfolding Afix_eq
  apply (subst fix_eq) back apply simp
  apply (rule below_trans[OF ABinds_above_arg monofun_cfun_arg])
  apply (subst fix_eq) apply simp
  done
*)

lemma Afix_reorder: "map_of Γ = map_of Δ ⟹ Afix Γ = Afix Δ"
  by (intro cfun_eqI)(simp add: Afix_eq cong: Abinds_reorder)

lemma Afix_repeat_singleton: "(μ xa. Afix Γ⋅(esing x⋅(n ⊔ xa x) ⊔ ae)) = Afix Γ⋅(esing x⋅n ⊔ ae)"
  apply (rule below_antisym)
  defer
  apply (subst fix_eq, simp)
  apply (intro monofun_cfun_arg join_mono below_refl join_above1)

  apply (rule fix_least_below, simp)
  apply (rule Afix_least_below, simp)
  apply (intro join_below below_refl iffD2[OF esing_below_iff] below_trans[OF _ fun_belowD[OF Afix_above_arg]]  below_trans[OF _ Afix_above_arg] join_above1)
  apply simp
  done

lemma Afix_join_fresh: "ae' ` (domA Δ) ⊆ {⊥}  ⟹  Afix Δ⋅(ae ⊔ ae') = (Afix Δ⋅ae) ⊔ ae'"
  apply (rule below_antisym)
  apply (rule Afix_least_below)
  apply (subst Abinds_join_fresh, simp)
  apply (rule below_trans[OF Abinds_Afix_below join_above1])
  apply (rule join_below)
  apply (rule below_trans[OF Afix_above_arg join_above1])
  apply (rule join_above2)
  apply (rule join_below[OF monofun_cfun_arg [OF join_above1]])
  apply (rule below_trans[OF join_above2 Afix_above_arg])
  done


lemma Afix_restr_fresh:
  assumes "atom ` S ♯* Γ"
  shows "Afix Γ⋅ae f|` (- S) = Afix Γ⋅(ae  f|` (- S)) f|` (- S)"
  unfolding Afix_eq
proof (rule parallel_fix_ind[where P = "λ x y . x f|` (- S) = y  f|` (- S)"], goal_cases)
  case 1
  show ?case by simp
next
  case 2
  show ?case ..
next
  case prems: (3 aeL aeR)
  have "(ABinds Γ⋅aeL ⊔ ae) f|` (- S) = ABinds Γ⋅aeL  f|` (- S) ⊔ ae  f|` (- S)" by (simp add: env_restr_join)
  also have "… = ABinds Γ⋅(aeL  f|` (- S)) f|` (- S) ⊔ ae  f|` (- S)" by (rule arg_cong[OF ABinds_restr_fresh[OF assms]])
  also have "… = ABinds Γ⋅(aeR  f|` (- S)) f|` (- S) ⊔ ae  f|` (- S)" unfolding prems ..
  also have "… = ABinds Γ⋅aeR f|` (- S) ⊔ ae  f|` (- S)" by (rule arg_cong[OF ABinds_restr_fresh[OF assms, symmetric]])
  also have "… = (ABinds Γ⋅aeR ⊔ ae f|` (- S)) f|` (- S)" by (simp add: env_restr_join)
  finally show ?case by simp
qed

lemma Afix_restr:
  assumes "domA Γ ⊆ S"
  shows "Afix Γ⋅ae f|` S = Afix Γ⋅(ae  f|` S) f|` S"
  unfolding Afix_eq
  apply (rule parallel_fix_ind[where P = "λ x y . x f|`S = y  f|` S"])
  apply simp
  apply rule
  apply (auto   simp add: env_restr_join)
  apply (metis  ABinds_restr[OF assms, symmetric])
  done

lemma Afix_restr_subst':
  assumes "⋀ x' e a. (x',e) ∈ set Γ ⟹ Aexp e[x::=y]⋅a f|` S = Aexp e⋅a f|` S"
  assumes "x ∉ S"
  assumes "y ∉ S"
  assumes "domA Γ ⊆ S"
  shows "Afix Γ[x::h=y]⋅ae f|` S = Afix Γ⋅(ae f|` S) f|` S"
  unfolding Afix_eq
  apply (rule parallel_fix_ind[where P = "λ x y . x f|`S = y  f|` S"])
  apply simp
  apply rule
  apply (auto   simp add: env_restr_join)
  apply (subst ABinds_restr_subst[OF assms]) apply assumption
  apply (subst ABinds_restr[OF assms(4)]) back
  apply simp
  done

 
lemma Afix_subst_approx:
  assumes "⋀ v n. v ∈ domA Γ ⟹ Aexp (the (map_of Γ v))[y::=x]⋅n ⊑ (Aexp (the (map_of Γ v))⋅n)(y := ⊥, x := up⋅0)"
  assumes "x ∉ domA Γ"
  assumes "y ∉ domA Γ"
  shows "Afix Γ[y::h= x]⋅(ae(y := ⊥, x := up⋅0)) ⊑ (Afix Γ⋅ae)(y := ⊥, x := up⋅0)"
  unfolding Afix_eq
proof (rule parallel_fix_ind[where P = "λ aeL aeR . aeL ⊑ aeR(y := ⊥, x := up⋅0)"], goal_cases)
  case 1
  show ?case by simp
next
  case 2
  show ?case..
next
  case (3 aeL aeR)
  hence "ABinds Γ[y::h=x]⋅aeL ⊑ ABinds Γ[y::h=x]⋅(aeR (y := ⊥, x := up⋅0))" by (rule monofun_cfun_arg)
  also have "…  ⊑ (ABinds Γ⋅aeR)(y := ⊥, x := up⋅0)"
    using assms
  proof (induction rule: ABinds.induct, goal_cases)
    case 1
    thus ?case by simp
  next
    case prems: (2 v e Γ)
    have "⋀n. Aexp e[y::=x]⋅n ⊑ (Aexp e⋅n)(y := ⊥, x := up⋅0)" using prems(2)[where v = v] by auto
    hence IH1: "⋀ n. fup⋅(Aexp e[y::=x])⋅n ⊑ (fup⋅(Aexp e)⋅n)(y := ⊥, x := up⋅0)"  by (case_tac n) auto

    have "ABinds (delete v Γ)[y::h=x]⋅(aeR(y := ⊥, x := up⋅0)) ⊑ (ABinds (delete v Γ)⋅aeR)(y := ⊥, x := up⋅0)"
      apply (rule prems) using prems(2,3,4) by fastforce+
    hence IH2: "ABinds (delete v Γ[y::h=x])⋅(aeR(y := ⊥, x := up⋅0)) ⊑ (ABinds (delete v Γ)⋅aeR)(y := ⊥, x := up⋅0)"
       unfolding subst_heap_delete.
    
    have [simp]: "(aeR(y := ⊥, x := up⋅0)) v = aeR v" using prems(3,4) by auto
   
    show ?case by (simp del: fun_upd_apply join_comm) (rule join_mono[OF IH1 IH2])
  qed
  finally have "ABinds Γ[y::h=x]⋅aeL ⊑ (ABinds Γ⋅aeR)(y := ⊥, x := up⋅0)"
    by this simp
  thus ?case
    by (auto simp add: join_below_iff elim: below_trans)
qed

end

lemma Afix_eqvt[eqvt]: "π ∙ (ArityAnalysis.Afix Aexp Γ) = ArityAnalysis.Afix  (π ∙ Aexp) (π ∙ Γ)"
  unfolding ArityAnalysis.Afix_def
  by perm_simp (simp add: Abs_cfun_eqvt)


lemma Afix_cong[fundef_cong]:
  "⟦ (⋀ e. e ∈ snd ` set heap2 ⟹ aexp1 e = aexp2 e); heap1 = heap2 ⟧
      ⟹ ArityAnalysis.Afix aexp1 heap1 = ArityAnalysis.Afix aexp2 heap2"
   unfolding ArityAnalysis.Afix_def by (metis Abinds_cong)


context EdomArityAnalysis
begin

lemma Afix_edom: "edom (Afix Γ ⋅ ae) ⊆ fv Γ ∪ edom ae"
  unfolding Afix_eq
  by (rule fix_ind[where P = "λ ae' . edom ae' ⊆ fv Γ ∪ edom ae"] )
     (auto dest: subsetD[OF edom_AnalBinds])

lemma ABinds_lookup_fresh:
  "atom v ♯ Γ ⟹ (ABinds Γ⋅ae) v = ⊥"
by (induct Γ rule: ABinds.induct) (auto simp add: fresh_Cons fresh_Pair fup_Aexp_lookup_fresh fresh_delete)

lemma Afix_lookup_fresh:
  assumes "atom v ♯ Γ"
  shows "(Afix Γ⋅ae) v = ae v"
  apply (rule below_antisym)
  apply (subst Afix_eq)
  apply (rule fix_ind[where  P = "λ ae'. ae' v ⊑ ae v"])
  apply (auto simp add: ABinds_lookup_fresh[OF assms] fun_belowD[OF Afix_above_arg])
  done

lemma Afix_comp2join_fresh:
  "atom ` (domA Δ) ♯* Γ ⟹ ABinds Δ⋅(Afix Γ⋅ae) = ABinds Δ⋅ae"
proof (induct Δ rule: ABinds.induct)
  case 1 show ?case by (simp add: Afix_above_arg del: fun_meet_simp)
next
  case (2 v e Δ)
  from 2(2)
  have "atom v ♯ Γ" and  "atom ` domA (delete v Δ) ♯* Γ"
    by (auto simp add: fresh_star_def)
  from 2(1)[OF this(2)]
  show ?case by (simp del: fun_meet_simp add: Afix_lookup_fresh[OF ‹atom v ♯ Γ›])
qed

lemma Afix_append_fresh:
  assumes "atom ` domA Δ ♯* Γ"
  shows "Afix (Δ @ Γ)⋅ae = Afix Γ⋅(Afix Δ⋅ae)"
proof (rule below_antisym)
  show *: "Afix (Δ @ Γ)⋅ae ⊑ Afix Γ⋅(Afix Δ⋅ae)"
  apply (rule Afix_least_below)
  apply (simp add: Abinds_append_disjoint[OF fresh_distinct[OF assms]] Afix_comp2join_fresh[OF assms])
  apply (rule below_trans[OF join_mono[OF Abinds_Afix_below Abinds_Afix_below]])
  apply (simp_all add: Afix_above_arg  below_trans[OF Afix_above_arg Afix_above_arg])
  done
next
  show "Afix Γ⋅(Afix Δ⋅ae) ⊑ Afix (Δ @ Γ)⋅ae"
  proof (rule Afix_least_below)
    show "ABinds Γ⋅(Afix (Δ @ Γ)⋅ae) ⊑ Afix (Δ @ Γ)⋅ae"
      apply (rule below_trans[OF _ Abinds_Afix_below])
      apply (subst Abinds_append_disjoint[OF fresh_distinct[OF assms]])
      apply simp
      done
    have "ABinds Δ⋅(Afix (Δ @ Γ)⋅ae) ⊑ Afix (Δ @ Γ)⋅ae"
      apply (rule below_trans[OF _ Abinds_Afix_below])
      apply (subst Abinds_append_disjoint[OF fresh_distinct[OF assms]])
      apply simp
      done
    thus "Afix Δ⋅ae ⊑ Afix (Δ @ Γ)⋅ae"
      apply (rule Afix_least_below)
      apply (rule Afix_above_arg)
      done
  qed
qed


lemma Afix_e_to_heap:
   "Afix (delete x Γ)⋅(fup⋅(Aexp e)⋅n ⊔ ae) ⊑ Afix ((x, e) # delete x Γ)⋅(esing x⋅n ⊔ ae)"
    apply (simp add: Afix_eq)
    apply (rule fix_least_below, simp)
    apply (intro join_below)
    apply (subst fix_eq, simp)
    apply (subst fix_eq, simp)

    apply (rule below_trans[OF _ join_above2])
    apply (rule below_trans[OF _ join_above2])
    apply (rule below_trans[OF _ join_above2])
    apply (rule monofun_cfun_arg)
    apply (subst fix_eq, simp)
      
    apply (subst fix_eq, simp) back apply (simp add: below_trans[OF _ join_above2])
    done

lemma Afix_e_to_heap':
   "Afix (delete x Γ)⋅(Aexp e⋅n) ⊑ Afix ((x, e) # delete x Γ)⋅(esing x⋅(up⋅n))"
using Afix_e_to_heap[where ae = ⊥ and n = "up⋅n"] by simp

end


end