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