1.1 --- a/src/HOL/IMP/HoareT.thy	Thu May 30 13:59:20 2013 +1000
     1.2 +++ b/src/HOL/IMP/HoareT.thy	Thu May 30 08:27:51 2013 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (* Author: Tobias Nipkow *)
     1.5  
     1.6 -theory HoareT imports Hoare_Sound_Complete begin
     1.7 +theory HoareT imports Hoare_Sound_Complete Hoare_Examples begin
     1.8  
     1.9  subsection "Hoare Logic for Total Correctness"
    1.10  
    1.11 @@ -26,8 +26,8 @@
    1.12  If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s} c\<^isub>1 {Q}; \<turnstile>\<^sub>t {\<lambda>s. P s \<and> \<not> bval b s} c\<^isub>2 {Q} \<rbrakk>
    1.13    \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}" |
    1.14  While:
    1.15 -  "\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> T n s} c {\<lambda>s. P s \<and> (\<exists>n'. T n' s \<and> n' < n)} \<rbrakk>
    1.16 -   \<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> (\<exists>n. T n s)} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}" |
    1.17 +  "\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> T s n} c {\<lambda>s. P s \<and> (\<exists>n'. T s n' \<and> n' < n)} \<rbrakk>
    1.18 +   \<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> (\<exists>n. T s n)} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}" |
    1.19  conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s  \<rbrakk> \<Longrightarrow>
    1.20             \<turnstile>\<^sub>t {P'}c{Q'}"
    1.21  
    1.22 @@ -47,37 +47,30 @@
    1.23  by (simp add: strengthen_pre[OF _ Assign])
    1.24  
    1.25  lemma While':
    1.26 -assumes "\<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> T n s} c {\<lambda>s. P s \<and> (\<exists>n'. T n' s \<and> n' < n)}"
    1.27 +assumes "\<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> T s n} c {\<lambda>s. P s \<and> (\<exists>n'. T s n' \<and> n' < n)}"
    1.28      and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"
    1.29 -shows "\<turnstile>\<^sub>t {\<lambda>s. P s \<and> (\<exists>n. T n s)} WHILE b DO c {Q}"
    1.30 +shows "\<turnstile>\<^sub>t {\<lambda>s. P s \<and> (\<exists>n. T s n)} WHILE b DO c {Q}"
    1.31  by(blast intro: assms(1) weaken_post[OF While assms(2)])
    1.32  
    1.33  lemma While_fun:
    1.34    "\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> f s = n} c {\<lambda>s. P s \<and> f s < n}\<rbrakk>
    1.35     \<Longrightarrow> \<turnstile>\<^sub>t {P} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}"
    1.36 -  by (rule While [where T="\<lambda>n s. f s = n", simplified])
    1.37 +  by (rule While [where T="\<lambda>s n. f s = n", simplified])
    1.38  
    1.39  text{* Our standard example: *}
    1.40  
    1.41 -abbreviation "w n ==
    1.42 -  WHILE Less (V ''y'') (N n)
    1.43 -  DO ( ''y'' ::= Plus (V ''y'') (N 1);; ''x'' ::= Plus (V ''x'') (V ''y'') )"
    1.44 -
    1.45 -lemma "\<turnstile>\<^sub>t {\<lambda>s. 0 \<le> n} ''x'' ::= N 0;; ''y'' ::= N 0;; w n {\<lambda>s. s ''x'' = \<Sum>{1..n}}"
    1.46 +lemma "\<turnstile>\<^sub>t {\<lambda>s. s ''x'' = i} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = sum i}"
    1.47  apply(rule Seq)
    1.48 -prefer 2
    1.49 -apply(rule While'
    1.50 -  [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n"
    1.51 -   and T = "\<lambda>n' s. n' = nat (n - s ''y'')"])
    1.52 -apply(rule Seq)
    1.53 -prefer 2
    1.54 -apply(rule Assign)
    1.55 -apply(rule Assign')
    1.56 -apply (simp add: atLeastAtMostPlus1_int_conv algebra_simps)
    1.57 -apply clarsimp
    1.58 -apply(rule Seq)
    1.59 -prefer 2
    1.60 -apply(rule Assign)
    1.61 + prefer 2
    1.62 + apply(rule While' [where P = "\<lambda>s. (s ''y'' = sum i - sum(s ''x''))"
    1.63 +    and T = "\<lambda>s n. n = nat(s ''x'')"])
    1.64 +   apply(rule Seq)
    1.65 +   prefer 2
    1.66 +   apply(rule Assign)
    1.67 +  apply(rule Assign')
    1.68 +  apply simp
    1.69 +  apply(simp add: minus_numeral_simps(1)[symmetric] del: minus_numeral_simps)
    1.70 + apply(simp)
    1.71  apply(rule Assign')
    1.72  apply simp
    1.73  done
    1.74 @@ -90,7 +83,7 @@
    1.75    case (While P b T c)
    1.76    {
    1.77      fix s n
    1.78 -    have "\<lbrakk> P s; T n s \<rbrakk> \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t"
    1.79 +    have "\<lbrakk> P s; T s n \<rbrakk> \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t"
    1.80      proof(induction "n" arbitrary: s rule: less_induct)
    1.81        case (less n)
    1.82        thus ?case by (metis While(2) WhileFalse WhileTrue)
    1.83 @@ -168,25 +161,25 @@
    1.84  next
    1.85    case (While b c)
    1.86    let ?w = "WHILE b DO c"
    1.87 -  let ?T = "\<lambda>n s. Its b c s n"
    1.88 +  let ?T = "Its b c"
    1.89    have "\<forall>s. wp\<^sub>t (WHILE b DO c) Q s \<longrightarrow> wp\<^sub>t (WHILE b DO c) Q s \<and> (\<exists>n. Its b c s n)"
    1.90      unfolding wpt_def by (metis WHILE_Its)
    1.91    moreover
    1.92    { fix n
    1.93      { fix s t
    1.94 -      assume "bval b s" "?T n s" "(?w, s) \<Rightarrow> t" "Q t"
    1.95 +      assume "bval b s" "?T s n" "(?w, s) \<Rightarrow> t" "Q t"
    1.96        from `bval b s` `(?w, s) \<Rightarrow> t` obtain s' where
    1.97          "(c,s) \<Rightarrow> s'" "(?w,s') \<Rightarrow> t" by auto      
    1.98 -      from `(?w, s') \<Rightarrow> t` obtain n'' where "?T n'' s'" by (blast dest: WHILE_Its)
    1.99 +      from `(?w, s') \<Rightarrow> t` obtain n'' where "?T s' n''" by (blast dest: WHILE_Its)
   1.100        with `bval b s` `(c, s) \<Rightarrow> s'`
   1.101 -      have "?T (Suc n'') s" by (rule Its_Suc)
   1.102 -      with `?T n s` have "n = Suc n''" by (rule Its_fun)
   1.103 -      with `(c,s) \<Rightarrow> s'` `(?w,s') \<Rightarrow> t` `Q t` `?T n'' s'`
   1.104 -      have "wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'. ?T n' s' \<and> n' < n)) s"
   1.105 +      have "?T s (Suc n'')" by (rule Its_Suc)
   1.106 +      with `?T s n` have "n = Suc n''" by (rule Its_fun)
   1.107 +      with `(c,s) \<Rightarrow> s'` `(?w,s') \<Rightarrow> t` `Q t` `?T s' n''`
   1.108 +      have "wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'. ?T s' n' \<and> n' < n)) s"
   1.109          by (auto simp: wpt_def)
   1.110      } 
   1.111 -    hence "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> ?T n s \<longrightarrow>
   1.112 -              wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'. ?T n' s' \<and> n' < n)) s"
   1.113 +    hence "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> ?T s n \<longrightarrow>
   1.114 +              wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'. ?T s' n' \<and> n' < n)) s"
   1.115        unfolding wpt_def by auto
   1.116        (* by (metis WhileE Its_Suc Its_fun WHILE_Its lessI) *) 
   1.117      note strengthen_pre[OF this While]