--- a/thys/UTM.thy Thu Feb 07 01:00:55 2013 +0000
+++ b/thys/UTM.thy Thu Feb 07 03:01:51 2013 +0000
@@ -3648,11 +3648,11 @@
apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps)
done
-lemma [simp]: "fetch t_wcode_adjust (Suc (Suc (Suc (Suc 0)))) Bk = (L, 8)"
+lemma [simp]: "fetch t_wcode_adjust 4 Bk = (L, 8)"
apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_4_eq_4)
done
-lemma [simp]: "fetch t_wcode_adjust (Suc (Suc (Suc (Suc 0)))) Oc = (L, 5)"
+lemma [simp]: "fetch t_wcode_adjust 4 Oc = (L, 5)"
apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_4_eq_4)
done
@@ -4471,6 +4471,30 @@
declare numeral_2_eq_2[simp del]
+lemma [simp]: "wadjust_start m rs (c, Bk # list)
+ \<Longrightarrow> wadjust_start m rs (c, Oc # list)"
+apply(auto simp: wadjust_start.simps)
+done
+
+lemma [simp]: "wadjust_backto_standard_pos m rs (c, Bk # list)
+ \<Longrightarrow> wadjust_stop m rs (Bk # c, list)"
+apply(auto simp: wadjust_backto_standard_pos.simps
+wadjust_stop.simps wadjust_backto_standard_pos_B.simps)
+done
+
+lemma [simp]: "wadjust_start m rs (c, Oc # list)
+ \<Longrightarrow> wadjust_loop_start m rs (Oc # c, list)"
+apply(auto simp: wadjust_start.simps wadjust_loop_start.simps)
+apply(rule_tac x = ln in exI, simp)
+apply(rule_tac x = "rn" in exI, simp)
+apply(rule_tac x = 1 in exI, simp)
+done
+
+lemma [simp]:" wadjust_erase2 m rs (c, Oc # list)
+ \<Longrightarrow> wadjust_erase2 m rs (c, Bk # list)"
+apply(auto simp: wadjust_erase2.simps)
+done
+
lemma wadjust_correctness:
shows "let P = (\<lambda> (len, st, l, r). st = 0) in
let Q = (\<lambda> (len, st, l, r). wadjust_inv st m rs (l, r)) in
@@ -4491,9 +4515,10 @@
apply(rule_tac allI, rule_tac impI, case_tac "?f n", simp)
apply(simp add: step.simps)
apply(case_tac d, case_tac [2] aa, simp_all)
+ apply(simp_all only: wadjust_inv.simps split: if_splits)
+ apply(simp_all)
apply(simp_all add: wadjust_inv.simps wadjust_le_def
- abacus.lex_triple_def abacus.lex_pair_def lex_square_def numeral_4_eq_4
- split: if_splits)
+ abacus.lex_triple_def abacus.lex_pair_def lex_square_def split: if_splits)
done
next
show "?Q (?f 0)"
@@ -4928,7 +4953,7 @@
text {*
The correctness of @{text "UTM"}, the halt case.
*}
-lemma UTM_halt_lemma:
+lemma UTM_halt_lemma':
assumes tm_wf: "tm_wf (tp, 0)"
and result: "0 < rs"
and args: "args \<noteq> []"
@@ -5291,7 +5316,7 @@
The correctness of @{text "UTM"}, the unhalt case.
*}
-lemma UTM_uhalt_lemma:
+lemma UTM_uhalt_lemma':
assumes tm_wf: "tm_wf (tp, 0)"
and unhalt: "\<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <args>) tp stp))"
and args: "args \<noteq> []"
@@ -5301,4 +5326,101 @@
apply(case_tac "rec_ci rec_F", simp)
done
+lemma UTM_halt_lemma:
+ assumes tm_wf: "tm_wf (p, 0)"
+ and resut: "rs > 0"
+ and args: "(args::nat list) \<noteq> []"
+ and exec: "{(\<lambda>tp. tp = (Bk\<up>i, <args>))} p {(\<lambda>tp. tp = (Bk\<up>m, Oc\<up>rs @ Bk\<up>k))}"
+ shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM {(\<lambda>tp. (\<exists> m n. tp = (Bk\<up>m, Oc\<up>rs @ Bk\<up>n)))}"
+proof -
+ have "{(\<lambda> (l, r). l = [] \<and> r = <code p # args>)} (t_wcode |+| t_utm)
+ {(\<lambda> (l, r). (\<exists> m. l = Bk\<up>m) \<and> (\<exists> n. r = Oc\<up>rs @ Bk\<up>n))}"
+ proof(rule_tac Hoare_plus_halt)
+ show "{\<lambda>(l, r). l = [] \<and> r = <code p # args>} t_wcode {\<lambda> (l, r). (l = [Bk] \<and>
+ (\<exists> rn. r = Oc\<up>(Suc (code p)) @ Bk # Oc\<up>(Suc (bl_bin (<args>))) @ Bk\<up>(rn)))}"
+ apply(rule_tac Hoare_haltI, auto)
+ using wcode_lemma_1[of args "code p"] args
+ apply(auto)
+ apply(rule_tac x = stp in exI, simp)
+ done
+ next
+ have "\<exists> stp. steps0 (Suc 0, Bk\<up>i, <args>) p stp = (0, Bk\<up>m, Oc\<up>rs @ Bk\<up>k)"
+ using exec
+ apply(simp add: Hoare_halt_def, auto)
+ apply(case_tac "steps0 (Suc 0, Bk \<up> i, <args>) p n", simp)
+ apply(rule_tac x = n in exI, simp)
+ done
+ then obtain stp where k: "steps0 (Suc 0, Bk\<up>i, <args>) p stp = (0, Bk\<up>m, Oc\<up>rs @ Bk\<up>k)"
+ ..
+ thus "{\<lambda>(l, r). l = [Bk] \<and> (\<exists>rn. r = Oc \<up> Suc (code p) @ Bk # Oc \<up> Suc (bl_bin (<args>)) @ Bk \<up> rn)}
+ t_utm {\<lambda>(l, r). (\<exists>m. l = Bk \<up> m) \<and> (\<exists>n. r = Oc \<up> rs @ Bk \<up> n)}"
+ proof(rule_tac Hoare_haltI, auto)
+ fix rn
+ show "\<exists>n. is_final (steps0 (Suc 0, [Bk], Oc \<up> Suc (code p) @ Bk # Oc \<up> Suc (bl_bin (<args>)) @ Bk \<up> rn) t_utm n) \<and>
+ (\<lambda>(l, r). (\<exists>m. l = Bk \<up> m) \<and> (\<exists>n. r = Oc \<up> rs @ Bk \<up> n)) holds_for steps0
+ (Suc 0, [Bk], Oc \<up> Suc (code p) @ Bk # Oc \<up> Suc (bl_bin (<args>)) @ Bk \<up> rn) t_utm n"
+ using t_utm_halt_eq[of p i "args" stp m rs k rn] assms k
+ apply(auto simp: bin_wc_eq, auto)
+ apply(rule_tac x = stpa in exI, simp add: tape_of_nl_abv tape_of_nat_abv)
+ done
+ qed
+ next
+ show "tm_wf0 t_wcode" by auto
+ qed
+ thus "?thesis"
+ apply(case_tac "rec_ci rec_F")
+ apply(simp add: UTM_def t_utm_def F_aprog_def F_tprog_def)
+ apply(auto simp add: Hoare_halt_def)
+ apply(rule_tac x="n" in exI)
+ apply(auto)
+ apply(case_tac "(steps0 (Suc 0, [], <code p # args>)
+ (t_wcode |+| ((tm_of (a [+] dummy_abc (Suc (Suc 0)))) @
+ shift (mopup (Suc (Suc 0)))
+ (length (tm_of (a [+] dummy_abc (Suc (Suc 0)))) div
+ 2))) n)")
+ apply(simp)
+ done
+qed
+
+lemma UTM_halt_lemma2:
+ assumes tm_wf: "tm_wf (p, 0)"
+ and args: "(args::nat list) \<noteq> []"
+ and exec: "{(\<lambda>tp. tp = ([], <args>))} p {(\<lambda>tp. tp = (Bk\<up>m, <(n::nat)> @ Bk\<up>k))}"
+ shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM {(\<lambda>tp. (\<exists> m k. tp = (Bk\<up>m, <n> @ Bk\<up>k)))}"
+using UTM_halt_lemma[OF assms(1) _ assms(2), where i="0"]
+using assms(3)
+apply(simp add: tape_of_nat_abv)
+done
+
+
+lemma UTM_unhalt_lemma:
+ assumes tm_wf: "tm_wf (p, 0)"
+ and unhalt: "{(\<lambda>tp. tp = (Bk\<up>i, <args>))} p \<up>"
+ and args: "args \<noteq> []"
+ shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM \<up>"
+proof -
+ have "\<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(i), <args>) p stp))"
+ using unhalt
+ apply(auto simp: Hoare_unhalt_def)
+ apply(case_tac "steps0 (Suc 0, Bk \<up> i, <args>) p stp", simp)
+ apply(erule_tac x = stp in allE, simp add: TSTD_def)
+ done
+ then have "\<forall> stp. \<not> is_final (steps0 (Suc 0, [], <code p # args>) UTM stp)"
+ using assms
+ apply(rule_tac UTM_uhalt_lemma', simp_all)
+ done
+ thus "?thesis"
+ apply(simp add: Hoare_unhalt_def)
+ done
+qed
+
+lemma UTM_unhalt_lemma2:
+ assumes tm_wf: "tm_wf (p, 0)"
+ and unhalt: "{(\<lambda>tp. tp = ([], <args>))} p \<up>"
+ and args: "args \<noteq> []"
+ shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM \<up>"
+using UTM_unhalt_lemma[OF assms(1), where i="0"]
+using assms(2-3)
+apply(simp add: tape_of_nat_abv)
+done
end
\ No newline at end of file