Theory HOLCF_Main

section ‹Initial Setup for HOLCF-Prelude›

theory HOLCF_Main
  imports
    HOLCF
    "HOLCF-Library.Int_Discrete"
    "HOL-Library.Adhoc_Overloading"
begin

text ‹
  All theories from the Isabelle distribution which are used
  anywhere in the HOLCF-Prelude library must be imported via this file.
  This way, we only have to hide constant names and syntax in one place.
›

hide_type (open) list

hide_const (open)
  List.append List.concat List.Cons List.distinct List.filter List.last
  List.foldr List.foldl List.length List.lists List.map List.Nil List.nth
  List.partition List.replicate List.set List.take List.upto List.zip
  Orderings.less Product_Type.fst Product_Type.snd

no_notation Map.map_add (infixl ‹++› 100)

no_notation List.upto (‹(1[_../_])›)

no_notation
  Rings.divide (infixl ‹div› 70) and
  Rings.modulo (infixl ‹mod› 70)

no_notation
  Set.member  (‹(:)›) and
  Set.member  (‹(‹notation=‹infix :››_/ : _)› [51, 51] 50)

no_translations
  "[x, xs]" == "x # [xs]"
  "[x]" == "x # []"

unbundle no list_enumeration_syntax

no_notation
  List.Nil (‹[]›)

no_syntax "_bracket" :: "types ⇒ type ⇒ type" (‹(‹notation=‹infix =>››[_]/ => _)› [0, 0] 0)
no_syntax "_bracket" :: "types ⇒ type ⇒ type" (‹(‹notation=‹infix ⇒››[_]/ ⇒ _)› [0, 0] 0)

no_translations
  "[x<-xs . P]" == "CONST List.filter (%x. P) xs"

no_syntax (ASCII)
  "_filter" :: "pttrn ⇒ 'a List.list ⇒ bool ⇒ 'a List.list"  (‹(‹indent=1 notation=‹mixfix filter››[_<-_./ _])›)
no_syntax
  "_filter" :: "pttrn ⇒ 'a List.list ⇒ bool ⇒ 'a List.list"  (‹(‹indent=1 notation=‹mixfix filter››[_←_ ./ _])›)

text ‹Declarations that belong in HOLCF/Tr.thy:›

declare trE [cases type: tr]
declare tr_induct [induct type: tr]

end