src/HOLCF/Library/List_Cpo.thy
author huffman
Tue Oct 12 06:20:05 2010 -0700 (2010-10-12)
changeset 40006 116e94f9543b
parent 39968 d841744718fe
child 40771 1c6f7d4b110e
permissions -rw-r--r--
remove unneeded lemmas from Fun_Cpo.thy
     1 (*  Title:      HOLCF/Library/List_Cpo.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 header {* Lists as a complete partial order *}
     6 
     7 theory List_Cpo
     8 imports HOLCF
     9 begin
    10 
    11 subsection {* Lists are a partial order *}
    12 
    13 instantiation list :: (po) po
    14 begin
    15 
    16 definition
    17   "xs \<sqsubseteq> ys \<longleftrightarrow> list_all2 (op \<sqsubseteq>) xs ys"
    18 
    19 instance proof
    20   fix xs :: "'a list"
    21   from below_refl show "xs \<sqsubseteq> xs"
    22     unfolding below_list_def
    23     by (rule list_all2_refl)
    24 next
    25   fix xs ys zs :: "'a list"
    26   assume "xs \<sqsubseteq> ys" and "ys \<sqsubseteq> zs"
    27   with below_trans show "xs \<sqsubseteq> zs"
    28     unfolding below_list_def
    29     by (rule list_all2_trans)
    30 next
    31   fix xs ys zs :: "'a list"
    32   assume "xs \<sqsubseteq> ys" and "ys \<sqsubseteq> xs"
    33   with below_antisym show "xs = ys"
    34     unfolding below_list_def
    35     by (rule list_all2_antisym)
    36 qed
    37 
    38 end
    39 
    40 lemma below_list_simps [simp]:
    41   "[] \<sqsubseteq> []"
    42   "x # xs \<sqsubseteq> y # ys \<longleftrightarrow> x \<sqsubseteq> y \<and> xs \<sqsubseteq> ys"
    43   "\<not> [] \<sqsubseteq> y # ys"
    44   "\<not> x # xs \<sqsubseteq> []"
    45 by (simp_all add: below_list_def)
    46 
    47 lemma Nil_below_iff [simp]: "[] \<sqsubseteq> xs \<longleftrightarrow> xs = []"
    48 by (cases xs, simp_all)
    49 
    50 lemma below_Nil_iff [simp]: "xs \<sqsubseteq> [] \<longleftrightarrow> xs = []"
    51 by (cases xs, simp_all)
    52 
    53 lemma list_below_induct [consumes 1, case_names Nil Cons]:
    54   assumes "xs \<sqsubseteq> ys"
    55   assumes 1: "P [] []"
    56   assumes 2: "\<And>x y xs ys. \<lbrakk>x \<sqsubseteq> y; xs \<sqsubseteq> ys; P xs ys\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys)"
    57   shows "P xs ys"
    58 using `xs \<sqsubseteq> ys`
    59 proof (induct xs arbitrary: ys)
    60   case Nil thus ?case by (simp add: 1)
    61 next
    62   case (Cons x xs) thus ?case by (cases ys, simp_all add: 2)
    63 qed
    64 
    65 lemma list_below_cases:
    66   assumes "xs \<sqsubseteq> ys"
    67   obtains "xs = []" and "ys = []" |
    68     x y xs' ys' where "xs = x # xs'" and "ys = y # ys'"
    69 using assms by (cases xs, simp, cases ys, auto)
    70 
    71 text "Thanks to Joachim Breitner"
    72 
    73 lemma list_Cons_below:
    74   assumes "a # as \<sqsubseteq> xs"
    75   obtains b and bs where "a \<sqsubseteq> b" and "as \<sqsubseteq> bs" and "xs = b # bs"
    76   using assms by (cases xs, auto)
    77 
    78 lemma list_below_Cons:
    79   assumes "xs \<sqsubseteq> b # bs"
    80   obtains a and as where "a \<sqsubseteq> b" and "as \<sqsubseteq> bs" and "xs = a # as"
    81   using assms by (cases xs, auto)
    82 
    83 lemma hd_mono: "xs \<sqsubseteq> ys \<Longrightarrow> hd xs \<sqsubseteq> hd ys"
    84 by (cases xs, simp, cases ys, simp, simp)
    85 
    86 lemma tl_mono: "xs \<sqsubseteq> ys \<Longrightarrow> tl xs \<sqsubseteq> tl ys"
    87 by (cases xs, simp, cases ys, simp, simp)
    88 
    89 lemma ch2ch_hd [simp]: "chain (\<lambda>i. S i) \<Longrightarrow> chain (\<lambda>i. hd (S i))"
    90 by (rule chainI, rule hd_mono, erule chainE)
    91 
    92 lemma ch2ch_tl [simp]: "chain (\<lambda>i. S i) \<Longrightarrow> chain (\<lambda>i. tl (S i))"
    93 by (rule chainI, rule tl_mono, erule chainE)
    94 
    95 lemma below_same_length: "xs \<sqsubseteq> ys \<Longrightarrow> length xs = length ys"
    96 unfolding below_list_def by (rule list_all2_lengthD)
    97 
    98 lemma list_chain_induct [consumes 1, case_names Nil Cons]:
    99   assumes "chain S"
   100   assumes 1: "P (\<lambda>i. [])"
   101   assumes 2: "\<And>A B. chain A \<Longrightarrow> chain B \<Longrightarrow> P B \<Longrightarrow> P (\<lambda>i. A i # B i)"
   102   shows "P S"
   103 using `chain S`
   104 proof (induct "S 0" arbitrary: S)
   105   case Nil
   106   have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF `chain S`])
   107   with Nil have "\<forall>i. S i = []" by simp
   108   thus ?case by (simp add: 1)
   109 next
   110   case (Cons x xs)
   111   have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF `chain S`])
   112   hence *: "\<forall>i. S i \<noteq> []" by (rule all_forward, insert Cons) auto
   113   have "chain (\<lambda>i. hd (S i))" and "chain (\<lambda>i. tl (S i))"
   114     using `chain S` by simp_all
   115   moreover have "P (\<lambda>i. tl (S i))"
   116     using `chain S` and `x # xs = S 0` [symmetric]
   117     by (simp add: Cons(1))
   118   ultimately have "P (\<lambda>i. hd (S i) # tl (S i))"
   119     by (rule 2)
   120   thus "P S" by (simp add: *)
   121 qed
   122 
   123 lemma list_chain_cases:
   124   assumes S: "chain S"
   125   obtains "S = (\<lambda>i. [])" |
   126     A B where "chain A" and "chain B" and "S = (\<lambda>i. A i # B i)"
   127 using S by (induct rule: list_chain_induct) simp_all
   128 
   129 subsection {* Lists are a complete partial order *}
   130 
   131 lemma is_lub_Cons:
   132   assumes A: "range A <<| x"
   133   assumes B: "range B <<| xs"
   134   shows "range (\<lambda>i. A i # B i) <<| x # xs"
   135 using assms
   136 unfolding is_lub_def is_ub_def
   137 by (clarsimp, case_tac u, simp_all)
   138 
   139 instance list :: (cpo) cpo
   140 proof
   141   fix S :: "nat \<Rightarrow> 'a list"
   142   assume "chain S" thus "\<exists>x. range S <<| x"
   143   proof (induct rule: list_chain_induct)
   144     case Nil thus ?case by (auto intro: lub_const)
   145   next
   146     case (Cons A B) thus ?case by (auto intro: is_lub_Cons cpo_lubI)
   147   qed
   148 qed
   149 
   150 subsection {* Continuity of list operations *}
   151 
   152 lemma cont2cont_Cons [simp, cont2cont]:
   153   assumes f: "cont (\<lambda>x. f x)"
   154   assumes g: "cont (\<lambda>x. g x)"
   155   shows "cont (\<lambda>x. f x # g x)"
   156 apply (rule contI)
   157 apply (rule is_lub_Cons)
   158 apply (erule contE [OF f])
   159 apply (erule contE [OF g])
   160 done
   161 
   162 lemma lub_Cons:
   163   fixes A :: "nat \<Rightarrow> 'a::cpo"
   164   assumes A: "chain A" and B: "chain B"
   165   shows "(\<Squnion>i. A i # B i) = (\<Squnion>i. A i) # (\<Squnion>i. B i)"
   166 by (intro thelubI is_lub_Cons cpo_lubI A B)
   167 
   168 lemma cont2cont_list_case:
   169   assumes f: "cont (\<lambda>x. f x)"
   170   assumes g: "cont (\<lambda>x. g x)"
   171   assumes h1: "\<And>y ys. cont (\<lambda>x. h x y ys)"
   172   assumes h2: "\<And>x ys. cont (\<lambda>y. h x y ys)"
   173   assumes h3: "\<And>x y. cont (\<lambda>ys. h x y ys)"
   174   shows "cont (\<lambda>x. case f x of [] \<Rightarrow> g x | y # ys \<Rightarrow> h x y ys)"
   175 apply (rule cont_apply [OF f])
   176 apply (rule contI)
   177 apply (erule list_chain_cases)
   178 apply (simp add: lub_const)
   179 apply (simp add: lub_Cons)
   180 apply (simp add: cont2contlubE [OF h2])
   181 apply (simp add: cont2contlubE [OF h3])
   182 apply (simp add: diag_lub ch2ch_cont [OF h2] ch2ch_cont [OF h3])
   183 apply (rule cpo_lubI, rule chainI, rule below_trans)
   184 apply (erule cont2monofunE [OF h2 chainE])
   185 apply (erule cont2monofunE [OF h3 chainE])
   186 apply (case_tac y, simp_all add: g h1)
   187 done
   188 
   189 lemma cont2cont_list_case' [simp, cont2cont]:
   190   assumes f: "cont (\<lambda>x. f x)"
   191   assumes g: "cont (\<lambda>x. g x)"
   192   assumes h: "cont (\<lambda>p. h (fst p) (fst (snd p)) (snd (snd p)))"
   193   shows "cont (\<lambda>x. case f x of [] \<Rightarrow> g x | y # ys \<Rightarrow> h x y ys)"
   194 using assms by (simp add: cont2cont_list_case prod_cont_iff)
   195 
   196 text {* The simple version (due to Joachim Breitner) is needed if the
   197   element type of the list is not a cpo. *}
   198 
   199 lemma cont2cont_list_case_simple [simp, cont2cont]:
   200   assumes "cont (\<lambda>x. f1 x)"
   201   assumes "\<And>y ys. cont (\<lambda>x. f2 x y ys)"
   202   shows "cont (\<lambda>x. case l of [] \<Rightarrow> f1 x | y # ys \<Rightarrow> f2 x y ys)"
   203 using assms by (cases l) auto
   204 
   205 text {* Lemma for proving continuity of recursive list functions: *}
   206 
   207 lemma list_contI:
   208   fixes f :: "'a::cpo list \<Rightarrow> 'b::cpo"
   209   assumes f: "\<And>x xs. f (x # xs) = g x xs (f xs)"
   210   assumes g1: "\<And>xs y. cont (\<lambda>x. g x xs y)"
   211   assumes g2: "\<And>x y. cont (\<lambda>xs. g x xs y)"
   212   assumes g3: "\<And>x xs. cont (\<lambda>y. g x xs y)"
   213   shows "cont f"
   214 proof (rule contI2)
   215   obtain h where h: "\<And>x xs y. g x xs y = h\<cdot>x\<cdot>xs\<cdot>y"
   216   proof
   217     fix x xs y show "g x xs y = (\<Lambda> x xs y. g x xs y)\<cdot>x\<cdot>xs\<cdot>y"
   218     by (simp add: cont2cont_LAM g1 g2 g3)
   219   qed
   220   show mono: "monofun f"
   221     apply (rule monofunI)
   222     apply (erule list_below_induct)
   223     apply simp
   224     apply (simp add: f h monofun_cfun)
   225     done
   226   fix Y :: "nat \<Rightarrow> 'a list"
   227   assume "chain Y" thus "f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))"
   228     apply (induct rule: list_chain_induct)
   229     apply simp
   230     apply (simp add: lub_Cons f h)
   231     apply (simp add: contlub_cfun [symmetric] ch2ch_monofun [OF mono])
   232     apply (simp add: monofun_cfun)
   233     done
   234 qed
   235 
   236 text {* There are probably lots of other list operations that also
   237 deserve to have continuity lemmas.  I'll add more as they are
   238 needed. *}
   239 
   240 subsection {* Using lists with fixrec *}
   241 
   242 definition
   243   match_Nil :: "'a::cpo list \<rightarrow> 'b match \<rightarrow> 'b match"
   244 where
   245   "match_Nil = (\<Lambda> xs k. case xs of [] \<Rightarrow> k | y # ys \<Rightarrow> Fixrec.fail)"
   246 
   247 definition
   248   match_Cons :: "'a::cpo list \<rightarrow> ('a \<rightarrow> 'a list \<rightarrow> 'b match) \<rightarrow> 'b match"
   249 where
   250   "match_Cons = (\<Lambda> xs k. case xs of [] \<Rightarrow> Fixrec.fail | y # ys \<Rightarrow> k\<cdot>y\<cdot>ys)"
   251 
   252 lemma match_Nil_simps [simp]:
   253   "match_Nil\<cdot>[]\<cdot>k = k"
   254   "match_Nil\<cdot>(x # xs)\<cdot>k = Fixrec.fail"
   255 unfolding match_Nil_def by simp_all
   256 
   257 lemma match_Cons_simps [simp]:
   258   "match_Cons\<cdot>[]\<cdot>k = Fixrec.fail"
   259   "match_Cons\<cdot>(x # xs)\<cdot>k = k\<cdot>x\<cdot>xs"
   260 unfolding match_Cons_def by simp_all
   261 
   262 setup {*
   263   Fixrec.add_matchers
   264     [ (@{const_name Nil}, @{const_name match_Nil}),
   265       (@{const_name Cons}, @{const_name match_Cons}) ]
   266 *}
   267 
   268 end