1.1 --- a/src/HOL/Library/While_Combinator.thy	Thu Oct 03 00:39:16 2013 +0200
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Thu Oct 03 12:34:32 2013 +0200
     1.3 @@ -80,72 +80,118 @@
     1.4    "\<lbrakk>\<forall>k' < k. f (c ((c^^k') s)) = c' (f ((c^^k') s))\<rbrakk> \<Longrightarrow> f ((c^^k) s) = (c'^^k) (f s)"
     1.5  by (induct k arbitrary: s) auto
     1.6  
     1.7 -lemma while_option_commute:
     1.8 -  assumes "\<And>s. b s = b' (f s)" "\<And>s. \<lbrakk>b s\<rbrakk> \<Longrightarrow> f (c s) = c' (f s)" 
     1.9 -  shows "Option.map f (while_option b c s) = while_option b' c' (f s)"
    1.10 +lemma while_option_commute_invariant:
    1.11 +assumes Invariant: "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> P (c s)"
    1.12 +assumes TestCommute: "\<And>s. P s \<Longrightarrow> b s = b' (f s)"
    1.13 +assumes BodyCommute: "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> f (c s) = c' (f s)"
    1.14 +assumes Initial: "P s"
    1.15 +shows "Option.map f (while_option b c s) = while_option b' c' (f s)"
    1.16  unfolding while_option_def
    1.17  proof (rule trans[OF if_distrib if_cong], safe, unfold option.inject)
    1.18 -  fix k assume "\<not> b ((c ^^ k) s)"
    1.19 -  thus "\<exists>k. \<not> b' ((c' ^^ k) (f s))"
    1.20 +  fix k
    1.21 +  assume "\<not> b ((c ^^ k) s)"
    1.22 +  with Initial show "\<exists>k. \<not> b' ((c' ^^ k) (f s))"
    1.23    proof (induction k arbitrary: s)
    1.24 -    case 0 thus ?case by (auto simp: assms(1) intro: exI[of _ 0])
    1.25 +    case 0 thus ?case by (auto simp: TestCommute intro: exI[of _ 0])
    1.26    next
    1.27 -    case (Suc k)
    1.28 -    hence "\<not> b ((c^^k) (c s))" by (auto simp: funpow_swap1)
    1.29 -    from Suc.IH[OF this] obtain k where "\<not> b' ((c' ^^ k) (f (c s)))" ..
    1.30 -    with assms show ?case
    1.31 -      by (cases "b s") (auto simp: funpow_swap1 intro: exI[of _ "Suc k"] exI[of _ "0"])
    1.32 +    case (Suc k) thus ?case
    1.33 +    proof (cases "b s")
    1.34 +      assume "b s"
    1.35 +      with Suc.IH[of "c s"] Suc.prems show ?thesis
    1.36 +        by (metis BodyCommute Invariant comp_apply funpow.simps(2) funpow_swap1)
    1.37 +    next
    1.38 +      assume "\<not> b s"
    1.39 +      with Suc show ?thesis by (auto simp: TestCommute intro: exI [of _ 0])
    1.40 +    qed
    1.41    qed
    1.42  next
    1.43 -  fix k assume "\<not> b' ((c' ^^ k) (f s))"
    1.44 -  thus "\<exists>k. \<not> b ((c ^^ k) s)"
    1.45 +  fix k
    1.46 +  assume "\<not> b' ((c' ^^ k) (f s))"
    1.47 +  with Initial show "\<exists>k. \<not> b ((c ^^ k) s)"
    1.48    proof (induction k arbitrary: s)
    1.49 -    case 0 thus ?case by (auto simp: assms(1) intro: exI[of _ 0])
    1.50 +    case 0 thus ?case by (auto simp: TestCommute intro: exI[of _ 0])
    1.51    next
    1.52 -    case (Suc k)
    1.53 -    hence *: "\<not> b' ((c'^^k) (c' (f s)))" by (auto simp: funpow_swap1)
    1.54 -    show ?case
    1.55 +    case (Suc k) thus ?case
    1.56      proof (cases "b s")
    1.57 -      case True
    1.58 -      with assms(2) * have "\<not> b' ((c'^^k) (f (c s)))" by simp
    1.59 -      from Suc.IH[OF this] obtain k where "\<not> b ((c ^^ k) (c s))" ..
    1.60 -      thus ?thesis by (auto simp: funpow_swap1 intro: exI[of _ "Suc k"])
    1.61 -    qed (auto intro: exI[of _ "0"])
    1.62 +       assume "b s"
    1.63 +      with Suc.IH[of "c s"] Suc.prems show ?thesis
    1.64 +        by (metis BodyCommute Invariant comp_apply funpow.simps(2) funpow_swap1)
    1.65 +    next
    1.66 +      assume "\<not> b s"
    1.67 +      with Suc show ?thesis by (auto simp: TestCommute intro: exI [of _ 0])
    1.68 +    qed
    1.69    qed
    1.70  next
    1.71 -  fix k assume k: "\<not> b' ((c' ^^ k) (f s))"
    1.72 -  have *: "(LEAST k. \<not> b' ((c' ^^ k) (f s))) = (LEAST k. \<not> b ((c ^^ k) s))" (is "?k' = ?k")
    1.73 +  fix k
    1.74 +  assume k: "\<not> b' ((c' ^^ k) (f s))"
    1.75 +  have *: "(LEAST k. \<not> b' ((c' ^^ k) (f s))) = (LEAST k. \<not> b ((c ^^ k) s))"
    1.76 +          (is "?k' = ?k")
    1.77    proof (cases ?k')
    1.78      case 0
    1.79 -    have "\<not> b' ((c'^^0) (f s))" unfolding 0[symmetric] by (rule LeastI[of _ k]) (rule k)
    1.80 -    hence "\<not> b s" unfolding assms(1) by simp
    1.81 +    have "\<not> b' ((c' ^^ 0) (f s))"
    1.82 +      unfolding 0[symmetric] by (rule LeastI[of _ k]) (rule k)
    1.83 +    hence "\<not> b s" by (auto simp: TestCommute Initial)
    1.84      hence "?k = 0" by (intro Least_equality) auto
    1.85      with 0 show ?thesis by auto
    1.86    next
    1.87      case (Suc k')
    1.88 -    have "\<not> b' ((c'^^Suc k') (f s))" unfolding Suc[symmetric] by (rule LeastI) (rule k)
    1.89 +    have "\<not> b' ((c' ^^ Suc k') (f s))"
    1.90 +      unfolding Suc[symmetric] by (rule LeastI) (rule k)
    1.91      moreover
    1.92      { fix k assume "k \<le> k'"
    1.93        hence "k < ?k'" unfolding Suc by simp
    1.94        hence "b' ((c' ^^ k) (f s))" by (rule iffD1[OF not_not, OF not_less_Least])
    1.95 -    } note b' = this
    1.96 +    }
    1.97 +    note b' = this
    1.98      { fix k assume "k \<le> k'"
    1.99 -      hence "f ((c ^^ k) s) = (c'^^k) (f s)" by (induct k) (auto simp: b' assms)
   1.100 -      with `k \<le> k'` have "b ((c^^k) s)"
   1.101 -      proof (induct k)
   1.102 -        case (Suc k) thus ?case unfolding assms(1) by (simp only: b')
   1.103 -      qed (simp add: b'[of 0, simplified] assms(1))
   1.104 -    } note b = this
   1.105 -    hence k': "f ((c^^k') s) = (c'^^k') (f s)" by (induct k') (auto simp: assms(2))
   1.106 +      hence "f ((c ^^ k) s) = (c' ^^ k) (f s)"
   1.107 +      and "b ((c ^^ k) s) = b' ((c' ^^ k) (f s))"
   1.108 +      and "P ((c ^^ k) s)"
   1.109 +        by (induct k) (auto simp: b' assms)
   1.110 +      with `k \<le> k'`
   1.111 +      have "b ((c ^^ k) s)"
   1.112 +      and "f ((c ^^ k) s) = (c' ^^ k) (f s)"
   1.113 +      and "P ((c ^^ k) s)"
   1.114 +        by (auto simp: b')
   1.115 +    }
   1.116 +    note b = this(1) and body = this(2) and inv = this(3)
   1.117 +    hence k': "f ((c ^^ k') s) = (c' ^^ k') (f s)" by auto
   1.118      ultimately show ?thesis unfolding Suc using b
   1.119 -    by (intro sym[OF Least_equality])
   1.120 -       (auto simp add: assms(1) assms(2)[OF b] k' not_less_eq_eq[symmetric])
   1.121 +    proof (intro Least_equality[symmetric])
   1.122 +      case goal1
   1.123 +      hence Test: "\<not> b' (f ((c ^^ Suc k') s))"
   1.124 +        by (auto simp: BodyCommute inv b)
   1.125 +      have "P ((c ^^ Suc k') s)" by (auto simp: Invariant inv b)
   1.126 +      with Test show ?case by (auto simp: TestCommute)
   1.127 +    next
   1.128 +      case goal2 thus ?case by (metis not_less_eq_eq)
   1.129 +    qed
   1.130    qed
   1.131    have "f ((c ^^ ?k) s) = (c' ^^ ?k') (f s)" unfolding *
   1.132 -    by (auto intro: funpow_commute assms(2) dest: not_less_Least)
   1.133 +  proof (rule funpow_commute, clarify)
   1.134 +    fix k assume "k < ?k"
   1.135 +    hence TestTrue: "b ((c ^^ k) s)" by (auto dest: not_less_Least)
   1.136 +    from `k < ?k` have "P ((c ^^ k) s)"
   1.137 +    proof (induct k)
   1.138 +      case 0 thus ?case by (auto simp: assms)
   1.139 +    next
   1.140 +      case (Suc h)
   1.141 +      hence "P ((c ^^ h) s)" by auto
   1.142 +      with Suc show ?case
   1.143 +        by (auto, metis (lifting, no_types) Invariant Suc_lessD not_less_Least)
   1.144 +    qed
   1.145 +    with TestTrue show "f (c ((c ^^ k) s)) = c' (f ((c ^^ k) s))"
   1.146 +      by (metis BodyCommute)
   1.147 +  qed
   1.148    thus "\<exists>z. (c ^^ ?k) s = z \<and> f z = (c' ^^ ?k') (f s)" by blast
   1.149  qed
   1.150  
   1.151 +lemma while_option_commute:
   1.152 +  assumes "\<And>s. b s = b' (f s)" "\<And>s. \<lbrakk>b s\<rbrakk> \<Longrightarrow> f (c s) = c' (f s)" 
   1.153 +  shows "Option.map f (while_option b c s) = while_option b' c' (f s)"
   1.154 +by(rule while_option_commute_invariant[where P = "\<lambda>_. True"])
   1.155 +  (auto simp add: assms)
   1.156 +
   1.157  subsection {* Total version *}
   1.158  
   1.159  definition while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
   1.160 @@ -199,11 +245,22 @@
   1.161    and "!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s)" and "P s"
   1.162    shows "EX t. while_option b c s = Some t"
   1.163  using assms(1,3)
   1.164 -apply (induct s)
   1.165 -using assms(2)
   1.166 -apply (subst while_option_unfold)
   1.167 -apply simp
   1.168 -done
   1.169 +proof (induction s)
   1.170 +  case less thus ?case using assms(2)
   1.171 +    by (subst while_option_unfold) simp
   1.172 +qed
   1.173 +
   1.174 +lemma wf_rel_while_option_Some:
   1.175 +assumes wf: "wf R"
   1.176 +assumes smaller: "\<And>s. P s \<and> b s \<Longrightarrow> (c s, s) \<in> R"
   1.177 +assumes inv: "\<And>s. P s \<and> b s \<Longrightarrow> P(c s)"
   1.178 +assumes init: "P s"
   1.179 +shows "\<exists>t. while_option b c s = Some t"
   1.180 +proof -
   1.181 + from smaller have "{(t,s). P s \<and> b s \<and> t = c s} \<subseteq> R" by auto
   1.182 + with wf have "wf {(t,s). P s \<and> b s \<and> t = c s}" by (auto simp: wf_subset)
   1.183 + with inv init show ?thesis by (auto simp: wf_while_option_Some)
   1.184 +qed
   1.185  
   1.186  theorem measure_while_option_Some: fixes f :: "'s \<Rightarrow> nat"
   1.187  shows "(!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s) \<and> f(c s) < f s)