648   prod_decode_max :: "nat \<Rightarrow> nat \<Rightarrow> nat"

   651   Max_triangle :: "nat \<Rightarrow> nat \<Rightarrow> nat"

   650   "prod_decode_max k m =

   653   "Max_triangle k m =

   651      (if m \<le> k then k else prod_decode_max (Suc k) (m - Suc k))"

   654      (if m \<le> k then k else Max_triangle (Suc k) (m - Suc k))"

   652 

   655 

   653 lemma t: "triangle (prod_decode_max k m) \<le> triangle k + m"

   656 declare Max_triangle.simps [simp del]

   654 apply (induct k m rule: prod_decode_max.induct)

   657 

   655 apply (subst prod_decode_max.simps)

   658 lemma k: "Max_triangle k z \<le> k + z"

   656 apply (simp)

   659 apply(induct z arbitrary: k rule: nat_less_induct)

   657 done

   660 apply(subst Max_triangle.simps)

   658 

   661 apply(simp del: Max_triangle.simps)

   659 lemma "prod_decode_max 0 z = (GREAT k. triangle k \<le> z)"

   662 apply(rule impI)

   663 apply(drule_tac x="n - Suc k" in spec)

   664 apply(drule mp)

   665 apply(auto)[1]

   666 apply(drule_tac x="Suc k" in spec)

   667 apply(simp)

   668 done

   669 

   670 lemma k_aux: "prod_add (prod_decode_aux k z) \<le> k + z"

   671 apply(induct z arbitrary: k rule: nat_less_induct)

   672 apply(subst prod_decode_aux.simps)

   673 apply(simp)

   674 apply(rule impI)

   675 apply(drule_tac x="n - Suc k" in spec)

   676 apply(drule mp)

   677 apply(auto)[1]

   678 apply(drule_tac x="Suc k" in spec)

   679 apply(simp)

   680 done

   681 

   682 lemma t: "triangle (Max_triangle k m) \<le> triangle k + m"

   683 apply (induct k m rule: Max_triangle.induct)

   684 apply (simp add: Max_triangle.simps)

   685 done

   686 

   687 lemma t_aux: 

   688   "triangle (prod_add (prod_decode_aux k m)) \<le> triangle k + m"

   689 apply (induct k m rule: prod_decode_aux.induct)

   690 apply (simp add: prod_decode_aux.simps)

   691 done

   692 

   693 lemma w: "Max_triangle 0 (triangle y + m) = Max_triangle y m"

   694 apply(induct y arbitrary: m)

   695 apply(simp)

   696 apply(simp only: triangle_Suc add_assoc)

   697 apply(subst Max_triangle.simps)

   698 apply(simp)

   699 done

   700 

   701 lemma w_aux: "prod_add (prod_decode (triangle y + m)) = prod_add (prod_decode_aux y m)"

   702 apply(simp add: prod_decode_triangle_add)

   703 done

   704 

   705 lemma y: "y \<le> Max_triangle y k"

   706 apply(induct k arbitrary: y rule: nat_less_induct)

   707 apply(subst Max_triangle.simps)

   708 apply(simp del: Max_triangle.simps)

   709 apply(rule impI)

   710 apply(drule_tac x="n - Suc y" in spec)

   711 apply(drule mp)

   712 apply(auto)[1]

   713 apply(drule_tac x="Suc y" in spec)

   714 apply(erule Suc_leD)

   715 done

   716 

   717 lemma y_aux: "y \<le> prod_add (prod_decode_aux y k)"

   718 apply(induct k arbitrary: y rule: nat_less_induct)

   719 apply(subst prod_decode_aux.simps)

   720 apply(simp)

   721 apply(rule impI)

   722 apply(drule_tac x="n - Suc y" in spec)

   723 apply(drule mp)

   724 apply(auto)[1]

   725 apply(drule_tac x="Suc y" in spec)

   726 apply(erule Suc_leD)

   727 done

   728 

   729 lemma q3: "Max_triangle 0 z = (GREAT k. (triangle k \<le> z \<and> k \<le> z) \<or> k = 0)"

   662 using t

   732 apply(rule disjI1)

   663 apply -[1]

   733 apply(rule conjI)

   664 apply (smt triangle_0)

   734 apply(rule t[of 0, simplified])

   665 apply(induct z arbitrary: y rule: nat_less_induct)

   735 apply(rule k[of 0, simplified])

   666 apply (subst prod_decode_max.simps)

   736 apply(erule disjE)

   667 apply (auto simp del: prod_decode_max.simps)

   737 apply(erule conjE)

   668 apply(case_tac y)

   738 apply(subst (asm) (1) le_iff_add)

   669 apply(simp)

   739 apply(erule exE)

   670 apply(simp)

   740 apply(clarify)

   671 

   741 apply(simp only: w)

   672 apply (subst prod_decode_max.simps)

   742 apply(rule y)

   673 apply (auto simp del: prod_decode_max.simps)

   743 apply(simp)

   674 

   744 done

   675 

   745 

   676 

   746 lemma q3_aux: "prod_add (prod_decode z) = (GREAT k. (triangle k \<le> z \<and> k \<le> z) \<or> k = 0)"

   677 apply(blast)

   747 apply(rule sym)

   678 

   748 apply(rule Great_equality)

   679 lemma "prod_decode z = (z - (i(z) * (1 + i(z))) div 2, (i(z) * (3 + i(z))) div 2 - z)"

   749 apply(rule disjI1)

   680 apply(simp add: prod_decode_def)

   750 apply(rule conjI)

   681 apply(case_tac z)

   751 apply(simp only: prod_decode_def)

   752 apply(rule t_aux[of 0, simplified])

   753 apply(simp only: prod_decode_def)

   754 apply(rule k_aux[of 0, simplified])

   755 apply(erule disjE)

   756 apply(erule conjE)

   757 apply(subst (asm) (1) le_iff_add)

   758 apply(erule exE)

   759 apply(clarify)

   760 apply(simp only: w_aux)

   761 apply(rule y_aux)

   762 apply(simp)

   763 done

   764 

   765 

   766 definition 

   767   "rec_triangle = CN rec_quo [CN rec_mult [Id 1 0, CN S [Id 1 0]], constn 2]"

   768 

   769 lemma triangle_lemma [simp]:

   770   "rec_eval rec_triangle [x] = triangle x"

   771 by (simp add: rec_triangle_def triangle_def)

   772  

   773 definition

   774   "rec_max_triangle = 

   775        (let cond = CN rec_not [CN rec_le [CN rec_triangle [Id 2 0], Id 2 1]] in

   776         CN (rec_max1 cond) [Id 1 0, Id 1 0])"

   777 

   778 lemma max_triangle_lemma_test:

   779   "rec_eval rec_max_triangle [x] = Max_triangle 0 x"

   780 apply(simp add: q3)

   781 apply(simp add: rec_max_triangle_def)

   782 apply(simp add: BMax_rec_eq1)

   783 done

   784 

   785 lemma max_triangle_lemma [simp]:

   786   "rec_eval rec_max_triangle [x] = prod_add (prod_decode x)"

   787 apply(simp add: q3_aux)

   788 apply(simp add: rec_max_triangle_def)

   789 apply(simp add: BMax_rec_eq1)

   790 done

   791 

   792 lemma ww: "fst (prod_decode_aux k z) + snd (prod_decode_aux k z) = Max_triangle k z"

   793 apply(induct z arbitrary: k rule: nat_less_induct)

   794 apply(subst Max_triangle.simps)

   795 apply(simp)

   796 apply(rule conjI)

   683 apply(simp)

   798 apply(rule impI)

   799 apply(drule_tac x="n - Suc k" in spec)

   800 apply(drule mp)

   801 apply(auto)[1]

   802 apply(drule_tac x="Suc k" in spec)

   803 apply(subst prod_decode_aux.simps)

   804 apply(subst (2) prod_decode_aux.simps)

   805 apply(simp)

   806 done

   807 

   808 lemma ww0:

   809   "fst (prod_decode z) + snd (prod_decode z) = Max_triangle 0 z"

   810 by (simp only: prod_decode_def ww)

   811 

   812 lemma zz: "fst (prod_decode_aux k z) = (triangle k + z) - triangle (Max_triangle k z)"

   813 apply(induct z arbitrary: k rule: nat_less_induct)

   814 apply(subst Max_triangle.simps)

   815 apply(simp)

   816 apply(rule conjI)

   817 apply(rule impI)

   818 apply(subst prod_decode_aux.simps)

   819 apply(simp)

   820 apply(rule impI)

   821 apply(subst prod_decode_aux.simps)

   822 apply(simp)

   823 done

   824 

   825 lemma zz0: 

   826   "fst (prod_decode z) = z - triangle (Max_triangle 0 z)"

   827 apply(simp add: prod_decode_def zz)

   828 done

   829 

   830 lemma yy0: 

   831   "snd (prod_decode z) = Max_triangle 0 z - fst (prod_decode z)"

   832 apply(simp add: ww0[symmetric])

   833 done

   834 

   835 lemma final: "prod_decode z = (let k = Max_triangle 0 z in 

   836                         let m = z - triangle k in (m, k - m))"

   837 apply(simp add: Let_def zz0[symmetric] yy0[symmetric])

   838 done

   839 

   840 definition

   841   "rec_penc = CN rec_add [CN rec_triangle [CN rec_add [Id 2 0, Id 2 1]], Id 2 0]"

   842 

   843 definition 

   844   "rec_pdec1 = CN rec_minus [Id 1 0, CN rec_triangle [CN rec_max_triangle [Id 1 0]]]" 

   845 

   846 definition 

   847   "rec_pdec2 = CN rec_minus [CN rec_max_triangle [Id 1 0], CN rec_pdec1 [Id 1 0]]" 

   848 

   849 lemma pdec1_lemma [simp]:

   850   "rec_eval rec_pdec1 [z] = fst (prod_decode z)"

   851 by (simp add: rec_pdec1_def zz0)

   852 

   853 lemma pdec2_lemma [simp]:

   854   "rec_eval rec_pdec2 [z] = snd (prod_decode z)"

   855 by (simp add: rec_pdec2_def yy0)

   856 

   857 lemma penc_lemma [simp]:

   858   "rec_eval rec_penc [m, n] = prod_encode (m, n)"

   859 by (simp add: rec_penc_def prod_encode_def)

   860