src/HOL/HOLCF/Library/List_Cpo.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 55465 0d31c0546286
child 62175 8ffc4d0e652d
permissions -rw-r--r--
modernized header;
     1 (*  Title:      HOL/HOLCF/Library/List_Cpo.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 section {* 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: is_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 lub_eqI is_lub_Cons cpo_lubI A B)
   167 
   168 lemma cont2cont_case_list:
   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: is_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_case_list' [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_case_list 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_case_list_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: lub_APP ch2ch_monofun [OF mono])
   232     apply (simp add: monofun_cfun)
   233     done
   234 qed
   235 
   236 text {* Continuity rule for map *}
   237 
   238 lemma cont2cont_map [simp, cont2cont]:
   239   assumes f: "cont (\<lambda>(x, y). f x y)"
   240   assumes g: "cont (\<lambda>x. g x)"
   241   shows "cont (\<lambda>x. map (\<lambda>y. f x y) (g x))"
   242 using f
   243 apply (simp add: prod_cont_iff)
   244 apply (rule cont_apply [OF g])
   245 apply (rule list_contI, rule list.map, simp, simp, simp)
   246 apply (induct_tac y, simp, simp)
   247 done
   248 
   249 text {* There are probably lots of other list operations that also
   250 deserve to have continuity lemmas.  I'll add more as they are
   251 needed. *}
   252 
   253 subsection {* Lists are a discrete cpo *}
   254 
   255 instance list :: (discrete_cpo) discrete_cpo
   256 proof
   257   fix xs ys :: "'a list"
   258   show "xs \<sqsubseteq> ys \<longleftrightarrow> xs = ys"
   259     by (induct xs arbitrary: ys, case_tac [!] ys, simp_all)
   260 qed
   261 
   262 subsection {* Compactness and chain-finiteness *}
   263 
   264 lemma compact_Nil [simp]: "compact []"
   265 apply (rule compactI2)
   266 apply (erule list_chain_cases)
   267 apply simp
   268 apply (simp add: lub_Cons)
   269 done
   270 
   271 lemma compact_Cons: "\<lbrakk>compact x; compact xs\<rbrakk> \<Longrightarrow> compact (x # xs)"
   272 apply (rule compactI2)
   273 apply (erule list_chain_cases)
   274 apply (auto simp add: lub_Cons dest!: compactD2)
   275 apply (rename_tac i j, rule_tac x="max i j" in exI)
   276 apply (drule (1) below_trans [OF _ chain_mono [OF _ max.cobounded1]])
   277 apply (drule (1) below_trans [OF _ chain_mono [OF _ max.cobounded2]])
   278 apply (erule (1) conjI)
   279 done
   280 
   281 lemma compact_Cons_iff [simp]:
   282   "compact (x # xs) \<longleftrightarrow> compact x \<and> compact xs"
   283 apply (safe intro!: compact_Cons)
   284 apply (simp only: compact_def)
   285 apply (subgoal_tac "cont (\<lambda>x. x # xs)")
   286 apply (drule (1) adm_subst, simp, simp)
   287 apply (simp only: compact_def)
   288 apply (subgoal_tac "cont (\<lambda>xs. x # xs)")
   289 apply (drule (1) adm_subst, simp, simp)
   290 done
   291 
   292 instance list :: (chfin) chfin
   293 proof
   294   fix Y :: "nat \<Rightarrow> 'a list" assume "chain Y"
   295   moreover have "\<And>(xs::'a list). compact xs"
   296     by (induct_tac xs, simp_all)
   297   ultimately show "\<exists>i. max_in_chain i Y"
   298     by (rule compact_imp_max_in_chain)
   299 qed
   300 
   301 subsection {* Using lists with fixrec *}
   302 
   303 definition
   304   match_Nil :: "'a::cpo list \<rightarrow> 'b match \<rightarrow> 'b match"
   305 where
   306   "match_Nil = (\<Lambda> xs k. case xs of [] \<Rightarrow> k | y # ys \<Rightarrow> Fixrec.fail)"
   307 
   308 definition
   309   match_Cons :: "'a::cpo list \<rightarrow> ('a \<rightarrow> 'a list \<rightarrow> 'b match) \<rightarrow> 'b match"
   310 where
   311   "match_Cons = (\<Lambda> xs k. case xs of [] \<Rightarrow> Fixrec.fail | y # ys \<Rightarrow> k\<cdot>y\<cdot>ys)"
   312 
   313 lemma match_Nil_simps [simp]:
   314   "match_Nil\<cdot>[]\<cdot>k = k"
   315   "match_Nil\<cdot>(x # xs)\<cdot>k = Fixrec.fail"
   316 unfolding match_Nil_def by simp_all
   317 
   318 lemma match_Cons_simps [simp]:
   319   "match_Cons\<cdot>[]\<cdot>k = Fixrec.fail"
   320   "match_Cons\<cdot>(x # xs)\<cdot>k = k\<cdot>x\<cdot>xs"
   321 unfolding match_Cons_def by simp_all
   322 
   323 setup {*
   324   Fixrec.add_matchers
   325     [ (@{const_name Nil}, @{const_name match_Nil}),
   326       (@{const_name Cons}, @{const_name match_Cons}) ]
   327 *}
   328 
   329 end