src/HOL/Library/While_Combinator.thy
author wenzelm
Sun Nov 26 21:08:32 2017 +0100 (16 months ago)
changeset 67091 1393c2340eec
parent 63561 fba08009ff3e
child 67613 ce654b0e6d69
permissions -rw-r--r--
more symbols;
haftmann@22803
     1
(*  Title:      HOL/Library/While_Combinator.thy
wenzelm@10251
     2
    Author:     Tobias Nipkow
krauss@37757
     3
    Author:     Alexander Krauss
wenzelm@10251
     4
*)
wenzelm@10251
     5
wenzelm@60500
     6
section \<open>A general ``while'' combinator\<close>
wenzelm@10251
     7
nipkow@15131
     8
theory While_Combinator
haftmann@30738
     9
imports Main
nipkow@15131
    10
begin
wenzelm@10251
    11
wenzelm@60500
    12
subsection \<open>Partial version\<close>
wenzelm@10251
    13
krauss@37757
    14
definition while_option :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
wenzelm@67091
    15
"while_option b c s = (if (\<exists>k. \<not> b ((c ^^ k) s))
wenzelm@67091
    16
   then Some ((c ^^ (LEAST k. \<not> b ((c ^^ k) s))) s)
krauss@37757
    17
   else None)"
wenzelm@10251
    18
krauss@37757
    19
theorem while_option_unfold[code]:
krauss@37757
    20
"while_option b c s = (if b s then while_option b c (c s) else Some s)"
krauss@37757
    21
proof cases
krauss@37757
    22
  assume "b s"
krauss@37757
    23
  show ?thesis
wenzelm@67091
    24
  proof (cases "\<exists>k. \<not> b ((c ^^ k) s)")
krauss@37757
    25
    case True
wenzelm@67091
    26
    then obtain k where 1: "\<not> b ((c ^^ k) s)" ..
wenzelm@60500
    27
    with \<open>b s\<close> obtain l where "k = Suc l" by (cases k) auto
wenzelm@67091
    28
    with 1 have "\<not> b ((c ^^ l) (c s))" by (auto simp: funpow_swap1)
wenzelm@67091
    29
    then have 2: "\<exists>l. \<not> b ((c ^^ l) (c s))" ..
krauss@37757
    30
    from 1
wenzelm@67091
    31
    have "(LEAST k. \<not> b ((c ^^ k) s)) = Suc (LEAST l. \<not> b ((c ^^ Suc l) s))"
wenzelm@60500
    32
      by (rule Least_Suc) (simp add: \<open>b s\<close>)
wenzelm@67091
    33
    also have "... = Suc (LEAST l. \<not> b ((c ^^ l) (c s)))"
krauss@37757
    34
      by (simp add: funpow_swap1)
krauss@37757
    35
    finally
krauss@37757
    36
    show ?thesis 
wenzelm@60500
    37
      using True 2 \<open>b s\<close> by (simp add: funpow_swap1 while_option_def)
krauss@37757
    38
  next
krauss@37757
    39
    case False
wenzelm@67091
    40
    then have "\<not> (\<exists>l. \<not> b ((c ^^ Suc l) s))" by blast
wenzelm@67091
    41
    then have "\<not> (\<exists>l. \<not> b ((c ^^ l) (c s)))"
krauss@37757
    42
      by (simp add: funpow_swap1)
wenzelm@60500
    43
    with False  \<open>b s\<close> show ?thesis by (simp add: while_option_def)
krauss@37757
    44
  qed
krauss@37757
    45
next
wenzelm@67091
    46
  assume [simp]: "\<not> b s"
wenzelm@67091
    47
  have least: "(LEAST k. \<not> b ((c ^^ k) s)) = 0"
krauss@37757
    48
    by (rule Least_equality) auto
krauss@37757
    49
  moreover 
wenzelm@67091
    50
  have "\<exists>k. \<not> b ((c ^^ k) s)" by (rule exI[of _ "0::nat"]) auto
krauss@37757
    51
  ultimately show ?thesis unfolding while_option_def by auto 
krauss@37757
    52
qed
krauss@37757
    53
nipkow@45834
    54
lemma while_option_stop2:
wenzelm@67091
    55
 "while_option b c s = Some t \<Longrightarrow> \<exists>k. t = (c^^k) s \<and> \<not> b t"
nipkow@45834
    56
apply(simp add: while_option_def split: if_splits)
blanchet@46365
    57
by (metis (lifting) LeastI_ex)
nipkow@45834
    58
wenzelm@67091
    59
lemma while_option_stop: "while_option b c s = Some t \<Longrightarrow> \<not> b t"
nipkow@45834
    60
by(metis while_option_stop2)
krauss@37757
    61
krauss@37757
    62
theorem while_option_rule:
wenzelm@63040
    63
  assumes step: "!!s. P s ==> b s ==> P (c s)"
wenzelm@63040
    64
    and result: "while_option b c s = Some t"
wenzelm@63040
    65
    and init: "P s"
wenzelm@63040
    66
  shows "P t"
krauss@37757
    67
proof -
wenzelm@67091
    68
  define k where "k = (LEAST k. \<not> b ((c ^^ k) s))"
krauss@37757
    69
  from assms have t: "t = (c ^^ k) s"
krauss@37757
    70
    by (simp add: while_option_def k_def split: if_splits)    
krauss@37757
    71
  have 1: "ALL i<k. b ((c ^^ i) s)"
krauss@37757
    72
    by (auto simp: k_def dest: not_less_Least)
krauss@37757
    73
wenzelm@67091
    74
  { fix i assume "i \<le> k" then have "P ((c ^^ i) s)"
krauss@37757
    75
      by (induct i) (auto simp: init step 1) }
krauss@37757
    76
  thus "P t" by (auto simp: t)
krauss@37757
    77
qed
krauss@37757
    78
traytel@50577
    79
lemma funpow_commute: 
traytel@50577
    80
  "\<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
    81
by (induct k arbitrary: s) auto
traytel@50577
    82
nipkow@54050
    83
lemma while_option_commute_invariant:
nipkow@54050
    84
assumes Invariant: "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> P (c s)"
nipkow@54050
    85
assumes TestCommute: "\<And>s. P s \<Longrightarrow> b s = b' (f s)"
nipkow@54050
    86
assumes BodyCommute: "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> f (c s) = c' (f s)"
nipkow@54050
    87
assumes Initial: "P s"
blanchet@55466
    88
shows "map_option f (while_option b c s) = while_option b' c' (f s)"
traytel@50577
    89
unfolding while_option_def
traytel@50577
    90
proof (rule trans[OF if_distrib if_cong], safe, unfold option.inject)
nipkow@54050
    91
  fix k
nipkow@54050
    92
  assume "\<not> b ((c ^^ k) s)"
nipkow@54050
    93
  with Initial show "\<exists>k. \<not> b' ((c' ^^ k) (f s))"
traytel@50577
    94
  proof (induction k arbitrary: s)
nipkow@54050
    95
    case 0 thus ?case by (auto simp: TestCommute intro: exI[of _ 0])
traytel@50577
    96
  next
nipkow@54050
    97
    case (Suc k) thus ?case
nipkow@54050
    98
    proof (cases "b s")
nipkow@54050
    99
      assume "b s"
nipkow@54050
   100
      with Suc.IH[of "c s"] Suc.prems show ?thesis
nipkow@54050
   101
        by (metis BodyCommute Invariant comp_apply funpow.simps(2) funpow_swap1)
nipkow@54050
   102
    next
nipkow@54050
   103
      assume "\<not> b s"
nipkow@54050
   104
      with Suc show ?thesis by (auto simp: TestCommute intro: exI [of _ 0])
nipkow@54050
   105
    qed
traytel@50577
   106
  qed
traytel@50577
   107
next
nipkow@54050
   108
  fix k
nipkow@54050
   109
  assume "\<not> b' ((c' ^^ k) (f s))"
nipkow@54050
   110
  with Initial show "\<exists>k. \<not> b ((c ^^ k) s)"
traytel@50577
   111
  proof (induction k arbitrary: s)
nipkow@54050
   112
    case 0 thus ?case by (auto simp: TestCommute intro: exI[of _ 0])
traytel@50577
   113
  next
nipkow@54050
   114
    case (Suc k) thus ?case
traytel@50577
   115
    proof (cases "b s")
nipkow@54050
   116
       assume "b s"
nipkow@54050
   117
      with Suc.IH[of "c s"] Suc.prems show ?thesis
nipkow@54050
   118
        by (metis BodyCommute Invariant comp_apply funpow.simps(2) funpow_swap1)
nipkow@54050
   119
    next
nipkow@54050
   120
      assume "\<not> b s"
nipkow@54050
   121
      with Suc show ?thesis by (auto simp: TestCommute intro: exI [of _ 0])
nipkow@54050
   122
    qed
traytel@50577
   123
  qed
traytel@50577
   124
next
nipkow@54050
   125
  fix k
nipkow@54050
   126
  assume k: "\<not> b' ((c' ^^ k) (f s))"
nipkow@54050
   127
  have *: "(LEAST k. \<not> b' ((c' ^^ k) (f s))) = (LEAST k. \<not> b ((c ^^ k) s))"
nipkow@54050
   128
          (is "?k' = ?k")
traytel@50577
   129
  proof (cases ?k')
traytel@50577
   130
    case 0
nipkow@54050
   131
    have "\<not> b' ((c' ^^ 0) (f s))"
nipkow@54050
   132
      unfolding 0[symmetric] by (rule LeastI[of _ k]) (rule k)
nipkow@54050
   133
    hence "\<not> b s" by (auto simp: TestCommute Initial)
traytel@50577
   134
    hence "?k = 0" by (intro Least_equality) auto
traytel@50577
   135
    with 0 show ?thesis by auto
traytel@50577
   136
  next
traytel@50577
   137
    case (Suc k')
nipkow@54050
   138
    have "\<not> b' ((c' ^^ Suc k') (f s))"
nipkow@54050
   139
      unfolding Suc[symmetric] by (rule LeastI) (rule k)
traytel@50577
   140
    moreover
traytel@50577
   141
    { fix k assume "k \<le> k'"
traytel@50577
   142
      hence "k < ?k'" unfolding Suc by simp
traytel@50577
   143
      hence "b' ((c' ^^ k) (f s))" by (rule iffD1[OF not_not, OF not_less_Least])
nipkow@54050
   144
    }
nipkow@54050
   145
    note b' = this
traytel@50577
   146
    { fix k assume "k \<le> k'"
nipkow@54050
   147
      hence "f ((c ^^ k) s) = (c' ^^ k) (f s)"
nipkow@54050
   148
      and "b ((c ^^ k) s) = b' ((c' ^^ k) (f s))"
nipkow@54050
   149
      and "P ((c ^^ k) s)"
nipkow@54050
   150
        by (induct k) (auto simp: b' assms)
wenzelm@60500
   151
      with \<open>k \<le> k'\<close>
nipkow@54050
   152
      have "b ((c ^^ k) s)"
nipkow@54050
   153
      and "f ((c ^^ k) s) = (c' ^^ k) (f s)"
nipkow@54050
   154
      and "P ((c ^^ k) s)"
nipkow@54050
   155
        by (auto simp: b')
nipkow@54050
   156
    }
nipkow@54050
   157
    note b = this(1) and body = this(2) and inv = this(3)
nipkow@54050
   158
    hence k': "f ((c ^^ k') s) = (c' ^^ k') (f s)" by auto
traytel@50577
   159
    ultimately show ?thesis unfolding Suc using b
wenzelm@61166
   160
    proof (intro Least_equality[symmetric], goal_cases)
wenzelm@60580
   161
      case 1
nipkow@54050
   162
      hence Test: "\<not> b' (f ((c ^^ Suc k') s))"
nipkow@54050
   163
        by (auto simp: BodyCommute inv b)
nipkow@54050
   164
      have "P ((c ^^ Suc k') s)" by (auto simp: Invariant inv b)
nipkow@54050
   165
      with Test show ?case by (auto simp: TestCommute)
nipkow@54050
   166
    next
wenzelm@60580
   167
      case 2
wenzelm@60580
   168
      thus ?case by (metis not_less_eq_eq)
nipkow@54050
   169
    qed
traytel@50577
   170
  qed
traytel@50577
   171
  have "f ((c ^^ ?k) s) = (c' ^^ ?k') (f s)" unfolding *
nipkow@54050
   172
  proof (rule funpow_commute, clarify)
nipkow@54050
   173
    fix k assume "k < ?k"
nipkow@54050
   174
    hence TestTrue: "b ((c ^^ k) s)" by (auto dest: not_less_Least)
wenzelm@60500
   175
    from \<open>k < ?k\<close> have "P ((c ^^ k) s)"
nipkow@54050
   176
    proof (induct k)
nipkow@54050
   177
      case 0 thus ?case by (auto simp: assms)
nipkow@54050
   178
    next
nipkow@54050
   179
      case (Suc h)
nipkow@54050
   180
      hence "P ((c ^^ h) s)" by auto
nipkow@54050
   181
      with Suc show ?case
nipkow@54050
   182
        by (auto, metis (lifting, no_types) Invariant Suc_lessD not_less_Least)
nipkow@54050
   183
    qed
nipkow@54050
   184
    with TestTrue show "f (c ((c ^^ k) s)) = c' (f ((c ^^ k) s))"
nipkow@54050
   185
      by (metis BodyCommute)
nipkow@54050
   186
  qed
traytel@50577
   187
  thus "\<exists>z. (c ^^ ?k) s = z \<and> f z = (c' ^^ ?k') (f s)" by blast
traytel@50577
   188
qed
krauss@37757
   189
nipkow@54050
   190
lemma while_option_commute:
nipkow@54050
   191
  assumes "\<And>s. b s = b' (f s)" "\<And>s. \<lbrakk>b s\<rbrakk> \<Longrightarrow> f (c s) = c' (f s)" 
blanchet@55466
   192
  shows "map_option f (while_option b c s) = while_option b' c' (f s)"
nipkow@54050
   193
by(rule while_option_commute_invariant[where P = "\<lambda>_. True"])
nipkow@54050
   194
  (auto simp add: assms)
nipkow@54050
   195
wenzelm@60500
   196
subsection \<open>Total version\<close>
krauss@37757
   197
krauss@37757
   198
definition while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
krauss@37757
   199
where "while b c s = the (while_option b c s)"
krauss@37757
   200
nipkow@50008
   201
lemma while_unfold [code]:
krauss@37757
   202
  "while b c s = (if b s then while b c (c s) else s)"
krauss@37757
   203
unfolding while_def by (subst while_option_unfold) simp
nipkow@10984
   204
wenzelm@18372
   205
lemma def_while_unfold:
wenzelm@18372
   206
  assumes fdef: "f == while test do"
wenzelm@18372
   207
  shows "f x = (if test x then f(do x) else x)"
krauss@37757
   208
unfolding fdef by (fact while_unfold)
nipkow@14300
   209
nipkow@14300
   210
wenzelm@60500
   211
text \<open>
wenzelm@10251
   212
 The proof rule for @{term while}, where @{term P} is the invariant.
wenzelm@60500
   213
\<close>
wenzelm@10251
   214
wenzelm@18372
   215
theorem while_rule_lemma:
wenzelm@18372
   216
  assumes invariant: "!!s. P s ==> b s ==> P (c s)"
wenzelm@18372
   217
    and terminate: "!!s. P s ==> \<not> b s ==> Q s"
wenzelm@18372
   218
    and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
wenzelm@18372
   219
  shows "P s \<Longrightarrow> Q (while b c s)"
wenzelm@19736
   220
  using wf
wenzelm@19736
   221
  apply (induct s)
wenzelm@18372
   222
  apply simp
wenzelm@18372
   223
  apply (subst while_unfold)
wenzelm@18372
   224
  apply (simp add: invariant terminate)
wenzelm@18372
   225
  done
wenzelm@10251
   226
nipkow@10653
   227
theorem while_rule:
nipkow@10984
   228
  "[| P s;
nipkow@10984
   229
      !!s. [| P s; b s  |] ==> P (c s);
nipkow@10984
   230
      !!s. [| P s; \<not> b s  |] ==> Q s;
wenzelm@10997
   231
      wf r;
nipkow@10984
   232
      !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
nipkow@10984
   233
   Q (while b c s)"
wenzelm@19736
   234
  apply (rule while_rule_lemma)
wenzelm@19736
   235
     prefer 4 apply assumption
wenzelm@19736
   236
    apply blast
wenzelm@19736
   237
   apply blast
wenzelm@19736
   238
  apply (erule wf_subset)
wenzelm@19736
   239
  apply blast
wenzelm@19736
   240
  done
nipkow@10653
   241
wenzelm@60500
   242
text\<open>Proving termination:\<close>
nipkow@41720
   243
nipkow@41720
   244
theorem wf_while_option_Some:
nipkow@41764
   245
  assumes "wf {(t, s). (P s \<and> b s) \<and> t = c s}"
wenzelm@67091
   246
  and "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s)" and "P s"
wenzelm@67091
   247
  shows "\<exists>t. while_option b c s = Some t"
nipkow@41764
   248
using assms(1,3)
nipkow@54050
   249
proof (induction s)
nipkow@54050
   250
  case less thus ?case using assms(2)
nipkow@54050
   251
    by (subst while_option_unfold) simp
nipkow@54050
   252
qed
nipkow@54050
   253
nipkow@54050
   254
lemma wf_rel_while_option_Some:
nipkow@54050
   255
assumes wf: "wf R"
nipkow@54050
   256
assumes smaller: "\<And>s. P s \<and> b s \<Longrightarrow> (c s, s) \<in> R"
nipkow@54050
   257
assumes inv: "\<And>s. P s \<and> b s \<Longrightarrow> P(c s)"
nipkow@54050
   258
assumes init: "P s"
nipkow@54050
   259
shows "\<exists>t. while_option b c s = Some t"
nipkow@54050
   260
proof -
nipkow@54050
   261
 from smaller have "{(t,s). P s \<and> b s \<and> t = c s} \<subseteq> R" by auto
nipkow@54050
   262
 with wf have "wf {(t,s). P s \<and> b s \<and> t = c s}" by (auto simp: wf_subset)
nipkow@54050
   263
 with inv init show ?thesis by (auto simp: wf_while_option_Some)
nipkow@54050
   264
qed
nipkow@41720
   265
nipkow@41720
   266
theorem measure_while_option_Some: fixes f :: "'s \<Rightarrow> nat"
wenzelm@67091
   267
shows "(\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s) \<and> f(c s) < f s)
wenzelm@67091
   268
  \<Longrightarrow> P s \<Longrightarrow> \<exists>t. while_option b c s = Some t"
nipkow@41764
   269
by(blast intro: wf_while_option_Some[OF wf_if_measure, of P b f])
wenzelm@10251
   270
wenzelm@60500
   271
text\<open>Kleene iteration starting from the empty set and assuming some finite
wenzelm@60500
   272
bounding set:\<close>
nipkow@45834
   273
nipkow@45834
   274
lemma while_option_finite_subset_Some: fixes C :: "'a set"
nipkow@45834
   275
  assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
nipkow@45834
   276
  shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
nipkow@45834
   277
proof(rule measure_while_option_Some[where
nipkow@45834
   278
    f= "%A::'a set. card C - card A" and P= "%A. A \<subseteq> C \<and> A \<subseteq> f A" and s= "{}"])
nipkow@45834
   279
  fix A assume A: "A \<subseteq> C \<and> A \<subseteq> f A" "f A \<noteq> A"
nipkow@45834
   280
  show "(f A \<subseteq> C \<and> f A \<subseteq> f (f A)) \<and> card C - card (f A) < card C - card A"
nipkow@45834
   281
    (is "?L \<and> ?R")
nipkow@45834
   282
  proof
wenzelm@60500
   283
    show ?L by(metis A(1) assms(2) monoD[OF \<open>mono f\<close>])
nipkow@45834
   284
    show ?R by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear rev_finite_subset)
nipkow@45834
   285
  qed
nipkow@45834
   286
qed simp
nipkow@45834
   287
nipkow@45834
   288
lemma lfp_the_while_option:
nipkow@45834
   289
  assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
nipkow@45834
   290
  shows "lfp f = the(while_option (\<lambda>A. f A \<noteq> A) f {})"
nipkow@45834
   291
proof-
nipkow@45834
   292
  obtain P where "while_option (\<lambda>A. f A \<noteq> A) f {} = Some P"
nipkow@45834
   293
    using while_option_finite_subset_Some[OF assms] by blast
nipkow@45834
   294
  with while_option_stop2[OF this] lfp_Kleene_iter[OF assms(1)]
nipkow@45834
   295
  show ?thesis by auto
nipkow@45834
   296
qed
nipkow@45834
   297
nipkow@50180
   298
lemma lfp_while:
nipkow@50180
   299
  assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C"
nipkow@50180
   300
  shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}"
nipkow@50180
   301
unfolding while_def using assms by (rule lfp_the_while_option) blast
nipkow@50180
   302
Andreas@63561
   303
lemma wf_finite_less:
Andreas@63561
   304
  assumes "finite (C :: 'a::order set)"
Andreas@63561
   305
  shows "wf {(x, y). {x, y} \<subseteq> C \<and> x < y}"
Andreas@63561
   306
by (rule wf_measure[where f="\<lambda>b. card {a. a \<in> C \<and> a < b}", THEN wf_subset])
Andreas@63561
   307
   (fastforce simp: less_eq assms intro: psubset_card_mono)
Andreas@63561
   308
Andreas@63561
   309
lemma wf_finite_greater:
Andreas@63561
   310
  assumes "finite (C :: 'a::order set)"
Andreas@63561
   311
  shows "wf {(x, y). {x, y} \<subseteq> C \<and> y < x}"
Andreas@63561
   312
by (rule wf_measure[where f="\<lambda>b. card {a. a \<in> C \<and> b < a}", THEN wf_subset])
Andreas@63561
   313
   (fastforce simp: less_eq assms intro: psubset_card_mono)
Andreas@63561
   314
Andreas@63561
   315
lemma while_option_finite_increasing_Some:
Andreas@63561
   316
  fixes f :: "'a::order \<Rightarrow> 'a"
Andreas@63561
   317
  assumes "mono f" and "finite (UNIV :: 'a set)" and "s \<le> f s"
Andreas@63561
   318
  shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f s = Some P"
Andreas@63561
   319
by (rule wf_rel_while_option_Some[where R="{(x, y). y < x}" and P="\<lambda>A. A \<le> f A" and s="s"])
Andreas@63561
   320
   (auto simp: assms monoD intro: wf_finite_greater[where C="UNIV::'a set", simplified])
Andreas@63561
   321
Andreas@63561
   322
lemma lfp_the_while_option_lattice:
Andreas@63561
   323
  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
Andreas@63561
   324
  assumes "mono f" and "finite (UNIV :: 'a set)"
Andreas@63561
   325
  shows "lfp f = the (while_option (\<lambda>A. f A \<noteq> A) f bot)"
Andreas@63561
   326
proof -
Andreas@63561
   327
  obtain P where "while_option (\<lambda>A. f A \<noteq> A) f bot = Some P"
Andreas@63561
   328
    using while_option_finite_increasing_Some[OF assms, where s=bot] by simp blast
Andreas@63561
   329
  with while_option_stop2[OF this] lfp_Kleene_iter[OF assms(1)]
Andreas@63561
   330
  show ?thesis by auto
Andreas@63561
   331
qed
Andreas@63561
   332
Andreas@63561
   333
lemma lfp_while_lattice:
Andreas@63561
   334
  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
Andreas@63561
   335
  assumes "mono f" and "finite (UNIV :: 'a set)"
Andreas@63561
   336
  shows "lfp f = while (\<lambda>A. f A \<noteq> A) f bot"
Andreas@63561
   337
unfolding while_def using assms by (rule lfp_the_while_option_lattice)
Andreas@63561
   338
Andreas@63561
   339
lemma while_option_finite_decreasing_Some:
Andreas@63561
   340
  fixes f :: "'a::order \<Rightarrow> 'a"
Andreas@63561
   341
  assumes "mono f" and "finite (UNIV :: 'a set)" and "f s \<le> s"
Andreas@63561
   342
  shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f s = Some P"
Andreas@63561
   343
by (rule wf_rel_while_option_Some[where R="{(x, y). x < y}" and P="\<lambda>A. f A \<le> A" and s="s"])
Andreas@63561
   344
   (auto simp add: assms monoD intro: wf_finite_less[where C="UNIV::'a set", simplified])
Andreas@63561
   345
Andreas@63561
   346
lemma gfp_the_while_option_lattice:
Andreas@63561
   347
  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
Andreas@63561
   348
  assumes "mono f" and "finite (UNIV :: 'a set)"
Andreas@63561
   349
  shows "gfp f = the(while_option (\<lambda>A. f A \<noteq> A) f top)"
Andreas@63561
   350
proof -
Andreas@63561
   351
  obtain P where "while_option (\<lambda>A. f A \<noteq> A) f top = Some P"
Andreas@63561
   352
    using while_option_finite_decreasing_Some[OF assms, where s=top] by simp blast
Andreas@63561
   353
  with while_option_stop2[OF this] gfp_Kleene_iter[OF assms(1)]
Andreas@63561
   354
  show ?thesis by auto
Andreas@63561
   355
qed
Andreas@63561
   356
Andreas@63561
   357
lemma gfp_while_lattice:
Andreas@63561
   358
  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
Andreas@63561
   359
  assumes "mono f" and "finite (UNIV :: 'a set)"
Andreas@63561
   360
  shows "gfp f = while (\<lambda>A. f A \<noteq> A) f top"
Andreas@63561
   361
unfolding while_def using assms by (rule gfp_the_while_option_lattice)
nipkow@53217
   362
wenzelm@60500
   363
text\<open>Computing the reflexive, transitive closure by iterating a successor
nipkow@53217
   364
function. Stops when an element is found that dos not satisfy the test.
nipkow@53217
   365
nipkow@53217
   366
More refined (and hence more efficient) versions can be found in ITP 2011 paper
nipkow@53217
   367
by Nipkow (the theories are in the AFP entry Flyspeck by Nipkow)
wenzelm@60500
   368
and the AFP article Executable Transitive Closures by René Thiemann.\<close>
nipkow@53217
   369
traytel@54196
   370
context
traytel@54196
   371
fixes p :: "'a \<Rightarrow> bool"
traytel@54196
   372
and f :: "'a \<Rightarrow> 'a list"
traytel@54196
   373
and x :: 'a
traytel@54196
   374
begin
nipkow@53217
   375
wenzelm@61115
   376
qualified fun rtrancl_while_test :: "'a list \<times> 'a set \<Rightarrow> bool"
traytel@54196
   377
where "rtrancl_while_test (ws,_) = (ws \<noteq> [] \<and> p(hd ws))"
traytel@54196
   378
wenzelm@61115
   379
qualified fun rtrancl_while_step :: "'a list \<times> 'a set \<Rightarrow> 'a list \<times> 'a set"
traytel@54196
   380
where "rtrancl_while_step (ws, Z) =
traytel@54196
   381
  (let x = hd ws; new = remdups (filter (\<lambda>y. y \<notin> Z) (f x))
traytel@54196
   382
  in (new @ tl ws, set new \<union> Z))"
traytel@54196
   383
traytel@54196
   384
definition rtrancl_while :: "('a list * 'a set) option"
traytel@54196
   385
where "rtrancl_while = while_option rtrancl_while_test rtrancl_while_step ([x],{x})"
traytel@54196
   386
wenzelm@61115
   387
qualified fun rtrancl_while_invariant :: "'a list \<times> 'a set \<Rightarrow> bool"
traytel@54196
   388
where "rtrancl_while_invariant (ws, Z) =
traytel@54196
   389
   (x \<in> Z \<and> set ws \<subseteq> Z \<and> distinct ws \<and> {(x,y). y \<in> set(f x)} `` (Z - set ws) \<subseteq> Z \<and>
traytel@54196
   390
    Z \<subseteq> {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z - set ws. p z))"
traytel@54196
   391
wenzelm@61115
   392
qualified lemma rtrancl_while_invariant: 
traytel@54196
   393
  assumes inv: "rtrancl_while_invariant st" and test: "rtrancl_while_test st"
traytel@54196
   394
  shows   "rtrancl_while_invariant (rtrancl_while_step st)"
traytel@54196
   395
proof (cases st)
traytel@54196
   396
  fix ws Z assume st: "st = (ws, Z)"
traytel@54196
   397
  with test obtain h t where "ws = h # t" "p h" by (cases ws) auto
traytel@54196
   398
  with inv st show ?thesis by (auto intro: rtrancl.rtrancl_into_rtrancl)
traytel@54196
   399
qed
traytel@54196
   400
traytel@54196
   401
lemma rtrancl_while_Some: assumes "rtrancl_while = Some(ws,Z)"
nipkow@53217
   402
shows "if ws = []
nipkow@53217
   403
       then Z = {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z. p z)
nipkow@53217
   404
       else \<not>p(hd ws) \<and> hd ws \<in> {(x,y). y \<in> set(f x)}^* `` {x}"
traytel@54196
   405
proof -
traytel@54196
   406
  have "rtrancl_while_invariant ([x],{x})" by simp
traytel@54196
   407
  with rtrancl_while_invariant have I: "rtrancl_while_invariant (ws,Z)"
nipkow@53217
   408
    by (rule while_option_rule[OF _ assms[unfolded rtrancl_while_def]])
nipkow@53217
   409
  { assume "ws = []"
nipkow@53217
   410
    hence ?thesis using I
haftmann@61424
   411
      by (auto simp del:Image_Collect_case_prod dest: Image_closed_trancl)
nipkow@53217
   412
  } moreover
nipkow@53217
   413
  { assume "ws \<noteq> []"
nipkow@53217
   414
    hence ?thesis using I while_option_stop[OF assms[unfolded rtrancl_while_def]]
nipkow@53217
   415
      by (simp add: subset_iff)
nipkow@53217
   416
  }
nipkow@53217
   417
  ultimately show ?thesis by simp
nipkow@53217
   418
qed
nipkow@53217
   419
traytel@54196
   420
lemma rtrancl_while_finite_Some:
traytel@54196
   421
  assumes "finite ({(x, y). y \<in> set (f x)}\<^sup>* `` {x})" (is "finite ?Cl")
traytel@54196
   422
  shows "\<exists>y. rtrancl_while = Some y"
traytel@54196
   423
proof -
traytel@54196
   424
  let ?R = "(\<lambda>(_, Z). card (?Cl - Z)) <*mlex*> (\<lambda>(ws, _). length ws) <*mlex*> {}"
traytel@54196
   425
  have "wf ?R" by (blast intro: wf_mlex)
traytel@54196
   426
  then show ?thesis unfolding rtrancl_while_def
traytel@54196
   427
  proof (rule wf_rel_while_option_Some[of ?R rtrancl_while_invariant])
traytel@54196
   428
    fix st assume *: "rtrancl_while_invariant st \<and> rtrancl_while_test st"
traytel@54196
   429
    hence I: "rtrancl_while_invariant (rtrancl_while_step st)"
traytel@54196
   430
      by (blast intro: rtrancl_while_invariant)
traytel@54196
   431
    show "(rtrancl_while_step st, st) \<in> ?R"
traytel@54196
   432
    proof (cases st)
traytel@54196
   433
      fix ws Z let ?ws = "fst (rtrancl_while_step st)" and ?Z = "snd (rtrancl_while_step st)"
traytel@54196
   434
      assume st: "st = (ws, Z)"
traytel@54196
   435
      with * obtain h t where ws: "ws = h # t" "p h" by (cases ws) auto
traytel@54196
   436
      { assume "remdups (filter (\<lambda>y. y \<notin> Z) (f h)) \<noteq> []"
traytel@54196
   437
        then obtain z where "z \<in> set (remdups (filter (\<lambda>y. y \<notin> Z) (f h)))" by fastforce
traytel@54196
   438
        with st ws I have "Z \<subset> ?Z" "Z \<subseteq> ?Cl" "?Z \<subseteq> ?Cl" by auto
traytel@54196
   439
        with assms have "card (?Cl - ?Z) < card (?Cl - Z)" by (blast intro: psubset_card_mono)
traytel@54196
   440
        with st ws have ?thesis unfolding mlex_prod_def by simp
traytel@54196
   441
      }
traytel@54196
   442
      moreover
traytel@54196
   443
      { assume "remdups (filter (\<lambda>y. y \<notin> Z) (f h)) = []"
traytel@54196
   444
        with st ws have "?Z = Z" "?ws = t"  by (auto simp: filter_empty_conv)
traytel@54196
   445
        with st ws have ?thesis unfolding mlex_prod_def by simp
traytel@54196
   446
      }
traytel@54196
   447
      ultimately show ?thesis by blast
traytel@54196
   448
    qed
traytel@54196
   449
  qed (simp_all add: rtrancl_while_invariant)
traytel@54196
   450
qed
traytel@54196
   451
wenzelm@10251
   452
end
traytel@54196
   453
traytel@54196
   454
end