Theory CoCallGraph-Nominal

theory "CoCallGraph-Nominal"
imports CoCallGraph "Launchbury.Nominal-HOLCF"
begin

instantiation CoCalls :: pt
begin
  lift_definition permute_CoCalls :: "perm  CoCalls  CoCalls" is "permute"
    by (auto intro!: symI elim: symE simp add: mem_permute_set)
instance
  apply standard
  apply (transfer, simp)+
  done
end

instance CoCalls :: cont_pt
  apply standard
  apply (rule contI2)
  apply (rule monofunI)
  apply transfer
  apply (metis (full_types) True_eqvt subset_eqvt)
  apply (thin_tac "chain _")+
  apply transfer
  apply simp
  done

lemmas lub_eqvt[OF exists_lub, simp, eqvt]

lemma cc_restr_perm:
  fixes G :: CoCalls
  assumes "supp p ♯* S" and [simp]: "finite S"
  shows "cc_restr S (p  G) = cc_restr S G"
  using assms
  apply -
  apply transfer
  apply (auto simp add: mem_permute_set)
  apply (subst (asm) perm_supp_eq, simp add: supp_minus_perm, metis (full_types) fresh_def fresh_star_def supp_set_elem_finite)+
  apply assumption
  apply (subst perm_supp_eq, simp add: supp_minus_perm, metis (full_types) fresh_def fresh_star_def supp_set_elem_finite)+
  apply assumption
  done



lemma inCC_eqvt[eqvt]: "π  (x--yG) = (πx)--(πy)(πG)"
  by transfer auto
lemma cc_restr_eqvt[eqvt]: "π  cc_restr S G = cc_restr (π  S) (π  G)"
  by transfer (perm_simp, rule)
lemma ccProd_eqvt[eqvt]: "π  ccProd S S' = ccProd (π  S) (π   S')" 
  by transfer (perm_simp, rule)
lemma ccSquare_eqvt[eqvt]: "π  ccSquare S = ccSquare (π  S)"
  unfolding ccSquare_def
  by perm_simp rule
lemma ccNeighbors_eqvt[eqvt]: "π  ccNeighbors S G = ccNeighbors (π  S) (π  G)"
  by transfer (perm_simp, rule)


end