|
(* Title: HOL/HOLCF/ex/Powerdomain_ex.thy
Author: Brian Huffman
*)
section \<open>Powerdomain examples\<close>
theory Powerdomain_ex
imports HOLCF
begin
subsection \<open>Monadic sorting example\<close>
domain ordering = LT | EQ | GT
definition
compare :: "int lift \ int lift \ ordering" where
"compare = (FLIFT x y. if x < y then LT else if x = y then EQ else GT)"
definition
is_le :: "int lift \ int lift \ tr" where
"is_le = (\ x y. case compare\x\y of LT \ TT | EQ \ TT | GT \ FF)"
definition
is_less :: "int lift \ int lift \ tr" where
"is_less = (\ x y. case compare\x\y of LT \ TT | EQ \ FF | GT \ FF)"
definition
r1 :: "(int lift \ 'a) \ (int lift \ 'a) \ tr convex_pd" where
"r1 = (\ (x,_) (y,_). case compare\x\y of
LT \<Rightarrow> {TT}\<natural> |
EQ \<Rightarrow> {TT, FF}\<natural> |
GT \<Rightarrow> {FF}\<natural>)"
definition
r2 :: "(int lift \ 'a) \ (int lift \ 'a) \ tr convex_pd" where
"r2 = (\ (x,_) (y,_). {is_le\x\y, is_less\x\y}\)"
lemma r1_r2: "r1\(x,a)\(y,b) = (r2\(x,a)\(y,b) :: tr convex_pd)"
apply (simp add: r1_def r2_def)
apply (simp add: is_le_def is_less_def)
apply (cases "compare\x\y")
apply simp_all
done
subsection \<open>Picking a leaf from a tree\<close>
domain 'a tree =
Node (lazy "'a tree") (lazy "'a tree") |
Leaf (lazy "'a")
fixrec
mirror :: "'a tree \ 'a tree"
where
mirror_Leaf: "mirror\(Leaf\a) = Leaf\a"
| mirror_Node: "mirror\(Node\l\r) = Node\(mirror\r)\(mirror\l)"
lemma mirror_strict [simp]: "mirror\\ = \"
by fixrec_simp
fixrec
pick :: "'a tree \ 'a convex_pd"
where
pick_Leaf: "pick\(Leaf\a) = {a}\"
| pick_Node: "pick\(Node\l\r) = pick\l \\ pick\r"
lemma pick_strict [simp]: "pick\\ = \"
by fixrec_simp
lemma pick_mirror: "pick\(mirror\t) = pick\t"
by (induct t) (simp_all add: convex_plus_ac)
fixrec tree1 :: "int lift tree"
where "tree1 = Node\(Node\(Leaf\(Def 1))\(Leaf\(Def 2)))
\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 3))\<cdot>(Leaf\<cdot>(Def 4)))"
fixrec tree2 :: "int lift tree"
where "tree2 = Node\(Node\(Leaf\(Def 1))\(Leaf\(Def 2)))
\<cdot>(Node\<cdot>\<bottom>\<cdot>(Leaf\<cdot>(Def 4)))"
fixrec tree3 :: "int lift tree"
where "tree3 = Node\(Node\(Leaf\(Def 1))\tree3)
\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 3))\<cdot>(Leaf\<cdot>(Def 4)))"
declare tree1.simps tree2.simps tree3.simps [simp del]
lemma pick_tree1:
"pick\tree1 = {Def 1, Def 2, Def 3, Def 4}\"
apply (subst tree1.simps)
apply simp
apply (simp add: convex_plus_ac)
done
lemma pick_tree2:
"pick\tree2 = {Def 1, Def 2, \, Def 4}\"
apply (subst tree2.simps)
apply simp
apply (simp add: convex_plus_ac)
done
lemma pick_tree3:
"pick\tree3 = {Def 1, \, Def 3, Def 4}\"
apply (subst tree3.simps)
apply simp
apply (induct rule: tree3.induct)
apply simp
apply simp
apply (simp add: convex_plus_ac)
apply simp
apply (simp add: convex_plus_ac)
done
end
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
