Theory CoCallGraph

theory CoCallGraph
imports "Vars" "HOLCF-Join-Classes" "HOLCF-Utils" "Set-Cpo"
begin

default_sort type

typedef CoCalls = "{G :: (var × var) set.  sym G}"
  morphisms Rep_CoCall Abs_CoCall
  by (auto intro: exI[where x = "{}"] symI)

setup_lifting type_definition_CoCalls

instantiation CoCalls :: po
begin
lift_definition below_CoCalls :: "CoCalls ⇒ CoCalls ⇒ bool" is "op ⊆".
instance
  apply standard
  apply ((transfer, auto)+)
  done
end

lift_definition coCallsLub :: "CoCalls set ⇒ CoCalls" is "λ S. ⋃ S"
  by (auto intro: symI elim: symE)

lemma coCallsLub_is_lub: "S <<| coCallsLub S"
proof (rule is_lubI)
  show "S <| coCallsLub S"
    by (rule is_ubI, transfer, auto)
next
  fix u
  assume "S <| u"
  hence "∀x ∈ S. x ⊑ u" by (auto dest: is_ubD)
  thus "coCallsLub S ⊑ u" by transfer auto
qed

instance CoCalls :: cpo
proof
  fix S :: "nat ⇒ CoCalls"
  show "∃x. range S <<| x" using coCallsLub_is_lub..
qed

lemma ccLubTransfer[transfer_rule]: "(rel_set pcr_CoCalls ===> pcr_CoCalls) Union lub"
proof-
  have "lub = coCallsLub"
    apply (rule)
    apply (rule lub_eqI)
    apply (rule coCallsLub_is_lub)
    done
  with coCallsLub.transfer
  show ?thesis by metis
qed

lift_definition is_cc_lub :: "CoCalls set ⇒ CoCalls ⇒ bool" is "(λ S x . x = Union S)".

lemma ccis_lubTransfer[transfer_rule]: "(rel_set pcr_CoCalls  ===> pcr_CoCalls ===> op =) (λ S x . x = Union S) op <<|"
proof-
  have "⋀ x xa . is_cc_lub x xa ⟷ xa = coCallsLub x" by transfer auto
  hence "is_cc_lub = op <<|"
  apply -
  apply (rule, rule)
  by (metis coCallsLub_is_lub is_lub_unique)
  thus ?thesis using is_cc_lub.transfer by simp
qed

lift_definition coCallsJoin :: "CoCalls ⇒ CoCalls  ⇒ CoCalls" is "op ∪"
    by (rule sym_Un)

lemma ccJoinTransfer[transfer_rule]: "(pcr_CoCalls ===> pcr_CoCalls ===> pcr_CoCalls) op ∪ op ⊔"
proof-
  have "op ⊔ = coCallsJoin"
    apply (rule)
    apply rule
    apply (rule lub_is_join)
    unfolding is_lub_def is_ub_def
    apply transfer
    apply auto
    done
  with coCallsJoin.transfer
  show ?thesis by metis
qed

lift_definition ccEmpty :: "CoCalls" is "{}" by (auto intro: symI)

lemma ccEmpty_below[simp]: "ccEmpty ⊑ G"
  by transfer auto

instance CoCalls :: pcpo
proof
  have "∀y . ccEmpty ⊑ y" by transfer simp
  thus "∃x. ∀y. (x::CoCalls) ⊑ y"..
qed

lemma ccBotTransfer[transfer_rule]: "pcr_CoCalls {} ⊥"
proof-
  have "⋀x. ccEmpty ⊑ x" by transfer simp
  hence "ccEmpty = ⊥" by (rule bottomI)
  thus ?thesis using ccEmpty.transfer by simp
qed

lemma cc_lub_below_iff:
  fixes G :: CoCalls
  shows "lub X ⊑ G ⟷ (∀ G'∈X. G' ⊑ G)" 
  by transfer auto

lift_definition ccField :: "CoCalls ⇒ var set" is Field.

lemma ccField_nil[simp]: "ccField ⊥ = {}"
  by transfer auto

lift_definition
  inCC :: "var ⇒ var ⇒ CoCalls ⇒ bool" ("_--_∈_" [1000, 1000, 900] 900)
  is "λ x y s. (x,y) ∈ s".

abbreviation
  notInCC :: "var ⇒ var ⇒ CoCalls ⇒ bool" ("_--_∉_" [1000, 1000, 900] 900)
  where "x--y∉S ≡ ¬ x--y∈S"

lemma notInCC_bot[simp]: "x--y∈⊥ ⟷ False"
  by transfer auto

lemma below_CoCallsI:
   "(⋀ x y. x--y∈G ⟹ x--y∈G') ⟹ G ⊑ G'"
  by transfer auto

lemma CoCalls_eqI:
   "(⋀ x y. x--y∈G ⟷ x--y∈G') ⟹ G = G'"
  by transfer auto

lemma in_join[simp]:
  "x--y ∈ (G⊔G') ⟷ x--y∈G ∨ x--y∈G'"
by transfer auto

lemma in_lub[simp]: "x--y∈(lub S) ⟷ (∃ G∈S. x--y∈G)"
  by transfer auto

lemma in_CoCallsLubI:
  "x--y∈G ⟹ G ∈ S ⟹ x--y∈lub S"
by transfer auto

lemma adm_not_in[simp]:
  assumes "cont t"
  shows "adm (λa. x--y∉t a)"
  by (rule admI) (auto simp add: cont2contlubE[OF assms])

lift_definition cc_delete :: "var ⇒ CoCalls ⇒ CoCalls"
  is "λ z. Set.filter (λ (x,y) . x ≠ z ∧ y ≠ z)"
  by (auto intro!: symI elim: symE)

lemma ccField_cc_delete: "ccField (cc_delete x S) ⊆ ccField S - {x}"
  by transfer (auto simp add: Field_def )

lift_definition ccProd :: "var set ⇒ var set ⇒ CoCalls" (infixr "G×" 90)
  is "λ S1 S2. S1 × S2 ∪ S2 × S1"
  by (auto intro!: symI elim: symE)

lemma ccProd_empty[simp]: "{} G× S = ⊥" by transfer auto

lemma ccProd_empty'[simp]: "S G× {} = ⊥" by transfer auto

lemma ccProd_union2[simp]: "S G× (S' ∪ S'') = S G× S' ⊔ S G× S''"
  by transfer auto

lemma ccProd_Union2[simp]: "S G× ⋃S' = (⨆ X∈S'. ccProd S X)"
  by transfer auto

lemma ccProd_Union2'[simp]: "S G× (⋃X∈S'. f X) = (⨆ X∈S'. ccProd S (f X))"
  by transfer auto

lemma in_ccProd[simp]: "x--y∈(S G× S') = (x ∈ S ∧ y ∈ S' ∨ x ∈ S' ∧ y ∈ S)"
  by transfer auto

lemma ccProd_union1[simp]: "(S' ∪ S'') G× S = S' G× S ⊔ S'' G× S"
  by transfer auto

lemma ccProd_insert2: "S G× insert x S' = S G× {x} ⊔ S G× S'"
  by transfer auto

lemma ccProd_insert1: "insert x S' G× S = {x} G× S ⊔ S' G× S"
  by transfer auto

lemma ccProd_mono1: "S' ⊆ S'' ⟹ S' G× S ⊑ S'' G× S"
  by transfer auto

lemma ccProd_mono2: "S' ⊆ S'' ⟹ S G× S' ⊑ S G× S''"
  by transfer auto

lemma ccProd_mono: "S ⊆ S' ⟹ T ⊆ T' ⟹ S G× T ⊑ S' G× T'"
  by transfer auto

lemma ccProd_comm: "S G× S' = S' G× S" by transfer auto

lemma ccProd_belowI:
   "(⋀ x y. x ∈ S ⟹ y ∈ S' ⟹ x--y∈G) ⟹ S G× S' ⊑ G"
  by transfer (auto elim: symE)


lift_definition cc_restr :: "var set ⇒ CoCalls ⇒ CoCalls"
  is "λ S. Set.filter (λ (x,y) . x ∈ S ∧ y ∈ S)"
  by (auto intro!: symI elim: symE)

abbreviation cc_restr_sym (infixl "G|`"  110) where "G G|` S ≡ cc_restr S G"

lemma elem_cc_restr[simp]: "x--y∈(G G|` S) = (x--y∈G ∧ x ∈ S ∧ y ∈ S)"
  by transfer auto

lemma ccField_cc_restr: "ccField (G G|` S) ⊆ ccField G ∩ S"
  by transfer (auto simp add: Field_def)

lemma cc_restr_empty: "ccField G ⊆ - S ⟹ G G|` S = ⊥"
  apply transfer
  apply (auto simp add: Field_def)
  apply (drule DomainI)
  apply (drule (1) set_mp)
  apply simp
  done

lemma cc_restr_empty_set[simp]: "cc_restr {} G = ⊥"
  by transfer auto
  
lemma cc_restr_noop[simp]: "ccField G ⊆ S ⟹ cc_restr S G = G"
  by transfer (force simp add: Field_def dest: DomainI RangeI elim: set_mp)

lemma cc_restr_bot[simp]: "cc_restr S ⊥ = ⊥"
  by simp

lemma ccRestr_ccDelete[simp]: "cc_restr (-{x}) G = cc_delete x G"
  by transfer auto

lemma cc_restr_join[simp]:
  "cc_restr S (G ⊔ G') = cc_restr S G ⊔ cc_restr S G'"
by transfer auto

lemma cont_cc_restr: "cont (cc_restr S)"
  apply (rule contI)
  apply (thin_tac "chain _")
  apply transfer
  apply auto
  done

lemmas cont_compose[OF cont_cc_restr, cont2cont, simp]

lemma cc_restr_mono1:
  "S ⊆ S' ⟹ cc_restr S G ⊑ cc_restr S' G" by transfer auto

lemma cc_restr_mono2:
  "G ⊑ G' ⟹ cc_restr S G ⊑ cc_restr S G'" by transfer auto

lemma cc_restr_below_arg:
  "cc_restr S G ⊑ G" by transfer auto

lemma cc_restr_lub[simp]:
  "cc_restr S (lub X) = (⨆ G∈X. cc_restr S G)" by transfer auto

lemma elem_to_ccField: "x--y∈G ⟹ x ∈ ccField G ∧ y ∈ ccField G"
  by transfer (auto simp add: Field_def)

lemma ccField_to_elem: "x ∈ ccField G ⟹ ∃ y. x--y∈G"
  by transfer (auto simp add: Field_def dest: symD)

lemma cc_restr_intersect: "ccField G ∩ ((S - S') ∪ (S' - S)) = {} ⟹ cc_restr S G = cc_restr S' G"
  by (rule CoCalls_eqI) (auto dest: elem_to_ccField)

lemma cc_restr_cc_restr[simp]: "cc_restr S (cc_restr S' G) = cc_restr (S ∩ S') G"
  by transfer auto

lemma cc_restr_twist: "cc_restr S (cc_restr S' G) = cc_restr S' (cc_restr S G) "
  by transfer auto

lemma cc_restr_cc_delete_twist: "cc_restr x (cc_delete S G) = cc_delete S (cc_restr x G)"
  by transfer auto

lemma cc_restr_ccProd[simp]:
  "cc_restr S (ccProd S⇩1 S⇩2) = ccProd (S⇩1 ∩ S) (S⇩2 ∩ S)"
  by transfer auto

lemma ccProd_below_cc_restr:
  "ccProd S S' ⊑ cc_restr S'' G ⟷ ccProd S S' ⊑ G ∧ (S = {} ∨ S' = {} ∨ S ⊆ S'' ∧ S' ⊆ S'')"
  by transfer auto

lemma cc_restr_eq_subset: "S ⊆ S' ⟹ cc_restr S' G = cc_restr S' G2 ⟹ cc_restr S G = cc_restr S G2"
  by transfer' (auto simp add: Set.filter_def)
 
definition ccSquare ("_²" [80] 80)
  where "S² = ccProd S S"

lemma ccField_ccSquare[simp]: "ccField (S²) = S"
  unfolding ccSquare_def by transfer (auto simp add: Field_def)
  
lemma below_ccSquare[iff]: "(G ⊑ S²) = (ccField G ⊆ S)"
  unfolding ccSquare_def by transfer (auto simp add: Field_def)

lemma cc_restr_ccSquare[simp]: "(S'²) G|` S = (S' ∩ S)²"
  unfolding ccSquare_def by auto

lemma ccSquare_empty[simp]: "{}² = ⊥"
  unfolding ccSquare_def by simp

lift_definition ccNeighbors :: "var ⇒ CoCalls ⇒ var set" 
  is "λ x G. {y .(y,x) ∈ G ∨ (x,y) ∈ G}".

lemma ccNeighbors_bot[simp]: "ccNeighbors x ⊥ = {}" by transfer auto

lemma cont_ccProd1:
  "cont (λ S. ccProd S S')"
  apply (rule contI)
  apply (thin_tac "chain _")
  apply (subst lub_set)
  apply transfer
  apply auto
  done

lemma cont_ccProd2:
  "cont (λ S'. ccProd S S')"
  apply (rule contI)
  apply (thin_tac "chain _")
  apply (subst lub_set)
  apply transfer
  apply auto
  done

lemmas cont_compose2[OF cont_ccProd1 cont_ccProd2, simp, cont2cont]

lemma cont_ccNeighbors[THEN cont_compose, cont2cont, simp]:
  "cont (λy. ccNeighbors x y)"
  apply (rule set_contI)
  apply (thin_tac "chain _")
  apply transfer
  apply auto
  done 


lemma ccNeighbors_join[simp]: "ccNeighbors x (G ⊔ G') = ccNeighbors x G ∪ ccNeighbors x G'"
  by transfer auto

lemma ccNeighbors_ccProd:
  "ccNeighbors x (ccProd S S') = (if x ∈ S then S' else {}) ∪ (if x ∈ S' then S else {})"
by transfer auto

lemma ccNeighbors_ccSquare: 
  "ccNeighbors x (ccSquare S) = (if x ∈ S then S else {})"
  unfolding ccSquare_def by (auto simp add: ccNeighbors_ccProd)

lemma ccNeighbors_cc_restr[simp]:
  "ccNeighbors x (cc_restr S G) = (if x ∈ S then ccNeighbors x G ∩ S else {})"
by transfer auto

lemma ccNeighbors_mono:
  "G ⊑ G' ⟹ ccNeighbors x G ⊆ ccNeighbors x G'"
  by transfer auto

lemma subset_ccNeighbors:
  "S ⊆ ccNeighbors x G ⟷ ccProd {x} S ⊑ G"
  by transfer (auto simp add: sym_def)

lemma elem_ccNeighbors[simp]:
  "y ∈ ccNeighbors x G ⟷ (y--x∈G)"
  by transfer (auto simp add: sym_def)

lemma ccNeighbors_ccField:
  "ccNeighbors x G ⊆ ccField G" by transfer (auto simp add: Field_def)

lemma ccNeighbors_disjoint_empty[simp]:
  "ccNeighbors x G = {} ⟷ x ∉ ccField G"
  by transfer (auto simp add: Field_def)

instance CoCalls :: Join_cpo
  by standard (metis coCallsLub_is_lub)

lemma ccNeighbors_lub[simp]: "ccNeighbors x (lub Gs) = lub (ccNeighbors x ` Gs)"
  by transfer (auto simp add: lub_set)

inductive list_pairs :: "'a list ⇒ ('a × 'a) ⇒ bool"
  where "list_pairs xs p ⟹ list_pairs (x#xs) p"
      | "y ∈ set xs ⟹ list_pairs (x#xs) (x,y)"

lift_definition ccFromList :: "var list ⇒ CoCalls" is "λ xs. {(x,y). list_pairs xs (x,y) ∨ list_pairs xs (y,x)}"
  by (auto intro: symI)

lemma ccFromList_Nil[simp]: "ccFromList [] = ⊥"
  by transfer (auto elim: list_pairs.cases)

lemma ccFromList_Cons[simp]: "ccFromList (x#xs) = ccProd {x} (set xs) ⊔ ccFromList xs"
  by transfer (auto elim: list_pairs.cases intro: list_pairs.intros)

lemma ccFromList_append[simp]: "ccFromList (xs@ys) = ccFromList xs ⊔ ccFromList ys ⊔ ccProd (set xs) (set ys)"
  by (induction xs) (auto simp add: ccProd_insert1[where S' = "set xs" for xs])

lemma ccFromList_filter[simp]:
  "ccFromList (filter P xs) = cc_restr {x. P x} (ccFromList xs)"
by (induction xs) (auto simp add: Collect_conj_eq)

lemma ccFromList_replicate[simp]: "ccFromList (replicate n x) = (if n ≤ 1 then ⊥  else ccProd {x} {x})"
  by (induction n) auto

definition ccLinear :: "var set ⇒ CoCalls ⇒ bool"
  where "ccLinear S G = (∀ x∈S. ∀ y∈S. x--y∉G)"

lemma ccLinear_bottom[simp]:
  "ccLinear S ⊥"
  unfolding ccLinear_def by simp

lemma ccLinear_empty[simp]:
  "ccLinear {} G"
  unfolding ccLinear_def by simp

lemma ccLinear_lub[simp]:
  "ccLinear S (lub X) = (∀ G∈X. ccLinear S G)"
 unfolding ccLinear_def by auto

(*
lemma ccLinear_ccNeighbors:
  "ccLinear S G ⟹ ccNeighbors S G ∩ S = {}"
 unfolding ccLinear_def by transfer auto
*)

lemma ccLinear_cc_restr[intro]:
  "ccLinear S G ⟹ ccLinear S (cc_restr S' G)"
 unfolding ccLinear_def by transfer auto

(* TODO: Sort *)

lemma ccLinear_join[simp]:
  "ccLinear S (G ⊔ G') ⟷ ccLinear S G ∧ ccLinear S G'"
  unfolding ccLinear_def
  by transfer auto

lemma ccLinear_ccProd[simp]:
  "ccLinear S (ccProd S⇩1 S⇩2) ⟷ S⇩1 ∩ S = {} ∨ S⇩2 ∩ S = {}"
  unfolding ccLinear_def
  by transfer auto

lemma ccLinear_mono1: "ccLinear S' G ⟹ S ⊆ S' ⟹ ccLinear S G"
  unfolding ccLinear_def
  by transfer auto

lemma ccLinear_mono2: "ccLinear S G' ⟹ G ⊑ G' ⟹ ccLinear S G"
  unfolding ccLinear_def
  by transfer auto

lemma ccField_join[simp]:
  "ccField (G ⊔ G') = ccField G ∪ ccField G'" by transfer auto

lemma ccField_lub[simp]:
  "ccField (lub S) = ⋃(ccField ` S)" by transfer auto

lemma ccField_ccProd:
  "ccField (ccProd S S') = (if S = {} then {} else if S' = {} then {} else  S ∪ S')"
  by transfer (auto simp add: Field_def)

lemma ccField_ccProd_subset:
  "ccField (ccProd S S') ⊆  S ∪ S'"
  by (simp add: ccField_ccProd)

lemma cont_ccField[THEN cont_compose, simp, cont2cont]:
  "cont ccField"
  by (rule set_contI) auto

end