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
  "mapL⋅f⋅LNil = LNil"
| "mapL⋅f⋅(LCons⋅x⋅xs) = LCons⋅(f⋅x)⋅(mapL⋅f⋅xs)"

lemma mapL_strict [simp]: "mapL⋅f⋅⊥ = ⊥"
by fixrec_simp

fixrec
  filterL :: "('a → tr) → 'a LList → 'a LList"
where
  "filterL⋅p⋅LNil = LNil"
| "filterL⋅p⋅(LCons⋅x⋅xs) =
    (If p⋅x then LCons⋅x⋅(filterL⋅p⋅xs) else filterL⋅p⋅xs)"

lemma filterL_strict [simp]: "filterL⋅p⋅⊥ = ⊥"
by fixrec_simp

fixrec
  foldrL :: "('a → 'b → 'b) → 'b → 'a LList → 'b"
where
  "foldrL⋅f⋅z⋅LNil = z"
| "foldrL⋅f⋅z⋅(LCons⋅x⋅xs) = f⋅x⋅(foldrL⋅f⋅z⋅xs)"

lemma foldrL_strict [simp]: "foldrL⋅f⋅z⋅⊥ = ⊥"
by fixrec_simp

fixrec
  enumFromToL :: "int⇩⊥ → int⇩⊥ → (int⇩⊥) LList"
where
  "enumFromToL⋅(up⋅x)⋅(up⋅y) =
    (if x ≤ y then LCons⋅(up⋅x)⋅(enumFromToL⋅(up⋅(x+1))⋅(up⋅y)) else LNil)"

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

declare enumFromToL.simps [simp del]

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

fixrec
  appendL :: "'a LList → 'a LList → 'a LList"
where
  "appendL⋅LNil⋅ys = ys"
| "appendL⋅(LCons⋅x⋅xs)⋅ys = LCons⋅x⋅(appendL⋅xs⋅ys)"

lemma appendL_strict [simp]: "appendL⋅⊥⋅ys = ⊥"
by fixrec_simp

lemma appendL_LNil_right: "appendL⋅xs⋅LNil = xs"
by (induct xs) simp_all

fixrec
  zipWithL :: "('a → 'b → 'c) → 'a LList → 'b LList → 'c LList"
where
  "zipWithL⋅f⋅LNil⋅ys = LNil"
| "zipWithL⋅f⋅(LCons⋅x⋅xs)⋅LNil = LNil"
| "zipWithL⋅f⋅(LCons⋅x⋅xs)⋅(LCons⋅y⋅ys) = LCons⋅(f⋅x⋅y)⋅(zipWithL⋅f⋅xs⋅ys)"

lemma zipWithL_strict [simp]:
  "zipWithL⋅f⋅⊥⋅ys = ⊥"
  "zipWithL⋅f⋅(LCons⋅x⋅xs)⋅⊥ = ⊥"
by fixrec_simp+

fixrec
  concatMapL :: "('a → 'b LList) → 'a LList → 'b LList"
where
  "concatMapL⋅f⋅LNil = LNil"
| "concatMapL⋅f⋅(LCons⋅x⋅xs) = appendL⋅(f⋅x)⋅(concatMapL⋅f⋅xs)"

lemma concatMapL_strict [simp]: "concatMapL⋅f⋅⊥ = ⊥"
by fixrec_simp

end