# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1367322791 -3600
# Node ID ac32cc069e3082ae4853ef12e5b266d9252fe0ab
# Parent  4a943f0fe1b089dc41251d76157010919b1ac6a0
added max and lg functions

diff -r 4a943f0fe1b0 -r ac32cc069e30 thys/Recs.thy
--- a/thys/Recs.thy	Mon Apr 29 11:02:23 2013 +0100
+++ b/thys/Recs.thy	Tue Apr 30 12:53:11 2013 +0100
@@ -4,8 +4,8 @@
 
 lemma if_zero_one [simp]:
   "(if P then 1 else 0) = (0::nat) \<longleftrightarrow> \<not> P"
-  "(if P then 0 else 1) = (0::nat) \<longleftrightarrow> P"
   "(0::nat) < (if P then 1 else 0) = P"
+  "(if P then 0 else 1) = (if \<not>P then 1 else (0::nat))"
 by (simp_all)
 
 lemma nth:
@@ -15,10 +15,15 @@
   "(x # y # z # u # xs) ! 3 = u"
 by (simp_all)
 
-lemma setprod_atMost_Suc[simp]: "(\<Prod>i \<le> Suc n. f i) = (\<Prod>i \<le> n. f i) * f(Suc n)"
+
+section {* Some auxiliary lemmas about @{text "\<Sum>"} and @{text "\<Prod>"} *}
+
+lemma setprod_atMost_Suc[simp]: 
+  "(\<Prod>i \<le> Suc n. f i) = (\<Prod>i \<le> n. f i) * f(Suc n)"
 by(simp add:atMost_Suc mult_ac)
 
-lemma setprod_lessThan_Suc[simp]: "(\<Prod>i < Suc n. f i) = (\<Prod>i < n. f i) * f n"
+lemma setprod_lessThan_Suc[simp]: 
+  "(\<Prod>i < Suc n. f i) = (\<Prod>i < n. f i) * f n"
 by (simp add:lessThan_Suc mult_ac)
 
 lemma setsum_add_nat_ivl2: "n \<le> p  \<Longrightarrow>
@@ -27,17 +32,16 @@
 apply(auto simp add: ivl_disj_un_one)
 done
 
-
 lemma setsum_eq_zero [simp]:
-  fixes n::nat
-  shows "(\<Sum>i < n. f i) = (0::nat) \<longleftrightarrow> (\<forall>i < n. f i = 0)" 
-        "(\<Sum>i \<le> n. f i) = (0::nat) \<longleftrightarrow> (\<forall>i \<le> n. f i = 0)" 
+  fixes f::"nat \<Rightarrow> nat"
+  shows "(\<Sum>i < n. f i) = 0 \<longleftrightarrow> (\<forall>i < n. f i = 0)" 
+        "(\<Sum>i \<le> n. f i) = 0 \<longleftrightarrow> (\<forall>i \<le> n. f i = 0)" 
 by (auto)
 
 lemma setprod_eq_zero [simp]:
-  fixes n::nat
-  shows "(\<Prod>i < n. f i) = (0::nat) \<longleftrightarrow> (\<exists>i < n. f i = 0)" 
-        "(\<Prod>i \<le> n. f i) = (0::nat) \<longleftrightarrow> (\<exists>i \<le> n. f i = 0)" 
+  fixes f::"nat \<Rightarrow> nat"
+  shows "(\<Prod>i < n. f i) = 0 \<longleftrightarrow> (\<exists>i < n. f i = 0)" 
+        "(\<Prod>i \<le> n. f i) = 0 \<longleftrightarrow> (\<exists>i \<le> n. f i = 0)" 
 by (auto)
 
 lemma setsum_one_less:
@@ -62,7 +66,7 @@
 by (induct n) (auto)
 
 lemma setsum_least_eq:
-  fixes n p::nat
+  fixes f::"nat \<Rightarrow> nat"
   assumes h0: "p \<le> n"
   assumes h1: "\<forall>i \<in> {..<p}. f i = 1"
   assumes h2: "\<forall>i \<in> {p..n}. f i = 0"
@@ -78,31 +82,32 @@
   finally show "(\<Sum>i \<le> n. f i) = p" using eq_p by simp
 qed
 
+lemma nat_mult_le_one:
+  fixes m n::nat
+  assumes "m \<le> 1" "n \<le> 1"
+  shows "m * n \<le> 1"
+using assms by (induct n) (auto)
+
 lemma setprod_one_le:
-  fixes n::nat
-  assumes "\<forall>i \<le> n. f i \<le> (1::nat)" 
+  fixes f::"nat \<Rightarrow> nat"
+  assumes "\<forall>i \<le> n. f i \<le> 1" 
   shows "(\<Prod>i \<le> n. f i) \<le> 1" 
-using assms
-apply(induct n) 
-apply(auto)
-by (metis One_nat_def eq_iff le_0_eq le_SucE mult_0 nat_mult_1)
+using assms by (induct n) (auto intro: nat_mult_le_one)
 
 lemma setprod_greater_zero:
-  fixes n::nat
-  assumes "\<forall>i \<le> n. f i \<ge> (0::nat)" 
+  fixes f::"nat \<Rightarrow> nat"
+  assumes "\<forall>i \<le> n. f i \<ge> 0" 
   shows "(\<Prod>i \<le> n. f i) \<ge> 0" 
-using assms
-by (induct n) (auto)
+using assms by (induct n) (auto)
 
 lemma setprod_eq_one:
-  fixes n::nat
+  fixes f::"nat \<Rightarrow> nat"
   assumes "\<forall>i \<le> n. f i = Suc 0" 
   shows "(\<Prod>i \<le> n. f i) = Suc 0" 
-using assms
-by (induct n) (auto)
+using assms by (induct n) (auto)
 
 lemma setsum_cut_off_less:
-  fixes n::nat
+  fixes f::"nat \<Rightarrow> nat"
   assumes h1: "m \<le> n"
   and     h2: "\<forall>i \<in> {m..<n}. f i = 0"
   shows "(\<Sum>i < n. f i) = (\<Sum>i < m. f i)"
@@ -116,7 +121,7 @@
 qed
 
 lemma setsum_cut_off_le:
-  fixes n::nat
+  fixes f::"nat \<Rightarrow> nat"
   assumes h1: "m \<le> n"
   and     h2: "\<forall>i \<in> {m..n}. f i = 0"
   shows "(\<Sum>i \<le> n. f i) = (\<Sum>i < m. f i)"
@@ -136,18 +141,21 @@
 by (induct n) (simp_all)
 
 
-datatype recf =  z
-              |  s
-              |  id nat nat
+
+section {* Recursive Functions *}
+
+datatype recf =  Z
+              |  S
+              |  Id nat nat
               |  Cn nat recf "recf list"
               |  Pr nat recf recf
               |  Mn nat recf 
 
 fun arity :: "recf \<Rightarrow> nat"
   where
-  "arity z = 1" 
-| "arity s = 1"
-| "arity (id m n) = m"
+  "arity Z = 1" 
+| "arity S = 1"
+| "arity (Id m n) = m"
 | "arity (Cn n f gs) = n"
 | "arity (Pr n f g) = Suc n"
 | "arity (Mn n f) = n"
@@ -160,9 +168,9 @@
 
 fun rec_eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
   where
-  "rec_eval z xs = 0" 
-| "rec_eval s xs = Suc (xs ! 0)" 
-| "rec_eval (id m n) xs = xs ! n" 
+  "rec_eval Z xs = 0" 
+| "rec_eval S xs = Suc (xs ! 0)" 
+| "rec_eval (Id m n) xs = xs ! n" 
 | "rec_eval (Cn n f gs) xs = rec_eval f (map (\<lambda>x. rec_eval x xs) gs)" 
 | "rec_eval (Pr n f g) (0 # xs) = rec_eval f xs"
 | "rec_eval (Pr n f g) (Suc x # xs) = 
@@ -172,9 +180,9 @@
 inductive 
   terminates :: "recf \<Rightarrow> nat list \<Rightarrow> bool"
 where
-  termi_z: "terminates z [n]"
-| termi_s: "terminates s [n]"
-| termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminates (id m n) xs"
+  termi_z: "terminates Z [n]"
+| termi_s: "terminates S [n]"
+| termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminates (Id m n) xs"
 | termi_cn: "\<lbrakk>terminates f (map (\<lambda>g. rec_eval g xs) gs); 
               \<forall>g \<in> set gs. terminates g xs; length xs = n\<rbrakk> \<Longrightarrow> terminates (Cn n f gs) xs"
 | termi_pr: "\<lbrakk>\<forall> y < x. terminates g (y # (rec_eval (Pr n f g) (y # xs) # xs));
@@ -194,49 +202,50 @@
 *}
 fun constn :: "nat \<Rightarrow> recf"
   where
-  "constn 0 = z"  |
-  "constn (Suc n) = CN s [constn n]"
+  "constn 0 = Z"  |
+  "constn (Suc n) = CN S [constn n]"
 
 definition
-  "rec_swap f = CN f [id 2 1, id 2 0]"
+  "rec_swap f = CN f [Id 2 1, Id 2 0]"
 
 definition
-  "rec_add = PR (id 1 0) (CN s [id 3 1])"
+  "rec_add = PR (Id 1 0) (CN S [Id 3 1])"
 
 definition 
-  "rec_mult = PR z (CN rec_add [id 3 1, id 3 2])"
+  "rec_mult = PR Z (CN rec_add [Id 3 1, Id 3 2])"
 
 definition 
-  "rec_power_swap = PR (constn 1) (CN rec_mult [id 3 1, id 3 2])"
+  "rec_power_swap = PR (constn 1) (CN rec_mult [Id 3 1, Id 3 2])"
 
 definition
   "rec_power = rec_swap rec_power_swap"
 
 definition
-  "rec_fact = PR (constn 1) (CN rec_mult [CN s [id 3 0], id 3 1])"
+  "rec_fact = PR (constn 1) (CN rec_mult [CN S [Id 3 0], Id 3 1])"
 
 definition 
-  "rec_pred = CN (PR z (id 3 0)) [id 1 0, id 1 0]"
+  "rec_pred = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]"
 
 definition 
-  "rec_minus_swap = (PR (id 1 0) (CN rec_pred [id 3 1]))"
+  "rec_minus_swap = (PR (Id 1 0) (CN rec_pred [Id 3 1]))"
 
 definition
   "rec_minus = rec_swap rec_minus_swap"
 
 text {* Sign function returning 1 when the input argument is greater than @{text "0"}. *}
-definition 
-  "rec_sign = CN rec_minus [constn 1, CN rec_minus [constn 1, id 1 0]]"
 
 definition 
-  "rec_not = CN rec_minus [constn 1, id 1 0]"
+  "rec_sign = CN rec_minus [constn 1, CN rec_minus [constn 1, Id 1 0]]"
+
+definition 
+  "rec_not = CN rec_minus [constn 1, Id 1 0]"
 
 text {*
   @{text "rec_eq"} compares two arguments: returns @{text "1"}
   if they are equal; @{text "0"} otherwise. *}
 definition 
   "rec_eq = CN rec_minus 
-             [CN (constn 1) [id 2 0], 
+             [CN (constn 1) [Id 2 0], 
               CN rec_add [rec_minus, rec_swap rec_minus]]"
 
 definition 
@@ -249,7 +258,12 @@
   "rec_disj = CN rec_sign [rec_add]"
 
 definition 
-  "rec_imp = CN rec_disj [CN rec_not [id 2 0], id 2 1]"
+  "rec_imp = CN rec_disj [CN rec_not [Id 2 0], Id 2 1]"
+
+text {* @{term "rec_ifz [z, x, y]"} returns x if z is zero,
+  y otherwise *}
+definition 
+  "rec_ifz = PR (Id 2 0) (Id 4 3)"
 
 text {*
   @{text "rec_less"} compares two arguments and returns @{text "1"} if
@@ -263,16 +277,16 @@
 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]])"
+  "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]])"
+  "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]])"
+  "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]])"
+  "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]])"
 
 text {* Bounded quantifiers for one and two arguments *}
 
@@ -291,11 +305,13 @@
 text {* Dvd *}
 
 definition 
-  "rec_dvd_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]"  
+  "rec_dvd_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_dvd = rec_swap rec_dvd_swap" 
 
+
+
 section {* Correctness of Recursive Functions *}
 
 lemma constn_lemma [simp]: 
@@ -374,6 +390,9 @@
   "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 sigma1_lemma [simp]: 
   shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. (rec_eval f)  [z, y])"
@@ -409,7 +428,8 @@
 
 
 lemma dvd_alt_def:
-  "(x dvd y) = (\<exists>k\<le>y. y = x * (k::nat))"
+  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)
@@ -424,33 +444,308 @@
   "rec_eval rec_dvd [x, y] = (if x dvd y then 1 else 0)"
 by (simp add: rec_dvd_def)
 
-definition 
-  "rec_prime = 
-    (let conj1 = CN rec_less [constn 1, id 1 0] in
-     let disj  = CN rec_disj [CN rec_eq [id 2 0, constn 1], rec_eq] in
-     let imp   = CN rec_imp [rec_dvd, disj] in
-     let conj2 = CN (rec_all1 imp) [id 1 0, id 1 0] in
-     CN rec_conj [conj1, conj2])"
+
+section {* Prime Numbers *}
 
 lemma prime_alt_def:
   fixes p::nat
   shows "prime p = (1 < p \<and> (\<forall>m \<le> p. m dvd p \<longrightarrow> m = 1 \<or> m = p))"
 apply(auto simp add: prime_nat_def dvd_def)
-by (metis One_nat_def le_neq_implies_less less_SucI less_Suc_eq_0_disj less_Suc_eq_le mult_is_0 n_less_n_mult_m not_less_eq_eq)
+apply(drule_tac x="k" in spec)
+apply(auto)
+done
+
+definition 
+  "rec_prime = 
+    (let conj1 = CN rec_less [constn 1, Id 1 0] in
+     let disj  = CN rec_disj [CN rec_eq [Id 2 0, constn 1], rec_eq] in
+     let imp   = CN rec_imp [rec_dvd, disj] in
+     let conj2 = CN (rec_all1 imp) [Id 1 0, Id 1 0] in
+     CN rec_conj [conj1, conj2])"
 
 lemma prime_lemma [simp]: 
   "rec_eval rec_prime [x] = (if prime x then 1 else 0)"
-by (simp add: rec_prime_def Let_def prime_alt_def)
+by (auto simp add: rec_prime_def Let_def prime_alt_def)
+
+section {* Bounded Min and 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"
+  where "BMax_set R x = Max ({z | z. z \<le> x \<and> R z} \<union> {0})"
+
+definition (in ord)
+  Great :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "GREAT " 10) where
+  "Great P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> y \<le> x))"
+
+lemma Great_equality:
+  fixes x::nat
+  assumes "P x" "\<And>y. P y \<Longrightarrow> y \<le> x"
+  shows "Great P = x"
+unfolding Great_def 
+using assms 
+by(rule_tac the_equality) (auto intro: le_antisym)
+
+lemma BMax_rec_eq1:
+ "BMax_rec R x = (GREAT z. (R z \<and> z \<le> x) \<or> z = 0)"
+apply(induct x)
+apply(auto intro: Great_equality Great_equality[symmetric])
+apply(simp add: le_Suc_eq)
+by metis
+
+lemma BMax_rec_eq2:
+  "BMax_rec R x = Max ({z | z. z \<le> x \<and> R z} \<union> {0})"
+apply(induct x)
+apply(auto intro: Max_eqI Max_eqI[symmetric])
+apply(simp add: le_Suc_eq)
+by metis
+
+definition 
+  "rec_max1 f = PR (constn 0)
+                   (CN rec_ifz [CN f [CN S [Id 3 0], Id 3 2], CN S [Id 4 0], Id 4 1])"
+ 
+lemma max1_lemma [simp]:
+  "rec_eval (rec_max1 f) [x, y] = BMax_rec (\<lambda>u. rec_eval f [u, y] = 0) x"
+by (induct x) (simp_all add: rec_max1_def)
+
+definition 
+  "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)
+
+definition
+  "rec_lg = 
+     (let calc = CN rec_not [CN rec_le [CN rec_power [Id 3 2, Id 3 0], Id 3 1]] in
+      let max  = CN (rec_max2 calc) [Id 2 0, Id 2 0, Id 2 1] in
+      let cond = CN rec_conj [CN rec_less [constn 1, Id 2 0], CN rec_less [constn 1, Id 2 1]] 
+      in CN rec_ifz [cond, Z, max])"
+
+definition
+  "Lg x y = (if 1 < x \<and> 1 < y then BMax_rec (\<lambda>u. y ^ u \<le> x) x else 0)"
+
+lemma lg_lemma:
+  "rec_eval rec_lg [x, y] = Lg x y"
+by (simp add: rec_lg_def Lg_def Let_def)
+
+
+
+
+
+fun mtest where
+  "mtest R 0 = if R 0 then 0 else 1"
+| "mtest R (Suc n) = (if R n then mtest R n else (Suc n))"
+
+
+lemma 
+  "rec_eval (rec_maxr2 f) [x, y1, y2] = XXX"
+apply(simp only: rec_maxr2_def)
+apply(case_tac x)
+apply(clarify)
+apply(subst rec_eval.simps)
+apply(simp only: constn_lemma)
+defer
+apply(clarify)
+apply(subst rec_eval.simps)
+apply(simp only: rec_maxr2_def[symmetric])
+apply(subst rec_eval.simps)
+apply(simp only: map.simps nth)
+apply(subst rec_eval.simps)
+apply(simp only: map.simps nth)
+apply(subst rec_eval.simps)
+apply(simp only: map.simps nth)
+apply(subst rec_eval.simps)
+apply(simp only: map.simps nth)
+apply(subst rec_eval.simps)
+apply(simp only: map.simps nth)
+apply(subst rec_eval.simps)
+apply(simp only: map.simps nth)
+
 
 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})"
+definition
+  "rec_maxr2 f = rec_sigma2 (CN rec_sign [CN (rec_sigma2 f) [S]])"
+
+definition Minr :: "(nat \<Rightarrow> nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat"
+  where "Minr R x ys = Min ({z | z. z \<le> x \<and> R z ys} \<union> {Suc x})"
+
+definition Maxr :: "(nat \<Rightarrow> nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat"
+  where "Maxr R x ys = Max ({z | z. z \<le> x \<and> R z ys} \<union> {0})"
+
+lemma rec_minr2_le_Suc:
+  "rec_eval (rec_minr2 f) [x, y1, y2] \<le> Suc x"
+apply(simp add: rec_minr2_def)
+apply(auto intro!: setsum_one_le setprod_one_le)
+done
+
+lemma rec_minr2_eq_Suc:
+  assumes "\<forall>z \<le> x. rec_eval f [z, y1, y2] = 0"
+  shows "rec_eval (rec_minr2 f) [x, y1, y2] = Suc x"
+using assms by (simp add: rec_minr2_def)
+
+lemma rec_minr2_le:
+  assumes h1: "y \<le> x" 
+  and     h2: "0 < rec_eval f [y, y1, y2]" 
+  shows "rec_eval (rec_minr2 f) [x, y1, y2] \<le> y"
+apply(simp add: rec_minr2_def)
+apply(subst setsum_cut_off_le[OF h1])
+using h2 apply(auto)
+apply(auto intro!: setsum_one_less setprod_one_le)
+done
+
+(* ??? *)
+lemma setsum_eq_one_le2:
+  fixes n::nat
+  assumes "\<forall>i \<le> n. f i \<le> 1" 
+  shows "((\<Sum>i \<le> n. f i) \<ge> Suc n) \<Longrightarrow> (\<forall>i \<le> n. f i = 1)"  
+using assms
+apply(induct n)
+apply(simp add: One_nat_def)
+apply(simp)
+apply(auto simp add: One_nat_def)
+apply(drule_tac x="Suc n" in spec)
+apply(auto)
+by (metis le_Suc_eq)
+
+
+lemma rec_min2_not:
+  assumes "rec_eval (rec_minr2 f) [x, y1, y2] = Suc x"
+  shows "\<forall>z \<le> x. rec_eval f [z, y1, y2] = 0"
+using assms
+apply(simp add: rec_minr2_def)
+apply(subgoal_tac "\<forall>i \<le> x. (\<Prod>z\<le>i. if rec_eval f [z, y1, y2] = 0 then 1 else 0) = (1::nat)")
+apply(simp)
+apply (metis atMost_iff le_refl zero_neq_one)
+apply(rule setsum_eq_one_le2)
+apply(auto)
+apply(rule setprod_one_le)
+apply(auto)
+done
+
+lemma disjCI2:
+  assumes "~P ==> Q" shows "P|Q"
+apply (rule classical)
+apply (iprover intro: assms disjI1 disjI2 notI elim: notE)
+done
 
 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)
+shows "rec_eval (rec_minr2 f) [x, y1, y2] = (LEAST z.  (z \<le> x \<and> 0 < rec_eval f [z, y1, y2]) \<or> z = Suc x)"
+apply(induct x)
+apply(rule Least_equality[symmetric])
+apply(simp add: rec_minr2_def)
+apply(erule disjE)
+apply(rule rec_minr2_le)
+apply(auto)[2]
+apply(simp)
+apply(rule rec_minr2_le_Suc)
+apply(simp)
+
+apply(rule rec_minr2_le)
+
+
+apply(rule rec_minr2_le_Suc)
+apply(rule disjCI)
+apply(simp add: rec_minr2_def)
+
+apply(ru le setsum_one_less)
+apply(clarify)
+apply(rule setprod_one_le)
+apply(auto)[1]
+apply(simp)
+apply(rule setsum_one_le)
+apply(clarify)
+apply(rule setprod_one_le)
+apply(auto)[1]
+thm disj_CE
+apply(auto)
+
+lemma minr_lemma:
+shows "rec_eval (rec_minr2 f) [x, y1, y2] = Minr (\<lambda>x xs. (0 < rec_eval f (x #xs))) x [y1, y2]"
+apply(simp only: Minr_def)
+apply(rule sym)
+apply(rule Min_eqI)
+apply(auto)[1]
+apply(simp)
+apply(erule disjE)
+apply(simp)
+apply(rule rec_minr2_le_Suc)
+apply(rule rec_minr2_le)
+apply(auto)[2]
+apply(simp)
+apply(induct x)
+apply(simp add: rec_minr2_def)
+apply(
+apply(rule disjCI)
+apply(rule rec_minr2_eq_Suc)
+apply(simp)
+apply(auto)
+
+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)
+
+lemma minr_lemma:
+shows "rec_eval (rec_minr2 f) [x, y1, y2] = Minr (\<lambda>x xs. (0 < rec_eval f (x #xs))) x [y1, y2]"
+apply(simp only: Minr_def rec_minr2_def)
 apply(simp)
 apply(rule sym)
 apply(rule Min_eqI)
@@ -515,15 +810,112 @@
 apply (metis (mono_tags) LeastI_ex)
 by (metis LeastI_ex)
 
+lemma disjCI2:
+  assumes "~P ==> Q" shows "P|Q"
+apply (rule classical)
+apply (iprover intro: assms disjI1 disjI2 notI elim: notE)
+done
+
+
+lemma minr_lemma [simp]:
+shows "rec_eval (rec_minr2 f) [x, y1, y2] = (LEAST z.  (z \<le> x \<and> 0 < rec_eval f [z, y1, y2]) \<or> z = Suc x)"
+(*apply(simp add: rec_minr2_def)*)
+apply(rule Least_equality[symmetric])
+prefer 2
+apply(erule disjE)
+apply(rule rec_minr2_le)
+apply(auto)[2]
+apply(clarify)
+apply(rule rec_minr2_le_Suc)
+apply(rule disjCI)
+apply(simp add: rec_minr2_def)
+
+apply(ru le setsum_one_less)
+apply(clarify)
+apply(rule setprod_one_le)
+apply(auto)[1]
+apply(simp)
+apply(rule setsum_one_le)
+apply(clarify)
+apply(rule setprod_one_le)
+apply(auto)[1]
+thm disj_CE
+apply(auto)
+apply(auto)
+prefer 2
+apply(rule le_tran
+
+apply(rule le_trans)
+apply(simp)
+defer
+apply(auto)
+apply(subst setsum_cut_off_le)
+
+
+lemma 
+  "Minr R x ys = (LEAST z. (R z ys \<or> z = Suc x))" 
+apply(simp add: Minr_def)
+apply(rule Min_eqI)
+apply(auto)[1]
+apply(simp)
+apply(rule Least_le)
+apply(auto)[1]
+apply(rule LeastI2_wellorder)
+apply(auto)
+done
+
+definition (in ord)
+  Great :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "GREAT " 10) where
+  "Great P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> y \<le> x))"
+
+(*
+lemma Great_equality:
+  assumes "P x"
+    and "\<And>y. P y \<Longrightarrow> y \<le> x"
+  shows "Great P = x"
+unfolding Great_def 
+apply(rule the_equality)
+apply(blast intro: assms)
+*)
+
+
+
+lemma 
+  "Maxr R x ys = (GREAT z. (R z ys \<or> z = 0))" 
+apply(simp add: Maxr_def)
+apply(rule Max_eqI)
+apply(auto)[1]
+apply(simp)
+thm Least_le Greatest_le
+oops
+
+lemma
+  "Maxr R x ys = x - Minr (\<lambda>z. R (x - z)) x ys"
+apply(simp add: Maxr_def Minr_def)
+apply(rule Max_eqI)
+apply(auto)[1]
+apply(simp)
+apply(erule disjE)
+apply(simp)
+apply(auto)[1]
+defer
+apply(simp)
+apply(auto)[1]
+thm Min_insert
+defer
+oops
+
+
+
 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]]"
+  "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"