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 ea  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_app1:
  "a_consistent (ae, a, as) (Γ, App e x, S)  a_consistent (ae, inca, 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_app2:
  assumes "a_consistent (ae, a, as) (Γ, (Lam [y]. e), Arg x # S)"
  shows "a_consistent (ae, (preda), as) (Γ, e[y::=x], S)"
proof-
  have "Aexp (e[y::=x])(preda) f|` (domA Γ  upds S)   (env_delete y ((Aexp e)(preda))  esing x(up0)) f|` (domA Γ  upds S)" by (rule env_restr_mono[OF Aexp_subst])
  also have " =  env_delete y ((Aexp e)(preda)) f|` (domA Γ  upds S)  esing x(up0) f|` (domA Γ  upds S)" by (simp add: env_restr_join)
  also have "env_delete y ((Aexp e)(preda))  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(up0) f|` (domA Γ  upds S)  ae" using assms
    by (cases "xedom 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])(preda) 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 = up0"
  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 = up0
  have "ABinds (delete x Γ)ae  Aexp e0 = 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 e0  AEstack as S) f|` (domA Γ  upds S)  ae" by simp
  then
  show ?thesis
     using ae x = up0 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 = upu"
  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  upu" 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 = upu
  have "ABinds (delete x Γ)ae  Aexp eu = 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 eu  AEstack as S) f|` (domA Γ  upds S)  ae" by simp
  hence "((ABinds (delete x Γ))(env_delete x ae)  Aexp eu  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 eu  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 eu  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 = upu 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 = upu"
  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  upu" 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 = upu
  have "ABinds ((x,e) # delete x Γ)ae  Aexp eu = 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 eu  AEstack as S) f|` (domA Γ  upds S)  ae" by simp
  then
  show ?thesis
     using ae x = upu 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_var2: "a_consistent (ae, a, as) ((x, e) # Γ, e, S)" 
    and a_consistent_UpdD: "ae x = up0""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 Δ ea  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 Δ ea  ae) = ABinds Δ(Aheap Δ ea)"
    by (rule Abinds_env_restr_cong) (simp add: env_restr_join)

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

  have [simp]: "ABinds Γ(Aheap Δ ea  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 Δ ea f|` (domA Δ  domA Γ  upds S) = Aheap Δ ea "
    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 Δ ea)  Aexp ea  Aheap Δ ea  Aexp (Let Δ e)a" by (rule Aexp_Let)
  ultimately
  have "(ABinds (Δ @ Γ)(Aheap Δ ea  ae)  Aexp ea  AEstack as S) f|` (domA (Δ@Γ)  upds S)  Aheap Δ ea  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_if1:
  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 scrut0  Aexp e1a  Aexp e2a) 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_if2:
  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