section‹Extra HOLCF›

lemma lfp_fusion:
  assumes "g = "
  assumes "g oo f = h oo g"
  shows "g(fixf) = fixh"
proof(induct rule: parallel_fix_ind)
  case 2 show "g = " by fact
  case (3 x y)
  from gx = y g oo f = h oo g show "g(fx) = hy"
    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_Pairxk = k(cfstx)(csndx)"
by (cases x) simp

lemmas oo_assoc = assoc_oo ―‹Normalize name›

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

lemma seq_below[iff]: "seqxy  y"
by (simp add: seq_conv_if)

lemma seq_strict_distr: "f =   seqx(fy) = f(seqxy)"
by (cases "x = "; clarsimp)

lemma strictify_below[iff]: "strictifyf  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 (negb 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. (fx, gx))"

abbreviation convol_syn :: "('a::cpo  'b::cpo)  ('a  'c::cpo)  'a  'b × 'c" (infix "&&" 65) where
  "f && g  convolfg"

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

lemma convol_simp[simp]: "(f && g)x = (fx, gx)"
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). (fx, gy))"

abbreviation map_prod_syn :: "('a  'c)  ('b  'd)  'a × 'b  'c × 'd" (infix "**" 65) where
  "f ** g  map_prodfg"

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(cfstx), g(csndx))"
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) = lemn"
by (cases m; cases n; simp add: one_Integer_def)

lemma plus_eq_MkI_conv:
  "l + n = MkIm  (l' n'. l = MkIl'  n = MkIn'  m = l' + n')"
by (cases l, simp) (cases n, auto)

lemma lt_defined:
  fixes x :: Integer
    "ltxy = TT  (x    y  )"
    "ltxy = FF  (x    y  )"
by (cases x; cases y; clarsimp)+

lemma le_defined:
  fixes x :: Integer
    "lexy = TT  (x    y  )"
    "lexy = 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 = {(MkIz', MkIz) |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 = MkIz') - d))"
    unfolding Integer_ge_less_than_def by clarsimp
qed simp

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


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 @{classpcpo}
where, if the @{consteq} function on this type is
given defined arguments, then its result is defined and coincides with
@{term (=)}.

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


class Eq_def = Eq_eq +
  assumes eq_defined: "x  ; y    eqxy  "

lemma eq_bottom_iff[simp]: "(eqxy = )  (x =   y = )"
using eq_defined by auto

lemma eq_defined_reflD[simp]:
  "(eqaa = TT)  a  "
  "(TT = eqaa)  a  "
  "a    eqaa = TT"
using eq_refl by auto

lemma eq_FF[simp]:
  "(FF = eqxsys)  (xs    ys    xs  ys)"
  "(eqxsys = 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 = eqxsys)  (xs    ys    xs = ys)"
  "(eqxsys = TT)  (xs    ys    xs = ys)"
by (auto simp: local.eq_TT_dest)


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.


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

nonterminal recbinds and recbindt and recbind

  "_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)

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

  "_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))"