Mercurial Mercurial > hg > tm / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys2/UF_Rec.thy
changeset 263 aa102c182132
parent 262 5704925ad138
child 264 bc2df9620f26
equal deleted inserted replaced
262:5704925ad138 263:aa102c182132 
   109                       else if a = 2 then penc (Suc (Read l)) r
 
   109                       else if a = 2 then penc (Suc (Read l)) r
 
   110                       else if a = 3 then pdec2 r
 
   110                       else if a = 3 then pdec2 r
 
   111                       else r)"
 
   111                       else r)"
 
   112 
   112 
   113 text {*
 
   113 text {*
 
   114   The @{text "Actn"} function given on page 92 of B book, which is used to 
   114   The @{text "Action"} function given on page 92 of B book, which is used to 
   115   fetch Turing Machine intructions. In @{text "Actn m q r"}, @{text "m"} is 
   115   fetch Turing Machine intructions. In @{text "Action m q r"}, @{text "m"} is 
   116   the code of the Turing Machine, @{text "q"} is the current state of 
   116   the code of the Turing Machine, @{text "q"} is the current state of 
   117   Turing Machine, and @{text "r"} is the scanned cell of is the right tape. 
   117   Turing Machine, and @{text "r"} is the scanned cell of is the right tape. 
   118 *}
 
   118 *}
 
   119 
   119 
   120 fun actn :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
 
   120 fun Actn :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
 
   121   "actn n 0 = pdec1 (pdec1 n)"
 
   121   "Actn n 0 = pdec1 (pdec1 n)"
 
   122 | "actn n _ = pdec1 (pdec2 n)"
 
   122 | "Actn n _ = pdec1 (pdec2 n)"
 
   123 
   123 
   124 fun Actn :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
 
   124 fun Action :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
 
   125   where
 
   125   where
 
   126   "Actn m q r = (if q \<noteq> 0 \<and> within m (q - 1) then (actn (ldec m (q - 1)) r) else 4)"
 
   126   "Action m q c = (if q \<noteq> 0 \<and> within m (q - 1) then Actn (ldec m (q - 1)) c else 4)"
 
   127 
   127 
   128 fun newstate :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
 
   128 fun Newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
 
   129   "newstate n 0 = pdec2 (pdec1 n)"
 
   129   "Newstat n 0 = pdec2 (pdec1 n)"
 
   130 | "newstate n _ = pdec2 (pdec2 n)"
 
   130 | "Newstat n _ = pdec2 (pdec2 n)"
 
   131 
   131 
   132 fun Newstate :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
 
   132 fun Newstate :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
 
   133   where
 
   133   where
 
   134   "Newstate m q r = (if q \<noteq> 0 then (newstate (ldec m (q - 1)) r) else 0)"
 
   134   "Newstate m q r = (if q \<noteq> 0 then Newstat (ldec m (q - 1)) r else 0)"
 
   135 
   135 
   136 fun Conf :: "nat \<times> (nat \<times> nat) \<Rightarrow> nat"
 
   136 fun Conf :: "nat \<times> (nat \<times> nat) \<Rightarrow> nat"
 
   137   where
 
   137   where
 
   138   "Conf (q, l, r) = lenc [q, l, r]"
 
   138   "Conf (q, l, r) = lenc [q, l, r]"
 
   139 
   139 
   147   "Right cf = ldec cf 2"
 
   147   "Right cf = ldec cf 2"
 
   148 
   148 
   149 fun Step :: "nat \<Rightarrow> nat \<Rightarrow> nat"
 
   149 fun Step :: "nat \<Rightarrow> nat \<Rightarrow> nat"
 
   150   where
 
   150   where
 
   151   "Step cf m = Conf (Newstate m (State cf) (Read (Right cf)), 
   151   "Step cf m = Conf (Newstate m (State cf) (Read (Right cf)), 
   152                      Newleft (Left cf) (Right cf) (Actn m (State cf) (Read (Right cf))),
 
   152                      Newleft (Left cf) (Right cf) (Action m (State cf) (Read (Right cf))),
 
   153                      Newright (Left cf) (Right cf) (Actn m (State cf) (Read (Right cf))))"
 
   153                      Newright (Left cf) (Right cf) (Action m (State cf) (Read (Right cf))))"
 
   154 
   154 
   155 text {*
 
   155 text {*
 
   156   @{text "Steps cf m k"} computes the TM configuration after @{text "k"} steps of execution
 
   156   @{text "Steps cf m k"} computes the TM configuration after @{text "k"} steps of execution
 
   157   of TM coded as @{text "m"}. 
   157   of TM coded as @{text "m"}. 
   158 *}
 
   158 *}
 
   345 apply(induct tp st c rule: fetch.induct)
 
   345 apply(induct tp st c rule: fetch.induct)
 
   346 apply(simp_all add: list_encode_inverse split: cell.split)
 
   346 apply(simp_all add: list_encode_inverse split: cell.split)
 
   347 done
 
   347 done
 
   348 
   348 
   349 lemma Fetch_action_simulate:
 
   349 lemma Fetch_action_simulate:
 
   350   "tm_wf tp \<Longrightarrow> Actn (Code_tprog tp) st (cell_num c) = action_num (fst (fetch tp st c))"
 
   350   "tm_wf tp \<Longrightarrow> Action (Code_tprog tp) st (cell_num c) = action_num (fst (fetch tp st c))"
 
   351 apply(induct tp st c rule: fetch.induct)
 
   351 apply(induct tp st c rule: fetch.induct)
 
   352 apply(simp_all add: list_encode_inverse split: cell.split)
 
   352 apply(simp_all add: list_encode_inverse split: cell.split)
 
   353 done
 
   353 done
 
   354 
   354 
   355 lemma Read_simulate:
 
   355 lemma Read_simulate:
 
   463 
   463 
   464 lemma write_lemma [simp]:
 
   464 lemma write_lemma [simp]:
 
   465   "rec_eval rec_write [x, y] = Write x y"
 
   465   "rec_eval rec_write [x, y] = Write x y"
 
   466 by (simp add: rec_write_def)
 
   466 by (simp add: rec_write_def)
 
   467 
   467 
   468 
       
   469 
       
   470 
       
   471 definition
 
   468 definition
 
   472     "rec_newleft =
 
   469     "rec_newleft =
 
   473        (let cond1 = CN rec_disj [CN rec_eq [Id 3 2, Z], CN rec_eq [Id 3 2, constn 1]] in
 
   470        (let cond0 = CN rec_eq [Id 3 2, constn 0] in 
       
   471         let cond1 = CN rec_eq [Id 3 2, constn 1] in
 
   474         let cond2 = CN rec_eq [Id 3 2, constn 2] in
 
   472         let cond2 = CN rec_eq [Id 3 2, constn 2] in
 
   475         let cond3 = CN rec_eq [Id 3 2, constn 3] in
 
   473         let cond3 = CN rec_eq [Id 3 2, constn 3] in
 
   476         let case3 = CN rec_add [CN rec_mult [constn 2, Id 3 0], 
   474         let case3 = CN rec_penc [CN S [CN rec_read [Id 3 1]], Id 3 0] in
 
   477                                 CN rec_mod [Id 3 1, constn 2]] in
 
   475         CN rec_if [cond0, Id 3 0,
 
   478         CN rec_if [cond1, Id 3 0, 
   476           CN rec_if [cond1, Id 3 0,  
   479           CN rec_if [cond2, CN rec_quo [Id 3 0, constn 2],
 
   477             CN rec_if [cond2, CN rec_pdec2 [Id 3 0],
 
   480             CN rec_if [cond3, case3, Id 3 0]]])"
 
   478               CN rec_if [cond3, case3, Id 3 0]]]])"
 
   481 
   479 
   482 definition
 
   480 definition
 
   483     "rec_newright =
 
   481     "rec_newright =
 
   484        (let condn = \<lambda>n. CN rec_eq [Id 3 2, constn n] in
 
   482        (let cond0 = CN rec_eq [Id 3 2, constn 0] in
 
   485         let case0 = CN rec_minus [Id 3 1, CN rec_scan [Id 3 1]] in
 
   483         let cond1 = CN rec_eq [Id 3 2, constn 1] in
 
   486         let case1 = CN rec_minus [CN rec_add [Id 3 1, constn 1], CN rec_scan [Id 3 1]] in
 
   484         let cond2 = CN rec_eq [Id 3 2, constn 2] in
 
   487         let case2 = CN rec_add [CN rec_mult [constn 2, Id 3 1],                     
   485         let cond3 = CN rec_eq [Id 3 2, constn 3] in
 
   488                                 CN rec_mod [Id 3 0, constn 2]] in
 
   486         let case2 = CN rec_penc [CN S [CN rec_read [Id 3 0]], Id 3 1] in
 
   489         let case3 = CN rec_quo [Id 2 1, constn 2] in
 
   487         CN rec_if [cond0, CN rec_write [constn 0, Id 3 1], 
   490         CN rec_if [condn 0, case0, 
   488           CN rec_if [cond1, CN rec_write [constn 1, Id 3 1],
 
   491           CN rec_if [condn 1, case1,
 
   489             CN rec_if [cond2, case2,
 
   492             CN rec_if [condn 2, case2,
 
   490               CN rec_if [cond3, CN rec_pdec2 [Id 3 1], Id 3 1]]]])"
 
   493               CN rec_if [condn 3, case3, Id 3 1]]]])"
 
   491 
   494 
   492 lemma newleft_lemma [simp]:
 
   495 definition 
   493   "rec_eval rec_newleft [p, r, a] = Newleft p r a"
 
   496   "rec_actn = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in
 
   494 by (simp add: rec_newleft_def Let_def)
 
   497                let add2 = CN rec_mult [constn 2, CN rec_scan [Id 3 2]] in
 
   495 
   498                let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]]
 
   496 lemma newright_lemma [simp]:
 
   499                in CN rec_if [Id 3 1, entry, constn 4])"
 
   497   "rec_eval rec_newright [p, r, a] = Newright p r a"
 
   500 
   498 by (simp add: rec_newright_def Let_def)
 
   501 definition rec_newstat :: "recf"
 
   499 
   502   where
 
   500 
   503   "rec_newstat = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in
 
   501 definition
 
   504                   let add2 = CN S [CN rec_mult [constn 2, CN rec_scan [Id 3 2]]] in
 
   502   "rec_actn = rec_swap (PR (CN rec_pdec1 [CN rec_pdec1 [Id 1 0]])
 
   505                   let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]]
 
   503                            (CN rec_pdec1 [CN rec_pdec2 [Id 3 2]]))"
 
   506                   in CN rec_if [Id 3 1, entry, Z])"
 
   504 
   507 
   505 lemma act_lemma [simp]:
 
   508 definition 
   506   "rec_eval rec_actn [n, c] = Actn n c"
 
   509   "rec_trpl = CN rec_penc [CN rec_penc [Id 3 0, Id 3 1], Id 3 2]"
 
   507 apply(simp add: rec_actn_def)
 
   510 
   508 apply(case_tac c)
 
   511 definition
 
   509 apply(simp_all)
 
   512   "rec_left = rec_pdec1"
 
   510 done
 
   513 
   511 
   514 definition 
   512 definition 
   515   "rec_right = CN rec_pdec2 [rec_pdec1]"
 
   513   "rec_action = (let cond1 = CN rec_noteq [Id 3 1, Z] in 
   516 
   514                  let cond2 = CN rec_within [Id 3 0, CN rec_pred [Id 3 1]] in
 
   517 definition 
   515                  let if_branch = CN rec_actn [CN rec_ldec [Id 3 0, CN rec_pred [Id 3 1]], Id 3 2]
 
   518   "rec_stat = CN rec_pdec2 [rec_pdec2]"
 
   516                  in CN rec_if [CN rec_conj [cond1, cond2], if_branch, constn 4])"
 
       
   517 
       
   518 lemma action_lemma [simp]:
 
       
   519   "rec_eval rec_action [m, q, c] = Action m q c"
 
       
   520 by (simp add: rec_action_def)
 
       
   521 
       
   522 definition
 
       
   523   "rec_newstat = rec_swap (PR (CN rec_pdec2 [CN rec_pdec1 [Id 1 0]])
 
       
   524                               (CN rec_pdec2 [CN rec_pdec2 [Id 3 2]]))"
 
       
   525 
       
   526 lemma newstat_lemma [simp]:
 
       
   527   "rec_eval rec_newstat [n, c] = Newstat n c"
 
       
   528 apply(simp add: rec_newstat_def)
 
       
   529 apply(case_tac c)
 
       
   530 apply(simp_all)
 
       
   531 done
 
       
   532 
       
   533 definition
 
       
   534   "rec_newstate = (let cond = CN rec_noteq [Id 3 1, Z] in
 
       
   535                    let if_branch = CN rec_newstat [CN rec_ldec [Id 3 0, CN rec_pred [Id 3 1]], Id 3 2]
 
       
   536                    in CN rec_if [cond, if_branch, Z])"
 
       
   537 
       
   538 lemma newstate_lemma [simp]:
 
       
   539   "rec_eval rec_newstate [m, q, r] = Newstate m q r"
 
       
   540 by (simp add: rec_newstate_def)
 
       
   541 
       
   542 definition
 
       
   543   "rec_conf = rec_lenc [Id 3 0, Id 3 1, Id 3 2]"
 
       
   544 
       
   545 lemma conf_lemma [simp]:
 
       
   546   "rec_eval rec_conf [q, l, r] = Conf (q, l, r)"
 
       
   547 by(simp add: rec_conf_def)
 
       
   548 
       
   549 definition 
       
   550   "rec_state = CN rec_ldec [Id 1 0, Z]"
 
       
   551 
       
   552 definition
 
       
   553   "rec_left = CN rec_ldec [Id 1 0, constn 1]"
 
       
   554 
       
   555 definition 
       
   556   "rec_right = CN rec_ldec [Id 1 0, constn 2]"
 
       
   557 
       
   558 lemma state_lemma [simp]:
 
       
   559   "rec_eval rec_state [cf] = State cf"
 
       
   560 by (simp add: rec_state_def)
 
       
   561 
       
   562 lemma left_lemma [simp]:
 
       
   563   "rec_eval rec_left [cf] = Left cf"
 
       
   564 by (simp add: rec_left_def)
 
       
   565 
       
   566 lemma right_lemma [simp]:
 
       
   567   "rec_eval rec_right [cf] = Right cf"
 
       
   568 by (simp add: rec_right_def)
 
       
   569 
       
   570 (* HERE *)
 
   519 
   571 
   520 definition 
   572 definition 
   521   "rec_newconf = (let act = CN rec_actn [Id 2 0, CN rec_stat [Id 2 1], CN rec_right [Id 2 1]] in
 
   573   "rec_newconf = (let act = CN rec_actn [Id 2 0, CN rec_stat [Id 2 1], CN rec_right [Id 2 1]] in
 
   522                   let left = CN rec_left [Id 2 1] in
 
   574                   let left = CN rec_left [Id 2 1] in
 
   523                   let right = CN rec_right [Id 2 1] in
 
   575                   let right = CN rec_right [Id 2 1] in
tm