equal
deleted
inserted
replaced
101 apply(simp add: assms) |
101 apply(simp add: assms) |
102 apply(auto simp del: steps.simps) |
102 apply(auto simp del: steps.simps) |
103 apply(rule_tac inv_begin_step) |
103 apply(rule_tac inv_begin_step) |
104 apply(simp_all add: assms) |
104 apply(simp_all add: assms) |
105 done |
105 done |
|
106 |
|
107 lemma begin_partial_correctness: |
|
108 assumes "\<exists>stp. steps0 cf tcopy_begin stp = (0, l, r)" |
106 |
109 |
107 fun measure_begin_state :: "config \<Rightarrow> nat" |
110 fun measure_begin_state :: "config \<Rightarrow> nat" |
108 where |
111 where |
109 "measure_begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)" |
112 "measure_begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)" |
110 |
113 |