
diff -r aea02b5a58d2 -r 6e7244ae43b8 thys/Recs.thy
--- a/thys/Recs.thy	Thu May 02 12:49:33 2013 +0100
+++ b/thys/Recs.thy	Thu May 02 13:19:50 2013 +0100
@@ -242,7 +242,9 @@
   "rec_minus = rec_swap (PR (Id 1 0) (CN rec_pred [Id 3 1]))"
 
 
-text {* Sign function returning 1 when the input argument is greater than @{text "0"}. *}
+text {* 
+  The @{text "sign"} function returns 1 when the input argument 
+  is greater than @{text "0"}. *}
 
 definition 
   "rec_sign = CN rec_minus [constn 1, CN rec_minus [constn 1, Id 1 0]]"
@@ -269,20 +271,19 @@
   "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 *}
+  y otherwise;  @{term "rec_if [z, x, y]"} returns x if z is *not*
+  zero, y otherwise *}
 
 definition 
   "rec_ifz = PR (Id 2 0) (Id 4 3)"
 
-text {* @{term "rec_if [z, x, y]"} returns x if z is *not* zero,
-  y otherwise *}
-
 definition 
   "rec_if = CN rec_ifz [CN rec_not [Id 3 0], Id 3 1, Id 3 2]"
 
 text {*
   @{text "rec_less"} compares two arguments and returns @{text "1"} if
   the first is less than the second; otherwise returns @{text "0"}. *}
+
 definition 
   "rec_less = CN rec_sign [rec_swap rec_minus]"
 
@@ -317,7 +318,7 @@
 definition
   "rec_ex2 f = CN rec_sign [rec_sigma2 f]"
 
-text {* Dvd, Quotient, Reminder *}
+text {* Dvd, Quotient, Modulo *}
 
 definition 
   "rec_dvd = 
@@ -331,7 +332,19 @@
               in PR Z if_stmt)"
 
 definition
-  "rec_rem = CN rec_minus [Id 2 0, CN rec_mult [Id 2 1, rec_quo]]"
+  "rec_mod = CN rec_minus [Id 2 0, CN rec_mult [Id 2 1, rec_quo]]"
+
+
+section {* Prime Numbers *}
+
+definition 
+  "rec_prime = 
+    (let conj1 = CN rec_less [constn 1, Id 1 0] in
+     let disj  = CN rec_disj [CN rec_eq [Id 2 0, constn 1], rec_eq] in
+     let imp   = CN rec_imp [rec_dvd, disj] in
+     let conj2 = CN (rec_all1 imp) [Id 1 0, Id 1 0] in
+     CN rec_conj [conj1, conj2])"
+
 
 section {* Correctness of Recursive Functions *}
 
@@ -506,8 +519,8 @@
 by (simp add: Quo_div Quo_rec_quo)
 
 lemma rem_lemma [simp]:
-  shows "rec_eval rec_rem [y, x] = y mod x"
-by (simp add: rec_rem_def mod_div_equality' nat_mult_commute)
+  shows "rec_eval rec_mod [y, x] = y mod x"
+by (simp add: rec_mod_def mod_div_equality' nat_mult_commute)
 
 
 section {* Prime Numbers *}
@@ -520,14 +533,6 @@
 apply(auto)
 done
 
-definition 
-  "rec_prime = 
-    (let conj1 = CN rec_less [constn 1, Id 1 0] in
-     let disj  = CN rec_disj [CN rec_eq [Id 2 0, constn 1], rec_eq] in
-     let imp   = CN rec_imp [rec_dvd, disj] in
-     let conj2 = CN (rec_all1 imp) [Id 1 0, Id 1 0] in
-     CN rec_conj [conj1, conj2])"
-
 lemma prime_lemma [simp]: 
   "rec_eval rec_prime [x] = (if prime x then 1 else 0)"
 by (auto simp add: rec_prime_def Let_def prime_alt_def)
@@ -605,7 +610,7 @@
 
 definition
   "rec_lo = 
-     (let calc = CN rec_noteq [CN rec_rem [Id 3 1, CN rec_power [Id 3 2, Id 3 0]], Z] in
+     (let calc = CN rec_noteq [CN rec_mod [Id 3 1, CN rec_power [Id 3 2, Id 3 0]], Z] in
       let max  = CN (rec_max2 calc) [Id 2 0, Id 2 0, Id 2 1] in
       let cond = CN rec_conj [CN rec_less [constn 1, Id 2 0], CN rec_less [constn 1, Id 2 1]] 
       in CN rec_ifz [cond, Z, max])"
@@ -616,7 +621,9 @@
 
 
 
-text {* @{text "NextPrime x"} returns the first prime number after @{text "x"}. *}
+text {* 
+  @{text "NextPrime x"} returns the first prime number after @{text "x"};
+  @{text "Pi i"} returns the i-th prime number. *}
 
 fun NextPrime ::"nat \<Rightarrow> nat"
   where
@@ -647,56 +654,10 @@
   "rec_eval rec_pi [x] = Pi x"
 by (induct x) (simp_all add: rec_pi_def)
 
-
 end
 
-
 (*
 
-
-
-fun mtest where
-  "mtest R 0 = if R 0 then 0 else 1"
-| "mtest R (Suc n) = (if R n then mtest R n else (Suc n))"
-
-
-lemma 
-  "rec_eval (rec_maxr2 f) [x, y1, y2] = XXX"
-apply(simp only: rec_maxr2_def)
-apply(case_tac x)
-apply(clarify)
-apply(subst rec_eval.simps)
-apply(simp only: constn_lemma)
-defer
-apply(clarify)
-apply(subst rec_eval.simps)
-apply(simp only: rec_maxr2_def[symmetric])
-apply(subst rec_eval.simps)
-apply(simp only: map.simps nth)
-apply(subst rec_eval.simps)
-apply(simp only: map.simps nth)
-apply(subst rec_eval.simps)
-apply(simp only: map.simps nth)
-apply(subst rec_eval.simps)
-apply(simp only: map.simps nth)
-apply(subst rec_eval.simps)
-apply(simp only: map.simps nth)
-apply(subst rec_eval.simps)
-apply(simp only: map.simps nth)
-
-
-definition
-  "rec_minr2 f = rec_sigma2 (rec_accum2 (CN rec_not [f]))"
-
-definition
-  "rec_maxr2 f = rec_sigma2 (CN rec_sign [CN (rec_sigma2 f) [S]])"
-
-definition Minr :: "(nat \<Rightarrow> nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat"
-  where "Minr R x ys = Min ({z | z. z \<le> x \<and> R z ys} \<union> {Suc x})"
-
-definition Maxr :: "(nat \<Rightarrow> nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat"
-  where "Maxr R x ys = Max ({z | z. z \<le> x \<and> R z ys} \<union> {0})"
-
 lemma rec_minr2_le_Suc:
   "rec_eval (rec_minr2 f) [x, y1, y2] \<le> Suc x"
 apply(simp add: rec_minr2_def)




