equal
deleted
inserted
replaced
216 assume 1: "lpfp\<^isub>c (step' \<top>) c = Some c'" |
216 assume 1: "lpfp\<^isub>c (step' \<top>) c = Some c'" |
217 have 2: "step' \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1]) |
217 have 2: "step' \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1]) |
218 have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c" |
218 have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c" |
219 by(simp add: strip_lpfpc[OF _ 1]) |
219 by(simp add: strip_lpfpc[OF _ 1]) |
220 have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')" |
220 have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')" |
221 proof(rule lfp_lowerbound[OF 3]) |
221 proof(rule lfp_lowerbound[simplified,OF 3]) |
222 show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')" |
222 show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')" |
223 proof(rule step_preserves_le[OF _ _ 3]) |
223 proof(rule step_preserves_le[OF _ _ 3]) |
224 show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp |
224 show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp |
225 show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2]) |
225 show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2]) |
226 qed |
226 qed |