src/HOL/Library/While_Combinator.thy
author Andreas Lochbihler
Wed Feb 27 10:33:30 2013 +0100 (2013-02-27)
changeset 51288 be7e9a675ec9
parent 50577 cfbad2d08412
child 53217 1a8673a6d669
permissions -rw-r--r--
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
haftmann@22803
     1
(*  Title:      HOL/Library/While_Combinator.thy
wenzelm@10251
     2
    Author:     Tobias Nipkow
krauss@37757
     3
    Author:     Alexander Krauss
wenzelm@10251
     4
    Copyright   2000 TU Muenchen
wenzelm@10251
     5
*)
wenzelm@10251
     6
wenzelm@14706
     7
header {* A general ``while'' combinator *}
wenzelm@10251
     8
nipkow@15131
     9
theory While_Combinator
haftmann@30738
    10
imports Main
nipkow@15131
    11
begin
wenzelm@10251
    12
krauss@37760
    13
subsection {* Partial version *}
krauss@37757
    14
krauss@37757
    15
definition while_option :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
krauss@37757
    16
"while_option b c s = (if (\<exists>k. ~ b ((c ^^ k) s))
krauss@37757
    17
   then Some ((c ^^ (LEAST k. ~ b ((c ^^ k) s))) s)
krauss@37757
    18
   else None)"
wenzelm@10251
    19
krauss@37757
    20
theorem while_option_unfold[code]:
krauss@37757
    21
"while_option b c s = (if b s then while_option b c (c s) else Some s)"
krauss@37757
    22
proof cases
krauss@37757
    23
  assume "b s"
krauss@37757
    24
  show ?thesis
krauss@37757
    25
  proof (cases "\<exists>k. ~ b ((c ^^ k) s)")
krauss@37757
    26
    case True
krauss@37757
    27
    then obtain k where 1: "~ b ((c ^^ k) s)" ..
krauss@37757
    28
    with `b s` obtain l where "k = Suc l" by (cases k) auto
krauss@37757
    29
    with 1 have "~ b ((c ^^ l) (c s))" by (auto simp: funpow_swap1)
krauss@37757
    30
    then have 2: "\<exists>l. ~ b ((c ^^ l) (c s))" ..
krauss@37757
    31
    from 1
krauss@37757
    32
    have "(LEAST k. ~ b ((c ^^ k) s)) = Suc (LEAST l. ~ b ((c ^^ Suc l) s))"
krauss@37757
    33
      by (rule Least_Suc) (simp add: `b s`)
krauss@37757
    34
    also have "... = Suc (LEAST l. ~ b ((c ^^ l) (c s)))"
krauss@37757
    35
      by (simp add: funpow_swap1)
krauss@37757
    36
    finally
krauss@37757
    37
    show ?thesis 
krauss@37757
    38
      using True 2 `b s` by (simp add: funpow_swap1 while_option_def)
krauss@37757
    39
  next
krauss@37757
    40
    case False
krauss@37757
    41
    then have "~ (\<exists>l. ~ b ((c ^^ Suc l) s))" by blast
krauss@37757
    42
    then have "~ (\<exists>l. ~ b ((c ^^ l) (c s)))"
krauss@37757
    43
      by (simp add: funpow_swap1)
krauss@37757
    44
    with False  `b s` show ?thesis by (simp add: while_option_def)
krauss@37757
    45
  qed
krauss@37757
    46
next
krauss@37757
    47
  assume [simp]: "~ b s"
krauss@37757
    48
  have least: "(LEAST k. ~ b ((c ^^ k) s)) = 0"
krauss@37757
    49
    by (rule Least_equality) auto
krauss@37757
    50
  moreover 
krauss@37757
    51
  have "\<exists>k. ~ b ((c ^^ k) s)" by (rule exI[of _ "0::nat"]) auto
krauss@37757
    52
  ultimately show ?thesis unfolding while_option_def by auto 
krauss@37757
    53
qed
wenzelm@10251
    54
nipkow@45834
    55
lemma while_option_stop2:
nipkow@45834
    56
 "while_option b c s = Some t \<Longrightarrow> EX k. t = (c^^k) s \<and> \<not> b t"
nipkow@45834
    57
apply(simp add: while_option_def split: if_splits)
blanchet@46365
    58
by (metis (lifting) LeastI_ex)
nipkow@45834
    59
nipkow@45834
    60
lemma while_option_stop: "while_option b c s = Some t \<Longrightarrow> ~ b t"
nipkow@45834
    61
by(metis while_option_stop2)
krauss@37757
    62
krauss@37757
    63
theorem while_option_rule:
krauss@37757
    64
assumes step: "!!s. P s ==> b s ==> P (c s)"
krauss@37757
    65
and result: "while_option b c s = Some t"
krauss@37757
    66
and init: "P s"
krauss@37757
    67
shows "P t"
krauss@37757
    68
proof -
krauss@37757
    69
  def k == "LEAST k. ~ b ((c ^^ k) s)"
krauss@37757
    70
  from assms have t: "t = (c ^^ k) s"
krauss@37757
    71
    by (simp add: while_option_def k_def split: if_splits)    
krauss@37757
    72
  have 1: "ALL i<k. b ((c ^^ i) s)"
krauss@37757
    73
    by (auto simp: k_def dest: not_less_Least)
krauss@37757
    74
krauss@37757
    75
  { fix i assume "i <= k" then have "P ((c ^^ i) s)"
krauss@37757
    76
      by (induct i) (auto simp: init step 1) }
krauss@37757
    77
  thus "P t" by (auto simp: t)
krauss@37757
    78
qed
krauss@37757
    79
traytel@50577
    80
lemma funpow_commute: 
traytel@50577
    81
  "\<lbrakk>\<forall>k' < k. f (c ((c^^k') s)) = c' (f ((c^^k') s))\<rbrakk> \<Longrightarrow> f ((c^^k) s) = (c'^^k) (f s)"
traytel@50577
    82
by (induct k arbitrary: s) auto
traytel@50577
    83
traytel@50577
    84
lemma while_option_commute:
traytel@50577
    85
  assumes "\<And>s. b s = b' (f s)" "\<And>s. \<lbrakk>b s\<rbrakk> \<Longrightarrow> f (c s) = c' (f s)" 
traytel@50577
    86
  shows "Option.map f (while_option b c s) = while_option b' c' (f s)"
traytel@50577
    87
unfolding while_option_def
traytel@50577
    88
proof (rule trans[OF if_distrib if_cong], safe, unfold option.inject)
traytel@50577
    89
  fix k assume "\<not> b ((c ^^ k) s)"
traytel@50577
    90
  thus "\<exists>k. \<not> b' ((c' ^^ k) (f s))"
traytel@50577
    91
  proof (induction k arbitrary: s)
traytel@50577
    92
    case 0 thus ?case by (auto simp: assms(1) intro: exI[of _ 0])
traytel@50577
    93
  next
traytel@50577
    94
    case (Suc k)
traytel@50577
    95
    hence "\<not> b ((c^^k) (c s))" by (auto simp: funpow_swap1)
traytel@50577
    96
    then guess k by (rule exE[OF Suc.IH[of "c s"]])
traytel@50577
    97
    with assms show ?case by (cases "b s") (auto simp: funpow_swap1 intro: exI[of _ "Suc k"] exI[of _ "0"])
traytel@50577
    98
  qed
traytel@50577
    99
next
traytel@50577
   100
  fix k assume "\<not> b' ((c' ^^ k) (f s))"
traytel@50577
   101
  thus "\<exists>k. \<not> b ((c ^^ k) s)"
traytel@50577
   102
  proof (induction k arbitrary: s)
traytel@50577
   103
    case 0 thus ?case by (auto simp: assms(1) intro: exI[of _ 0])
traytel@50577
   104
  next
traytel@50577
   105
    case (Suc k)
traytel@50577
   106
    hence *: "\<not> b' ((c'^^k) (c' (f s)))" by (auto simp: funpow_swap1)
traytel@50577
   107
    show ?case
traytel@50577
   108
    proof (cases "b s")
traytel@50577
   109
      case True
traytel@50577
   110
      with assms(2) * have "\<not> b' ((c'^^k) (f (c s)))" by simp 
traytel@50577
   111
      then guess k by (rule exE[OF Suc.IH[of "c s"]])
traytel@50577
   112
      thus ?thesis by (auto simp: funpow_swap1 intro: exI[of _ "Suc k"])
traytel@50577
   113
    qed (auto intro: exI[of _ "0"])
traytel@50577
   114
  qed
traytel@50577
   115
next
traytel@50577
   116
  fix k assume k: "\<not> b' ((c' ^^ k) (f s))"
traytel@50577
   117
  have *: "(LEAST k. \<not> b' ((c' ^^ k) (f s))) = (LEAST k. \<not> b ((c ^^ k) s))" (is "?k' = ?k")
traytel@50577
   118
  proof (cases ?k')
traytel@50577
   119
    case 0
traytel@50577
   120
    have "\<not> b' ((c'^^0) (f s))" unfolding 0[symmetric] by (rule LeastI[of _ k]) (rule k)
traytel@50577
   121
    hence "\<not> b s" unfolding assms(1) by simp
traytel@50577
   122
    hence "?k = 0" by (intro Least_equality) auto
traytel@50577
   123
    with 0 show ?thesis by auto
traytel@50577
   124
  next
traytel@50577
   125
    case (Suc k')
traytel@50577
   126
    have "\<not> b' ((c'^^Suc k') (f s))" unfolding Suc[symmetric] by (rule LeastI) (rule k)
traytel@50577
   127
    moreover
traytel@50577
   128
    { fix k assume "k \<le> k'"
traytel@50577
   129
      hence "k < ?k'" unfolding Suc by simp
traytel@50577
   130
      hence "b' ((c' ^^ k) (f s))" by (rule iffD1[OF not_not, OF not_less_Least])
traytel@50577
   131
    } note b' = this
traytel@50577
   132
    { fix k assume "k \<le> k'"
traytel@50577
   133
      hence "f ((c ^^ k) s) = (c'^^k) (f s)" by (induct k) (auto simp: b' assms)
traytel@50577
   134
      with `k \<le> k'` have "b ((c^^k) s)"
traytel@50577
   135
      proof (induct k)
traytel@50577
   136
        case (Suc k) thus ?case unfolding assms(1) by (simp only: b')
traytel@50577
   137
      qed (simp add: b'[of 0, simplified] assms(1))
traytel@50577
   138
    } note b = this
traytel@50577
   139
    hence k': "f ((c^^k') s) = (c'^^k') (f s)" by (induct k') (auto simp: assms(2))
traytel@50577
   140
    ultimately show ?thesis unfolding Suc using b
traytel@50577
   141
    by (intro sym[OF Least_equality])
traytel@50577
   142
       (auto simp add: assms(1) assms(2)[OF b] k' not_less_eq_eq[symmetric])
traytel@50577
   143
  qed
traytel@50577
   144
  have "f ((c ^^ ?k) s) = (c' ^^ ?k') (f s)" unfolding *
traytel@50577
   145
    by (auto intro: funpow_commute assms(2) dest: not_less_Least)
traytel@50577
   146
  thus "\<exists>z. (c ^^ ?k) s = z \<and> f z = (c' ^^ ?k') (f s)" by blast
traytel@50577
   147
qed
krauss@37757
   148
krauss@37760
   149
subsection {* Total version *}
krauss@37757
   150
krauss@37757
   151
definition while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
krauss@37757
   152
where "while b c s = the (while_option b c s)"
krauss@37757
   153
nipkow@50008
   154
lemma while_unfold [code]:
krauss@37757
   155
  "while b c s = (if b s then while b c (c s) else s)"
krauss@37757
   156
unfolding while_def by (subst while_option_unfold) simp
nipkow@10984
   157
wenzelm@18372
   158
lemma def_while_unfold:
wenzelm@18372
   159
  assumes fdef: "f == while test do"
wenzelm@18372
   160
  shows "f x = (if test x then f(do x) else x)"
krauss@37757
   161
unfolding fdef by (fact while_unfold)
nipkow@14300
   162
nipkow@14300
   163
wenzelm@10251
   164
text {*
wenzelm@10251
   165
 The proof rule for @{term while}, where @{term P} is the invariant.
wenzelm@10251
   166
*}
wenzelm@10251
   167
wenzelm@18372
   168
theorem while_rule_lemma:
wenzelm@18372
   169
  assumes invariant: "!!s. P s ==> b s ==> P (c s)"
wenzelm@18372
   170
    and terminate: "!!s. P s ==> \<not> b s ==> Q s"
wenzelm@18372
   171
    and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
wenzelm@18372
   172
  shows "P s \<Longrightarrow> Q (while b c s)"
wenzelm@19736
   173
  using wf
wenzelm@19736
   174
  apply (induct s)
wenzelm@18372
   175
  apply simp
wenzelm@18372
   176
  apply (subst while_unfold)
wenzelm@18372
   177
  apply (simp add: invariant terminate)
wenzelm@18372
   178
  done
wenzelm@10251
   179
nipkow@10653
   180
theorem while_rule:
nipkow@10984
   181
  "[| P s;
nipkow@10984
   182
      !!s. [| P s; b s  |] ==> P (c s);
nipkow@10984
   183
      !!s. [| P s; \<not> b s  |] ==> Q s;
wenzelm@10997
   184
      wf r;
nipkow@10984
   185
      !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
nipkow@10984
   186
   Q (while b c s)"
wenzelm@19736
   187
  apply (rule while_rule_lemma)
wenzelm@19736
   188
     prefer 4 apply assumption
wenzelm@19736
   189
    apply blast
wenzelm@19736
   190
   apply blast
wenzelm@19736
   191
  apply (erule wf_subset)
wenzelm@19736
   192
  apply blast
wenzelm@19736
   193
  done
nipkow@10653
   194
nipkow@41720
   195
text{* Proving termination: *}
nipkow@41720
   196
nipkow@41720
   197
theorem wf_while_option_Some:
nipkow@41764
   198
  assumes "wf {(t, s). (P s \<and> b s) \<and> t = c s}"
nipkow@41764
   199
  and "!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s)" and "P s"
nipkow@41720
   200
  shows "EX t. while_option b c s = Some t"
nipkow@41764
   201
using assms(1,3)
nipkow@41720
   202
apply (induct s)
nipkow@41764
   203
using assms(2)
nipkow@41720
   204
apply (subst while_option_unfold)
nipkow@41720
   205
apply simp
nipkow@41720
   206
done
nipkow@41720
   207
nipkow@41720
   208
theorem measure_while_option_Some: fixes f :: "'s \<Rightarrow> nat"
nipkow@41764
   209
shows "(!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s) \<and> f(c s) < f s)
nipkow@41764
   210
  \<Longrightarrow> P s \<Longrightarrow> EX t. while_option b c s = Some t"
nipkow@41764
   211
by(blast intro: wf_while_option_Some[OF wf_if_measure, of P b f])
wenzelm@10251
   212
nipkow@45834
   213
text{* Kleene iteration starting from the empty set and assuming some finite
nipkow@45834
   214
bounding set: *}
nipkow@45834
   215
nipkow@45834
   216
lemma while_option_finite_subset_Some: fixes C :: "'a set"
nipkow@45834
   217
  assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
nipkow@45834
   218
  shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
nipkow@45834
   219
proof(rule measure_while_option_Some[where
nipkow@45834
   220
    f= "%A::'a set. card C - card A" and P= "%A. A \<subseteq> C \<and> A \<subseteq> f A" and s= "{}"])
nipkow@45834
   221
  fix A assume A: "A \<subseteq> C \<and> A \<subseteq> f A" "f A \<noteq> A"
nipkow@45834
   222
  show "(f A \<subseteq> C \<and> f A \<subseteq> f (f A)) \<and> card C - card (f A) < card C - card A"
nipkow@45834
   223
    (is "?L \<and> ?R")
nipkow@45834
   224
  proof
nipkow@45834
   225
    show ?L by(metis A(1) assms(2) monoD[OF `mono f`])
nipkow@45834
   226
    show ?R by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear rev_finite_subset)
nipkow@45834
   227
  qed
nipkow@45834
   228
qed simp
nipkow@45834
   229
nipkow@45834
   230
lemma lfp_the_while_option:
nipkow@45834
   231
  assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
nipkow@45834
   232
  shows "lfp f = the(while_option (\<lambda>A. f A \<noteq> A) f {})"
nipkow@45834
   233
proof-
nipkow@45834
   234
  obtain P where "while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
nipkow@45834
   235
    using while_option_finite_subset_Some[OF assms] by blast
nipkow@45834
   236
  with while_option_stop2[OF this] lfp_Kleene_iter[OF assms(1)]
nipkow@45834
   237
  show ?thesis by auto
nipkow@45834
   238
qed
nipkow@45834
   239
nipkow@50180
   240
lemma lfp_while:
nipkow@50180
   241
  assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
nipkow@50180
   242
  shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}"
nipkow@50180
   243
unfolding while_def using assms by (rule lfp_the_while_option) blast
nipkow@50180
   244
wenzelm@10251
   245
end