equal
deleted
inserted
replaced
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 |
106 |
|
107 (* |
107 lemma begin_partial_correctness: |
108 lemma begin_partial_correctness: |
108 assumes "\<exists>stp. steps0 cf tcopy_begin stp = (0, l, r)" |
109 assumes "\<exists>stp. is_final (steps0 (1, [], Oc \<up> n) tcopy_begin stp)" |
|
110 shows "0 < n \<Longrightarrow> {inv_begin1 n} tcopy_begin {inv_begin0 n}" |
|
111 using assms |
|
112 apply(auto simp add: Hoare_halt_def) |
|
113 apply(rule_tac x="stp" in exI) |
|
114 apply(simp) |
|
115 apply(case_tac "steps0 (Suc 0, [], Oc \<up> n) tcopy_begin stp") |
|
116 apply(simp) |
|
117 apply(case_tac n) |
|
118 apply(simp) |
|
119 apply(simp) |
|
120 apply(case_tac nat) |
|
121 apply(simp) |
|
122 apply(simp) |
|
123 *) |
109 |
124 |
110 fun measure_begin_state :: "config \<Rightarrow> nat" |
125 fun measure_begin_state :: "config \<Rightarrow> nat" |
111 where |
126 where |
112 "measure_begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)" |
127 "measure_begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)" |
113 |
128 |