tm: comparison thys2/Recs.thy

equal deleted inserted replaced

-:fa3c214559b0
+:b1b47d28c295
 | "arity (Id m n) = m"
 | "arity (Cn n f gs) = n"
 | "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"
 abbreviation
 "PR f g \<equiv> Pr (arity f) f g"
 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"
 | "rec_eval S xs = Suc (xs ! 0)"
 | termi_mn: "\<lbrakk>length xs = n; terminates f (r # xs);
 rec_eval f (r # xs) = 0;
 \<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
 natural number @{text "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]:
+"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
 is greater than @{text "0"}. *}
 "rec_ifz = PR (Id 2 0) (Id 4 3)"
 definition
 "rec_if = CN rec_ifz [CN rec_not [Id 3 0], Id 3 1, Id 3 2]"
+lemma sign_lemma [simp]:
+"rec_eval rec_sign [x] = (if x = 0 then 0 else 1)"
+by (simp add: rec_sign_def)
+lemma not_lemma [simp]:
+"rec_eval rec_not [x] = (if x = 0 then 1 else 0)"
+by (simp add: rec_not_def)
+lemma eq_lemma [simp]:
+"rec_eval rec_eq [x, y] = (if x = y then 1 else 0)"
+by (simp add: rec_eq_def)
+lemma noteq_lemma [simp]:
+"rec_eval rec_noteq [x, y] = (if x \<noteq> y then 1 else 0)"
+by (simp add: rec_noteq_def)
+lemma conj_lemma [simp]:
+"rec_eval rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 else 1)"
+by (simp add: rec_conj_def)
+lemma disj_lemma [simp]:
+"rec_eval rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0 else 1)"
+by (simp add: rec_disj_def)
+lemma imp_lemma [simp]:
+"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]"
-text {* Sigma and Accum for function with one and two arguments *}
+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)"
+by(simp add: rec_le_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
 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 *}
+lemma sigma1_lemma [simp]:
+shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. (rec_eval f)  [z, y])"
+by (induct x) (simp_all add: rec_sigma1_def)
+lemma sigma2_lemma [simp]:
+shows "rec_eval (rec_sigma2 f) [x, y1, y2] = (\<Sum> z \<le> x. (rec_eval f)  [z, y1, y2])"
+by (induct x) (simp_all add: rec_sigma2_def)
+lemma accum1_lemma [simp]:
+shows "rec_eval (rec_accum1 f) [x, y] = (\<Prod> z \<le> x. (rec_eval f)  [z, y])"
+by (induct x) (simp_all add: rec_accum1_def)
+lemma accum2_lemma [simp]:
+shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. (rec_eval f)  [z, y1, y2])"
+by (induct x) (simp_all add: rec_accum2_def)
+lemma accum3_lemma [simp]:
+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
 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]]
+"rec_all2_less f = (let cond1 = CN rec_eq [Id 4 0, Id 4 1] in
-in CN (rec_all3 f') [Id 3 0, Id 3 0, Id 3 1, Id 3 2])"
+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]"
-text {* Dvd, Quotient, Modulo *}
+lemma ex1_lemma [simp]:
-(* FIXME: probably all not needed *)
+"rec_eval (rec_ex1 f) [x, y] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)"
-definition
+by (simp add: rec_ex1_def)
-"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])"
+lemma ex2_lemma [simp]:
+"rec_eval (rec_ex2 f) [x, y1, y2] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
+by (simp add: rec_ex2_def)
+lemma all1_lemma [simp]:
+"rec_eval (rec_all1 f) [x, y] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)"
+by (simp add: rec_all1_def)
+lemma all2_lemma [simp]:
+"rec_eval (rec_all2 f) [x, y1, y2] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
+by (simp add: rec_all2_def)
+lemma all3_lemma [simp]:
+"rec_eval (rec_all3 f) [x, y1, y2, y3] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2, y3]) then 1 else 0)"
+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)+
+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 *}
 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)"
-by (simp add: rec_sign_def)
-lemma not_lemma [simp]:
-"rec_eval rec_not [x] = (if x = 0 then 1 else 0)"
-by (simp add: rec_not_def)
-lemma eq_lemma [simp]:
-"rec_eval rec_eq [x, y] = (if x = y then 1 else 0)"
-by (simp add: rec_eq_def)
-lemma noteq_lemma [simp]:
-"rec_eval rec_noteq [x, y] = (if x \<noteq> y then 1 else 0)"
-by (simp add: rec_noteq_def)
-lemma conj_lemma [simp]:
-"rec_eval rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 else 1)"
-by (simp add: rec_conj_def)
-lemma disj_lemma [simp]:
-"rec_eval rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0 else 1)"
-by (simp add: rec_disj_def)
-lemma imp_lemma [simp]:
-"rec_eval rec_imp [x, y] = (if 0 < x \<and> y = 0 then 0 else 1)"
-by (simp add: rec_imp_def)
-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)"
-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)
-lemma if_lemma [simp]:
-"rec_eval rec_if [z, x, y] = (if 0 < z then x else y)"
-by (simp add: rec_if_def)
-lemma sigma1_lemma [simp]:
-shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. (rec_eval f)  [z, y])"
-by (induct x) (simp_all add: rec_sigma1_def)
-lemma sigma2_lemma [simp]:
-shows "rec_eval (rec_sigma2 f) [x, y1, y2] = (\<Sum> z \<le> x. (rec_eval f)  [z, y1, y2])"
-by (induct x) (simp_all add: rec_sigma2_def)
-lemma accum1_lemma [simp]:
-shows "rec_eval (rec_accum1 f) [x, y] = (\<Prod> z \<le> x. (rec_eval f)  [z, y])"
-by (induct x) (simp_all add: rec_accum1_def)
-lemma accum2_lemma [simp]:
-shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. (rec_eval f)  [z, y1, y2])"
-by (induct x) (simp_all add: rec_accum2_def)
-lemma accum3_lemma [simp]:
-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)
-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)
-lemma ex2_lemma [simp]:
-"rec_eval (rec_ex2 f) [x, y1, y2] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
-by (simp add: rec_ex2_def)
-lemma all1_lemma [simp]:
-"rec_eval (rec_all1 f) [x, y] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)"
-by (simp add: rec_all1_def)
-lemma all2_lemma [simp]:
-"rec_eval (rec_all2 f) [x, y1, y2] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)"
-by (simp add: rec_all2_def)
-lemma all3_lemma [simp]:
-"rec_eval (rec_all3 f) [x, y1, y2, y3] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2, y3]) then 1 else 0)"
-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)+
-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
-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)
 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)"
 lemma Quo0:
 shows "Quo 0 y = 0"
-apply(induct y)
+by (induct y) (auto)
-apply(auto)
-done
 lemma Quo1:
 "x * (Quo x y) \<le> y"
 by (induct y) (simp_all)
 lemma quo_lemma [simp]:
 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"
+section {* Iteration *}
-by (simp add: rec_mod_def mod_div_equality' nat_mult_commute)
+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 *}
 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)"
-definition BMax_set :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat"
+definition
-where "BMax_set R x = Max ({z. z \<le> x \<and> R z} \<union> {0})"
+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)"
 apply(induct x)
 apply(auto intro: Greatest_equality Greatest_equality[symmetric])
 "rec_max2 f = PR (constn 0) (CN rec_ifz [CN f [CN S [Id 4 0], Id 4 2, Id 4 3], CN S [Id 4 0], Id 4 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 *}
 text {*
 We use Cantor's pairing function from Nat_Bijection.
 apply(simp only: w_aux)
 apply(rule y_aux)
 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]"
 definition
 "rec_pdec1 = CN rec_minus [Id 1 0, CN rec_triangle [CN rec_max_triangle [Id 1 0]]]"
 lemma penc_lemma [simp]:
 "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"
 where
 "lenc [] = 0"
 lemma list_encode_inverse:
 "ldec (lenc xs) n = (if n < length xs then xs ! n else 0)"
 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"
 apply(simp_all add: prod_encode_def)
 apply(case_tac xs)
 apply(simp_all)
 done
+text {* Length of Encoded Lists *}
 lemma enclen_length [simp]:
 "enclen (lenc xs) = length xs"
 unfolding enclen_def
 apply(simp add: BMax_rec_eq1)
 apply(rule Greatest_equality)
 lemma enclen_zero [simp]:
 "enclen 0 = 0"
 by (simp add: enclen_def)
+text {* Recursive De3finitions for List Encodings *}
 fun
 rec_lenc :: "recf list \<Rightarrow> recf"
 where
 "rec_lenc [] = Z"
 | "rec_lenc (f # fs) = CN rec_penc [CN S [f], rec_lenc fs]"
 definition
 "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]:
 "rec_eval (rec_lenc fs) xs = lenc (map (\<lambda>f. rec_eval f xs) fs)"
 by (induct fs) (simp_all)

changeset 266	b1b47d28c295
parent 265	fa3c214559b0
child 269	fa40fd8abb54