--- a/thys2/Recs.thy Sat May 25 11:46:25 2013 +0100
+++ b/thys2/Recs.thy Sat May 25 16:40:48 2013 +0100
@@ -178,6 +178,8 @@
| "arity (Pr n f g) = Suc n"
| "arity (Mn n f) = n"
+text {* Abbreviations for calculating the arity of the constructors *}
+
abbreviation
"CN f gs \<equiv> Cn (arity (hd gs)) f gs"
@@ -187,6 +189,8 @@
abbreviation
"MN f \<equiv> Mn (arity f - 1) f"
+text {* the evaluation function and termination relation *}
+
fun rec_eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
where
"rec_eval Z xs = 0"
@@ -215,7 +219,7 @@
\<forall> i < r. terminates f (i # xs) \<and> rec_eval f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminates (Mn n f) xs"
-section {* Recursive Function Definitions *}
+section {* Arithmetic Functions *}
text {*
@{text "constn n"} is the recursive function which computes
@@ -247,6 +251,40 @@
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]:
+ "rec_eval (rec_swap f) [x, y] = rec_eval f [y, x]"
+by (simp add: rec_swap_def)
+
+lemma add_lemma [simp]:
+ "rec_eval rec_add [x, y] = x + y"
+by (induct x) (simp_all add: rec_add_def)
+
+lemma mult_lemma [simp]:
+ "rec_eval rec_mult [x, y] = x * y"
+by (induct x) (simp_all add: rec_mult_def)
+
+lemma power_lemma [simp]:
+ "rec_eval rec_power [x, y] = x ^ y"
+by (induct y) (simp_all add: rec_power_def)
+
+lemma fact_lemma [simp]:
+ "rec_eval rec_fact [x] = fact x"
+by (induct x) (simp_all add: rec_fact_def)
+
+lemma pred_lemma [simp]:
+ "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 *}
text {*
The @{text "sign"} function returns 1 when the input argument
@@ -286,127 +324,6 @@
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]"
-
-definition
- "rec_le = CN rec_disj [rec_less, rec_eq]"
-
-text {* Sigma and Accum for function with one and two arguments *}
-
-definition
- "rec_sigma1 f = PR (CN f [Z, Id 1 0]) (CN rec_add [Id 3 1, CN f [S, Id 3 2]])"
-
-definition
- "rec_sigma2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_add [Id 4 1, CN f [S, Id 4 2, Id 4 3]])"
-
-definition
- "rec_accum1 f = PR (CN f [Z, Id 1 0]) (CN rec_mult [Id 3 1, CN f [S, Id 3 2]])"
-
-definition
- "rec_accum2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_mult [Id 4 1, CN f [S, Id 4 2, Id 4 3]])"
-
-definition
- "rec_accum3 f = PR (CN f [Z, Id 3 0, Id 3 1, Id 3 2])
- (CN rec_mult [Id 5 1, CN f [S, Id 5 2, Id 5 3, Id 5 4]])"
-
-
-text {* Bounded quantifiers for one and two arguments *}
-
-definition
- "rec_all1 f = CN rec_sign [rec_accum1 f]"
-
-definition
- "rec_all2 f = CN rec_sign [rec_accum2 f]"
-
-definition
- "rec_all3 f = CN rec_sign [rec_accum3 f]"
-
-definition
- "rec_all1_less f = (let f' = CN rec_disj [CN rec_eq [Id 3 0, Id 3 1], CN f [Id 3 0, Id 3 2]]
- in CN (rec_all2 f') [Id 2 0, Id 2 0, Id 2 1])"
-
-definition
- "rec_all2_less f = (let f' = CN rec_disj [CN rec_eq [Id 4 0, Id 4 1], CN f [Id 4 0, Id 4 2, Id 4 3]]
- in CN (rec_all3 f') [Id 3 0, Id 3 0, Id 3 1, Id 3 2])"
-
-definition
- "rec_ex1 f = CN rec_sign [rec_sigma1 f]"
-
-definition
- "rec_ex2 f = CN rec_sign [rec_sigma2 f]"
-
-text {* Dvd, Quotient, Modulo *}
-
-(* FIXME: probably all not needed *)
-definition
- "rec_dvd =
- rec_swap (CN (rec_ex2 (CN rec_eq [Id 3 2, CN rec_mult [Id 3 1, Id 3 0]])) [Id 2 0, Id 2 1, Id 2 0])"
-
-definition
- "rec_quo = (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)"
-
-definition
- "rec_mod = CN rec_minus [Id 2 0, CN rec_mult [Id 2 1, rec_quo]]"
-
-text {* Iteration *}
-
-definition
- "rec_iter f = PR (Id 2 0) (CN f [Id 3 1])"
-
-fun Iter where
- "Iter f 0 = id"
-| "Iter f (Suc n) = f \<circ> (Iter f n)"
-
-lemma Iter_comm:
- "(Iter f n) (f x) = f ((Iter f n) x)"
-by (induct n) (simp_all)
-
-lemma iter_lemma [simp]:
- "rec_eval (rec_iter f) [n, x] = Iter (\<lambda>x. rec_eval f [x]) n x"
-by (induct n) (simp_all add: rec_iter_def)
-
-section {* Correctness of Recursive Functions *}
-
-lemma constn_lemma [simp]:
- "rec_eval (constn n) xs = n"
-by (induct n) (simp_all)
-
-lemma swap_lemma [simp]:
- "rec_eval (rec_swap f) [x, y] = rec_eval f [y, x]"
-by (simp add: rec_swap_def)
-
-lemma add_lemma [simp]:
- "rec_eval rec_add [x, y] = x + y"
-by (induct x) (simp_all add: rec_add_def)
-
-lemma mult_lemma [simp]:
- "rec_eval rec_mult [x, y] = x * y"
-by (induct x) (simp_all add: rec_mult_def)
-
-lemma power_lemma [simp]:
- "rec_eval rec_power [x, y] = x ^ y"
-by (induct y) (simp_all add: rec_power_def)
-
-lemma fact_lemma [simp]:
- "rec_eval rec_fact [x] = fact x"
-by (induct x) (simp_all add: rec_fact_def)
-
-lemma pred_lemma [simp]:
- "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)
lemma sign_lemma [simp]:
"rec_eval rec_sign [x] = (if x = 0 then 0 else 1)"
@@ -436,6 +353,26 @@
"rec_eval rec_imp [x, y] = (if 0 < x \<and> y = 0 then 0 else 1)"
by (simp add: rec_imp_def)
+lemma ifz_lemma [simp]:
+ "rec_eval rec_ifz [z, x, y] = (if z = 0 then x else y)"
+by (case_tac z) (simp_all add: rec_ifz_def)
+
+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 *}
+
+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]"
+
+definition
+ "rec_le = CN rec_disj [rec_less, rec_eq]"
+
lemma less_lemma [simp]:
"rec_eval rec_less [x, y] = (if x < y then 1 else 0)"
by (simp add: rec_less_def)
@@ -444,13 +381,25 @@
"rec_eval rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
by(simp add: rec_le_def)
-lemma ifz_lemma [simp]:
- "rec_eval rec_ifz [z, x, y] = (if z = 0 then x else y)"
-by (case_tac z) (simp_all add: rec_ifz_def)
+
+section {* Summation and Product Functions *}
+
+definition
+ "rec_sigma1 f = PR (CN f [Z, Id 1 0]) (CN rec_add [Id 3 1, CN f [S, Id 3 2]])"
+
+definition
+ "rec_sigma2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_add [Id 4 1, CN f [S, Id 4 2, Id 4 3]])"
-lemma if_lemma [simp]:
- "rec_eval rec_if [z, x, y] = (if 0 < z then x else y)"
-by (simp add: rec_if_def)
+definition
+ "rec_accum1 f = PR (CN f [Z, Id 1 0]) (CN rec_mult [Id 3 1, CN f [S, Id 3 2]])"
+
+definition
+ "rec_accum2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_mult [Id 4 1, CN f [S, Id 4 2, Id 4 3]])"
+
+definition
+ "rec_accum3 f = PR (CN f [Z, Id 3 0, Id 3 1, Id 3 2])
+ (CN rec_mult [Id 5 1, CN f [S, Id 5 2, Id 5 3, Id 5 4]])"
+
lemma sigma1_lemma [simp]:
shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. (rec_eval f) [z, y])"
@@ -472,6 +421,34 @@
shows "rec_eval (rec_accum3 f) [x, y1, y2, y3] = (\<Prod> z \<le> x. (rec_eval f) [z, y1, y2, y3])"
by (induct x) (simp_all add: rec_accum3_def)
+
+section {* Bounded Quantifiers *}
+
+definition
+ "rec_all1 f = CN rec_sign [rec_accum1 f]"
+
+definition
+ "rec_all2 f = CN rec_sign [rec_accum2 f]"
+
+definition
+ "rec_all3 f = CN rec_sign [rec_accum3 f]"
+
+definition
+ "rec_all1_less f = (let f' = CN rec_disj [CN rec_eq [Id 3 0, Id 3 1], CN f [Id 3 0, Id 3 2]]
+ in CN (rec_all2 f') [Id 2 0, Id 2 0, Id 2 1])"
+
+definition
+ "rec_all2_less f = (let cond1 = CN rec_eq [Id 4 0, Id 4 1] in
+ let cond2 = CN f [Id 4 0, Id 4 2, Id 4 3] in
+ CN (rec_all3 (CN rec_disj [cond1, cond2])) [Id 3 0, Id 3 0, Id 3 1, Id 3 2])"
+
+definition
+ "rec_ex1 f = CN rec_sign [rec_sigma1 f]"
+
+definition
+ "rec_ex2 f = CN rec_sign [rec_sigma2 f]"
+
+
lemma ex1_lemma [simp]:
"rec_eval (rec_ex1 f) [x, y] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)"
by (simp add: rec_ex1_def)
@@ -504,19 +481,14 @@
apply(metis nat_less_le)+
done
+section {* Quotients *}
-lemma dvd_alt_def:
- fixes x y k:: nat
- shows "(x dvd y) = (\<exists> k \<le> y. y = x * k)"
-apply(auto simp add: dvd_def)
-apply(case_tac x)
-apply(auto)
-done
-
-lemma dvd_lemma [simp]:
- "rec_eval rec_dvd [x, y] = (if x dvd y then 1 else 0)"
-unfolding dvd_alt_def
-by (auto simp add: rec_dvd_def)
+definition
+ "rec_quo = (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"
@@ -524,9 +496,7 @@
lemma Quo0:
shows "Quo 0 y = 0"
-apply(induct y)
-apply(auto)
-done
+by (induct y) (auto)
lemma Quo1:
"x * (Quo x y) \<le> y"
@@ -566,9 +536,23 @@
shows "rec_eval rec_quo [y, x] = y div x"
by (simp add: Quo_div Quo_rec_quo)
-lemma rem_lemma [simp]:
- shows "rec_eval rec_mod [y, x] = y mod x"
-by (simp add: rec_mod_def mod_div_equality' nat_mult_commute)
+
+section {* Iteration *}
+
+definition
+ "rec_iter f = PR (Id 2 0) (CN f [Id 3 1])"
+
+fun Iter where
+ "Iter f 0 = id"
+| "Iter f (Suc n) = f \<circ> (Iter f n)"
+
+lemma Iter_comm:
+ "(Iter f n) (f x) = f ((Iter f n) x)"
+by (induct n) (simp_all)
+
+lemma iter_lemma [simp]:
+ "rec_eval (rec_iter f) [n, x] = Iter (\<lambda>x. rec_eval f [x]) n x"
+by (induct n) (simp_all add: rec_iter_def)
section {* Bounded Maximisation *}
@@ -577,8 +561,10 @@
"BMax_rec R 0 = 0"
| "BMax_rec R (Suc n) = (if R (Suc n) then (Suc n) else BMax_rec R n)"
-definition BMax_set :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat"
- where "BMax_set R x = Max ({z. z \<le> x \<and> R z} \<union> {0})"
+definition
+ BMax_set :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "BMax_set R x = Max ({z. z \<le> x \<and> R z} \<union> {0})"
lemma BMax_rec_eq1:
"BMax_rec R x = (GREATEST z. (R z \<and> z \<le> x) \<or> z = 0)"
@@ -612,6 +598,7 @@
"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 *}
text {*
@@ -697,22 +684,27 @@
apply(simp)
done
+
definition
"rec_triangle = CN rec_quo [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 triangle_lemma [simp]:
"rec_eval rec_triangle [x] = triangle x"
by (simp add: rec_triangle_def triangle_def)
-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 *}
+
definition
"rec_penc = CN rec_add [CN rec_triangle [CN rec_add [Id 2 0, Id 2 1]], Id 2 0]"
@@ -734,7 +726,8 @@
"rec_eval rec_penc [m, n] = penc m n"
by (simp add: rec_penc_def prod_encode_def)
-text {* encoding and decoding of lists of natural numbers *}
+
+text {* Encodings of Lists *}
fun
lenc :: "nat list \<Rightarrow> nat"
@@ -762,11 +755,13 @@
by (induct xs arbitrary: n rule: lenc.induct)
(auto simp add: ldec_zero nth_Cons split: nat.splits)
-
lemma lenc_length_le:
"length xs \<le> lenc xs"
by (induct xs) (simp_all add: prod_encode_def)
+
+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"
@@ -787,6 +782,8 @@
apply(simp_all)
done
+text {* Length of Encoded Lists *}
+
lemma enclen_length [simp]:
"enclen (lenc xs) = length xs"
unfolding enclen_def
@@ -803,6 +800,9 @@
"enclen 0 = 0"
by (simp add: enclen_def)
+
+text {* Recursive De3finitions for List Encodings *}
+
fun
rec_lenc :: "recf list \<Rightarrow> recf"
where
@@ -819,11 +819,11 @@
"rec_enclen = CN (rec_max1 (CN rec_not [CN rec_within [Id 2 1, CN rec_pred [Id 2 0]]])) [Id 1 0, Id 1 0]"
lemma ldec_iter:
- "ldec z n = pdec1 ((Iter pdec2 n) z) - 1"
+ "ldec z n = pdec1 (Iter pdec2 n z) - 1"
by (induct n arbitrary: z) (simp | subst Iter_comm)+
lemma within_iter:
- "within z n = (0 < (Iter pdec2 n) z)"
+ "within z n = (0 < Iter pdec2 n z)"
by (induct n arbitrary: z) (simp | subst Iter_comm)+
lemma lenc_lemma [simp]: