Theory ArityTransformSafe

theory ArityTransformSafe
imports ArityTransform ArityConsistent ArityAnalysisSpec ArityEtaExpansionSafe AbstractTransform ConstOn
begin

locale CardinalityArityTransformation = ArityAnalysisLetSafeNoCard
begin
  sublocale AbstractTransformBoundSubst
    "λ a . inc⋅a"
    "λ a . pred⋅a"
    "λ Δ e a . (a, Aheap Δ e⋅a)"
    "fst"
    "snd"
    "λ _. 0"
    "Aeta_expand"
    "snd"
  apply standard
  apply (simp add: Aheap_subst)
  apply (rule subst_Aeta_expand)
  done

  abbreviation ccTransform where "ccTransform ≡ transform"

  lemma supp_transform: "supp (transform a e) ⊆ supp e"
    by (induction rule: transform.induct)
       (auto simp add: exp_assn.supp Let_supp dest!: set_mp[OF supp_map_transform] set_mp[OF supp_map_transform_step] )
  interpretation supp_bounded_transform transform
    by standard (auto simp add: fresh_def supp_transform) 

  fun transform_alts :: "Arity list ⇒ stack ⇒ stack"
    where 
      "transform_alts _ [] = []"
    | "transform_alts (a#as) (Alts e1 e2 # S) = (Alts (ccTransform a e1) (ccTransform a e2)) # transform_alts as S"
    | "transform_alts as (x # S) = x # transform_alts as S"

  lemma transform_alts_Nil[simp]: "transform_alts [] S = S"
    by (induction  S) auto

  lemma Astack_transform_alts[simp]:
    "Astack (transform_alts as S) = Astack S"
   by (induction rule: transform_alts.induct) auto

  lemma fresh_star_transform_alts[intro]: "a ♯* S ⟹ a ♯* transform_alts as S"
   by (induction as S  rule: transform_alts.induct) (auto simp add: fresh_star_Cons)

  fun a_transform :: "astate ⇒ conf ⇒ conf"
  where "a_transform (ae, a, as) (Γ, e, S) =
    (map_transform Aeta_expand ae (map_transform ccTransform ae Γ), 
     ccTransform a e,
     transform_alts as  S)"

  fun restr_conf :: "var set ⇒ conf ⇒ conf"
    where "restr_conf V (Γ, e, S) = (restrictA V Γ, e, restr_stack V S)"

  inductive consistent :: "astate ⇒ conf ⇒ bool" where
    consistentI[intro!]: 
    "a_consistent (ae, a, as) (Γ, e, S)
    ⟹ (⋀ x. x ∈ thunks Γ ⟹  ae x = up⋅0)
    ⟹ consistent (ae, a, as) (Γ, e, S)"  
  inductive_cases consistentE[elim!]: "consistent (ae, a, as) (Γ, e, S)"

  lemma closed_consistent:
    assumes "fv e = ({}::var set)"
    shows "consistent (⊥, 0, []) ([], e, [])"
  by (auto simp add: edom_empty_iff_bot closed_a_consistent[OF assms])

  lemma arity_tranform_safe:
    fixes c c'
    assumes "c ⇒⇧* c'" and "¬ boring_step c'" and "heap_upds_ok_conf c" and "consistent (ae,a,as) c"
    shows "∃ae' a' as'. consistent (ae',a',as') c' ∧ a_transform (ae,a,as) c ⇒⇧* a_transform (ae',a',as') c'"
  using assms(1,2) heap_upds_ok_invariant assms(3-)
  proof(induction c c' arbitrary: ae a as rule:step_invariant_induction)
  case (app⇩1 Γ e x S)
    from app⇩1 have "consistent (ae, inc⋅a, as) (Γ, e, Arg x # S)"
      by (auto intro: a_consistent_app⇩1)
    moreover
    have "a_transform (ae, a, as) (Γ, App e x, S) ⇒ a_transform (ae, inc⋅a, as) (Γ, e, Arg x # S)"
      by simp rule
    ultimately
    show ?case by (blast del: consistentI consistentE)
  next
  case (app⇩2 Γ y e x S)
    have "consistent (ae, pred⋅a, as) (Γ, e[y::=x], S)" using app⇩2
      by (auto 4 3 intro: a_consistent_app⇩2)
    moreover
    have "a_transform (ae, a, as) (Γ, Lam [y]. e, Arg x # S) ⇒ a_transform (ae, pred ⋅ a, as) (Γ, e[y::=x], S)" by (simp add: subst_transform[symmetric]) rule
    ultimately
    show ?case by (blast  del: consistentI consistentE)
  next
  case (thunk Γ x e S)
    hence "x ∈ thunks Γ" by auto
    hence [simp]: "x ∈ domA Γ" by (rule set_mp[OF thunks_domA])

    from `heap_upds_ok_conf (Γ, Var x, S)`
    have "x ∉ upds S"  by (auto dest!: heap_upds_okE)
    
    have "x ∈ edom ae" using thunk by auto
    have "ae x = up⋅0" using thunk `x ∈ thunks Γ` by (auto)

    have "a_consistent (ae, 0, as) (delete x Γ, e, Upd x # S)" using thunk `ae x = up⋅0`
      by (auto intro!: a_consistent_thunk_0 simp del: restr_delete)
    hence "consistent (ae, 0, as) (delete x Γ, e, Upd x # S)" using thunk `ae x = up⋅0` 
      by (auto simp add:  restr_delete_twist)
    moreover
  
    from  `map_of Γ x = Some e` `ae x = up⋅0`
    have "map_of (map_transform Aeta_expand ae (map_transform ccTransform ae Γ)) x = Some (transform 0 e)"
      by (simp add: map_of_map_transform)
    with `¬ isVal e`
    have "a_transform (ae, a, as) (Γ, Var x, S) ⇒ a_transform (ae, 0, as) (delete x Γ, e, Upd x # S)"
      by (auto simp add: map_transform_delete restr_delete_twist intro!: step.intros  simp del: restr_delete)
    ultimately
    show ?case by (blast del: consistentI consistentE)
  next
  case (lamvar Γ x e S)
    from lamvar(1) have [simp]: "x ∈ domA Γ" by (metis domI dom_map_of_conv_domA)

    have "up⋅a ⊑ (Aexp (Var x)⋅a f|` (domA Γ ∪ upds S)) x"
      by (simp) (rule Aexp_Var)
    also from lamvar have "Aexp (Var x)⋅a f|` (domA Γ ∪ upds S) ⊑ ae" by (auto simp add: join_below_iff env_restr_join a_consistent.simps)
    finally
    obtain u where "ae x = up⋅u" by (cases "ae x") (auto simp add: edom_def)
    hence "x ∈ edom ae" by (auto simp add: edomIff)

    have "a_consistent (ae, u, as) ((x,e) # delete x Γ, e, S)" using lamvar `ae x = up⋅u`
      by (auto intro!: a_consistent_lamvar simp del: restr_delete)
    hence "consistent (ae, u, as) ((x, e) # delete x Γ, e, S)"
      using lamvar by (auto simp add:  thunks_Cons restr_delete_twist elim: below_trans)
    moreover

    from `a_consistent _ _`
    have "Astack (transform_alts as S) ⊑ u" by (auto elim: a_consistent_stackD)
  
    {
    from `isVal e`
    have "isVal (transform u e)" by simp
    hence "isVal (Aeta_expand u (transform u e))" by (rule isVal_Aeta_expand)
    moreover
    from  `map_of Γ x = Some e`  `ae x = up ⋅ u`  `isVal (transform u e)`
    have "map_of (map_transform Aeta_expand ae (map_transform transform ae Γ)) x = Some (Aeta_expand u (transform u e))"
      by (simp add: map_of_map_transform)
    ultimately
    have "a_transform (ae, a, as) (Γ, Var x, S) ⇒⇧*
          ((x, Aeta_expand u (transform u e)) # delete x (map_transform Aeta_expand ae (map_transform transform ae Γ)), Aeta_expand u (transform u e), transform_alts as S)"
       by (auto intro: lambda_var simp del: restr_delete)
    also have "… = ((map_transform Aeta_expand ae (map_transform transform ae ((x,e) # delete x Γ))), Aeta_expand u (transform u e), transform_alts as S)"
      using `ae x = up ⋅ u` `isVal (transform u e)`
      by (simp add: map_transform_Cons map_transform_delete  del: restr_delete)
    also(subst[rotated]) have "… ⇒⇧* a_transform (ae, u, as) ((x, e) # delete x Γ, e, S)"
      by (simp add: restr_delete_twist) (rule Aeta_expand_safe[OF `Astack _ ⊑ u`])
    finally(rtranclp_trans)
    have "a_transform (ae, a, as) (Γ, Var x, S) ⇒⇧* a_transform (ae, u, as) ((x, e) # delete x Γ, e, S)".
    }
    ultimately show ?case by (blast del: consistentI consistentE)
  next
  case (var⇩2 Γ x e S)
    from var⇩2
    have "a_consistent (ae, a, as) (Γ, e, Upd x # S)" by auto
    from a_consistent_UpdD[OF this]
    have "ae x = up⋅0" and "a = 0".

    have "a_consistent (ae, a, as) ((x, e) # Γ, e, S)"
      using var⇩2 by (auto intro!: a_consistent_var⇩2)
    hence "consistent (ae, 0, as) ((x, e) # Γ, e, S)"
      using var⇩2 `a = 0`
      by (auto simp add: thunks_Cons elim: below_trans)
    moreover
    have "a_transform (ae, a, as) (Γ, e, Upd x # S) ⇒ a_transform (ae, 0, as) ((x, e) # Γ, e, S)"
      using `ae x = up⋅0` `a = 0` var⇩2
      by (auto intro!: step.intros simp add: map_transform_Cons)
    ultimately show ?case by (blast del: consistentI consistentE)
  next
    case (let⇩1 Δ Γ e S)
    let ?ae = "Aheap Δ e⋅a"
  
    have "domA Δ ∩ upds S = {}" using fresh_distinct_fv[OF let⇩1(2)] by (auto dest: set_mp[OF ups_fv_subset])
    hence *: "⋀ x. x ∈ upds S ⟹ x ∉ edom ?ae" by (auto simp add:  dest!: set_mp[OF edom_Aheap])
    have restr_stack_simp2: "restr_stack (edom (?ae ⊔ ae)) S = restr_stack (edom ae) S"
      by (auto intro: restr_stack_cong dest!: *)

    have "edom ae ⊆ domA Γ ∪ upds S" using let⇩1 by (auto dest!: a_consistent_edom_subsetD)
    from set_mp[OF this] fresh_distinct[OF let⇩1(1)] fresh_distinct_fv[OF let⇩1(2)]
    have "edom ae ∩ domA Δ = {}" by (auto dest: set_mp[OF ups_fv_subset])

    {
    { fix x e'
      assume "x ∈ thunks Γ"
      with let⇩1
      have "(?ae ⊔ ae) x = up⋅0" by auto
    }
    moreover
    { fix x e'
      assume "x ∈ thunks Δ" 
      hence "(?ae ⊔ ae) x = up⋅0" by (auto simp add: Aheap_heap3)
    }
    moreover
    
    have "a_consistent (ae, a, as) (Γ, Let Δ e, S)"
      using let⇩1 by auto
    hence "a_consistent (?ae ⊔ ae, a, as) (Δ @ Γ, e, S)"
      using let⇩1(1,2) `edom ae ∩ domA Δ = {}` 
      by (auto intro!:  a_consistent_let simp del: join_comm)
    ultimately
    have "consistent (?ae ⊔ ae, a, as) (Δ @ Γ, e, S)"
      by auto
    }
    moreover
    {
      have "⋀ x. x ∈ domA Γ ⟹ x ∉ edom ?ae"
        using fresh_distinct[OF let⇩1(1)]
        by (auto dest!: set_mp[OF edom_Aheap])
      hence "map_transform Aeta_expand (?ae ⊔ ae) (map_transform transform (?ae ⊔ ae) Γ)
         = map_transform Aeta_expand ae (map_transform transform ae Γ)"
         by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
      moreover
  
      from `edom ae ⊆ domA Γ ∪ upds S`
      have  "⋀ x. x ∈ domA Δ ⟹ x ∉ edom ae"
         using fresh_distinct[OF let⇩1(1)] fresh_distinct_fv[OF let⇩1(2)] 
         by (auto dest!:  set_mp[OF ups_fv_subset])
      hence "map_transform Aeta_expand (?ae ⊔ ae) (map_transform transform (?ae ⊔ ae) Δ)
         = map_transform Aeta_expand ?ae (map_transform transform ?ae Δ)"
         by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
      ultimately
      
      
      have "a_transform (ae, a, as) (Γ, Let Δ e, S) ⇒ a_transform (?ae ⊔ ae,  a, as) (Δ @ Γ, e, S)"
        using restr_stack_simp2 let⇩1(1,2)
        apply (auto simp add: map_transform_append restrictA_append  restr_stack_simp2[simplified] map_transform_restrA)
        apply (rule step.let⇩1)
        apply (auto dest: set_mp[OF edom_Aheap])
        done
    }
    ultimately
    show ?case by (blast del: consistentI consistentE)
  next
    case (if⇩1 Γ scrut e1 e2 S)
    have "consistent (ae, 0, a#as) (Γ, scrut, Alts e1 e2 # S)"
      using if⇩1  by (auto dest: a_consistent_if⇩1)
    moreover
    have "a_transform (ae,  a, as) (Γ, scrut ? e1 : e2, S) ⇒ a_transform (ae, 0, a#as) (Γ, scrut, Alts e1 e2 # S)"
      by (auto intro: step.intros)
    ultimately
    show ?case by (blast del: consistentI consistentE)
  next
    case (if⇩2 Γ b e1 e2 S)
    hence "a_consistent (ae, a, as) (Γ, Bool b, Alts e1 e2 # S)" by auto
    then  obtain a' as' where [simp]: "as = a' # as'" "a = 0"
      by (rule a_consistent_alts_on_stack)

    have "consistent (ae, a', as') (Γ, if b then e1 else e2, S)" 
      using if⇩2 by (auto dest!: a_consistent_if⇩2)
    moreover
    have "a_transform (ae, a, as) (Γ, Bool b, Alts e1 e2 # S) ⇒ a_transform (ae,  a', as') (Γ, if b then e1 else e2, S)"
      by (auto intro: step.if⇩2[where b = True, simplified] step.if⇩2[where b = False, simplified])
    ultimately
    show ?case by (blast del: consistentI consistentE)
  next
    case refl thus ?case by auto
  next
    case (trans c c' c'')
      from trans(3)[OF trans(5)]
      obtain ae' a' as' where "consistent (ae', a', as') c'" and *: "a_transform (ae, a, as) c ⇒⇧* a_transform (ae', a', as') c'" by blast
      from trans(4)[OF this(1)]
      obtain ae'' a'' as'' where "consistent (ae'', a'', as'') c''" and **: "a_transform (ae', a', as') c' ⇒⇧* a_transform (ae'', a'', as'') c''" by blast
      from this(1) rtranclp_trans[OF * **]
      show ?case by blast
  qed
end

end