diff -r 6b6d71d14e75 -r 06a6db387cd2 thys/Recursive.thy
--- 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