equal
deleted
inserted
replaced
125 apply blast |
125 apply blast |
126 apply (erule wf_subset) |
126 apply (erule wf_subset) |
127 apply blast |
127 apply blast |
128 done |
128 done |
129 |
129 |
|
130 text{* Proving termination: *} |
|
131 |
|
132 theorem wf_while_option_Some: |
|
133 assumes wf: "wf {(t, s). b s \<and> t = c s}" |
|
134 shows "EX t. while_option b c s = Some t" |
|
135 using wf |
|
136 apply (induct s) |
|
137 apply simp |
|
138 apply (subst while_option_unfold) |
|
139 apply simp |
|
140 done |
|
141 |
|
142 theorem measure_while_option_Some: fixes f :: "'s \<Rightarrow> nat" |
|
143 shows "(!!s. b s \<Longrightarrow> f(c s) < f s) \<Longrightarrow> EX t. while_option b c s = Some t" |
|
144 by(erule wf_while_option_Some[OF wf_if_measure]) |
|
145 |
130 |
146 |
131 end |
147 end |