(* Title: HOL/HOLCF/ex/Domain_Proofs.thy
Author: Brian Huffman
*)
section ‹Internal
domain package proofs
done manually
›
theory Domain_Proofs
imports HOLCF
begin
(*
The definitions and proofs below are for the following recursive
datatypes:
domain 'a foo = Foo1 | Foo2 (lazy 'a) (lazy "'a bar")
and 'a bar = Bar (lazy "'a baz \<rightarrow> tr")
and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr")
*)
(********************************************************************)
subsection ‹Step 1: Define the new type combinators
›
text ‹Start
with the one-step non-recursive version
›
definition
foo_bar_baz_deflF ::
"udom defl \ udom defl \ udom defl \ udom defl \ udom defl \ udom defl \ udom defl"
where
"foo_bar_baz_deflF = (\ a. Abs_cfun (\(t1, t2, t3).
( ssum_defl
⋅DEFL(one)
⋅(sprod_defl
⋅(u_defl
⋅a)
⋅(u_defl
⋅t2))
, u_defl
⋅(sfun_defl
⋅(u_defl
⋅t3)
⋅DEFL(tr))
, u_defl
⋅(sfun_defl
⋅(u_defl
⋅(convex_defl
⋅t1))
⋅DEFL(tr)))))
"
lemma foo_bar_baz_deflF_beta:
"foo_bar_baz_deflF\a\t =
( ssum_defl
⋅DEFL(one)
⋅(sprod_defl
⋅(u_defl
⋅a)
⋅(u_defl
⋅(fst (snd t))))
, u_defl
⋅(sfun_defl
⋅(u_defl
⋅(snd (snd t)))
⋅DEFL(tr))
, u_defl
⋅(sfun_defl
⋅(u_defl
⋅(convex_defl
⋅(fst t)))
⋅DEFL(tr)))
"
unfolding foo_bar_baz_deflF_def
by (simp add: split_def)
text ‹Individual type combinators are projected
from the fixed point.
›
definition foo_defl ::
"udom defl \ udom defl"
where "foo_defl = (\ a. fst (fix\(foo_bar_baz_deflF\a)))"
definition bar_defl ::
"udom defl \ udom defl"
where "bar_defl = (\ a. fst (snd (fix\(foo_bar_baz_deflF\a))))"
definition baz_defl ::
"udom defl \ udom defl"
where "baz_defl = (\ a. snd (snd (fix\(foo_bar_baz_deflF\a))))"
lemma defl_apply_thms:
"foo_defl\a = fst (fix\(foo_bar_baz_deflF\a))"
"bar_defl\a = fst (snd (fix\(foo_bar_baz_deflF\a)))"
"baz_defl\a = snd (snd (fix\(foo_bar_baz_deflF\a)))"
unfolding foo_defl_def bar_defl_def baz_defl_def
by simp_all
text ‹Unfold rules
for each combinator.
›
lemma foo_defl_unfold:
"foo_defl\a = ssum_defl\DEFL(one)\(sprod_defl\(u_defl\a)\(u_defl\(bar_defl\a)))"
unfolding defl_apply_thms
by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
lemma bar_defl_unfold:
"bar_defl\a = u_defl\(sfun_defl\(u_defl\(baz_defl\a))\DEFL(tr))"
unfolding defl_apply_thms
by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
lemma baz_defl_unfold:
"baz_defl\a = u_defl\(sfun_defl\(u_defl\(convex_defl\(foo_defl\a)))\DEFL(tr))"
unfolding defl_apply_thms
by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
text "The automation for the previous steps will be quite similar to
how the
fixrec package works.
"
(********************************************************************)
subsection ‹Step 2: Define
types, prove
class instances
›
text ‹Use ‹pcpodef› with the appropriate type combinator.
›
pcpodef 'a foo = "defl_set (foo_defl\DEFL('a))
"
by (rule defl_set_bottom, rule adm_defl_set)
pcpodef 'a bar = "defl_set (bar_defl\DEFL('a))
"
by (rule defl_set_bottom, rule adm_defl_set)
pcpodef 'a baz = "defl_set (baz_defl\DEFL('a))
"
by (rule defl_set_bottom, rule adm_defl_set)
text ‹Prove rep
instance using lemma ‹typedef_rep_class
›.
›
instantiation foo :: (
"domain")
"domain"
begin
definition emb_foo ::
"'a foo \ udom"
where "emb_foo \ (\ x. Rep_foo x)"
definition prj_foo ::
"udom \ 'a foo"
where "prj_foo \ (\ y. Abs_foo (cast\(foo_defl\DEFL('a))\y))"
definition defl_foo ::
"'a foo itself \ udom defl"
where "defl_foo \ \a. foo_defl\DEFL('a)"
definition
"(liftemb :: 'a foo u \ udom u) \ u_map\emb"
definition
"(liftprj :: udom u \ 'a foo u) \ u_map\prj"
definition
"liftdefl \ \(t::'a foo itself). liftdefl_of\DEFL('a foo)"
instance
apply (rule typedef_domain_class)
apply (rule type_definition_foo)
apply (rule below_foo_def)
apply (rule emb_foo_def)
apply (rule prj_foo_def)
apply (rule defl_foo_def)
apply (rule liftemb_foo_def)
apply (rule liftprj_foo_def)
apply (rule liftdefl_foo_def)
done
end
instantiation bar :: (
"domain")
"domain"
begin
definition emb_bar ::
"'a bar \ udom"
where "emb_bar \ (\ x. Rep_bar x)"
definition prj_bar ::
"udom \ 'a bar"
where "prj_bar \ (\ y. Abs_bar (cast\(bar_defl\DEFL('a))\y))"
definition defl_bar ::
"'a bar itself \ udom defl"
where "defl_bar \ \a. bar_defl\DEFL('a)"
definition
"(liftemb :: 'a bar u \ udom u) \ u_map\emb"
definition
"(liftprj :: udom u \ 'a bar u) \ u_map\prj"
definition
"liftdefl \ \(t::'a bar itself). liftdefl_of\DEFL('a bar)"
instance
apply (rule typedef_domain_class)
apply (rule type_definition_bar)
apply (rule below_bar_def)
apply (rule emb_bar_def)
apply (rule prj_bar_def)
apply (rule defl_bar_def)
apply (rule liftemb_bar_def)
apply (rule liftprj_bar_def)
apply (rule liftdefl_bar_def)
done
end
instantiation baz :: (
"domain")
"domain"
begin
definition emb_baz ::
"'a baz \ udom"
where "emb_baz \ (\ x. Rep_baz x)"
definition prj_baz ::
"udom \ 'a baz"
where "prj_baz \ (\ y. Abs_baz (cast\(baz_defl\DEFL('a))\y))"
definition defl_baz ::
"'a baz itself \ udom defl"
where "defl_baz \ \a. baz_defl\DEFL('a)"
definition
"(liftemb :: 'a baz u \ udom u) \ u_map\emb"
definition
"(liftprj :: udom u \ 'a baz u) \ u_map\prj"
definition
"liftdefl \ \(t::'a baz itself). liftdefl_of\DEFL('a baz)"
instance
apply (rule typedef_domain_class)
apply (rule type_definition_baz)
apply (rule below_baz_def)
apply (rule emb_baz_def)
apply (rule prj_baz_def)
apply (rule defl_baz_def)
apply (rule liftemb_baz_def)
apply (rule liftprj_baz_def)
apply (rule liftdefl_baz_def)
done
end
text ‹Prove DEFL rules
using lemma ‹typedef_DEFL
›.
›
lemma DEFL_foo:
"DEFL('a foo) = foo_defl\DEFL('a)"
apply (rule typedef_DEFL)
apply (rule defl_foo_def)
done
lemma DEFL_bar:
"DEFL('a bar) = bar_defl\DEFL('a)"
apply (rule typedef_DEFL)
apply (rule defl_bar_def)
done
lemma DEFL_baz:
"DEFL('a baz) = baz_defl\DEFL('a)"
apply (rule typedef_DEFL)
apply (rule defl_baz_def)
done
text ‹Prove DEFL equations
using type combinator unfold
lemmas.
›
lemma DEFL_foo
': "DEFL('a foo) = DEFL(one
⊕ 'a\<^sub>\ \ ('a bar)
🚫⊥)
"
unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
by (rule foo_defl_unfold)
lemma DEFL_bar
': "DEFL('a bar) = DEFL((
'a baz \ tr)\<^sub>\)"
unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
by (rule bar_defl_unfold)
lemma DEFL_baz
': "DEFL('a baz) = DEFL((
'a foo convex_pd \ tr)\<^sub>\)"
unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
by (rule baz_defl_unfold)
(********************************************************************)
subsection ‹Step 3: Define rep
and abs functions
›
text ‹Define them all
using ‹prj
› and ‹emb
›!
›
definition foo_rep ::
"'a foo \ one \ ('a\<^sub>\ \ ('a bar)\<^sub>\)"
where "foo_rep \ prj oo emb"
definition foo_abs ::
"one \ ('a\<^sub>\ \ ('a bar)\<^sub>\) \ 'a foo"
where "foo_abs \ prj oo emb"
definition bar_rep ::
"'a bar \ ('a baz \ tr)\<^sub>\"
where "bar_rep \ prj oo emb"
definition bar_abs ::
"('a baz \ tr)\<^sub>\ \ 'a bar"
where "bar_abs \ prj oo emb"
definition baz_rep ::
"'a baz \ ('a foo convex_pd \ tr)\<^sub>\"
where "baz_rep \ prj oo emb"
definition baz_abs ::
"('a foo convex_pd \ tr)\<^sub>\ \ 'a baz"
where "baz_abs \ prj oo emb"
text ‹Prove isomorphism rules.
›
lemma foo_abs_iso:
"foo_rep\(foo_abs\x) = x"
by (rule domain_abs_iso [OF DEFL_foo
' foo_abs_def foo_rep_def])
lemma foo_rep_iso:
"foo_abs\(foo_rep\x) = x"
by (rule domain_rep_iso [OF DEFL_foo
' foo_abs_def foo_rep_def])
lemma bar_abs_iso:
"bar_rep\(bar_abs\x) = x"
by (rule domain_abs_iso [OF DEFL_bar
' bar_abs_def bar_rep_def])
lemma bar_rep_iso:
"bar_abs\(bar_rep\x) = x"
by (rule domain_rep_iso [OF DEFL_bar
' bar_abs_def bar_rep_def])
lemma baz_abs_iso:
"baz_rep\(baz_abs\x) = x"
by (rule domain_abs_iso [OF DEFL_baz
' baz_abs_def baz_rep_def])
lemma baz_rep_iso:
"baz_abs\(baz_rep\x) = x"
by (rule domain_rep_iso [OF DEFL_baz
' baz_abs_def baz_rep_def])
text ‹Prove isodefl rules
using ‹isodefl_coerce
›.
›
lemma isodefl_foo_abs:
"isodefl d t \ isodefl (foo_abs oo d oo foo_rep) t"
by (rule isodefl_abs_rep [OF DEFL_foo
' foo_abs_def foo_rep_def])
lemma isodefl_bar_abs:
"isodefl d t \ isodefl (bar_abs oo d oo bar_rep) t"
by (rule isodefl_abs_rep [OF DEFL_bar
' bar_abs_def bar_rep_def])
lemma isodefl_baz_abs:
"isodefl d t \ isodefl (baz_abs oo d oo baz_rep) t"
by (rule isodefl_abs_rep [OF DEFL_baz
' baz_abs_def baz_rep_def])
(********************************************************************)
subsection ‹Step 4: Define map functions, prove isodefl property
›
text ‹Start
with the one-step non-recursive version.
›
text ‹Note that the type of the map
function depends on which
variables are used
in positive
and negative positions.
›
definition
foo_bar_baz_mapF ::
"('a \ 'b) \
(
'a foo \ 'b foo)
× (
'a bar \ 'b bar)
× (
'b baz \ 'a baz)
→
(
'a foo \ 'b foo)
× (
'a bar \ 'b bar)
× (
'b baz \ 'a baz)
"
where
"foo_bar_baz_mapF = (\ f. Abs_cfun (\(d1, d2, d3).
(
foo_abs oo
ssum_map
⋅ID
⋅(sprod_map
⋅(u_map
⋅f)
⋅(u_map
⋅d2))
oo foo_rep
,
bar_abs oo u_map
⋅(cfun_map
⋅d3
⋅ID) oo bar_rep
,
baz_abs oo u_map
⋅(cfun_map
⋅(convex_map
⋅d1)
⋅ID) oo baz_rep
)))
"
lemma foo_bar_baz_mapF_beta:
"foo_bar_baz_mapF\f\d =
(
foo_abs oo
ssum_map
⋅ID
⋅(sprod_map
⋅(u_map
⋅f)
⋅(u_map
⋅(fst (snd d))))
oo foo_rep
,
bar_abs oo u_map
⋅(cfun_map
⋅(snd (snd d))
⋅ID) oo bar_rep
,
baz_abs oo u_map
⋅(cfun_map
⋅(convex_map
⋅(fst d))
⋅ID) oo baz_rep
)
"
unfolding foo_bar_baz_mapF_def
by (simp add: split_def)
text ‹Individual map functions are projected
from the fixed point.
›
definition foo_map ::
"('a \ 'b) \ ('a foo \ 'b foo)"
where "foo_map = (\ f. fst (fix\(foo_bar_baz_mapF\f)))"
definition bar_map ::
"('a \ 'b) \ ('a bar \ 'b bar)"
where "bar_map = (\ f. fst (snd (fix\(foo_bar_baz_mapF\f))))"
definition baz_map ::
"('a \ 'b) \ ('b baz \ 'a baz)"
where "baz_map = (\ f. snd (snd (fix\(foo_bar_baz_mapF\f))))"
lemma map_apply_thms:
"foo_map\f = fst (fix\(foo_bar_baz_mapF\f))"
"bar_map\f = fst (snd (fix\(foo_bar_baz_mapF\f)))"
"baz_map\f = snd (snd (fix\(foo_bar_baz_mapF\f)))"
unfolding foo_map_def bar_map_def baz_map_def
by simp_all
text ‹Prove isodefl rules
for all map functions simultaneously.
›
lemma isodefl_foo_bar_baz:
assumes isodefl_d:
"isodefl d t"
shows
"isodefl (foo_map\d) (foo_defl\t) \
isodefl (bar_map
⋅d) (bar_defl
⋅t)
∧
isodefl (baz_map
⋅d) (baz_defl
⋅t)
"
unfolding map_apply_thms defl_apply_thms
apply (rule parallel_fix_ind)
apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id)
apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms)
apply (simp only: foo_bar_baz_mapF_beta
foo_bar_baz_deflF_beta
fst_conv snd_conv)
apply (elim conjE)
apply (intro
conjI
isodefl_foo_abs
isodefl_bar_abs
isodefl_baz_abs
domain_isodefl
isodefl_ID_DEFL isodefl_LIFTDEFL
isodefl_d
)
apply assumption+
done
lemmas isodefl_foo = isodefl_foo_bar_baz [
THEN conjunct1]
lemmas isodefl_bar = isodefl_foo_bar_baz [
THEN conjunct2,
THEN conjunct1]
lemmas isodefl_baz = isodefl_foo_bar_baz [
THEN conjunct2,
THEN conjunct2]
text ‹Prove map ID
lemmas,
using isodefl_DEFL_imp_ID
›
lemma foo_map_ID:
"foo_map\ID = ID"
apply (rule isodefl_DEFL_imp_ID)
apply (subst DEFL_foo)
apply (rule isodefl_foo)
apply (rule isodefl_ID_DEFL)
done
lemma bar_map_ID:
"bar_map\ID = ID"
apply (rule isodefl_DEFL_imp_ID)
apply (subst DEFL_bar)
apply (rule isodefl_bar)
apply (rule isodefl_ID_DEFL)
done
lemma baz_map_ID:
"baz_map\ID = ID"
apply (rule isodefl_DEFL_imp_ID)
apply (subst DEFL_baz)
apply (rule isodefl_baz)
apply (rule isodefl_ID_DEFL)
done
(********************************************************************)
subsection ‹Step 5: Define take functions, prove lub-take
lemmas›
definition
foo_bar_baz_takeF ::
"('a foo \ 'a foo) \ ('a bar \ 'a bar) \ ('a baz \ 'a baz) \
(
'a foo \ 'a foo)
× (
'a bar \ 'a bar)
× (
'a baz \ 'a baz)
"
where
"foo_bar_baz_takeF = (\ p.
( foo_abs oo
ssum_map
⋅ID
⋅(sprod_map
⋅(u_map
⋅ID)
⋅(u_map
⋅(fst (snd p))))
oo foo_rep
, bar_abs oo
u_map
⋅(cfun_map
⋅(snd (snd p))
⋅ID) oo bar_rep
, baz_abs oo
u_map
⋅(cfun_map
⋅(convex_map
⋅(fst p))
⋅ID) oo baz_rep
))
"
lemma foo_bar_baz_takeF_beta:
"foo_bar_baz_takeF\p =
( foo_abs oo
ssum_map
⋅ID
⋅(sprod_map
⋅(u_map
⋅ID)
⋅(u_map
⋅(fst (snd p))))
oo foo_rep
, bar_abs oo
u_map
⋅(cfun_map
⋅(snd (snd p))
⋅ID) oo bar_rep
, baz_abs oo
u_map
⋅(cfun_map
⋅(convex_map
⋅(fst p))
⋅ID) oo baz_rep
)
"
unfolding foo_bar_baz_takeF_def
by (rule beta_cfun, simp)
definition
foo_take ::
"nat \ 'a foo \ 'a foo"
where
"foo_take = (\n. fst (iterate n\foo_bar_baz_takeF\\))"
definition
bar_take ::
"nat \ 'a bar \ 'a bar"
where
"bar_take = (\n. fst (snd (iterate n\foo_bar_baz_takeF\\)))"
definition
baz_take ::
"nat \ 'a baz \ 'a baz"
where
"baz_take = (\n. snd (snd (iterate n\foo_bar_baz_takeF\\)))"
lemma chain_take_thms:
"chain foo_take" "chain bar_take" "chain baz_take"
unfolding foo_take_def bar_take_def baz_take_def
by (intro ch2ch_fst ch2ch_snd chain_iterate)+
lemma take_0_thms:
"foo_take 0 = \" "bar_take 0 = \" "baz_take 0 = \"
unfolding foo_take_def bar_take_def baz_take_def
by (simp only: iterate_0 fst_strict snd_strict)+
lemma take_Suc_thms:
"foo_take (Suc n) =
foo_abs oo ssum_map
⋅ID
⋅(sprod_map
⋅(u_map
⋅ID)
⋅(u_map
⋅(bar_take n))) oo foo_rep
"
"bar_take (Suc n) =
bar_abs oo u_map
⋅(cfun_map
⋅(baz_take n)
⋅ID) oo bar_rep
"
"baz_take (Suc n) =
baz_abs oo u_map
⋅(cfun_map
⋅(convex_map
⋅(foo_take n))
⋅ID) oo baz_rep
"
unfolding foo_take_def bar_take_def baz_take_def
by (simp only: iterate_Suc foo_bar_baz_takeF_beta fst_conv snd_conv)+
lemma lub_take_lemma:
"(\n. foo_take n, \n. bar_take n, \n. baz_take n)
= (foo_map
⋅(ID::
'a \ 'a), bar_map
⋅(ID::
'a \ 'a), baz_map
⋅(ID::
'a \ 'a))
"
apply (simp only: lub_Pair [symmetric] ch2ch_Pair chain_take_thms)
apply (simp only: map_apply_thms prod.collapse)
apply (simp only: fix_def2)
apply (rule lub_eq)
apply (rule nat.induct)
apply (simp only: iterate_0 Pair_strict take_0_thms)
apply (simp only: iterate_Suc prod_eq_iff fst_conv snd_conv
foo_bar_baz_mapF_beta take_Suc_thms simp_thms)
done
lemma lub_foo_take:
"(\n. foo_take n) = ID"
apply (rule trans [OF _ foo_map_ID])
using lub_take_lemma
apply (elim Pair_inject)
apply assumption
done
lemma lub_bar_take:
"(\n. bar_take n) = ID"
apply (rule trans [OF _ bar_map_ID])
using lub_take_lemma
apply (elim Pair_inject)
apply assumption
done
lemma lub_baz_take:
"(\n. baz_take n) = ID"
apply (rule trans [OF _ baz_map_ID])
using lub_take_lemma
apply (elim Pair_inject)
apply assumption
done
end
