| changeset 92 | b9d0dd18c81e |
| parent 91 | 2068654bdf54 |
| child 93 | f2bda6ba4952 |
| 91:2068654bdf54 | 92:b9d0dd18c81e |
|---|---|
47 where |
47 where |
48 "tcopy_end \<equiv> [(L, 0), (R, 2), (W1, 3), (L, 4), |
48 "tcopy_end \<equiv> [(L, 0), (R, 2), (W1, 3), (L, 4), |
49 (R, 2), (R, 2), (L, 5), (W0, 4), |
49 (R, 2), (R, 2), (L, 5), (W0, 4), |
50 (R, 0), (L, 5)]" |
50 (R, 0), (L, 5)]" |
51 |
51 |
52 idefinition |
52 definition |
53 tcopy :: "instr list" |
53 tcopy :: "instr list" |
54 where |
54 where |
55 "tcopy \<equiv> (tcopy_begin |+| tcopy_loop) |+| tcopy_end" |
55 "tcopy \<equiv> (tcopy_begin |+| tcopy_loop) |+| tcopy_end" |
56 |
56 |
57 |
57 |
135 lemma wf_begin_le: "wf init_LE" |
135 lemma wf_begin_le: "wf init_LE" |
136 by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def) |
136 by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def) |
137 |
137 |
138 lemma init_halt: |
138 lemma init_halt: |
139 "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (Suc 0, [], Oc\<up>x) tcopy_begin stp)" |
139 "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (Suc 0, [], Oc\<up>x) tcopy_begin stp)" |
140 proof(rule_tac LE = init_LE in halt_lemma) |
140 proof(rule_tac LE = init_LE in halt_lemma) |
141 show "wf init_LE" by(simp add: wf_begin_le) |
141 show "wf init_LE" by(simp add: wf_begin_le) |
142 next |
142 next |
143 assume h: "0 < x" |
143 assume h: "0 < x" |
144 show "\<forall>n. \<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow> |
144 show "\<forall>n. \<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow> |
145 (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), |
145 (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), |