Theory HLint

theory HLint
  imports
    "../HOLCF_Prelude"
    "../List_Comprehension"
begin

section ‹HLint›

text ‹
  The tool \texttt{hlint} analyses Haskell code and, based on a data base of
  rewrite rules, suggests stylistic improvements to it. We verify
  a number of these rules using our implementation of the Haskell standard
  library.
›

(* -- I/O *)
(*  putStrLn (show x) ==> print x *)
(*  mapM_ putChar ==> putStr *)
(*  hGetChar stdin ==> getChar *)
(*  hGetLine stdin ==> getLine *)
(*  hGetContents stdin ==> getContents *)
(*  hPutChar stdout ==> putChar *)
(*  hPutStr stdout ==> putStr *)
(*  hPutStrLn stdout ==> putStrLn *)
(*  hPrint stdout ==> print *)
(*  hWaitForInput a 0 ==> hReady a *)
(*  hPutStrLn a (show b) ==> hPrint a b *)
(*  hIsEOF stdin ==> isEOF *)
(* -- EXIT *)
(*  exitWith ExitSuccess ==> exitSuccess *)

subsection ‹Ord›

(*  not (a == b) ==> a /= b where note = "incorrect if either value is NaN" *)
(*  not (a /= b) ==> a == b where note = "incorrect if either value is NaN" *)
(*  not (a >  b) ==> a <= b where note = "incorrect if either value is NaN" *)
(*  not (a >= b) ==> a <  b where note = "incorrect if either value is NaN" *)
(*  not (a <  b) ==> a >= b where note = "incorrect if either value is NaN" *)
(*  not (a <= b) ==> a >  b where note = "incorrect if either value is NaN" *)

(*  compare x y /= GT ==> x <= y *)
(*  compare x y == LT ==> x < y *)
(*  compare x y /= LT ==> x >= y *)
(*  compare x y == GT ==> x > y *)

text ‹@{verbatim ‹x == a || x == b || x == c ==> x `elem` [a,b,c]› } ›
lemma "(eq⋅(x::'a::Eq_sym)⋅a orelse eq⋅x⋅b orelse eq⋅x⋅c) = elem⋅x⋅[a, b, c]"
  by (auto simp add: eq_sym)

text ‹@{verbatim ‹ x /= a && x /= b && x /= c ==> x `notElem` [a,b,c]› } ›
lemma "(neq⋅(x::'a::Eq_sym)⋅a andalso neq⋅x⋅b andalso neq⋅x⋅c) = notElem⋅x⋅[a, b, c]"
  by (auto simp add: eq_sym)

    (*  compare (f x) (f y) ==> Data.Ord.comparing f x y -- not that great *)
    (*  on compare f ==> Data.Ord.comparing f -- not that great *)
    (* -- READ/SHOW *)
    (*  showsPrec 0 x "" ==> show x *)
    (*  readsPrec 0 ==> reads *)
    (*  showsPrec 0 ==> shows *)
    (*  showIntAtBase 16 intToDigit ==> showHex *)
    (*  showIntAtBase 8 intToDigit ==> showOct *)

subsection ‹List›

text ‹@{verbatim ‹ concat (map f x) ==> concatMap f x› } ›
lemma "concat⋅(map⋅f⋅x) = concatMap⋅f⋅x"
  by (auto simp add: concatMap_def)

text ‹@{verbatim ‹ concat [a, b] ==> a ++ b› } ›
lemma "concat⋅[a, b] = a ++ b"
  by auto

text ‹@{verbatim ‹ map f (map g x) ==> map (f . g) x› } ›
lemma "map⋅f⋅(map⋅g⋅x) = map⋅(f oo g)⋅x"
  by auto

text ‹@{verbatim ‹ x !! 0 ==> head x› } ›
lemma "x !! 0 = head⋅x"
  by (cases x) auto

text ‹@{verbatim ‹ take n (repeat x) ==> replicate n x› } ›
lemma "take⋅n⋅(repeat⋅x) = replicate⋅n⋅x"
  by (simp add: replicate_def)

text ‹@{verbatim ‹lemma "head⋅(reverse⋅x) = last⋅x" › } ›
lemma "head⋅(reverse⋅x) = last⋅x"
proof (cases "finite_list x")
  case True then show ?thesis
    by (induct x rule: reverse_induct) (auto simp add: last_append_singleton)
next
  case False then show ?thesis
    by (simp add: last_spine_strict reverse_spine_strict)
qed

text ‹@{verbatim ‹ head (drop n x) ==> x !! n where note = "if the index is non-negative"› } ›
lemma
  assumes "le⋅0⋅n ≠ FF"
  shows "head⋅(drop⋅n⋅x) = x !! n"
proof (cases "le⋅0⋅n")
  assume "le⋅0⋅n = FF" with assms show ?thesis..
next
  assume "le⋅0⋅n = TT"
  then show ?thesis
  proof (induction arbitrary: x rule: nonneg_Integer_induct)
    case 0
    show ?case by (cases x) auto
  next
    case (step i x)
    from step.hyps have [simp]:"le⋅i⋅0 = FF" by (cases i, auto simp add: one_Integer_def zero_Integer_def)
    from step.hyps have [simp]:"eq⋅i⋅0 = FF" by (cases i, auto simp add: one_Integer_def zero_Integer_def)
    show ?case
      using step.IH  by (cases x)auto
  qed
qed simp

text ‹@{verbatim ‹ reverse (tail (reverse x)) ==> init x› } ›
lemma "reverse⋅(tail⋅(reverse⋅x)) ⊑ init⋅x"
proof (cases "finite_list x")
  case True
  then show ?thesis
    by (induct x rule: reverse_induct) (auto simp add: init_append_singleton)
next
  case False
  then show ?thesis
    by (auto simp add: reverse_spine_strict)
qed

text ‹@{verbatim ‹ take (length x - 1) x ==> init x› } ›
lemma
  assumes "x ≠ []"
  shows "take⋅(length⋅x - 1)⋅x ⊑ init⋅x"
  using assms
proof (induct x)
  case IH: (Cons y ys)
  show ?case
  proof (cases ys)
    case (Cons z zs)
    show ?thesis
      using IH
      by (cases "length⋅zs")
         (auto simp: Cons one_Integer_def dest: length_ge_0)
  qed (auto simp: one_Integer_def)
qed auto

text ‹@{verbatim ‹ foldr (++) [] ==> concat› } ›
lemma foldr_append_concat:"foldr⋅append⋅[] = concat"
proof (rule cfun_eqI)
  fix xs :: "[['a]]"
  show "foldr⋅append⋅[]⋅xs = concat⋅xs"
    by (induct xs) auto
qed

text ‹@{verbatim ‹ foldl (++) [] ==> concat› } ›
lemma "foldl⋅append⋅[] ⊑ concat"
proof (rule cfun_belowI)
  fix xs :: "[['a]]"
  show "foldl⋅append⋅[]⋅xs ⊑ concat⋅xs"
    by (cases "finite_list xs")
       (auto simp add: foldr_append_concat foldl_assoc_foldr foldl_spine_strict)
qed

text ‹@{verbatim ‹ span (not . p) ==> break p› } ›
lemma "span⋅(neg oo p) = break⋅p"
  by simp

text ‹@{verbatim ‹ break (not . p) ==> span p› } ›
lemma "break⋅(neg oo p) = span⋅p"
  by (unfold break.simps) (subst assoc_oo, simp)

(*  concatMap (++ "\n") ==> unlines *)

text ‹@{verbatim ‹ or (map p x) ==> any p x› } ›
lemma "the_or⋅(map⋅p⋅x) = any⋅p⋅x"
  by simp

text ‹@{verbatim ‹ and (map p x) ==> all p x› } ›
lemma "the_and⋅(map⋅p⋅x) = all⋅p⋅x"
  by simp

text ‹@{verbatim ‹ zipWith (,) ==> zip› } ›
lemma "zipWith⋅⟨,⟩ = zip"
  by (simp add: zip_def)

text ‹@{verbatim ‹ zipWith3 (,,) ==> zip3› } ›
lemma "zipWith3⋅⟨,,⟩ = zip3"
  by (simp add: zip3_def)

text ‹@{verbatim ‹ length x == 0 ==> null x where note = "increases laziness"› } ›
lemma "eq⋅(length⋅x)⋅0 ⊑ null⋅x"
proof (cases x)
  case (Cons y ys)
  then show ?thesis
    by (cases "length⋅ys")
       (auto dest: length_ge_0 simp: zero_Integer_def one_Integer_def)
qed simp+

text ‹@{verbatim ‹ length x /= 0 ==> not (null x)› } ›
lemma "neq⋅(length⋅x)⋅0 ⊑ neg⋅(null⋅x)"
proof (cases x)
  case (Cons y ys)
  then show ?thesis
    by (cases "length⋅ys")
       (auto dest: length_ge_0 simp: zero_Integer_def one_Integer_def)
qed simp+

(*  (\x -> [x]) ==> (:[]) *)

text ‹@{verbatim ‹ map (uncurry f) (zip x y) ==> zipWith f x y› } ›
lemma "map⋅(uncurry⋅f)⋅(zip⋅x⋅y) = zipWith⋅f⋅x⋅y"
proof (induct x arbitrary: y)
  case (Cons x xs y) then show ?case by (cases y) auto
qed auto

text ‹@{verbatim ‹ map f (zip x y) ==> zipWith (curry f) x y where _ = isVar f› } ›
lemma "map⋅f⋅(zip⋅x⋅y) = zipWith⋅(curry⋅f)⋅x⋅y"
proof(induct x arbitrary: y)
  case (Cons x xs y) then show ?case by (cases y) auto
qed auto

text ‹@{verbatim ‹ not (elem x y) ==> notElem x y› } ›
lemma "neg⋅(elem⋅x⋅y) = notElem⋅x⋅y"
  by (induct y) auto

text ‹@{verbatim ‹ foldr f z (map g x) ==> foldr (f . g) z x› } ›
lemma "foldr⋅f⋅z⋅(map⋅g⋅x) = foldr⋅(f oo g)⋅z⋅x"
  by (induct x) auto

(*  x ++ concatMap (' ':) y ==> unwords (x:y) *)
(*  intercalate " " ==> unwords *)
(*  concat (intersperse x y) ==> intercalate x y where _ = notEq x " " *)
(*  concat (intersperse " " x) ==> unwords x *)
text ‹@{verbatim ‹ null (filter f x) ==> not (any f x)› } ›
lemma "null⋅(filter⋅f⋅x) = neg⋅(any⋅f⋅x)"
proof (induct x)
  case (Cons x xs)
  then show ?case by (cases "f⋅x") auto
qed auto

text ‹@{verbatim ‹ filter f x == [] ==> not (any f x)› } ›
lemma "eq⋅(filter⋅f⋅x)⋅[] = neg⋅(any⋅f⋅x)"
proof (induct x)
  case (Cons x xs)
  then show ?case by (cases "f⋅x") auto
qed auto

text ‹@{verbatim ‹ filter f x /= [] ==> any f x› } ›
lemma "neq⋅(filter⋅f⋅x)⋅[] = any⋅f⋅x"
proof (induct x)
  case (Cons x xs)
  then show ?case by (cases "f⋅x") auto
qed auto

text ‹@{verbatim ‹ any (== a) ==> elem a› } ›
lemma "any⋅(Λ z. eq⋅z⋅a) = elem⋅a"
proof (rule cfun_eqI)
  fix xs
  show "any⋅(Λ z. eq⋅z⋅a)⋅xs = elem⋅a⋅xs"
    by (induct xs) auto
qed

text ‹@{verbatim ‹ any ((==) a) ==> elem a› } ›
lemma "any⋅(eq⋅(a::'a::Eq_sym)) = elem⋅a"
proof (rule cfun_eqI)
  fix xs
  show "any⋅(eq⋅a)⋅xs = elem⋅a⋅xs"
    by (induct xs) (auto simp: eq_sym)
qed

text ‹@{verbatim ‹any (a ==) ==> elem a› } ›
lemma "any⋅(Λ z. eq⋅(a::'a::Eq_sym)⋅z) = elem⋅a"
proof (rule cfun_eqI)
  fix xs
  show "any⋅(Λ z. eq⋅a⋅z)⋅xs = elem⋅a⋅xs"
    by (induct xs) (auto simp: eq_sym)
qed

text ‹@{verbatim ‹ all (/= a) ==> notElem a› } ›
lemma "all⋅(Λ z. neq⋅z⋅(a::'a::Eq_sym)) = notElem⋅a"
proof (rule cfun_eqI)
  fix xs
  show "all⋅(Λ z. neq⋅z⋅a)⋅xs = notElem⋅a⋅xs"
    by (induct xs) auto
qed

text ‹@{verbatim ‹ all (a /=) ==> notElem a› } ›
lemma "all⋅(Λ z. neq⋅(a::'a::Eq_sym)⋅z) = notElem⋅a"
proof (rule cfun_eqI)
  fix xs
  show "all⋅(Λ z. neq⋅a⋅z)⋅xs = notElem⋅a⋅xs"
    by (induct xs) (auto simp: eq_sym)
qed

(* findIndex ((==) a) ==> elemIndex a *)
(* findIndex (a ==) ==> elemIndex a *)
(* findIndex (== a) ==> elemIndex a *)
(* findIndices ((==) a) ==> elemIndices a *)
(* findIndices (a ==) ==> elemIndices a *)
(* findIndices (== a) ==> elemIndices a *)
(* lookup b (zip l [0..]) ==> elemIndex b l *)

subsection ‹Folds›

(*  foldr  (>>) (return ()) ==> sequence_ *)

text ‹@{verbatim ‹ foldr  (&&) True ==> and› } ›
lemma "foldr⋅trand⋅TT = the_and"
  by (subst the_and.simps, rule)

text ‹@{verbatim ‹ foldl  (&&) True ==> and› } ›
lemma foldl_to_and:"foldl⋅trand⋅TT ⊑ the_and"
proof (rule cfun_belowI)
  fix xs
  show "foldl⋅trand⋅TT⋅xs ⊑ the_and⋅xs"
    by (cases "finite_list xs") (auto simp: foldl_assoc_foldr foldl_spine_strict)
qed

text ‹@{verbatim ‹ foldr1 (&&)  ==> and› } ›
lemma "foldr1⋅trand ⊑ the_and"
proof (rule cfun_belowI)
  fix xs
  show "foldr1⋅trand⋅xs ⊑ the_and⋅xs"
  proof (induct xs)
    case (Cons y ys)
    then show ?case by (cases ys) (auto elim: monofun_cfun_arg)
  qed simp+
qed

text ‹@{verbatim ‹ foldl1 (&&)  ==> and› } ›
lemma "foldl1⋅trand ⊑ the_and"
proof (rule cfun_belowI)
  fix x
  have "foldl1⋅trand⋅x ⊑ foldl⋅trand⋅TT⋅x"
    by (cases x, auto)
  also have "... ⊑ the_and⋅x"
    by (rule monofun_cfun_fun[OF foldl_to_and])
  finally show "foldl1⋅trand⋅x ⊑ the_and⋅x" .
qed

text ‹@{verbatim ‹ foldr  (||) False ==> or› } ›
lemma "foldr⋅tror⋅FF = the_or"
  by (subst the_or.simps, rule)

text ‹@{verbatim ‹ foldl  (||) False ==> or› } ›
lemma foldl_to_or: "foldl⋅tror⋅FF ⊑ the_or"
proof (rule cfun_belowI)
  fix xs
  show "foldl⋅tror⋅FF⋅xs ⊑ the_or⋅xs"
    by (cases "finite_list xs") (auto simp: foldl_assoc_foldr foldl_spine_strict)
qed

text ‹@{verbatim ‹ foldr1 (||)  ==> or› } ›
lemma "foldr1⋅tror ⊑ the_or"
proof (rule cfun_belowI)
  fix xs
  show "foldr1⋅tror⋅xs ⊑ the_or⋅xs"
  proof (induct xs)
    case (Cons y ys)
    then show ?case by (cases ys) (auto elim: monofun_cfun_arg)
  qed simp+
qed

text ‹@{verbatim ‹ foldl1 (||)  ==> or› } ›
lemma "foldl1⋅tror ⊑ the_or"
proof(rule cfun_belowI)
  fix x
  have "foldl1⋅tror⋅x ⊑ foldl⋅tror⋅FF⋅x"
    by (cases x, auto)
  also have "... ⊑ the_or⋅x"
    by (rule monofun_cfun_fun[OF foldl_to_or])
  finally show "foldl1⋅tror⋅x ⊑ the_or⋅x" .
qed

(*  foldl  (+) 0 ==> sum *)
(*  foldr  (+) 0 ==> sum *)
(*  foldl1 (+)   ==> sum *)
(*  foldr1 (+)   ==> sum *)
(*  foldl  ( * ) 1 ==> product *)
(*  foldr  ( * ) 1 ==> product *)
(*  foldl1 ( * )   ==> product *)
(*  foldr1 ( * )   ==> product *)
(*  foldl1 max   ==> maximum *)
(*  foldr1 max   ==> maximum *)
(*  foldl1 min   ==> minimum *)
(*  foldr1 min   ==> minimum *)
(*  foldr mplus mzero ==> msum *)

subsection ‹Function›
text ‹@{verbatim ‹ (\x -> x) ==> id› } ›
lemma "(Λ x. x) = ID"
  by (metis ID_def)

text ‹@{verbatim ‹ (\x y -> x) ==> const› } ›
lemma "(Λ x y. x) = const"
  by (intro cfun_eqI) simp

text ‹@{verbatim ‹(\(x,y) -> y) ==> fst where _ = notIn x y› } ›
lemma "(Λ ⟨x, y⟩. x) = fst"
proof (rule cfun_eqI)
  fix p
  show "(case p of ⟨x, y⟩ ⇒ x) = fst ⋅ p"
  proof (cases p)
    case bottom then show ?thesis by simp
  next
    case Tuple2 then show ?thesis by simp
  qed
qed

text ‹@{verbatim ‹(\(x,y) -> y) ==> snd where _ = notIn x y› } ›
lemma "(Λ ⟨x, y⟩. y) = snd"
proof (rule cfun_eqI)
  fix p
  show "(case p of ⟨x, y⟩ ⇒ y) = snd ⋅ p"
  proof (cases p)
    case bottom then show ?thesis by simp
  next
    case Tuple2 then show ?thesis by simp
  qed
qed

text ‹@{verbatim ‹ (\x y-> f (x,y)) ==> curry f where _ = notIn [x,y] f› } ›
lemma "(Λ x y. f⋅⟨x, y⟩) = curry⋅f"
  by (auto intro!: cfun_eqI)

text ‹@{verbatim ‹ (\(x,y) -> f x y) ==> uncurry f where _ = notIn [x,y] f› } ›
lemma "(Λ ⟨x, y⟩. f⋅x⋅y) ⊑ uncurry⋅f"
  by (rule cfun_belowI, rename_tac x, case_tac x, auto)

(*  (($) . f) ==> f *)
(*  (f $) ==> f *)

text ‹@{verbatim ‹ (\x -> y) ==> const y where _ = isAtom y && notIn x y› } ›
lemma "(Λ x. y) = const⋅y"
  by (intro cfun_eqI) simp

(*  flip f x y ==> f y x where _ = isApp original *)
lemma "flip⋅f⋅x⋅y = f⋅y⋅x" by simp

(*  (\a b -> o (f a) (f b)) ==> o `Data.Function.on` f *)
(* -- CHAR *)
(*  a >= 'a' && a <= 'z' ==> isAsciiLower a *)
(*  a >= 'A' && a <= 'Z' ==> isAsciiUpper a *)
(*  a >= '0' && a <= '9' ==> isDigit a *)
(*  a >= '0' && a <= '7' ==> isOctDigit a *)
(*  not (isControl a) ==> isPrint a *)
(*  isLower a || isUpper a ==> isAlpha a *)
(*  isAlpha a || isDigit a ==> isAlphaNum a *)

subsection ‹Bool›

text ‹@{verbatim ‹ a == True ==> a› } ›
lemma eq_true:"eq⋅x⋅TT = x"
  by (cases x, auto)

text ‹@{verbatim ‹ a == False ==> not a› } ›
lemma eq_false:"eq⋅x⋅FF = neg⋅x"
  by (cases x, auto)

text ‹@{verbatim ‹ (if a then x else x) ==> x where note = "reduces strictness"› } ›
lemma if_equal:"(If a then x else x) ⊑ x"
  by (cases a, auto)

text ‹@{verbatim ‹ (if a then True else False) ==> a› } ›
lemma "(If a then TT else FF) = a"
  by (cases a, auto)

text ‹@{verbatim ‹ (if a then False else True) ==> not a› } ›
lemma "(If a then FF else TT) = neg⋅a"
  by (cases a, auto)

text ‹@{verbatim ‹ (if a then t else (if b then t else f)) ==> if a || b then t else f› } ›
lemma "(If a then t else (If b then t else f)) = (If a orelse b then t else f)"
  by (cases a, auto)

text ‹@{verbatim ‹ (if a then (if b then t else f) else f) ==> if a && b then t else f› } ›
lemma "(If a then (If b then t else f) else f) = (If a andalso b then t else f)"
  by (cases a, auto)

text ‹@{verbatim ‹ (if x then True else y) ==> x || y where _ = notEq y False› } ›
lemma "(If x then TT else y) = (x orelse y)"
  by (cases x, auto)

text ‹@{verbatim ‹ (if x then y else False) ==> x && y where _ = notEq y True› } ›
lemma "(If x then y else FF) = (x andalso y)"
  by (cases x, auto)

(*  case a of {True -> t; False -> f} ==> if a then t else f *)
(*  case a of {False -> f; True -> t} ==> if a then t else f *)
(*  case a of {True -> t; _ -> f} ==> if a then t else f *)
(*  case a of {False -> f; _ -> t} ==> if a then t else f *)
text ‹@{verbatim ‹ (if c then (True, x) else (False, x)) ==> (c, x) where note = "reduces strictness"› } ›
lemma "(If c then ⟨TT, x⟩ else ⟨FF, x⟩) ⊑ ⟨c, x⟩"
  by (cases c, auto)

text ‹@{verbatim ‹ (if c then (False, x) else (True, x)) ==> (not c, x) where note = "reduces strictness"› } ›
lemma "(If c then ⟨FF, x⟩ else ⟨TT, x⟩) ⊑ ⟨neg⋅c, x⟩"
  by (cases c, auto)

text ‹@{verbatim ‹ or [x,y]  ==> x || y› } ›
lemma "the_or⋅[x, y] = (x orelse y)"
  by (fixrec_simp)

text ‹@{verbatim ‹ or [x,y,z]  ==> x || y || z› } ›
lemma "the_or⋅[x, y, z] = (x orelse y orelse z)"
  by (fixrec_simp)

text ‹@{verbatim ‹ and [x,y]  ==> x && y› } ›
lemma "the_and⋅[x, y] = (x andalso y)"
  by (fixrec_simp)

text ‹@{verbatim ‹ and [x,y,z]  ==> x && y && z› } ›
lemma "the_and⋅[x, y, z] = (x andalso y andalso z)"
  by (fixrec_simp)

subsection ‹Arrow›

(*  id *** g ==> second g *)
(*  f *** id ==> first f *)
(*  zip (map f x) (map g x) ==> map (f Control.Arrow.&&& g) x *)
(*  (\(x,y) -> (f x, g y)) ==> f Control.Arrow.*** g where _ = notIn [x,y] [f,g] *)
(*  (\x -> (f x, g x)) ==> f Control.Arrow.&&& g where _ = notIn x [f,g] *)
(*  (\(x,y) -> (f x,y)) ==> Control.Arrow.first f where _ = notIn [x,y] f *)
(*  (\(x,y) -> (x,f y)) ==> Control.Arrow.second f where _ = notIn [x,y] f *)
(*  (f (fst x), g (snd x)) ==> (f Control.Arrow.*** g) x *)

text ‹@{verbatim ‹ (fst x, snd x) ==>  x› } ›
lemma "x ⊑ ⟨fst⋅x, snd⋅x⟩"
  by (cases x, auto)

(* -- FUNCTOR *)
(*  fmap f (fmap g x) ==> fmap (f . g) x *)
(*  fmap id ==> id *)
(* -- MONAD *)
(*  return a >>= f ==> f a *)
(*  m >>= return ==> m *)
(*  m >>= return . f ==> Control.Monad.liftM f m -- cannot be fmap, because is in Functor not Monad *)
(*  (if x then y else return ()) ==> Control.Monad.when x $ _noParen_ y where _ = not (isAtom y) *)
(*  (if x then y else return ()) ==> Control.Monad.when x y where _ = isAtom y *)
(*  (if x then return () else y) ==> Control.Monad.unless x $ _noParen_ y where _ = not (isAtom y) *)
(*  (if x then return () else y) ==> Control.Monad.unless x y where _ = isAtom y *)
(*  sequence (map f x) ==> mapM f x *)
(*  sequence_ (map f x) ==> mapM_ f x *)
(*  flip mapM ==> Control.Monad.forM *)
(*  flip mapM_ ==> Control.Monad.forM_ *)
(*  flip forM ==> mapM *)
(*  flip forM_ ==> mapM_ *)
(*  when (not x) ==> unless x *)
(*  x >>= id ==> Control.Monad.join x *)
(*  liftM f (liftM g x) ==> liftM (f . g) x *)
(*  a >> return () ==> void a *)
(*  fmap (const ()) ==> void *)
(*  flip (>=>) ==> (<=<) *)
(*  flip (<=<) ==> (>=>) *)
(*  (\x -> f x >>= g) ==> f Control.Monad.>=> g where _ = notIn x [f,g] *)
(*  (\x -> f =<< g x) ==> f Control.Monad.<=< g where _ = notIn x [f,g] *)
(*  a >> forever a ==> forever a *)
(*  liftM2 id ==> ap *)
(* -- MONAD LIST *)
(*  liftM unzip (mapM f x) ==> Control.Monad.mapAndUnzipM f x *)
(*  sequence (zipWith f x y) ==> Control.Monad.zipWithM f x y *)
(*  sequence_ (zipWith f x y) ==> Control.Monad.zipWithM_ f x y *)
(*  sequence (replicate n x) ==> Control.Monad.replicateM n x *)
(*  sequence_ (replicate n x) ==> Control.Monad.replicateM_ n x *)
(*  mapM f (map g x) ==> mapM (f . g) x *)
(*  mapM_ f (map g x) ==> mapM_ (f . g) x *)
(* -- APPLICATIVE / TRAVERSABLE *)
(*  flip traverse ==> for *)
(*  flip for ==> traverse *)
(*  flip traverse_ ==> for_ *)
(*  flip for_ ==> traverse_ *)
(*  foldr ( *>) (pure ()) ==> sequenceA_ *)
(*  foldr (<|>) empty ==> asum *)
(*  liftA2 (flip ($)) ==> (<**>) *)
(*  Just <$> a <|> pure Nothing ==> optional a *)
(* -- LIST COMP *)
(*  (if b then [x] else []) ==> [x | b] *)
(*  [x | x <- y] ==> y where _ = isVar x *)
(* -- SEQ *)

subsection ‹Seq›

text ‹@{verbatim ‹ x `seq` x ==> x› } ›
lemma "seq⋅x⋅x = x" by (simp add: seq_def)

(*  id $! x ==> x *)
(*  x `seq` y ==> y where _ = isWHNF x *)
(*  f $! x ==> f x where _ = isWHNF x *)
(*  evaluate x ==> return x where _ = isWHNF x *)
(* -- MAYBE *)
(*  maybe x id ==> Data.Maybe.fromMaybe x *)
(*  maybe False (const True) ==> Data.Maybe.isJust *)
(*  maybe True (const False) ==> Data.Maybe.isNothing *)
(*  not (isNothing x) ==> isJust x *)
(*  not (isJust x) ==> isNothing x *)
(*  maybe [] (:[]) ==> maybeToList *)
(*  catMaybes (map f x) ==> mapMaybe f x *)
(*  (case x of Nothing -> y; Just a -> a)  ==> fromMaybe y x *)
(*  (if isNothing x then y else f (fromJust x)) ==> maybe y f x *)
(*  (if isJust x then f (fromJust x) else y) ==> maybe y f x *)
(*  maybe Nothing (Just . f) ==> fmap f *)
(*  map fromJust . filter isJust  ==>  Data.Maybe.catMaybes *)
(*  x == Nothing  ==>  isNothing x *)
(*  Nothing == x  ==>  isNothing x *)
(*  x /= Nothing  ==>  Data.Maybe.isJust x *)
(*  Nothing /= x  ==>  Data.Maybe.isJust x *)
(*  concatMap (maybeToList . f) ==> Data.Maybe.mapMaybe f *)
(*  concatMap maybeToList ==> catMaybes *)
(*  maybe n Just x ==> Control.Monad.mplus x n *)
(*  (case x of Just a -> a; Nothing -> y)  ==> fromMaybe y x *)
(*  (if isNothing x then y else fromJust x) ==> fromMaybe y x *)
(*  (if isJust x then fromJust x else y) ==> fromMaybe y x *)
(*  isJust x && (fromJust x == y) ==> x == Just y *)
(*  mapMaybe f (map g x) ==> mapMaybe (f . g) x *)
(*  fromMaybe a (fmap f x) ==> maybe a f x *)
(*  [x | Just x <- a] ==> Data.Maybe.catMaybes a *)
(* -- EITHER *)
(*  [a | Left a <- a] ==> lefts a *)
(*  [a | Right a <- a] ==> rights a *)
(* -- INFIX *)
(*  X.elem x y ==> x `X.elem` y where _ = not (isInfixApp original) && not (isParen result) *)
(*  X.notElem x y ==> x `X.notElem` y where _ = not (isInfixApp original) && not (isParen result) *)
(*  X.isInfixOf x y ==> x `X.isInfixOf` y where _ = not (isInfixApp original) && not (isParen result) *)
(*  X.isSuffixOf x y ==> x `X.isSuffixOf` y where _ = not (isInfixApp original) && not (isParen result) *)
(*  X.isPrefixOf x y ==> x `X.isPrefixOf` y where _ = not (isInfixApp original) && not (isParen result) *)
(*  X.union x y ==> x `X.union` y where _ = not (isInfixApp original) && not (isParen result) *)
(*  X.intersect x y ==> x `X.intersect` y where _ = not (isInfixApp original) && not (isParen result) *)
(* -- MATHS *)
(*  fromIntegral x ==> x where _ = isLitInt x *)
(*  fromInteger x ==> x where _ = isLitInt x *)
(*  x + negate y ==> x - y *)
(*  0 - x ==> negate x *)
(*  log y / log x ==> logBase x y *)
(*  x ** 0.5 ==> sqrt x *)
(*  sin x / cos x ==> tan x *)
(*  sinh x / cosh x ==> tanh x *)
(*  n `rem` 2 == 0 ==> even n *)
(*  n `rem` 2 /= 0 ==> odd n *)
(*  not (even x) ==> odd x *)
(*  not (odd x) ==> even x *)
(*  x ** 0.5 ==> sqrt x *)
(*  x ^^ y ==> x ** y where _ = isLitInt y *)
(*  x ^ 0 ==> 1 *)
(*  round (x - 0.5) ==> floor x *)
(* -- CONCURRENT *)
(*  mapM_ (writeChan a) ==> writeList2Chan a *)
(* -- EXCEPTION *)
(*  Prelude.catch ==> Control.Exception.catch where note = "Prelude.catch does not catch most exceptions" *)
(*  flip Control.Exception.catch ==> handle *)
(*  flip handle ==> Control.Exception.catch *)
(*  flip (catchJust p) ==> handleJust p *)
(*  flip (handleJust p) ==> catchJust p *)
(*  Control.Exception.bracket b (const a) (const t) ==> Control.Exception.bracket_ b a t *)
(*  Control.Exception.bracket (openFile x y) hClose ==> withFile x y *)
(*  Control.Exception.bracket (openBinaryFile x y) hClose ==> withBinaryFile x y *)
(*  throw (ErrorCall a) ==> error a *)
(*  a `seq` return a ==> Control.Exception.evaluate a *)
(*  toException NonTermination ==> nonTermination *)
(*  toException NestedAtomically ==> nestedAtomically *)
(* -- WEAK POINTERS *)
(*  mkWeak a a b ==> mkWeakPtr a b *)
(*  mkWeak a (a, b) c ==> mkWeakPair a b c *)

subsection ‹Evaluate›

text ‹@{verbatim ‹ True && x ==> x› } ›
lemma "(TT andalso x) = x" by auto

text ‹@{verbatim ‹ False && x ==> False› } ›
lemma "(FF andalso x) = FF" by auto

text ‹@{verbatim ‹ True || x ==> True› } ›
lemma "(TT orelse x) = TT" by auto

text ‹@{verbatim ‹ False || x ==> x› } ›
lemma "(FF orelse x) = x" by auto

text ‹@{verbatim ‹ not True ==> False› } ›
lemma "neg⋅TT = FF" by auto

text ‹@{verbatim ‹ not False ==> True› } ›
lemma "neg⋅FF = TT" by auto

(*  Nothing >>= k ==> Nothing *)
(*  either f g (Left x) ==> f x *)
(*  either f g (Right y) ==> g y *)
text ‹@{verbatim ‹ fst (x,y) ==> x› } ›
lemma "fst⋅⟨x, y⟩ = x" by auto

text ‹@{verbatim ‹ snd (x,y) ==> y› } ›
lemma "snd⋅⟨x, y⟩ = y" by auto

text ‹@{verbatim ‹ f (fst p) (snd p) ==> uncurry f p› } ›
lemma "f⋅(fst⋅p)⋅(snd⋅p) = uncurry⋅f⋅p"
  by (cases p, auto)

text ‹@{verbatim ‹ init [x] ==> []› } ›
lemma "init⋅[x] = []" by auto

text ‹@{verbatim ‹ null [] ==> True› } ›
lemma "null⋅[] = TT" by auto

text ‹@{verbatim ‹ length [] ==> 0› } ›
lemma "length⋅[] = 0" by auto

text ‹@{verbatim ‹ foldl f z [] ==> z› } ›
lemma "foldl⋅f⋅z⋅[] = z" by simp

text ‹@{verbatim ‹ foldr f z [] ==> z› } ›
lemma "foldr⋅f⋅z⋅[] = z" by auto

text ‹@{verbatim ‹ foldr1 f [x] ==> x› } ›
lemma "foldr1⋅f⋅[x] = x" by simp

text ‹@{verbatim ‹ scanr f z [] ==> [z]› } ›
lemma "scanr⋅f⋅z⋅[] = [z]" by simp

text ‹@{verbatim ‹ scanr1 f [] ==> []› } ›
lemma "scanr1⋅f⋅[] = []" by simp

text ‹@{verbatim ‹ scanr1 f [x] ==> [x]› } ›
lemma "scanr1⋅f⋅[x] = [x]" by simp

text ‹@{verbatim ‹ take n [] ==> []› } ›
lemma "take⋅n⋅[] ⊑ []" by (cases n, auto)

text ‹@{verbatim ‹ drop n [] ==> []› } ›
lemma "drop⋅n⋅[] ⊑ []"
  by (subst drop.simps) (auto simp: if_equal)

text ‹@{verbatim ‹ takeWhile p [] ==> []› } ›
lemma "takeWhile⋅p⋅[] = []" by (fixrec_simp)

text ‹@{verbatim ‹ dropWhile p [] ==> []› } ›
lemma "dropWhile⋅p⋅[] = []" by (fixrec_simp)

text ‹@{verbatim ‹ span p [] ==> ([],[])› } ›
lemma "span⋅p⋅[] = ⟨[], []⟩" by (fixrec_simp)

(*  lines "" ==> [] *)
(*  unwords [] ==> "" *)
(*  x - 0 ==> x *)
(*  x * 1 ==> x *)
(*  x / 1 ==> x *)
text ‹@{verbatim ‹ concat [a] ==> a› } ›
lemma "concat⋅[a] = a" by auto

text ‹@{verbatim ‹ concat [] ==> []› } ›
lemma "concat⋅[] = []" by auto

text ‹@{verbatim ‹ zip [] [] ==> []› } ›
lemma "zip⋅[]⋅[] = []" by auto

text ‹@{verbatim ‹ id x ==> x› } ›
lemma "ID⋅x = x" by auto

text ‹@{verbatim ‹ const x y ==> x› } ›
lemma "const⋅x⋅y = x" by simp

subsection ‹Complex hints›

text ‹@{verbatim ‹ take (length t) s == t ==> t `Data.List.isPrefixOf` s› } ›
lemma
  fixes t :: "['a::Eq_sym]"
  shows "eq⋅(take⋅(length⋅t)⋅s)⋅t ⊑ isPrefixOf⋅t⋅s"
  by (subst eq_sym) (rule eq_take_length_isPrefixOf)

text ‹@{verbatim ‹ (take i s == t) ==> _eval_ ((i >= length t) && (t `Data.List.isPrefixOf` s))› } ›
text ‹The hint is not true in general, as the following two lemmas show:›
lemma
  assumes "t = []" and "s = x : xs" and "i = 1"
  shows "¬ (eq⋅(take⋅i⋅s)⋅t ⊑ (le⋅(length⋅t)⋅i andalso isPrefixOf⋅t⋅s))"
  using assms by simp

lemma
  assumes "le⋅0⋅i = TT" and "le⋅i⋅0 = FF"
    and "s = ⊥" and "t = []"
  shows "¬ ((le⋅(length⋅t)⋅i andalso isPrefixOf⋅t⋅s) ⊑ eq⋅(take⋅i⋅s)⋅t)"
  using assms by (subst take.simps) simp

(* -- clever hint, but not actually a good idea *)
(*  (do a <- f; g a) ==> f >>= g *)
(*  a $$$$ b $$$$ c ==> a . b $$$$$ c *)

(* not (a == b) ==> a /= b *)
lemma "neg⋅(eq⋅a⋅b) = neq⋅a⋅b" by auto

text ‹@{verbatim ‹not (a /= b) ==> a == b› } ›
lemma "neg⋅(neq⋅a⋅b) = eq⋅a⋅b" by auto

text ‹@{verbatim ‹map id ==> id› } ›
lemma map_id:"map⋅ID = ID" by (auto simp add: cfun_eq_iff)

text ‹@{verbatim ‹x == [] ==> null x› } ›
lemma "eq⋅x⋅[] = null⋅x" by (cases x, auto)

text ‹@{verbatim ‹any id ==> or› } ›
lemma "any⋅ID = the_or" by (auto simp add:map_id)

text ‹@{verbatim ‹all id ==> and› } ›
lemma "all⋅ID = the_and" by (auto simp add:map_id)

text ‹@{verbatim ‹(if x then False else y) ==> (not x && y)› } ›
lemma "(If x then FF else y) = (neg⋅x andalso y)" by (cases x, auto)

text ‹@{verbatim ‹(if x then y else True) ==> (not x || y)› } ›
lemma "(If x then y else TT) = (neg⋅x orelse y)" by (cases x, auto)

text ‹@{verbatim ‹not (not x) ==> x› } ›
lemma "neg⋅(neg⋅x) = x" by auto

text ‹@{verbatim ‹(if c then f x else f y) ==> f (if c then x else y)› } ›
lemma "(If c then f⋅x else f⋅y) ⊑ f⋅(If c then x else y)" by (cases c, auto)

text ‹@{verbatim ‹(\ x -> [x]) ==> (: [])› } ›
lemma "(Λ x. [x]) = (Λ z. z : [])" by auto

text ‹@{verbatim ‹True == a ==> a› } ›
lemma "eq⋅TT⋅a = a" by (cases a, auto)

text ‹@{verbatim ‹False == a ==> not a› } ›
lemma "eq⋅FF⋅a = neg⋅a" by (cases a, auto)

text ‹@{verbatim ‹a /= True ==> not a› } ›
lemma "neq⋅a⋅TT = neg⋅a" by (cases a, auto)

text ‹@{verbatim ‹a /= False ==> a› } ›
lemma "neq⋅a⋅FF = a" by (cases a, auto)

text ‹@{verbatim ‹True /= a ==> not a› } ›
lemma "neq⋅TT⋅a = neg⋅a" by (cases a, auto)

text ‹@{verbatim ‹False /= a ==> a› } ›
lemma "neq⋅FF⋅a = a" by (cases a, auto)

text ‹@{verbatim ‹not (isNothing x) ==> isJust x› } ›
lemma "neg⋅(isNothing⋅x) = isJust⋅x" by auto

text ‹@{verbatim ‹not (isJust x) ==> isNothing x› } ›
lemma "neg⋅(isJust⋅x) = isNothing⋅x" by auto

text ‹@{verbatim ‹x == Nothing ==> isNothing x› } ›
lemma "eq⋅x⋅Nothing = isNothing⋅x" by (cases x, auto)

text ‹@{verbatim ‹Nothing == x ==> isNothing x› } ›
lemma "eq⋅Nothing⋅x = isNothing⋅x" by (cases x, auto)

text ‹@{verbatim ‹x /= Nothing ==> Data.Maybe.isJust x› } ›
lemma "neq⋅x⋅Nothing = isJust⋅x" by (cases x, auto)

text ‹@{verbatim ‹Nothing /= x ==> Data.Maybe.isJust x› } ›
lemma "neq⋅Nothing⋅x = isJust⋅x" by (cases x, auto)

text ‹@{verbatim ‹(if isNothing x then y else fromJust x) ==> fromMaybe y x› } ›
lemma "(If isNothing⋅x then y else fromJust⋅x) = fromMaybe⋅y⋅x" by (cases x, auto)

text ‹@{verbatim ‹(if isJust x then fromJust x else y) ==> fromMaybe y x› } ›
lemma "(If isJust⋅x then fromJust⋅x else y) = fromMaybe⋅y⋅x" by (cases x, auto)

text ‹@{verbatim ‹(isJust x && (fromJust x == y)) ==> x == Just y› } ›
lemma "(isJust⋅x andalso (eq⋅(fromJust⋅x)⋅y)) = eq⋅x⋅(Just⋅y)" by (cases x, auto)

text ‹@{verbatim ‹elem True ==> or› } ›
lemma "elem⋅TT = the_or"
proof (rule cfun_eqI)
  fix xs
  show "elem⋅TT⋅xs = the_or⋅xs"
    by (induct xs) (auto simp: eq_true)
qed

text ‹@{verbatim ‹notElem False ==> and› } ›
lemma "notElem⋅FF = the_and"
proof (rule cfun_eqI)
  fix xs
  show "notElem⋅FF⋅xs = the_and⋅xs"
    by (induct xs) (auto simp: eq_false)
qed

text ‹@{verbatim ‹all ((/=) a) ==> notElem a› } ›
lemma "all⋅(neq⋅(a::'a::Eq_sym)) = notElem⋅a"
proof (rule cfun_eqI)
  fix xs
  show "all⋅(neq⋅a)⋅xs = notElem⋅a⋅xs"
    by (induct xs) (auto simp: eq_sym)
qed

text ‹@{verbatim ‹maybe x id ==> Data.Maybe.fromMaybe x› } ›
lemma "maybe⋅x⋅ID = fromMaybe⋅x"
proof (rule cfun_eqI)
  fix xs
  show "maybe⋅x⋅ID⋅xs = fromMaybe⋅x⋅xs"
    by (cases xs) auto
qed

text ‹@{verbatim ‹maybe False (const True) ==> Data.Maybe.isJust› } ›
lemma "maybe⋅FF⋅(const⋅TT) = isJust"
proof (rule cfun_eqI)
  fix x :: "'a Maybe"
  show "maybe⋅FF⋅(const⋅TT)⋅x = isJust⋅x"
    by (cases x) simp+
qed

text ‹@{verbatim ‹maybe True (const False) ==> Data.Maybe.isNothing› } ›
lemma "maybe⋅TT⋅(const⋅FF) = isNothing"
proof (rule cfun_eqI)
  fix x :: "'a Maybe"
  show "maybe⋅TT⋅(const⋅FF)⋅x = isNothing⋅x"
    by (cases x) simp+
qed

text ‹@{verbatim ‹maybe [] (: []) ==> maybeToList› } ›
lemma "maybe⋅[]⋅(Λ z. z : []) = maybeToList"
proof (rule cfun_eqI)
  fix x :: "'a Maybe"
  show "maybe⋅[]⋅(Λ z. z : [])⋅x = maybeToList⋅x"
    by (cases x) simp+
qed

text ‹@{verbatim ‹catMaybes (map f x) ==> mapMaybe f x› } ›
lemma "catMaybes⋅(map⋅f⋅x) = mapMaybe⋅f⋅x" by auto

text ‹@{verbatim ‹(if isNothing x then y else f (fromJust x)) ==> maybe y f x› } ›
lemma "(If isNothing⋅x then y else f⋅(fromJust⋅x)) = maybe⋅y⋅f⋅x" by (cases x, auto)

text ‹@{verbatim ‹(if isJust x then f (fromJust x) else y) ==> maybe y f x› } ›
lemma "(If isJust⋅x then f⋅(fromJust⋅x) else y) = maybe⋅y⋅f⋅x" by (cases x, auto)

text ‹@{verbatim ‹(map fromJust . filter isJust) ==> Data.Maybe.catMaybes› } ›
lemma "(map⋅fromJust oo filter⋅isJust) = catMaybes"
proof (rule cfun_eqI)
  fix xs :: "['a Maybe]"
  show "(map⋅fromJust oo filter⋅isJust)⋅xs = catMaybes⋅xs"
  proof (induct xs)
    case (Cons y ys)
    then show ?case by (cases y) simp+
  qed simp+
qed

text ‹@{verbatim ‹concatMap (maybeToList . f) ==> Data.Maybe.mapMaybe f› } ›
lemma "concatMap⋅(maybeToList oo f) = mapMaybe⋅f"
proof (rule cfun_eqI)
  fix xs
  show "concatMap⋅(maybeToList oo f)⋅xs = mapMaybe⋅f⋅xs"
    by (induct xs) auto
qed

text ‹@{verbatim ‹concatMap maybeToList ==> catMaybes› } ›
lemma "concatMap⋅maybeToList = catMaybes" by auto

text ‹@{verbatim ‹mapMaybe f (map g x) ==> mapMaybe (f . g) x› } ›
lemma "mapMaybe⋅f⋅(map⋅g⋅x) = mapMaybe⋅(f oo g)⋅x" by auto

text ‹@{verbatim ‹(($) . f) ==> f› } ›
lemma "(dollar oo f) = f" by (auto simp add:cfun_eq_iff)

text ‹@{verbatim ‹(f $) ==> f› } ›
lemma "(Λ z. dollar⋅f⋅z) = f" by (auto simp add:cfun_eq_iff)

text ‹@{verbatim ‹(\ a b -> g (f a) (f b)) ==> g `Data.Function.on` f› } ›
lemma "(Λ a b. g⋅(f⋅a)⋅(f⋅b)) = on⋅g⋅f" by (auto simp add:cfun_eq_iff)

text ‹@{verbatim ‹id $! x ==> x› } ›
lemma "dollarBang⋅ID⋅x = x" by (auto simp add:seq_def)

text ‹@{verbatim ‹[x | x <- y] ==> y› } ›
lemma "[x | x <- y] = y" by (induct y, auto)

text ‹@{verbatim ‹isPrefixOf (reverse x) (reverse y) ==> isSuffixOf x y› } ›
lemma "isPrefixOf⋅(reverse⋅x)⋅(reverse⋅y) = isSuffixOf⋅x⋅y" by auto

text ‹@{verbatim ‹concat (intersperse x y) ==> intercalate x y› } ›
lemma "concat⋅(intersperse⋅x⋅y) = intercalate⋅x⋅y" by auto

text ‹@{verbatim ‹x `seq` y ==> y› } ›
lemma
  assumes "x ≠ ⊥" shows "seq⋅x⋅y = y"
  using assms by (simp add: seq_def)

text ‹@{verbatim ‹f $! x ==> f x› } ›
lemma assumes "x ≠ ⊥" shows "dollarBang⋅f⋅x = f⋅x"
  using assms by (simp add: seq_def)

text ‹@{verbatim ‹maybe (f x) (f . g) ==> (f . maybe x g)› } ›
lemma "maybe⋅(f⋅x)⋅(f oo g) ⊑ (f oo maybe⋅x⋅g)"
proof (rule cfun_belowI)
  fix y
  show "maybe⋅(f⋅x)⋅(f oo g)⋅y ⊑ (f oo maybe⋅x⋅g)⋅y"
    by (cases y) auto
qed

end