src/HOL/HOLCF/ex/Powerdomain_ex.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 42151 4da4fc77664b
child 58880 0baae4311a9f
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 41399
diff changeset
     1
(*  Title:      HOL/HOLCF/ex/Powerdomain_ex.thy
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
     3
*)
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
     4
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
     5
header {* Powerdomain examples *}
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
     6
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
     7
theory Powerdomain_ex
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
     8
imports HOLCF
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
     9
begin
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    10
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    11
subsection {* Monadic sorting example *}
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    12
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    13
domain ordering = LT | EQ | GT
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    14
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    15
definition
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    16
  compare :: "int lift \<rightarrow> int lift \<rightarrow> ordering" where
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    17
  "compare = (FLIFT x y. if x < y then LT else if x = y then EQ else GT)"
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    18
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    19
definition
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    20
  is_le :: "int lift \<rightarrow> int lift \<rightarrow> tr" where
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    21
  "is_le = (\<Lambda> x y. case compare\<cdot>x\<cdot>y of LT \<Rightarrow> TT | EQ \<Rightarrow> TT | GT \<Rightarrow> FF)"
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    22
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    23
definition
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    24
  is_less :: "int lift \<rightarrow> int lift \<rightarrow> tr" where
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    25
  "is_less = (\<Lambda> x y. case compare\<cdot>x\<cdot>y of LT \<Rightarrow> TT | EQ \<Rightarrow> FF | GT \<Rightarrow> FF)"
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    26
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    27
definition
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    28
  r1 :: "(int lift \<times> 'a) \<rightarrow> (int lift \<times> 'a) \<rightarrow> tr convex_pd" where
35918
68397d86d454 use Pair instead of cpair
huffman
parents: 35917
diff changeset
    29
  "r1 = (\<Lambda> (x,_) (y,_). case compare\<cdot>x\<cdot>y of
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    30
          LT \<Rightarrow> {TT}\<natural> |
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    31
          EQ \<Rightarrow> {TT, FF}\<natural> |
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    32
          GT \<Rightarrow> {FF}\<natural>)"
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    33
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    34
definition
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    35
  r2 :: "(int lift \<times> 'a) \<rightarrow> (int lift \<times> 'a) \<rightarrow> tr convex_pd" where
35918
68397d86d454 use Pair instead of cpair
huffman
parents: 35917
diff changeset
    36
  "r2 = (\<Lambda> (x,_) (y,_). {is_le\<cdot>x\<cdot>y, is_less\<cdot>x\<cdot>y}\<natural>)"
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    37
35918
68397d86d454 use Pair instead of cpair
huffman
parents: 35917
diff changeset
    38
lemma r1_r2: "r1\<cdot>(x,a)\<cdot>(y,b) = (r2\<cdot>(x,a)\<cdot>(y,b) :: tr convex_pd)"
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    39
apply (simp add: r1_def r2_def)
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    40
apply (simp add: is_le_def is_less_def)
35781
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35769
diff changeset
    41
apply (cases "compare\<cdot>x\<cdot>y")
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    42
apply simp_all
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    43
done
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    44
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    45
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    46
subsection {* Picking a leaf from a tree *}
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    47
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    48
domain 'a tree =
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    49
  Node (lazy "'a tree") (lazy "'a tree") |
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    50
  Leaf (lazy "'a")
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    51
30158
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 29992
diff changeset
    52
fixrec
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    53
  mirror :: "'a tree \<rightarrow> 'a tree"
30158
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 29992
diff changeset
    54
where
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    55
  mirror_Leaf: "mirror\<cdot>(Leaf\<cdot>a) = Leaf\<cdot>a"
30158
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 29992
diff changeset
    56
| mirror_Node: "mirror\<cdot>(Node\<cdot>l\<cdot>r) = Node\<cdot>(mirror\<cdot>r)\<cdot>(mirror\<cdot>l)"
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    57
35917
85b0efdcdae9 use fixrec_simp instead of fixpat
huffman
parents: 35781
diff changeset
    58
lemma mirror_strict [simp]: "mirror\<cdot>\<bottom> = \<bottom>"
85b0efdcdae9 use fixrec_simp instead of fixpat
huffman
parents: 35781
diff changeset
    59
by fixrec_simp
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    60
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    61
fixrec
30158
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 29992
diff changeset
    62
  pick :: "'a tree \<rightarrow> 'a convex_pd"
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 29992
diff changeset
    63
where
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    64
  pick_Leaf: "pick\<cdot>(Leaf\<cdot>a) = {a}\<natural>"
41399
ad093e4638e2 changed syntax of powerdomain binary union operators
huffman
parents: 40774
diff changeset
    65
| pick_Node: "pick\<cdot>(Node\<cdot>l\<cdot>r) = pick\<cdot>l \<union>\<natural> pick\<cdot>r"
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    66
35917
85b0efdcdae9 use fixrec_simp instead of fixpat
huffman
parents: 35781
diff changeset
    67
lemma pick_strict [simp]: "pick\<cdot>\<bottom> = \<bottom>"
85b0efdcdae9 use fixrec_simp instead of fixpat
huffman
parents: 35781
diff changeset
    68
by fixrec_simp
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    69
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    70
lemma pick_mirror: "pick\<cdot>(mirror\<cdot>t) = pick\<cdot>t"
35781
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35769
diff changeset
    71
by (induct t) (simp_all add: convex_plus_ac)
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    72
30158
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 29992
diff changeset
    73
fixrec tree1 :: "int lift tree"
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 29992
diff changeset
    74
where "tree1 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>(Leaf\<cdot>(Def 2)))
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 29992
diff changeset
    75
                   \<cdot>(Node\<cdot>(Leaf\<cdot>(Def 3))\<cdot>(Leaf\<cdot>(Def 4)))"
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    76
30158
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 29992
diff changeset
    77
fixrec tree2 :: "int lift tree"
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 29992
diff changeset
    78
where "tree2 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>(Leaf\<cdot>(Def 2)))
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 29992
diff changeset
    79
                   \<cdot>(Node\<cdot>\<bottom>\<cdot>(Leaf\<cdot>(Def 4)))"
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    80
30158
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 29992
diff changeset
    81
fixrec tree3 :: "int lift tree"
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 29992
diff changeset
    82
where "tree3 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>tree3)
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 29992
diff changeset
    83
                   \<cdot>(Node\<cdot>(Leaf\<cdot>(Def 3))\<cdot>(Leaf\<cdot>(Def 4)))"
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    84
35769
500c32e5fadc fixrec now generates qualified theorem names
huffman
parents: 35169
diff changeset
    85
declare tree1.simps tree2.simps tree3.simps [simp del]
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    86
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    87
lemma pick_tree1:
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    88
  "pick\<cdot>tree1 = {Def 1, Def 2, Def 3, Def 4}\<natural>"
35769
500c32e5fadc fixrec now generates qualified theorem names
huffman
parents: 35169
diff changeset
    89
apply (subst tree1.simps)
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    90
apply simp
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    91
apply (simp add: convex_plus_ac)
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    92
done
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    93
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    94
lemma pick_tree2:
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    95
  "pick\<cdot>tree2 = {Def 1, Def 2, \<bottom>, Def 4}\<natural>"
35769
500c32e5fadc fixrec now generates qualified theorem names
huffman
parents: 35169
diff changeset
    96
apply (subst tree2.simps)
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    97
apply simp
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    98
apply (simp add: convex_plus_ac)
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
    99
done
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
   100
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
   101
lemma pick_tree3:
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
   102
  "pick\<cdot>tree3 = {Def 1, \<bottom>, Def 3, Def 4}\<natural>"
35769
500c32e5fadc fixrec now generates qualified theorem names
huffman
parents: 35169
diff changeset
   103
apply (subst tree3.simps)
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
   104
apply simp
35769
500c32e5fadc fixrec now generates qualified theorem names
huffman
parents: 35169
diff changeset
   105
apply (induct rule: tree3.induct)
29992
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
   106
apply simp
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
   107
apply simp
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
   108
apply (simp add: convex_plus_ac)
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
   109
apply simp
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
   110
apply (simp add: convex_plus_ac)
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
   111
done
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
   112
5deee36e33c4 add Powerdomain_ex.thy
huffman
parents:
diff changeset
   113
end