src/HOL/IMP/Hoare_Examples.thy
 changeset 67406 23307fd33906 parent 64851 33aab75ff423 child 68776 403dd13cf6e9
equal inserted replaced
`     2 `
`     2 `
`     3 theory Hoare_Examples imports Hoare begin`
`     3 theory Hoare_Examples imports Hoare begin`
`     4 `
`     4 `
`     5 hide_const (open) sum`
`     5 hide_const (open) sum`
`     6 `
`     6 `
`     7 text{* Summing up the first @{text x} natural numbers in variable @{text y}. *}`
`     7 text\<open>Summing up the first @{text x} natural numbers in variable @{text y}.\<close>`
`     8 `
`     8 `
`     9 fun sum :: "int \<Rightarrow> int" where`
`     9 fun sum :: "int \<Rightarrow> int" where`
`    10 "sum i = (if i \<le> 0 then 0 else sum (i - 1) + i)"`
`    10 "sum i = (if i \<le> 0 then 0 else sum (i - 1) + i)"`
`    11 `
`    11 `
`    12 lemma sum_simps[simp]:`
`    12 lemma sum_simps[simp]:`
`    20   WHILE Less (N 0) (V ''x'')`
`    20   WHILE Less (N 0) (V ''x'')`
`    21   DO (''y'' ::= Plus (V ''y'') (V ''x'');;`
`    21   DO (''y'' ::= Plus (V ''y'') (V ''x'');;`
`    22       ''x'' ::= Plus (V ''x'') (N (- 1)))"`
`    22       ''x'' ::= Plus (V ''x'') (N (- 1)))"`
`    23 `
`    23 `
`    24 `
`    24 `
`    25 subsubsection{* Proof by Operational Semantics *}`
`    25 subsubsection\<open>Proof by Operational Semantics\<close>`
`    26 `
`    26 `
`    27 text{* The behaviour of the loop is proved by induction: *}`
`    27 text\<open>The behaviour of the loop is proved by induction:\<close>`
`    28 `
`    28 `
`    29 lemma while_sum:`
`    29 lemma while_sum:`
`    30   "(wsum, s) \<Rightarrow> t \<Longrightarrow> t ''y'' = s ''y'' + sum(s ''x'')"`
`    30   "(wsum, s) \<Rightarrow> t \<Longrightarrow> t ''y'' = s ''y'' + sum(s ''x'')"`
`    31 apply(induction wsum s t rule: big_step_induct)`
`    31 apply(induction wsum s t rule: big_step_induct)`
`    32 apply(auto)`
`    32 apply(auto)`
`    33 done`
`    33 done`
`    34 `
`    34 `
`    35 text{* We were lucky that the proof was automatic, except for the`
`    35 text\<open>We were lucky that the proof was automatic, except for the`
`    36 induction. In general, such proofs will not be so easy. The automation is`
`    36 induction. In general, such proofs will not be so easy. The automation is`
`    37 partly due to the right inversion rules that we set up as automatic`
`    37 partly due to the right inversion rules that we set up as automatic`
`    38 elimination rules that decompose big-step premises.`
`    38 elimination rules that decompose big-step premises.`
`    39 `
`    39 `
`    40 Now we prefix the loop with the necessary initialization: *}`
`    40 Now we prefix the loop with the necessary initialization:\<close>`
`    41 `
`    41 `
`    42 lemma sum_via_bigstep:`
`    42 lemma sum_via_bigstep:`
`    43   assumes "(''y'' ::= N 0;; wsum, s) \<Rightarrow> t"`
`    43   assumes "(''y'' ::= N 0;; wsum, s) \<Rightarrow> t"`
`    44   shows "t ''y'' = sum (s ''x'')"`
`    44   shows "t ''y'' = sum (s ''x'')"`
`    45 proof -`
`    45 proof -`
`    46   from assms have "(wsum,s(''y'':=0)) \<Rightarrow> t" by auto`
`    46   from assms have "(wsum,s(''y'':=0)) \<Rightarrow> t" by auto`
`    47   from while_sum[OF this] show ?thesis by simp`
`    47   from while_sum[OF this] show ?thesis by simp`
`    48 qed`
`    48 qed`
`    49 `
`    49 `
`    50 `
`    50 `
`    51 subsubsection{* Proof by Hoare Logic *}`
`    51 subsubsection\<open>Proof by Hoare Logic\<close>`
`    52 `
`    52 `
`    53 text{* Note that we deal with sequences of commands from right to left,`
`    53 text\<open>Note that we deal with sequences of commands from right to left,`
`    54 pulling back the postcondition towards the precondition. *}`
`    54 pulling back the postcondition towards the precondition.\<close>`
`    55 `
`    55 `
`    56 lemma "\<turnstile> {\<lambda>s. s ''x'' = n} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = sum n}"`
`    56 lemma "\<turnstile> {\<lambda>s. s ''x'' = n} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = sum n}"`
`    57 apply(rule Seq)`
`    57 apply(rule Seq)`
`    58  prefer 2`
`    58  prefer 2`
`    59  apply(rule While' [where P = "\<lambda>s. (s ''y'' = sum n - sum(s ''x''))"])`
`    59  apply(rule While' [where P = "\<lambda>s. (s ''y'' = sum n - sum(s ''x''))"])`
`    65  apply simp`
`    65  apply simp`
`    66 apply(rule Assign')`
`    66 apply(rule Assign')`
`    67 apply simp`
`    67 apply simp`
`    68 done`
`    68 done`
`    69 `
`    69 `
`    70 text{* The proof is intentionally an apply script because it merely composes`
`    70 text\<open>The proof is intentionally an apply script because it merely composes`
`    71 the rules of Hoare logic. Of course, in a few places side conditions have to`
`    71 the rules of Hoare logic. Of course, in a few places side conditions have to`
`    72 be proved. But since those proofs are 1-liners, a structured proof is`
`    72 be proved. But since those proofs are 1-liners, a structured proof is`
`    73 overkill. In fact, we shall learn later that the application of the Hoare`
`    73 overkill. In fact, we shall learn later that the application of the Hoare`
`    74 rules can be automated completely and all that is left for the user is to`
`    74 rules can be automated completely and all that is left for the user is to`
`    75 provide the loop invariants and prove the side-conditions. *}`
`    75 provide the loop invariants and prove the side-conditions.\<close>`
`    76 `
`    76 `
`    77 end`
`    77 end`