Mercurial Mercurial > hg > tm / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added recusive functions that decode triangle numbers
authorChristian Urban <christian dot urban at kcl dot ac dot uk>
Wed, 15 May 2013 15:07:27 +0100
changeset 255 4bf4d425e65d
parent 254 0546ae452747
child 256 04700724250f
added recusive functions that decode triangle numbers
thys/Recs.thy file | annotate | diff | comparison | revisions 
--- 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 \<Rightarrow> nat \<Rightarrow> nat"
+  Max_triangle :: "nat \<Rightarrow> nat \<Rightarrow> nat"
 where
-  "prod_decode_max k m =
-     (if m \<le> k then k else prod_decode_max (Suc k) (m - Suc k))"
+  "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 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)
+done
 
-lemma t: "triangle (prod_decode_max k m) \<le> 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) \<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)
 done
 
-lemma "prod_decode_max 0 z = (GREAT k. triangle k \<le> 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 \<le> 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 \<le> 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 \<le> z \<and> k \<le> z) \<or> 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 \<le> z \<and> k \<le> z) \<or> 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 *}
tm