--- 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"