Theory Cardinality-Domain

theory "Cardinality-Domain"
imports "HOLCF-Utils"
begin

type_synonym oneShot = "one"
abbreviation notOneShot :: oneShot where "notOneShot ≡ ONE"
abbreviation oneShot :: oneShot where "oneShot ≡ ⊥"

type_synonym two = "oneShot⇩⊥"
abbreviation many :: two where "many ≡ up⋅notOneShot"
abbreviation once :: two where "once ≡ up⋅oneShot"
abbreviation none :: two where "none ≡ ⊥"

lemma many_max[simp]: "a ⊑ many" by (cases a) auto

lemma two_conj: "c = many ∨ c = once ∨ c = none" by (metis Exh_Up one_neq_iffs(1))

lemma two_cases[case_names many once none]:
  obtains "c = many" | "c = once" | "c = none" using two_conj by metis

definition two_pred where "two_pred = (Λ x. if x ⊑ once then ⊥ else x)"

lemma two_pred_simp: "two_pred⋅c = (if c ⊑ once then ⊥ else c)"
  unfolding two_pred_def
  apply (rule beta_cfun)
  apply (rule cont_if_else_above)
  apply (auto elim: below_trans)
  done

lemma two_pred_simps[simp]:
  "two_pred⋅many = many"
  "two_pred⋅once = none"
  "two_pred⋅none = none"
by (simp_all add: two_pred_simp)

lemma two_pred_below_arg: "two_pred ⋅ f ⊑ f"
  by (auto simp add: two_pred_simp)

lemma two_pred_none: "two_pred⋅c = none ⟷ c ⊑ once"
  by (auto simp add: two_pred_simp)

definition record_call where "record_call x = (Λ ce. (λ y. if x = y then two_pred⋅(ce y) else ce y))"

lemma record_call_simp: "(record_call x ⋅ f) x' = (if x = x' then two_pred ⋅ (f x') else f x')"
  unfolding record_call_def by auto

lemma record_call[simp]: "(record_call x ⋅ f) x = two_pred ⋅ (f x)"
  unfolding record_call_simp by auto

lemma record_call_other[simp]: "x' ≠ x ⟹ (record_call x ⋅ f) x' = f x'"
  unfolding record_call_simp by auto

lemma record_call_below_arg: "record_call x ⋅ f ⊑ f"
  unfolding record_call_def
  by (auto intro!: fun_belowI two_pred_below_arg)

definition two_add :: "two → two → two"
  where "two_add = (Λ x. (Λ y. if x ⊑ ⊥ then y else (if y ⊑ ⊥ then x else many)))"

lemma two_add_simp: "two_add⋅x⋅y = (if x ⊑ ⊥ then y else (if y ⊑ ⊥ then x else many))"
  unfolding two_add_def
  apply (subst beta_cfun)
  apply (rule cont2cont)
  apply (rule cont_if_else_above)
  apply (auto elim: below_trans)[1]
  apply (rule cont_if_else_above)
  apply (auto elim: below_trans)[8]
  apply (rule beta_cfun)
  apply (rule cont_if_else_above)
  apply (auto elim: below_trans)[1]
  apply (rule cont_if_else_above)
  apply auto
  done

lemma two_pred_two_add_once: "c ⊑ two_pred⋅(two_add⋅once⋅c)"
  by (cases c rule: two_cases) (auto simp add: two_add_simp)



end