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

section ‹Type Classes›

theory Type_Classes
  imports HOLCF_Main
begin


subsection ‹Eq class›

class Eq =
  fixes eq :: "'a → 'a → tr"

text ‹
  The Haskell type class does allow /= to be specified separately. For now, we assume
  that all modeled type classes use the default implementation, or an equivalent.
›
fixrec neq :: "'a::Eq → 'a → tr" where
  "neq⋅x⋅y = neg⋅(eq⋅x⋅y)"

class Eq_strict = Eq +
  assumes eq_strict [simp]:
    "eq⋅x⋅⊥ = ⊥"
    "eq⋅⊥⋅y = ⊥"

class Eq_sym = Eq_strict +
  assumes eq_sym: "eq⋅x⋅y = eq⋅y⋅x"

class Eq_equiv = Eq_sym +
  assumes eq_self_neq_FF [simp]: "eq⋅x⋅x ≠ FF"
    and eq_trans: "eq⋅x⋅y = TT ⟹ eq⋅y⋅z = TT ⟹ eq⋅x⋅z = TT"
begin

lemma eq_refl: "eq⋅x⋅x ≠ ⊥ ⟹ eq⋅x⋅x = TT"
  by (cases "eq⋅x⋅x") simp+

end

class Eq_eq = Eq_sym +
  assumes eq_self_neq_FF': "eq⋅x⋅x ≠ FF"
    and eq_TT_dest: "eq⋅x⋅y = TT ⟹ x = y"
begin

subclass Eq_equiv
  by standard (auto simp: eq_self_neq_FF' dest: eq_TT_dest)

lemma eqD [dest]:
  "eq⋅x⋅y = TT ⟹ x = y"
  "eq⋅x⋅y = FF ⟹ x ≠ y"
  by (auto elim: eq_TT_dest)

end

subsubsection ‹Class instances›

instantiation lift :: (countable) Eq_eq
begin

definition "eq ≡ (Λ(Def x) (Def y). Def (x = y))"

instance
  by standard (auto simp: eq_lift_def flift1_def split: lift.splits)

end

lemma eq_ONE_ONE [simp]: "eq⋅ONE⋅ONE = TT"
  unfolding ONE_def eq_lift_def by simp


subsection ‹Ord class›

domain Ordering = LT | EQ | GT

definition oppOrdering :: "Ordering → Ordering" where
  "oppOrdering = (Λ x. case x of LT ⇒ GT | EQ ⇒ EQ | GT ⇒ LT)"

lemma oppOrdering_simps [simp]:
  "oppOrdering⋅LT = GT"
  "oppOrdering⋅EQ = EQ"
  "oppOrdering⋅GT = LT"
  "oppOrdering⋅⊥ = ⊥"
  unfolding oppOrdering_def by simp_all

class Ord = Eq +
  fixes compare :: "'a → 'a → Ordering"
begin

definition lt :: "'a → 'a → tr" where
  "lt = (Λ x y. case compare⋅x⋅y of LT ⇒ TT | EQ ⇒ FF | GT ⇒ FF)"

definition le :: "'a → 'a → tr" where
  "le = (Λ x y. case compare⋅x⋅y of LT ⇒ TT | EQ ⇒ TT | GT ⇒ FF)"

lemma lt_eq_TT_iff: "lt⋅x⋅y = TT ⟷ compare⋅x⋅y = LT"
  by (cases "compare⋅x⋅y") (simp add: lt_def)+

end

class Ord_strict = Ord +
  assumes compare_strict [simp]:
    "compare⋅⊥⋅y = ⊥"
    "compare⋅x⋅⊥ = ⊥"
begin

lemma lt_strict [simp]:
  shows "lt⋅⊥⋅x = ⊥"
    and "lt⋅x⋅⊥ = ⊥"
  by (simp add: lt_def)+

lemma le_strict [simp]:
  shows "le⋅⊥⋅x = ⊥"
    and "le⋅x⋅⊥ = ⊥"
  by (simp add: le_def)+

end

text ‹TODO: It might make sense to have a class for preorders too,
analogous to class ‹eq_equiv›.›

class Ord_linear = Ord_strict +
  assumes eq_conv_compare: "eq⋅x⋅y = is_EQ⋅(compare⋅x⋅y)"
    and oppOrdering_compare [simp]:
    "oppOrdering⋅(compare⋅x⋅y) = compare⋅y⋅x"
    and compare_EQ_dest: "compare⋅x⋅y = EQ ⟹ x = y"
    and compare_self_below_EQ: "compare⋅x⋅x ⊑ EQ"
    and compare_LT_trans:
    "compare⋅x⋅y = LT ⟹ compare⋅y⋅z = LT ⟹ compare⋅x⋅z = LT"
  (*BH: Is this set of axioms complete?*)
  (*CS: How about totality of the order?*)
begin

lemma eq_TT_dest: "eq⋅x⋅y = TT ⟹ x = y"
  by (cases "compare⋅x⋅y") (auto dest: compare_EQ_dest simp: eq_conv_compare)+

lemma le_iff_lt_or_eq:
  "le⋅x⋅y = TT ⟷ lt⋅x⋅y = TT ∨ eq⋅x⋅y = TT"
  by (cases "compare⋅x⋅y") (simp add: le_def lt_def eq_conv_compare)+

lemma compare_sym:
  "compare⋅x⋅y = (case compare⋅y⋅x of LT ⇒ GT | EQ ⇒ EQ | GT ⇒ LT)"
  by (subst oppOrdering_compare [symmetric]) (simp add: oppOrdering_def)

lemma compare_self_neq_LT [simp]: "compare⋅x⋅x ≠ LT"
  using compare_self_below_EQ [of x] by clarsimp

lemma compare_self_neq_GT [simp]: "compare⋅x⋅x ≠ GT"
  using compare_self_below_EQ [of x] by clarsimp

declare compare_self_below_EQ [simp]

lemma lt_trans: "lt⋅x⋅y = TT ⟹ lt⋅y⋅z = TT ⟹ lt⋅x⋅z = TT"
  unfolding lt_eq_TT_iff by (rule compare_LT_trans)

lemma compare_GT_iff_LT: "compare⋅x⋅y = GT ⟷ compare⋅y⋅x = LT"
  by (cases "compare⋅x⋅y", simp_all add: compare_sym [of y x])

lemma compare_GT_trans:
  "compare⋅x⋅y = GT ⟹ compare⋅y⋅z = GT ⟹ compare⋅x⋅z = GT"
  unfolding compare_GT_iff_LT by (rule compare_LT_trans)

lemma compare_EQ_iff_eq_TT:
  "compare⋅x⋅y = EQ ⟷ eq⋅x⋅y = TT"
  by (cases "compare⋅x⋅y") (simp add: is_EQ_def eq_conv_compare)+

lemma compare_EQ_trans:
  "compare⋅x⋅y = EQ ⟹ compare⋅y⋅z = EQ ⟹ compare⋅x⋅z = EQ"
  by (blast dest: compare_EQ_dest)

lemma le_trans:
  "le⋅x⋅y = TT ⟹ le⋅y⋅z = TT ⟹ le⋅x⋅z = TT"
  by (auto dest: eq_TT_dest lt_trans simp: le_iff_lt_or_eq)

lemma neg_lt: "neg⋅(lt⋅x⋅y) = le⋅y⋅x"
  by (cases "compare⋅x⋅y", simp_all add: le_def lt_def compare_sym [of y x])

lemma neg_le: "neg⋅(le⋅x⋅y) = lt⋅y⋅x"
  by (cases "compare⋅x⋅y", simp_all add: le_def lt_def compare_sym [of y x])

subclass Eq_eq
proof
  fix x y
  show "eq⋅x⋅y = eq⋅y⋅x"
    unfolding eq_conv_compare
    by (cases "compare⋅x⋅y", simp_all add: compare_sym [of y x])
  show "eq⋅x⋅⊥ = ⊥"
    unfolding eq_conv_compare by simp
  show "eq⋅⊥⋅y = ⊥"
    unfolding eq_conv_compare by simp
  show "eq⋅x⋅x ≠ FF"
    unfolding eq_conv_compare
    by (cases "compare⋅x⋅x", simp_all)
  { assume "eq⋅x⋅y = TT" then show "x = y"
      unfolding eq_conv_compare
      by (cases "compare⋅x⋅y", auto dest: compare_EQ_dest) }
qed

end

text ‹A combinator for defining Ord instances for datatypes.›

definition thenOrdering :: "Ordering → Ordering → Ordering" where
  "thenOrdering = (Λ x y. case x of LT ⇒ LT | EQ ⇒ y | GT ⇒ GT)"

lemma thenOrdering_simps [simp]:
  "thenOrdering⋅LT⋅y = LT"
  "thenOrdering⋅EQ⋅y = y"
  "thenOrdering⋅GT⋅y = GT"
  "thenOrdering⋅⊥⋅y = ⊥"
  unfolding thenOrdering_def by simp_all

lemma thenOrdering_LT_iff [simp]:
  "thenOrdering⋅x⋅y = LT ⟷ x = LT ∨ x = EQ ∧ y = LT"
  by (cases x, simp_all)

lemma thenOrdering_EQ_iff [simp]:
  "thenOrdering⋅x⋅y = EQ ⟷ x = EQ ∧ y = EQ"
  by (cases x, simp_all)

lemma thenOrdering_GT_iff [simp]:
  "thenOrdering⋅x⋅y = GT ⟷ x = GT ∨ x = EQ ∧ y = GT"
  by (cases x, simp_all)

lemma thenOrdering_below_EQ_iff [simp]:
  "thenOrdering⋅x⋅y ⊑ EQ ⟷ x ⊑ EQ ∧ (x = ⊥ ∨ y ⊑ EQ)"
  by (cases x) simp_all

lemma is_EQ_thenOrdering [simp]:
  "is_EQ⋅(thenOrdering⋅x⋅y) = (is_EQ⋅x andalso is_EQ⋅y)"
  by (cases x) simp_all

lemma oppOrdering_thenOrdering:
  "oppOrdering⋅(thenOrdering⋅x⋅y) =
    thenOrdering⋅(oppOrdering⋅x)⋅(oppOrdering⋅y)"
  by (cases x) simp_all

instantiation lift :: ("{linorder,countable}") Ord_linear
begin

definition
  "compare ≡ (Λ (Def x) (Def y).
    if x < y then LT else if x > y then GT else EQ)"

instance proof
  fix x y z :: "'a lift"
  show "compare⋅⊥⋅y = ⊥"
    unfolding compare_lift_def by simp
  show "compare⋅x⋅⊥ = ⊥"
    unfolding compare_lift_def by (cases x, simp_all)
  show "oppOrdering⋅(compare⋅x⋅y) = compare⋅y⋅x"
    unfolding compare_lift_def
    by (cases x, cases y, simp, simp,
      cases y, simp, simp add: not_less less_imp_le)
  { assume "compare⋅x⋅y = EQ" then show "x = y"
      unfolding compare_lift_def
      by (cases x, cases y, simp, simp,
        cases y, simp, simp split: if_splits) }
  { assume "compare⋅x⋅y = LT" and "compare⋅y⋅z = LT" then show "compare⋅x⋅z = LT"
      unfolding compare_lift_def
      by (cases x, simp, cases y, simp, cases z, simp,
        auto split: if_splits) }
  show "eq⋅x⋅y = is_EQ⋅(compare⋅x⋅y)"
    unfolding eq_lift_def compare_lift_def
    by (cases x, simp, cases y, simp, auto)
  show "compare⋅x⋅x ⊑ EQ"
    unfolding compare_lift_def
    by (cases x, simp_all)
qed

end

lemma lt_le:
  "lt⋅(x::'a::Ord_linear)⋅y = (le⋅x⋅y andalso neq⋅x⋅y)"
  by (cases "compare⋅x⋅y")
     (auto simp: lt_def le_def eq_conv_compare)

end

section ‹Cpo for Numerals›

theory Numeral_Cpo
  imports HOLCF_Main
begin

class plus_cpo = plus + cpo +
  assumes cont_plus1: "cont (λx::'a::{plus,cpo}. x + y)"
  assumes cont_plus2: "cont (λy::'a::{plus,cpo}. x + y)"
begin

abbreviation plus_section :: "'a → 'a → 'a" ("'(+')") where
  "(+) ≡ Λ x y. x + y"

abbreviation plus_section_left :: "'a ⇒ 'a → 'a" ("'(_+')") where
  "(x+) ≡ Λ y. x + y"

abbreviation plus_section_right :: "'a ⇒ 'a → 'a" ("'(+_')") where
  "(+y) ≡ Λ x. x + y"

end

class minus_cpo = minus + cpo +
  assumes cont_minus1: "cont (λx::'a::{minus,cpo}. x - y)"
  assumes cont_minus2: "cont (λy::'a::{minus,cpo}. x - y)"
begin

abbreviation minus_section :: "'a → 'a → 'a" ("'(-')") where
  "(-) ≡ Λ x y. x - y"

abbreviation minus_section_left :: "'a ⇒ 'a → 'a" ("'(_-')") where
  "(x-) ≡ Λ y. x - y"

abbreviation minus_section_right :: "'a ⇒ 'a → 'a" ("'(-_')") where
  "(-y) ≡ Λ x. x - y"

end

class times_cpo = times + cpo +
  assumes cont_times1: "cont (λx::'a::{times,cpo}. x * y)"
  assumes cont_times2: "cont (λy::'a::{times,cpo}. x * y)"
begin

(*
This clashes with comment syntax
abbreviation times_section :: "'a → 'a → 'a" ("'(?')") where
  "(?) ≡ Λ x y. x * y"

abbreviation times_section_left :: "'a ⇒ 'a → 'a" ("'(_?')") where
  "(x?) ≡ Λ y. x * y"

abbreviation times_section_right :: "'a ⇒ 'a → 'a" ("'(?_')") where
  "(?y) ≡ Λ x. x - y"
*)
end


lemma cont2cont_plus [simp, cont2cont]:
  assumes "cont (λx. f x)" and "cont (λx. g x)"
  shows "cont (λx. f x + g x :: 'a::plus_cpo)"
  apply (rule cont_apply [OF assms(1) cont_plus1])
  apply (rule cont_apply [OF assms(2) cont_plus2])
  apply (rule cont_const)
  done

lemma cont2cont_minus [simp, cont2cont]:
  assumes "cont (λx. f x)" and "cont (λx. g x)"
  shows "cont (λx. f x - g x :: 'a::minus_cpo)"
  apply (rule cont_apply [OF assms(1) cont_minus1])
  apply (rule cont_apply [OF assms(2) cont_minus2])
  apply (rule cont_const)
  done

lemma cont2cont_times [simp, cont2cont]:
  assumes "cont (λx. f x)" and "cont (λx. g x)"
  shows "cont (λx. f x * g x :: 'a::times_cpo)"
  apply (rule cont_apply [OF assms(1) cont_times1])
  apply (rule cont_apply [OF assms(2) cont_times2])
  apply (rule cont_const)
  done

instantiation u :: ("{zero,cpo}") zero
begin
  definition "zero_u = up⋅(0::'a)"
  instance ..
end

instantiation u :: ("{one,cpo}") one
begin
  definition "one_u = up⋅(1::'a)"
  instance ..
end

instantiation u :: (plus_cpo) plus
begin
  definition "plus_u x y = (Λ(up⋅a) (up⋅b). up⋅(a + b))⋅x⋅y" for x y :: "'a⇩⊥"
  instance ..
end

instantiation u :: (minus_cpo) minus
begin
  definition "minus_u x y = (Λ(up⋅a) (up⋅b). up⋅(a - b))⋅x⋅y" for x y :: "'a⇩⊥"
  instance ..
end

instantiation u :: (times_cpo) times
begin
  definition "times_u x y = (Λ(up⋅a) (up⋅b). up⋅(a * b))⋅x⋅y" for x y :: "'a⇩⊥"
  instance ..
end

lemma plus_u_strict [simp]:
  fixes x :: "_ u" shows "x + ⊥ = ⊥" and "⊥ + x = ⊥"
  unfolding plus_u_def by (cases x, simp, simp)+

lemma minus_u_strict [simp]:
  fixes x :: "_ u" shows "x - ⊥ = ⊥" and "⊥ - x = ⊥"
  unfolding minus_u_def by (cases x, simp_all)+

lemma times_u_strict [simp]:
  fixes x :: "_ u" shows "x * ⊥ = ⊥" and "⊥ * x = ⊥"
  unfolding times_u_def by (cases x, simp_all)+

lemma plus_up_up [simp]: "up⋅x + up⋅y = up⋅(x + y)"
  unfolding plus_u_def by simp

lemma minus_up_up [simp]: "up⋅x - up⋅y = up⋅(x - y)"
  unfolding minus_u_def by simp

lemma times_up_up [simp]: "up⋅x * up⋅y = up⋅(x * y)"
  unfolding times_u_def by simp

instance u :: (plus_cpo) plus_cpo
  by standard (simp_all add: plus_u_def)

instance u :: (minus_cpo) minus_cpo
  by standard (simp_all add: minus_u_def)

instance u :: (times_cpo) times_cpo
  by standard (simp_all add: times_u_def)

instance u :: ("{semigroup_add,plus_cpo}") semigroup_add
proof
  fix a b c :: "'a u"
  show "(a + b) + c = a + (b + c)"
    unfolding plus_u_def
    by (cases a; cases b; cases c) (simp_all add: add.assoc)
qed

instance u :: ("{ab_semigroup_add,plus_cpo}") ab_semigroup_add
proof
  fix a b :: "'a u"
  show "a + b = b + a"
    by (cases a; cases b) (simp_all add: add.commute)
qed

instance u :: ("{monoid_add,plus_cpo}") monoid_add
proof
  fix a :: "'a u"
  show "0 + a = a"
    unfolding zero_u_def by (cases a) simp_all
  show "a + 0 = a"
    unfolding zero_u_def by (cases a) simp_all
qed

instance u :: ("{comm_monoid_add,plus_cpo}") comm_monoid_add
proof
  fix a :: "'a u"
  show "0 + a = a"
    unfolding zero_u_def by (cases a) simp_all
qed

instance u :: ("{numeral, plus_cpo}") numeral ..

instance int :: plus_cpo
  by standard simp_all

instance int :: minus_cpo
  by standard simp_all

end

section ‹Data: Functions›

theory Data_Function
  imports HOLCF_Main
begin

fixrec flip :: "('a -> 'b -> 'c) -> 'b -> 'a -> 'c" where
  "flip⋅f⋅x⋅y = f⋅y⋅x"

fixrec const :: "'a → 'b → 'a" where
  "const⋅x⋅_ = x"

fixrec dollar :: "('a -> 'b) -> 'a -> 'b" where
  "dollar⋅f⋅x = f⋅x"

fixrec dollarBang :: "('a -> 'b) -> 'a -> 'b" where
  "dollarBang⋅f⋅x = seq⋅x⋅(f⋅x)"

fixrec on :: "('b -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'a -> 'c" where
  "on⋅g⋅f⋅x⋅y = g⋅(f⋅x)⋅(f⋅y)"

end

section ‹Data: Bool›

theory Data_Bool
  imports Type_Classes
begin

subsection ‹Class instances›

text ‹Eq›

lemma eq_eqI[case_names bottomLTR bottomRTL LTR RTL]:
  "(x = ⊥ ⟹ y = ⊥) ⟹ (y = ⊥ ⟹ x = ⊥) ⟹ (x = TT ⟹ y = TT) ⟹ (y = TT ⟹ x = TT) ⟹ x = y"
by (metis Exh_tr)

lemma eq_tr_simps [simp]:
  shows "eq⋅TT⋅TT = TT" and "eq⋅TT⋅FF = FF"
    and "eq⋅FF⋅TT = FF" and "eq⋅FF⋅FF = TT"
  unfolding TT_def FF_def eq_lift_def by simp_all

text ‹Ord›

lemma compare_tr_simps [simp]:
  "compare⋅FF⋅FF = EQ"
  "compare⋅FF⋅TT = LT"
  "compare⋅TT⋅FF = GT"
  "compare⋅TT⋅TT = EQ"
  unfolding TT_def FF_def compare_lift_def
  by simp_all

subsection ‹Lemmas›

lemma andalso_eq_TT_iff [simp]:
  "(x andalso y) = TT ⟷ x = TT ∧ y = TT"
  by (cases x, simp_all)

lemma andalso_eq_FF_iff [simp]:
  "(x andalso y) = FF ⟷ x = FF ∨ (x = TT ∧ y = FF)"
  by (cases x, simp_all)

lemma andalso_eq_bottom_iff [simp]:
  "(x andalso y) = ⊥ ⟷ x = ⊥ ∨ (x = TT ∧ y = ⊥)"
  by (cases x, simp_all)

lemma orelse_eq_FF_iff [simp]:
  "(x orelse y) = FF ⟷ x = FF ∧ y = FF"
  by (cases x, simp_all)

lemma orelse_assoc [simp]:
  "((x orelse y) orelse z) = (x orelse y orelse z)"
  by (cases x) auto

lemma andalso_assoc [simp]:
  "((x andalso y) andalso z) = (x andalso y andalso z)"
  by (cases x) auto

lemma neg_orelse [simp]:
  "neg⋅(x orelse y) = (neg⋅x andalso neg⋅y)"
  by (cases x) auto

lemma neg_andalso [simp]:
  "neg⋅(x andalso y) = (neg⋅x orelse neg⋅y)"
  by (cases x) auto

text ‹Not suitable as default simp rules, because they cause the
  simplifier to loop:›
lemma neg_eq_simps:
  "neg⋅x = TT ⟹ x = FF"
  "neg⋅x = FF ⟹ x = TT"
  "neg⋅x = ⊥ ⟹ x = ⊥"
  by (cases x, simp_all)+

lemma neg_eq_TT_iff [simp]: "neg⋅x = TT ⟷ x = FF"
  by (cases x, simp_all)+

lemma neg_eq_FF_iff [simp]: "neg⋅x = FF ⟷ x = TT"
  by (cases x, simp_all)+

lemma neg_eq_bottom_iff [simp]: "neg⋅x = ⊥ ⟷ x = ⊥"
  by (cases x, simp_all)+

(* TODO: set up reorient_proc for TT and FF *)

lemma neg_eq [simp]:
  "neg⋅x = neg⋅y ⟷ x = y"
  by (cases y, simp_all)

lemma neg_neg [simp]:
  "neg⋅(neg⋅x) = x"
  by (cases x, auto)

lemma neg_comp_neg [simp]:
  "neg oo neg = ID"
  by (metis cfun_eqI cfcomp2 neg_neg ID1)

end

section ‹Data: Tuple›

theory Data_Tuple
  imports
    Type_Classes
    Data_Bool
begin

subsection ‹Datatype definitions›

domain Unit ("⟨⟩") = Unit ("⟨⟩")

domain ('a, 'b) Tuple2 ("⟨_, _⟩") =
  Tuple2 (lazy fst :: "'a") (lazy snd :: "'b") ("⟨_, _⟩")

notation Tuple2 ("⟨,⟩")

fixrec uncurry :: "('a → 'b → 'c) → ⟨'a, 'b⟩ → 'c"
  where "uncurry⋅f⋅p = f⋅(fst⋅p)⋅(snd⋅p)"

fixrec curry :: "(⟨'a, 'b⟩  → 'c) → 'a → 'b → 'c"
  where "curry⋅f⋅a⋅b = f⋅⟨a, b⟩"

domain ('a, 'b, 'c) Tuple3 ("⟨_, _, _⟩") =
  Tuple3 (lazy "'a") (lazy "'b") (lazy "'c") ("⟨_, _, _⟩")

notation Tuple3 ("⟨,,⟩")

subsection ‹Type class instances›

instantiation Unit :: Ord_linear
begin

definition
  "eq = (Λ ⟨⟩ ⟨⟩. TT)"

definition
  "compare = (Λ ⟨⟩ ⟨⟩. EQ)"

instance
  apply standard
        apply (unfold eq_Unit_def compare_Unit_def)
        apply simp
       apply (rename_tac x, case_tac x, simp, simp)
      apply (rename_tac x y, case_tac x, simp, case_tac y, simp, simp)
     apply (rename_tac x y, case_tac x, case_tac y, simp, simp, case_tac y, simp, simp)
    apply (rename_tac x y, case_tac x, simp, case_tac y, simp, simp)
   apply (rename_tac x, case_tac x, simp, simp)
  apply (rename_tac x y z, case_tac x, simp, case_tac y, simp, case_tac z, simp, simp)
  done

end

instantiation Tuple2 :: (Eq, Eq) Eq_strict
begin

definition
  "eq = (Λ ⟨x1, y1⟩ ⟨x2, y2⟩. eq⋅x1⋅x2 andalso eq⋅y1⋅y2)"

instance proof
  fix x :: "⟨'a, 'b⟩"
  show "eq⋅x⋅⊥ = ⊥"
    unfolding eq_Tuple2_def by (cases x, simp_all)
  show "eq⋅⊥⋅x = ⊥"
    unfolding eq_Tuple2_def by simp
qed

end

lemma eq_Tuple2_simps [simp]:
  "eq⋅⟨x1, y1⟩⋅⟨x2, y2⟩ = (eq⋅x1⋅x2 andalso eq⋅y1⋅y2)"
  unfolding eq_Tuple2_def by simp

instance Tuple2 :: (Eq_sym, Eq_sym) Eq_sym
proof
  fix x y :: "⟨'a, 'b⟩"
  show "eq⋅x⋅y = eq⋅y⋅x"
    unfolding eq_Tuple2_def
    by (cases x, simp, (cases y, simp, simp add: eq_sym)+)
qed

instance Tuple2 :: (Eq_equiv, Eq_equiv) Eq_equiv
proof
  fix x y z :: "⟨'a, 'b⟩"
  show "eq⋅x⋅x ≠ FF"
    by (cases x, simp_all)
  { assume "eq⋅x⋅y = TT" and "eq⋅y⋅z = TT" then show "eq⋅x⋅z = TT"
      by (cases x, simp, cases y, simp, cases z, simp, simp,
          fast intro: eq_trans) }
qed

instance Tuple2 :: (Eq_eq, Eq_eq) Eq_eq
proof
  fix x y :: "⟨'a, 'b⟩"
  show "eq⋅x⋅x ≠ FF"
    by (cases x, simp_all)
  { assume "eq⋅x⋅y = TT" then show "x = y"
      by (cases x, simp, cases y, simp, simp, fast) }
qed

instantiation Tuple2 :: (Ord, Ord) Ord_strict
begin

definition
  "compare = (Λ ⟨x1, y1⟩ ⟨x2, y2⟩.
    thenOrdering⋅(compare⋅x1⋅x2)⋅(compare⋅y1⋅y2))"

instance
  by standard (simp add: compare_Tuple2_def,
      rename_tac x, case_tac x, simp_all add: compare_Tuple2_def)

end

lemma compare_Tuple2_simps [simp]:
  "compare⋅⟨x1, y1⟩⋅⟨x2, y2⟩ = thenOrdering⋅(compare⋅x1⋅x2)⋅(compare⋅y1⋅y2)"
  unfolding compare_Tuple2_def by simp

instance Tuple2 :: (Ord_linear, Ord_linear) Ord_linear
proof
  fix x y z :: "⟨'a, 'b⟩"
  show "eq⋅x⋅y = is_EQ⋅(compare⋅x⋅y)"
    by (cases x, simp, cases y, simp, simp add: eq_conv_compare)
  show "oppOrdering⋅(compare⋅x⋅y) = compare⋅y⋅x"
    by (cases x, simp, cases y, simp, simp add: oppOrdering_thenOrdering)
  { assume "compare⋅x⋅y = EQ" then show "x = y"
      by (cases x, simp, cases y, simp, auto elim: compare_EQ_dest) }
  { assume "compare⋅x⋅y = LT" and "compare⋅y⋅z = LT" then show "compare⋅x⋅z = LT"
      apply (cases x, simp, cases y, simp, cases z, simp, simp)
      apply (elim disjE conjE)
         apply (fast elim!: compare_LT_trans)
        apply (fast dest: compare_EQ_dest)
       apply (fast dest: compare_EQ_dest)
      apply (drule compare_EQ_dest)
      apply (fast elim!: compare_LT_trans)
      done }
  show "compare⋅x⋅x ⊑ EQ"
    by (cases x, simp_all)
qed

instantiation Tuple3 :: (Eq, Eq, Eq) Eq_strict
begin

definition
  "eq = (Λ ⟨x1, y1, z1⟩ ⟨x2, y2, z2⟩.
    eq⋅x1⋅x2 andalso eq⋅y1⋅y2 andalso eq⋅z1⋅z2)"

instance proof
  fix x :: "⟨'a, 'b, 'c⟩"
  show "eq⋅x⋅⊥ = ⊥"
    unfolding eq_Tuple3_def by (cases x, simp_all)
  show "eq⋅⊥⋅x = ⊥"
    unfolding eq_Tuple3_def by simp
qed

end

lemma eq_Tuple3_simps [simp]:
  "eq⋅⟨x1, y1, z1⟩⋅⟨x2, y2, z2⟩ = (eq⋅x1⋅x2 andalso eq⋅y1⋅y2 andalso eq⋅z1⋅z2)"
  unfolding eq_Tuple3_def by simp

instance Tuple3 :: (Eq_sym, Eq_sym, Eq_sym) Eq_sym
proof
  fix x y :: "⟨'a, 'b, 'c⟩"
  show "eq⋅x⋅y = eq⋅y⋅x"
    unfolding eq_Tuple3_def
    by (cases x, simp, (cases y, simp, simp add: eq_sym)+)
qed

instance Tuple3 :: (Eq_equiv, Eq_equiv, Eq_equiv) Eq_equiv
proof
  fix x y z :: "⟨'a, 'b, 'c⟩"
  show "eq⋅x⋅x ≠ FF"
    by (cases x, simp_all)
  { assume "eq⋅x⋅y = TT" and "eq⋅y⋅z = TT" then show "eq⋅x⋅z = TT"
      by (cases x, simp, cases y, simp, cases z, simp, simp,
          fast intro: eq_trans) }
qed

instance Tuple3 :: (Eq_eq, Eq_eq, Eq_eq) Eq_eq
proof
  fix x y :: "⟨'a, 'b, 'c⟩"
  show "eq⋅x⋅x ≠ FF"
    by (cases x, simp_all)
  { assume "eq⋅x⋅y = TT" then show "x = y"
      by (cases x, simp, cases y, simp, simp, fast) }
qed

instantiation Tuple3 :: (Ord, Ord, Ord) Ord_strict
begin

definition
  "compare = (Λ ⟨x1, y1, z1⟩ ⟨x2, y2, z2⟩.
    thenOrdering⋅(compare⋅x1⋅x2)⋅(thenOrdering⋅(compare⋅y1⋅y2)⋅(compare⋅z1⋅z2)))"

instance
  by standard (simp add: compare_Tuple3_def,
    rename_tac x, case_tac x, simp_all add: compare_Tuple3_def)

end

lemma compare_Tuple3_simps [simp]:
  "compare⋅⟨x1, y1, z1⟩⋅⟨x2, y2, z2⟩ =
    thenOrdering⋅(compare⋅x1⋅x2)⋅
      (thenOrdering⋅(compare⋅y1⋅y2)⋅(compare⋅z1⋅z2))"
  unfolding compare_Tuple3_def by simp

instance Tuple3 :: (Ord_linear, Ord_linear, Ord_linear) Ord_linear
proof
  fix x y z :: "⟨'a, 'b, 'c⟩"
  show "eq⋅x⋅y = is_EQ⋅(compare⋅x⋅y)"
    by (cases x, simp, cases y, simp, simp add: eq_conv_compare)
  show "oppOrdering⋅(compare⋅x⋅y) = compare⋅y⋅x"
    by (cases x, simp, cases y, simp, simp add: oppOrdering_thenOrdering)
  { assume "compare⋅x⋅y = EQ" then show "x = y"
      by (cases x, simp, cases y, simp, auto elim: compare_EQ_dest) }
  { assume "compare⋅x⋅y = LT" and "compare⋅y⋅z = LT" then show "compare⋅x⋅z = LT"
      apply (cases x, simp, cases y, simp, cases z, simp, simp)
      apply (elim disjE conjE)
              apply (fast elim!: compare_LT_trans)
             apply (fast dest: compare_EQ_dest)
            apply (fast dest: compare_EQ_dest)
           apply (fast dest: compare_EQ_dest)
          apply (fast dest: compare_EQ_dest)
         apply (drule compare_EQ_dest)
         apply (fast elim!: compare_LT_trans)
        apply (fast dest: compare_EQ_dest)
       apply (fast dest: compare_EQ_dest)
      apply (fast dest: compare_EQ_dest elim!: compare_LT_trans)
      done }
  show "compare⋅x⋅x ⊑ EQ"
    by (cases x, simp_all)
qed

end

section ‹Data: Integers›

theory Data_Integer
  imports
    Numeral_Cpo
    Data_Bool
begin

domain Integer = MkI (lazy int)

instance Integer :: flat
proof
  fix x y :: Integer
  assume "x ⊑ y" then show "x = ⊥ ∨ x = y"
    by (cases x; cases y) simp_all
qed

instantiation Integer :: "{plus,times,minus,uminus,zero,one}"
begin

definition "0 = MkI⋅0"
definition "1 = MkI⋅1"
definition "a + b = (Λ (MkI⋅x) (MkI⋅y). MkI⋅(x + y))⋅a⋅b"
definition "a - b = (Λ (MkI⋅x) (MkI⋅y). MkI⋅(x - y))⋅a⋅b"
definition "a * b = (Λ (MkI⋅x) (MkI⋅y). MkI⋅(x * y))⋅a⋅b"
definition "- a = (Λ (MkI⋅x). MkI⋅(uminus x))⋅a"

instance ..

end

lemma Integer_arith_strict [simp]:
  fixes x :: Integer
  shows "⊥ + x = ⊥" and "x + ⊥ = ⊥"
    and "⊥ * x = ⊥" and "x * ⊥ = ⊥"
    and "⊥ - x = ⊥" and "x - ⊥ = ⊥"
    and "- ⊥ = (⊥::Integer)"
  unfolding plus_Integer_def times_Integer_def
  unfolding minus_Integer_def uminus_Integer_def
  by (cases x, simp, simp)+

lemma Integer_arith_simps [simp]:
  "MkI⋅a + MkI⋅b = MkI⋅(a + b)"
  "MkI⋅a * MkI⋅b = MkI⋅(a * b)"
  "MkI⋅a - MkI⋅b = MkI⋅(a - b)"
  "- MkI⋅a = MkI⋅(uminus a)"
  unfolding plus_Integer_def times_Integer_def
  unfolding minus_Integer_def uminus_Integer_def
  by simp_all

lemma plus_MkI_MkI:
  "MkI⋅x + MkI⋅y = MkI⋅(x + y)"
  unfolding plus_Integer_def by simp

instance Integer :: "{plus_cpo,minus_cpo,times_cpo}"
  by standard (simp_all add: flatdom_strict2cont)

instance Integer :: comm_monoid_add
proof
  fix a b c :: Integer
  show "(a + b) + c = a + (b + c)"
    by (cases a; cases b; cases c) simp_all
  show "a + b = b + a"
    by (cases a; cases b) simp_all
  show "0 + a = a"
    unfolding zero_Integer_def
    by (cases a) simp_all
qed

instance Integer :: comm_monoid_mult
proof
  fix a b c :: Integer
  show "(a * b) * c = a * (b * c)"
    by (cases a; cases b; cases c) simp_all
  show "a * b = b * a"
    by (cases a; cases b) simp_all
  show "1 * a = a"
    unfolding one_Integer_def
    by (cases a) simp_all
qed

instance Integer :: comm_semiring
proof
  fix a b c :: Integer
  show "(a + b) * c = a * c + b * c"
    by (cases a; cases b; cases c) (simp_all add: distrib_right)
qed

instance Integer :: semiring_numeral ..

lemma Integer_add_diff_cancel [simp]:
  "b ≠ ⊥ ⟹ (a::Integer) + b - b = a"
  by (cases a; cases b) simp_all

lemma zero_Integer_neq_bottom [simp]: "(0::Integer) ≠ ⊥"
  by (simp add: zero_Integer_def)

lemma one_Integer_neq_bottom [simp]: "(1::Integer) ≠ ⊥"
  by (simp add: one_Integer_def)

lemma plus_Integer_eq_bottom_iff [simp]:
  fixes x y :: Integer shows "x + y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"
  by (cases x, simp, cases y, simp, simp)

lemma diff_Integer_eq_bottom_iff [simp]:
  fixes x y :: Integer shows "x - y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"
  by (cases x, simp, cases y, simp, simp)

lemma mult_Integer_eq_bottom_iff [simp]:
  fixes x y :: Integer shows "x * y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"
  by (cases x, simp, cases y, simp, simp)

lemma minus_Integer_eq_bottom_iff [simp]:
  fixes x :: Integer shows "- x = ⊥ ⟷ x = ⊥"
  by (cases x, simp, simp)

lemma numeral_Integer_eq: "numeral k = MkI⋅(numeral k)"
  by (induct k, simp_all only: numeral.simps one_Integer_def plus_MkI_MkI)

lemma numeral_Integer_neq_bottom [simp]: "(numeral k::Integer) ≠ ⊥"
  unfolding numeral_Integer_eq by simp

text ‹Symmetric versions are also needed, because the reorient
  simproc does not apply to these comparisons.›

lemma bottom_neq_zero_Integer [simp]: "(⊥::Integer) ≠ 0"
  by (simp add: zero_Integer_def)

lemma bottom_neq_one_Integer [simp]: "(⊥::Integer) ≠ 1"
  by (simp add: one_Integer_def)

lemma bottom_neq_numeral_Integer [simp]: "(⊥::Integer) ≠ numeral k"
  unfolding numeral_Integer_eq by simp

instantiation Integer :: Ord_linear
begin

definition
  "eq = (Λ (MkI⋅x) (MkI⋅y). if x = y then TT else FF)"

definition
  "compare = (Λ (MkI⋅x) (MkI⋅y).
    if x < y then LT else if x > y then GT else EQ)"

instance proof
  fix x y z :: Integer
  show "compare⋅⊥⋅y = ⊥"
    unfolding compare_Integer_def by simp
  show "compare⋅x⋅⊥ = ⊥"
    unfolding compare_Integer_def by (cases x, simp_all)
  show "oppOrdering⋅(compare⋅x⋅y) = compare⋅y⋅x"
    unfolding compare_Integer_def
    by (cases x, cases y, simp, simp,
        cases y, simp, simp add: not_less less_imp_le)
  { assume "compare⋅x⋅y = EQ" then show "x = y"
      unfolding compare_Integer_def
      by (cases x, cases y, simp, simp,
          cases y, simp, simp split: if_splits) }
  { assume "compare⋅x⋅y = LT" and "compare⋅y⋅z = LT" then show "compare⋅x⋅z = LT"
      unfolding compare_Integer_def
      by (cases x, simp, cases y, simp, cases z, simp,
          auto split: if_splits) }
  show "eq⋅x⋅y = is_EQ⋅(compare⋅x⋅y)"
    unfolding eq_Integer_def compare_Integer_def
    by (cases x, simp, cases y, simp, auto)
  show "compare⋅x⋅x ⊑ EQ"
    unfolding compare_Integer_def
    by (cases x, simp_all)
qed

end

lemma eq_MkI_MkI [simp]:
  "eq⋅(MkI⋅m)⋅(MkI⋅n) = (if m = n then TT else FF)"
  by (simp add: eq_Integer_def)

lemma compare_MkI_MkI [simp]:
  "compare⋅(MkI⋅x)⋅(MkI⋅y) = (if x < y then LT else if x > y then GT else EQ)"
  unfolding compare_Integer_def by simp

lemma lt_MkI_MkI [simp]:
  "lt⋅(MkI⋅x)⋅(MkI⋅y) = (if x < y then TT else FF)"
  unfolding lt_def by simp

lemma le_MkI_MkI [simp]:
  "le⋅(MkI⋅x)⋅(MkI⋅y) = (if x ≤ y then TT else FF)"
  unfolding le_def by simp

lemma eq_Integer_bottom_iff [simp]:
  fixes x y :: Integer shows "eq⋅x⋅y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"
  by (cases x, simp, cases y, simp, simp)

lemma compare_Integer_bottom_iff [simp]:
  fixes x y :: Integer shows "compare⋅x⋅y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"
  by (cases x, simp, cases y, simp, simp)

lemma lt_Integer_bottom_iff [simp]:
  fixes x y :: Integer shows "lt⋅x⋅y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"
  by (cases x, simp, cases y, simp, simp)

lemma le_Integer_bottom_iff [simp]:
  fixes x y :: Integer shows "le⋅x⋅y = ⊥ ⟷ x = ⊥ ∨ y = ⊥"
  by (cases x, simp, cases y, simp, simp)

lemma compare_refl_Integer [simp]:
  "(x::Integer) ≠ ⊥ ⟹ compare⋅x⋅x = EQ"
  by (cases x) simp_all

lemma eq_refl_Integer [simp]:
  "(x::Integer) ≠ ⊥ ⟹ eq⋅x⋅x = TT"
  by (cases x) simp_all

lemma lt_refl_Integer [simp]:
  "(x::Integer) ≠ ⊥ ⟹ lt⋅x⋅x = FF"
  by (cases x) simp_all

lemma le_refl_Integer [simp]:
  "(x::Integer) ≠ ⊥ ⟹ le⋅x⋅x = TT"
  by (cases x) simp_all

lemma eq_Integer_numeral_simps [simp]:
  "eq⋅(0::Integer)⋅0 = TT"
  "eq⋅(0::Integer)⋅1 = FF"
  "eq⋅(1::Integer)⋅0 = FF"
  "eq⋅(1::Integer)⋅1 = TT"
  "eq⋅(0::Integer)⋅(numeral k) = FF"
  "eq⋅(numeral k)⋅(0::Integer) = FF"
  "k ≠ Num.One ⟹ eq⋅(1::Integer)⋅(numeral k) = FF"
  "k ≠ Num.One ⟹ eq⋅(numeral k)⋅(1::Integer) = FF"
  "eq⋅(numeral k::Integer)⋅(numeral l) = (if k = l then TT else FF)"
  unfolding zero_Integer_def one_Integer_def numeral_Integer_eq
  by simp_all

lemma compare_Integer_numeral_simps [simp]:
  "compare⋅(0::Integer)⋅0 = EQ"
  "compare⋅(0::Integer)⋅1 = LT"
  "compare⋅(1::Integer)⋅0 = GT"
  "compare⋅(1::Integer)⋅1 = EQ"
  "compare⋅(0::Integer)⋅(numeral k) = LT"
  "compare⋅(numeral k)⋅(0::Integer) = GT"
  "Num.One < k ⟹ compare⋅(1::Integer)⋅(numeral k) = LT"
  "Num.One < k ⟹ compare⋅(numeral k)⋅(1::Integer) = GT"
  "compare⋅(numeral k::Integer)⋅(numeral l) =
    (if k < l then LT else if k > l then GT else EQ)"
  unfolding zero_Integer_def one_Integer_def numeral_Integer_eq
  by simp_all

lemma lt_Integer_numeral_simps [simp]:
  "lt⋅(0::Integer)⋅0 = FF"
  "lt⋅(0::Integer)⋅1 = TT"
  "lt⋅(1::Integer)⋅0 = FF"
  "lt⋅(1::Integer)⋅1 = FF"
  "lt⋅(0::Integer)⋅(numeral k) = TT"
  "lt⋅(numeral k)⋅(0::Integer) = FF"
  "Num.One < k ⟹ lt⋅(1::Integer)⋅(numeral k) = TT"
  "lt⋅(numeral k)⋅(1::Integer) = FF"
  "lt⋅(numeral k::Integer)⋅(numeral l) = (if k < l then TT else FF)"
  unfolding zero_Integer_def one_Integer_def numeral_Integer_eq
  by simp_all

lemma le_Integer_numeral_simps [simp]:
  "le⋅(0::Integer)⋅0 = TT"
  "le⋅(0::Integer)⋅1 = TT"
  "le⋅(1::Integer)⋅0 = FF"
  "le⋅(1::Integer)⋅1 = TT"
  "le⋅(0::Integer)⋅(numeral k) = TT"
  "le⋅(numeral k)⋅(0::Integer) = FF"
  "le⋅(1::Integer)⋅(numeral k) = TT"
  "Num.One < k ⟹ le⋅(numeral k)⋅(1::Integer) = FF"
  "le⋅(numeral k::Integer)⋅(numeral l) = (if k ≤ l then TT else FF)"
  unfolding zero_Integer_def one_Integer_def numeral_Integer_eq
  by simp_all

lemma MkI_eq_0_iff [simp]: "MkI⋅n = 0 ⟷ n = 0"
  unfolding zero_Integer_def by simp

lemma MkI_eq_1_iff [simp]: "MkI⋅n = 1 ⟷ n = 1"
  unfolding one_Integer_def by simp

lemma MkI_eq_numeral_iff [simp]: "MkI⋅n = numeral k ⟷ n = numeral k"
  unfolding numeral_Integer_eq by simp

lemma MkI_0: "MkI⋅0 = 0"
  by simp

lemma MkI_1: "MkI⋅1 = 1"
  by simp

lemma le_plus_1:
  fixes m :: "Integer"
  assumes "le⋅m⋅n = TT"
  shows "le⋅m⋅(n + 1) = TT"
proof -
  from assms have "n ≠ ⊥" by auto
  then have "le⋅n⋅(n + 1) = TT"
    by (cases n) (auto, metis le_MkI_MkI less_add_one less_le_not_le one_Integer_def plus_MkI_MkI)
  with assms show ?thesis by (auto dest: le_trans)
qed

subsection ‹Induction rules that do not break the abstraction›

lemma nonneg_Integer_induct [consumes 1, case_names 0 step]:
  fixes i :: Integer
  assumes i_nonneg: "le⋅0⋅i = TT"
    and zero: "P 0"
    and step: "⋀i. le⋅1⋅i = TT ⟹ P (i - 1) ⟹ P i"
  shows "P i"
proof (cases i)
  case bottom
  then have False using i_nonneg by simp
  then show ?thesis ..
next
  case (MkI integer)
  show ?thesis
  proof (cases integer)
    case neg
    then have False using i_nonneg MkI by (auto simp add: zero_Integer_def one_Integer_def)
    then show ?thesis ..
  next
    case (nonneg nat)
    have "P (MkI⋅(int nat))"
    proof(induct nat)
      case 0
      show ?case using zero by (simp add: zero_Integer_def)
    next
      case (Suc nat)
      have "le⋅1⋅(MkI⋅(int (Suc nat))) = TT"
        by (simp add: one_Integer_def)
      moreover
      have "P (MkI⋅(int (Suc nat)) - 1)"
        using Suc
        by (simp add: one_Integer_def)
      ultimately
      show ?case
        by (rule step)
    qed
    then show ?thesis using nonneg MkI by simp
  qed
qed

end