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--y∈G) = (π∙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