Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
authornipkow
Tue Nov 07 14:52:27 2017 +0100 (19 months ago)
changeset 670197a3724078363
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
src/HOL/IMP/Big_Step.thy
src/HOL/IMP/Compiler2.thy
src/HOL/IMP/Denotational.thy
src/HOL/IMP/Hoare_Sound_Complete.thy
src/HOL/IMP/Hoare_Total.thy
src/HOL/IMP/Hoare_Total_EX.thy
src/HOL/IMP/Hoare_Total_EX2.thy
src/HOL/IMP/Live_True.thy
src/HOL/IMP/VCG_Total_EX.thy
src/HOL/IMP/VCG_Total_EX2.thy
src/HOL/ROOT
     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.36          by (simp add: algebra_simps)
    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.59      by (auto simp add:wpt_def)
    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.22 +  Askip                  ("SKIP") |
   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