--- a/thys/UF.thy Wed Apr 24 09:49:00 2013 +0100
+++ b/thys/UF.thy Thu Apr 25 21:37:05 2013 +0100
@@ -153,46 +153,46 @@
@ [Cn (Suc vl) s [id (Suc vl) (vl - 1)]])]))"
-declare rec_exec.simps[simp del] constn.simps[simp del]
+declare rec_eval.simps[simp del] constn.simps[simp del]
section {* Correctness of various recursive functions *}
-lemma add_lemma: "rec_exec rec_add [x, y] = x + y"
-by(induct_tac y, auto simp: rec_add_def rec_exec.simps)
-
-lemma mult_lemma: "rec_exec rec_mult [x, y] = x * y"
-by(induct_tac y, auto simp: rec_mult_def rec_exec.simps add_lemma)
-
-lemma pred_lemma: "rec_exec rec_pred [x] = x - 1"
-by(induct_tac x, auto simp: rec_pred_def rec_exec.simps)
-
-lemma minus_lemma: "rec_exec rec_minus [x, y] = x - y"
-by(induct_tac y, auto simp: rec_exec.simps rec_minus_def pred_lemma)
-
-lemma sg_lemma: "rec_exec rec_sg [x] = (if x = 0 then 0 else 1)"
-by(auto simp: rec_sg_def minus_lemma rec_exec.simps constn.simps)
-
-lemma constn_lemma: "rec_exec (constn n) [x] = n"
-by(induct n, auto simp: rec_exec.simps constn.simps)
-
-lemma less_lemma: "rec_exec rec_less [x, y] = (if x < y then 1 else 0)"
-by(induct_tac y, auto simp: rec_exec.simps
+lemma add_lemma: "rec_eval rec_add [x, y] = x + y"
+by(induct_tac y, auto simp: rec_add_def rec_eval.simps)
+
+lemma mult_lemma: "rec_eval rec_mult [x, y] = x * y"
+by(induct_tac y, auto simp: rec_mult_def rec_eval.simps add_lemma)
+
+lemma pred_lemma: "rec_eval rec_pred [x] = x - 1"
+by(induct_tac x, auto simp: rec_pred_def rec_eval.simps)
+
+lemma minus_lemma: "rec_eval rec_minus [x, y] = x - y"
+by(induct_tac y, auto simp: rec_eval.simps rec_minus_def pred_lemma)
+
+lemma sg_lemma: "rec_eval rec_sg [x] = (if x = 0 then 0 else 1)"
+by(auto simp: rec_sg_def minus_lemma rec_eval.simps constn.simps)
+
+lemma constn_lemma: "rec_eval (constn n) [x] = n"
+by(induct n, auto simp: rec_eval.simps constn.simps)
+
+lemma less_lemma: "rec_eval rec_less [x, y] = (if x < y then 1 else 0)"
+by(induct_tac y, auto simp: rec_eval.simps
rec_less_def minus_lemma sg_lemma)
-lemma not_lemma: "rec_exec rec_not [x] = (if x = 0 then 1 else 0)"
-by(induct_tac x, auto simp: rec_exec.simps rec_not_def
+lemma not_lemma: "rec_eval rec_not [x] = (if x = 0 then 1 else 0)"
+by(induct_tac x, auto simp: rec_eval.simps rec_not_def
constn_lemma minus_lemma)
-lemma eq_lemma: "rec_exec rec_eq [x, y] = (if x = y then 1 else 0)"
-by(induct_tac y, auto simp: rec_exec.simps rec_eq_def constn_lemma add_lemma minus_lemma)
-
-lemma conj_lemma: "rec_exec rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 else 1)"
-by(induct_tac y, auto simp: rec_exec.simps sg_lemma rec_conj_def mult_lemma)
-
-lemma disj_lemma: "rec_exec rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0 else 1)"
-by(induct_tac y, auto simp: rec_disj_def sg_lemma add_lemma rec_exec.simps)
+lemma eq_lemma: "rec_eval rec_eq [x, y] = (if x = y then 1 else 0)"
+by(induct_tac y, auto simp: rec_eval.simps rec_eq_def constn_lemma add_lemma minus_lemma)
+
+lemma conj_lemma: "rec_eval rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 else 1)"
+by(induct_tac y, auto simp: rec_eval.simps sg_lemma rec_conj_def mult_lemma)
+
+lemma disj_lemma: "rec_eval rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0 else 1)"
+by(induct_tac y, auto simp: rec_disj_def sg_lemma add_lemma rec_eval.simps)
declare mult_lemma[simp] add_lemma[simp] pred_lemma[simp]
minus_lemma[simp] sg_lemma[simp] constn_lemma[simp]
@@ -246,7 +246,7 @@
by auto
qed
-declare rec_exec.simps[simp del] get_fstn_args.simps[simp del]
+declare rec_eval.simps[simp del] get_fstn_args.simps[simp del]
arity.simps[simp del] Sigma.simps[simp del]
rec_sigma.simps[simp del]
@@ -254,20 +254,20 @@
by(simp add: arity.simps)
lemma rec_pr_0_simp_rewrite: "
- rec_exec (Pr n f g) (xs @ [0]) = rec_exec f xs"
- by(simp add: rec_exec.simps)
+ rec_eval (Pr n f g) (xs @ [0]) = rec_eval f xs"
+ by(simp add: rec_eval.simps)
lemma rec_pr_0_simp_rewrite_single_param: "
- rec_exec (Pr n f g) [0] = rec_exec f []"
- by(simp add: rec_exec.simps)
+ rec_eval (Pr n f g) [0] = rec_eval f []"
+ by(simp add: rec_eval.simps)
lemma rec_pr_Suc_simp_rewrite:
- "rec_exec (Pr n f g) (xs @ [Suc x]) = rec_exec g (xs @ [x] @ [rec_exec (Pr n f g) (xs @ [x])])"
-by(simp add: rec_exec.simps)
+ "rec_eval (Pr n f g) (xs @ [Suc x]) = rec_eval g (xs @ [x] @ [rec_eval (Pr n f g) (xs @ [x])])"
+by(simp add: rec_eval.simps)
lemma rec_pr_Suc_simp_rewrite_single_param:
- "rec_exec (Pr n f g) ([Suc x]) = rec_exec g ([x] @ [rec_exec (Pr n f g) ([x])])"
-by(simp add: rec_exec.simps)
+ "rec_eval (Pr n f g) ([Suc x]) = rec_eval g ([x] @ [rec_eval (Pr n f g) ([x])])"
+by(simp add: rec_eval.simps)
lemma Sigma_0_simp_rewrite_single_param:
"Sigma f [0] = f [0]"
@@ -289,13 +289,13 @@
by(simp add: nth_append)
lemma get_fstn_args_take: "\<lbrakk>length xs = m; n \<le> m\<rbrakk> \<Longrightarrow>
- map (\<lambda> f. rec_exec f xs) (get_fstn_args m n)= take n xs"
+ map (\<lambda> f. rec_eval f xs) (get_fstn_args m n)= take n xs"
proof(induct n)
case 0 thus "?case"
by(simp add: get_fstn_args.simps)
next
case (Suc n) thus "?case"
- by(simp add: get_fstn_args.simps rec_exec.simps
+ by(simp add: get_fstn_args.simps rec_eval.simps
take_Suc_conv_app_nth)
qed
@@ -307,11 +307,11 @@
lemma rec_sigma_Suc_simp_rewrite:
"primerec f (Suc (length xs))
- \<Longrightarrow> rec_exec (rec_sigma f) (xs @ [Suc x]) =
- rec_exec (rec_sigma f) (xs @ [x]) + rec_exec f (xs @ [Suc x])"
+ \<Longrightarrow> rec_eval (rec_sigma f) (xs @ [Suc x]) =
+ rec_eval (rec_sigma f) (xs @ [x]) + rec_eval f (xs @ [Suc x])"
apply(induct x)
apply(auto simp: rec_sigma.simps Let_def rec_pr_Suc_simp_rewrite
- rec_exec.simps get_fstn_args_take)
+ rec_eval.simps get_fstn_args_take)
done
text {*
@@ -319,9 +319,9 @@
*}
lemma sigma_lemma:
"primerec rg (Suc (length xs))
- \<Longrightarrow> rec_exec (rec_sigma rg) (xs @ [x]) = Sigma (rec_exec rg) (xs @ [x])"
+ \<Longrightarrow> rec_eval (rec_sigma rg) (xs @ [x]) = Sigma (rec_eval rg) (xs @ [x])"
apply(induct x)
-apply(auto simp: rec_exec.simps rec_sigma.simps Let_def
+apply(auto simp: rec_eval.simps rec_sigma.simps Let_def
get_fstn_args_take Sigma_0_simp_rewrite
Sigma_Suc_simp_rewrite)
done
@@ -366,11 +366,11 @@
lemma rec_accum_Suc_simp_rewrite:
"primerec f (Suc (length xs))
- \<Longrightarrow> rec_exec (rec_accum f) (xs @ [Suc x]) =
- rec_exec (rec_accum f) (xs @ [x]) * rec_exec f (xs @ [Suc x])"
+ \<Longrightarrow> rec_eval (rec_accum f) (xs @ [Suc x]) =
+ rec_eval (rec_accum f) (xs @ [x]) * rec_eval f (xs @ [Suc x])"
apply(induct x)
apply(auto simp: rec_sigma.simps Let_def rec_pr_Suc_simp_rewrite
- rec_exec.simps get_fstn_args_take)
+ rec_eval.simps get_fstn_args_take)
done
text {*
@@ -378,9 +378,9 @@
*}
lemma accum_lemma :
"primerec rg (Suc (length xs))
- \<Longrightarrow> rec_exec (rec_accum rg) (xs @ [x]) = Accum (rec_exec rg) (xs @ [x])"
+ \<Longrightarrow> rec_eval (rec_accum rg) (xs @ [x]) = Accum (rec_eval rg) (xs @ [x])"
apply(induct x)
-apply(auto simp: rec_exec.simps rec_sigma.simps Let_def
+apply(auto simp: rec_eval.simps rec_sigma.simps Let_def
get_fstn_args_take)
done
@@ -399,10 +399,10 @@
(get_fstn_args (vl - 1) (vl - 1) @ [rt])])"
lemma rec_accum_ex: "primerec rf (Suc (length xs)) \<Longrightarrow>
- (rec_exec (rec_accum rf) (xs @ [x]) = 0) =
- (\<exists> t \<le> x. rec_exec rf (xs @ [t]) = 0)"
+ (rec_eval (rec_accum rf) (xs @ [x]) = 0) =
+ (\<exists> t \<le> x. rec_eval rf (xs @ [t]) = 0)"
apply(induct x, simp_all add: rec_accum_Suc_simp_rewrite)
-apply(simp add: rec_exec.simps rec_accum.simps get_fstn_args_take,
+apply(simp add: rec_eval.simps rec_accum.simps get_fstn_args_take,
auto)
apply(rule_tac x = ta in exI, simp)
apply(case_tac "t = Suc x", simp_all)
@@ -415,16 +415,16 @@
lemma all_lemma:
"\<lbrakk>primerec rf (Suc (length xs));
primerec rt (length xs)\<rbrakk>
- \<Longrightarrow> rec_exec (rec_all rt rf) xs = (if (\<forall> x \<le> (rec_exec rt xs). 0 < rec_exec rf (xs @ [x])) then 1
+ \<Longrightarrow> rec_eval (rec_all rt rf) xs = (if (\<forall> x \<le> (rec_eval rt xs). 0 < rec_eval rf (xs @ [x])) then 1
else 0)"
apply(auto simp: rec_all.simps)
-apply(simp add: rec_exec.simps map_append get_fstn_args_take split: if_splits)
-apply(drule_tac x = "rec_exec rt xs" in rec_accum_ex)
-apply(case_tac "rec_exec (rec_accum rf) (xs @ [rec_exec rt xs]) = 0", simp_all)
+apply(simp add: rec_eval.simps map_append get_fstn_args_take split: if_splits)
+apply(drule_tac x = "rec_eval rt xs" in rec_accum_ex)
+apply(case_tac "rec_eval (rec_accum rf) (xs @ [rec_eval rt xs]) = 0", simp_all)
apply(erule_tac exE, erule_tac x = t in allE, simp)
-apply(simp add: rec_exec.simps map_append get_fstn_args_take)
-apply(drule_tac x = "rec_exec rt xs" in rec_accum_ex)
-apply(case_tac "rec_exec (rec_accum rf) (xs @ [rec_exec rt xs]) = 0", simp, simp)
+apply(simp add: rec_eval.simps map_append get_fstn_args_take)
+apply(drule_tac x = "rec_eval rt xs" in rec_accum_ex)
+apply(case_tac "rec_eval (rec_accum rf) (xs @ [rec_eval rt xs]) = 0", simp, simp)
apply(erule_tac x = x in allE, simp)
done
@@ -441,10 +441,10 @@
(get_fstn_args (vl - 1) (vl - 1) @ [rt])])"
lemma rec_sigma_ex: "primerec rf (Suc (length xs))
- \<Longrightarrow> (rec_exec (rec_sigma rf) (xs @ [x]) = 0) =
- (\<forall> t \<le> x. rec_exec rf (xs @ [t]) = 0)"
+ \<Longrightarrow> (rec_eval (rec_sigma rf) (xs @ [x]) = 0) =
+ (\<forall> t \<le> x. rec_eval rf (xs @ [t]) = 0)"
apply(induct x, simp_all add: rec_sigma_Suc_simp_rewrite)
-apply(simp add: rec_exec.simps rec_sigma.simps
+apply(simp add: rec_eval.simps rec_sigma.simps
get_fstn_args_take, auto)
apply(case_tac "t = Suc x", simp_all)
done
@@ -455,13 +455,13 @@
lemma ex_lemma:"
\<lbrakk>primerec rf (Suc (length xs));
primerec rt (length xs)\<rbrakk>
-\<Longrightarrow> (rec_exec (rec_ex rt rf) xs =
- (if (\<exists> x \<le> (rec_exec rt xs). 0 <rec_exec rf (xs @ [x])) then 1
+\<Longrightarrow> (rec_eval (rec_ex rt rf) xs =
+ (if (\<exists> x \<le> (rec_eval rt xs). 0 <rec_eval rf (xs @ [x])) then 1
else 0))"
-apply(auto simp: rec_ex.simps rec_exec.simps map_append get_fstn_args_take
+apply(auto simp: rec_ex.simps rec_eval.simps map_append get_fstn_args_take
split: if_splits)
-apply(drule_tac x = "rec_exec rt xs" in rec_sigma_ex, simp)
-apply(drule_tac x = "rec_exec rt xs" in rec_sigma_ex, simp)
+apply(drule_tac x = "rec_eval rt xs" in rec_sigma_ex, simp)
+apply(drule_tac x = "rec_eval rt xs" in rec_sigma_ex, simp)
done
text {*
@@ -523,7 +523,7 @@
by(insert Minr_range[of Rr xs w], auto)
text {*
- @{text "rec_Minr"} is the recursive function
+ @{text "rec_Minmr"} is the recursive function
used to implement @{text "Minr"}:
if @{text "Rr"} is implemented by a recursive function @{text "recf"},
then @{text "rec_Minr recf"} is the recursive function used to
@@ -637,11 +637,11 @@
apply(case_tac i, auto intro: prime_id)
done
-lemma Min_false1[simp]: "\<lbrakk>\<not> Min {uu. uu \<le> w \<and> 0 < rec_exec rf (xs @ [uu])} \<le> w;
- x \<le> w; 0 < rec_exec rf (xs @ [x])\<rbrakk>
+lemma Min_false1[simp]: "\<lbrakk>\<not> Min {uu. uu \<le> w \<and> 0 < rec_eval rf (xs @ [uu])} \<le> w;
+ x \<le> w; 0 < rec_eval rf (xs @ [x])\<rbrakk>
\<Longrightarrow> False"
-apply(subgoal_tac "finite {uu. uu \<le> w \<and> 0 < rec_exec rf (xs @ [uu])}")
-apply(subgoal_tac "{uu. uu \<le> w \<and> 0 < rec_exec rf (xs @ [uu])} \<noteq> {}")
+apply(subgoal_tac "finite {uu. uu \<le> w \<and> 0 < rec_eval rf (xs @ [uu])}")
+apply(subgoal_tac "{uu. uu \<le> w \<and> 0 < rec_eval rf (xs @ [uu])} \<noteq> {}")
apply(simp add: Min_le_iff, simp)
apply(rule_tac x = x in exI, simp)
apply(simp)
@@ -649,12 +649,12 @@
lemma sigma_minr_lemma:
assumes prrf: "primerec rf (Suc (length xs))"
- shows "UF.Sigma (rec_exec (rec_all (recf.id (Suc (length xs)) (length xs))
+ shows "UF.Sigma (rec_eval (rec_all (recf.id (Suc (length xs)) (length xs))
(Cn (Suc (Suc (length xs))) rec_not
[Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs)))
(length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])])))
(xs @ [w]) =
- Minr (\<lambda>args. 0 < rec_exec rf args) xs w"
+ Minr (\<lambda>args. 0 < rec_eval rf args) xs w"
proof(induct w)
let ?rt = "(recf.id (Suc (length xs)) ((length xs)))"
let ?rf = "(Cn (Suc (Suc (length xs)))
@@ -667,11 +667,11 @@
primerec ?rt (length (xs @ [0]))"
apply(auto simp: prrf nth_append)+
done
- show "Sigma (rec_exec (rec_all ?rt ?rf)) (xs @ [0])
- = Minr (\<lambda>args. 0 < rec_exec rf args) xs 0"
+ show "Sigma (rec_eval (rec_all ?rt ?rf)) (xs @ [0])
+ = Minr (\<lambda>args. 0 < rec_eval rf args) xs 0"
apply(simp add: Sigma.simps)
apply(simp only: prrf all_lemma,
- auto simp: rec_exec.simps get_fstn_args_take Minr.simps)
+ auto simp: rec_eval.simps get_fstn_args_take Minr.simps)
apply(rule_tac Min_eqI, auto)
done
next
@@ -684,17 +684,17 @@
(Suc ((length xs)))])])"
let ?rq = "(rec_all ?rt ?rf)"
assume ind:
- "Sigma (rec_exec (rec_all ?rt ?rf)) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w"
+ "Sigma (rec_eval (rec_all ?rt ?rf)) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_eval rf args) xs w"
have prrf: "primerec ?rf (Suc (length (xs @ [Suc w]))) \<and>
primerec ?rt (length (xs @ [Suc w]))"
apply(auto simp: prrf nth_append)+
done
- show "UF.Sigma (rec_exec (rec_all ?rt ?rf))
+ show "UF.Sigma (rec_eval (rec_all ?rt ?rf))
(xs @ [Suc w]) =
- Minr (\<lambda>args. 0 < rec_exec rf args) xs (Suc w)"
+ Minr (\<lambda>args. 0 < rec_eval rf args) xs (Suc w)"
apply(auto simp: Sigma_Suc_simp_rewrite ind Minr_Suc_simp)
apply(simp_all only: prrf all_lemma)
- apply(auto simp: rec_exec.simps get_fstn_args_take Let_def Minr.simps split: if_splits)
+ apply(auto simp: rec_eval.simps get_fstn_args_take Let_def Minr.simps split: if_splits)
apply(drule_tac Min_false1, simp, simp, simp)
apply(case_tac "x = Suc w", simp, simp)
apply(drule_tac Min_false1, simp, simp, simp)
@@ -707,7 +707,7 @@
*}
lemma Minr_lemma:
assumes h: "primerec rf (Suc (length xs))"
- shows "rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
+ shows "rec_eval (rec_Minr rf) (xs @ [w]) = Minr (\<lambda> args. (0 < rec_eval rf args)) xs w"
proof -
let ?rt = "(recf.id (Suc (length xs)) ((length xs)))"
let ?rf = "(Cn (Suc (Suc (length xs)))
@@ -722,8 +722,8 @@
done
moreover have "arity rf = Suc (length xs)"
using h by auto
- ultimately show "rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
- apply(simp add: rec_exec.simps rec_Minr.simps arity.simps Let_def
+ ultimately show "rec_eval (rec_Minr rf) (xs @ [w]) = Minr (\<lambda> args. (0 < rec_eval rf args)) xs w"
+ apply(simp add: rec_eval.simps rec_Minr.simps arity.simps Let_def
sigma_lemma all_lemma)
apply(rule_tac sigma_minr_lemma)
apply(simp add: h)
@@ -743,8 +743,8 @@
The correctness of @{text "rec_le"}.
*}
lemma le_lemma:
- "rec_exec rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
-by(auto simp: rec_le_def rec_exec.simps)
+ "rec_eval rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
+by(auto simp: rec_le_def rec_eval.simps)
text {*
Definition of @{text "Max[Rr]"} on page 77 of Boolos's book.
@@ -847,7 +847,7 @@
lemma Sigma_Max_lemma:
assumes prrf: "primerec rf (Suc (length xs))"
- shows "UF.Sigma (rec_exec (Cn (Suc (Suc (length xs))) rec_not
+ shows "UF.Sigma (rec_eval (Cn (Suc (Suc (length xs))) rec_not
[rec_all (recf.id (Suc (Suc (length xs))) (length xs))
(Cn (Suc (Suc (Suc (length xs)))) rec_disj
[Cn (Suc (Suc (Suc (length xs)))) rec_le
@@ -858,7 +858,7 @@
(get_fstn_args (Suc (Suc (Suc (length xs)))) (length xs) @
[recf.id (Suc (Suc (Suc (length xs)))) (Suc (Suc (length xs)))])]])]))
((xs @ [w]) @ [w]) =
- Maxr (\<lambda>args. 0 < rec_exec rf args) xs w"
+ Maxr (\<lambda>args. 0 < rec_eval rf args) xs w"
proof -
let ?rt = "(recf.id (Suc (Suc (length xs))) ((length xs)))"
let ?rf1 = "Cn (Suc (Suc (Suc (length xs))))
@@ -876,7 +876,7 @@
let ?notrq = "Cn (Suc (Suc (length xs))) rec_not [?rq]"
show "?thesis"
proof(auto simp: Maxr.simps)
- assume h: "\<forall>x\<le>w. rec_exec rf (xs @ [x]) = 0"
+ assume h: "\<forall>x\<le>w. rec_eval rf (xs @ [x]) = 0"
have "primerec ?rf (Suc (length (xs @ [w, i]))) \<and>
primerec ?rt (length (xs @ [w, i]))"
using prrf
@@ -884,54 +884,54 @@
apply(case_tac i, auto)
apply(case_tac ia, auto simp: h nth_append)
done
- hence "Sigma (rec_exec ?notrq) ((xs@[w])@[w]) = 0"
+ hence "Sigma (rec_eval ?notrq) ((xs@[w])@[w]) = 0"
apply(rule_tac Sigma_0)
- apply(auto simp: rec_exec.simps all_lemma
+ apply(auto simp: rec_eval.simps all_lemma
get_fstn_args_take nth_append h)
done
- thus "UF.Sigma (rec_exec ?notrq)
+ thus "UF.Sigma (rec_eval ?notrq)
(xs @ [w, w]) = 0"
by simp
next
fix x
- assume h: "x \<le> w" "0 < rec_exec rf (xs @ [x])"
- hence "\<exists> ma. Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])} = ma"
+ assume h: "x \<le> w" "0 < rec_eval rf (xs @ [x])"
+ hence "\<exists> ma. Max {y. y \<le> w \<and> 0 < rec_eval rf (xs @ [y])} = ma"
by auto
from this obtain ma where k1:
- "Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])} = ma" ..
- hence k2: "ma \<le> w \<and> 0 < rec_exec rf (xs @ [ma])"
+ "Max {y. y \<le> w \<and> 0 < rec_eval rf (xs @ [y])} = ma" ..
+ hence k2: "ma \<le> w \<and> 0 < rec_eval rf (xs @ [ma])"
using h
apply(subgoal_tac
- "Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])} \<in> {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])}")
+ "Max {y. y \<le> w \<and> 0 < rec_eval rf (xs @ [y])} \<in> {y. y \<le> w \<and> 0 < rec_eval rf (xs @ [y])}")
apply(erule_tac CollectE, simp)
apply(rule_tac Max_in, auto)
done
- hence k3: "\<forall> k < ma. (rec_exec ?notrq (xs @ [w, k]) = 1)"
+ hence k3: "\<forall> k < ma. (rec_eval ?notrq (xs @ [w, k]) = 1)"
apply(auto simp: nth_append)
apply(subgoal_tac "primerec ?rf (Suc (length (xs @ [w, k]))) \<and>
primerec ?rt (length (xs @ [w, k]))")
- apply(auto simp: rec_exec.simps all_lemma get_fstn_args_take nth_append)
+ apply(auto simp: rec_eval.simps all_lemma get_fstn_args_take nth_append)
using prrf
apply(case_tac i, auto)
apply(case_tac ia, auto simp: h nth_append)
done
- have k4: "\<forall> k \<ge> ma. (rec_exec ?notrq (xs @ [w, k]) = 0)"
+ have k4: "\<forall> k \<ge> ma. (rec_eval ?notrq (xs @ [w, k]) = 0)"
apply(auto)
apply(subgoal_tac "primerec ?rf (Suc (length (xs @ [w, k]))) \<and>
primerec ?rt (length (xs @ [w, k]))")
- apply(auto simp: rec_exec.simps all_lemma get_fstn_args_take nth_append)
- apply(subgoal_tac "x \<le> Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])}",
+ apply(auto simp: rec_eval.simps all_lemma get_fstn_args_take nth_append)
+ apply(subgoal_tac "x \<le> Max {y. y \<le> w \<and> 0 < rec_eval rf (xs @ [y])}",
simp add: k1)
apply(rule_tac Max_ge, auto)
using prrf
apply(case_tac i, auto)
apply(case_tac ia, auto simp: h nth_append)
done
- from k3 k4 k1 have "Sigma (rec_exec ?notrq) ((xs @ [w]) @ [w]) = ma"
+ from k3 k4 k1 have "Sigma (rec_eval ?notrq) ((xs @ [w]) @ [w]) = ma"
apply(rule_tac Sigma_max_point, simp, simp, simp add: k2)
done
- from k1 and this show "Sigma (rec_exec ?notrq) (xs @ [w, w]) =
- Max {y. y \<le> w \<and> 0 < rec_exec rf (xs @ [y])}"
+ from k1 and this show "Sigma (rec_eval ?notrq) (xs @ [w, w]) =
+ Max {y. y \<le> w \<and> 0 < rec_eval rf (xs @ [y])}"
by simp
qed
qed
@@ -941,13 +941,13 @@
*}
lemma Maxr_lemma:
assumes h: "primerec rf (Suc (length xs))"
- shows "rec_exec (rec_maxr rf) (xs @ [w]) =
- Maxr (\<lambda> args. 0 < rec_exec rf args) xs w"
+ shows "rec_eval (rec_maxr rf) (xs @ [w]) =
+ Maxr (\<lambda> args. 0 < rec_eval rf args) xs w"
proof -
from h have "arity rf = Suc (length xs)"
by auto
thus "?thesis"
- proof(simp add: rec_exec.simps rec_maxr.simps nth_append get_fstn_args_take)
+ proof(simp add: rec_eval.simps rec_maxr.simps nth_append get_fstn_args_take)
let ?rt = "(recf.id (Suc (Suc (length xs))) ((length xs)))"
let ?rf1 = "Cn (Suc (Suc (Suc (length xs))))
rec_le [recf.id (Suc (Suc (Suc (length xs))))
@@ -976,17 +976,17 @@
by(erule_tac primerec_all_iff, auto)
hence prnotrp: "primerec ?notrq (Suc (length ((xs @ [w]))))"
by(rule_tac prime_cn, auto)
- have g1: "rec_exec (rec_sigma ?notrq) ((xs @ [w]) @ [w])
- = Maxr (\<lambda>args. 0 < rec_exec rf args) xs w"
+ have g1: "rec_eval (rec_sigma ?notrq) ((xs @ [w]) @ [w])
+ = Maxr (\<lambda>args. 0 < rec_eval rf args) xs w"
using prnotrp
using sigma_lemma
apply(simp only: sigma_lemma)
apply(rule_tac Sigma_Max_lemma)
apply(simp add: h)
done
- thus "rec_exec (rec_sigma ?notrq)
+ thus "rec_eval (rec_sigma ?notrq)
(xs @ [w, w]) =
- Maxr (\<lambda>args. 0 < rec_exec rf args) xs w"
+ Maxr (\<lambda>args. 0 < rec_eval rf args) xs w"
apply(simp)
done
qed
@@ -1042,8 +1042,8 @@
The correctness of @{text "rec_noteq"}.
*}
lemma noteq_lemma:
- "rec_exec rec_noteq [x, y] = (if x \<noteq> y then 1 else 0)"
-by(simp add: rec_exec.simps rec_noteq_def)
+ "rec_eval rec_noteq [x, y] = (if x \<noteq> y then 1 else 0)"
+by(simp add: rec_eval.simps rec_noteq_def)
declare noteq_lemma[simp]
@@ -1079,8 +1079,8 @@
done
-lemma quo_lemma1: "rec_exec rec_quo [x, y] = quo [x, y]"
-proof(simp add: rec_exec.simps rec_quo_def)
+lemma quo_lemma1: "rec_eval rec_quo [x, y] = quo [x, y]"
+proof(simp add: rec_eval.simps rec_quo_def)
let ?rR = "(Cn (Suc (Suc (Suc 0))) rec_conj
[Cn (Suc (Suc (Suc 0))) rec_le
[Cn (Suc (Suc (Suc 0))) rec_mult
@@ -1091,7 +1091,7 @@
[recf.id (Suc (Suc (Suc 0)))
(Suc (0)), Cn (Suc (Suc (Suc 0))) (constn 0)
[recf.id (Suc (Suc (Suc 0))) (0)]]])"
- have "rec_exec (rec_maxr ?rR) ([x, y]@ [ x]) = Maxr (\<lambda> args. 0 < rec_exec ?rR args) [x, y] x"
+ have "rec_eval (rec_maxr ?rR) ([x, y]@ [ x]) = Maxr (\<lambda> args. 0 < rec_eval ?rR args) [x, y] x"
proof(rule_tac Maxr_lemma, simp)
show "primerec ?rR (Suc (Suc (Suc 0)))"
apply(auto)
@@ -1100,24 +1100,24 @@
apply(case_tac i, auto)
done
qed
- hence g1: "rec_exec (rec_maxr ?rR) ([x, y, x]) =
- Maxr (\<lambda> args. if rec_exec ?rR args = 0 then False
+ hence g1: "rec_eval (rec_maxr ?rR) ([x, y, x]) =
+ Maxr (\<lambda> args. if rec_eval ?rR args = 0 then False
else True) [x, y] x"
by simp
- have g2: "Maxr (\<lambda> args. if rec_exec ?rR args = 0 then False
+ have g2: "Maxr (\<lambda> args. if rec_eval ?rR args = 0 then False
else True) [x, y] x = quo [x, y]"
- apply(simp add: rec_exec.simps)
+ apply(simp add: rec_eval.simps)
apply(simp add: Maxr.simps quo.simps, auto)
done
from g1 and g2 show
- "rec_exec (rec_maxr ?rR) ([x, y, x]) = quo [x, y]"
+ "rec_eval (rec_maxr ?rR) ([x, y, x]) = quo [x, y]"
by simp
qed
text {*
The correctness of @{text "quo"}.
*}
-lemma quo_lemma2: "rec_exec rec_quo [x, y] = x div y"
+lemma quo_lemma2: "rec_eval rec_quo [x, y] = x div y"
using quo_lemma1[of x y] quo_div[of x y]
by simp
@@ -1134,8 +1134,8 @@
text {*
The correctness of @{text "rec_mod"}:
*}
-lemma mod_lemma: "rec_exec rec_mod [x, y] = (x mod y)"
-proof(simp add: rec_exec.simps rec_mod_def quo_lemma2)
+lemma mod_lemma: "rec_eval rec_mod [x, y] = (x mod y)"
+proof(simp add: rec_eval.simps rec_mod_def quo_lemma2)
fix x y
show "x - x div y * y = x mod (y::nat)"
using mod_div_equality2[of y x]
@@ -1178,56 +1178,56 @@
declare Embranch.simps[simp del] rec_embranch.simps[simp del]
lemma embranch_all0:
- "\<lbrakk>\<forall> j < length rcs. rec_exec (rcs ! j) xs = 0;
+ "\<lbrakk>\<forall> j < length rcs. rec_eval (rcs ! j) xs = 0;
length rgs = length rcs;
rcs \<noteq> [];
list_all (\<lambda> rf. primerec rf (length xs)) (rgs @ rcs)\<rbrakk> \<Longrightarrow>
- rec_exec (rec_embranch (zip rgs rcs)) xs = 0"
+ rec_eval (rec_embranch (zip rgs rcs)) xs = 0"
proof(induct rcs arbitrary: rgs, simp, case_tac rgs, simp)
fix a rcs rgs aa list
assume ind:
- "\<And>rgs. \<lbrakk>\<forall>j<length rcs. rec_exec (rcs ! j) xs = 0;
+ "\<And>rgs. \<lbrakk>\<forall>j<length rcs. rec_eval (rcs ! j) xs = 0;
length rgs = length rcs; rcs \<noteq> [];
list_all (\<lambda>rf. primerec rf (length xs)) (rgs @ rcs)\<rbrakk> \<Longrightarrow>
- rec_exec (rec_embranch (zip rgs rcs)) xs = 0"
- and h: "\<forall>j<length (a # rcs). rec_exec ((a # rcs) ! j) xs = 0"
+ rec_eval (rec_embranch (zip rgs rcs)) xs = 0"
+ and h: "\<forall>j<length (a # rcs). rec_eval ((a # rcs) ! j) xs = 0"
"length rgs = length (a # rcs)"
"a # rcs \<noteq> []"
"list_all (\<lambda>rf. primerec rf (length xs)) (rgs @ a # rcs)"
"rgs = aa # list"
- have g: "rcs \<noteq> [] \<Longrightarrow> rec_exec (rec_embranch (zip list rcs)) xs = 0"
+ have g: "rcs \<noteq> [] \<Longrightarrow> rec_eval (rec_embranch (zip list rcs)) xs = 0"
using h
by(rule_tac ind, auto)
- show "rec_exec (rec_embranch (zip rgs (a # rcs))) xs = 0"
+ show "rec_eval (rec_embranch (zip rgs (a # rcs))) xs = 0"
proof(case_tac "rcs = []", simp)
- show "rec_exec (rec_embranch (zip rgs [a])) xs = 0"
+ show "rec_eval (rec_embranch (zip rgs [a])) xs = 0"
using h
- apply(simp add: rec_embranch.simps rec_exec.simps)
+ apply(simp add: rec_embranch.simps rec_eval.simps)
apply(erule_tac x = 0 in allE, simp)
done
next
assume "rcs \<noteq> []"
- hence "rec_exec (rec_embranch (zip list rcs)) xs = 0"
+ hence "rec_eval (rec_embranch (zip list rcs)) xs = 0"
using g by simp
- thus "rec_exec (rec_embranch (zip rgs (a # rcs))) xs = 0"
+ thus "rec_eval (rec_embranch (zip rgs (a # rcs))) xs = 0"
using h
- apply(simp add: rec_embranch.simps rec_exec.simps)
+ apply(simp add: rec_embranch.simps rec_eval.simps)
apply(case_tac rcs,
- auto simp: rec_exec.simps rec_embranch.simps)
+ auto simp: rec_eval.simps rec_embranch.simps)
apply(case_tac list,
- auto simp: rec_exec.simps rec_embranch.simps)
+ auto simp: rec_eval.simps rec_embranch.simps)
done
qed
qed
-lemma embranch_exec_0: "\<lbrakk>rec_exec aa xs = 0; zip rgs list \<noteq> [];
+lemma embranch_exec_0: "\<lbrakk>rec_eval aa xs = 0; zip rgs list \<noteq> [];
list_all (\<lambda> rf. primerec rf (length xs)) ([a, aa] @ rgs @ list)\<rbrakk>
- \<Longrightarrow> rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs
- = rec_exec (rec_embranch (zip rgs list)) xs"
-apply(simp add: rec_exec.simps rec_embranch.simps)
+ \<Longrightarrow> rec_eval (rec_embranch ((a, aa) # zip rgs list)) xs
+ = rec_eval (rec_embranch (zip rgs list)) xs"
+apply(simp add: rec_eval.simps rec_embranch.simps)
apply(case_tac "zip rgs list", simp, case_tac ab,
- simp add: rec_embranch.simps rec_exec.simps)
+ simp add: rec_embranch.simps rec_eval.simps)
apply(subgoal_tac "arity a = length xs", auto)
apply(subgoal_tac "arity aaa = length xs", auto)
apply(case_tac rgs, simp, case_tac list, simp, simp)
@@ -1244,18 +1244,18 @@
lemma Embranch_0:
"\<lbrakk>length rgs = k; length rcs = k; k > 0;
- \<forall> j < k. rec_exec (rcs ! j) xs = 0\<rbrakk> \<Longrightarrow>
- Embranch (zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) rcs)) xs = 0"
+ \<forall> j < k. rec_eval (rcs ! j) xs = 0\<rbrakk> \<Longrightarrow>
+ Embranch (zip (map rec_eval rgs) (map (\<lambda>r args. 0 < rec_eval r args) rcs)) xs = 0"
proof(induct rgs arbitrary: rcs k, simp, simp)
fix a rgs rcs k
assume ind:
- "\<And>rcs k. \<lbrakk>length rgs = k; length rcs = k; 0 < k; \<forall>j<k. rec_exec (rcs ! j) xs = 0\<rbrakk>
- \<Longrightarrow> Embranch (zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) rcs)) xs = 0"
+ "\<And>rcs k. \<lbrakk>length rgs = k; length rcs = k; 0 < k; \<forall>j<k. rec_eval (rcs ! j) xs = 0\<rbrakk>
+ \<Longrightarrow> Embranch (zip (map rec_eval rgs) (map (\<lambda>r args. 0 < rec_eval r args) rcs)) xs = 0"
and h: "Suc (length rgs) = k" "length rcs = k"
- "\<forall>j<k. rec_exec (rcs ! j) xs = 0"
+ "\<forall>j<k. rec_eval (rcs ! j) xs = 0"
from h show
- "Embranch (zip (rec_exec a # map rec_exec rgs)
- (map (\<lambda>r args. 0 < rec_exec r args) rcs)) xs = 0"
+ "Embranch (zip (rec_eval a # map rec_eval rgs)
+ (map (\<lambda>r args. 0 < rec_eval r args) rcs)) xs = 0"
apply(case_tac rcs, simp, case_tac "rgs = []", simp)
apply(simp add: Embranch.simps)
apply(erule_tac x = 0 in allE, simp)
@@ -1273,51 +1273,51 @@
assumes branch_num:
"length rgs = n" "length rcs = n" "n > 0"
and partition:
- "(\<exists> i < n. (rec_exec (rcs ! i) xs = 1 \<and> (\<forall> j < n. j \<noteq> i \<longrightarrow>
- rec_exec (rcs ! j) xs = 0)))"
+ "(\<exists> i < n. (rec_eval (rcs ! i) xs = 1 \<and> (\<forall> j < n. j \<noteq> i \<longrightarrow>
+ rec_eval (rcs ! j) xs = 0)))"
and prime_all: "list_all (\<lambda> rf. primerec rf (length xs)) (rgs @ rcs)"
- shows "rec_exec (rec_embranch (zip rgs rcs)) xs =
- Embranch (zip (map rec_exec rgs)
- (map (\<lambda> r args. 0 < rec_exec r args) rcs)) xs"
+ 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"
using branch_num partition prime_all
proof(induct rgs arbitrary: rcs n, simp)
fix a rgs rcs n
assume ind:
"\<And>rcs n. \<lbrakk>length rgs = n; length rcs = n; 0 < n;
- \<exists>i<n. rec_exec (rcs ! i) xs = 1 \<and> (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_exec (rcs ! j) xs = 0);
+ \<exists>i<n. rec_eval (rcs ! i) xs = 1 \<and> (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_eval (rcs ! j) xs = 0);
list_all (\<lambda>rf. primerec rf (length xs)) (rgs @ rcs)\<rbrakk>
- \<Longrightarrow> rec_exec (rec_embranch (zip rgs rcs)) xs =
- Embranch (zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) rcs)) xs"
+ \<Longrightarrow> 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"
and h: "length (a # rgs) = n" "length (rcs::recf list) = n" "0 < n"
- " \<exists>i<n. rec_exec (rcs ! i) xs = 1 \<and>
- (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_exec (rcs ! j) xs = 0)"
+ " \<exists>i<n. rec_eval (rcs ! i) xs = 1 \<and>
+ (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_eval (rcs ! j) xs = 0)"
"list_all (\<lambda>rf. primerec rf (length xs)) ((a # rgs) @ rcs)"
- from h show "rec_exec (rec_embranch (zip (a # rgs) rcs)) xs =
- Embranch (zip (map rec_exec (a # rgs)) (map (\<lambda>r args.
- 0 < rec_exec r args) rcs)) xs"
+ from h show "rec_eval (rec_embranch (zip (a # rgs) rcs)) xs =
+ Embranch (zip (map rec_eval (a # rgs)) (map (\<lambda>r args.
+ 0 < rec_eval r args) rcs)) xs"
apply(case_tac rcs, simp, simp)
- apply(case_tac "rec_exec aa xs = 0")
+ apply(case_tac "rec_eval aa xs = 0")
apply(case_tac [!] "zip rgs list = []", simp)
- apply(subgoal_tac "rgs = [] \<and> list = []", simp add: Embranch.simps rec_exec.simps rec_embranch.simps)
+ apply(subgoal_tac "rgs = [] \<and> list = []", simp add: Embranch.simps rec_eval.simps rec_embranch.simps)
apply(rule_tac zip_null_iff, simp, simp, simp)
proof -
fix aa list
assume g:
"Suc (length rgs) = n" "Suc (length list) = n"
- "\<exists>i<n. rec_exec ((aa # list) ! i) xs = Suc 0 \<and>
- (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_exec ((aa # list) ! j) xs = 0)"
+ "\<exists>i<n. rec_eval ((aa # list) ! i) xs = Suc 0 \<and>
+ (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_eval ((aa # list) ! j) xs = 0)"
"primerec a (length xs) \<and>
list_all (\<lambda>rf. primerec rf (length xs)) rgs \<and>
primerec aa (length xs) \<and>
list_all (\<lambda>rf. primerec rf (length xs)) list"
- "rec_exec aa xs = 0" "rcs = aa # list" "zip rgs list \<noteq> []"
- have "rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs
- = rec_exec (rec_embranch (zip rgs list)) xs"
+ "rec_eval aa xs = 0" "rcs = aa # list" "zip rgs list \<noteq> []"
+ have "rec_eval (rec_embranch ((a, aa) # zip rgs list)) xs
+ = rec_eval (rec_embranch (zip rgs list)) xs"
apply(rule embranch_exec_0, simp_all add: g)
done
- from g and this show "rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs =
- Embranch ((rec_exec a, \<lambda>args. 0 < rec_exec aa args) #
- zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) list)) xs"
+ from g and this show "rec_eval (rec_embranch ((a, aa) # zip rgs list)) xs =
+ Embranch ((rec_eval a, \<lambda>args. 0 < rec_eval aa args) #
+ zip (map rec_eval rgs) (map (\<lambda>r args. 0 < rec_eval r args) list)) xs"
apply(simp add: Embranch.simps)
apply(rule_tac n = "n - Suc 0" in ind)
apply(case_tac n, simp, simp)
@@ -1331,32 +1331,32 @@
next
fix aa list
assume g: "Suc (length rgs) = n" "Suc (length list) = n"
- "\<exists>i<n. rec_exec ((aa # list) ! i) xs = Suc 0 \<and>
- (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_exec ((aa # list) ! j) xs = 0)"
+ "\<exists>i<n. rec_eval ((aa # list) ! i) xs = Suc 0 \<and>
+ (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_eval ((aa # list) ! j) xs = 0)"
"primerec a (length xs) \<and> list_all (\<lambda>rf. primerec rf (length xs)) rgs \<and>
primerec aa (length xs) \<and> list_all (\<lambda>rf. primerec rf (length xs)) list"
- "rcs = aa # list" "rec_exec aa xs \<noteq> 0" "zip rgs list = []"
- thus "rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs =
- Embranch ((rec_exec a, \<lambda>args. 0 < rec_exec aa args) #
- zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) list)) xs"
+ "rcs = aa # list" "rec_eval aa xs \<noteq> 0" "zip rgs list = []"
+ thus "rec_eval (rec_embranch ((a, aa) # zip rgs list)) xs =
+ Embranch ((rec_eval a, \<lambda>args. 0 < rec_eval aa args) #
+ zip (map rec_eval rgs) (map (\<lambda>r args. 0 < rec_eval r args) list)) xs"
apply(subgoal_tac "rgs = [] \<and> list = []", simp)
prefer 2
apply(rule_tac zip_null_iff, simp, simp, simp)
- apply(simp add: rec_exec.simps rec_embranch.simps Embranch.simps, auto)
+ apply(simp add: rec_eval.simps rec_embranch.simps Embranch.simps, auto)
done
next
fix aa list
assume g: "Suc (length rgs) = n" "Suc (length list) = n"
- "\<exists>i<n. rec_exec ((aa # list) ! i) xs = Suc 0 \<and>
- (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_exec ((aa # list) ! j) xs = 0)"
+ "\<exists>i<n. rec_eval ((aa # list) ! i) xs = Suc 0 \<and>
+ (\<forall>j<n. j \<noteq> i \<longrightarrow> rec_eval ((aa # list) ! j) xs = 0)"
"primerec a (length xs) \<and> list_all (\<lambda>rf. primerec rf (length xs)) rgs
\<and> primerec aa (length xs) \<and> list_all (\<lambda>rf. primerec rf (length xs)) list"
- "rcs = aa # list" "rec_exec aa xs \<noteq> 0" "zip rgs list \<noteq> []"
- have "rec_exec aa xs = Suc 0"
+ "rcs = aa # list" "rec_eval aa xs \<noteq> 0" "zip rgs list \<noteq> []"
+ have "rec_eval aa xs = Suc 0"
using g
- apply(case_tac "rec_exec aa xs", simp, auto)
+ apply(case_tac "rec_eval aa xs", simp, auto)
done
- moreover have "rec_exec (rec_embranch' (zip rgs list) (length xs)) xs = 0"
+ moreover have "rec_eval (rec_embranch' (zip rgs list) (length xs)) xs = 0"
proof -
have "rec_embranch' (zip rgs list) (length xs) = rec_embranch (zip rgs list)"
using g
@@ -1365,9 +1365,9 @@
apply(subgoal_tac "arity aaa = length xs", simp, auto)
apply(case_tac rgs, simp, simp, case_tac list, simp, simp)
done
- moreover have "rec_exec (rec_embranch (zip rgs list)) xs = 0"
+ moreover have "rec_eval (rec_embranch (zip rgs list)) xs = 0"
proof(rule embranch_all0)
- show " \<forall>j<length list. rec_exec (list ! j) xs = 0"
+ show " \<forall>j<length list. rec_eval (list ! j) xs = 0"
using g
apply(auto)
apply(case_tac i, simp)
@@ -1391,12 +1391,12 @@
apply auto
done
qed
- ultimately show "rec_exec (rec_embranch' (zip rgs list) (length xs)) xs = 0"
+ ultimately show "rec_eval (rec_embranch' (zip rgs list) (length xs)) xs = 0"
by simp
qed
moreover have
- "Embranch (zip (map rec_exec rgs)
- (map (\<lambda>r args. 0 < rec_exec r args) list)) xs = 0"
+ "Embranch (zip (map rec_eval rgs)
+ (map (\<lambda>r args. 0 < rec_eval r args) list)) xs = 0"
using g
apply(rule_tac k = "length rgs" in Embranch_0)
apply(simp, case_tac n, simp, simp)
@@ -1411,10 +1411,10 @@
using g
apply(auto)
done
- ultimately show "rec_exec (rec_embranch ((a, aa) # zip rgs list)) xs =
- Embranch ((rec_exec a, \<lambda>args. 0 < rec_exec aa args) #
- zip (map rec_exec rgs) (map (\<lambda>r args. 0 < rec_exec r args) list)) xs"
- apply(simp add: rec_exec.simps rec_embranch.simps Embranch.simps)
+ ultimately show "rec_eval (rec_embranch ((a, aa) # zip rgs list)) xs =
+ Embranch ((rec_eval a, \<lambda>args. 0 < rec_eval aa args) #
+ zip (map rec_eval rgs) (map (\<lambda>r args. 0 < rec_eval r args) list)) xs"
+ apply(simp add: rec_eval.simps rec_embranch.simps Embranch.simps)
done
qed
qed
@@ -1444,10 +1444,10 @@
declare numeral_2_eq_2[simp del] numeral_3_eq_3[simp del]
lemma exec_tmp:
- "rec_exec (rec_all (Cn 2 rec_minus [recf.id 2 0, Cn 2 (constn (Suc 0)) [recf.id 2 0]])
+ "rec_eval (rec_all (Cn 2 rec_minus [recf.id 2 0, Cn 2 (constn (Suc 0)) [recf.id 2 0]])
(Cn 3 rec_noteq [Cn 3 rec_mult [recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 0])) [x, k] =
- ((if (\<forall>w\<le>rec_exec (Cn 2 rec_minus [recf.id 2 0, Cn 2 (constn (Suc 0)) [recf.id 2 0]]) ([x, k]).
- 0 < rec_exec (Cn 3 rec_noteq [Cn 3 rec_mult [recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 0])
+ ((if (\<forall>w\<le>rec_eval (Cn 2 rec_minus [recf.id 2 0, Cn 2 (constn (Suc 0)) [recf.id 2 0]]) ([x, k]).
+ 0 < rec_eval (Cn 3 rec_noteq [Cn 3 rec_mult [recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 0])
([x, k] @ [w])) then 1 else 0))"
apply(rule_tac all_lemma)
apply(auto)
@@ -1458,8 +1458,8 @@
text {*
The correctness of @{text "Prime"}.
*}
-lemma prime_lemma: "rec_exec rec_prime [x] = (if prime x then 1 else 0)"
-proof(simp add: rec_exec.simps rec_prime_def)
+lemma prime_lemma: "rec_eval rec_prime [x] = (if prime x then 1 else 0)"
+proof(simp add: rec_eval.simps rec_prime_def)
let ?rt1 = "(Cn 2 rec_minus [recf.id 2 0,
Cn 2 (constn (Suc 0)) [recf.id 2 0]])"
let ?rf1 = "(Cn 3 rec_noteq [Cn 3 rec_mult
@@ -1467,8 +1467,8 @@
let ?rt2 = "(Cn (Suc 0) rec_minus
[recf.id (Suc 0) 0, constn (Suc 0)])"
let ?rf2 = "rec_all ?rt1 ?rf1"
- have h1: "rec_exec (rec_all ?rt2 ?rf2) ([x]) =
- (if (\<forall>k\<le>rec_exec ?rt2 ([x]). 0 < rec_exec ?rf2 ([x] @ [k])) then 1 else 0)"
+ have h1: "rec_eval (rec_all ?rt2 ?rf2) ([x]) =
+ (if (\<forall>k\<le>rec_eval ?rt2 ([x]). 0 < rec_eval ?rf2 ([x] @ [k])) then 1 else 0)"
proof(rule_tac all_lemma, simp_all)
show "primerec ?rf2 (Suc (Suc 0))"
apply(rule_tac primerec_all_iff)
@@ -1484,18 +1484,18 @@
done
qed
from h1 show
- "(Suc 0 < x \<longrightarrow> (rec_exec (rec_all ?rt2 ?rf2) [x] = 0 \<longrightarrow>
+ "(Suc 0 < x \<longrightarrow> (rec_eval (rec_all ?rt2 ?rf2) [x] = 0 \<longrightarrow>
\<not> prime x) \<and>
- (0 < rec_exec (rec_all ?rt2 ?rf2) [x] \<longrightarrow> prime x)) \<and>
- (\<not> Suc 0 < x \<longrightarrow> \<not> prime x \<and> (rec_exec (rec_all ?rt2 ?rf2) [x] = 0
+ (0 < rec_eval (rec_all ?rt2 ?rf2) [x] \<longrightarrow> prime x)) \<and>
+ (\<not> Suc 0 < x \<longrightarrow> \<not> prime x \<and> (rec_eval (rec_all ?rt2 ?rf2) [x] = 0
\<longrightarrow> \<not> prime x))"
- apply(auto simp:rec_exec.simps)
- apply(simp add: exec_tmp rec_exec.simps)
+ apply(auto simp:rec_eval.simps)
+ apply(simp add: exec_tmp rec_eval.simps)
proof -
assume "\<forall>k\<le>x - Suc 0. (0::nat) < (if \<forall>w\<le>x - Suc 0.
0 < (if k * w \<noteq> x then 1 else (0 :: nat)) then 1 else 0)" "Suc 0 < x"
thus "prime x"
- apply(simp add: rec_exec.simps split: if_splits)
+ apply(simp add: rec_eval.simps split: if_splits)
apply(simp add: prime_nat_def dvd_def, auto)
apply(erule_tac x = m in allE, auto)
apply(case_tac m, simp, case_tac nat, simp, simp)
@@ -1507,16 +1507,16 @@
by (simp add: prime_nat_def)
next
fix k
- assume "rec_exec (rec_all ?rt1 ?rf1)
+ assume "rec_eval (rec_all ?rt1 ?rf1)
[x, k] = 0" "k \<le> x - Suc 0" "prime x"
thus "False"
- by (auto simp add: exec_tmp rec_exec.simps prime_nat_def dvd_def split: if_splits)
+ by (auto simp add: exec_tmp rec_eval.simps prime_nat_def dvd_def split: if_splits)
next
fix k
- assume "rec_exec (rec_all ?rt1 ?rf1)
+ assume "rec_eval (rec_all ?rt1 ?rf1)
[x, k] = 0" "k \<le> x - Suc 0" "prime x"
thus "False"
- by(auto simp add: exec_tmp rec_exec.simps prime_nat_def dvd_def split: if_splits)
+ by(auto simp add: exec_tmp rec_eval.simps prime_nat_def dvd_def split: if_splits)
qed
qed
@@ -1539,26 +1539,26 @@
"fac 0 = 1" |
"fac (Suc x) = (Suc x) * fac x"
-lemma [simp]: "rec_exec rec_dummyfac [0, 0] = Suc 0"
-by(simp add: rec_dummyfac_def rec_exec.simps)
+lemma [simp]: "rec_eval rec_dummyfac [0, 0] = Suc 0"
+by(simp add: rec_dummyfac_def rec_eval.simps)
lemma rec_cn_simp:
- "rec_exec (Cn n f gs) xs = (let rgs = map (\<lambda> g. rec_exec g xs) gs in rec_exec f rgs)"
-by(simp add: rec_exec.simps)
-
-lemma rec_id_simp: "rec_exec (id m n) xs = xs ! n"
- by(simp add: rec_exec.simps)
-
-lemma fac_dummy: "rec_exec rec_dummyfac [x, y] = y !"
+ "rec_eval (Cn n f gs) xs = (let rgs = map (\<lambda> g. rec_eval g xs) gs in rec_eval f rgs)"
+by(simp add: rec_eval.simps)
+
+lemma rec_id_simp: "rec_eval (id m n) xs = xs ! n"
+ by(simp add: rec_eval.simps)
+
+lemma fac_dummy: "rec_eval rec_dummyfac [x, y] = y !"
apply(induct y)
-apply(auto simp: rec_dummyfac_def rec_exec.simps)
+apply(auto simp: rec_dummyfac_def rec_eval.simps)
done
text {*
The correctness of @{text "rec_fac"}.
*}
-lemma fac_lemma: "rec_exec rec_fac [x] = x!"
-apply(simp add: rec_fac_def rec_exec.simps fac_dummy)
+lemma fac_lemma: "rec_eval rec_fac [x] = x!"
+apply(simp add: rec_fac_def rec_eval.simps fac_dummy)
done
declare fac.simps[simp del]
@@ -1686,25 +1686,25 @@
text {*
The correctness of @{text "rec_np"}.
*}
-lemma np_lemma: "rec_exec rec_np [x] = Np x"
-proof(auto simp: rec_np_def rec_exec.simps Let_def fac_lemma)
+lemma np_lemma: "rec_eval rec_np [x] = Np x"
+proof(auto simp: rec_np_def rec_eval.simps Let_def fac_lemma)
let ?rr = "(Cn 2 rec_conj [Cn 2 rec_less [recf.id 2 0,
recf.id 2 (Suc 0)], Cn 2 rec_prime [recf.id 2 (Suc 0)]])"
let ?R = "\<lambda> zs. zs ! 0 < zs ! 1 \<and> prime (zs ! 1)"
- have g1: "rec_exec (rec_Minr ?rr) ([x] @ [Suc (x!)]) =
- Minr (\<lambda> args. 0 < rec_exec ?rr args) [x] (Suc (x!))"
- by(rule_tac Minr_lemma, auto simp: rec_exec.simps
+ have g1: "rec_eval (rec_Minr ?rr) ([x] @ [Suc (x!)]) =
+ Minr (\<lambda> args. 0 < rec_eval ?rr args) [x] (Suc (x!))"
+ by(rule_tac Minr_lemma, auto simp: rec_eval.simps
prime_lemma, auto simp: numeral_2_eq_2 numeral_3_eq_3)
- have g2: "Minr (\<lambda> args. 0 < rec_exec ?rr args) [x] (Suc (x!)) = Np x"
+ have g2: "Minr (\<lambda> args. 0 < rec_eval ?rr args) [x] (Suc (x!)) = Np x"
using prime_ex[of x]
- apply(auto simp: Minr.simps Np.simps rec_exec.simps)
+ apply(auto simp: Minr.simps Np.simps rec_eval.simps)
apply(erule_tac x = p in allE, simp add: prime_lemma)
apply(simp add: prime_lemma split: if_splits)
apply(subgoal_tac
"{uu. (prime uu \<longrightarrow> (x < uu \<longrightarrow> uu \<le> Suc (x!)) \<and> x < uu) \<and> prime uu}
= {y. y \<le> Suc (x!) \<and> x < y \<and> prime y}", auto)
done
- from g1 and g2 show "rec_exec (rec_Minr ?rr) ([x, Suc (x!)]) = Np x"
+ from g1 and g2 show "rec_eval (rec_Minr ?rr) ([x, Suc (x!)]) = Np x"
by simp
qed
@@ -1719,8 +1719,8 @@
text {*
The correctness of @{text "rec_power"}.
*}
-lemma power_lemma: "rec_exec rec_power [x, y] = x^y"
- by(induct y, auto simp: rec_exec.simps rec_power_def)
+lemma power_lemma: "rec_eval rec_power [x, y] = x^y"
+ by(induct y, auto simp: rec_eval.simps rec_power_def)
text{*
@{text "Pi k"} returns the @{text "k"}-th prime number.
@@ -1742,15 +1742,15 @@
where
"rec_pi = Cn 1 rec_dummy_pi [id 1 0, id 1 0]"
-lemma pi_dummy_lemma: "rec_exec rec_dummy_pi [x, y] = Pi y"
+lemma pi_dummy_lemma: "rec_eval rec_dummy_pi [x, y] = Pi y"
apply(induct y)
-by(auto simp: rec_exec.simps rec_dummy_pi_def Pi.simps np_lemma)
+by(auto simp: rec_eval.simps rec_dummy_pi_def Pi.simps np_lemma)
text {*
The correctness of @{text "rec_pi"}.
*}
-lemma pi_lemma: "rec_exec rec_pi [x] = Pi x"
-apply(simp add: rec_pi_def rec_exec.simps pi_dummy_lemma)
+lemma pi_lemma: "rec_eval rec_pi [x] = Pi x"
+apply(simp add: rec_pi_def rec_eval.simps pi_dummy_lemma)
done
fun loR :: "nat list \<Rightarrow> bool"
@@ -1833,23 +1833,23 @@
lemma rec_lo_Maxr_lor:
"\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow>
- rec_exec rec_lo [x, y] = Maxr loR [x, y] x"
-proof(auto simp: rec_exec.simps rec_lo_def Let_def
+ rec_eval rec_lo [x, y] = Maxr loR [x, y] x"
+proof(auto simp: rec_eval.simps rec_lo_def Let_def
numeral_2_eq_2 numeral_3_eq_3)
let ?rR = "(Cn (Suc (Suc (Suc 0))) rec_eq
[Cn (Suc (Suc (Suc 0))) rec_mod [recf.id (Suc (Suc (Suc 0))) 0,
Cn (Suc (Suc (Suc 0))) rec_power [recf.id (Suc (Suc (Suc 0)))
(Suc 0), recf.id (Suc (Suc (Suc 0))) (Suc (Suc 0))]],
Cn (Suc (Suc (Suc 0))) (constn 0) [recf.id (Suc (Suc (Suc 0))) (Suc 0)]])"
- have h: "rec_exec (rec_maxr ?rR) ([x, y] @ [x]) =
- Maxr (\<lambda> args. 0 < rec_exec ?rR args) [x, y] x"
- by(rule_tac Maxr_lemma, auto simp: rec_exec.simps
+ have h: "rec_eval (rec_maxr ?rR) ([x, y] @ [x]) =
+ Maxr (\<lambda> args. 0 < rec_eval ?rR args) [x, y] x"
+ by(rule_tac Maxr_lemma, auto simp: rec_eval.simps
mod_lemma power_lemma, auto simp: numeral_2_eq_2 numeral_3_eq_3)
- have "Maxr loR [x, y] x = Maxr (\<lambda> args. 0 < rec_exec ?rR args) [x, y] x"
- apply(simp add: rec_exec.simps mod_lemma power_lemma)
+ have "Maxr loR [x, y] x = Maxr (\<lambda> args. 0 < rec_eval ?rR args) [x, y] x"
+ apply(simp add: rec_eval.simps mod_lemma power_lemma)
apply(simp add: Maxr.simps loR.simps)
done
- from h and this show "rec_exec (rec_maxr ?rR) [x, y, x] =
+ from h and this show "rec_eval (rec_maxr ?rR) [x, y, x] =
Maxr loR [x, y] x"
apply(simp)
done
@@ -1901,23 +1901,23 @@
done
lemma lo_lemma': "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow>
- rec_exec rec_lo [x, y] = lo x y"
+ rec_eval rec_lo [x, y] = lo x y"
by(simp add: Maxr_lo rec_lo_Maxr_lor)
-lemma lo_lemma'': "\<lbrakk>\<not> Suc 0 < x\<rbrakk> \<Longrightarrow> rec_exec rec_lo [x, y] = lo x y"
-apply(case_tac x, auto simp: rec_exec.simps rec_lo_def
+lemma lo_lemma'': "\<lbrakk>\<not> Suc 0 < x\<rbrakk> \<Longrightarrow> rec_eval rec_lo [x, y] = lo x y"
+apply(case_tac x, auto simp: rec_eval.simps rec_lo_def
Let_def lo.simps)
done
-lemma lo_lemma''': "\<lbrakk>\<not> Suc 0 < y\<rbrakk> \<Longrightarrow> rec_exec rec_lo [x, y] = lo x y"
-apply(case_tac y, auto simp: rec_exec.simps rec_lo_def
+lemma lo_lemma''': "\<lbrakk>\<not> Suc 0 < y\<rbrakk> \<Longrightarrow> rec_eval rec_lo [x, y] = lo x y"
+apply(case_tac y, auto simp: rec_eval.simps rec_lo_def
Let_def lo.simps)
done
text {*
The correctness of @{text "rec_lo"}:
*}
-lemma lo_lemma: "rec_exec rec_lo [x, y] = lo x y"
+lemma lo_lemma: "rec_eval rec_lo [x, y] = lo x y"
apply(case_tac "Suc 0 < x \<and> Suc 0 < y")
apply(auto simp: lo_lemma' lo_lemma'' lo_lemma''')
done
@@ -1954,24 +1954,24 @@
Cn 2 rec_mult [conR2, Cn 2 (constn 0) [id 2 0]]])"
lemma lg_maxr: "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow>
- rec_exec rec_lg [x, y] = Maxr lgR [x, y] x"
-proof(simp add: rec_exec.simps rec_lg_def Let_def)
+ rec_eval rec_lg [x, y] = Maxr lgR [x, y] x"
+proof(simp add: rec_eval.simps rec_lg_def Let_def)
assume h: "Suc 0 < x" "Suc 0 < y"
let ?rR = "(Cn 3 rec_le [Cn 3 rec_power
[recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 0])"
- have "rec_exec (rec_maxr ?rR) ([x, y] @ [x])
- = Maxr ((\<lambda> args. 0 < rec_exec ?rR args)) [x, y] x"
+ have "rec_eval (rec_maxr ?rR) ([x, y] @ [x])
+ = Maxr ((\<lambda> args. 0 < rec_eval ?rR args)) [x, y] x"
proof(rule Maxr_lemma)
show "primerec (Cn 3 rec_le [Cn 3 rec_power
[recf.id 3 (Suc 0), recf.id 3 2], recf.id 3 0]) (Suc (length [x, y]))"
apply(auto simp: numeral_3_eq_3)+
done
qed
- moreover have "Maxr lgR [x, y] x = Maxr ((\<lambda> args. 0 < rec_exec ?rR args)) [x, y] x"
- apply(simp add: rec_exec.simps power_lemma)
+ moreover have "Maxr lgR [x, y] x = Maxr ((\<lambda> args. 0 < rec_eval ?rR args)) [x, y] x"
+ apply(simp add: rec_eval.simps power_lemma)
apply(simp add: Maxr.simps lgR.simps)
done
- ultimately show "rec_exec (rec_maxr ?rR) [x, y, x] = Maxr lgR [x, y] x"
+ ultimately show "rec_eval (rec_maxr ?rR) [x, y, x] = Maxr lgR [x, y] x"
by simp
qed
@@ -1991,22 +1991,22 @@
apply(erule_tac x = xa in allE, simp)
done
-lemma lg_lemma': "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow> rec_exec rec_lg [x, y] = lg x y"
+lemma lg_lemma': "\<lbrakk>Suc 0 < x; Suc 0 < y\<rbrakk> \<Longrightarrow> rec_eval rec_lg [x, y] = lg x y"
apply(simp add: maxr_lg lg_maxr)
done
-lemma lg_lemma'': "\<not> Suc 0 < x \<Longrightarrow> rec_exec rec_lg [x, y] = lg x y"
-apply(simp add: rec_exec.simps rec_lg_def Let_def lg.simps)
+lemma lg_lemma'': "\<not> Suc 0 < x \<Longrightarrow> rec_eval rec_lg [x, y] = lg x y"
+apply(simp add: rec_eval.simps rec_lg_def Let_def lg.simps)
done
-lemma lg_lemma''': "\<not> Suc 0 < y \<Longrightarrow> rec_exec rec_lg [x, y] = lg x y"
-apply(simp add: rec_exec.simps rec_lg_def Let_def lg.simps)
+lemma lg_lemma''': "\<not> Suc 0 < y \<Longrightarrow> rec_eval rec_lg [x, y] = lg x y"
+apply(simp add: rec_eval.simps rec_lg_def Let_def lg.simps)
done
text {*
The correctness of @{text "rec_lg"}.
*}
-lemma lg_lemma: "rec_exec rec_lg [x, y] = lg x y"
+lemma lg_lemma: "rec_eval rec_lg [x, y] = lg x y"
apply(case_tac "Suc 0 < x \<and> Suc 0 < y", auto simp:
lg_lemma' lg_lemma'' lg_lemma''')
done
@@ -2032,8 +2032,8 @@
text {*
The correctness of @{text "rec_entry"}.
*}
-lemma entry_lemma: "rec_exec rec_entry [str, i] = Entry str i"
- by(simp add: rec_entry_def rec_exec.simps lo_lemma pi_lemma)
+lemma entry_lemma: "rec_eval rec_entry [str, i] = Entry str i"
+ by(simp add: rec_entry_def rec_eval.simps lo_lemma pi_lemma)
subsection {* The construction of F *}
@@ -2057,9 +2057,9 @@
declare listsum2.simps[simp del] rec_listsum2.simps[simp del]
lemma listsum2_lemma: "\<lbrakk>length xs = vl; n \<le> vl\<rbrakk> \<Longrightarrow>
- rec_exec (rec_listsum2 vl n) xs = listsum2 xs n"
+ rec_eval (rec_listsum2 vl n) xs = listsum2 xs n"
apply(induct n, simp_all)
-apply(simp_all add: rec_exec.simps rec_listsum2.simps listsum2.simps)
+apply(simp_all add: rec_eval.simps rec_listsum2.simps listsum2.simps)
done
fun strt' :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
@@ -2081,9 +2081,9 @@
declare strt'.simps[simp del] rec_strt'.simps[simp del]
lemma strt'_lemma: "\<lbrakk>length xs = vl; n \<le> vl\<rbrakk> \<Longrightarrow>
- rec_exec (rec_strt' vl n) xs = strt' xs n"
+ rec_eval (rec_strt' vl n) xs = strt' xs n"
apply(induct n)
-apply(simp_all add: rec_exec.simps rec_strt'.simps strt'.simps
+apply(simp_all add: rec_eval.simps rec_strt'.simps strt'.simps
Let_def power_lemma listsum2_lemma)
done
@@ -2108,30 +2108,30 @@
"rec_strt vl = Cn vl (rec_strt' vl vl) (rec_map s vl)"
lemma map_s_lemma: "length xs = vl \<Longrightarrow>
- map ((\<lambda>a. rec_exec a xs) \<circ> (\<lambda>i. Cn vl s [recf.id vl i]))
+ map ((\<lambda>a. rec_eval a xs) \<circ> (\<lambda>i. Cn vl s [recf.id vl i]))
[0..<vl]
= map Suc xs"
-apply(induct vl arbitrary: xs, simp, auto simp: rec_exec.simps)
+apply(induct vl arbitrary: xs, simp, auto simp: rec_eval.simps)
apply(subgoal_tac "\<exists> ys y. xs = ys @ [y]", auto)
proof -
fix ys y
assume ind: "\<And>xs. length xs = length (ys::nat list) \<Longrightarrow>
- map ((\<lambda>a. rec_exec a xs) \<circ> (\<lambda>i. Cn (length ys) s
+ map ((\<lambda>a. rec_eval a xs) \<circ> (\<lambda>i. Cn (length ys) s
[recf.id (length ys) (i)])) [0..<length ys] = map Suc xs"
show
- "map ((\<lambda>a. rec_exec a (ys @ [y])) \<circ> (\<lambda>i. Cn (Suc (length ys)) s
+ "map ((\<lambda>a. rec_eval a (ys @ [y])) \<circ> (\<lambda>i. Cn (Suc (length ys)) s
[recf.id (Suc (length ys)) (i)])) [0..<length ys] = map Suc ys"
proof -
- have "map ((\<lambda>a. rec_exec a ys) \<circ> (\<lambda>i. Cn (length ys) s
+ have "map ((\<lambda>a. rec_eval a ys) \<circ> (\<lambda>i. Cn (length ys) s
[recf.id (length ys) (i)])) [0..<length ys] = map Suc ys"
apply(rule_tac ind, simp)
done
moreover have
- "map ((\<lambda>a. rec_exec a (ys @ [y])) \<circ> (\<lambda>i. Cn (Suc (length ys)) s
+ "map ((\<lambda>a. rec_eval a (ys @ [y])) \<circ> (\<lambda>i. Cn (Suc (length ys)) s
[recf.id (Suc (length ys)) (i)])) [0..<length ys]
- = map ((\<lambda>a. rec_exec a ys) \<circ> (\<lambda>i. Cn (length ys) s
+ = map ((\<lambda>a. rec_eval a ys) \<circ> (\<lambda>i. Cn (length ys) s
[recf.id (length ys) (i)])) [0..<length ys]"
- apply(rule_tac map_ext, auto simp: rec_exec.simps nth_append)
+ apply(rule_tac map_ext, auto simp: rec_eval.simps nth_append)
done
ultimately show "?thesis"
by simp
@@ -2149,9 +2149,9 @@
The correctness of @{text "rec_strt"}.
*}
lemma strt_lemma: "length xs = vl \<Longrightarrow>
- rec_exec (rec_strt vl) xs = strt xs"
-apply(simp add: strt.simps rec_exec.simps strt'_lemma)
-apply(subgoal_tac "(map ((\<lambda>a. rec_exec a xs) \<circ> (\<lambda>i. Cn vl s [recf.id vl (i)])) [0..<vl])
+ rec_eval (rec_strt vl) xs = strt xs"
+apply(simp add: strt.simps rec_eval.simps strt'_lemma)
+apply(subgoal_tac "(map ((\<lambda>a. rec_eval a xs) \<circ> (\<lambda>i. Cn vl s [recf.id vl (i)])) [0..<vl])
= map Suc xs", auto)
apply(rule map_s_lemma, simp)
done
@@ -2172,8 +2172,8 @@
text {*
The correctness of @{text "scan"}.
*}
-lemma scan_lemma: "rec_exec rec_scan [r] = r mod 2"
- by(simp add: rec_exec.simps rec_scan_def mod_lemma)
+lemma scan_lemma: "rec_eval rec_scan [r] = r mod 2"
+ by(simp add: rec_eval.simps rec_scan_def mod_lemma)
fun newleft0 :: "nat list \<Rightarrow> nat"
where
@@ -2295,7 +2295,7 @@
The correctness of @{text "rec_newleft"}.
*}
lemma newleft_lemma:
- "rec_exec rec_newleft [p, r, a] = newleft p r a"
+ "rec_eval rec_newleft [p, r, a] = newleft p r a"
proof(simp only: rec_newleft_def Let_def)
let ?rgs = "[Cn 3 rec_newleft0 [recf.id 3 0, recf.id 3 1], Cn 3 rec_newleft2
[recf.id 3 0, recf.id 3 1], Cn 3 rec_newleft3 [recf.id 3 0, recf.id 3 1], recf.id 3 0]"
@@ -2305,8 +2305,8 @@
Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 2) [recf.id 3 0]],
Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 3) [recf.id 3 0]],
Cn 3 rec_less [Cn 3 (constn 3) [recf.id 3 0], recf.id 3 2]]"
- have k1: "rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a]
- = Embranch (zip (map rec_exec ?rgs) (map (\<lambda>r args. 0 < rec_exec r args) ?rrs)) [p, r, a]"
+ have k1: "rec_eval (rec_embranch (zip ?rgs ?rrs)) [p, r, a]
+ = Embranch (zip (map rec_eval ?rgs) (map (\<lambda>r args. 0 < rec_eval r args) ?rrs)) [p, r, a]"
apply(rule_tac embranch_lemma )
apply(auto simp: numeral_3_eq_3 numeral_2_eq_2 rec_newleft0_def
rec_newleft1_def rec_newleft2_def rec_newleft3_def)+
@@ -2317,17 +2317,17 @@
apply(case_tac "a = 3", rule_tac x = "2" in exI)
prefer 2
apply(case_tac "a > 3", rule_tac x = "3" in exI, auto)
- apply(auto simp: rec_exec.simps)
- apply(erule_tac [!] Suc_Suc_Suc_Suc_induct, auto simp: rec_exec.simps)
+ apply(auto simp: rec_eval.simps)
+ apply(erule_tac [!] Suc_Suc_Suc_Suc_induct, auto simp: rec_eval.simps)
done
- have k2: "Embranch (zip (map rec_exec ?rgs) (map (\<lambda>r args. 0 < rec_exec r args) ?rrs)) [p, r, a] = newleft p r a"
+ have k2: "Embranch (zip (map rec_eval ?rgs) (map (\<lambda>r args. 0 < rec_eval r args) ?rrs)) [p, r, a] = newleft p r a"
apply(simp add: Embranch.simps)
- apply(simp add: rec_exec.simps)
- apply(auto simp: newleft.simps rec_newleft0_def rec_exec.simps
+ apply(simp add: rec_eval.simps)
+ apply(auto simp: newleft.simps rec_newleft0_def rec_eval.simps
rec_newleft1_def rec_newleft2_def rec_newleft3_def)
done
from k1 and k2 show
- "rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a] = newleft p r a"
+ "rec_eval (rec_embranch (zip ?rgs ?rrs)) [p, r, a] = newleft p r a"
by simp
qed
@@ -2384,7 +2384,7 @@
text {*
The correctness of @{text "rec_newrght"}.
*}
-lemma newrght_lemma: "rec_exec rec_newrght [p, r, a] = newrght p r a"
+lemma newrght_lemma: "rec_eval rec_newrght [p, r, a] = newrght p r a"
proof(simp only: rec_newrght_def Let_def)
let ?gs' = "[newrgt0, newrgt1, newrgt2, newrgt3, \<lambda> zs. zs ! 1]"
let ?r0 = "\<lambda> zs. zs ! 2 = 0"
@@ -2405,8 +2405,8 @@
Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 3) [recf.id 3 0]],
Cn 3 rec_less [Cn 3 (constn 3) [recf.id 3 0], recf.id 3 2]]"
- have k1: "rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a]
- = Embranch (zip (map rec_exec ?rgs) (map (\<lambda>r args. 0 < rec_exec r args) ?rrs)) [p, r, a]"
+ have k1: "rec_eval (rec_embranch (zip ?rgs ?rrs)) [p, r, a]
+ = Embranch (zip (map rec_eval ?rgs) (map (\<lambda>r args. 0 < rec_eval r args) ?rrs)) [p, r, a]"
apply(rule_tac embranch_lemma)
apply(auto simp: numeral_3_eq_3 numeral_2_eq_2 rec_newrgt0_def
rec_newrgt1_def rec_newrgt2_def rec_newrgt3_def)+
@@ -2418,18 +2418,18 @@
prefer 2
apply(case_tac "a = 3", rule_tac x = "3" in exI)
prefer 2
- apply(case_tac "a > 3", rule_tac x = "4" in exI, auto simp: rec_exec.simps)
- apply(erule_tac [!] Suc_5_induct, auto simp: rec_exec.simps)
+ apply(case_tac "a > 3", rule_tac x = "4" in exI, auto simp: rec_eval.simps)
+ apply(erule_tac [!] Suc_5_induct, auto simp: rec_eval.simps)
done
- have k2: "Embranch (zip (map rec_exec ?rgs)
- (map (\<lambda>r args. 0 < rec_exec r args) ?rrs)) [p, r, a] = newrght p r a"
- apply(auto simp:Embranch.simps rec_exec.simps)
+ have k2: "Embranch (zip (map rec_eval ?rgs)
+ (map (\<lambda>r args. 0 < rec_eval r args) ?rrs)) [p, r, a] = newrght p r a"
+ apply(auto simp:Embranch.simps rec_eval.simps)
apply(auto simp: newrght.simps rec_newrgt3_def rec_newrgt2_def
- rec_newrgt1_def rec_newrgt0_def rec_exec.simps
+ rec_newrgt1_def rec_newrgt0_def rec_eval.simps
scan_lemma)
done
from k1 and k2 show
- "rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a] =
+ "rec_eval (rec_embranch (zip ?rgs ?rrs)) [p, r, a] =
newrght p r a" by simp
qed
@@ -2466,8 +2466,8 @@
text {*
The correctness of @{text "actn"}.
*}
-lemma actn_lemma: "rec_exec rec_actn [m, q, r] = actn m q r"
- by(auto simp: rec_actn_def rec_exec.simps entry_lemma scan_lemma)
+lemma actn_lemma: "rec_eval rec_actn [m, q, r] = actn m q r"
+ by(auto simp: rec_actn_def rec_eval.simps entry_lemma scan_lemma)
fun newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
where
@@ -2486,8 +2486,8 @@
Cn 3 rec_mult [Cn 3 (constn 0) [id 3 0],
Cn 3 rec_eq [id 3 1, Cn 3 (constn 0) [id 3 0]]]] "
-lemma newstat_lemma: "rec_exec rec_newstat [m, q, r] = newstat m q r"
-by(auto simp: rec_exec.simps entry_lemma scan_lemma rec_newstat_def)
+lemma newstat_lemma: "rec_eval rec_newstat [m, q, r] = newstat m q r"
+by(auto simp: rec_eval.simps entry_lemma scan_lemma rec_newstat_def)
declare newstat.simps[simp del] actn.simps[simp del]
@@ -2504,8 +2504,8 @@
Cn 3 rec_power [Cn 3 (constn (Pi 1)) [id 3 0], id 3 1]],
Cn 3 rec_power [Cn 3 (constn (Pi 2)) [id 3 0], id 3 2]]"
declare trpl.simps[simp del]
-lemma trpl_lemma: "rec_exec rec_trpl [p, q, r] = trpl p q r"
-by(auto simp: rec_trpl_def rec_exec.simps power_lemma trpl.simps)
+lemma trpl_lemma: "rec_eval rec_trpl [p, q, r] = trpl p q r"
+by(auto simp: rec_trpl_def rec_eval.simps power_lemma trpl.simps)
text{*left, stat, rght: decode func*}
fun left :: "nat \<Rightarrow> nat"
@@ -2555,24 +2555,24 @@
Cn vl (rec_strt (vl - 1))
(map (\<lambda> i. id vl (i)) [1..<vl])]"
-lemma left_lemma: "rec_exec rec_left [c] = left c"
-by(simp add: rec_exec.simps rec_left_def left.simps lo_lemma)
+lemma left_lemma: "rec_eval rec_left [c] = left c"
+by(simp add: rec_eval.simps rec_left_def left.simps lo_lemma)
-lemma right_lemma: "rec_exec rec_right [c] = rght c"
-by(simp add: rec_exec.simps rec_right_def rght.simps lo_lemma)
-
-lemma stat_lemma: "rec_exec rec_stat [c] = stat c"
-by(simp add: rec_exec.simps rec_stat_def stat.simps lo_lemma)
+lemma right_lemma: "rec_eval rec_right [c] = rght c"
+by(simp add: rec_eval.simps rec_right_def rght.simps lo_lemma)
+
+lemma stat_lemma: "rec_eval rec_stat [c] = stat c"
+by(simp add: rec_eval.simps rec_stat_def stat.simps lo_lemma)
declare rec_strt.simps[simp del] strt.simps[simp del]
lemma map_cons_eq:
- "(map ((\<lambda>a. rec_exec a (m # xs)) \<circ>
+ "(map ((\<lambda>a. rec_eval a (m # xs)) \<circ>
(\<lambda>i. recf.id (Suc (length xs)) (i)))
[Suc 0..<Suc (length xs)])
= map (\<lambda> i. xs ! (i - 1)) [Suc 0..<Suc (length xs)]"
apply(rule map_ext, auto)
-apply(auto simp: rec_exec.simps nth_append nth_Cons split: nat.split)
+apply(auto simp: rec_eval.simps nth_append nth_Cons split: nat.split)
done
lemma list_map_eq:
@@ -2616,11 +2616,11 @@
lemma [elim]:
"Suc 0 \<le> length xs \<Longrightarrow>
- (map ((\<lambda>a. rec_exec a (m # xs)) \<circ>
+ (map ((\<lambda>a. rec_eval a (m # xs)) \<circ>
(\<lambda>i. recf.id (Suc (length xs)) (i)))
[Suc 0..<length xs] @ [(m # xs) ! length xs]) = xs"
using map_cons_eq[of m xs]
-apply(simp del: map_eq_conv add: rec_exec.simps)
+apply(simp del: map_eq_conv add: rec_eval.simps)
using list_map_eq[of "length xs" xs]
apply(simp)
done
@@ -2628,11 +2628,11 @@
lemma inpt_lemma:
"\<lbrakk>Suc (length xs) = vl\<rbrakk> \<Longrightarrow>
- rec_exec (rec_inpt vl) (m # xs) = inpt m xs"
-apply(auto simp: rec_exec.simps rec_inpt_def
+ rec_eval (rec_inpt vl) (m # xs) = inpt m xs"
+apply(auto simp: rec_eval.simps rec_inpt_def
trpl_lemma inpt.simps strt_lemma)
apply(subgoal_tac
- "(map ((\<lambda>a. rec_exec a (m # xs)) \<circ>
+ "(map ((\<lambda>a. rec_eval a (m # xs)) \<circ>
(\<lambda>i. recf.id (Suc (length xs)) (i)))
[Suc 0..<length xs] @ [(m # xs) ! length xs]) = xs", simp)
apply(auto, case_tac xs, auto)
@@ -2656,8 +2656,8 @@
Cn 2 rec_stat [id 2 1],
Cn 2 rec_right [id 2 1]]]]"
-lemma newconf_lemma: "rec_exec rec_newconf [m ,c] = newconf m c"
-by(auto simp: rec_newconf_def rec_exec.simps
+lemma newconf_lemma: "rec_eval rec_newconf [m ,c] = newconf m c"
+by(auto simp: rec_newconf_def rec_eval.simps
trpl_lemma newleft_lemma left_lemma
right_lemma stat_lemma newrght_lemma actn_lemma
newstat_lemma stat_lemma newconf.simps)
@@ -2685,15 +2685,15 @@
(Cn 4 rec_newconf [id 4 0, id 4 3])"
lemma conf_step:
- "rec_exec rec_conf [m, r, Suc t] =
- rec_exec rec_newconf [m, rec_exec rec_conf [m, r, t]]"
+ "rec_eval rec_conf [m, r, Suc t] =
+ rec_eval rec_newconf [m, rec_eval rec_conf [m, r, t]]"
proof -
- have "rec_exec rec_conf ([m, r] @ [Suc t]) =
- rec_exec rec_newconf [m, rec_exec rec_conf [m, r, t]]"
+ have "rec_eval rec_conf ([m, r] @ [Suc t]) =
+ rec_eval rec_newconf [m, rec_eval rec_conf [m, r, t]]"
by(simp only: rec_conf_def rec_pr_Suc_simp_rewrite,
- simp add: rec_exec.simps)
- thus "rec_exec rec_conf [m, r, Suc t] =
- rec_exec rec_newconf [m, rec_exec rec_conf [m, r, t]]"
+ simp add: rec_eval.simps)
+ thus "rec_eval rec_conf [m, r, Suc t] =
+ rec_eval rec_newconf [m, rec_eval rec_conf [m, r, t]]"
by simp
qed
@@ -2701,9 +2701,9 @@
The correctness of @{text "rec_conf"}.
*}
lemma conf_lemma:
- "rec_exec rec_conf [m, r, t] = conf m r t"
+ "rec_eval rec_conf [m, r, t] = conf m r t"
apply(induct t)
-apply(simp add: rec_conf_def rec_exec.simps conf.simps inpt_lemma trpl_lemma)
+apply(simp add: rec_conf_def rec_eval.simps conf.simps inpt_lemma trpl_lemma)
apply(simp add: conf_step conf.simps)
done
@@ -2735,21 +2735,21 @@
constn 2]], constn 1]]],
Cn 1 rec_eq [rec_right, constn 0]]"
-lemma NSTD_lemma1: "rec_exec rec_NSTD [c] = Suc 0 \<or>
- rec_exec rec_NSTD [c] = 0"
-by(simp add: rec_exec.simps rec_NSTD_def)
+lemma NSTD_lemma1: "rec_eval rec_NSTD [c] = Suc 0 \<or>
+ rec_eval rec_NSTD [c] = 0"
+by(simp add: rec_eval.simps rec_NSTD_def)
declare NSTD.simps[simp del]
-lemma NSTD_lemma2': "(rec_exec rec_NSTD [c] = Suc 0) \<Longrightarrow> NSTD c"
-apply(simp add: rec_exec.simps rec_NSTD_def stat_lemma left_lemma
+lemma NSTD_lemma2': "(rec_eval rec_NSTD [c] = Suc 0) \<Longrightarrow> NSTD c"
+apply(simp add: rec_eval.simps rec_NSTD_def stat_lemma left_lemma
lg_lemma right_lemma power_lemma NSTD.simps eq_lemma)
apply(auto)
apply(case_tac "0 < left c", simp, simp)
done
lemma NSTD_lemma2'':
- "NSTD c \<Longrightarrow> (rec_exec rec_NSTD [c] = Suc 0)"
-apply(simp add: rec_exec.simps rec_NSTD_def stat_lemma
+ "NSTD c \<Longrightarrow> (rec_eval rec_NSTD [c] = Suc 0)"
+apply(simp add: rec_eval.simps rec_NSTD_def stat_lemma
left_lemma lg_lemma right_lemma power_lemma NSTD.simps)
apply(auto split: if_splits)
done
@@ -2757,7 +2757,7 @@
text {*
The correctness of @{text "NSTD"}.
*}
-lemma NSTD_lemma2: "(rec_exec rec_NSTD [c] = Suc 0) = NSTD c"
+lemma NSTD_lemma2: "(rec_eval rec_NSTD [c] = Suc 0) = NSTD c"
using NSTD_lemma1
apply(auto intro: NSTD_lemma2' NSTD_lemma2'')
done
@@ -2766,7 +2766,7 @@
where
"nstd c = (if NSTD c then 1 else 0)"
-lemma nstd_lemma: "rec_exec rec_NSTD [c] = nstd c"
+lemma nstd_lemma: "rec_eval rec_NSTD [c] = nstd c"
using NSTD_lemma1
apply(simp add: NSTD_lemma2, auto)
done
@@ -2790,8 +2790,8 @@
The correctness of @{text "rec_nonstop"}.
*}
lemma nonstop_lemma:
- "rec_exec rec_nonstop [m, r, t] = nonstop m r t"
-apply(simp add: rec_exec.simps rec_nonstop_def nstd_lemma conf_lemma)
+ "rec_eval rec_nonstop [m, r, t] = nonstop m r t"
+apply(simp add: rec_eval.simps rec_nonstop_def nstd_lemma conf_lemma)
done
text{*
@@ -2985,51 +2985,51 @@
@{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
done
-lemma primerec_terminate:
- "\<lbrakk>primerec f x; length xs = x\<rbrakk> \<Longrightarrow> terminate f xs"
+lemma primerec_terminates:
+ "\<lbrakk>primerec f x; length xs = x\<rbrakk> \<Longrightarrow> terminates f xs"
proof(induct arbitrary: xs rule: primerec.induct)
fix xs
- assume "length (xs::nat list) = Suc 0" thus "terminate z xs"
+ assume "length (xs::nat list) = Suc 0" thus "terminates z xs"
by(case_tac xs, auto intro: termi_z)
next
fix xs
- assume "length (xs::nat list) = Suc 0" thus "terminate s xs"
+ assume "length (xs::nat list) = Suc 0" thus "terminates s xs"
by(case_tac xs, auto intro: termi_s)
next
fix n m xs
- assume "n < m" "length (xs::nat list) = m" thus "terminate (id m n) xs"
+ assume "n < m" "length (xs::nat list) = m" thus "terminates (id m n) xs"
by(erule_tac termi_id, simp)
next
fix f k gs m n xs
- assume ind: "\<forall>i<length gs. primerec (gs ! i) m \<and> (\<forall>x. length x = m \<longrightarrow> terminate (gs ! i) x)"
- and ind2: "\<And> xs. length xs = k \<Longrightarrow> terminate f xs"
+ assume ind: "\<forall>i<length gs. primerec (gs ! i) m \<and> (\<forall>x. length x = m \<longrightarrow> terminates (gs ! i) x)"
+ and ind2: "\<And> xs. length xs = k \<Longrightarrow> terminates f xs"
and h: "primerec f k" "length gs = k" "m = n" "length (xs::nat list) = m"
- have "terminate f (map (\<lambda>g. rec_exec g xs) gs)"
- using ind2[of "(map (\<lambda>g. rec_exec g xs) gs)"] h
+ have "terminates f (map (\<lambda>g. rec_eval g xs) gs)"
+ using ind2[of "(map (\<lambda>g. rec_eval g xs) gs)"] h
by simp
- moreover have "\<forall>g\<in>set gs. terminate g xs"
+ moreover have "\<forall>g\<in>set gs. terminates g xs"
using ind h
by(auto simp: set_conv_nth)
- ultimately show "terminate (Cn n f gs) xs"
+ ultimately show "terminates (Cn n f gs) xs"
using h
by(rule_tac termi_cn, auto)
next
fix f n g m xs
- assume ind1: "\<And>xs. length xs = n \<Longrightarrow> terminate f xs"
- and ind2: "\<And>xs. length xs = Suc (Suc n) \<Longrightarrow> terminate g xs"
+ assume ind1: "\<And>xs. length xs = n \<Longrightarrow> terminates f xs"
+ and ind2: "\<And>xs. length xs = Suc (Suc n) \<Longrightarrow> terminates g xs"
and h: "primerec f n" " primerec g (Suc (Suc n))" " m = Suc n" "length (xs::nat list) = m"
- have "\<forall>y<last xs. terminate g (butlast xs @ [y, rec_exec (Pr n f g) (butlast xs @ [y])])"
+ have "\<forall>y<last xs. terminates g (butlast xs @ [y, rec_eval (Pr n f g) (butlast xs @ [y])])"
using h
apply(auto)
by(rule_tac ind2, simp)
- moreover have "terminate f (butlast xs)"
+ moreover have "terminates f (butlast xs)"
using ind1[of "butlast xs"] h
by simp
moreover have "length (butlast xs) = n"
using h by simp
- ultimately have "terminate (Pr n f g) (butlast xs @ [last xs])"
+ ultimately have "terminates (Pr n f g) (butlast xs @ [last xs])"
by(rule_tac termi_pr, simp_all)
- thus "terminate (Pr n f g) xs"
+ thus "terminates (Pr n f g) xs"
using h
by(case_tac "xs = []", auto)
qed
@@ -3061,8 +3061,8 @@
text {*
The correctness of @{text "rec_valu"}.
*}
-lemma value_lemma: "rec_exec rec_valu [r] = valu r"
-apply(simp add: rec_exec.simps rec_valu_def lg_lemma)
+lemma value_lemma: "rec_eval rec_valu [r] = valu r"
+apply(simp add: rec_eval.simps rec_valu_def lg_lemma)
done
lemma [intro]: "primerec rec_valu (Suc 0)"
@@ -3101,12 +3101,12 @@
id (length ys) (k)"
by(erule_tac get_fstn_args_nth)
-lemma terminate_halt_lemma:
- "\<lbrakk>rec_exec rec_nonstop ([m, r] @ [t]) = 0;
- \<forall>i<t. 0 < rec_exec rec_nonstop ([m, r] @ [i])\<rbrakk> \<Longrightarrow> terminate rec_halt [m, r]"
+lemma terminates_halt_lemma:
+ "\<lbrakk>rec_eval rec_nonstop ([m, r] @ [t]) = 0;
+ \<forall>i<t. 0 < rec_eval rec_nonstop ([m, r] @ [i])\<rbrakk> \<Longrightarrow> terminates rec_halt [m, r]"
apply(simp add: rec_halt_def)
apply(rule_tac termi_mn, auto)
-apply(rule_tac [!] primerec_terminate, auto)
+apply(rule_tac [!] primerec_terminates, auto)
done
@@ -3114,17 +3114,17 @@
The correctness of @{text "rec_F"}, halt case.
*}
-lemma F_lemma: "rec_exec rec_halt [m, r] = t \<Longrightarrow> rec_exec rec_F [m, r] = (valu (rght (conf m r t)))"
-by(simp add: rec_F_def rec_exec.simps value_lemma right_lemma conf_lemma halt_lemma)
-
-lemma terminate_F_lemma: "terminate rec_halt [m, r] \<Longrightarrow> terminate rec_F [m, r]"
+lemma F_lemma: "rec_eval rec_halt [m, r] = t \<Longrightarrow> rec_eval rec_F [m, r] = (valu (rght (conf m r t)))"
+by(simp add: rec_F_def rec_eval.simps value_lemma right_lemma conf_lemma halt_lemma)
+
+lemma terminates_F_lemma: "terminates rec_halt [m, r] \<Longrightarrow> terminates rec_F [m, r]"
apply(simp add: rec_F_def)
apply(rule_tac termi_cn, auto)
-apply(rule_tac primerec_terminate, auto)
+apply(rule_tac primerec_terminates, auto)
apply(rule_tac termi_cn, auto)
-apply(rule_tac primerec_terminate, auto)
+apply(rule_tac primerec_terminates, auto)
apply(rule_tac termi_cn, auto)
-apply(rule_tac primerec_terminate, auto)
+apply(rule_tac primerec_terminates, auto)
apply(rule_tac [!] termi_id, auto)
done
@@ -4001,7 +4001,7 @@
lemma rec_t_eq_step:
"(\<lambda> (s, l, r). s \<le> length tp div 2) c \<Longrightarrow>
trpl_code (step0 c tp) =
- rec_exec rec_newconf [code tp, trpl_code c]"
+ rec_eval rec_newconf [code tp, trpl_code c]"
apply(cases c, simp)
proof(case_tac "fetch tp a (read ca)",
simp add: newconf.simps trpl_code.simps step.simps)
@@ -4163,8 +4163,8 @@
lemma [simp]:
"trpl_code (steps0 (Suc 0, Bk\<up>l, <lm>) tp 0) =
- rec_exec rec_conf [code tp, bl2wc (<lm>), 0]"
-apply(simp add: steps.simps rec_exec.simps conf_lemma conf.simps
+ rec_eval rec_conf [code tp, bl2wc (<lm>), 0]"
+apply(simp add: steps.simps rec_eval.simps conf_lemma conf.simps
inpt.simps trpl_code.simps bl2wc.simps)
done
@@ -4212,7 +4212,7 @@
lemma rec_t_eq_steps:
"tm_wf (tp,0) \<Longrightarrow>
trpl_code (steps0 (Suc 0, Bk\<up>l, <lm>) tp stp) =
- rec_exec rec_conf [code tp, bl2wc (<lm>), stp]"
+ rec_eval rec_conf [code tp, bl2wc (<lm>), stp]"
proof(induct stp)
case 0 thus "?case" by(simp)
next
@@ -4220,11 +4220,11 @@
proof -
assume ind:
"tm_wf (tp,0) \<Longrightarrow> trpl_code (steps0 (Suc 0, Bk\<up> l, <lm>) tp n)
- = rec_exec rec_conf [code tp, bl2wc (<lm>), n]"
+ = rec_eval rec_conf [code tp, bl2wc (<lm>), n]"
and h: "tm_wf (tp, 0)"
show
"trpl_code (steps0 (Suc 0, Bk\<up> l, <lm>) tp (Suc n)) =
- rec_exec rec_conf [code tp, bl2wc (<lm>), Suc n]"
+ rec_eval rec_conf [code tp, bl2wc (<lm>), Suc n]"
proof(case_tac "steps0 (Suc 0, Bk\<up> l, <lm>) tp n",
simp only: step_red conf_lemma conf.simps)
fix a b c
@@ -4235,7 +4235,7 @@
done
moreover hence
"trpl_code (step0 (a, b, c) tp) =
- rec_exec rec_newconf [code tp, trpl_code (a, b, c)]"
+ rec_eval rec_newconf [code tp, trpl_code (a, b, c)]"
apply(rule_tac rec_t_eq_step)
using h g
apply(simp add: state_in_range)
@@ -4293,11 +4293,11 @@
"\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up> m, Oc\<up> rs @ Bk\<up> n);
tm_wf (tp, 0);
rs > 0\<rbrakk>
- \<Longrightarrow> rec_exec rec_nonstop [code tp, bl2wc (<lm>), stp] = 0"
+ \<Longrightarrow> rec_eval rec_nonstop [code tp, bl2wc (<lm>), stp] = 0"
proof(simp add: nonstop_lemma nonstop.simps nstd.simps)
assume h: "steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up> m, Oc\<up> rs @ Bk\<up> n)"
and tc_t: "tm_wf (tp, 0)" "rs > 0"
- have g: "rec_exec rec_conf [code tp, bl2wc (<lm>), stp] =
+ have g: "rec_eval rec_conf [code tp, bl2wc (<lm>), stp] =
trpl_code (0, Bk\<up> m, Oc\<up> rs@Bk\<up> n)"
using rec_t_eq_steps[of tp l lm stp] tc_t h
by(simp)
@@ -4487,26 +4487,26 @@
execution of of TMs.
*}
-lemma terminate_halt:
+lemma terminates_halt:
"\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up>m, Oc\<up>rs@Bk\<up>n);
- tm_wf (tp,0); 0<rs\<rbrakk> \<Longrightarrow> terminate rec_halt [code tp, (bl2wc (<lm>))]"
+ tm_wf (tp,0); 0<rs\<rbrakk> \<Longrightarrow> terminates rec_halt [code tp, (bl2wc (<lm>))]"
apply(frule_tac halt_least_step, auto)
-thm terminate_halt_lemma
-apply(rule_tac t = stpa in terminate_halt_lemma)
+thm terminates_halt_lemma
+apply(rule_tac t = stpa in terminates_halt_lemma)
apply(simp_all add: nonstop_lemma, auto)
done
-lemma terminate_F:
+lemma terminates_F:
"\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up>m, Oc\<up>rs@Bk\<up>n);
- tm_wf (tp,0); 0<rs\<rbrakk> \<Longrightarrow> terminate rec_F [code tp, (bl2wc (<lm>))]"
-apply(drule_tac terminate_halt, simp_all)
-apply(erule_tac terminate_F_lemma)
+ tm_wf (tp,0); 0<rs\<rbrakk> \<Longrightarrow> terminates rec_F [code tp, (bl2wc (<lm>))]"
+apply(drule_tac terminates_halt, simp_all)
+apply(erule_tac terminates_F_lemma)
done
lemma F_correct:
"\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up>m, Oc\<up>rs@Bk\<up>n);
tm_wf (tp,0); 0<rs\<rbrakk>
- \<Longrightarrow> rec_exec rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
+ \<Longrightarrow> rec_eval rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
apply(frule_tac halt_least_step, auto)
apply(frule_tac nonstop_t_eq, auto simp: nonstop_lemma)
using rec_t_eq_steps[of tp l lm stp]
@@ -4523,11 +4523,11 @@
using halt_state_keep[of "code tp" lm stpa stp]
by(simp)
moreover have g2:
- "rec_exec rec_halt [code tp, (bl2wc (<lm>))] = stpa"
+ "rec_eval rec_halt [code tp, (bl2wc (<lm>))] = stpa"
using h
- by(auto simp: rec_exec.simps rec_halt_def nonstop_lemma intro!: Least_equality)
+ by(auto simp: rec_eval.simps rec_halt_def nonstop_lemma intro!: Least_equality)
show
- "rec_exec rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
+ "rec_eval rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
proof -
have
"valu (rght (conf (code tp) (bl2wc (<lm>)) stpa)) = rs - Suc 0"
@@ -4536,7 +4536,7 @@
bl2wc.simps bl2nat_append lg_power)
done
thus "?thesis"
- by(simp add: rec_exec.simps F_lemma g2)
+ by(simp add: rec_eval.simps F_lemma g2)
qed
qed