equal
deleted
inserted
replaced
1 theory Recs |
1 theory Recs |
2 imports Main Fact |
2 imports Main |
3 "~~/src/HOL/Number_Theory/Primes" |
3 "~~/src/HOL/Number_Theory/Primes" |
4 "~~/src/HOL/Library/Nat_Bijection" |
4 "~~/src/HOL/Library/Nat_Bijection" |
5 "~~/src/HOL/Library/Discrete" |
5 "~~/src/HOL/Library/Discrete" |
6 begin |
6 begin |
7 |
7 |
8 declare One_nat_def[simp del] |
8 declare One_nat_def[simp del] |
43 "(\<Prod>i < Suc n. f i) = (\<Prod>i < n. f i) * f n" |
43 "(\<Prod>i < Suc n. f i) = (\<Prod>i < n. f i) * f n" |
44 by (simp add:lessThan_Suc mult_ac) |
44 by (simp add:lessThan_Suc mult_ac) |
45 |
45 |
46 lemma setsum_add_nat_ivl2: "n \<le> p \<Longrightarrow> |
46 lemma setsum_add_nat_ivl2: "n \<le> p \<Longrightarrow> |
47 setsum f {..<n} + setsum f {n..p} = setsum f {..p::nat}" |
47 setsum f {..<n} + setsum f {n..p} = setsum f {..p::nat}" |
48 apply(subst setsum_Un_disjoint[symmetric]) |
48 apply(subst setsum.union_disjoint[symmetric]) |
49 apply(auto simp add: ivl_disj_un_one) |
49 apply(auto simp add: ivl_disj_un_one) |
50 done |
50 done |
51 |
51 |
52 lemma setsum_eq_zero [simp]: |
52 lemma setsum_eq_zero [simp]: |
53 fixes f::"nat \<Rightarrow> nat" |
53 fixes f::"nat \<Rightarrow> nat" |
54 shows "(\<Sum>i < n. f i) = 0 \<longleftrightarrow> (\<forall>i < n. f i = 0)" |
54 shows "(\<Sum>i < n. f i) = 0 \<longleftrightarrow> (\<forall>i < n. f i = 0)" |
247 |
247 |
248 definition |
248 definition |
249 "rec_fact = CN rec_fact_aux [Id 1 0, Id 1 0]" |
249 "rec_fact = CN rec_fact_aux [Id 1 0, Id 1 0]" |
250 |
250 |
251 definition |
251 definition |
252 "rec_pred = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]" |
252 "rec_predi = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]" |
253 |
253 |
254 definition |
254 definition |
255 "rec_minus = rec_swap (PR (Id 1 0) (CN rec_pred [Id 3 1]))" |
255 "rec_minus = rec_swap (PR (Id 1 0) (CN rec_predi [Id 3 1]))" |
256 |
256 |
257 lemma constn_lemma [simp]: |
257 lemma constn_lemma [simp]: |
258 "rec_eval (constn n) xs = n" |
258 "rec_eval (constn n) xs = n" |
259 by (induct n) (simp_all) |
259 by (induct n) (simp_all) |
260 |
260 |
281 lemma fact_lemma [simp]: |
281 lemma fact_lemma [simp]: |
282 "rec_eval rec_fact [x] = fact x" |
282 "rec_eval rec_fact [x] = fact x" |
283 by (simp add: rec_fact_def) |
283 by (simp add: rec_fact_def) |
284 |
284 |
285 lemma pred_lemma [simp]: |
285 lemma pred_lemma [simp]: |
286 "rec_eval rec_pred [x] = x - 1" |
286 "rec_eval rec_predi [x] = x - 1" |
287 by (induct x) (simp_all add: rec_pred_def) |
287 by (induct x) (simp_all add: rec_predi_def) |
288 |
288 |
289 lemma minus_lemma [simp]: |
289 lemma minus_lemma [simp]: |
290 "rec_eval rec_minus [x, y] = x - y" |
290 "rec_eval rec_minus [x, y] = x - y" |
291 by (induct y) (simp_all add: rec_minus_def) |
291 by (induct y) (simp_all add: rec_minus_def) |
292 |
292 |
821 where |
821 where |
822 "rec_lenc [] = Z" |
822 "rec_lenc [] = Z" |
823 | "rec_lenc (f # fs) = CN rec_penc [CN S [f], rec_lenc fs]" |
823 | "rec_lenc (f # fs) = CN rec_penc [CN S [f], rec_lenc fs]" |
824 |
824 |
825 definition |
825 definition |
826 "rec_ldec = CN rec_pred [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]" |
826 "rec_ldec = CN rec_predi [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]" |
827 |
827 |
828 definition |
828 definition |
829 "rec_within = CN rec_less [Z, rec_swap (rec_iter rec_pdec2)]" |
829 "rec_within = CN rec_less [Z, rec_swap (rec_iter rec_pdec2)]" |
830 |
830 |
831 definition |
831 definition |
832 "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]" |
832 "rec_enclen = CN (rec_max1 (CN rec_not [CN rec_within [Id 2 1, CN rec_predi [Id 2 0]]])) [Id 1 0, Id 1 0]" |
833 |
833 |
834 lemma ldec_iter: |
834 lemma ldec_iter: |
835 "ldec z n = pdec1 (Iter pdec2 n z) - 1" |
835 "ldec z n = pdec1 (Iter pdec2 n z) - 1" |
836 by (induct n arbitrary: z) (simp | subst Iter_comm)+ |
836 by (induct n arbitrary: z) (simp | subst Iter_comm)+ |
837 |
837 |