author traytel Mon Dec 17 15:17:32 2012 +0100 (2012-12-17) changeset 50577 cfbad2d08412 parent 50573 765c22baa1c9 child 50579 8ccffe44d193
useful commutative diagram for while_option
```     1.1 --- a/src/HOL/Library/While_Combinator.thy	Mon Dec 17 08:19:35 2012 +0100
1.2 +++ b/src/HOL/Library/While_Combinator.thy	Mon Dec 17 15:17:32 2012 +0100
1.3 @@ -77,6 +77,74 @@
1.4    thus "P t" by (auto simp: t)
1.5  qed
1.6
1.7 +lemma funpow_commute:
1.8 +  "\<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.9 +by (induct k arbitrary: s) auto
1.10 +
1.11 +lemma while_option_commute:
1.12 +  assumes "\<And>s. b s = b' (f s)" "\<And>s. \<lbrakk>b s\<rbrakk> \<Longrightarrow> f (c s) = c' (f s)"
1.13 +  shows "Option.map f (while_option b c s) = while_option b' c' (f s)"
1.14 +unfolding while_option_def
1.15 +proof (rule trans[OF if_distrib if_cong], safe, unfold option.inject)
1.16 +  fix k assume "\<not> b ((c ^^ k) s)"
1.17 +  thus "\<exists>k. \<not> b' ((c' ^^ k) (f s))"
1.18 +  proof (induction k arbitrary: s)
1.19 +    case 0 thus ?case by (auto simp: assms(1) intro: exI[of _ 0])
1.20 +  next
1.21 +    case (Suc k)
1.22 +    hence "\<not> b ((c^^k) (c s))" by (auto simp: funpow_swap1)
1.23 +    then guess k by (rule exE[OF Suc.IH[of "c s"]])
1.24 +    with assms show ?case by (cases "b s") (auto simp: funpow_swap1 intro: exI[of _ "Suc k"] exI[of _ "0"])
1.25 +  qed
1.26 +next
1.27 +  fix k assume "\<not> b' ((c' ^^ k) (f s))"
1.28 +  thus "\<exists>k. \<not> b ((c ^^ k) s)"
1.29 +  proof (induction k arbitrary: s)
1.30 +    case 0 thus ?case by (auto simp: assms(1) intro: exI[of _ 0])
1.31 +  next
1.32 +    case (Suc k)
1.33 +    hence *: "\<not> b' ((c'^^k) (c' (f s)))" by (auto simp: funpow_swap1)
1.34 +    show ?case
1.35 +    proof (cases "b s")
1.36 +      case True
1.37 +      with assms(2) * have "\<not> b' ((c'^^k) (f (c s)))" by simp
1.38 +      then guess k by (rule exE[OF Suc.IH[of "c s"]])
1.39 +      thus ?thesis by (auto simp: funpow_swap1 intro: exI[of _ "Suc k"])
1.40 +    qed (auto intro: exI[of _ "0"])
1.41 +  qed
1.42 +next
1.43 +  fix k assume k: "\<not> b' ((c' ^^ k) (f s))"
1.44 +  have *: "(LEAST k. \<not> b' ((c' ^^ k) (f s))) = (LEAST k. \<not> b ((c ^^ k) s))" (is "?k' = ?k")
1.45 +  proof (cases ?k')
1.46 +    case 0
1.47 +    have "\<not> b' ((c'^^0) (f s))" unfolding 0[symmetric] by (rule LeastI[of _ k]) (rule k)
1.48 +    hence "\<not> b s" unfolding assms(1) by simp
1.49 +    hence "?k = 0" by (intro Least_equality) auto
1.50 +    with 0 show ?thesis by auto
1.51 +  next
1.52 +    case (Suc k')
1.53 +    have "\<not> b' ((c'^^Suc k') (f s))" unfolding Suc[symmetric] by (rule LeastI) (rule k)
1.54 +    moreover
1.55 +    { fix k assume "k \<le> k'"
1.56 +      hence "k < ?k'" unfolding Suc by simp
1.57 +      hence "b' ((c' ^^ k) (f s))" by (rule iffD1[OF not_not, OF not_less_Least])
1.58 +    } note b' = this
1.59 +    { fix k assume "k \<le> k'"
1.60 +      hence "f ((c ^^ k) s) = (c'^^k) (f s)" by (induct k) (auto simp: b' assms)
1.61 +      with `k \<le> k'` have "b ((c^^k) s)"
1.62 +      proof (induct k)
1.63 +        case (Suc k) thus ?case unfolding assms(1) by (simp only: b')
1.64 +      qed (simp add: b'[of 0, simplified] assms(1))
1.65 +    } note b = this
1.66 +    hence k': "f ((c^^k') s) = (c'^^k') (f s)" by (induct k') (auto simp: assms(2))
1.67 +    ultimately show ?thesis unfolding Suc using b
1.68 +    by (intro sym[OF Least_equality])
1.69 +       (auto simp add: assms(1) assms(2)[OF b] k' not_less_eq_eq[symmetric])
1.70 +  qed
1.71 +  have "f ((c ^^ ?k) s) = (c' ^^ ?k') (f s)" unfolding *
1.72 +    by (auto intro: funpow_commute assms(2) dest: not_less_Least)
1.73 +  thus "\<exists>z. (c ^^ ?k) s = z \<and> f z = (c' ^^ ?k') (f s)" by blast
1.74 +qed
1.75
1.76  subsection {* Total version *}
1.77
```