src/HOL/Boogie/Examples/Boogie_Max.thy
 changeset 33663 a84fd6385832 parent 33445 f0c78a28e18e child 34068 a78307d72e58
```     1.1 --- a/src/HOL/Boogie/Examples/Boogie_Max.thy	Fri Nov 13 15:10:28 2009 +0100
1.2 +++ b/src/HOL/Boogie/Examples/Boogie_Max.thy	Fri Nov 13 15:11:41 2009 +0100
1.3 @@ -57,14 +57,20 @@
1.4  proof (split_vc (verbose) try: fast simp)
1.5    print_cases
1.6    case L_14_5c
1.7 -  thus ?case by (metis abs_of_nonneg zabs_less_one_iff zle_linear)
1.8 +  thus ?case by (metis less_le_not_le zle_add1_eq_le zless_linear)
1.9  next
1.10    case L_14_5b
1.11 -  thus ?case by (metis less_le_not_le linorder_not_le xt1(10) zle_linear
1.13 +  thus ?case by (metis less_le_not_le xt1(10) zle_linear zless_add1_eq)
1.14  next
1.15    case L_14_5a
1.16 -  thus ?case by (metis less_le_not_le zle_add1_eq_le zless_linear)
1.17 +  note max0 = `max0 = array 0`
1.18 +  {
1.19 +    fix i :: int
1.20 +    assume "0 \<le> i \<and> i < 1"
1.21 +    hence "i = 0" by simp
1.22 +    with max0 have "array i \<le> max0" by simp
1.23 +  }
1.24 +  thus ?case by simp
1.25  qed
1.26
1.27  boogie_end
```