author nipkow Tue Nov 07 14:52:27 2017 +0100 (17 months ago) changeset 67019 7a3724078363 parent 67018 f6aa133f9b16 child 67020 c32254ab1901 child 67036 783c901a62cb
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
 src/HOL/IMP/Abs_Int3.thy file | annotate | diff | revisions src/HOL/IMP/Big_Step.thy file | annotate | diff | revisions src/HOL/IMP/Compiler2.thy file | annotate | diff | revisions src/HOL/IMP/Denotational.thy file | annotate | diff | revisions src/HOL/IMP/Hoare_Sound_Complete.thy file | annotate | diff | revisions src/HOL/IMP/Hoare_Total.thy file | annotate | diff | revisions src/HOL/IMP/Hoare_Total_EX.thy file | annotate | diff | revisions src/HOL/IMP/Hoare_Total_EX2.thy file | annotate | diff | revisions src/HOL/IMP/Live_True.thy file | annotate | diff | revisions src/HOL/IMP/VCG_Total_EX.thy file | annotate | diff | revisions src/HOL/IMP/VCG_Total_EX2.thy file | annotate | diff | revisions src/HOL/ROOT file | annotate | diff | revisions
```     1.1 --- a/src/HOL/IMP/Abs_Int3.thy	Tue Nov 07 11:11:37 2017 +0100
1.2 +++ b/src/HOL/IMP/Abs_Int3.thy	Tue Nov 07 14:52:27 2017 +0100
1.3 @@ -187,21 +187,19 @@
1.4  shows "P p \<and> f p \<le> p"
1.5  proof-
1.6    let ?Q = "%p. P p \<and> f p \<le> p \<and> p \<le> p0"
1.7 -  { fix p assume "?Q p"
1.8 -    note P = conjunct1[OF this] and 12 = conjunct2[OF this]
1.9 +  have "?Q (p \<triangle> f p)" if Q: "?Q p" for p
1.10 +  proof auto
1.11 +    note P = conjunct1[OF Q] and 12 = conjunct2[OF Q]
1.12      note 1 = conjunct1[OF 12] and 2 = conjunct2[OF 12]
1.13      let ?p' = "p \<triangle> f p"
1.14 -    have "?Q ?p'"
1.15 -    proof auto
1.16 -      show "P ?p'" by (blast intro: P Pinv)
1.17 -      have "f ?p' \<le> f p" by(rule mono[OF `P (p \<triangle> f p)`  P narrow2_acom[OF 1]])
1.18 -      also have "\<dots> \<le> ?p'" by(rule narrow1_acom[OF 1])
1.19 -      finally show "f ?p' \<le> ?p'" .
1.20 -      have "?p' \<le> p" by (rule narrow2_acom[OF 1])
1.21 -      also have "p \<le> p0" by(rule 2)
1.22 -      finally show "?p' \<le> p0" .
1.23 -    qed
1.24 -  }
1.25 +    show "P ?p'" by (blast intro: P Pinv)
1.26 +    have "f ?p' \<le> f p" by(rule mono[OF `P (p \<triangle> f p)`  P narrow2_acom[OF 1]])
1.27 +    also have "\<dots> \<le> ?p'" by(rule narrow1_acom[OF 1])
1.28 +    finally show "f ?p' \<le> ?p'" .
1.29 +    have "?p' \<le> p" by (rule narrow2_acom[OF 1])
1.30 +    also have "p \<le> p0" by(rule 2)
1.31 +    finally show "?p' \<le> p0" .
1.32 +  qed
1.33    thus ?thesis
1.34      using while_option_rule[where P = ?Q, OF _ assms(6)[simplified iter_narrow_def]]
1.35      by (blast intro: assms(4,5) le_refl)
```
```     2.1 --- a/src/HOL/IMP/Big_Step.thy	Tue Nov 07 11:11:37 2017 +0100
2.2 +++ b/src/HOL/IMP/Big_Step.thy	Tue Nov 07 14:52:27 2017 +0100
2.3 @@ -178,8 +178,9 @@
2.4  proof -
2.5    -- "to show the equivalence, we look at the derivation tree for"
2.6    -- "each side and from that construct a derivation tree for the other side"
2.7 -  { fix s t assume "(?w, s) \<Rightarrow> t"
2.8 -    hence  "(?iw, s) \<Rightarrow> t"
2.9 +  have "(?iw, s) \<Rightarrow> t" if assm: "(?w, s) \<Rightarrow> t" for s t
2.10 +  proof -
2.11 +    from assm show ?thesis
2.12      proof cases --"rule inversion on \<open>(?w, s) \<Rightarrow> t\<close>"
2.13        case WhileFalse
2.14        thus ?thesis by blast
2.15 @@ -193,11 +194,12 @@
2.16        -- "then the whole @{text IF}"
2.17        with `bval b s` show ?thesis by (rule IfTrue)
2.18      qed
2.19 -  }
2.20 +  qed
2.21    moreover
2.22    -- "now the other direction:"
2.23 -  { fix s t assume "(?iw, s) \<Rightarrow> t"
2.24 -    hence "(?w, s) \<Rightarrow> t"
2.25 +  have "(?w, s) \<Rightarrow> t" if assm: "(?iw, s) \<Rightarrow> t" for s t
2.26 +  proof -
2.27 +    from assm show ?thesis
2.28      proof cases --"rule inversion on \<open>(?iw, s) \<Rightarrow> t\<close>"
2.29        case IfFalse
2.30        hence "s = t" using `(?iw, s) \<Rightarrow> t` by blast
2.31 @@ -212,7 +214,7 @@
2.32        with `bval b s`
2.33        show ?thesis by (rule WhileTrue)
2.34      qed
2.35 -  }
2.36 +  qed
2.37    ultimately
2.38    show ?thesis by blast
2.39  qed
```
```     3.1 --- a/src/HOL/IMP/Compiler2.thy	Tue Nov 07 11:11:37 2017 +0100
3.2 +++ b/src/HOL/IMP/Compiler2.thy	Tue Nov 07 14:52:27 2017 +0100
3.3 @@ -108,10 +108,11 @@
3.4    "succs (x#xs) n = isuccs x n \<union> succs xs (1+n)" (is "_ = ?x \<union> ?xs")
3.5  proof
3.6    let ?isuccs = "\<lambda>p P n i::int. 0 \<le> i \<and> i < size P \<and> p \<in> isuccs (P!!i) (n+i)"
3.7 -  { fix p assume "p \<in> succs (x#xs) n"
3.8 -    then obtain i::int where isuccs: "?isuccs p (x#xs) n i"
3.9 +  have "p \<in> ?x \<union> ?xs" if assm: "p \<in> succs (x#xs) n" for p
3.10 +  proof -
3.11 +    from assm obtain i::int where isuccs: "?isuccs p (x#xs) n i"
3.12        unfolding succs_def by auto
3.13 -    have "p \<in> ?x \<union> ?xs"
3.14 +    show ?thesis
3.15      proof cases
3.16        assume "i = 0" with isuccs show ?thesis by simp
3.17      next
3.18 @@ -121,11 +122,12 @@
3.19        hence "p \<in> ?xs" unfolding succs_def by blast
3.20        thus ?thesis ..
3.21      qed
3.22 -  }
3.23 +  qed
3.24    thus "succs (x#xs) n \<subseteq> ?x \<union> ?xs" ..
3.25 -
3.26 -  { fix p assume "p \<in> ?x \<or> p \<in> ?xs"
3.27 -    hence "p \<in> succs (x#xs) n"
3.28 +
3.29 +  have "p \<in> succs (x#xs) n" if assm: "p \<in> ?x \<or> p \<in> ?xs" for p
3.30 +  proof -
3.31 +    from assm show ?thesis
3.32      proof
3.33        assume "p \<in> ?x" thus ?thesis by (fastforce simp: succs_def)
3.34      next
3.35 @@ -136,7 +138,7 @@
3.37        thus ?thesis unfolding succs_def by blast
3.38      qed
3.39 -  }
3.40 +  qed
3.41    thus "?x \<union> ?xs \<subseteq> succs (x#xs) n" by blast
3.42  qed
3.43
3.44 @@ -300,20 +302,19 @@
3.45
3.46    note split_paired_Ex [simp del]
3.47
3.48 -  { assume "j0 \<in> {0 ..< size c}"
3.49 -    with j0 j rest c
3.50 -    have ?case
3.51 +  have ?case if assm: "j0 \<in> {0 ..< size c}"
3.52 +  proof -
3.53 +    from assm j0 j rest c show ?case
3.54        by (fastforce dest!: Suc.IH intro!: exec_Suc)
3.55 -  } moreover {
3.56 -    assume "j0 \<notin> {0 ..< size c}"
3.57 -    moreover
3.58 +  qed
3.59 +  moreover
3.60 +  have ?case if assm: "j0 \<notin> {0 ..< size c}"
3.61 +  proof -
3.62      from c j0 have "j0 \<in> succs c 0"
3.63        by (auto dest: succs_iexec1 simp: exec1_def simp del: iexec.simps)
3.64 -    ultimately
3.65 -    have "j0 \<in> exits c" by (simp add: exits_def)
3.66 -    with c j0 rest
3.67 -    have ?case by fastforce
3.68 -  }
3.69 +    with assm have "j0 \<in> exits c" by (simp add: exits_def)
3.70 +    with c j0 rest show ?case by fastforce
3.71 +  qed
3.72    ultimately
3.73    show ?case by cases
3.74  qed
3.75 @@ -560,14 +561,16 @@
3.76    show ?case
3.77    proof (induction n arbitrary: s rule: nat_less_induct)
3.78      case (1 n)
3.79 -
3.80 -    { assume "\<not> bval b s"
3.81 -      with "1.prems"
3.82 -      have ?case
3.83 -        by simp
3.84 -           (fastforce dest!: bcomp_exec_n bcomp_split simp: exec_n_simps)
3.85 -    } moreover {
3.86 -      assume b: "bval b s"
3.87 +
3.88 +    have ?case if assm: "\<not> bval b s"
3.89 +    proof -
3.90 +      from assm "1.prems"
3.91 +      show ?case
3.92 +        by simp (fastforce dest!: bcomp_split simp: exec_n_simps)
3.93 +    qed
3.94 +    moreover
3.95 +    have ?case if b: "bval b s"
3.96 +    proof -
3.97        let ?c0 = "WHILE b DO c"
3.98        let ?cs = "ccomp ?c0"
3.99        let ?bs = "bcomp b False (size (ccomp c) + 1)"
3.100 @@ -579,7 +582,7 @@
3.101          k:  "k \<le> n"
3.102          by (fastforce dest!: bcomp_split)
3.103
3.104 -      have ?case
3.105 +      show ?case
3.106        proof cases
3.107          assume "ccomp c = []"
3.108          with cs k
3.109 @@ -612,7 +615,7 @@
3.110          ultimately
3.111          show ?case using b by blast
3.112        qed
3.113 -    }
3.114 +    qed
3.115      ultimately show ?case by cases
3.116    qed
3.117  qed
```
```     4.1 --- a/src/HOL/IMP/Denotational.thy	Tue Nov 07 11:11:37 2017 +0100
4.2 +++ b/src/HOL/IMP/Denotational.thy	Tue Nov 07 14:52:27 2017 +0100
4.3 @@ -90,9 +90,13 @@
4.4  lemma chain_iterates: fixes f :: "'a set \<Rightarrow> 'a set"
4.5    assumes "mono f" shows "chain(\<lambda>n. (f^^n) {})"
4.6  proof-
4.7 -  { fix n have "(f ^^ n) {} \<subseteq> (f ^^ Suc n) {}" using assms
4.8 -    by(induction n) (auto simp: mono_def) }
4.9 -  thus ?thesis by(auto simp: chain_def)
4.10 +  have "(f ^^ n) {} \<subseteq> (f ^^ Suc n) {}" for n
4.11 +  proof (induction n)
4.12 +    case 0 show ?case by simp
4.13 +  next
4.14 +    case (Suc n) thus ?case using assms by (auto simp: mono_def)
4.15 +  qed
4.16 +  thus ?thesis by(auto simp: chain_def assms)
4.17  qed
4.18
4.19  theorem lfp_if_cont:
4.20 @@ -112,8 +116,9 @@
4.21      finally show "f ?U \<subseteq> ?U" by simp
4.22    qed
4.23  next
4.24 -  { fix n p assume "f p \<subseteq> p"
4.25 -    have "(f^^n){} \<subseteq> p"
4.26 +  have "(f^^n){} \<subseteq> p" if "f p \<subseteq> p" for n p
4.27 +  proof -
4.28 +    show ?thesis
4.29      proof(induction n)
4.30        case 0 show ?case by simp
4.31      next
4.32 @@ -121,7 +126,7 @@
4.33        from monoD[OF mono_if_cont[OF assms] Suc] `f p \<subseteq> p`
4.34        show ?case by simp
4.35      qed
4.36 -  }
4.37 +  qed
4.38    thus "?U \<subseteq> lfp f" by(auto simp: lfp_def)
4.39  qed
4.40
```
```     5.1 --- a/src/HOL/IMP/Hoare_Sound_Complete.thy	Tue Nov 07 11:11:37 2017 +0100
5.2 +++ b/src/HOL/IMP/Hoare_Sound_Complete.thy	Tue Nov 07 14:52:27 2017 +0100
5.3 @@ -11,15 +11,13 @@
5.4  lemma hoare_sound: "\<turnstile> {P}c{Q}  \<Longrightarrow>  \<Turnstile> {P}c{Q}"
5.5  proof(induction rule: hoare.induct)
5.6    case (While P b c)
5.7 -  { fix s t
5.8 -    have "(WHILE b DO c,s) \<Rightarrow> t  \<Longrightarrow>  P s  \<Longrightarrow>  P t \<and> \<not> bval b t"
5.9 -    proof(induction "WHILE b DO c" s t rule: big_step_induct)
5.10 -      case WhileFalse thus ?case by blast
5.11 -    next
5.12 -      case WhileTrue thus ?case
5.13 -        using While.IH unfolding hoare_valid_def by blast
5.14 -    qed
5.15 -  }
5.16 +  have "(WHILE b DO c,s) \<Rightarrow> t  \<Longrightarrow>  P s  \<Longrightarrow>  P t \<and> \<not> bval b t" for s t
5.17 +  proof(induction "WHILE b DO c" s t rule: big_step_induct)
5.18 +    case WhileFalse thus ?case by blast
5.19 +  next
5.20 +    case WhileTrue thus ?case
5.21 +      using While.IH unfolding hoare_valid_def by blast
5.22 +  qed
5.23    thus ?case unfolding hoare_valid_def by blast
5.24  qed (auto simp: hoare_valid_def)
5.25
```
```     6.1 --- a/src/HOL/IMP/Hoare_Total.thy	Tue Nov 07 11:11:37 2017 +0100
6.2 +++ b/src/HOL/IMP/Hoare_Total.thy	Tue Nov 07 14:52:27 2017 +0100
6.3 @@ -95,14 +95,10 @@
6.4  theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q}  \<Longrightarrow>  \<Turnstile>\<^sub>t {P}c{Q}"
6.5  proof(unfold hoare_tvalid_def, induction rule: hoaret.induct)
6.6    case (While P b T c)
6.7 -  {
6.8 -    fix s n
6.9 -    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"
6.10 -    proof(induction "n" arbitrary: s rule: less_induct)
6.11 -      case (less n)
6.12 -      thus ?case by (metis While.IH WhileFalse WhileTrue)
6.13 -    qed
6.14 -  }
6.15 +  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" for s n
6.16 +  proof(induction "n" arbitrary: s rule: less_induct)
6.17 +    case (less n) thus ?case by (metis While.IH WhileFalse WhileTrue)
6.18 +  qed
6.19    thus ?case by auto
6.20  next
6.21    case If thus ?case by auto blast
6.22 @@ -176,12 +172,13 @@
6.23    case (While b c)
6.24    let ?w = "WHILE b DO c"
6.25    let ?T = "Its b c"
6.26 -  have "\<forall>s. wp\<^sub>t ?w Q s \<longrightarrow> wp\<^sub>t ?w Q s \<and> (\<exists>n. Its b c s n)"
6.27 +  have 1: "\<forall>s. wp\<^sub>t ?w Q s \<longrightarrow> wp\<^sub>t ?w Q s \<and> (\<exists>n. Its b c s n)"
6.28      unfolding wpt_def by (metis WHILE_Its)
6.29 -  moreover
6.30 -  { fix n
6.31 -    let ?R = "\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'<n. ?T s' n')"
6.32 -    { fix s t assume "bval b s" and "?T s n" and "(?w, s) \<Rightarrow> t" and "Q t"
6.33 +  let ?R = "\<lambda>n s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'<n. ?T s' n')"
6.34 +  have "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> ?T s n \<longrightarrow> wp\<^sub>t c (?R n) s" for n
6.35 +  proof -
6.36 +    have "wp\<^sub>t c (?R n) s" if "bval b s" and "?T s n" and "(?w, s) \<Rightarrow> t" and "Q t" for s t
6.37 +    proof -
6.38        from `bval b s` and `(?w, s) \<Rightarrow> t` obtain s' where
6.39          "(c,s) \<Rightarrow> s'" "(?w,s') \<Rightarrow> t" by auto
6.40        from `(?w, s') \<Rightarrow> t` obtain n' where "?T s' n'"
6.41 @@ -189,16 +186,16 @@
6.42        with `bval b s` and `(c, s) \<Rightarrow> s'` have "?T s (Suc n')" by (rule Its_Suc)
6.43        with `?T s n` have "n = Suc n'" by (rule Its_fun)
6.44        with `(c,s) \<Rightarrow> s'` and `(?w,s') \<Rightarrow> t` and `Q t` and `?T s' n'`
6.45 -      have "wp\<^sub>t c ?R s" by (auto simp: wpt_def)
6.46 -    }
6.47 -    hence "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> ?T s n \<longrightarrow> wp\<^sub>t c ?R s"
6.48 +      show ?thesis by (auto simp: wpt_def)
6.49 +    qed
6.50 +    thus ?thesis
6.51        unfolding wpt_def by auto
6.52        (* by (metis WhileE Its_Suc Its_fun WHILE_Its lessI) *)
6.53 -    note strengthen_pre[OF this While.IH]
6.54 -  } note hoaret.While[OF this]
6.55 -  moreover have "\<forall>s. wp\<^sub>t ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s"
6.56 +  qed
6.57 +  note 2 = hoaret.While[OF strengthen_pre[OF this While.IH]]
6.58 +  have "\<forall>s. wp\<^sub>t ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s"
6.60 -  ultimately show ?case by (rule conseq)
6.61 +  with 1 2 show ?case by (rule conseq)
6.62  qed
6.63
6.64
```
```     7.1 --- a/src/HOL/IMP/Hoare_Total_EX.thy	Tue Nov 07 11:11:37 2017 +0100
7.2 +++ b/src/HOL/IMP/Hoare_Total_EX.thy	Tue Nov 07 14:52:27 2017 +0100
7.3 @@ -55,16 +55,13 @@
7.4  theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q}  \<Longrightarrow>  \<Turnstile>\<^sub>t {P}c{Q}"
7.5  proof(unfold hoare_tvalid_def, induction rule: hoaret.induct)
7.6    case (While P c b)
7.7 -  {
7.8 -    fix n s
7.9 -    have "\<lbrakk> P n s \<rbrakk> \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P 0 t"
7.10 -    proof(induction "n" arbitrary: s)
7.11 -      case 0 thus ?case using While.hyps(3) WhileFalse by blast
7.12 -    next
7.13 -      case (Suc n)
7.14 -      thus ?case by (meson While.IH While.hyps(2) WhileTrue)
7.15 -    qed
7.16 -  }
7.17 +  have "P n s \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P 0 t" for n s
7.18 +  proof(induction "n" arbitrary: s)
7.19 +    case 0 thus ?case using While.hyps(3) WhileFalse by blast
7.20 +  next
7.21 +    case Suc
7.22 +    thus ?case by (meson While.IH While.hyps(2) WhileTrue)
7.23 +  qed
7.24    thus ?case by auto
7.25  next
7.26    case If thus ?case by auto blast
7.27 @@ -125,11 +122,11 @@
7.28    have c3: "\<forall>s. wpw b c 0 Q s \<longrightarrow> Q s" by simp
7.29    have w2: "\<forall>n s. wpw b c (Suc n) Q s \<longrightarrow> bval b s" by simp
7.30    have w3: "\<forall>s. wpw b c 0 Q s \<longrightarrow> \<not> bval b s" by simp
7.31 -  { fix n
7.32 -    have 1: "\<forall>s. wpw b c (Suc n) Q s \<longrightarrow> (\<exists>t. (c, s) \<Rightarrow> t \<and> wpw b c n Q t)"
7.33 -      by simp
7.34 -    note strengthen_pre[OF 1 While.IH[of "wpw b c n Q", unfolded wpt_def]]
7.35 -  }
7.36 +  have "\<turnstile>\<^sub>t {wpw b c (Suc n) Q} c {wpw b c n Q}" for n
7.37 +  proof -
7.38 +    have *: "\<forall>s. wpw b c (Suc n) Q s \<longrightarrow> (\<exists>t. (c, s) \<Rightarrow> t \<and> wpw b c n Q t)" by simp
7.39 +    show ?thesis by(rule strengthen_pre[OF * While.IH[of "wpw b c n Q", unfolded wpt_def]])
7.40 +  qed
7.41    from conseq[OF c1 hoaret.While[OF this w2 w3] c3]
7.42    show ?case .
7.43  qed
```
```     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/HOL/IMP/Hoare_Total_EX2.thy	Tue Nov 07 14:52:27 2017 +0100
8.3 @@ -0,0 +1,193 @@
8.4 +(* Author: Tobias Nipkow *)
8.5 +
8.6 +theory Hoare_Total_EX2
8.7 +imports Hoare
8.8 +begin
8.9 +
8.10 +subsubsection "Hoare Logic for Total Correctness --- With Logical Variables"
8.11 +
8.12 +text{* This is the standard set of rules that you find in many publications.
8.13 +In the while-rule, a logical variable is needed to remember the pre-value
8.14 +of the variant (an expression that decreases by one with each iteration).
8.15 +In this theory, logical variables are modeled explicitly.
8.16 +A simpler (but not quite as flexible) approach is found in theory \<open>Hoare_Total_EX\<close>:
8.17 +pre and post-condition are connected via a universally quantified HOL variable. *}
8.18 +
8.19 +type_synonym lvname = string
8.20 +type_synonym assn2 = "(lvname \<Rightarrow> nat) \<Rightarrow> state \<Rightarrow> bool"
8.21 +
8.22 +definition hoare_tvalid :: "assn2 \<Rightarrow> com \<Rightarrow> assn2 \<Rightarrow> bool"
8.23 +  ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where
8.24 +"\<Turnstile>\<^sub>t {P}c{Q}  \<longleftrightarrow>  (\<forall>l s. P l s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q l t))"
8.25 +
8.26 +inductive
8.27 +  hoaret :: "assn2 \<Rightarrow> com \<Rightarrow> assn2 \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50)
8.28 +where
8.29 +
8.30 +Skip:  "\<turnstile>\<^sub>t {P} SKIP {P}"  |
8.31 +
8.32 +Assign:  "\<turnstile>\<^sub>t {\<lambda>l s. P l (s[a/x])} x::=a {P}"  |
8.33 +
8.34 +Seq: "\<lbrakk> \<turnstile>\<^sub>t {P\<^sub>1} c\<^sub>1 {P\<^sub>2}; \<turnstile>\<^sub>t {P\<^sub>2} c\<^sub>2 {P\<^sub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^sub>1} c\<^sub>1;;c\<^sub>2 {P\<^sub>3}" |
8.35 +
8.36 +If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>l s. P l s \<and> bval b s} c\<^sub>1 {Q}; \<turnstile>\<^sub>t {\<lambda>l s. P l s \<and> \<not> bval b s} c\<^sub>2 {Q} \<rbrakk>
8.37 +  \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" |
8.38 +
8.39 +While:
8.40 +  "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>l. P (l(x := Suc(l(x))))} c {P};
8.41 +     \<forall>l s. l x > 0 \<and> P l s \<longrightarrow> bval b s;
8.42 +     \<forall>l s. l x = 0 \<and> P l s \<longrightarrow> \<not> bval b s \<rbrakk>
8.43 +   \<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>l s. \<exists>n. P (l(x:=n)) s} WHILE b DO c {\<lambda>l s. P (l(x := 0)) s}" |
8.44 +
8.45 +conseq: "\<lbrakk> \<forall>l s. P' l s \<longrightarrow> P l s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>l s. Q l s \<longrightarrow> Q' l s  \<rbrakk> \<Longrightarrow>
8.46 +           \<turnstile>\<^sub>t {P'}c{Q'}"
8.47 +
8.48 +text{* Building in the consequence rule: *}
8.49 +
8.50 +lemma strengthen_pre:
8.51 +  "\<lbrakk> \<forall>l s. P' l s \<longrightarrow> P l s;  \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}"
8.52 +by (metis conseq)
8.53 +
8.54 +lemma weaken_post:
8.55 +  "\<lbrakk> \<turnstile>\<^sub>t {P} c {Q};  \<forall>l s. Q l s \<longrightarrow> Q' l s \<rbrakk> \<Longrightarrow>  \<turnstile>\<^sub>t {P} c {Q'}"
8.56 +by (metis conseq)
8.57 +
8.58 +lemma Assign': "\<forall>l s. P l s \<longrightarrow> Q l (s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}"
8.59 +by (simp add: strengthen_pre[OF _ Assign])
8.60 +
8.61 +text{* The soundness theorem: *}
8.62 +
8.63 +theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q}  \<Longrightarrow>  \<Turnstile>\<^sub>t {P}c{Q}"
8.64 +proof(unfold hoare_tvalid_def, induction rule: hoaret.induct)
8.65 +  case (While P x c b)
8.66 +  have "\<lbrakk> l x = n; P l s \<rbrakk> \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P (l(x := 0)) t" for n l s
8.67 +  proof(induction "n" arbitrary: l s)
8.68 +    case 0 thus ?case using While.hyps(3) WhileFalse
8.69 +      by (metis fun_upd_triv)
8.70 +  next
8.71 +    case Suc
8.72 +    thus ?case using While.IH While.hyps(2) WhileTrue
8.73 +      by (metis fun_upd_same fun_upd_triv fun_upd_upd zero_less_Suc)
8.74 +  qed
8.75 +  thus ?case by fastforce
8.76 +next
8.77 +  case If thus ?case by auto blast
8.78 +qed fastforce+
8.79 +
8.80 +
8.81 +definition wpt :: "com \<Rightarrow> assn2 \<Rightarrow> assn2" ("wp\<^sub>t") where
8.82 +"wp\<^sub>t c Q  =  (\<lambda>l s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q l t)"
8.83 +
8.84 +lemma [simp]: "wp\<^sub>t SKIP Q = Q"
8.85 +by(auto intro!: ext simp: wpt_def)
8.86 +
8.87 +lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>l s. Q l (s(x := aval e s)))"
8.88 +by(auto intro!: ext simp: wpt_def)
8.89 +
8.90 +lemma wpt_Seq[simp]: "wp\<^sub>t (c\<^sub>1;;c\<^sub>2) Q = wp\<^sub>t c\<^sub>1 (wp\<^sub>t c\<^sub>2 Q)"
8.91 +by (auto simp: wpt_def fun_eq_iff)
8.92 +
8.93 +lemma [simp]:
8.94 + "wp\<^sub>t (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q = (\<lambda>l s. wp\<^sub>t (if bval b s then c\<^sub>1 else c\<^sub>2) Q l s)"
8.95 +by (auto simp: wpt_def fun_eq_iff)
8.96 +
8.97 +
8.98 +text{* Function @{text wpw} computes the weakest precondition of a While-loop
8.99 +that is unfolded a fixed number of times. *}
8.100 +
8.101 +fun wpw :: "bexp \<Rightarrow> com \<Rightarrow> nat \<Rightarrow> assn2 \<Rightarrow> assn2" where
8.102 +"wpw b c 0 Q l s = (\<not> bval b s \<and> Q l s)" |
8.103 +"wpw b c (Suc n) Q l s = (bval b s \<and> (\<exists>s'. (c,s) \<Rightarrow> s' \<and>  wpw b c n Q l s'))"
8.104 +
8.105 +lemma WHILE_Its:
8.106 +  "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> Q l t \<Longrightarrow> \<exists>n. wpw b c n Q l s"
8.107 +proof(induction "WHILE b DO c" s t arbitrary: l rule: big_step_induct)
8.108 +  case WhileFalse thus ?case using wpw.simps(1) by blast
8.109 +next
8.110 +  case WhileTrue show ?case
8.111 +    using wpw.simps(2) WhileTrue(1,2) WhileTrue(5)[OF WhileTrue(6)] by blast
8.112 +qed
8.113 +
8.114 +definition support :: "assn2 \<Rightarrow> string set" where
8.115 +"support P = {x. \<exists>l1 l2 s. (\<forall>y. y \<noteq> x \<longrightarrow> l1 y = l2 y) \<and> P l1 s \<noteq> P l2 s}"
8.116 +
8.117 +lemma support_wpt: "support (wp\<^sub>t c Q) \<subseteq> support Q"
8.118 +by(simp add: support_def wpt_def) blast
8.119 +
8.120 +
8.121 +lemma support_wpw0: "support (wpw b c n Q) \<subseteq> support Q"
8.122 +proof(induction n)
8.123 +  case 0 show ?case by (simp add: support_def) blast
8.124 +next
8.125 +  case Suc
8.126 +  have 1: "support (\<lambda>l s. A s \<and> B l s) \<subseteq> support B" for A B
8.127 +    by(auto simp: support_def)
8.128 +  have 2: "support (\<lambda>l s. \<exists>s'. A s s' \<and> B l s') \<subseteq> support B" for A B
8.129 +    by(auto simp: support_def) blast+
8.130 +  from Suc 1 2 show ?case by simp (meson order_trans)
8.131 +qed
8.132 +
8.133 +lemma support_wpw_Un:
8.134 +  "support (%l. wpw b c (l x) Q l) \<subseteq> insert x (UN n. support(wpw b c n Q))"
8.135 +using support_wpw0[of b c _ Q]
8.136 +apply(auto simp add: support_def subset_iff)
8.137 +apply metis
8.138 +apply metis
8.139 +done
8.140 +
8.141 +lemma support_wpw: "support (%l. wpw b c (l x) Q l) \<subseteq> insert x (support Q)"
8.142 +using support_wpw0[of b c _ Q] support_wpw_Un[of b c _ Q]
8.143 +by blast
8.144 +
8.145 +lemma assn2_lupd: "x \<notin> support Q \<Longrightarrow> Q (l(x:=n)) = Q l"
8.146 +by(simp add: support_def fun_upd_other fun_eq_iff)
8.147 +  (metis (no_types, lifting) fun_upd_def)
8.148 +
8.149 +abbreviation "new Q \<equiv> SOME x. x \<notin> support Q"
8.150 +
8.151 +lemma wpw_lupd: "x \<notin> support Q \<Longrightarrow> wpw b c n Q (l(x := u)) = wpw b c n Q l"
8.152 +by(induction n) (auto simp: assn2_lupd fun_eq_iff)
8.153 +
8.154 +lemma wpt_is_pre: "finite(support Q) \<Longrightarrow> \<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"
8.155 +proof (induction c arbitrary: Q)
8.156 +  case SKIP show ?case by (auto intro:hoaret.Skip)
8.157 +next
8.158 +  case Assign show ?case by (auto intro:hoaret.Assign)
8.159 +next
8.160 +  case (Seq c1 c2) show ?case
8.161 +    by (auto intro:hoaret.Seq Seq finite_subset[OF support_wpt])
8.162 +next
8.163 +  case If thus ?case by (auto intro:hoaret.If hoaret.conseq)
8.164 +next
8.165 +  case (While b c)
8.166 +  let ?x = "new Q"
8.167 +  have "\<exists>x. x \<notin> support Q" using While.prems infinite_UNIV_listI
8.168 +    using ex_new_if_finite by blast
8.169 +  hence [simp]: "?x \<notin> support Q" by (rule someI_ex)
8.170 +  let ?w = "WHILE b DO c"
8.171 +  have fsup: "finite (support (\<lambda>l. wpw b c (l x) Q l))" for x
8.172 +    using finite_subset[OF support_wpw] While.prems by simp
8.173 +  have c1: "\<forall>l s. wp\<^sub>t ?w Q l s \<longrightarrow> (\<exists>n. wpw b c n Q l s)"
8.174 +    unfolding wpt_def by (metis WHILE_Its)
8.175 +  have c2: "\<forall>l s. l ?x = 0 \<and> wpw b c (l ?x) Q l s \<longrightarrow> \<not> bval b s"
8.176 +    by (simp cong: conj_cong)
8.177 +  have w2: "\<forall>l s. 0 < l ?x \<and> wpw b c (l ?x) Q l s \<longrightarrow> bval b s"
8.178 +    by (auto simp: gr0_conv_Suc cong: conj_cong)
8.179 +  have 1: "\<forall>l s. wpw b c (Suc(l ?x)) Q l s \<longrightarrow>
8.180 +                  (\<exists>t. (c, s) \<Rightarrow> t \<and> wpw b c (l ?x) Q l t)"
8.181 +    by simp
8.182 +  have *: "\<turnstile>\<^sub>t {\<lambda>l. wpw b c (Suc (l ?x)) Q l} c {\<lambda>l. wpw b c (l ?x) Q l}"
8.183 +    by(rule strengthen_pre[OF 1
8.184 +          While.IH[of "\<lambda>l. wpw b c (l ?x) Q l", unfolded wpt_def, OF fsup]])
8.185 +  show ?case
8.186 +  apply(rule conseq[OF _ hoaret.While[OF _ w2 c2]])
8.187 +    apply (simp_all add: c1 * assn2_lupd wpw_lupd del: wpw.simps(2))
8.188 +  done
8.189 +qed
8.190 +
8.191 +theorem hoaret_complete: "finite(support Q) \<Longrightarrow> \<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}"
8.192 +apply(rule strengthen_pre[OF _ wpt_is_pre])
8.193 +apply(auto simp: hoare_tvalid_def wpt_def)
8.194 +done
8.195 +
8.196 +end
```
```     9.1 --- a/src/HOL/IMP/Live_True.thy	Tue Nov 07 11:11:37 2017 +0100
9.2 +++ b/src/HOL/IMP/Live_True.thy	Tue Nov 07 14:52:27 2017 +0100
9.3 @@ -15,18 +15,18 @@
9.4
9.5  lemma L_mono: "mono (L c)"
9.6  proof-
9.7 -  { fix X Y have "X \<subseteq> Y \<Longrightarrow> L c X \<subseteq> L c Y"
9.8 -    proof(induction c arbitrary: X Y)
9.9 -      case (While b c)
9.10 -      show ?case
9.11 -      proof(simp, rule lfp_mono)
9.12 -        fix Z show "vars b \<union> X \<union> L c Z \<subseteq> vars b \<union> Y \<union> L c Z"
9.13 -          using While by auto
9.14 -      qed
9.15 -    next
9.16 -      case If thus ?case by(auto simp: subset_iff)
9.17 -    qed auto
9.18 -  } thus ?thesis by(rule monoI)
9.19 +  have "X \<subseteq> Y \<Longrightarrow> L c X \<subseteq> L c Y" for X Y
9.20 +  proof(induction c arbitrary: X Y)
9.21 +    case (While b c)
9.22 +    show ?case
9.23 +    proof(simp, rule lfp_mono)
9.24 +      fix Z show "vars b \<union> X \<union> L c Z \<subseteq> vars b \<union> Y \<union> L c Z"
9.25 +        using While by auto
9.26 +    qed
9.27 +  next
9.28 +    case If thus ?case by(auto simp: subset_iff)
9.29 +  qed auto
9.30 +  thus ?thesis by(rule monoI)
9.31  qed
9.32
9.33  lemma mono_union_L:
```
```    10.1 --- a/src/HOL/IMP/VCG_Total_EX.thy	Tue Nov 07 11:11:37 2017 +0100
10.2 +++ b/src/HOL/IMP/VCG_Total_EX.thy	Tue Nov 07 14:52:27 2017 +0100
10.3 @@ -1,7 +1,7 @@
10.4  (* Author: Tobias Nipkow *)
10.5
10.6  theory VCG_Total_EX
10.7 -imports "~~/src/HOL/IMP/Hoare_Total_EX"
10.8 +imports Hoare_Total_EX
10.9  begin
10.10
10.11  subsection "Verification Conditions for Total Correctness"
```
```    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/HOL/IMP/VCG_Total_EX2.thy	Tue Nov 07 14:52:27 2017 +0100
11.3 @@ -0,0 +1,134 @@
11.4 +(* Author: Tobias Nipkow *)
11.5 +
11.6 +theory VCG_Total_EX2
11.7 +imports Hoare_Total_EX2
11.8 +begin
11.9 +
11.10 +subsection "Verification Conditions for Total Correctness"
11.11 +
11.12 +text \<open>
11.13 +Theory \<open>VCG_Total_EX\<close> conatins a VCG built on top of a Hoare logic without logical variables.
11.14 +As a result the completeness proof runs into a problem. This theory uses a Hoare logic
11.15 +with logical variables and proves soundness and completeness.
11.16 +\<close>
11.17 +
11.18 +text{* Annotated commands: commands where loops are annotated with
11.19 +invariants. *}
11.20 +
11.21 +datatype acom =
11.23 +  Aassign vname aexp     ("(_ ::= _)" [1000, 61] 61) |
11.24 +  Aseq   acom acom       ("_;;/ _"  [60, 61] 60) |
11.25 +  Aif bexp acom acom     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61) |
11.26 +  Awhile assn2 lvname bexp acom
11.27 +    ("({_'/_}/ WHILE _/ DO _)"  [0, 0, 0, 61] 61)
11.28 +
11.29 +notation com.SKIP ("SKIP")
11.30 +
11.31 +text{* Strip annotations: *}
11.32 +
11.33 +fun strip :: "acom \<Rightarrow> com" where
11.34 +"strip SKIP = SKIP" |
11.35 +"strip (x ::= a) = (x ::= a)" |
11.36 +"strip (C\<^sub>1;; C\<^sub>2) = (strip C\<^sub>1;; strip C\<^sub>2)" |
11.37 +"strip (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = (IF b THEN strip C\<^sub>1 ELSE strip C\<^sub>2)" |
11.38 +"strip ({_/_} WHILE b DO C) = (WHILE b DO strip C)"
11.39 +
11.40 +text{* Weakest precondition from annotated commands: *}
11.41 +
11.42 +fun pre :: "acom \<Rightarrow> assn2 \<Rightarrow> assn2" where
11.43 +"pre SKIP Q = Q" |
11.44 +"pre (x ::= a) Q = (\<lambda>l s. Q l (s(x := aval a s)))" |
11.45 +"pre (C\<^sub>1;; C\<^sub>2) Q = pre C\<^sub>1 (pre C\<^sub>2 Q)" |
11.46 +"pre (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q =
11.47 +  (\<lambda>l s. if bval b s then pre C\<^sub>1 Q l s else pre C\<^sub>2 Q l s)" |
11.48 +"pre ({I/x} WHILE b DO C) Q = (\<lambda>l s. EX n. I (l(x:=n)) s)"
11.49 +
11.50 +text{* Verification condition: *}
11.51 +
11.52 +fun vc :: "acom \<Rightarrow> assn2 \<Rightarrow> bool" where
11.53 +"vc SKIP Q = True" |
11.54 +"vc (x ::= a) Q = True" |
11.55 +"vc (C\<^sub>1;; C\<^sub>2) Q = (vc C\<^sub>1 (pre C\<^sub>2 Q) \<and> vc C\<^sub>2 Q)" |
11.56 +"vc (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q = (vc C\<^sub>1 Q \<and> vc C\<^sub>2 Q)" |
11.57 +"vc ({I/x} WHILE b DO C) Q =
11.58 +  (\<forall>l s. (I (l(x:=Suc(l x))) s \<longrightarrow> pre C I l s) \<and>
11.59 +       (l x > 0 \<and> I l s \<longrightarrow> bval b s) \<and>
11.60 +       (I (l(x := 0)) s \<longrightarrow> \<not> bval b s \<and> Q l s) \<and>
11.61 +       vc C I)"
11.62 +
11.63 +lemma vc_sound: "vc C Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C Q} strip C {Q}"
11.64 +proof(induction C arbitrary: Q)
11.65 +  case (Awhile I x b C)
11.66 +  show ?case
11.67 +  proof(simp, rule weaken_post[OF While[of I x]], goal_cases)
11.68 +    case 1 show ?case
11.69 +      using Awhile.IH[of "I"] Awhile.prems by (auto intro: strengthen_pre)
11.70 +  next
11.71 +    case 3 show ?case
11.72 +      using Awhile.prems by (simp) (metis fun_upd_triv)
11.73 +  qed (insert Awhile.prems, auto)
11.74 +qed (auto intro: conseq Seq If simp: Skip Assign)
11.75 +
11.76 +
11.77 +text{* Completeness: *}
11.78 +
11.79 +lemma pre_mono:
11.80 +  "\<forall>l s. P l s \<longrightarrow> P' l s \<Longrightarrow> pre C P l s \<Longrightarrow> pre C P' l s"
11.81 +proof (induction C arbitrary: P P' l s)
11.82 +  case Aseq thus ?case by simp metis
11.83 +qed simp_all
11.84 +
11.85 +lemma vc_mono:
11.86 +  "\<forall>l s. P l s \<longrightarrow> P' l s \<Longrightarrow> vc C P \<Longrightarrow> vc C P'"
11.87 +proof(induction C arbitrary: P P')
11.88 +  case Aseq thus ?case by simp (metis pre_mono)
11.89 +qed simp_all
11.90 +
11.91 +lemma vc_complete:
11.92 + "\<turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<exists>C. strip C = c \<and> vc C Q \<and> (\<forall>l s. P l s \<longrightarrow> pre C Q l s)"
11.93 +  (is "_ \<Longrightarrow> \<exists>C. ?G P c Q C")
11.94 +proof (induction rule: hoaret.induct)
11.95 +  case Skip
11.96 +  show ?case (is "\<exists>C. ?C C")
11.97 +  proof show "?C Askip" by simp qed
11.98 +next
11.99 +  case (Assign P a x)
11.100 +  show ?case (is "\<exists>C. ?C C")
11.101 +  proof show "?C(Aassign x a)" by simp qed
11.102 +next
11.103 +  case (Seq P c1 Q c2 R)
11.104 +  from Seq.IH obtain C1 where ih1: "?G P c1 Q C1" by blast
11.105 +  from Seq.IH obtain C2 where ih2: "?G Q c2 R C2" by blast
11.106 +  show ?case (is "\<exists>C. ?C C")
11.107 +  proof
11.108 +    show "?C(Aseq C1 C2)"
11.109 +      using ih1 ih2 by (fastforce elim!: pre_mono vc_mono)
11.110 +  qed
11.111 +next
11.112 +  case (If P b c1 Q c2)
11.113 +  from If.IH obtain C1 where ih1: "?G (\<lambda>l s. P l s \<and> bval b s) c1 Q C1"
11.114 +    by blast
11.115 +  from If.IH obtain C2 where ih2: "?G (\<lambda>l s. P l s \<and> \<not>bval b s) c2 Q C2"
11.116 +    by blast
11.117 +  show ?case (is "\<exists>C. ?C C")
11.118 +  proof
11.119 +    show "?C(Aif b C1 C2)" using ih1 ih2 by simp
11.120 +  qed
11.121 +next
11.122 +  case (While P x c b)
11.123 +  from While.IH obtain C where
11.124 +    ih: "?G (\<lambda>l s. P (l(x:=Suc(l x))) s \<and> bval b s) c P C"
11.125 +    by blast
11.126 +  show ?case (is "\<exists>C. ?C C")
11.127 +  proof
11.128 +    have "vc ({P/x} WHILE b DO C) (\<lambda>l. P (l(x := 0)))"
11.129 +      using ih While.hyps(2,3)
11.130 +      by simp (metis fun_upd_same zero_less_Suc)
11.131 +    thus "?C(Awhile P x b C)" using ih by simp
11.132 + qed
11.133 +next
11.134 +  case conseq thus ?case by(fast elim!: pre_mono vc_mono)
11.135 +qed
11.136 +
11.137 +end
```
```    12.1 --- a/src/HOL/ROOT	Tue Nov 07 11:11:37 2017 +0100
12.2 +++ b/src/HOL/ROOT	Tue Nov 07 14:52:27 2017 +0100
12.3 @@ -153,6 +153,7 @@
12.4      VCG
12.5      Hoare_Total
12.6      VCG_Total_EX
12.7 +    VCG_Total_EX2
12.8      Collecting1
12.9      Collecting_Examples
12.10      Abs_Int_Tests
```