equal
deleted
inserted
replaced
560 apply(drule_tac x = "rec_exec rt xs" in rec_sigma_ex, simp) |
560 apply(drule_tac x = "rec_exec rt xs" in rec_sigma_ex, simp) |
561 apply(drule_tac x = "rec_exec rt xs" in rec_sigma_ex, simp) |
561 apply(drule_tac x = "rec_exec rt xs" in rec_sigma_ex, simp) |
562 done |
562 done |
563 |
563 |
564 text {* |
564 text {* |
565 Defintiion of @{text "Min[R]"} on page 77 of Boolos's book. |
565 Definition of @{text "Min[R]"} on page 77 of Boolos's book. |
566 *} |
566 *} |
567 |
567 |
568 fun Minr :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> nat" |
568 fun Minr :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> nat" |
569 where "Minr Rr xs w = (let setx = {y | y. (y \<le> w) \<and> Rr (xs @ [y])} in |
569 where "Minr Rr xs w = (let setx = {y | y. (y \<le> w) \<and> Rr (xs @ [y])} in |
570 if (setx = {}) then (Suc w) |
570 if (setx = {}) then (Suc w) |
846 lemma le_lemma: |
846 lemma le_lemma: |
847 "\<And>x y. rec_exec rec_le [x, y] = (if (x \<le> y) then 1 else 0)" |
847 "\<And>x y. rec_exec rec_le [x, y] = (if (x \<le> y) then 1 else 0)" |
848 by(auto simp: rec_le_def rec_exec.simps) |
848 by(auto simp: rec_le_def rec_exec.simps) |
849 |
849 |
850 text {* |
850 text {* |
851 Defintiion of @{text "Max[Rr]"} on page 77 of Boolos's book. |
851 Definition of @{text "Max[Rr]"} on page 77 of Boolos's book. |
852 *} |
852 *} |
853 |
853 |
854 fun Maxr :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> nat" |
854 fun Maxr :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> nat" |
855 where |
855 where |
856 "Maxr Rr xs w = (let setx = {y. y \<le> w \<and> Rr (xs @[y])} in |
856 "Maxr Rr xs w = (let setx = {y. y \<le> w \<and> Rr (xs @[y])} in |
872 [Cn (Suc (Suc vl)) |
872 [Cn (Suc (Suc vl)) |
873 rr (get_fstn_args (Suc (Suc vl)) |
873 rr (get_fstn_args (Suc (Suc vl)) |
874 (vl - 1) @ |
874 (vl - 1) @ |
875 [id (Suc (Suc vl)) ((Suc vl))])] in |
875 [id (Suc (Suc vl)) ((Suc vl))])] in |
876 let rf = Cn (Suc (Suc vl)) rec_disj [rf1, rf2] in |
876 let rf = Cn (Suc (Suc vl)) rec_disj [rf1, rf2] in |
877 let rq = rec_all rt rf in |
|
878 let Qf = Cn (Suc vl) rec_not [rec_all rt rf] |
877 let Qf = Cn (Suc vl) rec_not [rec_all rt rf] |
879 in Cn vl (rec_sigma Qf) (get_fstn_args vl vl @ |
878 in Cn vl (rec_sigma Qf) (get_fstn_args vl vl @ |
880 [id vl (vl - 1)]))" |
879 [id vl (vl - 1)]))" |
881 |
880 |
882 declare rec_maxr.simps[simp del] Maxr.simps[simp del] |
881 declare rec_maxr.simps[simp del] Maxr.simps[simp del] |
2174 | "listsum2 xs (Suc n) = listsum2 xs n + xs ! n" |
2173 | "listsum2 xs (Suc n) = listsum2 xs n + xs ! n" |
2175 |
2174 |
2176 fun rec_listsum2 :: "nat \<Rightarrow> nat \<Rightarrow> recf" |
2175 fun rec_listsum2 :: "nat \<Rightarrow> nat \<Rightarrow> recf" |
2177 where |
2176 where |
2178 "rec_listsum2 vl 0 = Cn vl z [id vl 0]" |
2177 "rec_listsum2 vl 0 = Cn vl z [id vl 0]" |
2179 | "rec_listsum2 vl (Suc n) = Cn vl rec_add |
2178 | "rec_listsum2 vl (Suc n) = Cn vl rec_add [rec_listsum2 vl n, id vl n]" |
2180 [rec_listsum2 vl n, id vl (n)]" |
|
2181 |
2179 |
2182 declare listsum2.simps[simp del] rec_listsum2.simps[simp del] |
2180 declare listsum2.simps[simp del] rec_listsum2.simps[simp del] |
2183 |
2181 |
2184 lemma listsum2_lemma: "\<lbrakk>length xs = vl; n \<le> vl\<rbrakk> \<Longrightarrow> |
2182 lemma listsum2_lemma: "\<lbrakk>length xs = vl; n \<le> vl\<rbrakk> \<Longrightarrow> |
2185 rec_exec (rec_listsum2 vl n) xs = listsum2 xs n" |
2183 rec_exec (rec_listsum2 vl n) xs = listsum2 xs n" |
2221 "strt xs = (let ys = map Suc xs in |
2219 "strt xs = (let ys = map Suc xs in |
2222 strt' ys (length ys))" |
2220 strt' ys (length ys))" |
2223 |
2221 |
2224 fun rec_map :: "recf \<Rightarrow> nat \<Rightarrow> recf list" |
2222 fun rec_map :: "recf \<Rightarrow> nat \<Rightarrow> recf list" |
2225 where |
2223 where |
2226 "rec_map rf vl = map (\<lambda> i. Cn vl rf [id vl (i)]) [0..<vl]" |
2224 "rec_map rf vl = map (\<lambda> i. Cn vl rf [id vl i]) [0..<vl]" |
2227 |
2225 |
2228 text {* |
2226 text {* |
2229 @{text "rec_strt"} is the recursive function used to implement @{text "strt"}. |
2227 @{text "rec_strt"} is the recursive function used to implement @{text "strt"}. |
2230 *} |
2228 *} |
2231 fun rec_strt :: "nat \<Rightarrow> recf" |
2229 fun rec_strt :: "nat \<Rightarrow> recf" |