added lemmas to List_Cpo.thy
authorhuffman
Fri Oct 01 07:40:57 2010 -0700 (2010-10-01)
changeset 3996620c74cf9c112
parent 39965 da88519e6a0b
child 39967 1c6dce3ef477
added lemmas to List_Cpo.thy
src/HOLCF/Library/List_Cpo.thy
     1.1 --- a/src/HOLCF/Library/List_Cpo.thy	Thu Sep 30 19:42:12 2010 -0700
     1.2 +++ b/src/HOLCF/Library/List_Cpo.thy	Fri Oct 01 07:40:57 2010 -0700
     1.3 @@ -50,6 +50,24 @@
     1.4  lemma below_Nil_iff [simp]: "xs \<sqsubseteq> [] \<longleftrightarrow> xs = []"
     1.5  by (cases xs, simp_all)
     1.6  
     1.7 +lemma list_below_induct [consumes 1, case_names Nil Cons]:
     1.8 +  assumes "xs \<sqsubseteq> ys"
     1.9 +  assumes 1: "P [] []"
    1.10 +  assumes 2: "\<And>x y xs ys. \<lbrakk>x \<sqsubseteq> y; xs \<sqsubseteq> ys; P xs ys\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys)"
    1.11 +  shows "P xs ys"
    1.12 +using `xs \<sqsubseteq> ys`
    1.13 +proof (induct xs arbitrary: ys)
    1.14 +  case Nil thus ?case by (simp add: 1)
    1.15 +next
    1.16 +  case (Cons x xs) thus ?case by (cases ys, simp_all add: 2)
    1.17 +qed
    1.18 +
    1.19 +lemma list_below_cases:
    1.20 +  assumes "xs \<sqsubseteq> ys"
    1.21 +  obtains "xs = []" and "ys = []" |
    1.22 +    x y xs' ys' where "xs = x # xs'" and "ys = y # ys'"
    1.23 +using assms by (cases xs, simp, cases ys, auto)
    1.24 +
    1.25  text "Thanks to Joachim Breitner"
    1.26  
    1.27  lemma list_Cons_below:
    1.28 @@ -77,25 +95,36 @@
    1.29  lemma below_same_length: "xs \<sqsubseteq> ys \<Longrightarrow> length xs = length ys"
    1.30  unfolding below_list_def by (rule list_all2_lengthD)
    1.31  
    1.32 +lemma list_chain_induct [consumes 1, case_names Nil Cons]:
    1.33 +  assumes "chain S"
    1.34 +  assumes 1: "P (\<lambda>i. [])"
    1.35 +  assumes 2: "\<And>A B. chain A \<Longrightarrow> chain B \<Longrightarrow> P B \<Longrightarrow> P (\<lambda>i. A i # B i)"
    1.36 +  shows "P S"
    1.37 +using `chain S`
    1.38 +proof (induct "S 0" arbitrary: S)
    1.39 +  case Nil
    1.40 +  have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF `chain S`])
    1.41 +  with Nil have "\<forall>i. S i = []" by simp
    1.42 +  thus ?case by (simp add: 1)
    1.43 +next
    1.44 +  case (Cons x xs)
    1.45 +  have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF `chain S`])
    1.46 +  hence *: "\<forall>i. S i \<noteq> []" by (rule all_forward, insert Cons) auto
    1.47 +  have "chain (\<lambda>i. hd (S i))" and "chain (\<lambda>i. tl (S i))"
    1.48 +    using `chain S` by simp_all
    1.49 +  moreover have "P (\<lambda>i. tl (S i))"
    1.50 +    using `chain S` and `x # xs = S 0` [symmetric]
    1.51 +    by (simp add: Cons(1))
    1.52 +  ultimately have "P (\<lambda>i. hd (S i) # tl (S i))"
    1.53 +    by (rule 2)
    1.54 +  thus "P S" by (simp add: *)
    1.55 +qed
    1.56 +
    1.57  lemma list_chain_cases:
    1.58    assumes S: "chain S"
    1.59 -  obtains "\<forall>i. S i = []" |
    1.60 -    A B where "chain A" and "chain B" and "\<forall>i. S i = A i # B i"
    1.61 -proof (cases "S 0")
    1.62 -  case Nil
    1.63 -  have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF S])
    1.64 -  with Nil have "\<forall>i. S i = []" by simp
    1.65 -  thus ?thesis ..
    1.66 -next
    1.67 -  case (Cons x xs)
    1.68 -  have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF S])
    1.69 -  hence *: "\<forall>i. S i \<noteq> []" by (rule all_forward) (auto simp add: Cons)
    1.70 -  let ?A = "\<lambda>i. hd (S i)"
    1.71 -  let ?B = "\<lambda>i. tl (S i)"
    1.72 -  from S have "chain ?A" and "chain ?B" by simp_all
    1.73 -  moreover have "\<forall>i. S i = ?A i # ?B i" by (simp add: *)
    1.74 -  ultimately show ?thesis ..
    1.75 -qed
    1.76 +  obtains "S = (\<lambda>i. [])" |
    1.77 +    A B where "chain A" and "chain B" and "S = (\<lambda>i. A i # B i)"
    1.78 +using S by (induct rule: list_chain_induct) simp_all
    1.79  
    1.80  subsection {* Lists are a complete partial order *}
    1.81  
    1.82 @@ -107,38 +136,15 @@
    1.83  unfolding is_lub_def is_ub_def Ball_def [symmetric]
    1.84  by (clarsimp, case_tac u, simp_all)
    1.85  
    1.86 -lemma list_cpo_lemma:
    1.87 -  fixes S :: "nat \<Rightarrow> 'a::cpo list"
    1.88 -  assumes "chain S" and "\<forall>i. length (S i) = n"
    1.89 -  shows "\<exists>x. range S <<| x"
    1.90 -using assms
    1.91 - apply (induct n arbitrary: S)
    1.92 -  apply (subgoal_tac "S = (\<lambda>i. [])")
    1.93 -  apply (fast intro: lub_const)
    1.94 -  apply (simp add: fun_eq_iff)
    1.95 - apply (drule_tac x="\<lambda>i. tl (S i)" in meta_spec, clarsimp)
    1.96 - apply (rule_tac x="(\<Squnion>i. hd (S i)) # x" in exI)
    1.97 - apply (subgoal_tac "range (\<lambda>i. hd (S i) # tl (S i)) = range S")
    1.98 -  apply (erule subst)
    1.99 -  apply (rule is_lub_Cons)
   1.100 -   apply (rule thelubE [OF _ refl])
   1.101 -   apply (erule ch2ch_hd)
   1.102 -  apply assumption
   1.103 - apply (rule_tac f="\<lambda>S. range S" in arg_cong)
   1.104 - apply (rule ext)
   1.105 - apply (rule hd_Cons_tl)
   1.106 - apply (drule_tac x=i in spec, auto)
   1.107 -done
   1.108 -
   1.109  instance list :: (cpo) cpo
   1.110  proof
   1.111    fix S :: "nat \<Rightarrow> 'a list"
   1.112 -  assume "chain S"
   1.113 -  hence "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono)
   1.114 -  hence "\<forall>i. length (S i) = length (S 0)"
   1.115 -    by (fast intro: below_same_length [symmetric])
   1.116 -  with `chain S` show "\<exists>x. range S <<| x"
   1.117 -    by (rule list_cpo_lemma)
   1.118 +  assume "chain S" thus "\<exists>x. range S <<| x"
   1.119 +  proof (induct rule: list_chain_induct)
   1.120 +    case Nil thus ?case by (auto intro: lub_const)
   1.121 +  next
   1.122 +    case (Cons A B) thus ?case by (auto intro: is_lub_Cons cpo_lubI)
   1.123 +  qed
   1.124  qed
   1.125  
   1.126  subsection {* Continuity of list operations *}
   1.127 @@ -196,6 +202,37 @@
   1.128    shows "cont (\<lambda>x. case l of [] \<Rightarrow> f1 x | y # ys \<Rightarrow> f2 x y ys)"
   1.129  using assms by (cases l) auto
   1.130  
   1.131 +text {* Lemma for proving continuity of recursive list functions: *}
   1.132 +
   1.133 +lemma list_contI:
   1.134 +  fixes f :: "'a::cpo list \<Rightarrow> 'b::cpo"
   1.135 +  assumes f: "\<And>x xs. f (x # xs) = g x xs (f xs)"
   1.136 +  assumes g1: "\<And>xs y. cont (\<lambda>x. g x xs y)"
   1.137 +  assumes g2: "\<And>x y. cont (\<lambda>xs. g x xs y)"
   1.138 +  assumes g3: "\<And>x xs. cont (\<lambda>y. g x xs y)"
   1.139 +  shows "cont f"
   1.140 +proof (rule contI2)
   1.141 +  obtain h where h: "\<And>x xs y. g x xs y = h\<cdot>x\<cdot>xs\<cdot>y"
   1.142 +  proof
   1.143 +    fix x xs y show "g x xs y = (\<Lambda> x xs y. g x xs y)\<cdot>x\<cdot>xs\<cdot>y"
   1.144 +    by (simp add: cont2cont_LAM g1 g2 g3)
   1.145 +  qed
   1.146 +  show mono: "monofun f"
   1.147 +    apply (rule monofunI)
   1.148 +    apply (erule list_below_induct)
   1.149 +    apply simp
   1.150 +    apply (simp add: f h monofun_cfun)
   1.151 +    done
   1.152 +  fix Y :: "nat \<Rightarrow> 'a list"
   1.153 +  assume "chain Y" thus "f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))"
   1.154 +    apply (induct rule: list_chain_induct)
   1.155 +    apply simp
   1.156 +    apply (simp add: lub_Cons f h)
   1.157 +    apply (simp add: contlub_cfun [symmetric] ch2ch_monofun [OF mono])
   1.158 +    apply (simp add: monofun_cfun)
   1.159 +    done
   1.160 +qed
   1.161 +
   1.162  text {* There are probably lots of other list operations that also
   1.163  deserve to have continuity lemmas.  I'll add more as they are
   1.164  needed. *}