equal
deleted
inserted
replaced
136 "Rprg \<in> ((metric-`{m}) - fixedpoint) LeadsTo (metric-`(lessThan m))" |
136 "Rprg \<in> ((metric-`{m}) - fixedpoint) LeadsTo (metric-`(lessThan m))" |
137 apply (simp (no_asm) add: Diff_fixedpoint Rprg_def) |
137 apply (simp (no_asm) add: Diff_fixedpoint Rprg_def) |
138 apply (rule LeadsTo_UN, auto) |
138 apply (rule LeadsTo_UN, auto) |
139 apply (ensures_tac "asgt a b") |
139 apply (ensures_tac "asgt a b") |
140 prefer 2 apply blast |
140 prefer 2 apply blast |
141 apply (simp (no_asm_use) add: not_less_iff_le) |
141 apply (simp (no_asm_use) add: linorder_not_less) |
142 apply (drule metric_le [THEN order_antisym]) |
142 apply (drule metric_le [THEN order_antisym]) |
143 apply (auto elim: less_not_refl3 [THEN [2] rev_notE]) |
143 apply (auto elim: less_not_refl3 [THEN [2] rev_notE]) |
144 done |
144 done |
145 |
145 |
146 lemma LeadsTo_Un_fixedpoint: |
146 lemma LeadsTo_Un_fixedpoint: |