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.34        by (simp add: funpow_swap1)
    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.44        by (simp add: funpow_swap1)
    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