regexp: comparison utm/abacus.thy

equal deleted inserted replaced

-:1ce04eb1c8ad
+:48b231495281
 header {*
-{\em Abacus} (a kind of register machine)
+{\em abacus} a kind of register machine
 *}
 theory abacus
 imports Main turing_basic
 begin
 apply(simp add: tms_of.simps tpairs_of.simps)
 apply(simp add: tms_of.simps tpairs_of.simps abc_fetch.simps)
 apply(erule_tac t_split, auto simp: tm_of.simps)
 done
-subsubsection {* The compilation of @{text "Inc n"} *}
+(*
+subsection {* The compilation of @{text "Inc n"} *}
+*)
 text {*
 The lemmas in this section lead to the correctness of
 the compilation of @{text "Inc n"} instruction.
 *}
-(*****Begin: inc crsp*******)
 fun at_begin_fst_bwtn :: "inc_inv_t"
 where
 "at_begin_fst_bwtn (as, lm) (s, l, r) ires =
 (\<exists> lm1 tn rn. lm1 = (lm @ (0\<^bsup>tn\<^esup>)) \<and> length lm1 = s \<and>
 (if lm1 = [] then l = Bk # Bk # ires
 start_of ly as - Suc 0) stp) ires"
 proof -
 from inc_crsp_ex_pre [OF layout corresponds inc] show ?thesis .
 qed
-(*******End: inc crsp********)
+(*
+subsection {* The compilation of @{text "Dec n e"} *}
-(*******Begin: dec crsp******)
+*)
-subsubsection {* The compilation of @{text "Dec n e"} *}
 text {*
 The lemmas in this section lead to the correctness of the compilation
 of @{text "Dec n e"} instruction using the same techniques as
 @{text "Inc n"}.
 start_of ly as - Suc 0) stp) ires"
 proof -
 from dec_crsp_ex_pre layout dec correspond  show ?thesis by blast
 qed
+(*
-(*******End: dec crsp********)
+subsection {* Compilation of @{text "Goto n"}*}
+*)
-subsubsection {* Compilation of @{text "Goto n"}*}
-(*******Begin: goto crsp********)
 lemma goto_fetch:
 "fetch (ci (layout_of aprog)
 (start_of (layout_of aprog) as) (Goto n)) (Suc 0)  b
 = (Nop, start_of (layout_of aprog) n)"
 apply(auto simp: ci.simps fetch.simps nth_of.simps
 (t_steps tc (ci (layout_of aprog) (start_of ly as) (Goto n),
 start_of ly as - Suc 0) stp) ires"
 proof -
 from goto_crsp_ex_pre and layout goto correspondence show "?thesis" by blast
 qed
-(*******End : goto crsp*********)
+subsection {*
-subsubsection {*
 The correctness of the compiler
 *}
 declare abc_step_l.simps[simp del]
 shows "(\<exists> n'. crsp_l ly ac' (t_steps tc (tprog, 0) n') ires)"
 proof -
 from steps_crsp_pre [OF layout compiled correspond execution] show ?thesis .
 qed
+subsection {* The Mop-up machine *}
-subsubsection {* The Mop-up machine *}
 fun mop_bef :: "nat \<Rightarrow> tprog"
 where
 "mop_bef 0 = []" |
 "mop_bef (Suc n) = mop_bef n @
 apply(simp add: abc_lm_v.simps, auto)
 apply(case_tac list, simp_all add: tape_of_nl_abv tape_of_nat_list.simps abc_lm_v.simps)
 apply(erule_tac x = rn in allE, simp_all)
 done
-(***Begin: mopup stop***)
 fun abc_mopup_stage1 :: "t_conf \<Rightarrow> nat \<Rightarrow> nat"
 where
 "abc_mopup_stage1 (s, l, r) n =
 (if s > 0 \<and> s \<le> 2*n then 6
 else if s = 2*n + 1 then 4
 apply(rule_tac x = na in exI, case_tac "(t_steps (Suc 0, l, r)
 (mop_bef n @ tshift mp_up (2 * n), 0) na)", simp)
 apply(rule_tac mopup_init, auto)
 done
 (***End: mopup stop****)
-(*
-lemma mopup_stop_cond: "mopup_inv (0, l, r) lm n ires \<Longrightarrow>
-(\<exists>ln rn. ?l = Bk\<^bsup>ln\<^esup> @ Bk # Bk # ?ires \<and> ?r = <abc_lm_v ?lm ?n> @ Bk\<^bsup>rn\<^esup>) "
-t_halt_conf (0, l, r) \<and> t_result r = Suc (abc_lm_v lm n)"
-apply(simp add: mopup_inv.simps mopup_stop.simps t_halt_conf.simps
-t_result.simps, auto simp: tape_of_nat_abv)
-apply(rule_tac x = rn in exI,
-rule_tac x = "Suc (abc_lm_v lm n)" in exI,
-simp add: tape_of_nat_abv)
-apply(simp add: tape_of_nat_abv  exponent_def)
-apply(subgoal_tac "takeWhile (\<lambda>a. a = Oc)
-(replicate (abc_lm_v lm n) Oc @ replicate rn Bk)
-= replicate (abc_lm_v lm n) Oc @ takeWhile (\<lambda>a. a = Oc)
-(replicate rn Bk)", simp)
-apply(case_tac rn, simp, simp)
-apply(rule takeWhile_append2)
-apply(case_tac x, auto)
-done
-*)
 lemma mopup_halt_conf_pre:
 "\<lbrakk>n < length lm; crsp_l ly (as, lm) (s, l, r) ires\<rbrakk>
 \<Longrightarrow> \<exists> na. (\<lambda> (s', l', r').  s' = 0 \<and> mopup_stop (s', l', r') lm n ires)
 (t_steps (Suc 0, l, r)
 apply(rule_tac mopup_inv_steps, simp, simp)
 apply(rule_tac mopup_init, simp, simp)
 apply(rule_tac mopup_halt, simp, simp)
 done
-thm mopup_stop.simps
 lemma  mopup_halt_conf:
 assumes len: "n < length lm"
 and correspond: "crsp_l ly (as, lm) (s, l, r) ires"
 shows
-"\<exists> na. (\<lambda> (s', l', r'). ((\<exists>ln rn. s' = 0 \<and> l' = Bk\<^bsup>ln\<^esup> @ Bk # Bk # ires \<and> r' = Oc\<^bsup>Suc (abc_lm_v lm n)\<^esup> @ Bk\<^bsup>rn\<^esup>)))
+"\<exists> na. (\<lambda> (s', l', r'). ((\<exists>ln rn. s' = 0 \<and> l' = Bk\<^bsup>ln\<^esup> @ Bk # Bk # ires
+\<and> r' = Oc\<^bsup>Suc (abc_lm_v lm n)\<^esup> @ Bk\<^bsup>rn\<^esup>)))
 (t_steps (Suc 0, l, r)
 ((mop_bef n @ tshift mp_up (2 * n)), 0) na)"
 using len correspond mopup_halt_conf_pre[of n lm ly as s l r ires]
 apply(simp add: mopup_stop.simps tape_of_nat_abv tape_of_nat_list.simps)
 done
-(*********End: mop_up****************************)
+subsection {* Final results about Abacus machine *}
-subsubsection {* Final results about Abacus machine *}
-thm mopup_halt
 lemma mopup_halt_bef: "\<lbrakk>n < length lm; crsp_l ly (as, lm) (s, l, r) ires\<rbrakk>
 \<Longrightarrow> \<exists>stp. (\<lambda>(s, l, r). s \<noteq> 0 \<and> ((\<lambda> (s', l', r'). s' = 0)
 (t_step (s, l, r) (mop_bef n @ tshift mp_up (2 * n), 0))))
 (t_steps (Suc 0, l, r) (mop_bef n @ tshift mp_up (2 * n), 0) stp)"
 apply(insert mopup_halt[of n lm ly as s l r ires], simp, erule_tac exE)
 apply(subgoal_tac "start_of (layout_of aprog) (length aprog) > 0",
 case_tac "start_of (layout_of aprog) (length aprog)",
 simp, simp)
 apply(rule startof_not0, auto)
 done
-(*
-lemma stop_conf: "mopup_inv (0, aca, bc) am n
-\<Longrightarrow> t_halt_conf (0, aca, bc) \<and> t_result bc = Suc (abc_lm_v am n)"
-apply(case_tac n,
-auto simp: mopup_inv.simps mopup_stop.simps t_halt_conf.simps
-t_result.simps tape_of_nl_abv tape_of_nat_abv )
-apply(rule_tac x = "rn" in exI,
-rule_tac x = "Suc (abc_lm_v am 0)" in exI, simp)
-apply(subgoal_tac "takeWhile (\<lambda>a. a = Oc) (Oc\<^bsup>abc_lm_v am 0\<^esup> @ Bk\<^bsup>rn\<^esup>)
-= Oc\<^bsup>abc_lm_v am 0\<^esup> @ takeWhile (\<lambda>a. a = Oc) (Bk\<^bsup>rn\<^esup>)", simp)
-apply(simp add: exponent_def, case_tac rn, simp, simp)
-apply(rule_tac takeWhile_append2, simp add: exponent_def)
-apply(rule_tac x = rn in exI,
-rule_tac x = "Suc (abc_lm_v am (Suc nat))" in exI, simp)
-apply(subgoal_tac
-"takeWhile (\<lambda>a. a = Oc) (Oc\<^bsup>abc_lm_v am (Suc nat)\<^esup> @ Bk\<^bsup>rn\<^esup>) =
-Oc\<^bsup>abc_lm_v am (Suc nat)\<^esup> @ takeWhile (\<lambda>a. a = Oc) (Bk\<^bsup>rn\<^esup>)", simp)
-apply(simp add: exponent_def, case_tac rn, simp, simp)
-apply(rule_tac takeWhile_append2, simp add: exponent_def)
-done
-*)
 lemma start_of_out_range:
 "as \<ge> length aprog \<Longrightarrow>
 start_of (layout_of aprog) as =
 start_of (layout_of aprog) (length aprog)"
 -- {*
 After @{text "stp"} steps of execution of the TM composed of @{text "tprog"} and the mopup
 TM @{text "(tMp n (mop_ss - 1))"} will halt and gives rise to a configuration which
 only hold the content of memory cell @{text "n"}:
 *}
-"\<exists> stp. (\<lambda> (s, l, r). \<exists> ln rn. s = 0 \<and>  l = Bk\<^bsup>ln\<^esup> @ Bk # Bk # ires \<and> r = Oc\<^bsup>Suc (abc_lm_v am n)\<^esup> @ Bk\<^bsup>rn\<^esup>)
+"\<exists> stp. (\<lambda> (s, l, r). \<exists> ln rn. s = 0 \<and>  l = Bk\<^bsup>ln\<^esup> @ Bk # Bk # ires
+\<and> r = Oc\<^bsup>Suc (abc_lm_v am n)\<^esup> @ Bk\<^bsup>rn\<^esup>)
 (t_steps tc (tprog @ (tMp n (mop_ss - 1)), 0) stp)"
 proof -
 from layout complied correspond halt_state abc_exec rs_len mopup_start
 and abacus_turing_eq_halt_case_pre [of ly aprog tprog ac tc ires n am stp as mop_ss]
 show "?thesis"
 (t_steps tc (tprog @ (tMp n (mop_ss - 1)), 0) stp))"
 using layout compiled correspond abc_unhalt mopup_start
 apply(rule_tac abacus_turing_eq_unhalt_case_pre, auto)
 done
 definition abc_list_crsp:: "nat list \<Rightarrow> nat list \<Rightarrow> bool"
 where
 "abc_list_crsp xs ys = (\<exists> n. xs = ys @ 0\<^bsup>n\<^esup> \<or> ys = xs @ 0\<^bsup>n\<^esup>)"
 lemma [intro]: "abc_list_crsp (lm @ 0\<^bsup>m\<^esup>) lm"
 apply(auto simp: abc_list_crsp_def)
 done
-thm abc_lm_v.simps
 lemma abc_list_crsp_lm_v:
 "abc_list_crsp lma lmb \<Longrightarrow> abc_lm_v lma n = abc_lm_v lmb n"
 apply(auto simp: abc_list_crsp_def abc_lm_v.simps
 nth_append exponent_def)
 done
 apply(case_tac i, auto simp: abc_step_l.simps
 abc_list_crsp_lm_s abc_list_crsp_lm_v Let_def
 split: abc_inst.splits if_splits)
 done
-thm abc_step_l.simps
 lemma abc_steps_red:
 "abc_steps_l ac aprog stp = (as, am) \<Longrightarrow>
 abc_steps_l ac aprog (Suc stp) =
 abc_step_l (as, am) (abc_fetch as aprog)"
 using abc_steps_ind[of ac aprog stp]
 case_tac "abc_step_l (aa, lma) (abc_fetch aa aprog)", simp)
 apply(rule_tac abc_list_crsp_step, auto)
 done
 qed
-text {* Begin: equvilence between steps and t_steps*}
 lemma [simp]: "(case ca of [] \<Rightarrow> Bk | Bk # xs \<Rightarrow> Bk | Oc # xs \<Rightarrow> Oc) =
 (case ca of [] \<Rightarrow> Bk | x # xs \<Rightarrow> x)"
 by(case_tac ca, simp_all, case_tac a, simp, simp)
-text {* needed to interpret*}
 lemma steps_eq: "length t mod 2 = 0 \<Longrightarrow>
 t_steps c (t, 0) stp = steps c t stp"
 apply(induct stp)
 apply(simp add: steps.simps t_steps.simps)
 apply(simp add:tstep_red t_steps_ind)
 apply(case_tac "steps c t stp", simp)
 apply(auto simp: t_step.simps tstep.simps)
 done
-text{* end: equvilence between steps and t_steps*}
 lemma crsp_l_start: "crsp_l ly (0, lm) (Suc 0, Bk # Bk # ires, <lm> @ Bk\<^bsup>rn\<^esup>) ires"
 apply(simp add: crsp_l.simps, auto simp: start_of.simps)
 done
 apply(rule_tac x = stpa in exI,
 simp add:  exponent_def, auto)
 done
-thm tinres_steps
 lemma list_length: "xs = ys \<Longrightarrow> length xs = length ys"
 by simp
 lemma [elim]: "tinres (Bk\<^bsup>m\<^esup>) b \<Longrightarrow> \<exists>m. b = Bk\<^bsup>m\<^esup>"
 apply(auto simp: tinres_def)
 apply(rule_tac x = "m-n" in exI,
 text {*
 Main theorem for the case when the original Abacus program does halt.
 *}
 lemma abacus_turing_eq_halt:
 assumes layout:
 "ly = layout_of aprog"
 -- {* There is an Abacus program @{text "aprog"} with layout @{text "ly"}: *}
 and compiled: "tprog = tm_of aprog"
 apply(subgoal_tac
 "length (tm_of aprog @ tMp n
 (start_of ly (length aprog) - Suc 0)) mod 2 = 0")
 apply(simp add: steps_eq, auto simp: isS0_def)
 done
-(*
-lemma abacus_turing_eq_uhalt_pre:
-"\<lbrakk>ly = layout_of aprog;
-tprog = tm_of aprog;
-\<forall> stp. ((\<lambda> (as, am). as < length aprog)
-(abc_steps_l (0, lm) aprog stp));
-mop_ss = start_of ly (length aprog)\<rbrakk>
-\<Longrightarrow> (\<not> (\<exists> stp. isS0 (steps (Suc 0, [Bk, Bk], <lm>)
-(tprog @ (tMp n (mop_ss - 1))) stp)))"
-apply(drule_tac k = 0 and n = n  in abacus_turing_eq_uhalt', auto)
-apply(erule_tac x = stp in allE, erule_tac x = stp in allE)
-apply(subgoal_tac "tinres ([Bk]) (Bk\<^bsup>k\<^esup>)")
-apply(case_tac "steps (Suc 0, Bk\<^bsup>k\<^esup>, <lm>)
-(tm_of aprog @ tMp n (start_of ly (length aprog) - Suc 0)) stp")
-apply(case_tac
-"steps (Suc 0, [Bk], <lm>)
-(tm_of aprog @ tMp n (start_of ly (length aprog) - Suc 0)) stp")
-apply(drule_tac tinres_steps, auto simp: isS0_def)
-done
-*)
 text {*
 Main theorem for the case when the original Abacus program does not halt.
 *}
 lemma abacus_turing_eq_uhalt:
 assumes layout:
 (tprog @ (tMp n (mop_ss - 1))) stp))"
 using abacus_turing_eq_uhalt'
 layout compiled abc_unhalt mop_start
 by(auto)
 end

changeset 371	48b231495281
parent 370	1ce04eb1c8ad