equal
deleted
inserted
replaced
4 imports Abs_Int_den1 |
4 imports Abs_Int_den1 |
5 begin |
5 begin |
6 |
6 |
7 subsection "Interval Analysis" |
7 subsection "Interval Analysis" |
8 |
8 |
9 datatype ivl = I "int option" "int option" |
9 datatype_new ivl = I "int option" "int option" |
10 |
10 |
11 text{* We assume an important invariant: arithmetic operations are never |
11 text{* We assume an important invariant: arithmetic operations are never |
12 applied to empty intervals @{term"I (Some i) (Some j)"} with @{term"j < |
12 applied to empty intervals @{term"I (Some i) (Some j)"} with @{term"j < |
13 i"}. This avoids special cases. Why can we assume this? Because an empty |
13 i"}. This avoids special cases. Why can we assume this? Because an empty |
14 interval of values for a variable means that the current program point is |
14 interval of values for a variable means that the current program point is |