# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1367479908 -3600
# Node ID af60d84e06773dafe469bef1b46d29c3a530809b
# Parent  8dba6ae39bf0c6740bf66ba8c8ac05e452f16ed6
introduced rec_if

diff -r 8dba6ae39bf0 -r af60d84e0677 thys/Recs.thy
--- a/thys/Recs.thy	Wed May 01 15:56:57 2013 +0100
+++ b/thys/Recs.thy	Thu May 02 08:31:48 2013 +0100
@@ -280,6 +280,12 @@
 definition 
   "rec_ifz = PR (Id 2 0) (Id 4 3)"
 
+text {* @{term "rec_if [z, x, y]"} returns x if z is *not* zero,
+  y otherwise *}
+
+definition 
+  "rec_if = CN rec_ifz [CN rec_not [Id 3 0], Id 3 1, Id 3 2]"
+
 text {*
   @{text "rec_less"} compares two arguments and returns @{text "1"} if
   the first is less than the second; otherwise returns @{text "0"}. *}
@@ -328,9 +334,9 @@
 definition
   "rec_quo = (let lhs = CN S [Id 3 0] in
               let rhs = CN rec_mult [Id 3 2, CN S [Id 3 1]] in
-              let cond = CN rec_noteq [lhs, rhs] in
-              let ifz = CN rec_ifz [cond, CN S [Id 3 1], Id 3 1]
-              in PR Z ifz)"
+              let cond = CN rec_eq [lhs, rhs] in
+              let if_stmt = CN rec_if [cond, CN S [Id 3 1], Id 3 1]
+              in PR Z if_stmt)"
 
 definition
   "rec_rem = CN rec_minus [Id 2 0, CN rec_mult [Id 2 1, rec_quo]]"
@@ -417,6 +423,10 @@
   "rec_eval rec_ifz [z, x, y] = (if z = 0 then x else y)" 
 by (case_tac z) (simp_all add: rec_ifz_def)
 
+lemma if_lemma [simp]:
+  "rec_eval rec_if [z, x, y] = (if 0 < z then x else y)" 
+by (simp add: rec_if_def)
+
 lemma sigma1_lemma [simp]: 
   shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. (rec_eval f)  [z, y])"
 by (induct x) (simp_all add: rec_sigma1_def)
@@ -611,33 +621,358 @@
   "rec_eval rec_lg [x, y] = Lg x y"
 by (simp add: rec_lg_def Lg_def Let_def)
 
+definition
+  "Lo x y = (if 1 < x \<and> 1 < y then BMax_rec (\<lambda>u. x mod (y ^ u) = 0) x else 0)"
+
+definition
+  "rec_lo = 
+     (let calc = CN rec_noteq [CN rec_rem [Id 3 1, CN rec_power [Id 3 2, Id 3 0]], Z] in
+      let max  = CN (rec_max2 calc) [Id 2 0, Id 2 0, Id 2 1] in
+      let cond = CN rec_conj [CN rec_less [constn 1, Id 2 0], CN rec_less [constn 1, Id 2 1]] 
+      in CN rec_ifz [cond, Z, max])"
+
+lemma lo_lemma [simp]:
+  "rec_eval rec_lo [x, y] = Lo x y"
+by (simp add: rec_lo_def Lo_def Let_def)
+
 
 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)
+
+
+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)
+
+
+
+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 specifation of the mutli-way branching statement on
+  page 79 of Boolos's book. *}
+
+type_synonym ftype = "nat list \<Rightarrow> nat"
+type_synonym rtype = "nat list \<Rightarrow> bool"
+
+fun Embranch :: "(ftype * rtype) list \<Rightarrow> nat list \<Rightarrow> nat"
+  where
+  "Embranch [] xs = 0" |
+  "Embranch ((g, c) # gcs) xs = (if c xs then g xs else Embranch gcs xs)"
+
+fun rec_embranch' :: "(recf * recf) list \<Rightarrow> nat \<Rightarrow> recf"
+  where
+  "rec_embranch' [] xs = Z" |
+  "rec_embranch' ((g, c) # gcs) xs = 
+      CN rec_add [CN rec_mult [g, c], rec_embranch' gcs xs]"
+
+fun rec_embranch :: "(recf * recf) list \<Rightarrow> recf"
+  where
+  "rec_embranch [] = Z"
+| "rec_embranch ((rg, rc) # rgcs) = (let vl = arity rg in 
+                                     rec_embranch' ((rg, rc) # rgcs) vl)"
+
+(*
+lemma embranch_lemma [simp]:
+  shows "rec_eval (rec_embranch (zip rgs rcs)) xs =
+           Embranch (zip (map rec_eval rgs) (map (\<lambda>r args. 0 < rec_eval r args) rcs)) xs"
+apply(induct rcs arbitrary: rgs)
+apply(simp)
+apply(simp)
+apply(case_tac rgs)
+apply(simp)
+apply(simp)
+apply(case_tac rcs)
+apply(simp_all)
+apply(rule conjI)
+*)
+
+fun Newleft0 :: "nat list \<Rightarrow> nat"
+  where
+  "Newleft0 [p, r] = p"
+
+definition rec_newleft0 :: "recf"
+  where
+  "rec_newleft0 = Id 2 0"
+
+fun Newrgt0 :: "nat list \<Rightarrow> nat"
+  where
+  "Newrgt0 [p, r] = r - Scan r"
+
+definition rec_newrgt0 :: "recf"
+  where
+  "rec_newrgt0 = CN rec_minus [Id 2 1, CN rec_scan [Id 2 1]]"
+
+(*newleft1, newrgt1: left rgt number after execute on step*)
+fun Newleft1 :: "nat list \<Rightarrow> nat"
+  where
+  "Newleft1 [p, r] = p"
+
+definition rec_newleft1 :: "recf"
+  where
+  "rec_newleft1 = Id 2 0"
+
+fun Newrgt1 :: "nat list \<Rightarrow> nat"
+  where
+  "Newrgt1 [p, r] = r + 1 - Scan r"
+
+definition 
+  "rec_newrgt1 = CN rec_minus [CN rec_add [Id 2 1, constn 1], CN rec_scan [Id 2 1]]"
+
+fun Newleft2 :: "nat list \<Rightarrow> nat"
+  where
+  "Newleft2 [p, r] = p div 2"
+
+definition 
+  "rec_newleft2 = CN rec_quo [Id 2 0, constn 2]"
+
+fun Newrgt2 :: "nat list \<Rightarrow> nat"
+  where
+  "Newrgt2 [p, r] = 2 * r + p mod 2"
+
+definition 
+  "rec_newrgt2 = CN rec_add [CN rec_mult [constn 2, Id 2 1],                     
+                             CN rec_rem [Id 2 0, constn 2]]"
+
+fun Newleft3 :: "nat list \<Rightarrow> nat"
+  where
+  "Newleft3 [p, r] = 2 * p + r mod 2"
+
+definition rec_newleft3 :: "recf"
+  where
+  "rec_newleft3 = CN rec_add [CN rec_mult [constn 2, Id 2 0], 
+                              CN rec_rem [Id 2 1, constn 2]]"
+
+fun Newrgt3 :: "nat list \<Rightarrow> nat"
+  where
+  "Newrgt3 [p, r] = r div 2"
+
+definition 
+  "rec_newrgt3 = CN rec_quo [Id 2 1, constn 2]"
+
+text {* The @{text "new_left"} function 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 Newleft0 [p, r] 
+                    else if a = 2 then Newleft2 [p, r]
+                    else if a = 3 then Newleft3 [p, r]
+                    else p)"
+
+definition
+    "rec_newleft =
+       (let g0 = CN rec_newleft0 [Id 3 0, Id 3 1] in 
+        let g1 = CN rec_newleft2 [Id 3 0, Id 3 1] in 
+        let g2 = CN rec_newleft3 [Id 3 0, Id 3 1] in 
+        let g3 = Id 3 0 in
+        let r0 = CN rec_disj [CN rec_eq [Id 3 2, constn 0],
+                              CN rec_eq [Id 3 2, constn 1]] in 
+        let r1 = CN rec_eq [Id 3 2, constn 2] in 
+        let r2 = CN rec_eq [Id 3 2, constn 3] in
+        let r3 = CN rec_less [constn 3, Id 3 2] in 
+        let gs = [g0, g1, g2, g3] in 
+        let rs = [r0, r1, r2, r3] in 
+        rec_embranch (zip gs rs))"
+
+
+fun Trpl :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+  "Trpl p q r = (Pi 0) ^ p * (Pi 1) ^ q * (Pi 2) ^ r"
+
+
+
 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)"
+  "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)"
+
+text {*
+  @{text "Conf m r k"} computes the TM configuration after 
+  @{text "k"} steps of execution of the TM coded as @{text "m"} 
+  starting from the initial configuration where the left number 
+  equals @{text "0"} and the right number equals @{text "r"}. 
+  *}
+fun Conf 
+  where
+  "Conf m r 0 = Trpl 0 (Suc 0) r"
+| "Conf m r (Suc t) = Newconf m (Conf m r t)"
 
 
-definition 
-  "value x = (Lg (Suc x) 2) - 1"
+text{* 
+  @{text "Nonstop m r t"} means that afer @{text "t"} steps of 
+  execution, the TM coded by @{text "m"} is not at a stardard 
+  final configuration.
+  *}
+fun Nostop 
+  where
+  "Nostop m r t = Nstd (Conf m r t)"
+
+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 value_def)
+  "rec_eval rec_value [x] = Value x"
+by (simp add: rec_value_def)
 
 definition 
-  where
-  "rec_UF = CN rec_valu [CN rec_right [CN rec_conf [Id 2 0, Id 2 1, rec_halt]]]"
+  "rec_UF = CN rec_value [CN rec_right [CN rec_conf [Id 2 0, Id 2 1, rec_halt]]]"
 
 end