# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1368685166 -3600
# Node ID 04700724250f7449483e3e201d136dbb61c81877
# Parent  4bf4d425e65d3f7a7e7ffb8d798f041249e69be6
completed coding functions

diff -r 4bf4d425e65d -r 04700724250f thys/Recs.thy
--- 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
diff -r 4bf4d425e65d -r 04700724250f thys/UF_Rec.thy
--- a/thys/UF_Rec.thy	Wed May 15 15:07:27 2013 +0100
+++ b/thys/UF_Rec.thy	Thu May 16 07:19:26 2013 +0100
@@ -4,8 +4,6 @@
 
 
 
-
-
 section {* Universal Function in HOL *}
 
 text {*
@@ -73,36 +71,21 @@
 
 fun Trpl :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
   where
-  "Trpl p q r = (Pi 0) ^ p * (Pi 1) ^ q * (Pi 2) ^ r"
+  "Trpl p q r = list_encode [p, q, r]"
 
 fun Left where
-  "Left c = Lo c (Pi 0)"
+  "Left c = list_decode c ! 0"
 
 fun Right where
-  "Right c = Lo c (Pi 2)"
+  "Right c = list_decode c ! 1"
 
 fun Stat where
-  "Stat c = Lo c (Pi 1)"
+  "Stat c = list_decode c ! 2"
 
 lemma mod_dvd_simp: 
   "(x mod y = (0::nat)) = (y dvd x)"
 by(auto simp add: dvd_def)
 
-lemma Trpl_Left [simp]:
-  "Left (Trpl p q r) = p"
-apply(simp)
-apply(subst Lo_def)
-apply(subst dvd_eq_mod_eq_0[symmetric])
-apply(simp)
-apply(auto)
-thm Lo_def
-thm mod_dvd_simp
-apply(simp add: left.simps trpl.simps lo.simps 
-              loR.simps mod_dvd_simp, auto simp: conf_decode1)
-apply(case_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r",
-      auto)
-apply(erule_tac x = l in allE, auto)
-
 
 fun Inpt :: "nat \<Rightarrow> nat list \<Rightarrow> nat"
   where
@@ -312,19 +295,16 @@
                   in CN rec_if [Id 3 1, entry, Z])"
 
 definition 
-  "rec_trpl = CN rec_mult [CN rec_mult 
-       [CN rec_power [constn (Pi 0), Id 3 0], 
-        CN rec_power [constn (Pi 1), Id 3 1]],
-        CN rec_power [constn (Pi 2), Id 3 2]]"
+  "rec_trpl = CN rec_penc [CN rec_penc [Id 3 0, Id 3 1], Id 3 2]"
 
 definition
-  "rec_left = CN rec_lo [Id 1 0, constn (Pi 0)]"
+  "rec_left = rec_pdec1"
 
 definition 
-  "rec_right = CN rec_lo [Id 1 0, constn (Pi 2)]"
+  "rec_right = CN rec_pdec2 [rec_pdec1]"
 
 definition 
-  "rec_stat = CN rec_lo [Id 1 0, constn (Pi 1)]"
+  "rec_stat = CN rec_pdec2 [rec_pdec2]"
 
 definition 
   "rec_newconf = (let act = CN rec_actn [Id 2 0, CN rec_stat [Id 2 1], CN rec_right [Id 2 1]] in
@@ -412,7 +392,8 @@
 
 lemma trpl_lemma [simp]: 
   "rec_eval rec_trpl [p, q, r] = Trpl p q r"
-by (simp add: rec_trpl_def)
+apply(simp)
+apply (simp add: rec_trpl_def)
 
 lemma left_lemma [simp]:
   "rec_eval rec_left [c] = Left c"