--- a/thys/Recursive.thy Fri Apr 05 09:18:17 2013 +0100
+++ b/thys/Recursive.thy Mon Apr 22 08:26:16 2013 +0100
@@ -6,6 +6,7 @@
where
"addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, Inc m, Goto 4]"
+(* moves register m to register n *)
fun mv_box :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
where
"mv_box m n = [Dec m 3, Inc n, Goto 0]"
@@ -18,7 +19,7 @@
text {* The compilation of @{text "s"}-operator. *}
definition rec_ci_s :: "abc_inst list"
where
- "rec_ci_s \<equiv> (addition 0 1 2 [+] [Inc 1])"
+ "rec_ci_s \<equiv> addition 0 1 2 [+] [Inc 1]"
text {* The compilation of @{text "id i j"}-operator *}
@@ -36,8 +37,7 @@
"empty_boxes 0 = []" |
"empty_boxes (Suc n) = empty_boxes n [+] [Dec n 2, Goto 0]"
-fun cn_merge_gs ::
- "(abc_inst list \<times> nat \<times> nat) list \<Rightarrow> nat \<Rightarrow> abc_inst list"
+fun cn_merge_gs :: "(abc_inst list \<times> nat \<times> nat) list \<Rightarrow> nat \<Rightarrow> abc_inst list"
where
"cn_merge_gs [] p = []" |
"cn_merge_gs (g # gs) p =
@@ -91,20 +91,7 @@
declare abc_steps_l.simps[simp del] abc_fetch.simps[simp del]
abc_step_l.simps[simp del]
-inductive_cases terminate_pr_reverse: "terminate (Pr n f g) xs"
-
-inductive_cases terminate_z_reverse[elim!]: "terminate z xs"
-
-inductive_cases terminate_s_reverse[elim!]: "terminate s xs"
-
-inductive_cases terminate_id_reverse[elim!]: "terminate (id m n) xs"
-
-inductive_cases terminate_cn_reverse[elim!]: "terminate (Cn n f gs) xs"
-
-inductive_cases terminate_mn_reverse[elim!]:"terminate (Mn n f) xs"
-
-fun addition_inv :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow>
- nat list \<Rightarrow> bool"
+fun addition_inv :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool"
where
"addition_inv (as, lm') m n p lm =
(let sn = lm ! n in
@@ -153,21 +140,18 @@
else if as = 4 then 0
else 0)"
-fun addition_measure :: "((nat \<times> nat list) \<times> nat \<times> nat) \<Rightarrow>
- (nat \<times> nat \<times> nat)"
+fun addition_measure :: "((nat \<times> nat list) \<times> nat \<times> nat) \<Rightarrow> (nat \<times> nat \<times> nat)"
where
"addition_measure ((as, lm), m, p) =
(addition_stage1 (as, lm) m p,
addition_stage2 (as, lm) m p,
addition_stage3 (as, lm) m p)"
-definition addition_LE :: "(((nat \<times> nat list) \<times> nat \<times> nat) \<times>
- ((nat \<times> nat list) \<times> nat \<times> nat)) set"
+definition addition_LE :: "(((nat \<times> nat list) \<times> nat \<times> nat) \<times> ((nat \<times> nat list) \<times> nat \<times> nat)) set"
where "addition_LE \<equiv> (inv_image lex_triple addition_measure)"
lemma [simp]: "wf addition_LE"
-by(auto simp: wf_inv_image addition_LE_def lex_triple_def
- lex_pair_def)
+by(auto simp: wf_inv_image addition_LE_def lex_triple_def lex_pair_def)
declare addition_inv.simps[simp del]
@@ -329,12 +313,18 @@
qed
lemma compile_s_correct':
- "{\<lambda>nl. nl = n # 0 \<up> 2 @ anything} addition 0 (Suc 0) 2 [+] [Inc (Suc 0)] {\<lambda>nl. nl = n # Suc n # 0 # anything}"
+ "{\<lambda>nl. nl = n # 0 \<up> 2 @ anything}
+ addition 0 (Suc 0) 2 [+] [Inc (Suc 0)]
+ {\<lambda>nl. nl = n # Suc n # 0 # anything}"
proof(rule_tac abc_Hoare_plus_halt)
- 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)}"
+ 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)}"
by(rule_tac addition_correct, auto simp: numeral_2_eq_2)
next
- 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}"
+ 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}"
by(rule_tac abc_Hoare_haltI, rule_tac x = 1 in exI, auto simp: addition_inv.simps
abc_steps_l.simps abc_step_l.simps abc_fetch.simps numeral_2_eq_2 abc_lm_s.simps abc_lm_v.simps)
qed