
diff -r 8a3e63163910 -r 582916f289ea thys/Abacus.thy
--- a/thys/Abacus.thy	Sun Feb 10 20:56:08 2013 +0000
+++ b/thys/Abacus.thy	Mon Feb 11 00:08:54 2013 +0000
@@ -1,60 +1,26 @@
-header {* 
- {\em abacus} a kind of register machine
-*}
-
 theory Abacus
 imports Uncomputable
 begin
 
-(*
-declare tm_comp.simps [simp add] 
-declare adjust.simps[simp add] 
-declare shift.simps[simp add]
-declare tm_wf.simps[simp add]
-declare step.simps[simp add]
-declare steps.simps[simp add]
-*)
 declare replicate_Suc[simp add]
 
-text {*
-  {\em Abacus} instructions:
-*}
+(* Abacus instructions *)
 
 datatype abc_inst =
-  -- {* @{text "Inc n"} increments the memory cell (or register) with address @{text "n"} by one.
-     *}
      Inc nat
-  -- {*
-     @{text "Dec n label"} decrements the memory cell with address @{text "n"} by one. 
-      If cell @{text "n"} is already zero, no decrements happens and the executio jumps to
-      the instruction labeled by @{text "label"}.
-     *}
    | Dec nat nat
-  -- {*
-  @{text "Goto label"} unconditionally jumps to the instruction labeled by @{text "label"}.
-  *}
    | Goto nat
   
-
-text {*
-  Abacus programs are defined as lists of Abacus instructions.
-*}
 type_synonym abc_prog = "abc_inst list"
 
-section {*
-  Sample Abacus programs
-  *}
-
-text {*
-  Abacus for addition and clearance.
-*}
+section {* Some Sample Abacus programs *}
+
+(* Abacus for addition and clearance *)
 fun plus_clear :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"  
   where
   "plus_clear m n e = [Dec m e, Inc n, Goto 0]"
 
-text {*
-  Abacus for clearing memory untis.
-*}
+(* Abacus for clearing memory untis *)
 fun clear :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
   where
   "clear n e = [Dec n e, Goto 0]"
@@ -72,17 +38,8 @@
   where
   "expo n m1 m2 p e = [Inc n, Dec m1 e] @ mult m2 n n p 2"
 
-
-text {*
-  The state of Abacus machine.
-  *}
 type_synonym abc_state = nat
 
-(* text {*
-  The memory of Abacus machine is defined as a function from address to contents.
-*}
-type_synonym abc_mem = "nat \<Rightarrow> nat" *)
-
 text {*
   The memory of Abacus machine is defined as a list of contents, with 
   every units addressed by index into the list.
@@ -312,33 +269,16 @@
 fun tm_of :: "abc_prog \<Rightarrow> instr list"
   where "tm_of ap = concat (tms_of ap)"
 
-text {*
-  The following two functions specify the well-formedness of complied TM.
-*}
-(*
-fun t_ncorrect :: "tprog \<Rightarrow> bool"
-  where
-  "t_ncorrect tp = (length tp mod 2 = 0)"
-
-fun abc2t_correct :: "abc_prog \<Rightarrow> bool"
-  where 
-  "abc2t_correct ap = list_all (\<lambda> (n, tm). 
-             t_ncorrect (ci (layout_of ap) n tm)) (tpairs_of ap)"
-*)
-
 lemma length_findnth: 
   "length (findnth n) = 4 * n"
-apply(induct n, auto)
-done
+by (induct n, auto)
 
 lemma ci_length : "length (ci ns n ai) div 2 = length_of ai"
 apply(auto simp: ci.simps tinc_b_def tdec_b_def length_findnth
                  split: abc_inst.splits)
 done
 
-subsection {*
-  Representation of Abacus memory by TM tape
-*}
+subsection {* Representation of Abacus memory by TM tapes *}
 
 text {*
   @{text "crsp acf tcf"} meams the abacus configuration @{text "acf"}
@@ -353,28 +293,6 @@
 
 declare crsp.simps[simp del]
 
-subsection {*
-  A more general definition of TM execution. 
-*}
-
-(*
-fun nnth_of :: "(taction \<times> nat) list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (taction \<times> nat)"
-  where
-  "nnth_of p s b = (if 2*s < length p 
-                    then (p ! (2*s + b)) else (Nop, 0))"
-
-thm nth_of.simps
-
-fun nfetch :: "tprog \<Rightarrow> nat \<Rightarrow> block \<Rightarrow> taction \<times> nat"
-  where
-  "nfetch p 0 b = (Nop, 0)" |
-  "nfetch p (Suc s) b = 
-             (case b of 
-                Bk \<Rightarrow> nnth_of p s 0 |
-                Oc \<Rightarrow> nnth_of p s 1)"
-*)
-
-                    
 text {*
   The type of invarints expressing correspondence between 
   Abacus configuration and TM configuration.
@@ -388,10 +306,6 @@
         ci.simps [simp del] length_of.simps[simp del] 
         layout_of.simps[simp del]
 
-(*
-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.
@@ -2327,29 +2241,6 @@
       else l = Oc\<up>ml @ Bk # <rev lm1> @ Bk # Bk # ires) \<and> 
      (r = Oc\<up>mr @ [Bk] @ <lm2>@ Bk\<up>rn \<or> (lm2 = [] \<and> r = Oc\<up>mr))
   )"
-(*
-fun dec_inv_1 :: "layout \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> dec_inv_t"
-  where
-  "dec_inv_1 ly n e (as, am) (s, l, r) ires = 
-           (let ss = start_of ly as in
-            let am' = abc_lm_s am n (abc_lm_v am n - Suc 0) in
-            let am'' = abc_lm_s am n (abc_lm_v am n) in
-              if s = start_of ly e then inv_stop (as, am'') (s, l, r) ires
-              else if s = ss then False
-              else if s = ss + 2 * n then 
-                  inv_locate_a (as, am) (n, l, r) ires
-                \<or> inv_locate_a (as, am'') (n, l, r) ires
-              else if s = ss + 2 * n + 1 then 
-                  inv_locate_b (as, am) (n, l, r) ires
-              else if s = ss + 2 * n + 13 then 
-                  inv_on_left_moving (as, am'') (s, l, r) ires
-              else if s = ss + 2 * n + 14 then 
-                  inv_check_left_moving (as, am'') (s, l, r) ires
-              else if s = ss + 2 * n + 15 then 
-                  inv_after_left_moving (as, am'') (s, l, r) ires
-              else False)"
-*)
-
 
 fun dec_inv_1 :: "layout \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> dec_inv_t"
   where
@@ -2832,50 +2723,6 @@
 apply(auto simp: inv_locate_b.simps in_middle.simps split: if_splits)
 done
 
-(*
-
-lemma  inv_locate_b_2_on_left_moving_b[simp]: 
-   "inv_locate_b (as, am) (n, l, []) ires
-     \<Longrightarrow> inv_on_left_moving (as, 
-                  abc_lm_s am n (abc_lm_v am n)) (s, [], [Bk]) ires"
-apply(auto simp: inv_locate_b.simps inv_on_left_moving.simps inv_on_left_moving_in_middle_B.simps
-                 in_middle.simps split: if_splits)
-apply(drule_tac length_equal, simp)
-
-apply(insert inv_locate_b_2_on_left_moving[of as am n l "[]" ires s])
-apply(simp only: inv_on_left_moving.simps, simp)
-apply(subgoal_tac "\<not> inv_on_left_moving_in_middle_B 
-         (as, abc_lm_s am n (abc_lm_v am n)) (s, tl l, [hd l]) ires", simp)
-*)
-
-(*
-lemma [simp]:
-  "inv_locate_b (as, am) (n, l, []) ires; l \<noteq> []\<rbrakk>
- \<Longrightarrow> inv_on_left_moving (as, abc_lm_s am n 
-                  (abc_lm_v am n)) (s, tl l, [hd l]) ires"
-apply(auto simp: inv_locate_b.simps inv_on_left_moving.simps inv_on_left_moving_in_middle_B.simps
-                 in_middle.simps split: if_splits)
-apply(drule_tac length_equal, simp)
-
-apply(insert inv_locate_b_2_on_left_moving[of as am n l "[]" ires s])
-apply(simp only: inv_on_left_moving.simps, simp)
-apply(subgoal_tac "\<not> inv_on_left_moving_in_middle_B 
-         (as, abc_lm_s am n (abc_lm_v am n)) (s, tl l, [hd l]) ires", simp)
-
-apply(insert inv_locate_b_2_on_left_moving[of as am n l "[]" ires s])
-apply(simp only: inv_on_left_moving.simps, simp)
-apply(subgoal_tac "\<not> inv_on_left_moving_in_middle_B 
-         (as, abc_lm_s am n (abc_lm_v am n)) (s, tl l, [hd l]) ires", simp)
-apply(simp only: inv_on_left_moving_norm.simps)
-apply(erule_tac exE)+
-apply(erule_tac conjE)+
-apply(rule_tac x = lm1 in exI, rule_tac x = lm2 in exI, 
-      rule_tac x = m in exI, rule_tac x = ml in exI, 
-      rule_tac x = mr in exI, simp)
-apply(case_tac mr, simp, simp, case_tac nat, auto intro: nil_2_nil)
-done
-*)
-
 lemma [simp]: 
  "\<lbrakk>dec_first_on_right_moving n (as, am) (s, aaa, Oc # xs) ires\<rbrakk>
    \<Longrightarrow> dec_first_on_right_moving n (as, am) (s', Oc # aaa, xs) ires"
@@ -3051,14 +2898,6 @@
 apply(auto simp: dec_left_move.simps inv_on_left_moving.simps split: if_splits)
 done
 
-(*
-lemma [simp]: "inv_on_left_moving_in_middle_B (as, lm1 @ [m]) 
-                        (s', Oc # Oc\<^bsup>m\<^esup> @ Bk # <rev lm1> @ Bk\<^bsup>ln\<^esup>, [Bk])  ires"
-apply(auto simp: inv_on_left_moving_in_middle_B.simps)
-apply(rule_tac x = "lm1 @ [m]" in exI, rule_tac x = "[]" in exI, auto)
-done
-*)
-
 lemma [simp]: "dec_left_move (as, am) (s, l, []) ires
              \<Longrightarrow> inv_on_left_moving (as, am) (s', tl l, [hd l]) ires"
 apply(auto simp: dec_left_move.simps inv_on_left_moving.simps split: if_splits)
@@ -3848,33 +3687,6 @@
   and crsp: "crsp ly (as, lm) (s, l, r) ires"
   shows "\<exists> stp. crsp ly (abc_steps_l (as, lm) ap n)
                       (steps (s, l, r) (tp, 0) stp) ires"
-(*
-proof(induct n)
-  case 0
-  have "crsp ly (abc_steps_l (as, lm) ap 0) (steps (s, l, r) (tp, 0) 0) ires"
-    using crsp by(simp add: steps.simps abc_steps_l.simps)
-  thus "?case"
-    by(rule_tac x = 0 in exI, simp)
-next
-  case (Suc n)
-  obtain as' lm' where a: "abc_steps_l (as, lm) ap n = (as', lm')"
-    by(case_tac "abc_steps_l (as, lm) ap n", auto) 
-  have "\<exists>stp\<ge>n. crsp ly (abc_steps_l (as, lm) ap n) (steps (s, l, r) (tp, 0) stp) ires"
-    by fact
-  from this a obtain stpa where b:
-    "stpa\<ge>n \<and> crsp ly (as', lm') (steps (s, l, r) (tp, 0) stpa) ires" by auto
-  obtain s' l' r' where "steps (s, l, r) (tp, 0) stpa = (s', l', r')"
-    by(case_tac "steps (s, l, r) (tp, 0) stpa")
-  then have "stpa\<ge>n \<and> crsp ly (as', lm') (s', l', r') ires" using b by simp
-  from a and this show "?case"
-  proof(cases "abc_fetch as' ap")
-    case None
-    
-  
-
-    have "crsp ly (abc_steps_l (as, lm) ap 0) (steps (s, l, r) (tp, 0) stp) ires"
-    apply(simp add: steps.simps abc_steps_l.simps)
-*)
   using crsp
   apply(induct n)
   apply(rule_tac x = 0 in exI) 
@@ -3970,43 +3782,7 @@
 apply(case_tac b)
 apply(simp_all add: start_of.simps fetch.simps nth_append)
 done
-(*
-lemma tp_correct: 
-  assumes layout: "ly = layout_of ap"
-  and compile: "tp = tm_of ap"
-  and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires"
-  and abc_halt: "abc_steps_l (0, lm) ap stp = (length ap, am)"
-  shows "\<exists> stp k. steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp = (0, Bk # Bk # ires, <am> @ Bk\<up>k)"
-  using assms
-proof -
-  have "\<exists> stp k. steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp =
-    (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)"
-  proof -
-    have "\<exists> stp k. steps (Suc 0, l, r) (tp, 0) stp =
-    (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)"
-      using assms
-      apply(rule_tac tp_correct', simp_all)
-      done
-    from this obtain stp k where "steps (Suc 0, l, r) (tp, 0) stp =
-    (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)" by blast
-    thus "?thesis"
-      apply(rule_tac x = stp in exI, rule_tac x = k in exI)
-      apply(drule_tac tm_append_first_steps_eq, simp_all)
-      done
-  qed
-  from this obtain stp k where 
-    "steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp =
-    (start_of ly (length ap), Bk # Bk # ires, <am> @ Bk\<up>k)"
-    by blast
-  thus "\<exists>stp k. steps (Suc 0, l, r) (tp @ [(Nop, 0), (Nop, 0)], 0) stp 
-    = (0, Bk # Bk # ires, <am> @ Bk \<up> k)"
-    using assms
-    apply(rule_tac x = "stp + Suc 0" in exI)
-    apply(simp add: steps_add)
-    apply(auto simp: step.simps)
-    done
-qed
- *)   
+
 (********for mopup***********)
 fun mopup_a :: "nat \<Rightarrow> instr list"
   where




