63 inv_begin2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and |
63 inv_begin2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and |
64 inv_begin3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and |
64 inv_begin3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and |
65 inv_begin4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
65 inv_begin4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
66 where |
66 where |
67 "inv_begin0 n (l, r) = ((n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc])) \<or> |
67 "inv_begin0 n (l, r) = ((n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc])) \<or> |
68 (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc])))" |
68 (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc])))" |
69 | "inv_begin1 n (l, r) = ((l, r) = ([], Oc \<up> n))" |
69 | "inv_begin1 n (l, r) = ((l, r) = ([], Oc \<up> n))" |
70 | "inv_begin2 n (l, r) = (\<exists> i j. i > 0 \<and> i + j = n \<and> (l, r) = (Oc \<up> i, Oc \<up> j))" |
70 | "inv_begin2 n (l, r) = (\<exists> i j. i > 0 \<and> i + j = n \<and> (l, r) = (Oc \<up> i, Oc \<up> j))" |
71 | "inv_begin3 n (l, r) = (n > 0 \<and> (l, tl r) = (Bk # Oc \<up> n, []))" |
71 | "inv_begin3 n (l, r) = (n > 0 \<and> (l, tl r) = (Bk # Oc \<up> n, []))" |
72 | "inv_begin4 n (l, r) = (n > 0 \<and> ((l, r) = (Oc \<up> n, [Bk, Oc]) \<or> (l, r) = (Oc \<up> (n - 1), [Oc, Bk, Oc])))" |
72 | "inv_begin4 n (l, r) = (n > 0 \<and> (l, r) = (Oc \<up> n, [Bk, Oc]) \<or> (l, r) = (Oc \<up> (n - 1), [Oc, Bk, Oc]))" |
73 |
73 |
74 fun inv_begin :: "nat \<Rightarrow> config \<Rightarrow> bool" |
74 fun inv_begin :: "nat \<Rightarrow> config \<Rightarrow> bool" |
75 where |
75 where |
76 "inv_begin n (s, l, r) = |
76 "inv_begin n (s, l, r) = |
77 (if s = 0 then inv_begin0 n (l, r) else |
77 (if s = 0 then inv_begin0 n (l, r) else |
81 if s = 4 then inv_begin4 n (l, r) |
81 if s = 4 then inv_begin4 n (l, r) |
82 else False)" |
82 else False)" |
83 |
83 |
84 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> |
84 lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow> |
85 \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia" |
85 \<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia" |
86 apply(rule_tac x = "Suc i" in exI, simp) |
86 by (rule_tac x = "Suc i" in exI, simp) |
87 done |
|
88 |
87 |
89 lemma inv_begin_step: |
88 lemma inv_begin_step: |
90 "\<lbrakk>inv_begin x cf; x > 0\<rbrakk> \<Longrightarrow> inv_begin x (step cf (tcopy_begin, 0))" |
89 assumes "inv_begin x cf" |
|
90 and "x > 0" |
|
91 shows "inv_begin x (step0 cf tcopy_begin)" |
|
92 using assms |
91 unfolding tcopy_begin_def |
93 unfolding tcopy_begin_def |
92 apply(case_tac cf) |
94 apply(case_tac cf) |
93 apply(auto simp: inv_begin.simps step.simps tcopy_begin_def numeral split: if_splits) |
95 apply(auto simp: inv_begin.simps step.simps tcopy_begin_def numeral split: if_splits) |
94 apply(case_tac "hd c", auto simp: inv_begin.simps) |
96 apply(case_tac "hd c", auto simp: inv_begin.simps) |
95 apply(case_tac c, simp_all) |
97 apply(case_tac c, simp_all) |
96 done |
98 done |
97 |
99 |
98 lemma inv_begin_steps: |
100 lemma inv_begin_steps: |
99 "\<lbrakk>inv_begin x (s, l, r); x > 0\<rbrakk> |
101 assumes "inv_begin x cf" |
100 \<Longrightarrow> inv_begin x (steps (s, l, r) (tcopy_begin, 0) stp)" |
102 and "x > 0" |
101 apply(induct stp, simp add: steps.simps) |
103 shows "inv_begin x (steps0 cf tcopy_begin stp)" |
|
104 apply(induct stp) |
|
105 apply(simp add: steps.simps assms) |
102 apply(auto simp: step_red) |
106 apply(auto simp: step_red) |
103 apply(rule_tac inv_begin_step, simp_all) |
107 apply(rule_tac inv_begin_step) |
|
108 apply(simp_all add: assms) |
104 done |
109 done |
105 |
110 |
106 fun begin_state :: "config \<Rightarrow> nat" |
111 fun begin_state :: "config \<Rightarrow> nat" |
107 where |
112 where |
108 "begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)" |
113 "begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)" |
134 |
139 |
135 lemma wf_begin_le: "wf begin_LE" |
140 lemma wf_begin_le: "wf begin_LE" |
136 by(auto intro:wf_inv_image simp:begin_LE_def lex_pair_def) |
141 by(auto intro:wf_inv_image simp:begin_LE_def lex_pair_def) |
137 |
142 |
138 lemma begin_halt: |
143 lemma begin_halt: |
139 "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (Suc 0, [], Oc\<up>x) tcopy_begin stp)" |
144 "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (1, [], Oc\<up>x) tcopy_begin stp)" |
140 proof(rule_tac LE = begin_LE in halt_lemma) |
145 proof(rule_tac LE = begin_LE in halt_lemma) |
141 show "wf begin_LE" by(simp add: wf_begin_le) |
146 show "wf begin_LE" by(simp add: wf_begin_le) |
142 next |
147 next |
143 assume h: "0 < x" |
148 assume h: "0 < x" |
144 show "\<forall>n. \<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow> |
149 show "\<forall>n. \<not> is_final (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow> |
145 (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), |
150 (steps (1, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), |
146 steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE" |
151 steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE" |
147 proof(rule_tac allI, rule_tac impI) |
152 proof(rule_tac allI, rule_tac impI) |
148 fix n |
153 fix n |
149 assume a: "\<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n)" |
154 assume a: "\<not> is_final (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n)" |
150 have b: "inv_begin x (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n)" |
155 have b: "inv_begin x (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n)" |
151 apply(rule_tac inv_begin_steps) |
156 apply(rule_tac inv_begin_steps) |
152 apply(simp_all add: inv_begin.simps h) |
157 apply(simp_all add: inv_begin.simps h) |
153 done |
158 done |
154 obtain s l r where c: "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) = (s, l, r)" |
159 obtain s l r where c: "(steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) = (s, l, r)" |
155 apply(case_tac "steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n", auto) |
160 apply(case_tac "steps (1, [], Oc \<up> x) (tcopy_begin, 0) n", auto) |
156 done |
161 done |
157 moreover hence "inv_begin x (s, l, r)" |
162 moreover hence "inv_begin x (s, l, r)" |
158 using c b by simp |
163 using c b by simp |
159 ultimately show "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), |
164 ultimately show "(steps (1, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), |
160 steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE" |
165 steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE" |
161 using a |
166 using a |
162 proof(simp del: inv_begin.simps) |
167 proof(simp del: inv_begin.simps) |
163 assume "inv_begin x (s, l, r)" "0 < s" |
168 assume "inv_begin x (s, l, r)" "0 < s" |
164 thus "(step (s, l, r) (tcopy_begin, 0), s, l, r) \<in> begin_LE" |
169 thus "(step (s, l, r) (tcopy_begin, 0), s, l, r) \<in> begin_LE" |
165 apply(auto simp: begin_LE_def lex_pair_def step.simps tcopy_begin_def numeral split: if_splits) |
170 apply(auto simp: begin_LE_def lex_pair_def step.simps tcopy_begin_def numeral split: if_splits) |
172 lemma begin_correct: |
177 lemma begin_correct: |
173 "0 < x \<Longrightarrow> {inv_begin1 x} tcopy_begin {inv_begin0 x}" |
178 "0 < x \<Longrightarrow> {inv_begin1 x} tcopy_begin {inv_begin0 x}" |
174 proof(rule_tac Hoare_haltI) |
179 proof(rule_tac Hoare_haltI) |
175 fix l r |
180 fix l r |
176 assume h: "0 < x" "inv_begin1 x (l, r)" |
181 assume h: "0 < x" "inv_begin1 x (l, r)" |
177 hence "\<exists> stp. is_final (steps0 (Suc 0, [], Oc \<up> x) tcopy_begin stp)" |
182 hence "\<exists> stp. is_final (steps0 (1, [], Oc \<up> x) tcopy_begin stp)" |
178 by (rule_tac begin_halt) |
183 by (rule_tac begin_halt) |
179 then obtain stp where "is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)" .. |
184 then obtain stp where "is_final (steps (1, [], Oc\<up>x) (tcopy_begin, 0) stp)" .. |
180 moreover have "inv_begin x (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)" |
185 moreover have "inv_begin x (steps (1, [], Oc\<up>x) (tcopy_begin, 0) stp)" |
181 apply(rule_tac inv_begin_steps) |
186 apply(rule_tac inv_begin_steps) |
182 using h by(simp_all add: inv_begin.simps) |
187 using h by(simp_all add: inv_begin.simps) |
183 ultimately show |
188 ultimately show |
184 "\<exists>n. is_final (steps (1, l, r) (tcopy_begin, 0) n) \<and> |
189 "\<exists>n. is_final (steps (1, l, r) (tcopy_begin, 0) n) \<and> |
185 inv_begin0 x holds_for steps (1, l, r) (tcopy_begin, 0) n" |
190 inv_begin0 x holds_for steps (1, l, r) (tcopy_begin, 0) n" |
186 using h |
191 using h |
187 apply(rule_tac x = stp in exI) |
192 apply(rule_tac x = stp in exI) |
188 apply(case_tac "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) stp)", simp add: inv_begin.simps) |
193 apply(case_tac "(steps (1, [], Oc \<up> x) (tcopy_begin, 0) stp)", simp add: inv_begin.simps) |
189 done |
194 done |
190 qed |
195 qed |
191 |
196 |
192 |
197 |
193 (* tcopy_loop *) |
198 (* tcopy_loop *) |