tm2: comparison thys/Recs.thy

equal deleted inserted replaced

-:087d82632852
+:e04123f4bacc
 section {* Arithmetic Functions *}
 text {*
-@{text "constn n"} is the recursive function which computes
+@{text "constn n"} is the recursive function which generates
-natural number @{text "n"}.
+the natural number @{text "n"}. *}
-*}
 fun constn :: "nat \<Rightarrow> recf"
 where
 "constn 0 = Z"  |
 "constn (Suc n) = CN S [constn n]"
 "rec_pred = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]"
 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)
 lemma swap_lemma [simp]:
 lemma fact_lemma [simp]:
 "rec_eval rec_fact [x] = fact x"
 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]:
 "rec_eval rec_minus [x, y] = x - y"
 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
 is greater than @{text "0"}. *}
 "rec_disj = CN rec_sign [rec_add]"
 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,
+text {* @{term "rec_ifz [z, x, y]"} returns @{text x} if @{text z} is zero, and
-y otherwise;  @{term "rec_if [z, x, y]"} returns x if z is *not*
+@{text y} otherwise;  @{term "rec_if [z, x, y]"} returns @{text x} if @{text z}
-zero, y otherwise *}
+is *not* zero, and @{text y} otherwise. *}
 definition
 "rec_ifz = PR (Id 2 0) (Id 4 3)"
 definition
 lemma if_lemma [simp]:
 "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]"
 definition
 lemma less_lemma [simp]:
 "rec_eval rec_less [x, y] = (if x < y then 1 else 0)"
 by (simp add: rec_less_def)
 lemma le_lemma [simp]:
-"rec_eval rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
+"rec_eval rec_le [x, y] = (if x \<le> y then 1 else 0)"
-by(simp add: rec_le_def)
+by (simp add: rec_le_def)
 section {* Summation and Product Functions *}
 definition
 by (induct x) (simp_all add: rec_accum3_def)
 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]"
 definition
 "rec_all2 f = CN rec_sign [rec_accum2 f]"
 by (simp add: rec_all3_def)
 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]:
 "rec_eval (rec_all2_less f) [x, y1, y2] = (if (\<forall>z < x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
 apply(auto simp add: Let_def rec_all2_less_def)
 apply(metis nat_less_le)+
 done
-section {* Quotients *}
+section {* Natural Number Division *}
-definition
-"rec_quo = (let lhs = CN S [Id 3 0] in
+definition
+"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
+fun Div where
-"Quo x 0 = 0"
+"Div x 0 = 0"
-| "Quo x (Suc y) = (if (Suc y = x * (Suc (Quo x y))) then Suc (Quo x y) else Quo x y)"
+| "Div x (Suc y) = (if (Suc y = x * (Suc (Div x y))) then Suc (Div x y) else Div x y)"
-lemma Quo0:
+lemma Div0:
-shows "Quo 0 y = 0"
+shows "Div 0 y = 0"
 by (induct y) (auto)
-lemma Quo1:
+lemma Div1:
-"x * (Quo x y) \<le> y"
+"x * (Div x y) \<le> y"
 by (induct y) (simp_all)
-lemma Quo2:
+lemma Div2:
-"b * (Quo b a) + a mod b = a"
+"x * (Div x y) + y mod x = y"
-by (induct a) (auto simp add: mod_Suc)
+by (induct y) (auto simp add: mod_Suc)
-lemma Quo3:
+lemma Div3:
-"n * (Quo n m) = m - m mod n"
+"x * (Div x y) = y - y mod x"
-using Quo2[of n m] by (auto)
+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:
+lemma Div_div:
-shows "Quo x y = y div x"
+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:
+lemma Div_rec_div:
-shows "rec_eval rec_quo [y, x] = Quo x y"
+shows "rec_eval rec_div [y, x] = Div x y"
-by (induct y) (simp_all add: rec_quo_def)
+by (induct y) (simp_all add: rec_div_def)
-lemma quo_lemma [simp]:
+lemma div_lemma [simp]:
-shows "rec_eval rec_quo [y, x] = y div x"
+shows "rec_eval rec_div [y, x] = y div x"
-by (simp add: Quo_div Quo_rec_quo)
+by (simp add: Div_div Div_rec_div)
 section {* Iteration *}
 definition
 by (induct n) (simp_all add: rec_iter_def)
 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"
 | "BMax_rec R (Suc n) = (if R (Suc n) then (Suc n) else BMax_rec R n)"
 apply(auto intro: Max_eqI Max_eqI[symmetric])
 apply(simp add: le_Suc_eq)
 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
 "rec_max1 f = PR Z (CN rec_ifz [CN f [CN S [Id 3 0], Id 3 2], CN S [Id 3 0], Id 3 1])"
 lemma max2_lemma [simp]:
 "rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x"
 by (induct x) (simp_all add: rec_max2_def)
-section {* Encodings using Cantor's pairing function *}
+section {* Encodings using Cantor's Pairing Function *}
-text {*
+text {* We use Cantor's pairing function from the theory
-We use Cantor's pairing function from Nat_Bijection.
+Nat_Bijection. However, we need to prove that the formulation
-However, we need to prove that the formulation of the
+of the decoding function there is recursive. For this we first
-decoding function there is recursive. For this we first
 prove that we can extract the maximal triangle number
 using @{term prod_decode}.
 *}
 abbreviation Max_triangle_aux where
 apply(simp)
 done
 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 =
 (let cond = CN rec_not [CN rec_le [CN rec_triangle [Id 2 0], Id 2 1]] in
 CN (rec_max1 cond) [Id 1 0, Id 1 0])"
 lemma max_triangle_lemma [simp]:
 "rec_eval rec_max_triangle [x] = Max_triangle x"
 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]"
 definition
 lemma penc_lemma [simp]:
 "rec_eval rec_penc [m, n] = penc m n"
 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"
 where
 "lenc [] = 0"
 lemma lenc_length_le:
 "length xs \<le> lenc xs"
 by (induct xs) (simp_all add: prod_encode_def)
+text {* The membership predicate for an encoded list. *}
-text {* Membership for the List Encoding *}
 fun within :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
 "within z 0 = (0 < z)"
 | "within z (Suc n) = within (pdec2 z) n"
 apply(simp_all add: prod_encode_def)
 apply(case_tac xs)
 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"
 unfolding enclen_def
 apply(simp add: BMax_rec_eq1)

changeset 20	e04123f4bacc
parent 15	e3ecf558aef2