--- 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