Theory LazyList

section ‹Lazy Lists›

theory LazyList
imports HOLCF "HOLCF-Library.Int_Discrete"
begin

domain 'a LList = LNil | LCons (lazy 'a) (lazy "'a LList")
 
fixrec
  mapL :: "('a  'b)  'a LList  'b LList"
where
  "mapLfLNil = LNil"
| "mapLf(LConsxxs) = LCons(fx)(mapLfxs)"

lemma mapL_strict [simp]: "mapLf = "
by fixrec_simp

fixrec
  filterL :: "('a  tr)  'a LList  'a LList"
where
  "filterLpLNil = LNil"
| "filterLp(LConsxxs) =
    (If px then LConsx(filterLpxs) else filterLpxs)"

lemma filterL_strict [simp]: "filterLp = "
by fixrec_simp

fixrec
  foldrL :: "('a  'b  'b)  'b  'a LList  'b"
where
  "foldrLfzLNil = z"
| "foldrLfz(LConsxxs) = fx(foldrLfzxs)"

lemma foldrL_strict [simp]: "foldrLfz = "
by fixrec_simp

fixrec
  enumFromToL :: "int  int  (int) LList"
where
  "enumFromToL(upx)(upy) =
    (if x  y then LCons(upx)(enumFromToL(up(x+1))(upy)) else LNil)"

lemma enumFromToL_simps' [simp]:
  "x  y 
    enumFromToL(upx)(upy) = LCons(upx)(enumFromToL(up(x+1))(upy))"
  "¬ x  y  enumFromToL(upx)(upy) = LNil"
  by simp_all

declare enumFromToL.simps [simp del]

lemma enumFromToL_strict [simp]:
  "enumFromToLy = "
  "enumFromToLx = "
apply (subst enumFromToL.unfold, simp)
apply (induct x)
apply (subst enumFromToL.unfold, simp)+
done

fixrec
  appendL :: "'a LList  'a LList  'a LList"
where
  "appendLLNilys = ys"
| "appendL(LConsxxs)ys = LConsx(appendLxsys)"

lemma appendL_strict [simp]: "appendLys = "
by fixrec_simp

lemma appendL_LNil_right: "appendLxsLNil = xs"
by (induct xs) simp_all

fixrec
  zipWithL :: "('a  'b  'c)  'a LList  'b LList  'c LList"
where
  "zipWithLfLNilys = LNil"
| "zipWithLf(LConsxxs)LNil = LNil"
| "zipWithLf(LConsxxs)(LConsyys) = LCons(fxy)(zipWithLfxsys)"

lemma zipWithL_strict [simp]:
  "zipWithLfys = "
  "zipWithLf(LConsxxs) = "
by fixrec_simp+

fixrec
  concatMapL :: "('a  'b LList)  'a LList  'b LList"
where
  "concatMapLfLNil = LNil"
| "concatMapLf(LConsxxs) = appendL(fx)(concatMapLfxs)"

lemma concatMapL_strict [simp]: "concatMapLf = "
by fixrec_simp

end