Theory Nats
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
number is equal to itself and unequal to everything else, and there is no
bottom). Think of these functions as the machine operations.
We could actually lift all HOL types and classes in this way; indeed
the HOLCF theory "Lift" does something similar, but is not as
fine-grained as this development.
Note: we default to just CPOs (not pointed CPOs) in this theory. We
adopt bothg the Isabelle syntax for overloaded arithmetic and the
notation for unboxed operators of \<^citet>‹"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‹
As Brian Huffman helpfully observed, the "@{term "⊥"}" type
constructor supports the monadic operations; it's isomorphic to
Haskell's @{term "Maybe a"}, or ML's @{typ "'a option"}.
Note that @{term "return"} is @{term "up"}.
›
definition
bbind :: "('a::cpo)⇩⊥ → ('a → ('b::pcpo)) → 'b" where
"bbind ≡ Λ b g. fup⋅g⋅b"
abbreviation
bbind_syn :: "('a::cpo)⇩⊥ ⇒ ('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‹
Kleisli composition is sometimes helpful. It forms a monad too,
and has many useful algebraic properties. Unfortunately it is more
work than is useful to write the lemmas in a way that makes the
higher-order unifier in the simplifier happy. Seems easier just to
unfold the definition and go from there.
›
definition
bKleisli :: "('a::cpo → ('b::cpo)⇩⊥) → ('b → ('c::cpo)⇩⊥) → ('a → 'c⇩⊥)" where
"bKleisli ≡ Λ f g x. f⋅x >>= g"
abbreviation
bKleisli_syn :: "('a::cpo → ('b::cpo)⇩⊥) ⇒ ('b → ('c::cpo)⇩⊥) ⇒ ('a → 'c⇩⊥)" (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 ‹
The "Box" type denotes computations that, when demanded, yield
either @{term "⊥"} or an unboxed value. Note that the @{term "Box"}
constructor is strict, and so merely tags the lifted computation @{typ
"'a⇩⊥"}. @{typ "'a"} can be pointed or unpointed. This approach enables
us to distinguish the boxed values from the lifted-function-space that
models recursive functions with unboxed codomains.
›
domain 'a Box = Box (unbox :: "'a⇩⊥")
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‹
If we suceed in @{term "box"}ing something, then clearly that
something 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 ‹
The optimisations of \<^citet>‹"SPJ-JL:1991"›.
p11: Repeated unboxing of the same value can be done once (roughly:
store 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
and 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‹
Define the arithmetic operations. We need extra continuity lemmas as
we're using the full function space, so we can re-use the conventional
operators. 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 "<⇩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
playing 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