Theory CallArityEnd2EndSafe

theory CallArityEnd2EndSafe
imports CallArityEnd2End CardArityTransformSafe CoCallImplSafe CoCallImplTTreeSafe TTreeImplCardinalitySafe
theory CallArityEnd2EndSafe
imports CallArityEnd2End CardArityTransformSafe CoCallImplSafe CoCallImplTTreeSafe TTreeImplCardinalitySafe
begin

locale CallArityEnd2EndSafe
begin
sublocale CoCallImplSafe.
sublocale CallArityEnd2End.

abbreviation transform_syn' ("𝒯_") where "𝒯a ≡ transform a"

lemma end2end:
  "c ⇒* c' ⟹
  ¬ boring_step c' ⟹
  heap_upds_ok_conf c ⟹
  consistent (ae, ce, a, as, r) c ⟹
  ∃ae' ce' a' as' r'. consistent  (ae', ce', a', as', r') c' ∧ conf_transform  (ae, ce, a, as, r) c ⇒G* conf_transform  (ae', ce', a', as', r') c'"
  by (rule card_arity_transform_safe)

theorem end2end_closed:
  assumes closed: "fv e = ({} :: var set)"
  assumes "([], e, []) ⇒* (Γ,v,[])" and "isVal v"
  obtains Γ' and v'
  where "([], 𝒯0 e, []) ⇒* (Γ',v',[])" and "isVal v'"
    and "card (domA Γ') ≤ card (domA Γ)"
proof-
  note assms(2)
  moreover
  have "¬ boring_step (Γ,v,[])" by (simp add: boring_step.simps)
  moreover
  have "heap_upds_ok_conf ([], e, [])" by simp
  moreover
  have "consistent (⊥,⊥,0,[],[]) ([], e, [])" using closed by (rule closed_consistent)
  ultimately
  obtain ae ce a as r where
    *: "consistent  (ae, ce, a, as, r) (Γ,v,[])" and
    **: "conf_transform  (⊥, ⊥, 0, [], []) ([],e,[]) ⇒G* conf_transform (ae, ce, a, as, r) (Γ,v,[])"
    by (metis end2end)

  let ?Γ = "map_transform Aeta_expand ae (map_transform transform ae (restrictA (-set r) Γ))"
  let ?v = "transform a v"

  from * have "set r ⊆ domA Γ" by auto

  have "conf_transform  (⊥, ⊥, 0, [], []) ([],e,[]) = ([],transform 0 e,[])" by simp
  with **
  have "([], transform 0 e, []) ⇒G* (?Γ, ?v, map Dummy (rev r))" by simp

  have "isVal ?v" using `isVal v` by simp

  have "fv (transform 0 e) = ({} :: var set)" using closed
    by (auto dest: set_mp[OF fv_transform])

  note sestoftUnGC'[OF `([], transform 0 e, []) ⇒G* (?Γ, ?v, map Dummy (rev r))` `isVal ?v` `fv (transform 0 e) = {}`]
  then obtain Γ'
    where "([], transform 0 e, []) ⇒* (Γ', ?v, [])"
    and "?Γ = restrictA (- set r) Γ'"
    and "set r ⊆ domA Γ'"
    by auto

  have "card (domA Γ) = card (domA ?Γ ∪ (set r ∩ domA Γ))"
    by (rule arg_cong[where f = card]) auto
  also have "… = card (domA ?Γ) + card (set r ∩ domA Γ)"
    by (rule card_Un_disjoint) auto
  also note `?Γ = restrictA (- set r) Γ'`
  also have "set r ∩ domA Γ = set r ∩ domA Γ'"
    using `set r ⊆ domA Γ`  `set r ⊆ domA Γ'` by auto
  also have "card (domA (restrictA (- set r) Γ')) + card (set r ∩ domA Γ') = card (domA Γ')"
    by (subst card_Un_disjoint[symmetric]) (auto intro: arg_cong[where f = card])
  finally
  have "card (domA Γ') ≤ card (domA Γ)" by simp
  with `([], transform 0 e, []) ⇒* (Γ', ?v, [])`  `isVal ?v`
  show thesis using that by blast
qed

lemma fresh_var_eqE[elim_format]: "fresh_var e = x ⟹ x ∉  fv e"
  by (metis fresh_var_not_free)

lemma example1:
  fixes e :: exp
  fixes f g x y z :: var
  assumes Aexp_e: "⋀a. Aexp e⋅a = esing x⋅(up⋅a) ⊔ esing y⋅(up⋅a)"
  assumes ccExp_e: "⋀a. CCexp e⋅a = ⊥"
  assumes [simp]: "transform 1 e = e"
  assumes "isVal e"
  assumes disj: "y ≠ f" "y ≠ g" "x ≠ y" "z ≠ f" "z ≠ g" "y ≠ x"
  assumes fresh: "atom z ♯ e"
  shows "transform 1 (let y be  App (Var f) g in (let x be e in (Var x))) = 
         let y be (Lam [z]. App (App (Var f) g) z) in (let x be (Lam [z]. App e z) in (Var x))"
proof-
  from arg_cong[where f = edom, OF Aexp_e]
  have "x ∈ fv e" by simp (metis Aexp_edom' insert_subset)
  hence [simp]: "¬ nonrec [(x,e)]"
    by (simp add: nonrec_def)
 
  from `isVal e`
  have [simp]: "thunks [(x, e)] = {}"
    by (simp add: thunks_Cons)

  have [simp]: "CCfix [(x, e)]⋅(esing x⋅(up⋅1) ⊔ esing y⋅(up⋅1), ⊥) = ⊥"
    unfolding CCfix_def
    apply (simp add: fix_bottom_iff ccBindsExtra_simp)
    apply (simp add: ccBind_eq disj ccExp_e)
    done

  have [simp]: "Afix [(x, e)]⋅(esing x⋅(up⋅1)) = esing x⋅(up⋅1) ⊔ esing y⋅(up⋅1)"
    unfolding Afix_def
    apply simp
    apply (rule fix_eqI)
    apply (simp add: disj Aexp_e)
    apply (case_tac "z x")
    apply (auto simp add: disj Aexp_e)
    done

  have [simp]: "Aheap [(y, App (Var f) g)] (let x be e in Var x)⋅1 = esing y⋅((Aexp (let x be e in Var x )⋅1) y)"
    by (auto simp add:  Aheap_nonrec_simp ABind_nonrec_eq pure_fresh fresh_at_base disj)

  have [simp]: "(Aexp (let x be e in Var x)⋅1) = esing y⋅(up⋅1)"
    by (simp add: env_restr_join disj)
    
  have [simp]: "Aheap [(x, e)] (Var x)⋅1 = esing x⋅(up⋅1)"
    by (simp add: env_restr_join disj)

  have [simp]: "Aeta_expand 1 (App (Var f) g) = (Lam [z]. App (App (Var f) g) z)"
    apply (simp add: one_is_inc_zero del: exp_assn.eq_iff)
    apply (subst change_Lam_Variable[of z "fresh_var (App (Var f) g)"])
    apply (auto simp add: fresh_Pair fresh_at_base pure_fresh disj intro!: flip_fresh_fresh  elim!: fresh_var_eqE)
    done

  have [simp]: "Aeta_expand 1 e = (Lam [z]. App e z)"
    apply (simp add: one_is_inc_zero del: exp_assn.eq_iff)
    apply (subst change_Lam_Variable[of z "fresh_var e"])
    apply (auto simp add: fresh_Pair fresh_at_base pure_fresh disj fresh intro!: flip_fresh_fresh  elim!: fresh_var_eqE)
    done

  show ?thesis
    by (simp del: Let_eq_iff add: map_transform_Cons disj[symmetric])
qed


end
end