--- a/thys/Recs.thy Thu May 02 08:31:48 2013 +0100
+++ b/thys/Recs.thy Thu May 02 11:32:37 2013 +0100
@@ -636,7 +636,6 @@
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"}. *}
@@ -670,310 +669,6 @@
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)"
-
-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)"
-
-
-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)
-
-definition
- "rec_UF = CN rec_value [CN rec_right [CN rec_conf [Id 2 0, Id 2 1, rec_halt]]]"
-
end