Theory ArityConsistent

theory ArityConsistent
imports  ArityAnalysisSpec  ArityStack ArityAnalysisStack
begin

context ArityAnalysisLetSafe
begin

type_synonym astate = "(AEnv × Arity × Arity list)"

inductive stack_consistent :: "Arity list ⇒ stack ⇒ bool"
  where 
    "stack_consistent [] []"
  | "Astack S ⊑ a ⟹ stack_consistent as S ⟹ stack_consistent (a#as) (Alts e1 e2 # S)"
  | "stack_consistent as S ⟹ stack_consistent as (Upd x # S)"
  | "stack_consistent as S ⟹ stack_consistent as (Arg x # S)"
inductive_simps stack_consistent_foo[simp]:
  "stack_consistent [] []" "stack_consistent (a#as) (Alts e1 e2 # S)" "stack_consistent as (Upd x # S)" "stack_consistent as (Arg x # S)"
inductive_cases [elim!]: "stack_consistent as (Alts e1 e2 # S)"

inductive a_consistent :: "astate ⇒ conf ⇒ bool" where
  a_consistentI:
  "edom ae ⊆ domA Γ ∪ upds S
  ⟹ Astack S ⊑ a
  ⟹ (ABinds Γ⋅ae ⊔ Aexp e⋅a ⊔ AEstack as S) f|` (domA Γ ∪ upds S) ⊑ ae
  ⟹ stack_consistent as S
  ⟹ a_consistent (ae, a, as) (Γ, e, S)"  
inductive_cases a_consistentE: "a_consistent (ae, a, as) (Γ, e, S)"

lemma a_consistent_restrictA:
  assumes "a_consistent (ae, a, as) (Γ, e, S)"
  assumes "edom ae ⊆ V"
  shows "a_consistent (ae, a, as) (restrictA V Γ, e, S)"
proof-
  have "domA Γ ∩ V ∪ upds S ⊆ domA Γ ∪ upds S" by auto
  note * = below_trans[OF env_restr_mono2[OF this]]
  
  show " a_consistent (ae, a, as) (restrictA V Γ, e, S)"
    using assms
    by (auto simp add: a_consistent.simps env_restr_join join_below_iff ABinds_restrict_edom
                  intro: * below_trans[OF env_restr_mono[OF ABinds_restrict_below]])
qed

lemma a_consistent_edom_subsetD:
  "a_consistent (ae, a, as) (Γ, e, S) ⟹ edom ae ⊆ domA Γ ∪ upds S"
  by (rule a_consistentE)

lemma a_consistent_stackD:
  "a_consistent (ae, a, as) (Γ, e, S) ⟹ Astack S ⊑ a"
  by (rule a_consistentE)


lemma a_consistent_app⇩1:
  "a_consistent (ae, a, as) (Γ, App e x, S) ⟹ a_consistent (ae, inc⋅a, as) (Γ, e, Arg x # S)"
  by (auto simp add: join_below_iff env_restr_join a_consistent.simps
           dest!: below_trans[OF env_restr_mono[OF Aexp_App]]
           elim: below_trans)

lemma a_consistent_app⇩2:
  assumes "a_consistent (ae, a, as) (Γ, (Lam [y]. e), Arg x # S)"
  shows "a_consistent (ae, (pred⋅a), as) (Γ, e[y::=x], S)"
proof-
  have "Aexp (e[y::=x])⋅(pred⋅a) f|` (domA Γ ∪ upds S)  ⊑ (env_delete y ((Aexp e)⋅(pred⋅a)) ⊔ esing x⋅(up⋅0)) f|` (domA Γ ∪ upds S)" by (rule env_restr_mono[OF Aexp_subst])
  also have "… =  env_delete y ((Aexp e)⋅(pred⋅a)) f|` (domA Γ ∪ upds S) ⊔ esing x⋅(up⋅0) f|` (domA Γ ∪ upds S)" by (simp add: env_restr_join)
  also have "env_delete y ((Aexp e)⋅(pred⋅a)) ⊑ Aexp (Lam [y]. e)⋅a" by (rule Aexp_Lam)
  also have "… f|` (domA Γ ∪ upds S) ⊑ ae" using assms  by (auto simp add: join_below_iff env_restr_join a_consistent.simps)
  also have "esing x⋅(up⋅0) f|` (domA Γ ∪ upds S) ⊑ ae" using assms
    by (cases "x∈edom ae") (auto simp add: env_restr_join join_below_iff a_consistent.simps)
  also have "ae ⊔ ae = ae" by simp
  finally
  have "Aexp (e[y::=x])⋅(pred⋅a) f|` (domA Γ ∪ upds S) ⊑ ae" by this simp_all
  thus ?thesis using assms
    by (auto elim: below_trans edom_mono  simp add: join_below_iff env_restr_join a_consistent.simps)
qed

lemma a_consistent_thunk_0:
  assumes "a_consistent (ae, a, as) (Γ, Var x, S)"
  assumes "map_of Γ x = Some e"
  assumes "ae x = up⋅0"
  shows "a_consistent (ae, 0, as) (delete x Γ, e, Upd x # S)"
proof-
  from assms(2)
  have [simp]: "x ∈ domA Γ" by (metis domI dom_map_of_conv_domA)

  from assms(3)
  have [simp]: "x ∈ edom ae" by (auto simp add: edom_def)

  have "x ∈ domA Γ" by (metis assms(2) domI dom_map_of_conv_domA)
  hence [simp]: "insert x (domA Γ - {x} ∪ upds S)  = (domA Γ ∪ upds S)"
    by auto

  from Abinds_reorder1[OF ‹map_of Γ x = Some e›] ‹ae x = up⋅0›
  have "ABinds (delete x Γ)⋅ae ⊔ Aexp e⋅0 = ABinds Γ⋅ae" by (auto intro: join_comm)
  moreover have "(… ⊔ AEstack as S) f|` (domA Γ ∪ upds S) ⊑ ae"
    using assms(1) by (auto simp add: join_below_iff env_restr_join a_consistent.simps)
  ultimately have "((ABinds (delete x Γ))⋅ae ⊔ Aexp e⋅0 ⊔ AEstack as S) f|` (domA Γ ∪ upds S) ⊑ ae" by simp
  then
  show ?thesis
     using ‹ae x = up⋅0› assms(1)
     by (auto simp add: join_below_iff env_restr_join  a_consistent.simps)
qed

lemma a_consistent_thunk_once:
  assumes "a_consistent (ae, a, as) (Γ, Var x, S)"
  assumes "map_of Γ x = Some e"
  assumes [simp]: "ae x = up⋅u"
  assumes "heap_upds_ok (Γ, S)"
  shows "a_consistent (env_delete x ae, u, as) (delete x Γ, e, S)"
proof-
  from assms(2)
  have [simp]: "x ∈ domA Γ" by (metis domI dom_map_of_conv_domA)

  from assms(1) have "Aexp (Var x)⋅a f|` (domA Γ ∪ upds S) ⊑ ae" by (auto simp add: join_below_iff env_restr_join a_consistent.simps)
  from fun_belowD[where x = x, OF this] 
  have "(Aexp (Var x)⋅a) x ⊑ up⋅u" by simp
  from below_trans[OF Aexp_Var this]
  have "a ⊑ u" by simp

  from ‹heap_upds_ok (Γ, S)›
  have "x ∉ upds S" by (auto simp add: a_consistent.simps elim!: heap_upds_okE)
  hence [simp]: "(- {x} ∩ (domA Γ ∪ upds S)) = (domA Γ - {x} ∪ upds S)" by auto

  have "Astack S ⊑ u" using assms(1) ‹a ⊑ u›
    by (auto elim: below_trans simp add: a_consistent.simps)
  
  from Abinds_reorder1[OF ‹map_of Γ x = Some e›] ‹ae x = up⋅u›
  have "ABinds (delete x Γ)⋅ae ⊔ Aexp e⋅u = ABinds Γ⋅ae" by (auto intro: join_comm)
  moreover
  have "(… ⊔ AEstack as S) f|` (domA Γ ∪ upds S) ⊑ ae"
    using assms(1) by (auto simp add: join_below_iff env_restr_join a_consistent.simps)
  ultimately
  have "((ABinds (delete x Γ))⋅ae ⊔ Aexp e⋅u ⊔ AEstack as S) f|` (domA Γ ∪ upds S) ⊑ ae" by simp
  hence "((ABinds (delete x Γ))⋅(env_delete x ae) ⊔ Aexp e⋅u ⊔ AEstack as S) f|` (domA Γ ∪ upds S) ⊑ ae"
    by (auto simp add: join_below_iff env_restr_join elim:  below_trans[OF env_restr_mono[OF monofun_cfun_arg[OF env_delete_below_arg]]])
  hence "env_delete x (((ABinds (delete x Γ))⋅(env_delete x ae) ⊔ Aexp e⋅u ⊔ AEstack as S) f|` (domA Γ ∪ upds S)) ⊑ env_delete x ae"
    by (rule env_delete_mono)
  hence "(((ABinds (delete x Γ))⋅(env_delete x ae) ⊔ Aexp e⋅u ⊔ AEstack as S) f|` (domA (delete x Γ) ∪ upds S)) ⊑ env_delete x ae"
    by (simp add: env_delete_restr)
  then
  show ?thesis
     using ‹ae x = up⋅u› ‹Astack S ⊑ u› assms(1)
     by (auto simp add: join_below_iff env_restr_join  a_consistent.simps elim : below_trans)
qed

lemma a_consistent_lamvar:
  assumes "a_consistent (ae, a, as) (Γ, Var x, S)"
  assumes "map_of Γ x = Some e"
  assumes [simp]: "ae x = up⋅u"
  shows "a_consistent (ae, u, as) ((x,e)# delete x Γ, e, S)"
proof-
  have [simp]: "x ∈ domA Γ" by (metis assms(2) domI dom_map_of_conv_domA)
  have [simp]: "insert x (domA Γ ∪ upds S) = (domA Γ ∪ upds S)" 
    by auto

  from assms(1) have "Aexp (Var x)⋅a f|` (domA Γ ∪ upds S) ⊑ ae" by (auto simp add: join_below_iff env_restr_join a_consistent.simps)
  from fun_belowD[where x = x, OF this] 
  have "(Aexp (Var x)⋅a) x ⊑ up⋅u" by simp
  from below_trans[OF Aexp_Var this]
  have "a ⊑ u" by simp

  have "Astack S ⊑ u" using assms(1) ‹a ⊑ u›
    by (auto elim: below_trans simp add: a_consistent.simps)
  
  from Abinds_reorder1[OF ‹map_of Γ x = Some e›] ‹ae x = up⋅u›
  have "ABinds ((x,e) # delete x Γ)⋅ae ⊔ Aexp e⋅u = ABinds Γ⋅ae" by (auto intro: join_comm)
  moreover
  have "(… ⊔ AEstack as S) f|` (domA Γ ∪ upds S) ⊑ ae"
    using assms(1) by (auto simp add: join_below_iff env_restr_join a_consistent.simps)
  ultimately
  have "((ABinds ((x,e) # delete x Γ))⋅ae ⊔ Aexp e⋅u ⊔ AEstack as S) f|` (domA Γ ∪ upds S) ⊑ ae" by simp
  then
  show ?thesis
     using ‹ae x = up⋅u› ‹Astack S ⊑ u› assms(1)
     by (auto simp add: join_below_iff env_restr_join  a_consistent.simps)
qed

lemma 
  assumes "a_consistent (ae, a, as) (Γ, e, Upd x # S)"
  shows a_consistent_var⇩2: "a_consistent (ae, a, as) ((x, e) # Γ, e, S)" 
    and a_consistent_UpdD: "ae x = up⋅0""a = 0"
    using assms
    by (auto simp add: join_below_iff env_restr_join a_consistent.simps 
               elim:below_trans[OF env_restr_mono[OF ABinds_delete_below]])

lemma a_consistent_let:
  assumes "a_consistent (ae, a, as) (Γ, Let Δ e, S)"
  assumes "atom ` domA Δ ♯* Γ"
  assumes "atom ` domA Δ ♯* S"
  assumes "edom ae ∩ domA Δ = {}"
  shows "a_consistent (Aheap Δ e⋅a ⊔ ae, a, as) (Δ @ Γ, e, S)"
proof-
  txt ‹
    First some boring stuff about scope:
›
  
  have [simp]: "⋀ S. S ⊆ domA Δ ⟹ ae f|` S = ⊥" using assms(4) by auto
  have [simp]: "ABinds Δ⋅(Aheap Δ e⋅a ⊔ ae) = ABinds Δ⋅(Aheap Δ e⋅a)"
    by (rule Abinds_env_restr_cong) (simp add: env_restr_join)

  have [simp]: "Aheap Δ e⋅a f|` domA Γ = ⊥"
    using fresh_distinct[OF assms(2)]
    by (auto intro: env_restr_empty dest!: subsetD[OF edom_Aheap])

  have [simp]: "ABinds Γ⋅(Aheap Δ e⋅a ⊔ ae) = ABinds Γ⋅ae"
    by (rule Abinds_env_restr_cong) (simp add: env_restr_join)

  have [simp]: "ABinds Γ⋅ae f|` (domA Δ ∪ domA Γ ∪ upds S)  = ABinds Γ⋅ae f|` (domA Γ ∪ upds S)" 
    using fresh_distinct_fv[OF assms(2)]
    by (auto intro: env_restr_cong dest!: subsetD[OF edom_AnalBinds])

  have [simp]: "AEstack as S f|` (domA Δ ∪ domA Γ ∪ upds S) = AEstack as S f|` (domA Γ ∪ upds S)" 
    using fresh_distinct_fv[OF assms(3)]
    by (auto intro: env_restr_cong dest!:  subsetD[OF edom_AEstack])

  have [simp]: "Aexp (Let Δ e)⋅a f|` (domA Δ ∪ domA Γ ∪ upds S) = Aexp (Terms.Let Δ e)⋅a f|` (domA Γ ∪ upds S)"
    by (rule env_restr_cong) (auto dest!: subsetD[OF Aexp_edom])
  
  have [simp]: "Aheap Δ e⋅a f|` (domA Δ ∪ domA Γ ∪ upds S) = Aheap Δ e⋅a "
    by (rule env_restr_useless) (auto dest!: subsetD[OF edom_Aheap])

  have "((ABinds Γ)⋅ae ⊔ AEstack as S) f|` (domA Γ ∪ upds S) ⊑ ae" using assms(1) by (auto simp add: a_consistent.simps join_below_iff env_restr_join)
  moreover
  have" Aexp (Let Δ e)⋅a f|` (domA Γ ∪ upds S) ⊑ ae"  using assms(1) by (auto simp add: a_consistent.simps join_below_iff env_restr_join)
  moreover
  have "ABinds Δ⋅(Aheap Δ e⋅a) ⊔ Aexp e⋅a ⊑ Aheap Δ e⋅a ⊔ Aexp (Let Δ e)⋅a" by (rule Aexp_Let)
  ultimately
  have "(ABinds (Δ @ Γ)⋅(Aheap Δ e⋅a ⊔ ae) ⊔ Aexp e⋅a ⊔ AEstack as S) f|` (domA (Δ@Γ) ∪ upds S) ⊑ Aheap Δ e⋅a ⊔ ae"
    by (auto 4 4 simp add: env_restr_join Abinds_append_disjoint[OF fresh_distinct[OF assms(2)]] join_below_iff
                 simp del: join_comm
                 elim: below_trans below_trans[OF env_restr_mono])
  moreover
  note fresh_distinct[OF assms(2)]
  moreover
  from fresh_distinct_fv[OF assms(3)]
  have  "domA Δ ∩ upds S = {}" by (auto dest!: subsetD[OF ups_fv_subset])
  ultimately
  show ?thesis using assms(1)
    by (auto simp add: a_consistent.simps dest!: subsetD[OF edom_Aheap] intro: heap_upds_ok_append)
qed

lemma a_consistent_if⇩1:
  assumes "a_consistent (ae, a, as) (Γ, scrut ? e1 : e2, S)"
  shows "a_consistent (ae, 0, a#as) (Γ, scrut, Alts e1 e2 # S)"
proof-
  from assms
  have "Aexp (scrut ? e1 : e2)⋅a f|` (domA Γ ∪ upds S) ⊑ ae" by (auto simp add: a_consistent.simps env_restr_join join_below_iff)
  hence "(Aexp scrut⋅0 ⊔ Aexp e1⋅a ⊔ Aexp e2⋅a) f|` (domA Γ ∪ upds S) ⊑ ae"
    by (rule below_trans[OF env_restr_mono[OF Aexp_IfThenElse]])
  thus ?thesis
    using assms
    by (auto simp add: a_consistent.simps join_below_iff env_restr_join)
qed

lemma a_consistent_if⇩2:
  assumes "a_consistent (ae, a, a'#as') (Γ, Bool b, Alts e1 e2 # S)"
  shows "a_consistent (ae, a', as') (Γ, if b then e1 else e2, S)"
using assms by (auto simp add: a_consistent.simps join_below_iff env_restr_join)

lemma a_consistent_alts_on_stack:
  assumes "a_consistent (ae, a, as) (Γ, Bool b, Alts e1 e2 # S)"
  obtains a' as' where "as = a' # as'" "a = 0"
using assms by (auto simp add: a_consistent.simps)

lemma closed_a_consistent:
  "fv e = ({}::var set) ⟹ a_consistent (⊥, 0, []) ([], e, [])"
  by (auto simp add: edom_empty_iff_bot a_consistent.simps  dest!: subsetD[OF Aexp_edom])

end

end