src/HOL/IMP/Hoare_Examples.thy
changeset 64851 33aab75ff423
parent 61028 99d58362eeeb
child 67406 23307fd33906
equal deleted inserted replaced
64847:54f5afc9c413 64851:33aab75ff423
     1 (* Author: Tobias Nipkow *)
     1 (* Author: Tobias Nipkow *)
     2 
     2 
     3 theory Hoare_Examples imports Hoare begin
     3 theory Hoare_Examples imports Hoare begin
       
     4 
       
     5 hide_const (open) sum
     4 
     6 
     5 text{* Summing up the first @{text x} natural numbers in variable @{text y}. *}
     7 text{* Summing up the first @{text x} natural numbers in variable @{text y}. *}
     6 
     8 
     7 fun sum :: "int \<Rightarrow> int" where
     9 fun sum :: "int \<Rightarrow> int" where
     8 "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)"