Theory NoCardinalityAnalysis

theory NoCardinalityAnalysis
imports CardinalityAnalysisSpec ArityAnalysisStack
begin

locale NoCardinalityAnalysis = ArityAnalysisLetSafe +
  assumes Aheap_thunk: "x ∈ thunks Γ ⟹ (Aheap Γ e⋅a) x = up⋅0"
begin

definition a2c :: "Arity⇩⊥ → two" where "a2c = (Λ a. if a ⊑ ⊥ then ⊥ else many)"
lemma a2c_simp: "a2c⋅a = (if a ⊑ ⊥ then ⊥ else many)"
  unfolding a2c_def by (rule beta_cfun[OF cont_if_else_above]) auto


lemma a2c_eqvt[eqvt]: "π ∙ a2c = a2c"
  unfolding a2c_def
  apply perm_simp
  apply (rule Abs_cfun_eqvt)
  apply (rule cont_if_else_above)
  apply auto
  done

definition ae2ce :: "AEnv ⇒ (var ⇒ two)" where "ae2ce ae x = a2c⋅(ae x)"

lemma ae2ce_cont: "cont ae2ce"
  by (auto simp add: ae2ce_def) 
lemmas cont_compose[OF ae2ce_cont, cont2cont, simp]

lemma ae2ce_eqvt[eqvt]: "π ∙ ae2ce ae x = ae2ce (π ∙ ae) (π ∙ x)"
  unfolding ae2ce_def by perm_simp rule

lemma ae2ce_to_env_restr: "ae2ce ae = (λ_ . many) f|` edom ae"
  by (auto simp add: ae2ce_def lookup_env_restr_eq edom_def a2c_simp)

lemma edom_ae2ce[simp]: "edom (ae2ce ae) = edom ae"
  unfolding edom_def
  by (auto simp add: ae2ce_def  a2c_simp)


definition cHeap :: "heap ⇒ exp ⇒ Arity → (var ⇒ two)"
  where "cHeap Γ e = (Λ a. ae2ce (Aheap Γ e⋅a))"
lemma cHeap_simp[simp]: "cHeap Γ e⋅a = ae2ce (Aheap Γ e⋅a)"
  unfolding cHeap_def by simp

sublocale CardinalityHeap cHeap.

sublocale CardinalityHeapSafe cHeap Aheap
  apply standard
  apply (erule Aheap_thunk)
  apply simp
  done

fun prognosis where 
  "prognosis ae as a (Γ, e, S) = ((λ_. many) f|` (edom (ABinds Γ⋅ae) ∪ edom (Aexp e⋅a) ∪ edom (AEstack as S)))"

lemma record_all_noop[simp]:
  "record_call x⋅((λ_. many) f|` S) = (λ_. many) f|` S"
  by (auto simp add: record_call_def lookup_env_restr_eq)

lemma const_on_restr_constI[intro]:
  "S' ⊆ S ⟹ const_on ((λ _. x) f|` S) S' x"
  by fastforce

lemma ap_subset_edom_AEstack: "ap S ⊆ edom (AEstack as S)"
  by (induction as S rule:AEstack.induct) (auto simp del: fun_meet_simp)
  

sublocale CardinalityPrognosis prognosis.

sublocale CardinalityPrognosisShape prognosis
proof (standard, goal_cases)
  case 1
  thus ?case by (simp cong: Abinds_env_restr_cong)
next
  case 2
  thus ?case by (simp cong: Abinds_reorder)
next
  case 3
  thus ?case by (auto dest: set_mp[OF ap_subset_edom_AEstack])
next
  case 4
  thus ?case by (auto intro: env_restr_mono2 )
next
  case (5 ae x as a Γ e S)
  from `ae x = ⊥`
  have "ABinds (delete x Γ)⋅ae = ABinds Γ⋅ae" by (rule ABinds_delete_bot)
  thus ?case by simp
next
  case (6 ae as a Γ x S)
  from Aexp_Var[where n = a and x = x]
  have "(Aexp (Var x)⋅a) x ≠ ⊥" by auto
  hence "x ∈ edom (Aexp (Var x)⋅a)" by (simp add: edomIff)
  thus ?case by simp
qed

sublocale CardinalityPrognosisApp prognosis
proof (standard, goal_cases)
  case 1
  thus ?case
    using edom_mono[OF Aexp_App] by (auto intro!: env_restr_mono2)
qed

sublocale CardinalityPrognosisLam prognosis
proof (standard, goal_cases)
  case (1 ae as a Γ e y x S)
  have "edom (Aexp e[y::=x]⋅(pred⋅a)) ⊆ insert x (edom (env_delete y (Aexp e⋅(pred⋅a))))"
    by (auto dest: set_mp[OF edom_mono[OF Aexp_subst]] )
  also have "… ⊆ insert x (edom (Aexp (Lam [y]. e)⋅a))"
    using edom_mono[OF Aexp_Lam] by auto
  finally show ?case by (auto intro!: env_restr_mono2)
qed

sublocale CardinalityPrognosisVar prognosis
proof (standard, goal_cases)
  case prems: 1
  thus ?case by (auto intro!: env_restr_mono2 simp add: Abinds_reorder1[OF prems(1)])
next
  case prems: 2
  thus ?case
    by (auto intro!: env_restr_mono2 simp add: Abinds_reorder1[OF prems(1)])
       (metis Aexp_Var edomIff not_up_less_UU)
next
  case (3 e x Γ ae as S)
  have "fup⋅(Aexp e)⋅(ae x) ⊑ Aexp e⋅0" by (cases "ae x") (auto intro: monofun_cfun_arg)
  from edom_mono[OF this]
  show ?case by (auto intro!: env_restr_mono2 dest: set_mp[OF edom_mono[OF ABinds_delete_below]])
qed

sublocale CardinalityPrognosisIfThenElse prognosis
proof (standard, goal_cases)
  case (1 ae a as Γ scrut e1 e2 S)
  have "edom (Aexp scrut⋅0 ⊔ Aexp e1⋅a ⊔ Aexp e2⋅a) ⊆ edom (Aexp (scrut ? e1 : e2)⋅a)"
    by (rule edom_mono[OF Aexp_IfThenElse])
  thus ?case
    by (auto intro!: env_restr_mono2)
next
  case (2 ae as a Γ b e1 e2 S)
  show ?case by (auto intro!: env_restr_mono2)
qed

  
sublocale CardinalityPrognosisLet prognosis  cHeap Aheap
proof (standard, goal_cases)
  case prems: (1 Δ Γ S ae e a as)

  from set_mp[OF prems(3)] fresh_distinct[OF prems(1)] fresh_distinct_fv[OF prems(2)]
  have  "ae f|` domA Δ = ⊥"
    by (auto dest: set_mp[OF ups_fv_subset])
  hence [simp]: "ABinds Δ⋅(ae ⊔ Aheap Δ e⋅a) = ABinds Δ⋅(Aheap Δ e⋅a)" by (simp cong: Abinds_env_restr_cong add: env_restr_join)

  from  fresh_distinct[OF prems(1)]
  have "Aheap Δ e⋅a f|` domA Γ = ⊥" by (auto dest!: set_mp[OF edom_Aheap])
  hence [simp]: "ABinds Γ⋅(ae ⊔ Aheap Δ e⋅a) = ABinds Γ⋅ae" by (simp cong: Abinds_env_restr_cong add: env_restr_join)
  
  have "edom (ABinds (Δ @ Γ)⋅(Aheap Δ e⋅a ⊔ ae)) ∪ edom (Aexp e⋅a)  = edom (ABinds Δ⋅(Aheap Δ e⋅a)) ∪ edom (ABinds Γ⋅ae) ∪  edom (Aexp e⋅a) "
    by (simp add: Abinds_append_disjoint[OF fresh_distinct[OF prems(1)]] Un_commute)
  also have "… = edom (ABinds Γ⋅ae) ∪ edom (ABinds Δ⋅(Aheap Δ e⋅a) ⊔ Aexp e⋅a)"
    by force
  also have "… ⊆ edom (ABinds Γ⋅ae) ∪ edom (Aheap Δ e⋅a ⊔ Aexp (Let Δ e)⋅a)"
    using  edom_mono[OF Aexp_Let] by force
  also have "… = edom (Aheap Δ e⋅a) ∪ edom (ABinds Γ⋅ae) ∪ edom (Aexp (Let Δ e)⋅a)"
    by auto
  finally
  have "edom (ABinds (Δ @ Γ)⋅(Aheap Δ e⋅a ⊔ ae)) ∪ edom (Aexp e⋅a) ⊆ edom (Aheap Δ e⋅a) ∪ edom (ABinds Γ⋅ae) ∪ edom (Aexp (Let Δ e)⋅a)".
  hence "edom (ABinds (Δ @ Γ)⋅(Aheap Δ e⋅a ⊔ ae)) ∪ edom (Aexp e⋅a) ∪ edom (AEstack as S) ⊆ edom (Aheap Δ e⋅a) ∪ edom (ABinds Γ⋅ae) ∪ edom (Aexp (Let Δ e)⋅a) ∪ edom (AEstack as S)" by auto
  thus ?case by (simp add: ae2ce_to_env_restr env_restr_join2 Un_assoc[symmetric] env_restr_mono2)
qed

sublocale CardinalityPrognosisEdom prognosis
  by standard (auto dest: set_mp[OF Aexp_edom] set_mp[OF ap_fv_subset] set_mp[OF edom_AnalBinds]  set_mp[OF edom_AEstack])


sublocale CardinalityPrognosisSafe prognosis cHeap Aheap Aexp..
end

end