--- a/thys/Recs.thy Wed May 15 15:07:27 2013 +0100
+++ b/thys/Recs.thy Thu May 16 07:19:26 2013 +0100
@@ -552,21 +552,10 @@
definition BMax_set :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat"
where "BMax_set R x = Max ({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)"
+ "BMax_rec R x = (GREATEST z. (R z \<and> z \<le> x) \<or> z = 0)"
apply(induct x)
-apply(auto intro: Great_equality Great_equality[symmetric])
+apply(auto intro: Greatest_equality Greatest_equality[symmetric])
apply(simp add: le_Suc_eq)
by metis
@@ -595,128 +584,56 @@
"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)
-section {* Encodings *}
-
-fun prod_decode1 where
- "prod_decode1 z = z - (triangle (BMax_rec (\<lambda>k. triangle k \<le> z) z))"
-
-fun prod_decode2 where
- "prod_decode2 z = BMax_rec (\<lambda>k. triangle k \<le> z) z - prod_decode1 z"
+section {* Encodings using Cantor's pairing function *}
-section {* Encodings *}
+text {*
+ We first have to prove that we can extract the maximal
+ triangle number using @{term prod_decode}.
+*}
-lemma triangle_sum:
- "triangle k = (\<Sum>i \<le> k. i)"
-by (induct k) (simp_all)
-
-fun sqrt where
- "sqrt z = BMax_rec (\<lambda>x. x * x \<le> z) z"
+abbreviation Max_triangle_aux where
+ "Max_triangle_aux k z \<equiv> fst (prod_decode_aux k z) + snd (prod_decode_aux k z)"
-lemma sqrt_bounded_Max:
- "Discrete.sqrt n = Max (Set.filter (\<lambda>m. m\<twosuperior> \<le> n) {0..n})"
-proof -
- from power2_nat_le_imp_le [of _ n] have "{m. m \<le> n \<and> m\<twosuperior> \<le> n} = {m. m\<twosuperior> \<le> n}" by auto
- then show ?thesis by (simp add: Discrete.sqrt_def Set.filter_def)
-qed
+abbreviation Max_triangle where
+ "Max_triangle z \<equiv> Max_triangle_aux 0 z"
-lemma sqrt: "Discrete.sqrt z = sqrt z"
-apply(simp add: BMax_rec_eq3 sqrt_bounded_Max Set.filter_def power2_eq_square)
-apply(rule_tac f="Max" in arg_cong)
-apply(auto)
-done
-
-fun i where
- "i z = (Discrete.sqrt (1 + 8 * z) - 1) div 2"
-
-lemma "map prod_decode [0,1,2,3,4,5,6,7,8,9,10,11,12] =
- [(0, 0), (0, 1), (1, 0), (0, 2), (1, 1), (2, 0), (0, 3),
- (1, 2), (2, 1), (3, 0), (0, 4), (1, 3), (2, 2)]"
-apply(simp add: prod_decode_def prod_decode_aux.simps)
+lemma fst_prod_decode:
+ "fst (prod_decode z) = z - triangle (Max_triangle z)"
+apply(subst (3) prod_decode_inverse[symmetric])
+apply(simp add: prod_encode_def)
+apply(case_tac "prod_decode z")
+apply(simp add: prod_decode_def)
done
-lemma "map triangle [0, 1, 2, 3, 4, 5, 6 ] = [0, 1, 3, 6, 10, 15, 21]"
-by(simp add: numeral_eq_Suc One_nat_def)
-
-lemma "map (\<lambda>z. (z - (i(z) * (1 + i(z))) div 2, (i(z) * (3 + i(z))) div 2 - z))
- [0,1,2,3,4,5,6,7,8,9,10,11,12] =
- [(0, 0), (0, 1), (1, 0), (0, 2), (1, 1), (2, 0), (0, 3),
- (1, 2), (2, 1), (3, 0), (0, 4), (1, 3), (2, 2)]"
-apply(simp add: sqrt)
-by eval
-
-fun prod_add where
- "prod_add (m, n) = m + n"
+lemma snd_prod_decode:
+ "snd (prod_decode z) = Max_triangle z - fst (prod_decode z)"
+by (simp only: prod_decode_def)
-fun
- Max_triangle :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-where
- "Max_triangle k m =
- (if m \<le> k then k else Max_triangle (Suc k) (m - Suc k))"
-
-declare Max_triangle.simps [simp del]
+lemma le_triangle:
+ "m \<le> triangle (n + m)"
+by (induct_tac m) (simp_all)
-lemma k: "Max_triangle k z \<le> k + z"
-apply(induct z arbitrary: k rule: nat_less_induct)
-apply(subst Max_triangle.simps)
-apply(simp del: Max_triangle.simps)
-apply(rule impI)
-apply(drule_tac x="n - Suc k" in spec)
-apply(drule mp)
-apply(auto)[1]
-apply(drule_tac x="Suc k" in spec)
-apply(simp)
+lemma k_aux:
+ "Max_triangle z \<le> z"
+apply(subst (8) prod_decode_inverse[symmetric])
+apply(case_tac "prod_decode z")
+apply(simp add: prod_decode_def prod_encode_def le_triangle)
done
-lemma k_aux: "prod_add (prod_decode_aux k z) \<le> k + z"
-apply(induct z arbitrary: k rule: nat_less_induct)
-apply(subst prod_decode_aux.simps)
-apply(simp)
-apply(rule impI)
-apply(drule_tac x="n - Suc k" in spec)
-apply(drule mp)
-apply(auto)[1]
-apply(drule_tac x="Suc k" in spec)
-apply(simp)
-done
-
-lemma t: "triangle (Max_triangle k m) \<le> triangle k + m"
-apply (induct k m rule: Max_triangle.induct)
-apply (simp add: Max_triangle.simps)
-done
-
-lemma t_aux:
- "triangle (prod_add (prod_decode_aux k m)) \<le> triangle k + m"
-apply (induct k m rule: prod_decode_aux.induct)
-apply (simp add: prod_decode_aux.simps)
+lemma t_aux:
+ "triangle (Max_triangle z) \<le> z"
+apply(subst (9) prod_decode_inverse[symmetric])
+apply(case_tac "prod_decode z")
+apply(simp add: prod_decode_def prod_encode_def)
done
-lemma w: "Max_triangle 0 (triangle y + m) = Max_triangle y m"
-apply(induct y arbitrary: m)
-apply(simp)
-apply(simp only: triangle_Suc add_assoc)
-apply(subst Max_triangle.simps)
-apply(simp)
-done
+lemma w_aux:
+ "Max_triangle (triangle k + m) = Max_triangle_aux k m"
+by (simp add: prod_decode_def[symmetric] prod_decode_triangle_add)
-lemma w_aux: "prod_add (prod_decode (triangle y + m)) = prod_add (prod_decode_aux y m)"
-apply(simp add: prod_decode_triangle_add)
-done
-
-lemma y: "y \<le> Max_triangle y k"
+lemma y_aux: "y \<le> Max_triangle_aux y k"
apply(induct k arbitrary: y rule: nat_less_induct)
-apply(subst Max_triangle.simps)
-apply(simp del: Max_triangle.simps)
-apply(rule impI)
-apply(drule_tac x="n - Suc y" in spec)
-apply(drule mp)
-apply(auto)[1]
-apply(drule_tac x="Suc y" in spec)
-apply(erule Suc_leD)
-done
-
-lemma y_aux: "y \<le> prod_add (prod_decode_aux y k)"
-apply(induct k arbitrary: y rule: nat_less_induct)
-apply(subst prod_decode_aux.simps)
+apply(subst (1 2) prod_decode_aux.simps)
apply(simp)
apply(rule impI)
apply(drule_tac x="n - Suc y" in spec)
@@ -726,32 +643,13 @@
apply(erule Suc_leD)
done
-lemma q3: "Max_triangle 0 z = (GREAT k. (triangle k \<le> z \<and> k \<le> z) \<or> k = 0)"
-apply(rule sym)
-apply(rule Great_equality)
+lemma Max_triangle_greatest:
+ "Max_triangle z = (GREATEST k. (triangle k \<le> z \<and> k \<le> z) \<or> k = 0)"
+apply(rule Greatest_equality[symmetric])
apply(rule disjI1)
apply(rule conjI)
-apply(rule t[of 0, simplified])
-apply(rule k[of 0, simplified])
-apply(erule disjE)
-apply(erule conjE)
-apply(subst (asm) (1) le_iff_add)
-apply(erule exE)
-apply(clarify)
-apply(simp only: w)
-apply(rule y)
-apply(simp)
-done
-
-lemma q3_aux: "prod_add (prod_decode z) = (GREAT k. (triangle k \<le> z \<and> k \<le> z) \<or> k = 0)"
-apply(rule sym)
-apply(rule Great_equality)
-apply(rule disjI1)
-apply(rule conjI)
-apply(simp only: prod_decode_def)
-apply(rule t_aux[of 0, simplified])
-apply(simp only: prod_decode_def)
-apply(rule k_aux[of 0, simplified])
+apply(rule t_aux)
+apply(rule k_aux)
apply(erule disjE)
apply(erule conjE)
apply(subst (asm) (1) le_iff_add)
@@ -762,9 +660,8 @@
apply(simp)
done
-
definition
- "rec_triangle = CN rec_quo [CN rec_mult [Id 1 0, CN S [Id 1 0]], constn 2]"
+ "rec_triangle = CN rec_quo [CN rec_mult [Id 1 0, S], constn 2]"
lemma triangle_lemma [simp]:
"rec_eval rec_triangle [x] = triangle x"
@@ -775,67 +672,9 @@
(let cond = CN rec_not [CN rec_le [CN rec_triangle [Id 2 0], Id 2 1]] in
CN (rec_max1 cond) [Id 1 0, Id 1 0])"
-lemma max_triangle_lemma_test:
- "rec_eval rec_max_triangle [x] = Max_triangle 0 x"
-apply(simp add: q3)
-apply(simp add: rec_max_triangle_def)
-apply(simp add: BMax_rec_eq1)
-done
-
lemma max_triangle_lemma [simp]:
- "rec_eval rec_max_triangle [x] = prod_add (prod_decode x)"
-apply(simp add: q3_aux)
-apply(simp add: rec_max_triangle_def)
-apply(simp add: BMax_rec_eq1)
-done
-
-lemma ww: "fst (prod_decode_aux k z) + snd (prod_decode_aux k z) = Max_triangle k z"
-apply(induct z arbitrary: k rule: nat_less_induct)
-apply(subst Max_triangle.simps)
-apply(simp)
-apply(rule conjI)
-apply(simp add: prod_decode_aux.simps)
-apply(rule impI)
-apply(drule_tac x="n - Suc k" in spec)
-apply(drule mp)
-apply(auto)[1]
-apply(drule_tac x="Suc k" in spec)
-apply(subst prod_decode_aux.simps)
-apply(subst (2) prod_decode_aux.simps)
-apply(simp)
-done
-
-lemma ww0:
- "fst (prod_decode z) + snd (prod_decode z) = Max_triangle 0 z"
-by (simp only: prod_decode_def ww)
-
-lemma zz: "fst (prod_decode_aux k z) = (triangle k + z) - triangle (Max_triangle k z)"
-apply(induct z arbitrary: k rule: nat_less_induct)
-apply(subst Max_triangle.simps)
-apply(simp)
-apply(rule conjI)
-apply(rule impI)
-apply(subst prod_decode_aux.simps)
-apply(simp)
-apply(rule impI)
-apply(subst prod_decode_aux.simps)
-apply(simp)
-done
-
-lemma zz0:
- "fst (prod_decode z) = z - triangle (Max_triangle 0 z)"
-apply(simp add: prod_decode_def zz)
-done
-
-lemma yy0:
- "snd (prod_decode z) = Max_triangle 0 z - fst (prod_decode z)"
-apply(simp add: ww0[symmetric])
-done
-
-lemma final: "prod_decode z = (let k = Max_triangle 0 z in
- let m = z - triangle k in (m, k - m))"
-apply(simp add: Let_def zz0[symmetric] yy0[symmetric])
-done
+ "rec_eval rec_max_triangle [x] = Max_triangle x"
+by (simp add: Max_triangle_greatest rec_max_triangle_def Let_def BMax_rec_eq1)
definition
"rec_penc = CN rec_add [CN rec_triangle [CN rec_add [Id 2 0, Id 2 1]], Id 2 0]"
@@ -848,17 +687,18 @@
lemma pdec1_lemma [simp]:
"rec_eval rec_pdec1 [z] = fst (prod_decode z)"
-by (simp add: rec_pdec1_def zz0)
+by (simp add: rec_pdec1_def fst_prod_decode)
lemma pdec2_lemma [simp]:
"rec_eval rec_pdec2 [z] = snd (prod_decode z)"
-by (simp add: rec_pdec2_def yy0)
+by (simp add: rec_pdec2_def snd_prod_decode)
lemma penc_lemma [simp]:
"rec_eval rec_penc [m, n] = prod_encode (m, n)"
by (simp add: rec_penc_def prod_encode_def)
+
section {* Discrete Logarithms *}
definition
@@ -889,7 +729,7 @@
"rec_eval rec_lo [x, y] = Lo x y"
by (simp add: rec_lo_def Lo_def Let_def)
-
+section {* NextPrime number function *}
text {*
@{text "NextPrime x"} returns the first prime number after @{text "x"};
@@ -945,447 +785,3 @@
end
-(*
-
-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] = (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)
-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)
-
-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]]"
-
-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_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: 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)
-apply(auto simp del: not_lemma)
-apply(simp)
-apply(simp only: not_lemma sign_lemma)
-apply(rule sym)
-apply(rule Min_eqI)
-apply(auto)[1]
-apply(simp)
-apply(subst setsum_cut_off_le[where m="ya"])
-apply(simp)
-apply(simp)
-apply(metis Icc_subset_Ici_iff atLeast_def in_mono le_refl mem_Collect_eq)
-apply(rule setsum_one_less)
-apply(default)
-apply(rule impI)
-apply(rule setprod_one_le)
-apply(auto split: if_splits)[1]
-apply(simp)
-apply(rule conjI)
-apply(subst setsum_cut_off_le[where m="xa"])
-apply(simp)
-apply(simp)
-apply (metis Icc_subset_Ici_iff atLeast_def in_mono le_refl mem_Collect_eq)
-apply(rule le_trans)
-apply(rule setsum_one_less)
-apply(default)
-apply(rule impI)
-apply(rule setprod_one_le)
-apply(auto split: if_splits)[1]
-apply(simp)
-apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y])")
-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 3)
-apply(assumption)
-prefer 3
-apply (metis LeastI_ex)
-apply(auto)[1]
-apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y])")
-prefer 2
-apply(auto)[1]
-apply(rotate_tac 5)
-apply(drule not_less_Least)
-apply(auto)[1]
-apply(auto)
-by (metis (mono_tags) LeastI_ex)
-
-
-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}))"
-
-lemma Minr2_Minr:
- "Minr2 R x y = Minr R x y"
-apply(auto)
-apply (metis (lifting, no_types) Min_singleton empty_Collect_eq)
-apply(rule min_absorb2)
-apply(subst Min_le_iff)
-apply(auto)
-done
- *)
\ No newline at end of file