Quelle  Nats.thy

(*<*)
(*
 * Domains of natural numbers.
 * (C)opyright 2009-2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

theory Nats
imports HOLCF
begin
(*>*)

section‹Boxed Types, HOL's natural numbers hoisted.›

subsection‹Unboxed naturals.›

text‹We can represent the unboxed naturals as a discrete domain (every
  is equal to itself and unequal to everything else, and there is no
 ). Think of these functions as the machine operations.

  could actually lift all HOL types and classes in this way; indeed
  HOLCF theory "Lift" does something similar, but is not as
 -grained as this development.

 : we default to just CPOs (not pointed CPOs) in this theory. We
  bothg the Isabelle syntax for overloaded arithmetic and the
  for unboxed operators of 🍋‹"SPJ-JL:1991"›.›

default_sort predomain

type_synonym UNat = "nat discr"

instantiation discr :: (zero) zero
begin
definition zero_discr_def: "0 ≡ Discr 0"
instance ..
end

lemma zero_discr[simp]: "undiscr 0 = 0" unfolding zero_discr_def by simp

instantiation discr :: (one) one
begin
definition one_discr_def: "1 ≡ Discr 1"
instance ..
end

lemma one_discr[simp]: "undiscr 1 = 1" unfolding one_discr_def by simp

instantiation discr :: (ord) ord
begin
definition less_def[simp]: "m < n ≡ (undiscr m) < (undiscr n)"
definition le_def[simp]:   "m ≤ n ≡ (undiscr m) ≤ (undiscr n)"
instance ..
end

definition
  uPlus :: "UNat → UNat → UNat" where
  "uPlus ≡ Λ x y. Discr (undiscr x + undiscr y)"

abbreviation
  uPlus_syn :: "UNat ==> UNat ==> UNat" (infixl ‹+_#› 65) where
  "x +_# y ≡ uPlus⋅x⋅y"

instantiation discr :: (plus) plus
begin
definition plus_discr_def[simp]: "x + y ≡ Discr (undiscr x + undiscr y)"
instance ..
end

definition
  uMinus :: "UNat → UNat → UNat" where
  "uMinus ≡ Λ x y. Discr (undiscr x - undiscr y)"

abbreviation
  uMinus_syn :: "UNat ==> UNat ==> UNat" (infixl ‹-_#› 65) where
  "x -_# y ≡ uMinus⋅x⋅y"

instantiation discr :: (minus) minus
begin
definition minus_discr_def[simp]: "x - y ≡ Discr (undiscr x - undiscr y)"
instance ..
end

definition
  uMult :: "UNat → UNat → UNat" where
  "uMult ≡ Λ x y. Discr (undiscr x * undiscr y)"

abbreviation
  uMult_syn :: "UNat ==> UNat ==> UNat" (infixl ‹*_#› 65) where
  "x *_# y ≡ uMult⋅x⋅y"

instantiation discr :: (times) times
begin
definition times_discr_def[simp]: "x * y ≡ Discr (undiscr x * undiscr y)"
instance ..
end

lemma uMult_unit_left: "1 *_# (x::UNat) = x"
  unfolding uMult_def one_discr_def by simp
lemma uMult_unit_right: "(x::UNat) *_# 1 = x"
  unfolding uMult_def one_discr_def by simp

lemma uMult_assoc: "(x *_# y) *_# z = x *_# (y *_# z)"
  unfolding uMult_def by simp

lemma uMult_commute: "x *_# y = y *_# x"
  unfolding uMult_def by simp

lemma uMult_left_commute: "a *_# (b *_# c) = b *_# (a *_# c)"
  unfolding uMult_def by simp

lemmas uMult_arithmetic =
  uMult_unit_left uMult_unit_right uMult_assoc uMult_commute uMult_left_commute

subsection ‹The "@{term ⊥}" monad.›

text‹

  Brian Huffman helpfully observed, the "@{term "⊥"}" type
  supports the monadic operations; it's isomorphic to
 's @{term "Maybe a"}, or ML's @{typ "'a option"}.

  that @{term "return"} is @{term "up"}.

 ›

definition
  bbind :: "('a::cpo)_\<bottom> → ('a → ('b::pcpo)) → 'b" where
  "bbind ≡ Λ b g. fup⋅g⋅b"

abbreviation
  bbind_syn :: "('a::cpo)_\<bottom> ==> ('a → ('b::pcpo)) ==> 'b" (infixl ‹>>=› 65) where
  "b >>= g ≡ bbind⋅b⋅g"

lemma bbind_strict1[simp]: "bbind⋅⊥ = ⊥"
  by (simp add: bbind_def)
lemma bbind_strict2[simp]: "x >>= ⊥ = ⊥"
  by (cases x, simp_all add: bbind_def)

lemma bbind_leftID[simp]: "up⋅a >>= f = f⋅a" by (simp add: bbind_def)
lemma bbind_rightID[simp]: "m >>= up = m" by (cases m, simp_all)

lemma bbind_assoc[simp]: "f >>= g >>= h = f >>= (Λ x. g⋅x >>= h)"
  by (cases f, simp_all)

lemma bbind_case_distr_strict: "f⋅⊥ = ⊥ ==> f⋅(g >>= h) = g >>= (Λ x. f⋅(h⋅x))"
  unfolding bbind_def by (cases g, simp_all)

text‹

  composition is sometimes helpful. It forms a monad too,
  has many useful algebraic properties. Unfortunately it is more
  than is useful to write the lemmas in a way that makes the
 -order unifier in the simplifier happy. Seems easier just to
  the definition and go from there.

 ›

definition
  bKleisli :: "('a::cpo → ('b::cpo)_\<bottom>) → ('b → ('c::cpo)_\<bottom>) → ('a → 'c_\<bottom>)" where
  "bKleisli ≡ Λ f g x. f⋅x >>= g"

abbreviation
  bKleisli_syn :: "('a::cpo → ('b::cpo)_\<bottom>) ==> ('b → ('c::cpo)_\<bottom>) ==> ('a → 'c_\<bottom>)" (infixl ‹>=>› 65) where
  "b >=> g ≡ bKleisli⋅b⋅g"

lemma bKleisli_strict1[simp]: "bKleisli⋅⊥ = ⊥"
  by (simp add: bKleisli_def)
lemma bKleisli_strict2[simp]: "b >=> ⊥ = ⊥"
  by (rule cfun_eqI, simp add: bKleisli_def)

lemma bKleisli_bbind: "(f >>= g) >=> h = f >>= (Λ x. g⋅x >=> h)"
  by (cases f, simp_all)

text ‹

  "Box" type denotes computations that, when demanded, yield
  @{term "⊥"} or an unboxed value. Note that the @{term "Box"}
  is strict, and so merely tags the lifted computation @{typ
 'a_\⊥"}. @{typ "'a"} can be pointed or unpointed. This approach enables
  to distinguish the boxed values from the lifted-function-space that
  recursive functions with unboxed codomains.

 ›

domain 'a Box = Box (unbox :: "'a_\<bottom>")

definition
  box :: "('a::predomain) → 'a Box" where
  "box ≡ Box oo up"

lemma boxI: "Box⋅(up⋅x) = box⋅x" unfolding box_def by simp
lemma unbox_box[simp]: "unbox⋅(box⋅x) = up⋅x" unfolding box_def by simp
lemma unbox_Box[simp]: "x ≠ ⊥ ==> unbox⋅(Box⋅x) = x" by simp

text‹

  we suceed in @{term "box"}ing something, then clearly that
  was not @{term "⊥"}.

 ›

lemma box_casedist[case_names bottom Box, cases type: Box]:
  assumes xbot: "x = ⊥ ==> P"
      and xbox: "∧u. x = box⋅u ==> P"
  shows "P"
proof(cases x)
  case bottom with xbot show ?thesis by simp
next
  case (Box u) with xbox show ?thesis
    by (cases u, simp_all add: box_def up_def cont_Iup bottomI[OF minimal_up])
qed

lemma bbind_leftID'[simp]: "unbox⋅a >>= box = a" by (cases a, simp_all add: bbind_def)

(*<*)
text ‹

  optimisations of 🍋‹"SPJ-JL:1991"›.

 : Repeated unboxing of the same value can be done once (roughly:
  the value in a register). Their story is more general.

 ›

lemma box_repeated:
  "x >>= (Λ x'. f >>= (Λ y'. x >>= body⋅x'⋅y'))
  = x >>= (Λ x'. f >>= (Λ y'. body⋅x'⋅y'⋅x'))"
  by (cases x, simp_all)
(*>*)

text‹Lift binary predicates over @{typ "'a discr"} into @{typ "'a discr Box"}.›

text ‹@{term "bliftM"} and @{term "bliftM2"} encapsulate the boxing
  unboxing.›

definition
  bliftM :: "('a::predomain → 'b::predomain) ==> 'a Box → 'b Box" where
  "bliftM f ≡ Λ x. unbox⋅x >>= (Λ x'. box⋅(f⋅x'))"

lemma bliftM_strict1[simp]: "bliftM f⋅⊥ = ⊥" by (simp add: bliftM_def)
lemma bliftM_op[simp]: "bliftM f⋅(box⋅x) = box⋅(f⋅x)" by (simp add: bliftM_def)

definition
  bliftM2 :: "('a::predomain → 'b::predomain → 'c::predomain) ==> 'a Box → 'b Box → 'c Box" where
  "bliftM2 f ≡ Λ x y. unbox⋅x >>= (Λ x'. unbox⋅y >>= (Λ y'. box⋅(f⋅x'⋅y')))"

lemma bliftM2_strict1[simp]: "bliftM2 f⋅⊥ = ⊥" by (rule cfun_eqI)+ (simp add: bliftM2_def)
lemma bliftM2_strict2[simp]: "bliftM2 f⋅x⋅⊥ = ⊥" by (cases x, simp_all add: bliftM2_def)
lemma bliftM2_op[simp]: "bliftM2 f⋅(box⋅x)⋅(box⋅y) = box⋅(f⋅x⋅y)" by (simp add: bliftM2_def)

text‹

  the arithmetic operations. We need extra continuity lemmas as
 're using the full function space, so we can re-use the conventional
 . The goal is to work at this level.

 ›

instantiation Box :: ("{predomain,plus}") plus
begin
definition plus_Box_def: "x + y ≡ bliftM2 (Λ a b. a + b)⋅x⋅y"
instance ..
end

lemma plus_Box_cont[simp, cont2cont]:
  "[cont g; cont h] ==> cont (λx. (g x :: 'a :: {predomain, plus} Box) + h x)"
  unfolding plus_Box_def by simp

lemma plus_Box_strict1[simp]: "⊥ + (y :: 'a::{predomain, plus} Box) = ⊥"
  unfolding plus_Box_def by simp
lemma plus_Box_strict2[simp]: "(x :: 'a::{predomain, plus} Box) + ⊥ = ⊥"
  unfolding plus_Box_def by simp

instantiation Box :: ("{predomain,minus}") minus
begin
definition minus_Box_def: "x - y ≡ bliftM2 (Λ a b. a - b)⋅x⋅y"
instance ..
end

lemma minus_Box_cont[simp, cont2cont]:
  "[cont g; cont h] ==> cont (λx. (g x :: 'a :: {predomain, minus} Box) - h x)"
  unfolding minus_Box_def by simp

lemma minus_Box_strict1[simp]: "⊥ - (y :: 'a::{predomain, minus} Box) = ⊥"
  unfolding minus_Box_def by simp
lemma minus_Box_strict2[simp]: "(x :: 'a::{predomain, minus} Box) - ⊥ = ⊥"
  unfolding minus_Box_def by simp

instantiation Box :: ("{predomain,times}") times
begin
definition times_Box_def: "x * y ≡ bliftM2 (Λ a b. a * b)⋅x⋅y"
instance ..
end

lemma times_Box_cont[simp, cont2cont]:
  "[cont g; cont h] ==> cont (λx. (g x :: 'a :: {predomain, times} Box) * h x)"
  unfolding times_Box_def by simp

lemma times_Box_strict1[simp]: "⊥ * (y :: 'a::{predomain, times} Box) = ⊥"
  unfolding times_Box_def by simp
lemma times_Box_strict2[simp]: "(x :: 'a::{predomain, times} Box) * ⊥ = ⊥"
  unfolding times_Box_def by simp

definition
  bpred :: "('a::countable discr ==> 'a discr ==> bool) ==> 'a discr Box → 'a discr Box → tr" where
  "bpred p ≡ Λ x y. unbox⋅x >>= (Λ x'. unbox⋅y >>= (Λ y'. if p x' y' then TT else FF))"

lemma bpred_strict1[simp]: "bpred p⋅⊥ = ⊥" unfolding bpred_def by (rule cfun_eqI, simp)
lemma bpred_strict2[simp]: "bpred p⋅x⋅⊥ = ⊥" unfolding bpred_def by (cases x, simp_all)

lemma bpred_eval[simp]: "bpred p⋅(box⋅x)⋅(box⋅y) = (if p x y then TT else FF)"
  unfolding bpred_def by simp

abbreviation
  beq_syn :: "'a::countable discr Box ==> 'a discr Box ==> tr" (infix ‹=_B› 50) where
  "x =_B y ≡ bpred (=)⋅x⋅y"

abbreviation
  ble_syn :: "'a::{countable,ord} discr Box ==> 'a discr Box ==> tr" (infix ‹≤_B› 50) where
  "x ≤_B y ≡ bpred (≤)⋅x⋅y"

abbreviation
  blt_syn :: "'a::{countable,ord} discr Box ==> 'a discr Box ==> tr" (infix ‹<\<^sub>B› 50) where
  "x <_B y ≡ bpred (<)⋅x⋅y"

subsection‹The flat domain of natural numbers›

text‹Lift arithmetic to the boxed naturals. Define some things that make
  with boxed naturals more convenient.›

type_synonym Nat = "UNat Box"

instantiation Box :: ("{predomain, zero}") zero
begin
definition zero_Nat_def: "0 ≡ box⋅0"
instance ..
end

instantiation Box :: ("{predomain, one}") one
begin
definition one_Nat_def: "1 ≡ box⋅1"
instance ..
end

text ‹We need to know the underlying operations are continuous for these to work.›

lemma plus_Nat_eval[simp]: "(box⋅x :: Nat) + box⋅y = box⋅(x + y)" unfolding plus_Box_def by simp
lemma minus_Nat_eval[simp]: "(box⋅x :: Nat) - box⋅y = box⋅(x - y)" unfolding minus_Box_def by simp
lemma times_Nat_eval[simp]: "(box⋅x :: Nat) * box⋅y = box⋅(x * y)" unfolding times_Box_def by simp

definition
  Nat_case :: "'a::domain → (Nat → 'a) → Nat → 'a" where
  "Nat_case ≡ Λ z s n. unbox⋅n >>= (Λ n'. case_nat z (λn''. s⋅(box⋅(Discr n''))) (undiscr n'))"

lemma cont_case_nat[simp]:
  "[cont (λx. f x); ∧n. cont (λx. g x n) ] ==> cont (λx. case_nat (f x) (g x) n)"
  by (cases n, simp_all)

lemma Nat_case_strict[simp]: "Nat_case⋅z⋅s⋅⊥ = ⊥" by (simp add: Nat_case_def)
lemma Nat_case_zero[simp]: "Nat_case⋅z⋅s⋅0 = z" by (simp add: Nat_case_def zero_Nat_def zero_discr_def)
lemma Nat_case_suc[simp]:  "Nat_case⋅z⋅s⋅(box⋅(Discr (Suc n))) = s⋅(box⋅(Discr n))"
  by (simp add: Nat_case_def)

lemma Nat_case_add_1[simp]:
  assumes ndef: "n ≠ ⊥"
  shows "Nat_case⋅z⋅s⋅(n + 1) = s⋅n"
proof -
  from ndef obtain nu where nu: "n = box⋅nu"
    unfolding box_def
    apply (cases "n" rule: Box.exhaust)
    apply simp
    apply (case_tac "u")
    apply simp_all
    done
  then obtain u where "nu = Discr u"
    unfolding box_def
    apply (cases nu)
    apply simp
    done
  with nu show ?thesis unfolding one_Nat_def by simp
qed

lemma Nat_case_case_nat: "Nat_case⋅z⋅s⋅(box⋅(Discr n)) = case_nat z (λn'. s⋅(box⋅(Discr n'))) n"
  by (simp add: Nat_case_def)

lemma Nat_casedist[case_names bottom zero Suc]:
  fixes x :: Nat
  assumes xbot: "x = ⊥ ==> P"
      and xzero: "x = 0 ==> P"
      and xsuc: "∧n. x = n + 1 ==> P"
  shows "P"
proof(cases x rule: Box.exhaust)
  case bottom with xbot show ?thesis by simp
next
  case (Box u) hence xu: "x = Box⋅u" and ubottom: "u ≠ ⊥" .
  from ubottom obtain n where ndn: "u = up⋅(Discr n)" apply (cases u) apply simp_all apply (case_tac x) apply simp done
  show ?thesis
  proof(cases n)
    case 0 with ndn xu xzero show ?thesis unfolding zero_Nat_def by (simp add: boxI zero_discr_def)
  next
    case (Suc m) with ndn xu xsuc[where n="box⋅(Discr m)"]
    show ?thesis
      unfolding plus_Box_def unfolding one_Nat_def by (simp add: boxI one_discr_def)
  qed
qed

lemma cont_Nat_case[simp]:
  "[cont (λx. f x); ∧n. cont (λx. g x⋅n) ] ==> cont (λx. Nat_case⋅(f x)⋅(g x)⋅n)"
  apply (cases n rule: Nat_casedist)
    apply simp_all
  apply (case_tac na rule: Box.exhaust)
   apply simp_all
  done

lemma Nat_induct[case_names bottom zero Suc]:
  fixes P :: "Nat ==> bool"
  assumes xbot: "P ⊥"
      and xzero: "P 0"
      and xsuc: "∧n. [n ≠ ⊥; P n ] ==> P (n + 1)"
  shows "P x"
proof(cases x rule: box_casedist)
  case bottom with xbot show ?thesis by simp
next
  case (Box u)
  then obtain n where un: "u = Discr n" by (cases u, simp)
  {
    fix n
    have "∧x. x = box⋅(Discr n) ==> P x"
    proof(induct n)
      case 0 with xzero show ?case unfolding zero_Nat_def zero_discr_def by simp
    next
      case (Suc n)
      hence "P (box⋅(Discr n))" by simp
      with xsuc[where n="box⋅(Discr n)"] have "P (box⋅(Discr n) + 1)" unfolding box_def by simp
      with Suc show ?case unfolding one_Nat_def one_discr_def plus_Box_def by simp
    qed
  }
  with un Box show ?thesis by simp
qed

lemma plus_commute: "(x :: Nat) + y = y + x"
proof -
  have dc: "∧u v. (undiscr (u::nat discr) + undiscr v) = (undiscr v + undiscr u)"
    by simp
  thus ?thesis
    apply (cases x)
     apply simp
    apply (cases y)
    by (simp_all add: dc plus_Box_def)
qed

lemma mult_unit: "(x::Nat) * 1 = x"
  unfolding times_Box_def one_Nat_def by (cases x, simp_all)

lemma mult_commute: "(x :: Nat) * y = y * x"
proof -
  have dc: "∧u v. (undiscr (u::nat discr) * undiscr v) = (undiscr v * undiscr u)"
    by simp
  show ?thesis
    apply (cases x)
     apply simp
    apply (cases y)
    by (simp_all add: dc)
qed

lemma mult_assoc: "((x :: Nat) * y) * z = x * (y * z)"
proof -
  have ac: "∧u v w. undiscr (u::nat discr) * (undiscr v * undiscr w)
                   = (undiscr u * undiscr v) * undiscr w" by simp
  show ?thesis
    apply (cases x)
     apply simp
    apply (cases y)
     apply simp
    apply (cases z)
     apply simp
    by (simp add: ac)
qed

text‹Restore the HOLCF default sort.›

default_sort "domain"

(*<*)
end
(*>*)