90 and "x > 0" |
82 and "x > 0" |
91 shows "inv_begin x (step0 cf tcopy_begin)" |
83 shows "inv_begin x (step0 cf tcopy_begin)" |
92 using assms |
84 using assms |
93 unfolding tcopy_begin_def |
85 unfolding tcopy_begin_def |
94 apply(case_tac cf) |
86 apply(case_tac cf) |
95 apply(auto simp: inv_begin.simps step.simps tcopy_begin_def numeral split: if_splits) |
87 apply(auto simp: numeral split: if_splits) |
96 apply(case_tac "hd c", auto simp: inv_begin.simps) |
88 apply(case_tac "hd c") |
97 apply(case_tac c, simp_all) |
89 apply(auto) |
|
90 apply(case_tac c) |
|
91 apply(simp_all) |
98 done |
92 done |
99 |
93 |
100 lemma inv_begin_steps: |
94 lemma inv_begin_steps: |
101 assumes "inv_begin x cf" |
95 assumes "inv_begin x cf" |
102 and "x > 0" |
96 and "x > 0" |
103 shows "inv_begin x (steps0 cf tcopy_begin stp)" |
97 shows "inv_begin x (steps0 cf tcopy_begin stp)" |
104 apply(induct stp) |
98 apply(induct stp) |
105 apply(simp add: steps.simps assms) |
99 apply(simp add: assms) |
106 apply(auto simp: step_red) |
100 apply(auto simp del: steps.simps) |
107 apply(rule_tac inv_begin_step) |
101 apply(rule_tac inv_begin_step) |
108 apply(simp_all add: assms) |
102 apply(simp_all add: assms) |
109 done |
103 done |
110 |
104 |
111 fun begin_state :: "config \<Rightarrow> nat" |
105 fun measure_begin_state :: "config \<Rightarrow> nat" |
112 where |
106 where |
113 "begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)" |
107 "measure_begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)" |
114 |
108 |
115 fun begin_step :: "config \<Rightarrow> nat" |
109 fun measure_begin_step :: "config \<Rightarrow> nat" |
116 where |
110 where |
117 "begin_step (s, l, r) = |
111 "measure_begin_step (s, l, r) = |
118 (if s = 2 then length r else |
112 (if s = 2 then length r else |
119 if s = 3 then (if r = [] \<or> r = [Bk] then 1 else 0) else |
113 if s = 3 then (if r = [] \<or> r = [Bk] then 1 else 0) else |
120 if s = 4 then length l |
114 if s = 4 then length l |
121 else 0)" |
115 else 0)" |
122 |
116 |
123 fun begin_measure :: "config \<Rightarrow> nat \<times> nat" |
117 definition |
124 where |
118 "begin_LE = measures [measure_begin_state, measure_begin_step]" |
125 "begin_measure c = (begin_state c, begin_step c)" |
|
126 |
|
127 |
|
128 definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set" |
|
129 where |
|
130 "lex_pair \<equiv> less_than <*lex*> less_than" |
|
131 |
|
132 definition begin_LE :: "(config \<times> config) set" |
|
133 where |
|
134 "begin_LE \<equiv> (inv_image lex_pair begin_measure)" |
|
135 |
119 |
136 lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]" |
120 lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]" |
137 by (case_tac r, auto, case_tac a, auto) |
121 by (case_tac r, auto, case_tac a, auto) |
138 |
|
139 |
|
140 lemma wf_begin_le: "wf begin_LE" |
|
141 by(auto intro:wf_inv_image simp:begin_LE_def lex_pair_def) |
|
142 |
122 |
143 lemma begin_halt: |
123 lemma begin_halt: |
144 "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (1, [], Oc\<up>x) tcopy_begin stp)" |
124 "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (1, [], Oc\<up>x) tcopy_begin stp)" |
145 proof(rule_tac LE = begin_LE in halt_lemma) |
125 proof(rule_tac LE = begin_LE in halt_lemma) |
146 show "wf begin_LE" by(simp add: wf_begin_le) |
126 show "wf begin_LE" unfolding begin_LE_def by (auto) |
147 next |
127 next |
148 assume h: "0 < x" |
128 assume h: "0 < x" |
149 show "\<forall>n. \<not> is_final (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow> |
129 show "\<forall>n. \<not> is_final (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow> |
150 (steps (1, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), |
130 (steps (1, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), |
151 steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE" |
131 steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE" |
162 moreover hence "inv_begin x (s, l, r)" |
142 moreover hence "inv_begin x (s, l, r)" |
163 using c b by simp |
143 using c b by simp |
164 ultimately show "(steps (1, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), |
144 ultimately show "(steps (1, [], Oc \<up> x) (tcopy_begin, 0) (Suc n), |
165 steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE" |
145 steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE" |
166 using a |
146 using a |
167 proof(simp del: inv_begin.simps) |
147 proof(simp del: inv_begin.simps step.simps steps.simps) |
168 assume "inv_begin x (s, l, r)" "0 < s" |
148 assume "inv_begin x (s, l, r)" "0 < s" |
169 thus "(step (s, l, r) (tcopy_begin, 0), s, l, r) \<in> begin_LE" |
149 thus "(step (s, l, r) (tcopy_begin, 0), s, l, r) \<in> begin_LE" |
170 apply(auto simp: begin_LE_def lex_pair_def step.simps tcopy_begin_def numeral split: if_splits) |
150 apply(auto simp: begin_LE_def step.simps tcopy_begin_def numeral split: if_splits) |
171 apply(case_tac r, auto, case_tac a, auto) |
151 apply(case_tac r, auto, case_tac a, auto) |
172 done |
152 done |
173 qed |
153 qed |
174 qed |
154 qed |
175 qed |
155 qed |
475 else if s = 4 then length r |
462 else if s = 4 then length r |
476 else if s = 5 then length l |
463 else if s = 5 then length l |
477 else if s = 6 then length l |
464 else if s = 6 then length l |
478 else 0)" |
465 else 0)" |
479 |
466 |
480 definition lex_triple :: |
|
481 "((nat \<times> (nat \<times> nat)) \<times> (nat \<times> (nat \<times> nat))) set" |
|
482 where |
|
483 "lex_triple \<equiv> less_than <*lex*> lex_pair" |
|
484 |
|
485 lemma wf_lex_triple: "wf lex_triple" |
|
486 by (auto intro:wf_lex_prod simp:lex_triple_def lex_pair_def) |
|
487 |
|
488 fun loop_measure :: "config \<Rightarrow> nat \<times> nat \<times> nat" |
|
489 where |
|
490 "loop_measure c = |
|
491 (loop_stage c, loop_state c, loop_step c)" |
|
492 |
|
493 definition loop_LE :: "(config \<times> config) set" |
467 definition loop_LE :: "(config \<times> config) set" |
494 where |
468 where |
495 "loop_LE \<equiv> (inv_image lex_triple loop_measure)" |
469 "loop_LE = measures [loop_stage, loop_state, loop_step]" |
496 |
470 |
497 lemma wf_loop_le: "wf loop_LE" |
471 lemma wf_loop_le: "wf loop_LE" |
498 by (auto intro:wf_inv_image simp: loop_LE_def wf_lex_triple) |
472 unfolding loop_LE_def |
|
473 by (auto) |
499 |
474 |
500 lemma [simp]: "inv_loop2 x ([], b) = False" |
475 lemma [simp]: "inv_loop2 x ([], b) = False" |
501 by (auto simp: inv_loop2.simps) |
476 by (auto simp: inv_loop2.simps) |
502 |
477 |
503 lemma [simp]: "inv_loop2 x (l', []) = False" |
478 lemma [simp]: "inv_loop2 x (l', []) = False" |
613 apply(simp) |
588 apply(simp) |
614 done |
589 done |
615 hence "(step(s', l', r') (tcopy_loop, 0), s', l', r') \<in> loop_LE" |
590 hence "(step(s', l', r') (tcopy_loop, 0), s', l', r') \<in> loop_LE" |
616 using h |
591 using h |
617 apply(case_tac r', case_tac [2] a) |
592 apply(case_tac r', case_tac [2] a) |
618 apply(auto simp: inv_loop.simps step.simps tcopy_loop_def |
593 apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral loop_LE_def split: if_splits) |
619 numeral loop_LE_def lex_triple_def lex_pair_def split: if_splits) |
|
620 done |
594 done |
621 thus "(steps (Suc 0, l, r) (tcopy_loop, 0) (Suc n), |
595 thus "(steps (Suc 0, l, r) (tcopy_loop, 0) (Suc n), |
622 steps (Suc 0, l, r) (tcopy_loop, 0) n) \<in> loop_LE" |
596 steps (Suc 0, l, r) (tcopy_loop, 0) n) \<in> loop_LE" |
623 using d |
597 using d |
624 apply(simp add: step_red) |
598 apply(simp add: step_red) |
831 else if s = 5 then length l |
805 else if s = 5 then length l |
832 else if s = 2 then 1 |
806 else if s = 2 then 1 |
833 else if s = 3 then 0 |
807 else if s = 3 then 0 |
834 else 0)" |
808 else 0)" |
835 |
809 |
836 fun end_measure :: "config \<Rightarrow> nat \<times> nat \<times> nat" |
|
837 where |
|
838 "end_measure c = |
|
839 (end_state c, end_stage c, end_step c)" |
|
840 |
|
841 definition end_LE :: "(config \<times> config) set" |
810 definition end_LE :: "(config \<times> config) set" |
842 where |
811 where |
843 "end_LE \<equiv> (inv_image lex_triple end_measure)" |
812 "end_LE = measures [end_state, end_stage, end_step]" |
844 |
813 |
845 lemma wf_end_le: "wf end_LE" |
814 lemma wf_end_le: "wf end_LE" |
846 by (auto intro: wf_inv_image simp: end_LE_def wf_lex_triple) |
815 unfolding end_LE_def |
|
816 by (auto) |
847 |
817 |
848 lemma [simp]: "inv_end5 x ([], Oc # list) = False" |
818 lemma [simp]: "inv_end5 x ([], Oc # list) = False" |
849 by (auto simp: inv_end5.simps inv_end5_loop.simps) |
819 by (auto simp: inv_end5.simps inv_end5_loop.simps) |
850 |
820 |
851 lemma end_halt: |
821 lemma end_halt: |
868 using great inv_start notfinal |
838 using great inv_start notfinal |
869 apply(drule_tac stp = n in inv_end_steps, auto) |
839 apply(drule_tac stp = n in inv_end_steps, auto) |
870 done |
840 done |
871 hence "(step (s', l', r') (tcopy_end, 0), s', l', r') \<in> end_LE" |
841 hence "(step (s', l', r') (tcopy_end, 0), s', l', r') \<in> end_LE" |
872 apply(case_tac r', case_tac [2] a) |
842 apply(case_tac r', case_tac [2] a) |
873 apply(auto simp: inv_end.simps step.simps tcopy_end_def |
843 apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral end_LE_def split: if_splits) |
874 numeral end_LE_def lex_triple_def lex_pair_def split: if_splits) |
|
875 done |
844 done |
876 thus "(steps (Suc 0, l, r) (tcopy_end, 0) (Suc n), |
845 thus "(steps (Suc 0, l, r) (tcopy_end, 0) (Suc n), |
877 steps (Suc 0, l, r) (tcopy_end, 0) n) \<in> end_LE" |
846 steps (Suc 0, l, r) (tcopy_end, 0) n) \<in> end_LE" |
878 using d |
847 using d |
879 by simp |
848 by simp |