src/HOL/HOLCF/Library/Option_Cpo.thy
author huffman
Thu, 06 Jan 2011 16:52:35 -0800
changeset 41436 480978f80eae
parent 41393 17bf4ddd0833
child 42151 4da4fc77664b
permissions -rw-r--r--
rename constant pdefl to liftdefl_of
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     1
(*  Title:      HOLCF/Option_Cpo.thy
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     3
*)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     4
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     5
header {* Cpo class instance for HOL option type *}
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     6
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     7
theory Option_Cpo
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
     8
imports HOLCF Sum_Cpo
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     9
begin
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    10
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    11
subsection {* Ordering on option type *}
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    12
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    13
instantiation option :: (below) below
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    14
begin
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    15
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    16
definition below_option_def:
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    17
  "x \<sqsubseteq> y \<equiv> case x of
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    18
         None \<Rightarrow> (case y of None \<Rightarrow> True | Some b \<Rightarrow> False) |
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    19
         Some a \<Rightarrow> (case y of None \<Rightarrow> False | Some b \<Rightarrow> a \<sqsubseteq> b)"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    20
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    21
instance ..
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    22
end
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    23
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    24
lemma None_below_None [simp]: "None \<sqsubseteq> None"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    25
unfolding below_option_def by simp
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    26
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    27
lemma Some_below_Some [simp]: "Some x \<sqsubseteq> Some y \<longleftrightarrow> x \<sqsubseteq> y"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    28
unfolding below_option_def by simp
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    29
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    30
lemma Some_below_None [simp]: "\<not> Some x \<sqsubseteq> None"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    31
unfolding below_option_def by simp
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    32
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    33
lemma None_below_Some [simp]: "\<not> None \<sqsubseteq> Some y"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    34
unfolding below_option_def by simp
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    35
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    36
lemma Some_mono: "x \<sqsubseteq> y \<Longrightarrow> Some x \<sqsubseteq> Some y"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    37
by simp
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    38
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    39
lemma None_below_iff [simp]: "None \<sqsubseteq> x \<longleftrightarrow> x = None"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    40
by (cases x, simp_all)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    41
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    42
lemma below_None_iff [simp]: "x \<sqsubseteq> None \<longleftrightarrow> x = None"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    43
by (cases x, simp_all)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    44
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    45
lemma option_below_cases:
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    46
  assumes "x \<sqsubseteq> y"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    47
  obtains "x = None" and "y = None"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    48
  | a b where "x = Some a" and "y = Some b" and "a \<sqsubseteq> b"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    49
using assms unfolding below_option_def
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    50
by (simp split: option.split_asm)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    51
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    52
subsection {* Option type is a complete partial order *}
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    53
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    54
instance option :: (po) po
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    55
proof
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    56
  fix x :: "'a option"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    57
  show "x \<sqsubseteq> x"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    58
    unfolding below_option_def
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    59
    by (simp split: option.split)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    60
next
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    61
  fix x y :: "'a option"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    62
  assume "x \<sqsubseteq> y" and "y \<sqsubseteq> x" thus "x = y"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    63
    unfolding below_option_def
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    64
    by (auto split: option.split_asm intro: below_antisym)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    65
next
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    66
  fix x y z :: "'a option"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    67
  assume "x \<sqsubseteq> y" and "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    68
    unfolding below_option_def
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    69
    by (auto split: option.split_asm intro: below_trans)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    70
qed
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    71
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    72
lemma monofun_the: "monofun the"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    73
by (rule monofunI, erule option_below_cases, simp_all)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    74
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    75
lemma option_chain_cases:
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    76
  assumes Y: "chain Y"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    77
  obtains "Y = (\<lambda>i. None)" | A where "chain A" and "Y = (\<lambda>i. Some (A i))"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    78
 apply (cases "Y 0")
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    79
  apply (rule that(1))
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    80
  apply (rule ext)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    81
  apply (cut_tac j=i in chain_mono [OF Y le0], simp)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    82
 apply (rule that(2))
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    83
  apply (rule ch2ch_monofun [OF monofun_the Y])
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    84
 apply (rule ext)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    85
 apply (cut_tac j=i in chain_mono [OF Y le0], simp)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    86
 apply (case_tac "Y i", simp_all)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    87
done
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    88
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    89
lemma is_lub_Some: "range S <<| x \<Longrightarrow> range (\<lambda>i. Some (S i)) <<| Some x"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    90
 apply (rule is_lubI)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    91
  apply (rule ub_rangeI)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    92
  apply (simp add: is_lub_rangeD1)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    93
 apply (frule ub_rangeD [where i=arbitrary])
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    94
 apply (case_tac u, simp_all)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    95
 apply (erule is_lubD2)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    96
 apply (rule ub_rangeI)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    97
 apply (drule ub_rangeD, simp)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    98
done
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    99
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   100
instance option :: (cpo) cpo
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   101
 apply intro_classes
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   102
 apply (erule option_chain_cases, safe)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   103
  apply (rule exI, rule is_lub_const)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   104
 apply (rule exI)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   105
 apply (rule is_lub_Some)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   106
 apply (erule cpo_lubI)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   107
done
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   108
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   109
subsection {* Continuity of Some and case function *}
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   110
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   111
lemma cont_Some: "cont Some"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   112
by (intro contI is_lub_Some cpo_lubI)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   113
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   114
lemmas cont2cont_Some [simp, cont2cont] = cont_compose [OF cont_Some]
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   115
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   116
lemmas ch2ch_Some [simp] = ch2ch_cont [OF cont_Some]
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   117
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   118
lemmas lub_Some = cont2contlubE [OF cont_Some, symmetric]
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   119
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   120
lemma cont2cont_option_case:
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   121
  assumes f: "cont (\<lambda>x. f x)"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   122
  assumes g: "cont (\<lambda>x. g x)"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   123
  assumes h1: "\<And>a. cont (\<lambda>x. h x a)"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   124
  assumes h2: "\<And>x. cont (\<lambda>a. h x a)"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   125
  shows "cont (\<lambda>x. case f x of None \<Rightarrow> g x | Some a \<Rightarrow> h x a)"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   126
apply (rule cont_apply [OF f])
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   127
apply (rule contI)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   128
apply (erule option_chain_cases)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   129
apply (simp add: is_lub_const)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   130
apply (simp add: lub_Some)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   131
apply (simp add: cont2contlubE [OF h2])
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   132
apply (rule cpo_lubI, rule chainI)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   133
apply (erule cont2monofunE [OF h2 chainE])
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   134
apply (case_tac y, simp_all add: g h1)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   135
done
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   136
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   137
lemma cont2cont_option_case' [simp, cont2cont]:
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   138
  assumes f: "cont (\<lambda>x. f x)"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   139
  assumes g: "cont (\<lambda>x. g x)"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   140
  assumes h: "cont (\<lambda>p. h (fst p) (snd p))"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   141
  shows "cont (\<lambda>x. case f x of None \<Rightarrow> g x | Some a \<Rightarrow> h x a)"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   142
using assms by (simp add: cont2cont_option_case prod_cont_iff)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   143
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   144
text {* Simple version for when the element type is not a cpo. *}
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   145
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   146
lemma cont2cont_option_case_simple [simp, cont2cont]:
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   147
  assumes "cont (\<lambda>x. f x)"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   148
  assumes "\<And>a. cont (\<lambda>x. g x a)"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   149
  shows "cont (\<lambda>x. case z of None \<Rightarrow> f x | Some a \<Rightarrow> g x a)"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   150
using assms by (cases z) auto
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   151
41325
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   152
text {* Continuity rule for map. *}
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   153
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   154
lemma cont2cont_option_map [simp, cont2cont]:
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   155
  assumes f: "cont (\<lambda>(x, y). f x y)"
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   156
  assumes g: "cont (\<lambda>x. g x)"
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   157
  shows "cont (\<lambda>x. Option.map (\<lambda>y. f x y) (g x))"
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   158
using assms by (simp add: prod_cont_iff Option.map_def)
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   159
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   160
subsection {* Compactness and chain-finiteness *}
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   161
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   162
lemma compact_None [simp]: "compact None"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   163
apply (rule compactI2)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   164
apply (erule option_chain_cases, safe)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   165
apply simp
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   166
apply (simp add: lub_Some)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   167
done
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   168
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   169
lemma compact_Some: "compact a \<Longrightarrow> compact (Some a)"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   170
apply (rule compactI2)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   171
apply (erule option_chain_cases, safe)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   172
apply simp
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   173
apply (simp add: lub_Some)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   174
apply (erule (2) compactD2)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   175
done
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   176
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   177
lemma compact_Some_rev: "compact (Some a) \<Longrightarrow> compact a"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   178
unfolding compact_def
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   179
by (drule adm_subst [OF cont_Some], simp)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   180
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   181
lemma compact_Some_iff [simp]: "compact (Some a) = compact a"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   182
by (safe elim!: compact_Some compact_Some_rev)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   183
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   184
instance option :: (chfin) chfin
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   185
apply intro_classes
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   186
apply (erule compact_imp_max_in_chain)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   187
apply (case_tac "\<Squnion>i. Y i", simp_all)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   188
done
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   189
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   190
instance option :: (discrete_cpo) discrete_cpo
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   191
by intro_classes (simp add: below_option_def split: option.split)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   192
41325
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   193
subsection {* Using option types with Fixrec *}
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   194
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   195
definition
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   196
  "match_None = (\<Lambda> x k. case x of None \<Rightarrow> k | Some a \<Rightarrow> Fixrec.fail)"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   197
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   198
definition
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   199
  "match_Some = (\<Lambda> x k. case x of None \<Rightarrow> Fixrec.fail | Some a \<Rightarrow> k\<cdot>a)"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   200
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   201
lemma match_None_simps [simp]:
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   202
  "match_None\<cdot>None\<cdot>k = k"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   203
  "match_None\<cdot>(Some a)\<cdot>k = Fixrec.fail"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   204
unfolding match_None_def by simp_all
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   205
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   206
lemma match_Some_simps [simp]:
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   207
  "match_Some\<cdot>None\<cdot>k = Fixrec.fail"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   208
  "match_Some\<cdot>(Some a)\<cdot>k = k\<cdot>a"
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   209
unfolding match_Some_def by simp_all
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   210
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   211
setup {*
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   212
  Fixrec.add_matchers
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   213
    [ (@{const_name None}, @{const_name match_None}),
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   214
      (@{const_name Some}, @{const_name match_Some}) ]
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   215
*}
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   216
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   217
subsection {* Option type is a predomain *}
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   218
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   219
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
   220
  "encode_option = (\<Lambda> x. case x of None \<Rightarrow> Inl () | Some a \<Rightarrow> Inr a)"
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   221
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   222
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
   223
  "decode_option = (\<Lambda> x. case x of Inl (u::unit) \<Rightarrow> None | Inr a \<Rightarrow> Some a)"
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   224
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
   225
lemma decode_encode_option [simp]: "decode_option\<cdot>(encode_option\<cdot>x) = x"
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
   226
unfolding decode_option_def encode_option_def
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
   227
by (cases x, simp_all)
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
   228
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
   229
lemma encode_decode_option [simp]: "encode_option\<cdot>(decode_option\<cdot>x) = x"
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
   230
unfolding decode_option_def encode_option_def
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
   231
by (cases x, simp_all)
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   232
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   233
instantiation option :: (predomain) predomain
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   234
begin
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   235
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   236
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
   237
  "liftemb = liftemb oo u_map\<cdot>encode_option"
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   238
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   239
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
   240
  "liftprj = u_map\<cdot>decode_option oo liftprj"
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   241
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   242
definition
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
   243
  "liftdefl (t::('a option) itself) = LIFTDEFL(unit + 'a)"
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   244
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   245
instance proof
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
   246
  show "ep_pair liftemb (liftprj :: udom u \<rightarrow> ('a option) u)"
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   247
    unfolding liftemb_option_def liftprj_option_def
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
   248
    apply (intro ep_pair_comp ep_pair_u_map predomain_ep)
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   249
    apply (rule ep_pair.intro, simp, simp)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   250
    done
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
   251
  show "cast\<cdot>LIFTDEFL('a option) = liftemb oo (liftprj :: udom u \<rightarrow> ('a option) u)"
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   252
    unfolding liftemb_option_def liftprj_option_def liftdefl_option_def
41292
2b7bc8d9fd6e use deflations over type 'udom u' to represent predomains;
huffman
parents: 41112
diff changeset
   253
    by (simp add: cast_liftdefl cfcomp1 u_map_map ID_def [symmetric] u_map_ID)
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   254
qed
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   255
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   256
end
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   257
41325
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   258
subsection {* Configuring domain package to work with option type *}
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   259
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   260
lemma liftdefl_option [domain_defl_simps]:
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   261
  "LIFTDEFL('a::predomain option) = LIFTDEFL(unit + 'a)"
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   262
by (rule liftdefl_option_def)
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   263
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   264
abbreviation option_map
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   265
  where "option_map f \<equiv> Abs_cfun (Option.map (Rep_cfun f))"
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   266
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   267
lemma option_map_ID [domain_map_ID]: "option_map ID = ID"
41393
17bf4ddd0833 fix another proof script broken by a35af5180c01
huffman
parents: 41325
diff changeset
   268
by (simp add: ID_def cfun_eq_iff Option.map.identity id_def)
41325
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   269
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   270
lemma deflation_option_map [domain_deflation]:
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   271
  "deflation d \<Longrightarrow> deflation (option_map d)"
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   272
apply default
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   273
apply (induct_tac x, simp_all add: deflation.idem)
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   274
apply (induct_tac x, simp_all add: deflation.below)
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   275
done
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   276
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   277
lemma encode_option_option_map:
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   278
  "encode_option\<cdot>(Option.map (\<lambda>x. f\<cdot>x) (decode_option\<cdot>x)) = sum_map' ID f\<cdot>x"
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   279
by (induct x, simp_all add: decode_option_def encode_option_def)
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   280
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   281
lemma isodefl_option [domain_isodefl]:
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   282
  assumes "isodefl' d t"
41436
480978f80eae rename constant pdefl to liftdefl_of
huffman
parents: 41393
diff changeset
   283
  shows "isodefl' (option_map d) (sum_liftdefl\<cdot>(liftdefl_of\<cdot>DEFL(unit))\<cdot>t)"
41325
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   284
using isodefl_sum [OF isodefl_LIFTDEFL [where 'a=unit] assms]
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   285
unfolding isodefl'_def liftemb_option_def liftprj_option_def liftdefl_eq
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   286
by (simp add: cfcomp1 u_map_map encode_option_option_map)
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   287
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   288
setup {*
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   289
  Domain_Take_Proofs.add_rec_type (@{type_name "option"}, [true])
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   290
*}
b27e5c9f5c10 configure domain package to work with HOL option type
huffman
parents: 41292
diff changeset
   291
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
   292
end