equal
deleted
inserted
replaced
75 text {* Now, let's prove the three hard assertions of @{text max}: *} |
75 text {* Now, let's prove the three hard assertions of @{text max}: *} |
76 |
76 |
77 boogie_vc max (examine: L_14_5c L_14_5b L_14_5a) |
77 boogie_vc max (examine: L_14_5c L_14_5b L_14_5a) |
78 proof boogie_cases |
78 proof boogie_cases |
79 case L_14_5c |
79 case L_14_5c |
80 thus ?case by (metis less_le_not_le zle_add1_eq_le zless_linear) |
80 thus ?case by (metis less_le_not_le zle_add1_eq_le less_linear) |
81 next |
81 next |
82 case L_14_5b |
82 case L_14_5b |
83 thus ?case by (metis less_le_not_le xt1(10) zle_linear zless_add1_eq) |
83 thus ?case by (metis less_le_not_le xt1(10) linorder_linear zless_add1_eq) |
84 next |
84 next |
85 case L_14_5a |
85 case L_14_5a |
86 note max0 = `max0 = array 0` |
86 note max0 = `max0 = array 0` |
87 { |
87 { |
88 fix i :: int |
88 fix i :: int |