diff -r 6b6d71d14e75 -r 06a6db387cd2 thys/UF.thy
--- a/thys/UF.thy	Fri Apr 05 09:18:17 2013 +0100
+++ b/thys/UF.thy	Mon Apr 22 08:26:16 2013 +0100
@@ -152,93 +152,58 @@
                     Cn (Suc vl) rf (get_fstn_args (Suc vl) (vl - 1) 
                         @ [Cn (Suc vl) s [id (Suc vl) (vl - 1)]])]))"
 
-text {*
-  @{text "rec_exec"} is the interpreter function for
-  reursive functions. The function is defined such that 
-  it always returns meaningful results for primitive recursive 
-  functions.
-  *}
 
 declare rec_exec.simps[simp del] constn.simps[simp del]
 
-text {*
-  Correctness of @{text "rec_add"}.
-  *}
-lemma add_lemma: "\<And> x y. rec_exec rec_add [x, y] =  x + y"
+
+section {* Correctness of various recursive functions *}
+
+
+lemma add_lemma: "rec_exec rec_add [x, y] =  x + y"
 by(induct_tac y, auto simp: rec_add_def rec_exec.simps)
 
-text {*
-  Correctness of @{text "rec_mult"}.
-  *}
-lemma mult_lemma: "\<And> x y. rec_exec rec_mult [x, y] = x * y"
+lemma mult_lemma: "rec_exec rec_mult [x, y] = x * y"
 by(induct_tac y, auto simp: rec_mult_def rec_exec.simps add_lemma)
 
-text {*
-  Correctness of @{text "rec_pred"}.
-  *}
-lemma pred_lemma: "\<And> x. rec_exec rec_pred [x] =  x - 1"
+lemma pred_lemma: "rec_exec rec_pred [x] =  x - 1"
 by(induct_tac x, auto simp: rec_pred_def rec_exec.simps)
 
-text {*
-  Correctness of @{text "rec_minus"}.
-  *}
-lemma minus_lemma: "\<And> x y. rec_exec rec_minus [x, y] = x - y"
+lemma minus_lemma: "rec_exec rec_minus [x, y] = x - y"
 by(induct_tac y, auto simp: rec_exec.simps rec_minus_def pred_lemma)
 
-text {*
-  Correctness of @{text "rec_sg"}.
-  *}
-lemma sg_lemma: "\<And> x. rec_exec rec_sg [x] = (if x = 0 then 0 else 1)"
+lemma sg_lemma: "rec_exec rec_sg [x] = (if x = 0 then 0 else 1)"
 by(auto simp: rec_sg_def minus_lemma rec_exec.simps constn.simps)
 
-text {*
-  Correctness of @{text "constn"}.
-  *}
 lemma constn_lemma: "rec_exec (constn n) [x] = n"
 by(induct n, auto simp: rec_exec.simps constn.simps)
 
-text {*
-  Correctness of @{text "rec_less"}.
-  *}
-lemma less_lemma: "\<And> x y. rec_exec rec_less [x, y] = 
-  (if x < y then 1 else 0)"
+lemma less_lemma: "rec_exec rec_less [x, y] = (if x < y then 1 else 0)"
 by(induct_tac y, auto simp: rec_exec.simps 
   rec_less_def minus_lemma sg_lemma)
 
-text {*
-  Correctness of @{text "rec_not"}.
-  *}
-lemma not_lemma: 
-  "\<And> x. rec_exec rec_not [x] = (if x = 0 then 1 else 0)"
+lemma not_lemma: "rec_exec rec_not [x] = (if x = 0 then 1 else 0)"
 by(induct_tac x, auto simp: rec_exec.simps rec_not_def
   constn_lemma minus_lemma)
 
+lemma eq_lemma: "rec_exec rec_eq [x, y] = (if x = y then 1 else 0)"
+by(induct_tac y, auto simp: rec_exec.simps rec_eq_def constn_lemma add_lemma minus_lemma)
+
+lemma conj_lemma: "rec_exec rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 else 1)"
+by(induct_tac y, auto simp: rec_exec.simps sg_lemma rec_conj_def mult_lemma)
+
+lemma disj_lemma: "rec_exec rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0 else 1)"
+by(induct_tac y, auto simp: rec_disj_def sg_lemma add_lemma rec_exec.simps)
+
+declare mult_lemma[simp] add_lemma[simp] pred_lemma[simp] 
+        minus_lemma[simp] sg_lemma[simp] constn_lemma[simp] 
+        less_lemma[simp] not_lemma[simp] eq_lemma[simp]
+        conj_lemma[simp] disj_lemma[simp]
+
 text {*
-  Correctness of @{text "rec_eq"}.
-  *}
-lemma eq_lemma: "\<And> x y. rec_exec rec_eq [x, y] = (if x = y then 1 else 0)"
-by(induct_tac y, auto simp: rec_exec.simps rec_eq_def constn_lemma add_lemma minus_lemma)
-
-text {*
-  Correctness of @{text "rec_conj"}.
+  @{text "primrec recf n"} is true iff @{text "recf"} is a primitive
+  recursive function with arity @{text "n"}.
   *}
-lemma conj_lemma: "\<And> x y. rec_exec rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 
-                                                       else 1)"
-by(induct_tac y, auto simp: rec_exec.simps sg_lemma rec_conj_def mult_lemma)
-
-text {*
-  Correctness of @{text "rec_disj"}.
-  *}
-lemma disj_lemma: "\<And> x y. rec_exec rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0
-                                                     else 1)"
-by(induct_tac y, auto simp: rec_disj_def sg_lemma add_lemma rec_exec.simps)
-
-
-text {*
-  @{text "primrec recf n"} is true iff 
-  @{text "recf"} is a primitive recursive function 
-  with arity @{text "n"}.
-  *}
+
 inductive primerec :: "recf \<Rightarrow> nat \<Rightarrow> bool"
   where
 prime_z[intro]:  "primerec z (Suc 0)" |
@@ -259,10 +224,7 @@
 inductive_cases prime_cn_reverse[elim]: "primerec (Cn n f gs) m"
 inductive_cases prime_pr_reverse[elim]: "primerec (Pr n f g) m"
 
-declare mult_lemma[simp] add_lemma[simp] pred_lemma[simp] 
-        minus_lemma[simp] sg_lemma[simp] constn_lemma[simp] 
-        less_lemma[simp] not_lemma[simp] eq_lemma[simp]
-        conj_lemma[simp] disj_lemma[simp]
+
 
 text {*
   @{text "Sigma"} is the logical specification of 
@@ -271,17 +233,16 @@
 function Sigma :: "(nat list \<Rightarrow> nat) \<Rightarrow> nat list \<Rightarrow> nat"
   where
   "Sigma g xs = (if last xs = 0 then g xs
-                 else (Sigma g (butlast xs @ [last xs - 1]) +
-                       g xs)) "
+                 else (Sigma g (butlast xs @ [last xs - 1]) + g xs)) "
 by pat_completeness auto
+
 termination
 proof
   show "wf (measure (\<lambda> (f, xs). last xs))" by auto
 next
   fix g xs
   assume "last (xs::nat list) \<noteq> 0"
-  thus "((g, butlast xs @ [last xs - 1]), g, xs)  
-                   \<in> measure (\<lambda>(f, xs). last xs)"
+  thus "((g, butlast xs @ [last xs - 1]), g, xs) \<in> measure (\<lambda>(f, xs). last xs)"
     by auto
 qed
 
@@ -290,25 +251,22 @@
         rec_sigma.simps[simp del]
 
 lemma [simp]: "arity z = 1"
- by(simp add: arity.simps)
+  by(simp add: arity.simps)
 
 lemma rec_pr_0_simp_rewrite: "
   rec_exec (Pr n f g) (xs @ [0]) = rec_exec f xs"
-by(simp add: rec_exec.simps)
+  by(simp add: rec_exec.simps)
 
 lemma rec_pr_0_simp_rewrite_single_param: "
   rec_exec (Pr n f g) [0] = rec_exec f []"
-by(simp add: rec_exec.simps)
+  by(simp add: rec_exec.simps)
 
 lemma rec_pr_Suc_simp_rewrite: 
-  "rec_exec (Pr n f g) (xs @ [Suc x]) =
-                       rec_exec g (xs @ [x] @ 
-                        [rec_exec (Pr n f g) (xs @ [x])])"
+  "rec_exec (Pr n f g) (xs @ [Suc x]) = rec_exec g (xs @ [x] @ [rec_exec (Pr n f g) (xs @ [x])])"
 by(simp add: rec_exec.simps)
 
 lemma rec_pr_Suc_simp_rewrite_single_param: 
-  "rec_exec (Pr n f g) ([Suc x]) =
-           rec_exec g ([x] @ [rec_exec (Pr n f g) ([x])])"
+  "rec_exec (Pr n f g) ([Suc x]) = rec_exec g ([x] @ [rec_exec (Pr n f g) ([x])])"
 by(simp add: rec_exec.simps)
 
 lemma Sigma_0_simp_rewrite_single_param:
@@ -748,10 +706,9 @@
 text {*
   The correctness of @{text "rec_Minr"}.
   *}
-lemma Minr_lemma: "
-  \<lbrakk>primerec rf (Suc (length xs))\<rbrakk> 
-     \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = 
-            Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
+lemma Minr_lemma: 
+  assumes h: "primerec rf (Suc (length xs))" 
+  shows "rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
 proof -
   let ?rt = "(recf.id (Suc (length xs)) ((length xs)))"
   let ?rf = "(Cn (Suc (Suc (length xs))) 
@@ -760,15 +717,13 @@
                 [recf.id (Suc (Suc (length xs))) 
     (Suc ((length xs)))])])"
   let ?rq = "(rec_all ?rt ?rf)"
-  assume h: "primerec rf (Suc (length xs))"
   have h1: "primerec ?rq (Suc (length xs))"
     apply(rule_tac primerec_all_iff)
     apply(auto simp: h nth_append)+
     done
   moreover have "arity rf = Suc (length xs)"
     using h by auto
-  ultimately show "rec_exec (rec_Minr rf) (xs @ [w]) = 
-    Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
+  ultimately show "rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
     apply(simp add: rec_exec.simps rec_Minr.simps arity.simps Let_def 
                     sigma_lemma all_lemma)
     apply(rule_tac  sigma_minr_lemma)
@@ -789,7 +744,7 @@
   The correctness of @{text "rec_le"}.
   *}
 lemma le_lemma: 
-  "\<And>x y. rec_exec rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
+  "rec_exec rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
 by(auto simp: rec_le_def rec_exec.simps)
 
 text {*
@@ -857,8 +812,7 @@
   done
 
 lemma [simp]:  
-  "length ys = Suc n \<Longrightarrow> (take n ys @ [ys ! n, ys ! n]) =  
-                                                  ys @ [ys ! n]"
+  "length ys = Suc n \<Longrightarrow> (take n ys @ [ys ! n, ys ! n]) = ys @ [ys ! n]"
 apply(simp)
 apply(subgoal_tac "\<exists> xs y. ys = xs @ [y]", auto)
 apply(rule_tac x = "butlast ys" in exI, rule_tac x = "last ys" in exI)