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  ("(_/ : _)" [51, 51] 50)

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

no_syntax
  "_list" :: "args ⇒ 'a List.list"    ("[(_)]")

no_notation
  List.Nil ("[]")

no_syntax "_bracket" :: "types ⇒ type ⇒ type" ("([_]/ => _)" [0, 0] 0)
no_syntax "_bracket" :: "types ⇒ type ⇒ type" ("([_]/ ⇒ _)" [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" ("(1[_<-_./ _])")

no_syntax
  "_filter" :: "pttrn ⇒ 'a List.list ⇒ bool ⇒ 'a List.list" ("(1[_←_ ./ _])")

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

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

end