equal
deleted
inserted
replaced
124 |
124 |
125 lemma metric_less [intro!]: "~ s x ==> metric (s(x:=True)) < metric s" |
125 lemma metric_less [intro!]: "~ s x ==> metric (s(x:=True)) < metric s" |
126 by (erule Suc_metric [THEN subst], blast) |
126 by (erule Suc_metric [THEN subst], blast) |
127 |
127 |
128 lemma metric_le: "metric (s(y:=s x | s y)) \<le> metric s" |
128 lemma metric_le: "metric (s(y:=s x | s y)) \<le> metric s" |
129 apply (case_tac "s x --> s y") |
129 by (cases "s x --> s y") (auto intro: less_imp_le simp add: fun_upd_idem) |
130 apply (auto intro: less_imp_le simp add: fun_upd_idem) |
|
131 done |
|
132 |
130 |
133 lemma LeadsTo_Diff_fixedpoint: |
131 lemma LeadsTo_Diff_fixedpoint: |
134 "Rprg \<in> ((metric-`{m}) - fixedpoint) LeadsTo (metric-`(lessThan m))" |
132 "Rprg \<in> ((metric-`{m}) - fixedpoint) LeadsTo (metric-`(lessThan m))" |
135 apply (simp (no_asm) add: Diff_fixedpoint Rprg_def) |
133 apply (simp (no_asm) add: Diff_fixedpoint Rprg_def) |
136 apply (rule LeadsTo_UN, auto) |
134 apply (rule LeadsTo_UN, auto) |