diff -r 087d82632852 -r e04123f4bacc thys/Recs.thy
--- a/thys/Recs.thy	Tue Apr 29 15:26:48 2014 +0100
+++ b/thys/Recs.thy	Fri May 30 12:04:49 2014 +0100
@@ -222,9 +222,9 @@
 section {* Arithmetic Functions *}
 
 text {*
-  @{text "constn n"} is the recursive function which computes 
-  natural number @{text "n"}.
-*}
+  @{text "constn n"} is the recursive function which generates
+  the natural number @{text "n"}. *}
+
 fun constn :: "nat \<Rightarrow> recf"
   where
   "constn 0 = Z"  |
@@ -254,6 +254,7 @@
 definition 
   "rec_minus = rec_swap (PR (Id 1 0) (CN rec_pred [Id 3 1]))"
 
+
 lemma constn_lemma [simp]: 
   "rec_eval (constn n) xs = n"
 by (induct n) (simp_all)
@@ -283,7 +284,7 @@
 by (simp add: rec_fact_def)
 
 lemma pred_lemma [simp]: 
-  "rec_eval rec_pred [x] =  x - 1"
+  "rec_eval rec_pred [x] = x - 1"
 by (induct x) (simp_all add: rec_pred_def)
 
 lemma minus_lemma [simp]: 
@@ -291,7 +292,7 @@
 by (induct y) (simp_all add: rec_minus_def)
 
 
-section {* Logical functions *}
+section {* Logical Functions *}
 
 text {* 
   The @{text "sign"} function returns 1 when the input argument 
@@ -321,9 +322,9 @@
 definition 
   "rec_imp = CN rec_disj [CN rec_not [Id 2 0], Id 2 1]"
 
-text {* @{term "rec_ifz [z, x, y]"} returns x if z is zero,
-  y otherwise;  @{term "rec_if [z, x, y]"} returns x if z is *not*
-  zero, y otherwise *}
+text {* @{term "rec_ifz [z, x, y]"} returns @{text x} if @{text z} is zero, and
+  @{text y} otherwise;  @{term "rec_if [z, x, y]"} returns @{text x} if @{text z} 
+  is *not* zero, and @{text y} otherwise. *}
 
 definition 
   "rec_ifz = PR (Id 2 0) (Id 4 3)"
@@ -368,11 +369,12 @@
   "rec_eval rec_if [z, x, y] = (if 0 < z then x else y)" 
 by (simp add: rec_if_def)
 
-section {* Less and Le Relations *}
+
+section {* The Less and Less-Equal Relations *}
 
 text {*
   @{text "rec_less"} compares two arguments and returns @{text "1"} if
-  the first is less than the second; otherwise returns @{text "0"}. *}
+  the first is less than the second; otherwise it returns @{text "0"}. *}
 
 definition 
   "rec_less = CN rec_sign [rec_swap rec_minus]"
@@ -385,8 +387,8 @@
 by (simp add: rec_less_def)
 
 lemma le_lemma [simp]: 
-  "rec_eval rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
-by(simp add: rec_le_def)
+  "rec_eval rec_le [x, y] = (if x \<le> y then 1 else 0)"
+by (simp add: rec_le_def)
 
 
 section {* Summation and Product Functions *}
@@ -435,6 +437,11 @@
 
 section {* Bounded Quantifiers *}
 
+text {* Instead of defining quantifiers taking an aritrary 
+  list of arguments, we define the simpler quantifiers taking
+  one, two and three extra arguments besides the argument
+  that is quantified over. *}
+
 definition
   "rec_all1 f = CN rec_sign [rec_accum1 f]"
 
@@ -484,7 +491,7 @@
 lemma all1_less_lemma [simp]:
   "rec_eval (rec_all1_less f) [x, y] = (if (\<forall>z < x. 0 < rec_eval f [z, y]) then 1 else 0)"
 apply(auto simp add: Let_def rec_all1_less_def)
-apply (metis nat_less_le)+
+apply(metis nat_less_le)+
 done
 
 lemma all2_less_lemma [simp]:
@@ -493,60 +500,61 @@
 apply(metis nat_less_le)+
 done
 
-section {* Quotients *}
+
+section {* Natural Number Division *}
 
 definition
-  "rec_quo = (let lhs = CN S [Id 3 0] in
+  "rec_div = (let lhs = CN S [Id 3 0] in
               let rhs = CN rec_mult [Id 3 2, CN S [Id 3 1]] in
               let cond = CN rec_eq [lhs, rhs] in
               let if_stmt = CN rec_if [cond, CN S [Id 3 1], Id 3 1]
               in PR Z if_stmt)"
 
-fun Quo where
-  "Quo x 0 = 0"
-| "Quo x (Suc y) = (if (Suc y = x * (Suc (Quo x y))) then Suc (Quo x y) else Quo x y)"
+fun Div where
+  "Div x 0 = 0"
+| "Div x (Suc y) = (if (Suc y = x * (Suc (Div x y))) then Suc (Div x y) else Div x y)"
 
-lemma Quo0:
-  shows "Quo 0 y = 0"
+lemma Div0:
+  shows "Div 0 y = 0"
 by (induct y) (auto)
 
-lemma Quo1:
-  "x * (Quo x y) \<le> y"
+lemma Div1:
+  "x * (Div x y) \<le> y"
 by (induct y) (simp_all)
 
-lemma Quo2: 
-  "b * (Quo b a) + a mod b = a"
-by (induct a) (auto simp add: mod_Suc)
+lemma Div2: 
+  "x * (Div x y) + y mod x = y"
+by (induct y) (auto simp add: mod_Suc)
 
-lemma Quo3:
-  "n * (Quo n m) = m - m mod n"
-using Quo2[of n m] by (auto)
+lemma Div3:
+  "x * (Div x y) = y - y mod x"
+using Div2[of x y] by (auto)
 
-lemma Quo4:
+lemma Div4:
   assumes h: "0 < x"
-  shows "y < x + x * Quo x y"
+  shows "y < x + x * Div x y"
 proof -
   have "x - (y mod x) > 0" using mod_less_divisor assms by auto
   then have "y < y + (x - (y mod x))" by simp
   then have "y < x + (y - (y mod x))" by simp
-  then show "y < x + x * (Quo x y)" by (simp add: Quo3) 
+  then show "y < x + x * (Div x y)" by (simp add: Div3) 
 qed
 
-lemma Quo_div: 
-  shows "Quo x y = y div x"
+lemma Div_div: 
+  shows "Div x y = y div x"
 apply(case_tac "x = 0")
-apply(simp add: Quo0)
+apply(simp add: Div0)
 apply(subst split_div_lemma[symmetric])
-apply(auto intro: Quo1 Quo4)
+apply(auto intro: Div1 Div4)
 done
 
-lemma Quo_rec_quo:
-  shows "rec_eval rec_quo [y, x] = Quo x y"
-by (induct y) (simp_all add: rec_quo_def)
+lemma Div_rec_div:
+  shows "rec_eval rec_div [y, x] = Div x y"
+by (induct y) (simp_all add: rec_div_def)
 
-lemma quo_lemma [simp]:
-  shows "rec_eval rec_quo [y, x] = y div x"
-by (simp add: Quo_div Quo_rec_quo)
+lemma div_lemma [simp]:
+  shows "rec_eval rec_div [y, x] = y div x"
+by (simp add: Div_div Div_rec_div)
 
 
 section {* Iteration *}
@@ -569,6 +577,9 @@
 
 section {* Bounded Maximisation *}
 
+text {* Computes the greatest number below a bound @{text n}
+  such that a predicate holds. If such a maximum does not exist,
+  then @{text 0} is returned. *}
 
 fun BMax_rec where
   "BMax_rec R 0 = 0"
@@ -594,7 +605,7 @@
 by metis
 
 lemma BMax_rec_eq3:
-  "BMax_rec R x = Max (Set.filter (\<lambda>z. R z) {..x} \<union> {0})"
+  "BMax_rec R x = Max (Set.filter R {..x} \<union> {0})"
 by (simp add: BMax_rec_eq2 Set.filter_def)
 
 definition 
@@ -612,12 +623,11 @@
 by (induct x) (simp_all add: rec_max2_def)
 
 
-section {* Encodings using Cantor's pairing function *}
+section {* Encodings using Cantor's Pairing Function *}
 
-text {*
-  We use Cantor's pairing function from Nat_Bijection.
-  However, we need to prove that the formulation of the
-  decoding function there is recursive. For this we first 
+text {* We use Cantor's pairing function from the theory 
+  Nat_Bijection. However, we need to prove that the formulation 
+  of the decoding function there is recursive. For this we first 
   prove that we can extract the maximal triangle number 
   using @{term prod_decode}.
 *}
@@ -699,7 +709,7 @@
 
 
 definition 
-  "rec_triangle = CN rec_quo [CN rec_mult [Id 1 0, S], constn 2]"
+  "rec_triangle = CN rec_div [CN rec_mult [Id 1 0, S], constn 2]"
 
 definition
   "rec_max_triangle = 
@@ -716,7 +726,7 @@
 by (simp add: Max_triangle_greatest rec_max_triangle_def Let_def BMax_rec_eq1) 
 
 
-text {* Encodings for Products *}
+text {* Encodings for Pairs of Natural Numbers *}
 
 definition
   "rec_penc = CN rec_add [CN rec_triangle [CN rec_add [Id 2 0, Id 2 1]], Id 2 0]"
@@ -740,7 +750,7 @@
 by (simp add: rec_penc_def prod_encode_def)
 
 
-text {* Encodings of Lists *}
+text {* Encodings of Lists of Natural Numbers *}
 
 fun 
   lenc :: "nat list \<Rightarrow> nat" 
@@ -772,8 +782,7 @@
   "length xs \<le> lenc xs"  
 by (induct xs) (simp_all add: prod_encode_def)
 
-
-text {* Membership for the List Encoding *}
+text {* The membership predicate for an encoded list. *}
 
 fun within :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
   "within z 0 = (0 < z)"
@@ -795,7 +804,7 @@
 apply(simp_all)
 done
 
-text {* Length of Encoded Lists *}
+text {* The length of an encoded list. *}
 
 lemma enclen_length [simp]:
   "enclen (lenc xs) = length xs"