useful commutative diagram for while_option
authortraytel
Mon Dec 17 15:17:32 2012 +0100 (2012-12-17)
changeset 50577cfbad2d08412
parent 50573 765c22baa1c9
child 50579 8ccffe44d193
useful commutative diagram for while_option
src/HOL/Library/While_Combinator.thy
     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