Theory HOLCF_ROOT

(*<*)
theory HOLCF_ROOT
imports
  "HOLCF-Prelude.HOLCF_Prelude"
begin

(*>*)
section‹Extra HOLCF›

lemma lfp_fusion:
  assumes "g⋅⊥ = ⊥"
  assumes "g oo f = h oo g"
  shows "g⋅(fix⋅f) = fix⋅h"
proof(induct rule: parallel_fix_ind)
  case 2 show "g⋅⊥ = ⊥" by fact
  case (3 x y)
  from ‹g⋅x = y› ‹g oo f = h oo g› show "g⋅(f⋅x) = h⋅y"
    by (simp add: cfun_eq_iff)
qed simp

lemma predE:
  obtains (strict) "p⋅⊥ = ⊥" | (FF) "p = (Λ x. FF)" | (TT) "p = (Λ x. TT)"
using flat_codom[where f=p and x=⊥] by (cases "p⋅⊥"; force simp: cfun_eq_iff)

lemma retraction_cfcomp_strict:
  assumes "f oo g = ID"
  shows "f⋅⊥ = ⊥"
using assms retraction_strict by (clarsimp simp: cfun_eq_iff)

lemma match_Pair_csplit[simp]: "match_Pair⋅x⋅k = k⋅(cfst⋅x)⋅(csnd⋅x)"
by (cases x) simp

lemmas oo_assoc = assoc_oo ―‹Normalize name›

lemma If_cancel[simp]: "(If b then x else x) = seq⋅b⋅x"
by (cases b) simp_all

lemma seq_below[iff]: "seq⋅x⋅y ⊑ y"
by (simp add: seq_conv_if)

lemma seq_strict_distr: "f⋅⊥ = ⊥ ⟹ seq⋅x⋅(f⋅y) = f⋅(seq⋅x⋅y)"
by (cases "x = ⊥"; clarsimp)

lemma strictify_below[iff]: "strictify⋅f ⊑ f"
unfolding strictify_def by (clarsimp simp: cfun_below_iff)

lemma If_distr:
  "⟦f ⊥ = ⊥; cont f⟧ ⟹ f (If b then t else e) = (If b then f t else f e)"
  "⟦cont t'; cont e'⟧ ⟹ (If b then t' else e') x = (If b then t' x else e' x)"
  "(If b then t''' else e''')⋅x = (If b then t'''⋅x else e'''⋅x)"
  "⟦g ⊥ = ⊥; cont g⟧ ⟹ g (If b then t'' else e'') y = (If b then g t'' y else g e'' y)"
by (case_tac [!] b) simp_all

lemma If2_split_asm: "P (If2 Q x y) ⟷ ¬(Q = ⊥ ∧ ¬P ⊥ ∨ Q = TT ∧ ¬P x ∨ Q = FF ∧ ¬P y)"
  by (cases Q) (simp_all add: If2_def)

lemmas If2_splits = split_If2 If2_split_asm

lemma If2_cont[simp, cont2cont]:
  assumes "cont i"
  assumes "cont t"
  assumes "cont e"
  shows "cont (λx. If2 (i x) (t x) (e x))"
using assms unfolding If2_def by simp

lemma If_else_FF[simp]: "(If b then t else FF) = (b andalso t)"
by (cases b) simp_all

lemma If_then_TT[simp]: "(If b then TT else e) = (b orelse e)"
by (cases b) simp_all

lemma If_cong:
  assumes "b = b'"
  assumes"b = TT ⟹ t = t'"
  assumes "b = FF ⟹ e = e'"
  shows "(If b then t else e) = (If b' then t' else e')"
using assms by (cases b) simp_all

lemma If_tr: "(If b then t else e) = ((b andalso t) orelse (neg⋅b andalso e))"
by (cases b) simp_all

lemma If_andalso:
  shows "If p andalso q then t else e = If p then If q then t else e else e"
by (cases p) simp_all

lemma If_else_absorb:
  assumes "c = ⊥ ⟹ e = ⊥"
  assumes "c = TT ⟹ e = t"
  shows "If c then t else e = e"
using assms by (cases c; clarsimp)

lemma andalso_cong: "⟦P = P'; P' = TT ⟹ Q = Q'⟧ ⟹ (P andalso Q) = (P' andalso Q')"
by (cases P) simp_all

lemma andalso_weaken_left:
  assumes "P = TT ⟹ Q = TT"
  assumes "P = FF ⟹ Q ≠ ⊥"
  assumes "P = ⊥ ⟹ Q ≠ FF"
  shows "P = (Q andalso P)"
using assms by (cases P; cases Q; simp)

lemma orelse_cong: "⟦P = P'; P' = FF ⟹ Q = Q'⟧ ⟹ (P orelse Q) = (P' orelse Q')"
by (cases P) simp_all

lemma orelse_conv[simp]:
  "((x orelse y) = TT) ⟷ (x = TT ∨ (x = FF ∧ y = TT))"
  "((x orelse y) = ⊥) ⟷ (x = ⊥ ∨ (x = FF ∧ y = ⊥))"
by (cases x; cases y; simp)+

lemma csplit_cfun2: "cont F ⟹ (Λ x. F x) = (Λ (x, y). F (x, y))"
by (clarsimp simp: cfun_eq_iff prod_cont_iff)

lemma csplit_cfun3: "cont F ⟹ (Λ x. F x) = (Λ (x, y, z). F (x, y, z))"
by (clarsimp simp: cfun_eq_iff prod_cont_iff)

definition convol :: "('a::cpo → 'b::cpo) → ('a → 'c::cpo) → 'a → 'b × 'c" where
  "convol = (Λ f g x. (f⋅x, g⋅x))"

abbreviation convol_syn :: "('a::cpo → 'b::cpo) ⇒ ('a → 'c::cpo) ⇒ 'a → 'b × 'c" (infix "&&" 65) where
  "f && g ≡ convol⋅f⋅g"

lemma convol_strict[simp]:
  "convol⋅⊥⋅⊥ = ⊥"
unfolding convol_def by simp

lemma convol_simp[simp]: "(f && g)⋅x = (f⋅x, g⋅x)"
unfolding convol_def by simp

definition map_prod :: "('a::cpo → 'c::cpo) → ('b::cpo → 'd) → 'a × 'b → 'c × 'd" where
  "map_prod = (Λ f g (x, y). (f⋅x, g⋅y))"

abbreviation map_prod_syn :: "('a → 'c) ⇒ ('b → 'd) ⇒ 'a × 'b → 'c × 'd" (infix "**" 65) where
  "f ** g ≡ map_prod⋅f⋅g"

lemma map_prod_cfcomp[simp]: "(f ** m) oo (g ** n) = (f oo g) ** (m oo n)"
unfolding map_prod_def by (clarsimp simp: cfun_eq_iff)

lemma map_prod_ID[simp]: "ID ** ID = ID"
unfolding map_prod_def by (clarsimp simp: cfun_eq_iff)

lemma map_prod_app[simp]: "(f ** g)⋅x = (f⋅(cfst⋅x), g⋅(csnd⋅x))"
unfolding map_prod_def by (cases x) (clarsimp simp: cfun_eq_iff)

lemma map_prod_cfst[simp]: "cfst oo (f ** g) = f oo cfst"
by (clarsimp simp: cfun_eq_iff)

lemma map_prod_csnd[simp]: "csnd oo (f ** g) = g oo csnd"
by (clarsimp simp: cfun_eq_iff)


subsection‹ Extra HOLCF Prelude. ›

lemma eq_strict[simp]: "eq⋅(⊥::'a::Eq_strict) = ⊥"
by (simp add: cfun_eq_iff)

lemma Integer_le_both_plus_1[simp]:
  fixes m :: Integer
  shows "le⋅(m + 1)⋅(n + 1) = le⋅m⋅n"
by (cases m; cases n; simp add: one_Integer_def)

lemma plus_eq_MkI_conv:
  "l + n = MkI⋅m ⟷ (∃l' n'. l = MkI⋅l' ∧ n = MkI⋅n' ∧ m = l' + n')"
by (cases l, simp) (cases n, auto)

lemma lt_defined:
  fixes x :: Integer
  shows
    "lt⋅x⋅y = TT ⟹ (x ≠ ⊥ ∧ y ≠ ⊥)"
    "lt⋅x⋅y = FF ⟹ (x ≠ ⊥ ∧ y ≠ ⊥)"
by (cases x; cases y; clarsimp)+

lemma le_defined:
  fixes x :: Integer
  shows
    "le⋅x⋅y = TT ⟹ (x ≠ ⊥ ∧ y ≠ ⊥)"
    "le⋅x⋅y = FF ⟹ (x ≠ ⊥ ∧ y ≠ ⊥)"
by (cases x; cases y; clarsimp)+

text‹Induction on ‹Integer›, following the setup for the ‹int› type.›

definition Integer_ge_less_than :: "int ⇒ (Integer × Integer) set"
  where "Integer_ge_less_than d = {(MkI⋅z', MkI⋅z) |z z'. d ≤ z' ∧ z' < z}"

lemma wf_Integer_ge_less_than: "wf (Integer_ge_less_than d)"
proof(rule wf_subset)
  show "Integer_ge_less_than d ⊆ measure (λz. nat (if z = ⊥ then d else (THE z'. z = MkI⋅z') - d))"
    unfolding Integer_ge_less_than_def by clarsimp
qed simp


subsection‹ Element equality \label{sec:equality} ›

text‹

To avoid many extraneous headaches that take us far away from the
interesting parts of our derivation, we assume that the elements of
the pattern and text are drawn from a @{class ‹pcpo›}
where, if the @{const ‹eq›} function on this type is
given defined arguments, then its result is defined and coincides with
@{term ‹(=)›}.

Note this effectively restricts us to @{class ‹flat›}
element types; see \<^citet>‹‹\S4.12› in
"Paulson:1987"› for a discussion.

›

class Eq_def = Eq_eq +
  assumes eq_defined: "⟦x ≠ ⊥; y ≠ ⊥⟧ ⟹ eq⋅x⋅y ≠ ⊥"
begin

lemma eq_bottom_iff[simp]: "(eq⋅x⋅y = ⊥) ⟷ (x = ⊥ ∨ y = ⊥)"
using eq_defined by auto

lemma eq_defined_reflD[simp]:
  "(eq⋅a⋅a = TT) ⟷ a ≠ ⊥"
  "(TT = eq⋅a⋅a) ⟷ a ≠ ⊥"
  "a ≠ ⊥ ⟹ eq⋅a⋅a = TT"
using eq_refl by auto

lemma eq_FF[simp]:
  "(FF = eq⋅xs⋅ys) ⟷ (xs ≠ ⊥ ∧ ys ≠ ⊥ ∧ xs ≠ ys)"
  "(eq⋅xs⋅ys = FF) ⟷ (xs ≠ ⊥ ∧ ys ≠ ⊥ ∧ xs ≠ ys)"
by (metis (mono_tags, opaque_lifting) Exh_tr dist_eq_tr(5) eq_TT_dest eq_bottom_iff eq_self_neq_FF')+

lemma eq_TT[simp]:
  "(TT = eq⋅xs⋅ys) ⟷ (xs ≠ ⊥ ∧ ys ≠ ⊥ ∧ xs = ys)"
  "(eq⋅xs⋅ys = TT) ⟷ (xs ≠ ⊥ ∧ ys ≠ ⊥ ∧ xs = ys)"
by (auto simp: local.eq_TT_dest)

end

instance Integer :: Eq_def by standard simp


subsection ‹Recursive let bindings›

text‹

@{verbatim ‹
Title: HOL/HOLCF/ex/Letrec.thy
Author: Brian Huffman
›}

See \S\ref{sec:KMP:final_version} for an example use.

›

definition
  CLetrec :: "('a::pcpo → 'a × 'b::pcpo) → 'b" where
  "CLetrec = (Λ F. prod.snd (F⋅(μ x. prod.fst (F⋅x))))"

nonterminal recbinds and recbindt and recbind

syntax
  "_recbind"  :: "logic ⇒ logic ⇒ recbind"         ("(2_ =/ _)" 10)
  ""          :: "recbind ⇒ recbindt"               ("_")
  "_recbindt" :: "recbind ⇒ recbindt ⇒ recbindt"   ("_,/ _")
  ""          :: "recbindt ⇒ recbinds"              ("_")
  "_recbinds" :: "recbindt ⇒ recbinds ⇒ recbinds"  ("_;/ _")
  "_Letrec"   :: "recbinds ⇒ logic ⇒ logic"        ("(Letrec (_)/ in (_))" 10)

translations
  (recbindt) "x = a, (y,ys) = (b,bs)" == (recbindt) "(x,y,ys) = (a,b,bs)"
  (recbindt) "x = a, y = b"          == (recbindt) "(x,y) = (a,b)"

translations
  "_Letrec (_recbinds b bs) e" == "_Letrec b (_Letrec bs e)"
  "Letrec xs = a in (e,es)"    == "CONST CLetrec⋅(Λ xs. (a,e,es))"
  "Letrec xs = a in e"         == "CONST CLetrec⋅(Λ xs. (a,e))"

(*<*)

end
(*>*)