--- 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"