src/HOL/IMP/Abs_Int3.thy
 changeset 55357 1dd39517e1ce parent 53015 a1119cf551e8 child 55599 6535c537b243
equal inserted replaced
55356:3ea8ace6bc8a 55357:1dd39517e1ce
`   594 text{* Widening is increasing by assumption, but @{prop"x \<le> f x"} is not an invariant of widening.`
`   594 text{* Widening is increasing by assumption, but @{prop"x \<le> f x"} is not an invariant of widening.`
`   595 It can already be lost after the first step: *}`
`   595 It can already be lost after the first step: *}`
`   596 `
`   596 `
`   597 lemma assumes "!!x y::'a::wn. x \<le> y \<Longrightarrow> f x \<le> f y"`
`   597 lemma assumes "!!x y::'a::wn. x \<le> y \<Longrightarrow> f x \<le> f y"`
`   598 and "x \<le> f x" and "\<not> f x \<le> x" shows "x \<nabla> f x \<le> f(x \<nabla> f x)"`
`   598 and "x \<le> f x" and "\<not> f x \<le> x" shows "x \<nabla> f x \<le> f(x \<nabla> f x)"`
`   599 nitpick[card = 3, expect = genuine, show_consts]`
`   599 nitpick[card = 3, expect = genuine, show_consts, timeout = 120]`
`   600 (*`
`   600 (*`
`   601 1 < 2 < 3,`
`   601 1 < 2 < 3,`
`   602 f x = 2,`
`   602 f x = 2,`
`   603 x widen y = 3 -- guarantees termination with top=3`
`   603 x widen y = 3 -- guarantees termination with top=3`
`   604 x = 1`
`   604 x = 1`
`   611 In the following model, Kleene iteration goes from 0 to the least pfp`
`   611 In the following model, Kleene iteration goes from 0 to the least pfp`
`   612 in one step but widening takes 2 steps to reach a strictly larger pfp: *}`
`   612 in one step but widening takes 2 steps to reach a strictly larger pfp: *}`
`   613 lemma assumes "!!x y::'a::wn. x \<le> y \<Longrightarrow> f x \<le> f y"`
`   613 lemma assumes "!!x y::'a::wn. x \<le> y \<Longrightarrow> f x \<le> f y"`
`   614 and "x \<le> f x" and "\<not> f x \<le> x" and "f(f x) \<le> f x"`
`   614 and "x \<le> f x" and "\<not> f x \<le> x" and "f(f x) \<le> f x"`
`   615 shows "f(x \<nabla> f x) \<le> x \<nabla> f x"`
`   615 shows "f(x \<nabla> f x) \<le> x \<nabla> f x"`
`   616 nitpick[card = 4, expect = genuine, show_consts]`
`   616 nitpick[card = 4, expect = genuine, show_consts, timeout = 120]`
`   617 (*`
`   617 (*`
`   618 `
`   618 `
`   619    0 < 1 < 2 < 3`
`   619    0 < 1 < 2 < 3`
`   620 f: 1   1   3   3`
`   620 f: 1   1   3   3`
`   621 `
`   621 `