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