--- 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 "\<forall>i \<le> n. f i \<le> 1" 
+  shows "(\<Sum>i \<le> n. f i) \<le> Suc n"  
+using assms
+by (induct n) (auto)
+
+lemma setsum_eq_one_le:
+  fixes n::nat
+  assumes "\<forall>i \<le> n. f i = 1" 
+  shows "(\<Sum>i \<le> n. f i) = Suc n"  
+using assms
+by (induct n) (auto)
+
 lemma setsum_least_eq:
   fixes n p::nat
   assumes h0: "p \<le> 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 \<Rightarrow> bool) \<Rightarrow> nat list \<Rightarrow> nat"
+  where "Minr2 R (x # ys) = Min ({z | z. z \<le> x \<and> R (z # ys)} \<union> {Suc x})"
+
+lemma minr_lemma [simp]:
+shows "rec_eval (rec_minr2 f) [x, y1, y2] = Minr2 (\<lambda>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 "(\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)) \<or>
+                   (\<not> (\<forall>z\<le>x. (\<Prod>z\<le>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 "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y1, y2])")
+defer
+apply metis
+apply(erule exE)
+apply(subgoal_tac "l \<le> 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 \<Rightarrow> nat \<Rightarrow> 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 \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
   where "Minr R x y = (let setx = {z | z. z \<le> x \<and> 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 (\<lambda>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 \<longleftrightarrow> 1 < x \<and> (\<forall>u < x. \<forall>v < x. x \<noteq> 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 \<longleftrightarrow> 1 < x \<and> (\<forall>u \<le> x - 1. \<forall>v \<le> x - 1. x \<noteq> u * v)"
-unfolding prime_alt_iff
-sorry
-*)
+fun Minr2 :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where "Minr2 R x y = (let setx = {z | z. z \<le> x \<and> R [z, y]} in 
+                        Min (setx \<union> {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 \<Longrightarrow> (if P then 1 else (0::nat)) = (if Q then 1 else 0)"
-by simp
-
-
-
-
 end
\ No newline at end of file