theory CValue
imports C
begin

domain CValue
  = CFn (lazy "(C → CValue) → (C → CValue)")
  | CB (lazy "bool discr")

fixrec CFn_project :: "CValue → (C → CValue) → (C → CValue)"
 where "CFn_project⋅(CFn⋅f)⋅v = f ⋅ v"

abbreviation CFn_project_abbr (infix ‹↓CFn› 55)
  where "f ↓CFn v ≡ CFn_project⋅f⋅v"

lemma CFn_project_strict[simp]:
  "⊥ ↓CFn v = ⊥"
  "CB⋅b ↓CFn v = ⊥"
  by (fixrec_simp)+

lemma CB_below[simp]: "CB⋅b ⊑ v ⟷ v = CB⋅b"
  by (cases v) auto

fixrec CB_project :: "CValue → CValue → CValue → CValue" where
  "CB_project⋅(CB⋅db)⋅v₁⋅v₂ = (if undiscr db then v₁ else v₂)"

lemma [simp]:
  "CB_project⋅(CB⋅(Discr b))⋅v₁⋅v₂ = (if b then v₁ else v₂)"
  "CB_project⋅⊥⋅v₁⋅v₂ = ⊥"
  "CB_project⋅(CFn⋅f)⋅v₁⋅v₂ = ⊥"
by fixrec_simp+

lemma CB_project_not_bot:
  "CB_project⋅scrut⋅v₁⋅v₂ ≠ ⊥ ⟷ (∃ b. scrut = CB⋅(Discr b) ∧ (if b then v₁ else v₂) ≠ ⊥)"
  apply (cases scrut)
  apply simp
  apply simp
  by (metis (poly_guards_query) CB_project.simps CValue.injects(2) discr.exhaust undiscr_Discr)

text ‹HOLCF provides us @{const CValue_take}‹::›@{typeof CValue_take};
  want a similar function for @{typ "C → CValue"}.›

abbreviation C_to_CValue_take :: "nat → (C → CValue) → (C → CValue)"
   where "C_to_CValue_take n ≡ cfun_map⋅ID⋅(CValue_take n)"

lemma C_to_CValue_chain_take: "chain C_to_CValue_take"
  by (auto intro: chainI cfun_belowI chainE[OF CValue.chain_take] monofun_cfun_fun)

lemma C_to_CValue_reach: "(⊔ n. C_to_CValue_take n⋅x) = x"
  by (auto intro:  cfun_eqI simp add: contlub_cfun_fun[OF ch2ch_Rep_cfunL[OF C_to_CValue_chain_take]]  CValue.reach)


end