diff -r 0546ae452747 -r 4bf4d425e65d thys/Recs.thy --- a/thys/Recs.thy Mon May 13 15:28:48 2013 +0100 +++ b/thys/Recs.thy Wed May 15 15:07:27 2013 +0100 @@ -644,43 +644,220 @@ apply(simp add: sqrt) by eval +fun prod_add where + "prod_add (m, n) = m + n" + fun - prod_decode_max :: "nat \ nat \ nat" + Max_triangle :: "nat \ nat \ nat" where - "prod_decode_max k m = - (if m \ k then k else prod_decode_max (Suc k) (m - Suc k))" + "Max_triangle k m = + (if m \ k then k else Max_triangle (Suc k) (m - Suc k))" + +declare Max_triangle.simps [simp del] + +lemma k: "Max_triangle k z \ 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) +done -lemma t: "triangle (prod_decode_max k m) \ triangle k + m" -apply (induct k m rule: prod_decode_max.induct) -apply (subst prod_decode_max.simps) -apply (simp) +lemma k_aux: "prod_add (prod_decode_aux k z) \ 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) \ 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)) \ triangle k + m" +apply (induct k m rule: prod_decode_aux.induct) +apply (simp add: prod_decode_aux.simps) done -lemma "prod_decode_max 0 z = (GREAT k. triangle k \ z)" +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: "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 \ Max_triangle 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 \ prod_add (prod_decode_aux y k)" +apply(induct k arbitrary: y rule: nat_less_induct) +apply(subst prod_decode_aux.simps) +apply(simp) +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 q3: "Max_triangle 0 z = (GREAT k. (triangle k \ z \ k \ z) \ k = 0)" +apply(rule sym) +apply(rule Great_equality) +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 \ z \ k \ z) \ k = 0)" apply(rule sym) apply(rule Great_equality) -using t -apply -[1] -apply (smt triangle_0) -apply(induct z arbitrary: y rule: nat_less_induct) -apply (subst prod_decode_max.simps) -apply (auto simp del: prod_decode_max.simps) -apply(case_tac y) +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(erule disjE) +apply(erule conjE) +apply(subst (asm) (1) le_iff_add) +apply(erule exE) +apply(clarify) +apply(simp only: w_aux) +apply(rule y_aux) apply(simp) -apply(simp) - -apply (subst prod_decode_max.simps) -apply (auto simp del: prod_decode_max.simps) +done +definition + "rec_triangle = CN rec_quo [CN rec_mult [Id 1 0, CN S [Id 1 0]], constn 2]" -apply(blast) +lemma triangle_lemma [simp]: + "rec_eval rec_triangle [x] = triangle x" +by (simp add: rec_triangle_def triangle_def) + +definition + "rec_max_triangle = + (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 "prod_decode z = (z - (i(z) * (1 + i(z))) div 2, (i(z) * (3 + i(z))) div 2 - z)" -apply(simp add: prod_decode_def) -apply(case_tac z) -apply(simp add: prod_decode_aux.simps) +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 + +definition + "rec_penc = CN rec_add [CN rec_triangle [CN rec_add [Id 2 0, Id 2 1]], Id 2 0]" + +definition + "rec_pdec1 = CN rec_minus [Id 1 0, CN rec_triangle [CN rec_max_triangle [Id 1 0]]]" + +definition + "rec_pdec2 = CN rec_minus [CN rec_max_triangle [Id 1 0], CN rec_pdec1 [Id 1 0]]" + +lemma pdec1_lemma [simp]: + "rec_eval rec_pdec1 [z] = fst (prod_decode z)" +by (simp add: rec_pdec1_def zz0) + +lemma pdec2_lemma [simp]: + "rec_eval rec_pdec2 [z] = snd (prod_decode z)" +by (simp add: rec_pdec2_def yy0) + +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 *}