# HG changeset patch # User Christian Urban # Date 1366934867 -3600 # Node ID e59e549e6ab66fea431aa900a8e83b734554ffb5 # Parent 696081f445c2d465a07c744494ffee9a59b5fb3e uodated diff -r 696081f445c2 -r e59e549e6ab6 thys/Recs.thy --- a/thys/Recs.thy Thu Apr 25 21:37:05 2013 +0100 +++ b/thys/Recs.thy Fri Apr 26 01:07:47 2013 +0100 @@ -47,6 +47,20 @@ using assms by (induct n) (auto) +lemma setsum_one_le: + fixes n::nat + assumes "\i \ n. f i \ 1" + shows "(\i \ n. f i) \ Suc n" +using assms +by (induct n) (auto) + +lemma setsum_eq_one_le: + fixes n::nat + assumes "\i \ n. f i = 1" + shows "(\i \ n. f i) = Suc n" +using assms +by (induct n) (auto) + lemma setsum_least_eq: fixes n p::nat assumes h0: "p \ n" @@ -428,19 +442,124 @@ "rec_eval rec_prime [x] = (if prime x then 1 else 0)" by (simp add: rec_prime_def Let_def prime_alt_def) +definition + "rec_minr2 f = rec_sigma2 (rec_accum2 (CN rec_not [f]))" + +fun Minr2 :: "(nat list \ bool) \ nat list \ nat" + where "Minr2 R (x # ys) = Min ({z | z. z \ x \ R (z # ys)} \ {Suc x})" + +lemma minr_lemma [simp]: +shows "rec_eval (rec_minr2 f) [x, y1, y2] = Minr2 (\xs. (0 < rec_eval f xs)) [x, y1, y2]" +apply(simp only: rec_minr2_def) +apply(simp) +apply(rule sym) +apply(rule Min_eqI) +apply(auto)[1] +apply(simp) +apply(erule disjE) +apply(simp) +apply(rule setsum_one_le) +apply(auto)[1] +apply(rule setprod_one_le) +apply(auto)[1] +apply(subst setsum_cut_off_le) +apply(auto)[2] +apply(rule setsum_one_less) +apply(auto)[1] +apply(rule setprod_one_le) +apply(auto)[1] +apply(simp) +thm setsum_eq_one_le +apply(subgoal_tac "(\z\x. (\z\z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)) \ + (\ (\z\x. (\z\z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)))") +prefer 2 +apply(auto)[1] +apply(erule disjE) +apply(rule disjI1) +apply(rule setsum_eq_one_le) +apply(simp) +apply(rule disjI2) +apply(simp) +apply(clarify) +apply(subgoal_tac "\l. l = (LEAST z. 0 < rec_eval f [z, y1, y2])") +defer +apply metis +apply(erule exE) +apply(subgoal_tac "l \ x") +defer +apply (metis not_leE not_less_Least order_trans) +apply(subst setsum_least_eq) +apply(rotate_tac 4) +apply(assumption) +apply(auto)[1] +apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])") +prefer 2 +apply(auto)[1] +apply(rotate_tac 5) +apply(drule not_less_Least) +apply(auto)[1] +apply(auto) +apply(rule_tac x="(LEAST z. 0 < rec_eval f [z, y1, y2])" in exI) +apply(simp) +apply (metis LeastI_ex) +apply(subst setsum_least_eq) +apply(rotate_tac 3) +apply(assumption) +apply(simp) +apply(auto)[1] +apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])") +prefer 2 +apply(auto)[1] +apply (metis neq0_conv not_less_Least) +apply(auto)[1] +apply (metis (mono_tags) LeastI_ex) +by (metis LeastI_ex) + +definition quo :: "nat \ nat \ nat" + where + "quo x y = (if y = 0 then 0 else x div y)" + + +definition + "rec_quo = CN rec_mult [CN rec_sign [id 2 1], + CN (rec_minr2 (CN rec_less [id 3 1, CN rec_mult [CN s [id 3 0], id 3 2]])) + [id 2 0, id 2 0, id 2 1]]" + +lemma div_lemma [simp]: + "rec_eval rec_quo [x, y] = quo x y" +apply(simp add: rec_quo_def quo_def) +apply(rule impI) +apply(rule Min_eqI) +apply(auto)[1] +apply(simp) +apply(erule disjE) +apply(simp) +apply(auto)[1] +apply (metis div_le_dividend le_SucI) +defer +apply(simp) +apply(auto)[1] +apply (metis mult_Suc_right nat_mult_commute split_div_lemma) +apply(auto)[1] + +apply (smt div_le_dividend fst_divmod_nat) +apply(simp add: quo_def) +apply(auto)[1] + +apply(auto) fun Minr :: "(nat list \ bool) \ nat \ nat \ nat" where "Minr R x y = (let setx = {z | z. z \ x \ R [z, y]} in if (setx = {}) then (Suc x) else (Min setx))" definition - "rec_minr f = rec_sigma (rec_accum (CN rec_not [f]))" + "rec_minr f = rec_sigma1 (rec_accum1 (CN rec_not [f]))" lemma minr_lemma [simp]: shows "rec_eval (rec_minr f) [x, y] = Minr (\xs. (0 < rec_eval f xs)) x y" apply(simp only: rec_minr_def) -apply(simp only: sigma_lemma) -apply(simp only: accum_lemma) +apply(simp only: sigma1_lemma) +apply(simp only: accum1_lemma) apply(subst rec_eval.simps) apply(simp only: map.simps nth) apply(simp only: Minr.simps Let_def) @@ -495,55 +614,18 @@ apply(auto) by (metis (mono_tags) LeastI_ex) -(* -lemma prime_alt_iff: - fixes x::nat - shows "prime x \ 1 < x \ (\u < x. \v < x. x \ u * v)" -unfolding prime_nat_simp dvd_def -apply(auto) -by (smt n_less_m_mult_n nat_mult_commute) -lemma prime_alt2_iff: - fixes x::nat - shows "prime x \ 1 < x \ (\u \ x - 1. \v \ x - 1. x \ u * v)" -unfolding prime_alt_iff -sorry -*) +fun Minr2 :: "(nat list \ bool) \ nat \ nat \ nat" + where "Minr2 R x y = (let setx = {z | z. z \ x \ R [z, y]} in + Min (setx \ {Suc x}))" -definition - "rec_prime = CN rec_conj - [CN rec_less [constn 1, id 1 0], - CN (rec_all (CN (rec_all2 (CN rec_noteq [id 3 2, CN rec_mult [id 3 1, id 3 0]])) - [CN rec_pred [id 2 1], id 2 0, id 2 1])) - [CN rec_pred [id 1 0], id 1 0]]" - -lemma prime_lemma [simp]: - "rec_eval rec_prime [x] = (if prime x then 1 else 0)" -apply(rule trans) -apply(simp add: rec_prime_def) -apply(simp only: prime_nat_def dvd_def) +lemma Minr2_Minr: + "Minr2 R x y = Minr R x y" apply(auto) -apply(drule_tac x="m" in spec) -apply(auto) -apply(case_tac m) -apply(auto) -apply(case_tac nat) -apply(auto) -apply(case_tac k) -apply(auto) -apply(case_tac nat) -apply(auto) +apply (metis (lifting, no_types) Min_singleton empty_Collect_eq) +apply(rule min_absorb2) +apply(subst Min_le_iff) +apply(auto) done -lemma if_zero [simp]: - "(0::nat) < (if P then 1 else 0) = P" -by (simp) - -lemma if_cong: - "P = Q \ (if P then 1 else (0::nat)) = (if Q then 1 else 0)" -by simp - - - - end \ No newline at end of file