src/HOL/Hoare/HoareAbort.thy
changeset 34940 3e80eab831a1
parent 32149 ef59550a55d3
child 35054 a5db9779b026
equal deleted inserted replaced
34939:44294cfecb1d 34940:3e80eab831a1
     1 (*  Title:      HOL/Hoare/HoareAbort.thy
     1 (*  Title:      HOL/Hoare/HoareAbort.thy
     2     ID:         $Id$
       
     3     Author:     Leonor Prensa Nieto & Tobias Nipkow
     2     Author:     Leonor Prensa Nieto & Tobias Nipkow
     4     Copyright   2003 TUM
     3     Copyright   2003 TUM
     5 
     4 
     6 Like Hoare.thy, but with an Abort statement for modelling run time errors.
     5 Like Hoare.thy, but with an Abort statement for modelling run time errors.
     7 *)
     6 *)
   259 syntax
   258 syntax
   260   guarded_com :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(2_ \<rightarrow>/ _)" 71)
   259   guarded_com :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(2_ \<rightarrow>/ _)" 71)
   261   array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70,65] 61)
   260   array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70,65] 61)
   262 translations
   261 translations
   263   "P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
   262   "P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
   264   "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := list_update a i v)"
   263   "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
   265   (* reverse translation not possible because of duplicate "a" *)
   264   (* reverse translation not possible because of duplicate "a" *)
   266 
   265 
   267 text{* Note: there is no special syntax for guarded array access. Thus
   266 text{* Note: there is no special syntax for guarded array access. Thus
   268 you must write @{text"j < length a \<rightarrow> a[i] := a!j"}. *}
   267 you must write @{text"j < length a \<rightarrow> a[i] := a!j"}. *}
   269 
   268