Theory Nominal-HOLCF

theory "Nominal-HOLCF"
imports
  "Nominal-Utils" "HOLCF-Utils"
begin

subsubsection ‹Type class of continuous permutations and variations thereof›

class cont_pt = 
  cpo + 
  pt +
  assumes perm_cont: "⋀p. cont ((permute p) :: 'a::{cpo,pt} ⇒ 'a)"

class discr_pt = 
  discrete_cpo + 
  pt

class pcpo_pt = 
  cont_pt + 
  pcpo

instance pcpo_pt ⊆ cont_pt
 by standard (auto intro: perm_cont)

instance discr_pt ⊆ cont_pt
 by standard auto

lemma (in cont_pt) perm_cont_simp[simp]: "π ∙ x ⊑ π ∙ y ⟷ x ⊑ y"
  apply rule
  apply (drule cont2monofunE[OF perm_cont, of _ _ "-π"], simp)[1]
  apply (erule cont2monofunE[OF perm_cont, of _ _ "π"])
  done

lemma (in cont_pt) perm_below_to_right: "π ∙ x ⊑ y ⟷ x ⊑ - π ∙  y"
  by (metis perm_cont_simp pt_class.permute_minus_cancel(2))
 
lemma perm_is_ub_simp[simp]: "π ∙ S <| π ∙ (x::'a::cont_pt) ⟷ S <| x"
  by (auto simp add: is_ub_def permute_set_def)

lemma perm_is_ub_eqvt[simp,eqvt]: "S <| (x::'a::cont_pt) ⟹ π ∙ S <| π ∙ x"
  by simp

lemma perm_is_lub_simp[simp]: "π ∙ S <<| π ∙ (x::'a::cont_pt) ⟷ S <<| x"
  apply (rule perm_rel_lemma)
  by (metis is_lubI is_lubD1 is_lubD2 perm_cont_simp perm_is_ub_simp)

lemma perm_is_lub_eqvt[simp,eqvt]: "S <<| (x::'a::cont_pt) ==> π ∙ S <<| π ∙ x"
  by simp

lemmas perm_cont2cont[simp,cont2cont] = cont_compose[OF perm_cont]

lemma perm_still_cont: "cont (π ∙ f) = cont (f :: ('a :: cont_pt) ⇒ ('b :: cont_pt))"
proof
  have imp:"⋀ (f :: 'a ⇒ 'b) π. cont f ⟹ cont (π ∙ f)"
    unfolding permute_fun_def
    by (metis cont_compose perm_cont)
  show "cont f ⟹ cont (π ∙ f)" using imp[of "f" "π"].
  show "cont (π ∙ f) ⟹ cont (f)" using imp[of "π ∙ f" "-π"] by simp
qed

lemma perm_bottom[simp,eqvt]: "π ∙ ⊥ = (⊥::'a::{cont_pt,pcpo})"
  proof-
  have "⊥ ⊑ -π ∙ (⊥::'a::{cont_pt,pcpo})" by simp
  hence "π ∙ ⊥ ⊑ π ∙ (-π ∙ (⊥::'a::{cont_pt,pcpo}))" by(rule cont2monofunE[OF perm_cont])
  hence "π ∙ ⊥ ⊑ (⊥::'a::{cont_pt,pcpo})" by simp
  thus "π ∙ ⊥ = (⊥::'a::{cont_pt,pcpo})" by simp
qed

lemma bot_supp[simp]: "supp (⊥ :: 'a :: pcpo_pt) = {}"
  by (rule supp_fun_eqvt) (simp add: eqvt_def)

lemma bot_fresh[simp]: "a ♯ (⊥ :: 'a :: pcpo_pt)"
  by (simp add: fresh_def)

lemma bot_fresh_star[simp]: "a ♯* (⊥ :: 'a :: pcpo_pt)"
  by (simp add: fresh_star_def)

lemma below_eqvt [eqvt]:
    "π ∙ (x ⊑ y) = (π ∙ x ⊑ π ∙ (y::'a::cont_pt))" by (auto simp add: permute_pure)

lemma lub_eqvt[simp]:
  "(∃ z. S <<| (z::'a::{cont_pt})) ⟹ π ∙ lub S = lub (π ∙ S)"
  by (metis lub_eqI perm_is_lub_simp)

lemma chain_eqvt[eqvt]:
  fixes F :: "nat ⇒ 'a::cont_pt"
  shows "chain F ⟹ chain (π ∙ F)"
  apply (rule chainI)
  apply (drule_tac i = i in chainE)
  apply (subst (asm) perm_cont_simp[symmetric, where π = π])
  by (metis permute_fun_app_eq permute_pure)

subsubsection ‹Instance for @{type cfun}›

instantiation "cfun" :: (cont_pt, cont_pt) pt
begin
  definition "p ∙ (f :: 'a  → 'b) = (Λ x. p ∙ (f ⋅ (- p ∙ x)))"

  instance
  apply standard
  apply (simp add: permute_cfun_def eta_cfun)
  apply (simp add: permute_cfun_def cfun_eqI minus_add)
  done
end

lemma permute_cfun_eq: "permute p = (λ f. (Abs_cfun (permute p)) oo f oo (Abs_cfun (permute (-p))))"
  by (rule, rule cfun_eqI, auto simp add: permute_cfun_def)

lemma Cfun_app_eqvt[eqvt]:
  "π ∙ (f ⋅ x) = (π ∙ f) ⋅ (π ∙ x)"
  unfolding permute_cfun_def
  by auto

lemma permute_Lam: "cont f ⟹ p ∙ (Λ x. f x) = (Λ x. (p ∙ f) x)"
  apply (rule cfun_eqI)
  unfolding permute_cfun_def
  by (metis Abs_cfun_inverse2 eqvt_lambda unpermute_def )

lemma Abs_cfun_eqvt: "cont f ⟹ (p ∙ Abs_cfun) f = Abs_cfun f"
  apply (subst permute_fun_def)
  by (metis permute_Lam perm_still_cont permute_minus_cancel(1))

lemma cfun_eqvtI: "(⋀x. p ∙ (f ⋅ x) = f' ⋅ (p ∙ x)) ⟹ p ∙ f = f'"
  by (metis Cfun_app_eqvt cfun_eqI permute_minus_cancel(1))

lemma ID_eqvt[eqvt]: "π ∙ ID = ID"
  unfolding ID_def
  apply perm_simp
  apply (simp add: Abs_cfun_eqvt)
  done

instance "cfun" :: (cont_pt, cont_pt) cont_pt
  by standard (subst permute_cfun_eq, auto)

instance "cfun" :: ("{pure,cont_pt}", "{pure,cont_pt}") pure
  by standard (auto  simp add: permute_cfun_def permute_pure Cfun.cfun.Rep_cfun_inverse)

instance "cfun" :: (cont_pt, pcpo_pt) pcpo_pt
  by standard

subsubsection ‹Instance for @{type fun}›

lemma permute_fun_eq: "permute p = (λ f. (permute p) ∘ f ∘ (permute (-p)))"
  by (rule, rule, metis comp_apply eqvt_lambda unpermute_def)

instance "fun" :: (pt, cont_pt) cont_pt
  apply standard
  apply (rule cont2cont_lambda)
  apply (subst permute_fun_def)
  apply (rule perm_cont2cont)
  apply (rule cont_fun)
  done

lemma fix_eqvt[eqvt]:
  "π ∙ fix = (fix :: ('a → 'a) → 'a::{cont_pt,pcpo})"
apply (rule cfun_eqI)
apply (subst permute_cfun_def)
apply simp
apply (rule parallel_fix_ind[OF adm_subst2])
apply (auto simp add: permute_self)
done

subsubsection ‹Instance for @{type u}›

(* Everything very pure. Does this work?
instantiation u :: (cpo) pt
begin
  definition "p ∙ (x :: 'a u) = x"
  instance by standard (auto simp add: permute_u_def)
end
instance u :: (cpo) pure by standard (simp add: permute_u_def)
instance u :: (cpo) cont_pt by standard (simp add: pure_permute_id)
instance u :: (cpo) pcpo_pt ..
*)


instantiation u :: (cont_pt) pt
begin
  definition "p ∙ (x :: 'a u) = fup⋅(Λ x. up⋅(p ∙ x))⋅x"
  instance
  apply standard
  apply (case_tac x) apply (auto simp add: permute_u_def)
  apply (case_tac x) apply (auto simp add: permute_u_def)
  done
end

instance u :: (cont_pt) cont_pt
proof
  fix p
  (* Fighting eta contraction... *)
  have "permute p = (λ x. fup⋅(Λ x. up⋅(p ∙ x))⋅(x:: 'a u))" 
    by (rule ext, rule permute_u_def)
  moreover have "cont (λ x. fup⋅(Λ x. up⋅(p ∙ x))⋅(x:: 'a u))" by simp
  ultimately show "cont (permute p :: 'a u ⇒ 'a u)" by simp
qed

instance u :: (cont_pt) pcpo_pt ..

class pure_cont_pt = pure + cont_pt

instance u :: (pure_cont_pt) pure
  apply standard
  apply (case_tac x)
  apply (auto simp add: permute_u_def permute_pure)
  done  


lemma up_eqvt[eqvt]: "π ∙ up = up"
  apply (rule cfun_eqI)
  apply (subst permute_cfun_def, simp)
  apply (simp add: permute_u_def)
  done

lemma fup_eqvt[eqvt]: "π ∙ fup = fup"
  apply (rule cfun_eqI)
  apply (rule cfun_eqI)
  apply (subst permute_cfun_def, simp)
  apply (subst permute_cfun_def, simp)
  apply (case_tac xa)
  apply simp
  apply (simp add: permute_self)
  done

subsubsection ‹Instance for @{type lift}›

instantiation lift :: (pt) pt
begin
  definition "p ∙ (x :: 'a lift) = case_lift ⊥ (λ x. Def (p ∙ x)) x"
  instance
  apply standard
  apply (case_tac x) apply (auto simp add: permute_lift_def)
  apply (case_tac x) apply (auto simp add: permute_lift_def)
  done
end

instance lift :: (pt) cont_pt
proof
  fix p
  (* Fighting eta contraction... *)
  have "permute p = (λ x. case_lift ⊥ (λ x. Def (p ∙ x)) (x::'a lift))" 
    by (rule ext, rule permute_lift_def)
  moreover have "cont (λ x. case_lift ⊥ (λ x. Def (p ∙ x)) (x::'a lift))" by simp
  ultimately show "cont (permute p :: 'a lift ⇒ 'a lift)" by simp
qed

instance lift :: (pt) pcpo_pt ..

instance lift :: (pure) pure
  apply standard
  apply (case_tac x)
  apply (auto simp add: permute_lift_def permute_pure)
  done  

lemma Def_eqvt[eqvt]: "π ∙ (Def x) = Def (π ∙ x)"
  by (simp add: permute_lift_def)

lemma case_lift_eqvt[eqvt]: "π ∙ case_lift d f x = case_lift (π ∙ d) (π ∙ f) (π ∙ x)"
  by (cases x) (auto simp add: permute_self)

subsubsection ‹Instance for @{type prod}›

instance prod :: (cont_pt, cont_pt) cont_pt
proof
  fix p
  (* Fighting eta contraction... *)
  have "permute p = (λ (x :: ('a, 'b) prod). (p ∙ fst x, p ∙ snd x))"  by auto
  moreover have "cont ..." by (intro cont2cont)
  ultimately show "cont (permute p :: ('a,'b) prod  ⇒ ('a,'b) prod)" by simp
qed


end