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⇩1⋅v⇩2 = (if undiscr db then v⇩1 else v⇩2)" lemma [simp]: "CB_project⋅(CB⋅(Discr b))⋅v⇩1⋅v⇩2 = (if b then v⇩1 else v⇩2)" "CB_project⋅⊥⋅v⇩1⋅v⇩2 = ⊥" "CB_project⋅(CFn⋅f)⋅v⇩1⋅v⇩2 = ⊥" by fixrec_simp+ lemma CB_project_not_bot: "CB_project⋅scrut⋅v⇩1⋅v⇩2 ≠ ⊥ ⟷ (∃ b. scrut = CB⋅(Discr b) ∧ (if b then v⇩1 else v⇩2) ≠ ⊥)" 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}@{text "::"}@{typeof CValue_take}; we 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