diff -r af60d84e0677 -r e113420a2fce thys/UF_Rec.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/UF_Rec.thy	Thu May 02 11:32:37 2013 +0100
@@ -0,0 +1,864 @@
+theory UF_Rec
+imports Recs
+begin
+
+section {* Universal Function *}
+
+text {* @{text "NextPrime x"} returns the first prime number after @{text "x"}. *}
+
+fun NextPrime ::"nat \<Rightarrow> nat"
+  where
+  "NextPrime x = (LEAST y. y \<le> Suc (fact x) \<and> x < y \<and> prime y)"
+
+definition rec_nextprime :: "recf"
+  where
+  "rec_nextprime = (let conj1 = CN rec_le [Id 2 0, CN S [CN rec_fact [Id 2 1]]] in
+                    let conj2 = CN rec_less [Id 2 1, Id 2 0] in
+                    let conj3 = CN rec_prime [Id 2 0] in 
+                    let conjs = CN rec_conj [CN rec_conj [conj2, conj1], conj3]
+                    in MN (CN rec_not [conjs]))"
+
+lemma nextprime_lemma [simp]:
+  "rec_eval rec_nextprime [x] = NextPrime x"
+by (simp add: rec_nextprime_def Let_def)
+
+
+fun Pi :: "nat \<Rightarrow> nat"
+  where
+  "Pi 0 = 2" |
+  "Pi (Suc x) = NextPrime (Pi x)"
+
+definition 
+  "rec_pi = PR (constn 2) (CN rec_nextprime [Id 2 1])"
+
+lemma pi_lemma [simp]:
+  "rec_eval rec_pi [x] = Pi x"
+by (induct x) (simp_all add: rec_pi_def)
+
+
+
+text{* coding of the configuration *}
+
+text {*
+  @{text "Entry sr i"} returns the @{text "i"}-th entry of a list of natural 
+  numbers encoded by number @{text "sr"} using Godel's coding.
+  *}
+fun Entry where
+  "Entry sr i = Lo sr (Pi (Suc i))"
+
+definition 
+  "rec_entry = CN rec_lo [Id 2 0, CN rec_pi [CN S [Id 2 1]]]"
+
+lemma entry_lemma [simp]:
+  "rec_eval rec_entry [sr, i] = Entry sr i"
+by(simp add: rec_entry_def)
+
+
+fun Listsum2 :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Listsum2 xs 0 = 0"
+| "Listsum2 xs (Suc n) = Listsum2 xs n + xs ! n"
+
+fun rec_listsum2 :: "nat \<Rightarrow> nat \<Rightarrow> recf"
+  where
+  "rec_listsum2 vl 0 = CN Z [Id vl 0]"
+| "rec_listsum2 vl (Suc n) = CN rec_add [rec_listsum2 vl n, Id vl n]"
+
+lemma listsum2_lemma [simp]: 
+  "length xs = vl \<Longrightarrow> rec_eval (rec_listsum2 vl n) xs = Listsum2 xs n"
+by (induct n) (simp_all)
+
+text {*
+  @{text "Strt"} corresponds to the @{text "strt"} function on page 90 of the 
+  B book, but this definition generalises the original one to deal with multiple 
+  input arguments.
+  *}
+fun Strt' :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Strt' xs 0 = 0"
+| "Strt' xs (Suc n) = (let dbound = Listsum2 xs n + n 
+                       in Strt' xs n + (2 ^ (xs ! n + dbound) - 2 ^ dbound))"
+
+fun Strt :: "nat list \<Rightarrow> nat"
+  where
+  "Strt xs = (let ys = map Suc xs in Strt' ys (length ys))"
+
+fun rec_strt' :: "nat \<Rightarrow> nat \<Rightarrow> recf"
+  where
+  "rec_strt' xs 0 = Z"
+| "rec_strt' xs (Suc n) = 
+      (let dbound = CN rec_add [rec_listsum2 xs n, constn n] in
+       let t1 = CN rec_power [constn 2, dbound] in
+       let t2 = CN rec_power [constn 2, CN rec_add [Id xs n, dbound]] in
+       CN rec_add [rec_strt' xs n, CN rec_minus [t2, t1]])"
+
+fun rec_map :: "recf \<Rightarrow> nat \<Rightarrow> recf list"
+  where
+  "rec_map rf vl = map (\<lambda>i. CN rf [Id vl i]) [0..<vl]"
+
+fun rec_strt :: "nat \<Rightarrow> recf"
+  where
+  "rec_strt xs = CN (rec_strt' xs xs) (rec_map S xs)"
+
+lemma strt'_lemma [simp]:
+  "length xs = vl \<Longrightarrow> rec_eval (rec_strt' vl n) xs = Strt' xs n"
+by (induct n) (simp_all add: Let_def)
+
+
+lemma map_suc:
+  "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs"
+proof -
+  have "Suc \<circ> (\<lambda>x. xs ! x) = (\<lambda>x. Suc (xs ! x))" by (simp add: comp_def)
+  then have "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map (Suc \<circ> (\<lambda>x. xs ! x)) [0..<length xs]" by simp
+  also have "... = map Suc (map (\<lambda>x. xs ! x) [0..<length xs])" by simp
+  also have "... = map Suc xs" by (simp add: map_nth)
+  finally show "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs" .
+qed
+
+lemma strt_lemma [simp]: 
+  "length xs = vl \<Longrightarrow> rec_eval (rec_strt vl) xs = Strt xs"
+by (simp add: comp_def map_suc[symmetric])
+
+
+text {* The @{text "Scan"} function on page 90 of B book. *}
+fun Scan :: "nat \<Rightarrow> nat"
+  where
+  "Scan r = r mod 2"
+
+definition 
+  "rec_scan = CN rec_rem [Id 1 0, constn 2]"
+
+lemma scan_lemma [simp]: 
+  "rec_eval rec_scan [r] = r mod 2"
+by(simp add: rec_scan_def)
+
+text {* The @{text Newleft} and @{text Newright} functions on page 91 of B book. *}
+
+fun Newleft :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Newleft p r a = (if a = 0 \<or> a = 1 then p 
+                    else if a = 2 then p div 2
+                    else if a = 3 then 2 * p + r mod 2
+                    else p)"
+
+fun Newright :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Newright p r a  = (if a = 0 then r - Scan r
+                      else if a = 1 then r + 1 - Scan r
+                      else if a = 2 then 2 * r + p mod 2
+                      else if a = 3 then r div 2
+                      else r)"
+
+definition
+    "rec_newleft =
+       (let cond1 = CN rec_disj [CN rec_eq [Id 3 2, Z], CN rec_eq [Id 3 2, constn 1]] in
+        let cond2 = CN rec_eq [Id 3 2, constn 2] in
+        let cond3 = CN rec_eq [Id 3 2, constn 3] in
+        let case3 = CN rec_add [CN rec_mult [constn 2, Id 3 0], 
+                                CN rec_rem [Id 3 1, constn 2]] in
+        CN rec_if [cond1, Id 3 0, 
+          CN rec_if [cond2, CN rec_quo [Id 3 0, constn 2],
+            CN rec_if [cond3, case3, Id 3 0]]])"
+
+definition
+    "rec_newright =
+       (let condn = \<lambda>n. CN rec_eq [Id 3 2, constn n] in
+        let case0 = CN rec_minus [Id 3 1, CN rec_scan [Id 3 1]] in
+        let case1 = CN rec_minus [CN rec_add [Id 3 1, constn 1], CN rec_scan [Id 3 1]] in
+        let case2 = CN rec_add [CN rec_mult [constn 2, Id 3 1],                     
+                                CN rec_rem [Id 3 0, constn 2]] in
+        let case3 = CN rec_quo [Id 2 1, constn 2] in
+        CN rec_if [condn 0, case0, 
+          CN rec_if [condn 1, case1,
+            CN rec_if [condn 2, case2,
+              CN rec_if [condn 3, case3, Id 3 1]]]])"
+
+lemma newleft_lemma [simp]:
+  "rec_eval rec_newleft [p, r, a] = Newleft p r a"
+by (simp add: rec_newleft_def Let_def)
+
+lemma newright_lemma [simp]:
+  "rec_eval rec_newright [p, r, a] = Newright p r a"
+by (simp add: rec_newright_def Let_def)
+
+text {*
+  The @{text "Actn"} function given on page 92 of B book, which is used to 
+  fetch Turing Machine intructions. In @{text "Actn m q r"}, @{text "m"} is 
+  the Goedel coding of a Turing Machine, @{text "q"} is the current state of 
+  Turing Machine, @{text "r"} is the right number of Turing Machine tape.
+  *}
+fun Actn :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Actn m q r = (if q \<noteq> 0 then Entry m (4 * (q - 1) + 2 * Scan r) else 4)"
+
+definition 
+  "rec_actn = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in
+               let add2 = CN rec_mult [constn 2, CN rec_scan [Id 3 2]] in
+               let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]]
+               in CN rec_if [Id 3 1, entry, constn 4])"
+
+lemma actn_lemma [simp]:
+  "rec_eval rec_actn [m, q, r] = Actn m q r"
+by (simp add: rec_actn_def)
+
+fun Newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Newstat m q r = (if q \<noteq> 0 then Entry m (4 * (q - 1) + 2 * Scan r + 1) else 0)"
+
+definition rec_newstat :: "recf"
+  where
+  "rec_newstat = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in
+                  let add2 = CN S [CN rec_mult [constn 2, CN rec_scan [Id 3 2]]] in
+                  let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]]
+                  in CN rec_if [Id 3 1, entry, Z])"
+
+lemma newstat_lemma [simp]: 
+  "rec_eval rec_newstat [m, q, r] = Newstat m q r"
+by (simp add: rec_newstat_def)
+
+
+fun Trpl :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Trpl p q r = (Pi 0) ^ p * (Pi 1) ^ q * (Pi 2) ^ r"
+
+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]]"
+
+lemma trpl_lemma [simp]: 
+  "rec_eval rec_trpl [p, q, r] = Trpl p q r"
+by (simp add: rec_trpl_def)
+
+
+
+fun Left where
+  "Left c = Lo c (Pi 0)"
+
+definition
+  "rec_left = CN rec_lo [Id 1 0, constn (Pi 0)]"
+
+lemma left_lemma [simp]:
+  "rec_eval rec_left [c] = Left c" 
+by(simp add: rec_left_def)
+
+fun Right where
+  "Right c = Lo c (Pi 2)"
+
+definition 
+  "rec_right = CN rec_lo [Id 1 0, constn (Pi 2)]"
+
+lemma right_lemma [simp]:
+  "rec_eval rec_right [c] = Right c" 
+by(simp add: rec_right_def)
+
+fun Stat where
+  "Stat c = Lo c (Pi 1)"
+
+definition 
+  "rec_stat = CN rec_lo [Id 1 0, constn (Pi 1)]"
+
+lemma stat_lemma [simp]:
+  "rec_eval rec_stat [c] = Stat c" 
+by(simp add: rec_stat_def)
+
+fun Inpt :: "nat \<Rightarrow> nat list \<Rightarrow> nat"
+  where
+  "Inpt m xs = Trpl 0 1 (Strt xs)"
+
+fun Newconf :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Newconf m c = Trpl (Newleft (Left c) (Right c) (Actn m (Stat c) (Right c)))
+                      (Newstat m (Stat c) (Right c)) 
+                      (Newright (Left c) (Right c) (Actn m (Stat c) (Right c)))"
+
+definition 
+  "rec_newconf = (let act = CN rec_actn [Id 2 0, CN rec_stat [Id 2 1], CN rec_right [Id 2 1]] in
+                  let left = CN rec_left [Id 2 1] in
+                  let right = CN rec_right [Id 2 1] in
+                  let stat = CN rec_stat [Id 2 1] in
+                  let one = CN rec_newleft [left, right, act] in
+                  let two = CN rec_newstat [Id 2 0, stat, right] in
+                  let three = CN rec_newright [left, right, act]
+                  in CN rec_trpl [one, two, three])" 
+
+lemma newconf_lemma [simp]: 
+  "rec_eval rec_newconf [m, c] = Newconf m c"
+by (simp add: rec_newconf_def Let_def)
+
+text {*
+  @{text "Conf k m r"} computes the TM configuration after @{text "k"} steps of execution
+  of TM coded as @{text "m"} starting from the initial configuration where the left 
+  number equals @{text "0"}, right number equals @{text "r"}. 
+  *}
+fun Conf :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Conf 0 m r  = Trpl 0 1 r"
+| "Conf (Suc k) m r = Newconf m (Conf k m r)"
+
+definition 
+  "rec_conf = PR (CN rec_trpl [constn 0, constn 1, Id 2 1])
+                 (CN rec_newconf [Id 4 2 , Id 4 1])"
+
+lemma conf_lemma [simp]: 
+  "rec_eval rec_conf [k, m, r] = Conf k m r"
+by(induct k) (simp_all add: rec_conf_def)
+
+
+text {*
+  @{text "Nstd c"} returns true if the configuration coded 
+  by @{text "c"} is not a stardard final configuration.
+  *}
+fun Nstd :: "nat \<Rightarrow> bool"
+  where
+  "Nstd c = (Stat c \<noteq> 0 \<or> 
+             Left c \<noteq> 0 \<or> 
+             Right c \<noteq> 2 ^ (Lg (Suc (Right c)) 2) - 1 \<or> 
+             Right c = 0)"
+
+definition 
+  "rec_nstd = (let disj1 = CN rec_noteq [rec_stat, constn 0] in
+               let disj2 = CN rec_noteq [rec_left, constn 0] in
+               let rhs = CN rec_pred [CN rec_power [constn 2, CN rec_lg [CN S [rec_right], constn 2]]] in
+               let disj3 = CN rec_noteq [rec_right, rhs] in
+               let disj4 = CN rec_eq [rec_right, constn 0] in
+               CN rec_disj [CN rec_disj [CN rec_disj [disj1, disj2], disj3], disj4])"
+
+lemma nstd_lemma [simp]:
+  "rec_eval rec_nstd [c] = (if Nstd c then 1 else 0)"
+by(simp add: rec_nstd_def)
+
+
+text{* 
+  @{text "Nostop t m r"} means that afer @{text "t"} steps of 
+  execution, the TM coded by @{text "m"} is not at a stardard 
+  final configuration.
+  *}
+fun Nostop :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+  where
+  "Nostop t m r = Nstd (Conf t m r)"
+
+definition 
+  "rec_nostop = CN rec_nstd [rec_conf]"
+
+lemma nostop_lemma [simp]:
+  "rec_eval rec_nostop [t, m, r] = (if Nostop t m r then 1 else 0)" 
+by (simp add: rec_nostop_def)
+
+
+fun Value where
+  "Value x = (Lg (Suc x) 2) - 1"
+
+definition 
+  "rec_value = CN rec_pred [CN rec_lg [S, constn 2]]"
+
+lemma value_lemma [simp]:
+  "rec_eval rec_value [x] = Value x"
+by (simp add: rec_value_def)
+
+text{*
+  @{text "rec_halt"} is the recursive function calculating the steps a TM needs to execute before
+  to reach a stardard final configuration. This recursive function is the only one
+  using @{text "Mn"} combinator. So it is the only non-primitive recursive function 
+  needs to be used in the construction of the universal function @{text "rec_uf"}.
+  *}
+
+definition 
+  "rec_halt = MN rec_nostop" 
+
+
+definition 
+  "rec_uf = CN rec_value [CN rec_right [CN rec_conf [rec_halt, Id 2 0, Id 2 1]]]"
+
+end
+
+
+(*
+
+
+
+fun mtest where
+  "mtest R 0 = if R 0 then 0 else 1"
+| "mtest R (Suc n) = (if R n then mtest R n else (Suc n))"
+
+
+lemma 
+  "rec_eval (rec_maxr2 f) [x, y1, y2] = XXX"
+apply(simp only: rec_maxr2_def)
+apply(case_tac x)
+apply(clarify)
+apply(subst rec_eval.simps)
+apply(simp only: constn_lemma)
+defer
+apply(clarify)
+apply(subst rec_eval.simps)
+apply(simp only: rec_maxr2_def[symmetric])
+apply(subst rec_eval.simps)
+apply(simp only: map.simps nth)
+apply(subst rec_eval.simps)
+apply(simp only: map.simps nth)
+apply(subst rec_eval.simps)
+apply(simp only: map.simps nth)
+apply(subst rec_eval.simps)
+apply(simp only: map.simps nth)
+apply(subst rec_eval.simps)
+apply(simp only: map.simps nth)
+apply(subst rec_eval.simps)
+apply(simp only: map.simps nth)
+
+
+definition
+  "rec_minr2 f = rec_sigma2 (rec_accum2 (CN rec_not [f]))"
+
+definition
+  "rec_maxr2 f = rec_sigma2 (CN rec_sign [CN (rec_sigma2 f) [S]])"
+
+definition Minr :: "(nat \<Rightarrow> nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat"
+  where "Minr R x ys = Min ({z | z. z \<le> x \<and> R z ys} \<union> {Suc x})"
+
+definition Maxr :: "(nat \<Rightarrow> nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat"
+  where "Maxr R x ys = Max ({z | z. z \<le> x \<and> R z ys} \<union> {0})"
+
+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