--- a/thys/UF.thy Thu Mar 14 20:43:43 2013 +0000
+++ b/thys/UF.thy Wed Mar 27 09:47:02 2013 +0000
@@ -158,60 +158,6 @@
it always returns meaningful results for primitive recursive
functions.
*}
-function rec_exec :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
- where
- "rec_exec z xs = 0" |
- "rec_exec s xs = (Suc (xs ! 0))" |
- "rec_exec (id m n) xs = (xs ! n)" |
- "rec_exec (Cn n f gs) xs =
- (let ys = (map (\<lambda> a. rec_exec a xs) gs) in
- rec_exec f ys)" |
- "rec_exec (Pr n f g) xs =
- (if last xs = 0 then
- rec_exec f (butlast xs)
- else rec_exec g (butlast xs @ [last xs - 1] @
- [rec_exec (Pr n f g) (butlast xs @ [last xs - 1])]))" |
- "rec_exec (Mn n f) xs = (LEAST x. rec_exec f (xs @ [x]) = 0)"
-by pat_completeness auto
-termination
-proof
- show "wf (measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). last xs)])"
- by auto
-next
- fix n f gs xs x
- assume "(x::recf) \<in> set gs"
- thus "((x, xs), Cn n f gs, xs) \<in>
- measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]"
- by(induct gs, auto)
-next
- fix n f gs xs x
- assume "x = map (\<lambda>a. rec_exec a xs) gs"
- "\<And>x. x \<in> set gs \<Longrightarrow> rec_exec_dom (x, xs)"
- thus "((f, x), Cn n f gs, xs) \<in>
- measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]"
- by(auto)
-next
- fix n f g xs
- show "((f, butlast xs), Pr n f g, xs) \<in>
- measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]"
- by auto
-next
- fix n f g xs
- assume "last xs \<noteq> (0::nat)" thus
- "((Pr n f g, butlast xs @ [last xs - 1]), Pr n f g, xs)
- \<in> measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]"
- by auto
-next
- fix n f g xs
- show "((g, butlast xs @ [last xs - 1] @ [rec_exec (Pr n f g) (butlast xs @ [last xs - 1])]),
- Pr n f g, xs) \<in> measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]"
- by auto
-next
- fix n f xs x
- show "((f, xs @ [x]), Mn n f, xs) \<in>
- measures [\<lambda>(r, xs). size r, \<lambda>(r, xs). last xs]"
- by auto
-qed
declare rec_exec.simps[simp del] constn.simps[simp del]
@@ -280,7 +226,6 @@
else 1)"
by(induct_tac y, auto simp: rec_exec.simps sg_lemma rec_conj_def mult_lemma)
-
text {*
Correctness of @{text "rec_disj"}.
*}
@@ -2948,190 +2893,6 @@
The lemma relates the interpreter of primitive fucntions with
the calculation relation of general recursive functions.
*}
-lemma prime_rel_exec_eq: "primerec r (length xs)
- \<Longrightarrow> rec_calc_rel r xs rs = (rec_exec r xs = rs)"
-proof(induct r xs arbitrary: rs rule: rec_exec.induct, simp_all)
- fix xs rs
- assume "primerec z (length (xs::nat list))"
- hence "length xs = Suc 0" by(erule_tac prime_z_reverse, simp)
- thus "rec_calc_rel z xs rs = (rec_exec z xs = rs)"
- apply(case_tac xs, simp, auto)
- apply(erule_tac calc_z_reverse, simp add: rec_exec.simps)
- apply(simp add: rec_exec.simps, rule_tac calc_z)
- done
-next
- fix xs rs
- assume "primerec s (length (xs::nat list))"
- hence "length xs = Suc 0" ..
- thus "rec_calc_rel s xs rs = (rec_exec s xs = rs)"
- by(case_tac xs, auto simp: rec_exec.simps intro: calc_s
- elim: calc_s_reverse)
-next
- fix m n xs rs
- assume "primerec (recf.id m n) (length (xs::nat list))"
- thus
- "rec_calc_rel (recf.id m n) xs rs =
- (rec_exec (recf.id m n) xs = rs)"
- apply(erule_tac prime_id_reverse)
- apply(simp add: rec_exec.simps, auto)
- apply(erule_tac calc_id_reverse, simp)
- apply(rule_tac calc_id, auto)
- done
-next
- fix n f gs xs rs
- assume ind1:
- "\<And>x rs. \<lbrakk>x \<in> set gs; primerec x (length xs)\<rbrakk> \<Longrightarrow>
- rec_calc_rel x xs rs = (rec_exec x xs = rs)"
- and ind2:
- "\<And>x rs. \<lbrakk>x = map (\<lambda>a. rec_exec a xs) gs;
- primerec f (length gs)\<rbrakk> \<Longrightarrow>
- rec_calc_rel f (map (\<lambda>a. rec_exec a xs) gs) rs =
- (rec_exec f (map (\<lambda>a. rec_exec a xs) gs) = rs)"
- and h: "primerec (Cn n f gs) (length xs)"
- show "rec_calc_rel (Cn n f gs) xs rs =
- (rec_exec (Cn n f gs) xs = rs)"
- proof(auto simp: rec_exec.simps, erule_tac calc_cn_reverse, auto)
- fix ys
- assume g1:"\<forall>k<length gs. rec_calc_rel (gs ! k) xs (ys ! k)"
- and g2: "length ys = length gs"
- and g3: "rec_calc_rel f ys rs"
- have "rec_calc_rel f (map (\<lambda>a. rec_exec a xs) gs) rs =
- (rec_exec f (map (\<lambda>a. rec_exec a xs) gs) = rs)"
- apply(rule_tac ind2, auto)
- using h
- apply(erule_tac prime_cn_reverse, simp)
- done
- moreover have "ys = (map (\<lambda>a. rec_exec a xs) gs)"
- proof(rule_tac nth_equalityI, auto simp: g2)
- fix i
- assume "i < length gs" thus "ys ! i = rec_exec (gs!i) xs"
- using ind1[of "gs ! i" "ys ! i"] g1 h
- apply(erule_tac prime_cn_reverse, simp)
- done
- qed
- ultimately show "rec_exec f (map (\<lambda>a. rec_exec a xs) gs) = rs"
- using g3
- by(simp)
- next
- from h show
- "rec_calc_rel (Cn n f gs) xs
- (rec_exec f (map (\<lambda>a. rec_exec a xs) gs))"
- apply(rule_tac rs = "(map (\<lambda>a. rec_exec a xs) gs)" in calc_cn,
- auto)
- apply(erule_tac [!] prime_cn_reverse, auto)
- proof -
- fix k
- assume "k < length gs" "primerec f (length gs)"
- "\<forall>i<length gs. primerec (gs ! i) (length xs)"
- thus "rec_calc_rel (gs ! k) xs (rec_exec (gs ! k) xs)"
- using ind1[of "gs!k" "(rec_exec (gs ! k) xs)"]
- by(simp)
- next
- assume "primerec f (length gs)"
- "\<forall>i<length gs. primerec (gs ! i) (length xs)"
- thus "rec_calc_rel f (map (\<lambda>a. rec_exec a xs) gs)
- (rec_exec f (map (\<lambda>a. rec_exec a xs) gs))"
- using ind2[of "(map (\<lambda>a. rec_exec a xs) gs)"
- "(rec_exec f (map (\<lambda>a. rec_exec a xs) gs))"]
- by simp
- qed
- qed
-next
- fix n f g xs rs
- assume ind1:
- "\<And>rs. \<lbrakk>last xs = 0; primerec f (length xs - Suc 0)\<rbrakk>
- \<Longrightarrow> rec_calc_rel f (butlast xs) rs =
- (rec_exec f (butlast xs) = rs)"
- and ind2 :
- "\<And>rs. \<lbrakk>0 < last xs;
- primerec (Pr n f g) (Suc (length xs - Suc 0))\<rbrakk> \<Longrightarrow>
- rec_calc_rel (Pr n f g) (butlast xs @ [last xs - Suc 0]) rs
- = (rec_exec (Pr n f g) (butlast xs @ [last xs - Suc 0]) = rs)"
- and ind3:
- "\<And>rs. \<lbrakk>0 < last xs; primerec g (Suc (Suc (length xs - Suc 0)))\<rbrakk>
- \<Longrightarrow> rec_calc_rel g (butlast xs @
- [last xs - Suc 0, rec_exec (Pr n f g)
- (butlast xs @ [last xs - Suc 0])]) rs =
- (rec_exec g (butlast xs @ [last xs - Suc 0,
- rec_exec (Pr n f g)
- (butlast xs @ [last xs - Suc 0])]) = rs)"
- and h: "primerec (Pr n f g) (length (xs::nat list))"
- show "rec_calc_rel (Pr n f g) xs rs = (rec_exec (Pr n f g) xs = rs)"
- proof(auto)
- assume "rec_calc_rel (Pr n f g) xs rs"
- thus "rec_exec (Pr n f g) xs = rs"
- proof(erule_tac calc_pr_reverse)
- fix l
- assume g: "xs = l @ [0]"
- "rec_calc_rel f l rs"
- "n = length l"
- thus "rec_exec (Pr n f g) xs = rs"
- using ind1[of rs] h
- apply(simp add: rec_exec.simps,
- erule_tac prime_pr_reverse, simp)
- done
- next
- fix l y ry
- assume d:"xs = l @ [Suc y]"
- "rec_calc_rel (Pr (length l) f g) (l @ [y]) ry"
- "n = length l"
- "rec_calc_rel g (l @ [y, ry]) rs"
- moreover hence "primerec g (Suc (Suc n))" using h
- proof(erule_tac prime_pr_reverse)
- assume "primerec g (Suc (Suc n))" "length xs = Suc n"
- thus "?thesis" by simp
- qed
- ultimately show "rec_exec (Pr n f g) xs = rs"
- apply(simp)
- using ind3[of rs]
- apply(simp add: rec_pr_Suc_simp_rewrite)
- using ind2[of ry] h
- apply(simp)
- done
- qed
- next
- show "rec_calc_rel (Pr n f g) xs (rec_exec (Pr n f g) xs)"
- proof -
- have "rec_calc_rel (Pr n f g) (butlast xs @ [last xs])
- (rec_exec (Pr n f g) (butlast xs @ [last xs]))"
- using h
- apply(erule_tac prime_pr_reverse, simp)
- apply(case_tac "last xs", simp)
- apply(rule_tac calc_pr_zero, simp)
- using ind1[of "rec_exec (Pr n f g) (butlast xs @ [0])"]
- apply(simp add: rec_exec.simps, simp, simp, simp)
- apply(rule_tac rk = "rec_exec (Pr n f g)
- (butlast xs@[last xs - Suc 0])" in calc_pr_ind)
- using ind2[of "rec_exec (Pr n f g)
- (butlast xs @ [last xs - Suc 0])"] h
- apply(simp, simp, simp)
- proof -
- fix nat
- assume "length xs = Suc n"
- "primerec g (Suc (Suc n))"
- "last xs = Suc nat"
- thus
- "rec_calc_rel g (butlast xs @ [nat, rec_exec (Pr n f g)
- (butlast xs @ [nat])]) (rec_exec (Pr n f g) (butlast xs @ [Suc nat]))"
- using ind3[of "rec_exec (Pr n f g)
- (butlast xs @ [Suc nat])"]
- apply(simp add: rec_exec.simps)
- done
- qed
- thus "rec_calc_rel (Pr n f g) xs (rec_exec (Pr n f g) xs)"
- using h
- apply(erule_tac prime_pr_reverse, simp)
- apply(subgoal_tac "butlast xs @ [last xs] = xs", simp)
- apply(case_tac xs, simp, simp)
- done
- qed
- qed
-next
- fix n f xs rs
- assume "primerec (Mn n f) (length (xs::nat list))"
- thus "rec_calc_rel (Mn n f) xs rs = (rec_exec (Mn n f) xs = rs)"
- by(erule_tac prime_mn_reverse)
-qed
declare numeral_2_eq_2[simp] numeral_3_eq_3[simp]
@@ -3141,11 +2902,6 @@
@{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
done
-lemma [simp]:
-"rec_calc_rel rec_right [r] rs = (rec_exec rec_right [r] = rs)"
-apply(rule_tac prime_rel_exec_eq, auto)
-done
-
lemma [intro]: "primerec rec_pi (Suc 0)"
apply(simp add: rec_pi_def rec_dummy_pi_def
rec_np_def rec_fac_def rec_prime_def
@@ -3283,12 +3039,6 @@
apply(auto simp: numeral_4_eq_4)
done
-lemma [simp]:
- "rec_calc_rel rec_conf [m, r, t] rs =
- (rec_exec rec_conf [m, r, t] = rs)"
-apply(rule_tac prime_rel_exec_eq, auto)
-done
-
lemma [intro]: "primerec rec_lg (Suc (Suc 0))"
apply(simp add: rec_lg_def Let_def)
apply(tactic {* resolve_tac [@{thm prime_cn},
@@ -3303,38 +3053,61 @@
@{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
done
-lemma nonstop_eq[simp]:
- "rec_calc_rel rec_nonstop [m, r, t] rs =
- (rec_exec rec_nonstop [m, r, t] = rs)"
-apply(rule prime_rel_exec_eq, auto)
-done
-
-lemma halt_lemma':
- "rec_calc_rel rec_halt [m, r] t =
- (rec_calc_rel rec_nonstop [m, r, t] 0 \<and>
- (\<forall> t'< t.
- (\<exists> y. rec_calc_rel rec_nonstop [m, r, t'] y \<and>
- y \<noteq> 0)))"
-apply(auto simp: rec_halt_def)
-apply(erule calc_mn_reverse, simp)
-apply(erule_tac calc_mn_reverse)
-apply(erule_tac x = t' in allE, simp)
-apply(rule_tac calc_mn, simp_all)
-done
+lemma primerec_terminate:
+ "\<lbrakk>primerec f x; length xs = x\<rbrakk> \<Longrightarrow> terminate f xs"
+proof(induct arbitrary: xs rule: primerec.induct)
+ fix xs
+ assume "length (xs::nat list) = Suc 0" thus "terminate z xs"
+ by(case_tac xs, auto intro: termi_z)
+next
+ fix xs
+ assume "length (xs::nat list) = Suc 0" thus "terminate 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"
+ 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"
+ 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
+ by simp
+ moreover have "\<forall>g\<in>set gs. terminate g xs"
+ using ind h
+ by(auto simp: set_conv_nth)
+ ultimately show "terminate (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"
+ 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])])"
+ using h
+ apply(auto)
+ by(rule_tac ind2, simp)
+ moreover have "terminate 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])"
+ by(rule_tac termi_pr, simp_all)
+ thus "terminate (Pr n f g) xs"
+ using h
+ by(case_tac "xs = []", auto)
+qed
text {*
The following lemma gives the correctness of @{text "rec_halt"}.
It says: if @{text "rec_halt"} calculates that the TM coded by @{text "m"}
will reach a standard final configuration after @{text "t"} steps of execution, then it is indeed so.
*}
-lemma halt_lemma:
- "rec_calc_rel (rec_halt) [m, r] t =
- (rec_exec rec_nonstop [m, r, t] = 0 \<and>
- (\<forall> t'< t. (\<exists> y. rec_exec rec_nonstop [m, r, t'] = y
- \<and> y \<noteq> 0)))"
-using halt_lemma'[of m r t]
-by simp
-
+
text {*F: universal machine*}
text {*
@@ -3370,11 +3143,6 @@
show "primerec (constn (Suc (Suc 0))) (Suc 0)" by auto
qed
-lemma [simp]: "rec_calc_rel rec_valu [r] rs =
- (rec_exec rec_valu [r] = rs)"
-apply(rule_tac prime_rel_exec_eq, auto)
-done
-
declare valu.simps[simp del]
text {*
@@ -3393,77 +3161,42 @@
done
lemma [simp]:
- "\<lbrakk>ys \<noteq> []; k < length ys\<rbrakk> \<Longrightarrow>
+ "\<lbrakk>ys \<noteq> [];
+ k < length ys\<rbrakk> \<Longrightarrow>
(get_fstn_args (length ys) (length ys) ! k) =
id (length ys) (k)"
by(erule_tac get_fstn_args_nth)
-lemma calc_rel_get_pren:
- "\<lbrakk>ys \<noteq> []; k < length ys\<rbrakk> \<Longrightarrow>
- rec_calc_rel (get_fstn_args (length ys) (length ys) ! k) ys
- (ys ! k)"
-apply(simp)
-apply(rule_tac calc_id, auto)
+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]"
+apply(simp add: rec_halt_def)
+apply(rule_tac termi_mn, auto)
+apply(rule_tac [!] primerec_terminate, auto)
done
-lemma [elim]:
- "\<lbrakk>xs \<noteq> []; k < Suc (length xs)\<rbrakk> \<Longrightarrow>
- rec_calc_rel (get_fstn_args (Suc (length xs))
- (Suc (length xs)) ! k) (m # xs) ((m # xs) ! k)"
-using calc_rel_get_pren[of "m#xs" k]
-apply(simp)
-done
text {*
The correctness of @{text "rec_F"}, halt case.
*}
-lemma F_lemma:
- "rec_calc_rel rec_halt [m, r] t \<Longrightarrow>
- rec_calc_rel rec_F [m, r] (valu (rght (conf m r t)))"
+
+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]"
apply(simp add: rec_F_def)
-apply(rule_tac rs = "[rght (conf m r t)]" in calc_cn,
- auto simp: value_lemma)
-apply(rule_tac rs = "[conf m r t]" in calc_cn,
- auto simp: right_lemma)
-apply(rule_tac rs = "[m, r, t]" in calc_cn, auto)
-apply(subgoal_tac " k = 0 \<or> k = Suc 0 \<or> k = Suc (Suc 0)",
- auto simp:nth_append)
-apply(rule_tac [1-2] calc_id, simp_all add: conf_lemma)
+apply(rule_tac termi_cn, auto)
+apply(rule_tac primerec_terminate, auto)
+apply(rule_tac termi_cn, auto)
+apply(rule_tac primerec_terminate, auto)
+apply(rule_tac termi_cn, auto)
+apply(rule_tac primerec_terminate, auto)
+apply(rule_tac [!] termi_id, auto)
done
-
text {*
The correctness of @{text "rec_F"}, nonhalt case.
*}
-lemma F_lemma2:
- "\<forall> t. \<not> rec_calc_rel rec_halt [m, r] t \<Longrightarrow>
- \<forall> rs. \<not> rec_calc_rel rec_F [m, r] rs"
-apply(auto simp: rec_F_def)
-apply(erule_tac calc_cn_reverse, simp (no_asm_use))+
-proof -
- fix rs rsa rsb rsc
- assume h:
- "\<forall>t. \<not> rec_calc_rel rec_halt [m, r] t"
- "length rsa = Suc 0"
- "rec_calc_rel rec_valu rsa rs"
- "length rsb = Suc 0"
- "rec_calc_rel rec_right rsb (rsa ! 0)"
- "length rsc = (Suc (Suc (Suc 0)))"
- "rec_calc_rel rec_conf rsc (rsb ! 0)"
- and g: "\<forall>k<Suc (Suc (Suc 0)). rec_calc_rel ([recf.id (Suc (Suc 0)) 0,
- recf.id (Suc (Suc 0)) (Suc 0), rec_halt] ! k) [m, r] (rsc ! k)"
- have "rec_calc_rel (rec_halt ) [m, r]
- (rsc ! (Suc (Suc 0)))"
- using g
- apply(erule_tac x = "(Suc (Suc 0))" in allE)
- apply(simp add:nth_append)
- done
- thus "False"
- using h
- apply(erule_tac x = "ysb ! (Suc (Suc 0))" in allE, simp)
- done
-qed
-
subsection {* Coding function of TMs *}
@@ -4860,10 +4593,26 @@
execution of of TMs.
*}
+lemma terminate_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>))]"
+apply(frule_tac halt_least_step, auto)
+thm terminate_halt_lemma
+apply(rule_tac t = stpa in terminate_halt_lemma)
+apply(simp_all add: nonstop_lemma, auto)
+done
+
+lemma terminate_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)
+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_calc_rel rec_F [code tp, (bl2wc (<lm>))] (rs - Suc 0)"
+ \<Longrightarrow> rec_exec 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]
@@ -4880,24 +4629,20 @@
using halt_state_keep[of "code tp" lm stpa stp]
by(simp)
moreover have g2:
- "rec_calc_rel rec_halt [code tp, (bl2wc (<lm>))] stpa"
+ "rec_exec rec_halt [code tp, (bl2wc (<lm>))] = stpa"
using h
- apply(simp add: halt_lemma nonstop_lemma, auto)
- done
+ by(auto simp: rec_exec.simps rec_halt_def nonstop_lemma intro!: Least_equality)
show
- "rec_calc_rel rec_F [code tp, (bl2wc (<lm>))] (rs - Suc 0)"
+ "rec_exec rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
proof -
have
- "rec_calc_rel rec_F [code tp, (bl2wc (<lm>))]
- (valu (rght (conf (code tp) (bl2wc (<lm>)) stpa)))"
- apply(rule F_lemma) using g2 h by auto
- moreover have
"valu (rght (conf (code tp) (bl2wc (<lm>)) stpa)) = rs - Suc 0"
using g1
apply(simp add: valu.simps trpl_code.simps
bl2wc.simps bl2nat_append lg_power)
done
- ultimately show "?thesis" by simp
+ thus "?thesis"
+ by(simp add: rec_exec.simps F_lemma g2)
qed
qed