Theory SestoftCorrect

theory SestoftCorrect
imports BalancedTraces Launchbury.Launchbury Sestoft
begin


lemma lemma_2:
  assumes "Γ : e ⇓⇘L⇙ Δ : z"
  and     "fv (Γ, e, S) ⊆ set L ∪ domA Γ"
  shows "(Γ, e, S) ⇒⇧* (Δ, z, S)"
using assms
proof(induction arbitrary: S  rule:reds.induct)
  case (Lambda Γ x e L)
  show ?case..
next
  case (Application y Γ e x L Δ Θ z e')
  from ‹fv (Γ, App e x, S) ⊆ set L ∪ domA Γ›
  have prem1: "fv (Γ, e, Arg x # S) ⊆ set L ∪ domA Γ" by simp
  
  from prem1 reds_pres_closed[OF ‹Γ : e ⇓⇘L⇙ Δ : Lam [y]. e'›] reds_doesnt_forget[OF ‹Γ : e ⇓⇘L⇙ Δ : Lam [y]. e'›]
  have prem2: "fv (Δ, e'[y::=x], S) ⊆ set L ∪ domA Δ" by (auto simp add: fv_subst_eq)

  have "(Γ, App e x, S) ⇒ (Γ, e, Arg x # S)"..
  also have "… ⇒⇧* (Δ, Lam [y]. e', Arg x# S)" by (rule Application.IH(1)[OF prem1])
  also have "… ⇒ (Δ, e'[y ::= x], S)"..
  also have "… ⇒⇧* (Θ, z, S)" by (rule Application.IH(2)[OF prem2])
  finally show ?case.
next
case (Variable Γ x e L Δ z S)
  from Variable(2)
  have "isVal z" by (rule result_evaluated)

  have "x ∉ domA Δ" by (rule reds_avoids_live[OF Variable(2), where x = x]) simp_all

  from ‹fv (Γ, Var x, S) ⊆ set L ∪ domA Γ›
  have prem: "fv (delete x Γ, e, Upd x # S) ⊆ set (x#L) ∪ domA (delete x Γ)"
    by (auto dest: subsetD[OF fv_delete_subset] subsetD[OF map_of_Some_fv_subset[OF ‹map_of Γ x = Some e›]])

  from ‹map_of Γ x = Some e›
  have "(Γ, Var x, S) ⇒ (delete x Γ, e, Upd x # S)"..
  also have "… ⇒⇧* (Δ, z, Upd x # S)" by (rule Variable.IH[OF prem])
  also have "… ⇒ ((x,z)#Δ, z, S)" using ‹x ∉ domA Δ› ‹isVal z› by (rule var⇩2)
  finally show ?case.
next
case (Bool Γ b L S)
  show ?case..
next
case (IfThenElse Γ scrut L Δ b e⇩1 e⇩2 Θ z S)
  have "(Γ, scrut ? e⇩1 : e⇩2, S) ⇒ (Γ, scrut, Alts e⇩1 e⇩2 #S)"..
  also
  from IfThenElse.prems
  have prem1: "fv (Γ, scrut, Alts e⇩1 e⇩2 #S) ⊆ set L ∪ domA Γ" by auto
  hence "(Γ, scrut, Alts e⇩1 e⇩2 #S) ⇒⇧* (Δ, Bool b, Alts e⇩1 e⇩2 #S)"
    by (rule IfThenElse.IH)
  also
  have "(Δ, Bool b, Alts e⇩1 e⇩2 #S) ⇒ (Δ, if b then e⇩1 else e⇩2, S)"..
  also
  from prem1 reds_pres_closed[OF IfThenElse(1)] reds_doesnt_forget[OF IfThenElse(1)]
  have prem2: "fv (Δ, if b then e⇩1 else e⇩2, S) ⊆ set L ∪ domA Δ"  by auto
  hence "(Δ, if b then e⇩1 else e⇩2, S) ⇒⇧* (Θ, z, S)" by (rule IfThenElse.IH(2))
  finally
  show ?case.
next
case (Let as Γ L body Δ z S)
  from Let(4)
  have prem: "fv (as @ Γ, body, S) ⊆ set L ∪ domA (as @ Γ)" by auto

  from Let(1) 
  have "atom ` domA as ♯* Γ" by (auto simp add: fresh_star_Pair)
  moreover
  from Let(1)
  have "domA as ∩ fv (Γ, L) = {}"
    by (rule fresh_distinct_fv)
  hence "domA as ∩ (set L ∪ domA Γ) = {}"
    by (auto dest: subsetD[OF domA_fv_subset])
  with Let(4)
  have "domA as ∩ fv S = {}"
    by auto
  hence "atom ` domA as ♯* S"
    by (auto simp add: fresh_star_def fv_def fresh_def)
  ultimately
  have "(Γ, Terms.Let as body, S) ⇒ (as@Γ, body, S)"..
  also have "… ⇒⇧* (Δ, z, S)"
    by (rule Let.IH[OF prem])
  finally show ?case.
qed

type_synonym trace = "conf list"

fun stack :: "conf ⇒ stack" where "stack (Γ, e, S) = S"
                 
interpretation traces step.

abbreviation trace_syn ("_ ⇒⇧*⇘_⇙ _" [50,50,50] 50) where "trace_syn ≡ trace"

lemma conf_trace_induct_final[consumes 1, case_names trace_nil trace_cons]:
  "(Γ, e, S) ⇒⇧*⇘T⇙ final ⟹ (⋀ Γ e S. final = (Γ, e, S) ⟹ P Γ e S [] (Γ, e, S)) ⟹ (⋀Γ e S T Γ' e' S'. (Γ', e', S') ⇒⇧*⇘T⇙ final ⟹ P Γ' e' S' T final ⟹ (Γ, e, S) ⇒ (Γ', e', S') ⟹ P Γ e S ((Γ', e', S') # T) final) ⟹ P Γ e S T final"
  by (induction "(Γ, e, S)" T final arbitrary: Γ e S rule: trace_induct_final) auto

interpretation balance_trace step  stack
  apply standard
  apply (erule step.cases)
  apply auto
  done

abbreviation bal_syn ("_ ⇒⇧b⇧*⇘_⇙ _" [50,50,50] 50) where "bal_syn ≡ bal"

lemma isVal_stops:
  assumes "isVal e"
  assumes "(Γ, e, S) ⇒⇧b⇧*⇘T⇙ (Δ, z, S)"
  shows "T=[]"
  using assms
  apply -
  apply (erule balE)
  apply (erule trace.cases)
  apply simp
  apply auto
  apply (auto elim!: step.cases)
  done

 
lemma Ball_subst[simp]:
  "(∀p∈set (Γ[y::h=x]). f p) ⟷ (∀p∈set Γ. case p of (z,e) ⇒ f (z, e[y::=x]))"
  by (induction Γ) auto

lemma lemma_3:
  assumes "(Γ, e, S) ⇒⇧b⇧*⇘T⇙ (Δ, z, S)"
  assumes "isVal z"
  shows "Γ : e ⇓⇘upds_list S⇙ Δ : z"
using assms
proof(induction T arbitrary: Γ e S Δ z rule: measure_induct_rule[where f = length])
  case (less T Γ e S Δ z)
  from ‹(Γ, e, S) ⇒⇧b⇧*⇘T⇙ (Δ, z, S)›
  have "(Γ, e, S) ⇒⇧*⇘T⇙ (Δ, z, S)" and "∀ c'∈set T. S ≲ stack c'" unfolding bal.simps by auto

  from this(1)
  show ?case
  proof(cases)
  case trace_nil
    from ‹isVal z›  trace_nil show ?thesis by (auto intro: reds_isValI)
  next
  case (trace_cons conf' T')
    from ‹T = conf' # T'› and ‹∀ c'∈set T. S ≲ stack c'› have "S ≲ stack conf'" by auto

    from ‹(Γ, e, S) ⇒ conf'›
    show ?thesis
    proof(cases)
    case (app⇩1 e x)
      obtain T⇩1 c⇩3 c⇩4 T⇩2
      where "T' = T⇩1 @ c⇩4 # T⇩2" and prem1: "(Γ, e, Arg x # S) ⇒⇧b⇧*⇘T⇩1⇙ c⇩3" and "c⇩3 ⇒ c⇩4" and prem2: " c⇩4 ⇒⇧b⇧*⇘T⇩2⇙ (Δ, z, S)"
        by (rule bal_consE[OF  ‹bal _ T _›[unfolded app⇩1 trace_cons]]) (simp, rule)

      from ‹T = _› ‹T' = _› have "length T⇩1 < length T" and "length T⇩2 < length T" by auto

      from prem1 have "stack c⇩3 =  Arg x # S" by (auto dest:  bal_stackD)
      moreover
      from prem2 have "stack c⇩4 = S" by (auto dest: bal_stackD)
      moreover
      note ‹c⇩3 ⇒ c⇩4›
      ultimately
      obtain Δ' y e' where "c⇩3 = (Δ', Lam [y]. e', Arg x # S)" and "c⇩4 = (Δ', e'[y ::= x], S)"
        by (auto elim!: step.cases simp del: exp_assn.eq_iff)

      
      from less(1)[OF ‹length T⇩1 < length T› prem1[unfolded ‹c⇩3 = _› ‹c⇩4 = _›]]
      have "Γ : e ⇓⇘upds_list S⇙ Δ' : Lam [y]. e'" by simp
      moreover
      from less(1)[OF ‹length T⇩2 < length T› prem2[unfolded ‹c⇩3 = _› ‹c⇩4 = _›] ‹isVal z›]
      have "Δ' : e'[y::=x] ⇓⇘upds_list S⇙ Δ : z" by simp
      ultimately
      show ?thesis unfolding app⇩1
        by (rule reds_ApplicationI)
    next
    case (app⇩2 y e x S')
      from ‹conf' =_› ‹S = _ # S'› ‹S ≲ stack conf'›
      have False by (auto simp add: extends_def)
      thus ?thesis..
    next
    case (var⇩1 x e)
      obtain T⇩1 c⇩3 c⇩4 T⇩2
      where "T' = T⇩1 @ c⇩4 # T⇩2" and prem1: "(delete x Γ, e, Upd x # S) ⇒⇧b⇧*⇘T⇩1⇙ c⇩3" and "c⇩3 ⇒ c⇩4" and prem2: "c⇩4 ⇒⇧b⇧*⇘T⇩2⇙ (Δ, z, S)"
        by (rule bal_consE[OF  ‹bal _ T _›[unfolded var⇩1 trace_cons]]) (simp, rule)
      
      from ‹T = _› ‹T' = _› have "length T⇩1 < length T" and "length T⇩2 < length T" by auto

      from prem1 have "stack c⇩3 = Upd x # S" by (auto dest:  bal_stackD)
      moreover
      from prem2 have "stack c⇩4 = S" by (auto dest: bal_stackD)
      moreover
      note ‹c⇩3 ⇒ c⇩4›
      ultimately
      obtain Δ' z' where "c⇩3 = (Δ', z', Upd x # S)" and "c⇩4 = ((x,z')#Δ', z', S)" and "isVal z'"
        by (auto elim!: step.cases simp del: exp_assn.eq_iff)

      from ‹isVal z'› and prem2[unfolded ‹c⇩4 = _›]
      have "T⇩2 = []" by (rule isVal_stops)
      with prem2 ‹c⇩4 = _›
      have "z' = z" and "Δ = (x,z)#Δ'" by auto
          
      from less(1)[OF ‹length T⇩1 < length T› prem1[unfolded ‹c⇩3 = _› ‹c⇩4 = _›  ‹z' = _›]  ‹isVal z›]
      have "delete x Γ : e ⇓⇘x # upds_list S⇙ Δ' : z" by simp
      with ‹map_of _ _ = _›
      show ?thesis unfolding var⇩1(1) ‹Δ = _› by rule
    next
    case (var⇩2 x S')
      from ‹conf' = _› ‹S = _ # S'› ‹S ≲ stack conf'›
      have False by (auto simp add: extends_def)
      thus ?thesis..
    next
    case (if⇩1 scrut  e⇩1 e⇩2)
      obtain T⇩1 c⇩3 c⇩4 T⇩2
      where "T' = T⇩1 @ c⇩4 # T⇩2" and prem1: "(Γ, scrut, Alts e⇩1 e⇩2 # S) ⇒⇧b⇧*⇘T⇩1⇙ c⇩3" and "c⇩3 ⇒ c⇩4" and prem2: "c⇩4 ⇒⇧b⇧*⇘T⇩2⇙ (Δ, z, S)"
        by (rule bal_consE[OF  ‹bal _ T _›[unfolded if⇩1 trace_cons]])  (simp, rule)

      from ‹T = _› ‹T' = _› have "length T⇩1 < length T" and "length T⇩2 < length T" by auto

      from prem1 have "stack c⇩3 = Alts e⇩1 e⇩2 # S" by (auto dest:  bal_stackD)
      moreover
      from prem2 have "stack c⇩4 = S" by (auto dest: bal_stackD)
      moreover
      note ‹c⇩3 ⇒ c⇩4›
      ultimately
      obtain Δ' b where "c⇩3 = (Δ', Bool b, Alts e⇩1 e⇩2 # S)" and "c⇩4 = (Δ', (if b then e⇩1 else e⇩2), S)"
        by (auto elim!: step.cases simp del: exp_assn.eq_iff)

      from less(1)[OF ‹length T⇩1 < length T› prem1[unfolded ‹c⇩3 = _› ‹c⇩4 = _› ] isVal_Bool]
      have "Γ : scrut ⇓⇘upds_list S⇙ Δ' : Bool b" by simp
      moreover
      from less(1)[OF ‹length T⇩2 < length T› prem2[unfolded ‹c⇩4 = _›] ‹isVal z›]
      have "Δ' : (if b then e⇩1 else e⇩2) ⇓⇘upds_list S⇙ Δ : z".
      ultimately
      show ?thesis unfolding if⇩1 by (rule reds.IfThenElse)
   next
    case (if⇩2 b e1 e2 S')
      from ‹conf' = _› ‹S = _ # S'› ‹S ≲ stack conf'›
      have False by (auto simp add: extends_def)
      thus ?thesis..
    next
    case (let⇩1 as e)
      from ‹T = conf' # T'› have "length T' < length T" by auto
      moreover
      have "(as @ Γ, e, S) ⇒⇧b⇧*⇘T'⇙ (Δ, z, S)" 
        using trace_cons ‹conf' = _›  ‹∀ c'∈set T. S ≲ stack c'› by fastforce
      moreover
      note ‹isVal z›
      ultimately
      have "as @ Γ : e ⇓⇘upds_list S⇙ Δ : z" by (rule less)
      moreover
      from ‹atom ` domA as ♯* Γ›  ‹atom ` domA as ♯* S›
      have "atom ` domA as ♯* (Γ, upds_list S)" by (auto simp add: fresh_star_Pair)
      ultimately
      show ?thesis unfolding let⇩1  by (rule reds.Let[rotated])
    qed
  qed
qed

lemma dummy_stack_extended:
  "set S ⊆  Dummy ` UNIV ⟹ x ∉ Dummy ` UNIV ⟹ (S ≲ x # S') ⟷  S ≲ S'"
  apply (auto simp add: extends_def)
  apply (case_tac S'')
  apply auto
  done

lemma[simp]: "Arg x ∉ range Dummy"  "Upd x ∉ range Dummy"   "Alts e⇩1 e⇩2 ∉ range Dummy" by auto

lemma dummy_stack_balanced:
  assumes "set S ⊆ Dummy ` UNIV"
  assumes "(Γ, e, S) ⇒⇧* (Δ, z, S)"
  obtains T where "(Γ, e, S) ⇒⇧b⇧*⇘T⇙ (Δ, z, S)"
proof-
  from build_trace[OF assms(2)]
  obtain T where "(Γ, e, S) ⇒⇧*⇘T⇙ (Δ, z, S)"..
  moreover
  hence "∀ c'∈set T. stack (Γ, e, S) ≲ stack c'"
    by (rule conjunct1[OF traces_list_all])
       (auto elim: step.cases simp add: dummy_stack_extended[OF ‹set S ⊆ Dummy ` UNIV›])
  ultimately
  have "(Γ, e, S) ⇒⇧b⇧*⇘T⇙ (Δ, z, S)"
    by (rule balI) simp
  thus ?thesis by (rule that)
qed

end