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 var2)
  finally show ?case.
next
case (Bool Γ b L S)
  show ?case..
next
case (IfThenElse Γ scrut L Δ b e1 e2 Θ z S)
  have "(Γ, scrut ? e1 : e2, S)  (Γ, scrut, Alts e1 e2 #S)"..
  also
  from IfThenElse.prems
  have prem1: "fv (Γ, scrut, Alts e1 e2 #S)  set L  domA Γ" by auto
  hence "(Γ, scrut, Alts e1 e2 #S) * (Δ, Bool b, Alts e1 e2 #S)"
    by (rule IfThenElse.IH)
  also
  have "(Δ, Bool b, Alts e1 e2 #S)  (Δ, if b then e1 else e2, S)"..
  also
  from prem1 reds_pres_closed[OF IfThenElse(1)] reds_doesnt_forget[OF IfThenElse(1)]
  have prem2: "fv (Δ, if b then e1 else e2, S)  set L  domA Δ"  by auto
  hence "(Δ, if b then e1 else e2, 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)*Tfinal  ( Γ e S. final = (Γ, e, S)  P Γ e S [] (Γ, e, S))  (Γ e S T Γ' e' S'. (Γ', e', S')*Tfinal  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]:
  "(pset (Γ[y::h=x]). f p)  (pset Γ. 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 (app1 e x)
      obtain T1 c3 c4 T2
      where "T' = T1 @ c4 # T2" and prem1: "(Γ, e, Arg x # S)b*T1c3" and "c3  c4" and prem2: " c4b*T2(Δ, z, S)"
        by (rule bal_consE[OF  bal _ T _[unfolded app1 trace_cons]]) (simp, rule)

      from T = _ T' = _ have "length T1 < length T" and "length T2 < length T" by auto

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

      
      from less(1)[OF length T1 < length T prem1[unfolded c3 = _ c4 = _]]
      have "Γ : e ⇓⇘upds_list SΔ' : Lam [y]. e'" by simp
      moreover
      from less(1)[OF length T2 < length T prem2[unfolded c3 = _ c4 = _] isVal z]
      have "Δ' : e'[y::=x] ⇓⇘upds_list SΔ : z" by simp
      ultimately
      show ?thesis unfolding app1
        by (rule reds_ApplicationI)
    next
    case (app2 y e x S')
      from conf' =_ S = _ # S' S  stack conf'
      have False by (auto simp add: extends_def)
      thus ?thesis..
    next
    case (var1 x e)
      obtain T1 c3 c4 T2
      where "T' = T1 @ c4 # T2" and prem1: "(delete x Γ, e, Upd x # S)b*T1c3" and "c3  c4" and prem2: "c4b*T2(Δ, z, S)"
        by (rule bal_consE[OF  bal _ T _[unfolded var1 trace_cons]]) (simp, rule)
      
      from T = _ T' = _ have "length T1 < length T" and "length T2 < length T" by auto

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

      from isVal z' and prem2[unfolded c4 = _]
      have "T2 = []" by (rule isVal_stops)
      with prem2 c4 = _
      have "z' = z" and "Δ = (x,z)#Δ'" by auto
          
      from less(1)[OF length T1 < length T prem1[unfolded c3 = _ c4 = _  z' = _]  isVal z]
      have "delete x Γ : e ⇓⇘x # upds_list SΔ' : z" by simp
      with map_of _ _ = _
      show ?thesis unfolding var1(1) Δ = _ by rule
    next
    case (var2 x S')
      from conf' = _ S = _ # S' S  stack conf'
      have False by (auto simp add: extends_def)
      thus ?thesis..
    next
    case (if1 scrut  e1 e2)
      obtain T1 c3 c4 T2
      where "T' = T1 @ c4 # T2" and prem1: "(Γ, scrut, Alts e1 e2 # S)b*T1c3" and "c3  c4" and prem2: "c4b*T2(Δ, z, S)"
        by (rule bal_consE[OF  bal _ T _[unfolded if1 trace_cons]])  (simp, rule)

      from T = _ T' = _ have "length T1 < length T" and "length T2 < length T" by auto

      from prem1 have "stack c3 = Alts e1 e2 # S" by (auto dest:  bal_stackD)
      moreover
      from prem2 have "stack c4 = S" by (auto dest: bal_stackD)
      moreover
      note c3  c4
      ultimately
      obtain Δ' b where "c3 = (Δ', Bool b, Alts e1 e2 # S)" and "c4 = (Δ', (if b then e1 else e2), S)"
        by (auto elim!: step.cases simp del: exp_assn.eq_iff)

      from less(1)[OF length T1 < length T prem1[unfolded c3 = _ c4 = _ ] isVal_Bool]
      have "Γ : scrut ⇓⇘upds_list SΔ' : Bool b" by simp
      moreover
      from less(1)[OF length T2 < length T prem2[unfolded c4 = _] isVal z]
      have "Δ' : (if b then e1 else e2) ⇓⇘upds_list SΔ : z".
      ultimately
      show ?thesis unfolding if1 by (rule reds.IfThenElse)
   next
    case (if2 b e1 e2 S')
      from conf' = _ S = _ # S' S  stack conf'
      have False by (auto simp add: extends_def)
      thus ?thesis..
    next
    case (let1 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 let1  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 e1 e2  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