4 |
4 |
5 fun addition :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
5 fun addition :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
6 where |
6 where |
7 "addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, Inc m, Goto 4]" |
7 "addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, Inc m, Goto 4]" |
8 |
8 |
|
9 (* moves register m to register n *) |
9 fun mv_box :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
10 fun mv_box :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
10 where |
11 where |
11 "mv_box m n = [Dec m 3, Inc n, Goto 0]" |
12 "mv_box m n = [Dec m 3, Inc n, Goto 0]" |
12 |
13 |
13 text {* The compilation of @{text "z"}-operator. *} |
14 text {* The compilation of @{text "z"}-operator. *} |
16 "rec_ci_z \<equiv> [Goto 1]" |
17 "rec_ci_z \<equiv> [Goto 1]" |
17 |
18 |
18 text {* The compilation of @{text "s"}-operator. *} |
19 text {* The compilation of @{text "s"}-operator. *} |
19 definition rec_ci_s :: "abc_inst list" |
20 definition rec_ci_s :: "abc_inst list" |
20 where |
21 where |
21 "rec_ci_s \<equiv> (addition 0 1 2 [+] [Inc 1])" |
22 "rec_ci_s \<equiv> addition 0 1 2 [+] [Inc 1]" |
22 |
23 |
23 |
24 |
24 text {* The compilation of @{text "id i j"}-operator *} |
25 text {* The compilation of @{text "id i j"}-operator *} |
25 fun rec_ci_id :: "nat \<Rightarrow> nat \<Rightarrow> abc_inst list" |
26 fun rec_ci_id :: "nat \<Rightarrow> nat \<Rightarrow> abc_inst list" |
26 where |
27 where |
34 fun empty_boxes :: "nat \<Rightarrow> abc_inst list" |
35 fun empty_boxes :: "nat \<Rightarrow> abc_inst list" |
35 where |
36 where |
36 "empty_boxes 0 = []" | |
37 "empty_boxes 0 = []" | |
37 "empty_boxes (Suc n) = empty_boxes n [+] [Dec n 2, Goto 0]" |
38 "empty_boxes (Suc n) = empty_boxes n [+] [Dec n 2, Goto 0]" |
38 |
39 |
39 fun cn_merge_gs :: |
40 fun cn_merge_gs :: "(abc_inst list \<times> nat \<times> nat) list \<Rightarrow> nat \<Rightarrow> abc_inst list" |
40 "(abc_inst list \<times> nat \<times> nat) list \<Rightarrow> nat \<Rightarrow> abc_inst list" |
|
41 where |
41 where |
42 "cn_merge_gs [] p = []" | |
42 "cn_merge_gs [] p = []" | |
43 "cn_merge_gs (g # gs) p = |
43 "cn_merge_gs (g # gs) p = |
44 (let (gprog, gpara, gn) = g in |
44 (let (gprog, gpara, gn) = g in |
45 gprog [+] mv_box gpara p [+] cn_merge_gs gs (Suc p))" |
45 gprog [+] mv_box gpara p [+] cn_merge_gs gs (Suc p))" |
89 mv_box.simps[simp del] addition.simps[simp del] |
89 mv_box.simps[simp del] addition.simps[simp del] |
90 |
90 |
91 declare abc_steps_l.simps[simp del] abc_fetch.simps[simp del] |
91 declare abc_steps_l.simps[simp del] abc_fetch.simps[simp del] |
92 abc_step_l.simps[simp del] |
92 abc_step_l.simps[simp del] |
93 |
93 |
94 inductive_cases terminate_pr_reverse: "terminate (Pr n f g) xs" |
94 fun addition_inv :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool" |
95 |
|
96 inductive_cases terminate_z_reverse[elim!]: "terminate z xs" |
|
97 |
|
98 inductive_cases terminate_s_reverse[elim!]: "terminate s xs" |
|
99 |
|
100 inductive_cases terminate_id_reverse[elim!]: "terminate (id m n) xs" |
|
101 |
|
102 inductive_cases terminate_cn_reverse[elim!]: "terminate (Cn n f gs) xs" |
|
103 |
|
104 inductive_cases terminate_mn_reverse[elim!]:"terminate (Mn n f) xs" |
|
105 |
|
106 fun addition_inv :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> |
|
107 nat list \<Rightarrow> bool" |
|
108 where |
95 where |
109 "addition_inv (as, lm') m n p lm = |
96 "addition_inv (as, lm') m n p lm = |
110 (let sn = lm ! n in |
97 (let sn = lm ! n in |
111 let sm = lm ! m in |
98 let sm = lm ! m in |
112 lm ! p = 0 \<and> |
99 lm ! p = 0 \<and> |
151 else if as = 5 then 2 |
138 else if as = 5 then 2 |
152 else if as = 6 then 1 |
139 else if as = 6 then 1 |
153 else if as = 4 then 0 |
140 else if as = 4 then 0 |
154 else 0)" |
141 else 0)" |
155 |
142 |
156 fun addition_measure :: "((nat \<times> nat list) \<times> nat \<times> nat) \<Rightarrow> |
143 fun addition_measure :: "((nat \<times> nat list) \<times> nat \<times> nat) \<Rightarrow> (nat \<times> nat \<times> nat)" |
157 (nat \<times> nat \<times> nat)" |
|
158 where |
144 where |
159 "addition_measure ((as, lm), m, p) = |
145 "addition_measure ((as, lm), m, p) = |
160 (addition_stage1 (as, lm) m p, |
146 (addition_stage1 (as, lm) m p, |
161 addition_stage2 (as, lm) m p, |
147 addition_stage2 (as, lm) m p, |
162 addition_stage3 (as, lm) m p)" |
148 addition_stage3 (as, lm) m p)" |
163 |
149 |
164 definition addition_LE :: "(((nat \<times> nat list) \<times> nat \<times> nat) \<times> |
150 definition addition_LE :: "(((nat \<times> nat list) \<times> nat \<times> nat) \<times> ((nat \<times> nat list) \<times> nat \<times> nat)) set" |
165 ((nat \<times> nat list) \<times> nat \<times> nat)) set" |
|
166 where "addition_LE \<equiv> (inv_image lex_triple addition_measure)" |
151 where "addition_LE \<equiv> (inv_image lex_triple addition_measure)" |
167 |
152 |
168 lemma [simp]: "wf addition_LE" |
153 lemma [simp]: "wf addition_LE" |
169 by(auto simp: wf_inv_image addition_LE_def lex_triple_def |
154 by(auto simp: wf_inv_image addition_LE_def lex_triple_def lex_pair_def) |
170 lex_pair_def) |
|
171 |
155 |
172 declare addition_inv.simps[simp del] |
156 declare addition_inv.simps[simp del] |
173 |
157 |
174 lemma addition_inv_init: |
158 lemma addition_inv_init: |
175 "\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk> \<Longrightarrow> |
159 "\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk> \<Longrightarrow> |
327 apply(auto) |
311 apply(auto) |
328 done |
312 done |
329 qed |
313 qed |
330 |
314 |
331 lemma compile_s_correct': |
315 lemma compile_s_correct': |
332 "{\<lambda>nl. nl = n # 0 \<up> 2 @ anything} addition 0 (Suc 0) 2 [+] [Inc (Suc 0)] {\<lambda>nl. nl = n # Suc n # 0 # anything}" |
316 "{\<lambda>nl. nl = n # 0 \<up> 2 @ anything} |
|
317 addition 0 (Suc 0) 2 [+] [Inc (Suc 0)] |
|
318 {\<lambda>nl. nl = n # Suc n # 0 # anything}" |
333 proof(rule_tac abc_Hoare_plus_halt) |
319 proof(rule_tac abc_Hoare_plus_halt) |
334 show "{\<lambda>nl. nl = n # 0 \<up> 2 @ anything} addition 0 (Suc 0) 2 {\<lambda> nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \<up> 2 @ anything)}" |
320 show "{\<lambda>nl. nl = n # 0 \<up> 2 @ anything} |
|
321 addition 0 (Suc 0) 2 |
|
322 {\<lambda>nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \<up> 2 @ anything)}" |
335 by(rule_tac addition_correct, auto simp: numeral_2_eq_2) |
323 by(rule_tac addition_correct, auto simp: numeral_2_eq_2) |
336 next |
324 next |
337 show "{\<lambda>nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \<up> 2 @ anything)} [Inc (Suc 0)] {\<lambda>nl. nl = n # Suc n # 0 # anything}" |
325 show "{\<lambda>nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \<up> 2 @ anything)} |
|
326 [Inc (Suc 0)] |
|
327 {\<lambda>nl. nl = n # Suc n # 0 # anything}" |
338 by(rule_tac abc_Hoare_haltI, rule_tac x = 1 in exI, auto simp: addition_inv.simps |
328 by(rule_tac abc_Hoare_haltI, rule_tac x = 1 in exI, auto simp: addition_inv.simps |
339 abc_steps_l.simps abc_step_l.simps abc_fetch.simps numeral_2_eq_2 abc_lm_s.simps abc_lm_v.simps) |
329 abc_steps_l.simps abc_step_l.simps abc_fetch.simps numeral_2_eq_2 abc_lm_s.simps abc_lm_v.simps) |
340 qed |
330 qed |
341 |
331 |
342 declare rec_exec.simps[simp del] |
332 declare rec_exec.simps[simp del] |