156 @{text "rec_exec"} is the interpreter function for |
156 @{text "rec_exec"} is the interpreter function for |
157 reursive functions. The function is defined such that |
157 reursive functions. The function is defined such that |
158 it always returns meaningful results for primitive recursive |
158 it always returns meaningful results for primitive recursive |
159 functions. |
159 functions. |
160 *} |
160 *} |
161 function rec_exec :: "recf \<Rightarrow> nat list \<Rightarrow> nat" |
|
162 where |
|
163 "rec_exec z xs = 0" | |
|
164 "rec_exec s xs = (Suc (xs ! 0))" | |
|
165 "rec_exec (id m n) xs = (xs ! n)" | |
|
166 "rec_exec (Cn n f gs) xs = |
|
167 (let ys = (map (\<lambda> a. rec_exec a xs) gs) in |
|
168 rec_exec f ys)" | |
|
169 "rec_exec (Pr n f g) xs = |
|
170 (if last xs = 0 then |
|
171 rec_exec f (butlast xs) |
|
172 else rec_exec g (butlast xs @ [last xs - 1] @ |
|
173 [rec_exec (Pr n f g) (butlast xs @ [last xs - 1])]))" | |
|
174 "rec_exec (Mn n f) xs = (LEAST x. rec_exec f (xs @ [x]) = 0)" |
|
175 by pat_completeness auto |
|
176 termination |
|
177 proof |
|
178 show "wf (measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). last xs)])" |
|
179 by auto |
|
180 next |
|
181 fix n f gs xs x |
|
182 assume "(x::recf) \<in> set gs" |
|
183 thus "((x, xs), Cn n f gs, xs) \<in> |
|
184 measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]" |
|
185 by(induct gs, auto) |
|
186 next |
|
187 fix n f gs xs x |
|
188 assume "x = map (\<lambda>a. rec_exec a xs) gs" |
|
189 "\<And>x. x \<in> set gs \<Longrightarrow> rec_exec_dom (x, xs)" |
|
190 thus "((f, x), Cn n f gs, xs) \<in> |
|
191 measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]" |
|
192 by(auto) |
|
193 next |
|
194 fix n f g xs |
|
195 show "((f, butlast xs), Pr n f g, xs) \<in> |
|
196 measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]" |
|
197 by auto |
|
198 next |
|
199 fix n f g xs |
|
200 assume "last xs \<noteq> (0::nat)" thus |
|
201 "((Pr n f g, butlast xs @ [last xs - 1]), Pr n f g, xs) |
|
202 \<in> measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]" |
|
203 by auto |
|
204 next |
|
205 fix n f g xs |
|
206 show "((g, butlast xs @ [last xs - 1] @ [rec_exec (Pr n f g) (butlast xs @ [last xs - 1])]), |
|
207 Pr n f g, xs) \<in> measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]" |
|
208 by auto |
|
209 next |
|
210 fix n f xs x |
|
211 show "((f, xs @ [x]), Mn n f, xs) \<in> |
|
212 measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]" |
|
213 by auto |
|
214 qed |
|
215 |
161 |
216 declare rec_exec.simps[simp del] constn.simps[simp del] |
162 declare rec_exec.simps[simp del] constn.simps[simp del] |
217 |
163 |
218 text {* |
164 text {* |
219 Correctness of @{text "rec_add"}. |
165 Correctness of @{text "rec_add"}. |
2946 |
2891 |
2947 text {* |
2892 text {* |
2948 The lemma relates the interpreter of primitive fucntions with |
2893 The lemma relates the interpreter of primitive fucntions with |
2949 the calculation relation of general recursive functions. |
2894 the calculation relation of general recursive functions. |
2950 *} |
2895 *} |
2951 lemma prime_rel_exec_eq: "primerec r (length xs) |
|
2952 \<Longrightarrow> rec_calc_rel r xs rs = (rec_exec r xs = rs)" |
|
2953 proof(induct r xs arbitrary: rs rule: rec_exec.induct, simp_all) |
|
2954 fix xs rs |
|
2955 assume "primerec z (length (xs::nat list))" |
|
2956 hence "length xs = Suc 0" by(erule_tac prime_z_reverse, simp) |
|
2957 thus "rec_calc_rel z xs rs = (rec_exec z xs = rs)" |
|
2958 apply(case_tac xs, simp, auto) |
|
2959 apply(erule_tac calc_z_reverse, simp add: rec_exec.simps) |
|
2960 apply(simp add: rec_exec.simps, rule_tac calc_z) |
|
2961 done |
|
2962 next |
|
2963 fix xs rs |
|
2964 assume "primerec s (length (xs::nat list))" |
|
2965 hence "length xs = Suc 0" .. |
|
2966 thus "rec_calc_rel s xs rs = (rec_exec s xs = rs)" |
|
2967 by(case_tac xs, auto simp: rec_exec.simps intro: calc_s |
|
2968 elim: calc_s_reverse) |
|
2969 next |
|
2970 fix m n xs rs |
|
2971 assume "primerec (recf.id m n) (length (xs::nat list))" |
|
2972 thus |
|
2973 "rec_calc_rel (recf.id m n) xs rs = |
|
2974 (rec_exec (recf.id m n) xs = rs)" |
|
2975 apply(erule_tac prime_id_reverse) |
|
2976 apply(simp add: rec_exec.simps, auto) |
|
2977 apply(erule_tac calc_id_reverse, simp) |
|
2978 apply(rule_tac calc_id, auto) |
|
2979 done |
|
2980 next |
|
2981 fix n f gs xs rs |
|
2982 assume ind1: |
|
2983 "\<And>x rs. \<lbrakk>x \<in> set gs; primerec x (length xs)\<rbrakk> \<Longrightarrow> |
|
2984 rec_calc_rel x xs rs = (rec_exec x xs = rs)" |
|
2985 and ind2: |
|
2986 "\<And>x rs. \<lbrakk>x = map (\<lambda>a. rec_exec a xs) gs; |
|
2987 primerec f (length gs)\<rbrakk> \<Longrightarrow> |
|
2988 rec_calc_rel f (map (\<lambda>a. rec_exec a xs) gs) rs = |
|
2989 (rec_exec f (map (\<lambda>a. rec_exec a xs) gs) = rs)" |
|
2990 and h: "primerec (Cn n f gs) (length xs)" |
|
2991 show "rec_calc_rel (Cn n f gs) xs rs = |
|
2992 (rec_exec (Cn n f gs) xs = rs)" |
|
2993 proof(auto simp: rec_exec.simps, erule_tac calc_cn_reverse, auto) |
|
2994 fix ys |
|
2995 assume g1:"\<forall>k<length gs. rec_calc_rel (gs ! k) xs (ys ! k)" |
|
2996 and g2: "length ys = length gs" |
|
2997 and g3: "rec_calc_rel f ys rs" |
|
2998 have "rec_calc_rel f (map (\<lambda>a. rec_exec a xs) gs) rs = |
|
2999 (rec_exec f (map (\<lambda>a. rec_exec a xs) gs) = rs)" |
|
3000 apply(rule_tac ind2, auto) |
|
3001 using h |
|
3002 apply(erule_tac prime_cn_reverse, simp) |
|
3003 done |
|
3004 moreover have "ys = (map (\<lambda>a. rec_exec a xs) gs)" |
|
3005 proof(rule_tac nth_equalityI, auto simp: g2) |
|
3006 fix i |
|
3007 assume "i < length gs" thus "ys ! i = rec_exec (gs!i) xs" |
|
3008 using ind1[of "gs ! i" "ys ! i"] g1 h |
|
3009 apply(erule_tac prime_cn_reverse, simp) |
|
3010 done |
|
3011 qed |
|
3012 ultimately show "rec_exec f (map (\<lambda>a. rec_exec a xs) gs) = rs" |
|
3013 using g3 |
|
3014 by(simp) |
|
3015 next |
|
3016 from h show |
|
3017 "rec_calc_rel (Cn n f gs) xs |
|
3018 (rec_exec f (map (\<lambda>a. rec_exec a xs) gs))" |
|
3019 apply(rule_tac rs = "(map (\<lambda>a. rec_exec a xs) gs)" in calc_cn, |
|
3020 auto) |
|
3021 apply(erule_tac [!] prime_cn_reverse, auto) |
|
3022 proof - |
|
3023 fix k |
|
3024 assume "k < length gs" "primerec f (length gs)" |
|
3025 "\<forall>i<length gs. primerec (gs ! i) (length xs)" |
|
3026 thus "rec_calc_rel (gs ! k) xs (rec_exec (gs ! k) xs)" |
|
3027 using ind1[of "gs!k" "(rec_exec (gs ! k) xs)"] |
|
3028 by(simp) |
|
3029 next |
|
3030 assume "primerec f (length gs)" |
|
3031 "\<forall>i<length gs. primerec (gs ! i) (length xs)" |
|
3032 thus "rec_calc_rel f (map (\<lambda>a. rec_exec a xs) gs) |
|
3033 (rec_exec f (map (\<lambda>a. rec_exec a xs) gs))" |
|
3034 using ind2[of "(map (\<lambda>a. rec_exec a xs) gs)" |
|
3035 "(rec_exec f (map (\<lambda>a. rec_exec a xs) gs))"] |
|
3036 by simp |
|
3037 qed |
|
3038 qed |
|
3039 next |
|
3040 fix n f g xs rs |
|
3041 assume ind1: |
|
3042 "\<And>rs. \<lbrakk>last xs = 0; primerec f (length xs - Suc 0)\<rbrakk> |
|
3043 \<Longrightarrow> rec_calc_rel f (butlast xs) rs = |
|
3044 (rec_exec f (butlast xs) = rs)" |
|
3045 and ind2 : |
|
3046 "\<And>rs. \<lbrakk>0 < last xs; |
|
3047 primerec (Pr n f g) (Suc (length xs - Suc 0))\<rbrakk> \<Longrightarrow> |
|
3048 rec_calc_rel (Pr n f g) (butlast xs @ [last xs - Suc 0]) rs |
|
3049 = (rec_exec (Pr n f g) (butlast xs @ [last xs - Suc 0]) = rs)" |
|
3050 and ind3: |
|
3051 "\<And>rs. \<lbrakk>0 < last xs; primerec g (Suc (Suc (length xs - Suc 0)))\<rbrakk> |
|
3052 \<Longrightarrow> rec_calc_rel g (butlast xs @ |
|
3053 [last xs - Suc 0, rec_exec (Pr n f g) |
|
3054 (butlast xs @ [last xs - Suc 0])]) rs = |
|
3055 (rec_exec g (butlast xs @ [last xs - Suc 0, |
|
3056 rec_exec (Pr n f g) |
|
3057 (butlast xs @ [last xs - Suc 0])]) = rs)" |
|
3058 and h: "primerec (Pr n f g) (length (xs::nat list))" |
|
3059 show "rec_calc_rel (Pr n f g) xs rs = (rec_exec (Pr n f g) xs = rs)" |
|
3060 proof(auto) |
|
3061 assume "rec_calc_rel (Pr n f g) xs rs" |
|
3062 thus "rec_exec (Pr n f g) xs = rs" |
|
3063 proof(erule_tac calc_pr_reverse) |
|
3064 fix l |
|
3065 assume g: "xs = l @ [0]" |
|
3066 "rec_calc_rel f l rs" |
|
3067 "n = length l" |
|
3068 thus "rec_exec (Pr n f g) xs = rs" |
|
3069 using ind1[of rs] h |
|
3070 apply(simp add: rec_exec.simps, |
|
3071 erule_tac prime_pr_reverse, simp) |
|
3072 done |
|
3073 next |
|
3074 fix l y ry |
|
3075 assume d:"xs = l @ [Suc y]" |
|
3076 "rec_calc_rel (Pr (length l) f g) (l @ [y]) ry" |
|
3077 "n = length l" |
|
3078 "rec_calc_rel g (l @ [y, ry]) rs" |
|
3079 moreover hence "primerec g (Suc (Suc n))" using h |
|
3080 proof(erule_tac prime_pr_reverse) |
|
3081 assume "primerec g (Suc (Suc n))" "length xs = Suc n" |
|
3082 thus "?thesis" by simp |
|
3083 qed |
|
3084 ultimately show "rec_exec (Pr n f g) xs = rs" |
|
3085 apply(simp) |
|
3086 using ind3[of rs] |
|
3087 apply(simp add: rec_pr_Suc_simp_rewrite) |
|
3088 using ind2[of ry] h |
|
3089 apply(simp) |
|
3090 done |
|
3091 qed |
|
3092 next |
|
3093 show "rec_calc_rel (Pr n f g) xs (rec_exec (Pr n f g) xs)" |
|
3094 proof - |
|
3095 have "rec_calc_rel (Pr n f g) (butlast xs @ [last xs]) |
|
3096 (rec_exec (Pr n f g) (butlast xs @ [last xs]))" |
|
3097 using h |
|
3098 apply(erule_tac prime_pr_reverse, simp) |
|
3099 apply(case_tac "last xs", simp) |
|
3100 apply(rule_tac calc_pr_zero, simp) |
|
3101 using ind1[of "rec_exec (Pr n f g) (butlast xs @ [0])"] |
|
3102 apply(simp add: rec_exec.simps, simp, simp, simp) |
|
3103 apply(rule_tac rk = "rec_exec (Pr n f g) |
|
3104 (butlast xs@[last xs - Suc 0])" in calc_pr_ind) |
|
3105 using ind2[of "rec_exec (Pr n f g) |
|
3106 (butlast xs @ [last xs - Suc 0])"] h |
|
3107 apply(simp, simp, simp) |
|
3108 proof - |
|
3109 fix nat |
|
3110 assume "length xs = Suc n" |
|
3111 "primerec g (Suc (Suc n))" |
|
3112 "last xs = Suc nat" |
|
3113 thus |
|
3114 "rec_calc_rel g (butlast xs @ [nat, rec_exec (Pr n f g) |
|
3115 (butlast xs @ [nat])]) (rec_exec (Pr n f g) (butlast xs @ [Suc nat]))" |
|
3116 using ind3[of "rec_exec (Pr n f g) |
|
3117 (butlast xs @ [Suc nat])"] |
|
3118 apply(simp add: rec_exec.simps) |
|
3119 done |
|
3120 qed |
|
3121 thus "rec_calc_rel (Pr n f g) xs (rec_exec (Pr n f g) xs)" |
|
3122 using h |
|
3123 apply(erule_tac prime_pr_reverse, simp) |
|
3124 apply(subgoal_tac "butlast xs @ [last xs] = xs", simp) |
|
3125 apply(case_tac xs, simp, simp) |
|
3126 done |
|
3127 qed |
|
3128 qed |
|
3129 next |
|
3130 fix n f xs rs |
|
3131 assume "primerec (Mn n f) (length (xs::nat list))" |
|
3132 thus "rec_calc_rel (Mn n f) xs rs = (rec_exec (Mn n f) xs = rs)" |
|
3133 by(erule_tac prime_mn_reverse) |
|
3134 qed |
|
3135 |
2896 |
3136 declare numeral_2_eq_2[simp] numeral_3_eq_3[simp] |
2897 declare numeral_2_eq_2[simp] numeral_3_eq_3[simp] |
3137 |
2898 |
3138 lemma [intro]: "primerec rec_right (Suc 0)" |
2899 lemma [intro]: "primerec rec_right (Suc 0)" |
3139 apply(simp add: rec_right_def rec_lo_def Let_def) |
2900 apply(simp add: rec_right_def rec_lo_def Let_def) |
3140 apply(tactic {* resolve_tac [@{thm prime_cn}, |
2901 apply(tactic {* resolve_tac [@{thm prime_cn}, |
3141 @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+ |
2902 @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+ |
3142 done |
|
3143 |
|
3144 lemma [simp]: |
|
3145 "rec_calc_rel rec_right [r] rs = (rec_exec rec_right [r] = rs)" |
|
3146 apply(rule_tac prime_rel_exec_eq, auto) |
|
3147 done |
2903 done |
3148 |
2904 |
3149 lemma [intro]: "primerec rec_pi (Suc 0)" |
2905 lemma [intro]: "primerec rec_pi (Suc 0)" |
3150 apply(simp add: rec_pi_def rec_dummy_pi_def |
2906 apply(simp add: rec_pi_def rec_dummy_pi_def |
3151 rec_np_def rec_fac_def rec_prime_def |
2907 rec_np_def rec_fac_def rec_prime_def |
3301 rec_newstat_def) |
3051 rec_newstat_def) |
3302 apply(tactic {* resolve_tac [@{thm prime_cn}, |
3052 apply(tactic {* resolve_tac [@{thm prime_cn}, |
3303 @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+ |
3053 @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+ |
3304 done |
3054 done |
3305 |
3055 |
3306 lemma nonstop_eq[simp]: |
3056 lemma primerec_terminate: |
3307 "rec_calc_rel rec_nonstop [m, r, t] rs = |
3057 "\<lbrakk>primerec f x; length xs = x\<rbrakk> \<Longrightarrow> terminate f xs" |
3308 (rec_exec rec_nonstop [m, r, t] = rs)" |
3058 proof(induct arbitrary: xs rule: primerec.induct) |
3309 apply(rule prime_rel_exec_eq, auto) |
3059 fix xs |
3310 done |
3060 assume "length (xs::nat list) = Suc 0" thus "terminate z xs" |
3311 |
3061 by(case_tac xs, auto intro: termi_z) |
3312 lemma halt_lemma': |
3062 next |
3313 "rec_calc_rel rec_halt [m, r] t = |
3063 fix xs |
3314 (rec_calc_rel rec_nonstop [m, r, t] 0 \<and> |
3064 assume "length (xs::nat list) = Suc 0" thus "terminate s xs" |
3315 (\<forall> t'< t. |
3065 by(case_tac xs, auto intro: termi_s) |
3316 (\<exists> y. rec_calc_rel rec_nonstop [m, r, t'] y \<and> |
3066 next |
3317 y \<noteq> 0)))" |
3067 fix n m xs |
3318 apply(auto simp: rec_halt_def) |
3068 assume "n < m" "length (xs::nat list) = m" thus "terminate (id m n) xs" |
3319 apply(erule calc_mn_reverse, simp) |
3069 by(erule_tac termi_id, simp) |
3320 apply(erule_tac calc_mn_reverse) |
3070 next |
3321 apply(erule_tac x = t' in allE, simp) |
3071 fix f k gs m n xs |
3322 apply(rule_tac calc_mn, simp_all) |
3072 assume ind: "\<forall>i<length gs. primerec (gs ! i) m \<and> (\<forall>x. length x = m \<longrightarrow> terminate (gs ! i) x)" |
3323 done |
3073 and ind2: "\<And> xs. length xs = k \<Longrightarrow> terminate f xs" |
|
3074 and h: "primerec f k" "length gs = k" "m = n" "length (xs::nat list) = m" |
|
3075 have "terminate f (map (\<lambda>g. rec_exec g xs) gs)" |
|
3076 using ind2[of "(map (\<lambda>g. rec_exec g xs) gs)"] h |
|
3077 by simp |
|
3078 moreover have "\<forall>g\<in>set gs. terminate g xs" |
|
3079 using ind h |
|
3080 by(auto simp: set_conv_nth) |
|
3081 ultimately show "terminate (Cn n f gs) xs" |
|
3082 using h |
|
3083 by(rule_tac termi_cn, auto) |
|
3084 next |
|
3085 fix f n g m xs |
|
3086 assume ind1: "\<And>xs. length xs = n \<Longrightarrow> terminate f xs" |
|
3087 and ind2: "\<And>xs. length xs = Suc (Suc n) \<Longrightarrow> terminate g xs" |
|
3088 and h: "primerec f n" " primerec g (Suc (Suc n))" " m = Suc n" "length (xs::nat list) = m" |
|
3089 have "\<forall>y<last xs. terminate g (butlast xs @ [y, rec_exec (Pr n f g) (butlast xs @ [y])])" |
|
3090 using h |
|
3091 apply(auto) |
|
3092 by(rule_tac ind2, simp) |
|
3093 moreover have "terminate f (butlast xs)" |
|
3094 using ind1[of "butlast xs"] h |
|
3095 by simp |
|
3096 moreover have "length (butlast xs) = n" |
|
3097 using h by simp |
|
3098 ultimately have "terminate (Pr n f g) (butlast xs @ [last xs])" |
|
3099 by(rule_tac termi_pr, simp_all) |
|
3100 thus "terminate (Pr n f g) xs" |
|
3101 using h |
|
3102 by(case_tac "xs = []", auto) |
|
3103 qed |
3324 |
3104 |
3325 text {* |
3105 text {* |
3326 The following lemma gives the correctness of @{text "rec_halt"}. |
3106 The following lemma gives the correctness of @{text "rec_halt"}. |
3327 It says: if @{text "rec_halt"} calculates that the TM coded by @{text "m"} |
3107 It says: if @{text "rec_halt"} calculates that the TM coded by @{text "m"} |
3328 will reach a standard final configuration after @{text "t"} steps of execution, then it is indeed so. |
3108 will reach a standard final configuration after @{text "t"} steps of execution, then it is indeed so. |
3329 *} |
3109 *} |
3330 lemma halt_lemma: |
3110 |
3331 "rec_calc_rel (rec_halt) [m, r] t = |
|
3332 (rec_exec rec_nonstop [m, r, t] = 0 \<and> |
|
3333 (\<forall> t'< t. (\<exists> y. rec_exec rec_nonstop [m, r, t'] = y |
|
3334 \<and> y \<noteq> 0)))" |
|
3335 using halt_lemma'[of m r t] |
|
3336 by simp |
|
3337 |
|
3338 text {*F: universal machine*} |
3111 text {*F: universal machine*} |
3339 |
3112 |
3340 text {* |
3113 text {* |
3341 @{text "valu r"} extracts computing result out of the right number @{text "r"}. |
3114 @{text "valu r"} extracts computing result out of the right number @{text "r"}. |
3342 *} |
3115 *} |
3391 apply(case_tac "k = n", simp_all add: get_fstn_args.simps |
3159 apply(case_tac "k = n", simp_all add: get_fstn_args.simps |
3392 nth_append) |
3160 nth_append) |
3393 done |
3161 done |
3394 |
3162 |
3395 lemma [simp]: |
3163 lemma [simp]: |
3396 "\<lbrakk>ys \<noteq> []; k < length ys\<rbrakk> \<Longrightarrow> |
3164 "\<lbrakk>ys \<noteq> []; |
|
3165 k < length ys\<rbrakk> \<Longrightarrow> |
3397 (get_fstn_args (length ys) (length ys) ! k) = |
3166 (get_fstn_args (length ys) (length ys) ! k) = |
3398 id (length ys) (k)" |
3167 id (length ys) (k)" |
3399 by(erule_tac get_fstn_args_nth) |
3168 by(erule_tac get_fstn_args_nth) |
3400 |
3169 |
3401 lemma calc_rel_get_pren: |
3170 lemma terminate_halt_lemma: |
3402 "\<lbrakk>ys \<noteq> []; k < length ys\<rbrakk> \<Longrightarrow> |
3171 "\<lbrakk>rec_exec rec_nonstop ([m, r] @ [t]) = 0; |
3403 rec_calc_rel (get_fstn_args (length ys) (length ys) ! k) ys |
3172 \<forall>i<t. 0 < rec_exec rec_nonstop ([m, r] @ [i])\<rbrakk> \<Longrightarrow> terminate rec_halt [m, r]" |
3404 (ys ! k)" |
3173 apply(simp add: rec_halt_def) |
3405 apply(simp) |
3174 apply(rule_tac termi_mn, auto) |
3406 apply(rule_tac calc_id, auto) |
3175 apply(rule_tac [!] primerec_terminate, auto) |
3407 done |
3176 done |
3408 |
3177 |
3409 lemma [elim]: |
|
3410 "\<lbrakk>xs \<noteq> []; k < Suc (length xs)\<rbrakk> \<Longrightarrow> |
|
3411 rec_calc_rel (get_fstn_args (Suc (length xs)) |
|
3412 (Suc (length xs)) ! k) (m # xs) ((m # xs) ! k)" |
|
3413 using calc_rel_get_pren[of "m#xs" k] |
|
3414 apply(simp) |
|
3415 done |
|
3416 |
3178 |
3417 text {* |
3179 text {* |
3418 The correctness of @{text "rec_F"}, halt case. |
3180 The correctness of @{text "rec_F"}, halt case. |
3419 *} |
3181 *} |
3420 lemma F_lemma: |
3182 |
3421 "rec_calc_rel rec_halt [m, r] t \<Longrightarrow> |
3183 lemma F_lemma: "rec_exec rec_halt [m, r] = t \<Longrightarrow> rec_exec rec_F [m, r] = (valu (rght (conf m r t)))" |
3422 rec_calc_rel rec_F [m, r] (valu (rght (conf m r t)))" |
3184 by(simp add: rec_F_def rec_exec.simps value_lemma right_lemma conf_lemma halt_lemma) |
|
3185 |
|
3186 lemma terminate_F_lemma: "terminate rec_halt [m, r] \<Longrightarrow> terminate rec_F [m, r]" |
3423 apply(simp add: rec_F_def) |
3187 apply(simp add: rec_F_def) |
3424 apply(rule_tac rs = "[rght (conf m r t)]" in calc_cn, |
3188 apply(rule_tac termi_cn, auto) |
3425 auto simp: value_lemma) |
3189 apply(rule_tac primerec_terminate, auto) |
3426 apply(rule_tac rs = "[conf m r t]" in calc_cn, |
3190 apply(rule_tac termi_cn, auto) |
3427 auto simp: right_lemma) |
3191 apply(rule_tac primerec_terminate, auto) |
3428 apply(rule_tac rs = "[m, r, t]" in calc_cn, auto) |
3192 apply(rule_tac termi_cn, auto) |
3429 apply(subgoal_tac " k = 0 \<or> k = Suc 0 \<or> k = Suc (Suc 0)", |
3193 apply(rule_tac primerec_terminate, auto) |
3430 auto simp:nth_append) |
3194 apply(rule_tac [!] termi_id, auto) |
3431 apply(rule_tac [1-2] calc_id, simp_all add: conf_lemma) |
3195 done |
3432 done |
|
3433 |
|
3434 |
3196 |
3435 text {* |
3197 text {* |
3436 The correctness of @{text "rec_F"}, nonhalt case. |
3198 The correctness of @{text "rec_F"}, nonhalt case. |
3437 *} |
3199 *} |
3438 lemma F_lemma2: |
|
3439 "\<forall> t. \<not> rec_calc_rel rec_halt [m, r] t \<Longrightarrow> |
|
3440 \<forall> rs. \<not> rec_calc_rel rec_F [m, r] rs" |
|
3441 apply(auto simp: rec_F_def) |
|
3442 apply(erule_tac calc_cn_reverse, simp (no_asm_use))+ |
|
3443 proof - |
|
3444 fix rs rsa rsb rsc |
|
3445 assume h: |
|
3446 "\<forall>t. \<not> rec_calc_rel rec_halt [m, r] t" |
|
3447 "length rsa = Suc 0" |
|
3448 "rec_calc_rel rec_valu rsa rs" |
|
3449 "length rsb = Suc 0" |
|
3450 "rec_calc_rel rec_right rsb (rsa ! 0)" |
|
3451 "length rsc = (Suc (Suc (Suc 0)))" |
|
3452 "rec_calc_rel rec_conf rsc (rsb ! 0)" |
|
3453 and g: "\<forall>k<Suc (Suc (Suc 0)). rec_calc_rel ([recf.id (Suc (Suc 0)) 0, |
|
3454 recf.id (Suc (Suc 0)) (Suc 0), rec_halt] ! k) [m, r] (rsc ! k)" |
|
3455 have "rec_calc_rel (rec_halt ) [m, r] |
|
3456 (rsc ! (Suc (Suc 0)))" |
|
3457 using g |
|
3458 apply(erule_tac x = "(Suc (Suc 0))" in allE) |
|
3459 apply(simp add:nth_append) |
|
3460 done |
|
3461 thus "False" |
|
3462 using h |
|
3463 apply(erule_tac x = "ysb ! (Suc (Suc 0))" in allE, simp) |
|
3464 done |
|
3465 qed |
|
3466 |
|
3467 |
3200 |
3468 subsection {* Coding function of TMs *} |
3201 subsection {* Coding function of TMs *} |
3469 |
3202 |
3470 text {* |
3203 text {* |
3471 The purpose of this section is to get the coding function of Turing Machine, which is |
3204 The purpose of this section is to get the coding function of Turing Machine, which is |
4858 text {* |
4591 text {* |
4859 The correntess of @{text "rec_F"} which relates the interpreter function @{text "rec_F"} with the |
4592 The correntess of @{text "rec_F"} which relates the interpreter function @{text "rec_F"} with the |
4860 execution of of TMs. |
4593 execution of of TMs. |
4861 *} |
4594 *} |
4862 |
4595 |
|
4596 lemma terminate_halt: |
|
4597 "\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up>m, Oc\<up>rs@Bk\<up>n); |
|
4598 tm_wf (tp,0); 0<rs\<rbrakk> \<Longrightarrow> terminate rec_halt [code tp, (bl2wc (<lm>))]" |
|
4599 apply(frule_tac halt_least_step, auto) |
|
4600 thm terminate_halt_lemma |
|
4601 apply(rule_tac t = stpa in terminate_halt_lemma) |
|
4602 apply(simp_all add: nonstop_lemma, auto) |
|
4603 done |
|
4604 |
|
4605 lemma terminate_F: |
|
4606 "\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up>m, Oc\<up>rs@Bk\<up>n); |
|
4607 tm_wf (tp,0); 0<rs\<rbrakk> \<Longrightarrow> terminate rec_F [code tp, (bl2wc (<lm>))]" |
|
4608 apply(drule_tac terminate_halt, simp_all) |
|
4609 apply(erule_tac terminate_F_lemma) |
|
4610 done |
|
4611 |
4863 lemma F_correct: |
4612 lemma F_correct: |
4864 "\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up>m, Oc\<up>rs@Bk\<up>n); |
4613 "\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up>m, Oc\<up>rs@Bk\<up>n); |
4865 tm_wf (tp,0); 0<rs\<rbrakk> |
4614 tm_wf (tp,0); 0<rs\<rbrakk> |
4866 \<Longrightarrow> rec_calc_rel rec_F [code tp, (bl2wc (<lm>))] (rs - Suc 0)" |
4615 \<Longrightarrow> rec_exec rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)" |
4867 apply(frule_tac halt_least_step, auto) |
4616 apply(frule_tac halt_least_step, auto) |
4868 apply(frule_tac nonstop_t_eq, auto simp: nonstop_lemma) |
4617 apply(frule_tac nonstop_t_eq, auto simp: nonstop_lemma) |
4869 using rec_t_eq_steps[of tp l lm stp] |
4618 using rec_t_eq_steps[of tp l lm stp] |
4870 apply(simp add: conf_lemma) |
4619 apply(simp add: conf_lemma) |
4871 proof - |
4620 proof - |