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.12 -    zless_add1_eq)
    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