src/HOL/Library/While_Combinator.thy
 changeset 67091 1393c2340eec parent 63561 fba08009ff3e child 67613 ce654b0e6d69
```     1.1 --- a/src/HOL/Library/While_Combinator.thy	Sun Nov 26 13:19:52 2017 +0100
1.2 +++ b/src/HOL/Library/While_Combinator.thy	Sun Nov 26 21:08:32 2017 +0100
1.3 @@ -12,8 +12,8 @@
1.4  subsection \<open>Partial version\<close>
1.5
1.6  definition while_option :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
1.7 -"while_option b c s = (if (\<exists>k. ~ b ((c ^^ k) s))
1.8 -   then Some ((c ^^ (LEAST k. ~ b ((c ^^ k) s))) s)
1.9 +"while_option b c s = (if (\<exists>k. \<not> b ((c ^^ k) s))
1.10 +   then Some ((c ^^ (LEAST k. \<not> b ((c ^^ k) s))) s)
1.11     else None)"
1.12
1.13  theorem while_option_unfold[code]:
1.14 @@ -21,42 +21,42 @@
1.15  proof cases
1.16    assume "b s"
1.17    show ?thesis
1.18 -  proof (cases "\<exists>k. ~ b ((c ^^ k) s)")
1.19 +  proof (cases "\<exists>k. \<not> b ((c ^^ k) s)")
1.20      case True
1.21 -    then obtain k where 1: "~ b ((c ^^ k) s)" ..
1.22 +    then obtain k where 1: "\<not> b ((c ^^ k) s)" ..
1.23      with \<open>b s\<close> obtain l where "k = Suc l" by (cases k) auto
1.24 -    with 1 have "~ b ((c ^^ l) (c s))" by (auto simp: funpow_swap1)
1.25 -    then have 2: "\<exists>l. ~ b ((c ^^ l) (c s))" ..
1.26 +    with 1 have "\<not> b ((c ^^ l) (c s))" by (auto simp: funpow_swap1)
1.27 +    then have 2: "\<exists>l. \<not> b ((c ^^ l) (c s))" ..
1.28      from 1
1.29 -    have "(LEAST k. ~ b ((c ^^ k) s)) = Suc (LEAST l. ~ b ((c ^^ Suc l) s))"
1.30 +    have "(LEAST k. \<not> b ((c ^^ k) s)) = Suc (LEAST l. \<not> b ((c ^^ Suc l) s))"
1.31        by (rule Least_Suc) (simp add: \<open>b s\<close>)
1.32 -    also have "... = Suc (LEAST l. ~ b ((c ^^ l) (c s)))"
1.33 +    also have "... = Suc (LEAST l. \<not> b ((c ^^ l) (c s)))"
1.35      finally
1.36      show ?thesis
1.37        using True 2 \<open>b s\<close> by (simp add: funpow_swap1 while_option_def)
1.38    next
1.39      case False
1.40 -    then have "~ (\<exists>l. ~ b ((c ^^ Suc l) s))" by blast
1.41 -    then have "~ (\<exists>l. ~ b ((c ^^ l) (c s)))"
1.42 +    then have "\<not> (\<exists>l. \<not> b ((c ^^ Suc l) s))" by blast
1.43 +    then have "\<not> (\<exists>l. \<not> b ((c ^^ l) (c s)))"
1.45      with False  \<open>b s\<close> show ?thesis by (simp add: while_option_def)
1.46    qed
1.47  next
1.48 -  assume [simp]: "~ b s"
1.49 -  have least: "(LEAST k. ~ b ((c ^^ k) s)) = 0"
1.50 +  assume [simp]: "\<not> b s"
1.51 +  have least: "(LEAST k. \<not> b ((c ^^ k) s)) = 0"
1.52      by (rule Least_equality) auto
1.53    moreover
1.54 -  have "\<exists>k. ~ b ((c ^^ k) s)" by (rule exI[of _ "0::nat"]) auto
1.55 +  have "\<exists>k. \<not> b ((c ^^ k) s)" by (rule exI[of _ "0::nat"]) auto
1.56    ultimately show ?thesis unfolding while_option_def by auto
1.57  qed
1.58
1.59  lemma while_option_stop2:
1.60 - "while_option b c s = Some t \<Longrightarrow> EX k. t = (c^^k) s \<and> \<not> b t"
1.61 + "while_option b c s = Some t \<Longrightarrow> \<exists>k. t = (c^^k) s \<and> \<not> b t"
1.62  apply(simp add: while_option_def split: if_splits)
1.63  by (metis (lifting) LeastI_ex)
1.64
1.65 -lemma while_option_stop: "while_option b c s = Some t \<Longrightarrow> ~ b t"
1.66 +lemma while_option_stop: "while_option b c s = Some t \<Longrightarrow> \<not> b t"
1.67  by(metis while_option_stop2)
1.68
1.69  theorem while_option_rule:
1.70 @@ -65,13 +65,13 @@
1.71      and init: "P s"
1.72    shows "P t"
1.73  proof -
1.74 -  define k where "k = (LEAST k. ~ b ((c ^^ k) s))"
1.75 +  define k where "k = (LEAST k. \<not> b ((c ^^ k) s))"
1.76    from assms have t: "t = (c ^^ k) s"
1.77      by (simp add: while_option_def k_def split: if_splits)
1.78    have 1: "ALL i<k. b ((c ^^ i) s)"
1.79      by (auto simp: k_def dest: not_less_Least)
1.80
1.81 -  { fix i assume "i <= k" then have "P ((c ^^ i) s)"
1.82 +  { fix i assume "i \<le> k" then have "P ((c ^^ i) s)"
1.83        by (induct i) (auto simp: init step 1) }
1.84    thus "P t" by (auto simp: t)
1.85  qed
1.86 @@ -243,8 +243,8 @@
1.87
1.88  theorem wf_while_option_Some:
1.89    assumes "wf {(t, s). (P s \<and> b s) \<and> t = c s}"
1.90 -  and "!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s)" and "P s"
1.91 -  shows "EX t. while_option b c s = Some t"
1.92 +  and "\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s)" and "P s"
1.93 +  shows "\<exists>t. while_option b c s = Some t"
1.94  using assms(1,3)
1.95  proof (induction s)
1.96    case less thus ?case using assms(2)
1.97 @@ -264,8 +264,8 @@
1.98  qed
1.99
1.100  theorem measure_while_option_Some: fixes f :: "'s \<Rightarrow> nat"
1.101 -shows "(!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s) \<and> f(c s) < f s)
1.102 -  \<Longrightarrow> P s \<Longrightarrow> EX t. while_option b c s = Some t"
1.103 +shows "(\<And>s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s) \<and> f(c s) < f s)
1.104 +  \<Longrightarrow> P s \<Longrightarrow> \<exists>t. while_option b c s = Some t"
1.105  by(blast intro: wf_while_option_Some[OF wf_if_measure, of P b f])
1.106
1.107  text\<open>Kleene iteration starting from the empty set and assuming some finite
```