# HG changeset patch # User Christian Urban # Date 1369441955 -3600 # Node ID aa102c18213287fa15785961811577f4d2082956 # Parent 5704925ad1381fc4ac30a1d3285824a41674f7c0 more rec-funs definitions diff -r 5704925ad138 -r aa102c182132 thys2/Recs.thy --- a/thys2/Recs.thy Fri May 24 22:18:52 2013 +0100 +++ b/thys2/Recs.thy Sat May 25 01:32:35 2013 +0100 @@ -326,6 +326,7 @@ text {* Dvd, Quotient, Modulo *} +(* FIXME: probably all not needed *) definition "rec_dvd = rec_swap (CN (rec_ex2 (CN rec_eq [Id 3 2, CN rec_mult [Id 3 1, Id 3 0]])) [Id 2 0, Id 2 1, Id 2 0])" @@ -349,7 +350,7 @@ "Iter f 0 = id" | "Iter f (Suc n) = f \ (Iter f n)" -lemma iter_comm: +lemma Iter_comm: "(Iter f n) (f x) = f ((Iter f n) x)" by (induct n) (simp_all) @@ -697,6 +698,8 @@ "rec_eval rec_penc [m, n] = penc m n" by (simp add: rec_penc_def prod_encode_def) +text {* encoding and decoding of lists of natural numbers *} + fun lenc :: "nat list \ nat" where @@ -714,17 +717,15 @@ "pdec2 0 = 0" by (simp_all add: prod_decode_def prod_decode_aux.simps) -lemma w: +lemma ldec_zero: "ldec 0 n = 0" by (induct n) (simp_all add: prod_decode_def prod_decode_aux.simps) lemma list_encode_inverse: "ldec (lenc xs) n = (if n < length xs then xs ! n else 0)" -apply(induct xs arbitrary: n rule: lenc.induct) -apply(simp_all add: w) -apply(case_tac n) -apply(simp_all) -done +by (induct xs arbitrary: n rule: lenc.induct) + (auto simp add: ldec_zero nth_Cons split: nat.splits) + lemma lenc_length_le: "length xs \ lenc xs" @@ -766,21 +767,45 @@ "enclen 0 = 0" by (simp add: enclen_def) +fun + rec_lenc :: "recf list \ recf" +where + "rec_lenc [] = Z" +| "rec_lenc (f # fs) = CN rec_penc [CN S [f], rec_lenc fs]" definition "rec_ldec = CN rec_pred [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]" +definition + "rec_within = CN rec_less [Z, rec_swap (rec_iter rec_pdec2)]" + +definition + "rec_enclen = CN (rec_max1 (CN rec_not [CN rec_within [Id 2 1, CN rec_pred [Id 2 0]]])) [Id 1 0, Id 1 0]" + lemma ldec_iter: "ldec z n = pdec1 ((Iter pdec2 n) z) - 1" -apply(induct n arbitrary: z) -apply(simp_all) -apply(subst iter_comm) -apply(simp) -done +by (induct n arbitrary: z) (simp | subst Iter_comm)+ + +lemma within_iter: + "within z n = (0 < (Iter pdec2 n) z)" +by (induct n arbitrary: z) (simp | subst Iter_comm)+ + +lemma lenc_lemma [simp]: + "rec_eval (rec_lenc fs) xs = lenc (map (\f. rec_eval f xs) fs)" +by (induct fs) (simp_all) lemma ldec_lemma [simp]: "rec_eval rec_ldec [z, n] = ldec z n" by (simp add: ldec_iter rec_ldec_def) +lemma within_lemma [simp]: + "rec_eval rec_within [z, n] = (if within z n then 1 else 0)" +by (simp add: within_iter rec_within_def) + +lemma enclen_lemma [simp]: + "rec_eval rec_enclen [z] = enclen z" +by (simp add: rec_enclen_def enclen_def) + + end diff -r 5704925ad138 -r aa102c182132 thys2/UF_Rec.thy --- a/thys2/UF_Rec.thy Fri May 24 22:18:52 2013 +0100 +++ b/thys2/UF_Rec.thy Sat May 25 01:32:35 2013 +0100 @@ -111,27 +111,27 @@ else r)" text {* - The @{text "Actn"} function given on page 92 of B book, which is used to - fetch Turing Machine intructions. In @{text "Actn m q r"}, @{text "m"} is + The @{text "Action"} function given on page 92 of B book, which is used to + fetch Turing Machine intructions. In @{text "Action m q r"}, @{text "m"} is the code of the Turing Machine, @{text "q"} is the current state of Turing Machine, and @{text "r"} is the scanned cell of is the right tape. *} -fun actn :: "nat \ nat \ nat" where - "actn n 0 = pdec1 (pdec1 n)" -| "actn n _ = pdec1 (pdec2 n)" +fun Actn :: "nat \ nat \ nat" where + "Actn n 0 = pdec1 (pdec1 n)" +| "Actn n _ = pdec1 (pdec2 n)" -fun Actn :: "nat \ nat \ nat \ nat" +fun Action :: "nat \ nat \ nat \ nat" where - "Actn m q r = (if q \ 0 \ within m (q - 1) then (actn (ldec m (q - 1)) r) else 4)" + "Action m q c = (if q \ 0 \ within m (q - 1) then Actn (ldec m (q - 1)) c else 4)" -fun newstate :: "nat \ nat \ nat" where - "newstate n 0 = pdec2 (pdec1 n)" -| "newstate n _ = pdec2 (pdec2 n)" +fun Newstat :: "nat \ nat \ nat" where + "Newstat n 0 = pdec2 (pdec1 n)" +| "Newstat n _ = pdec2 (pdec2 n)" fun Newstate :: "nat \ nat \ nat \ nat" where - "Newstate m q r = (if q \ 0 then (newstate (ldec m (q - 1)) r) else 0)" + "Newstate m q r = (if q \ 0 then Newstat (ldec m (q - 1)) r else 0)" fun Conf :: "nat \ (nat \ nat) \ nat" where @@ -149,8 +149,8 @@ fun Step :: "nat \ nat \ nat" where "Step cf m = Conf (Newstate m (State cf) (Read (Right cf)), - Newleft (Left cf) (Right cf) (Actn m (State cf) (Read (Right cf))), - Newright (Left cf) (Right cf) (Actn m (State cf) (Read (Right cf))))" + Newleft (Left cf) (Right cf) (Action m (State cf) (Read (Right cf))), + Newright (Left cf) (Right cf) (Action m (State cf) (Read (Right cf))))" text {* @{text "Steps cf m k"} computes the TM configuration after @{text "k"} steps of execution @@ -347,7 +347,7 @@ done lemma Fetch_action_simulate: - "tm_wf tp \ Actn (Code_tprog tp) st (cell_num c) = action_num (fst (fetch tp st c))" + "tm_wf tp \ Action (Code_tprog tp) st (cell_num c) = action_num (fst (fetch tp st c))" apply(induct tp st c rule: fetch.induct) apply(simp_all add: list_encode_inverse split: cell.split) done @@ -465,57 +465,109 @@ "rec_eval rec_write [x, y] = Write x y" by (simp add: rec_write_def) - - - definition "rec_newleft = - (let cond1 = CN rec_disj [CN rec_eq [Id 3 2, Z], CN rec_eq [Id 3 2, constn 1]] in + (let cond0 = CN rec_eq [Id 3 2, constn 0] in + let cond1 = CN rec_eq [Id 3 2, constn 1] in let cond2 = CN rec_eq [Id 3 2, constn 2] in let cond3 = CN rec_eq [Id 3 2, constn 3] in - let case3 = CN rec_add [CN rec_mult [constn 2, Id 3 0], - CN rec_mod [Id 3 1, constn 2]] in - CN rec_if [cond1, Id 3 0, - CN rec_if [cond2, CN rec_quo [Id 3 0, constn 2], - CN rec_if [cond3, case3, Id 3 0]]])" + let case3 = CN rec_penc [CN S [CN rec_read [Id 3 1]], Id 3 0] in + CN rec_if [cond0, Id 3 0, + CN rec_if [cond1, Id 3 0, + CN rec_if [cond2, CN rec_pdec2 [Id 3 0], + CN rec_if [cond3, case3, Id 3 0]]]])" definition "rec_newright = - (let condn = \n. CN rec_eq [Id 3 2, constn n] in - let case0 = CN rec_minus [Id 3 1, CN rec_scan [Id 3 1]] in - let case1 = CN rec_minus [CN rec_add [Id 3 1, constn 1], CN rec_scan [Id 3 1]] in - let case2 = CN rec_add [CN rec_mult [constn 2, Id 3 1], - CN rec_mod [Id 3 0, constn 2]] in - let case3 = CN rec_quo [Id 2 1, constn 2] in - CN rec_if [condn 0, case0, - CN rec_if [condn 1, case1, - CN rec_if [condn 2, case2, - CN rec_if [condn 3, case3, Id 3 1]]]])" + (let cond0 = CN rec_eq [Id 3 2, constn 0] in + let cond1 = CN rec_eq [Id 3 2, constn 1] in + let cond2 = CN rec_eq [Id 3 2, constn 2] in + let cond3 = CN rec_eq [Id 3 2, constn 3] in + let case2 = CN rec_penc [CN S [CN rec_read [Id 3 0]], Id 3 1] in + CN rec_if [cond0, CN rec_write [constn 0, Id 3 1], + CN rec_if [cond1, CN rec_write [constn 1, Id 3 1], + CN rec_if [cond2, case2, + CN rec_if [cond3, CN rec_pdec2 [Id 3 1], Id 3 1]]]])" + +lemma newleft_lemma [simp]: + "rec_eval rec_newleft [p, r, a] = Newleft p r a" +by (simp add: rec_newleft_def Let_def) + +lemma newright_lemma [simp]: + "rec_eval rec_newright [p, r, a] = Newright p r a" +by (simp add: rec_newright_def Let_def) + + +definition + "rec_actn = rec_swap (PR (CN rec_pdec1 [CN rec_pdec1 [Id 1 0]]) + (CN rec_pdec1 [CN rec_pdec2 [Id 3 2]]))" + +lemma act_lemma [simp]: + "rec_eval rec_actn [n, c] = Actn n c" +apply(simp add: rec_actn_def) +apply(case_tac c) +apply(simp_all) +done definition - "rec_actn = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in - let add2 = CN rec_mult [constn 2, CN rec_scan [Id 3 2]] in - let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]] - in CN rec_if [Id 3 1, entry, constn 4])" + "rec_action = (let cond1 = CN rec_noteq [Id 3 1, Z] in + let cond2 = CN rec_within [Id 3 0, CN rec_pred [Id 3 1]] in + let if_branch = CN rec_actn [CN rec_ldec [Id 3 0, CN rec_pred [Id 3 1]], Id 3 2] + in CN rec_if [CN rec_conj [cond1, cond2], if_branch, constn 4])" + +lemma action_lemma [simp]: + "rec_eval rec_action [m, q, c] = Action m q c" +by (simp add: rec_action_def) + +definition + "rec_newstat = rec_swap (PR (CN rec_pdec2 [CN rec_pdec1 [Id 1 0]]) + (CN rec_pdec2 [CN rec_pdec2 [Id 3 2]]))" -definition rec_newstat :: "recf" - where - "rec_newstat = (let add1 = CN rec_mult [constn 4, CN rec_pred [Id 3 1]] in - let add2 = CN S [CN rec_mult [constn 2, CN rec_scan [Id 3 2]]] in - let entry = CN rec_entry [Id 3 0, CN rec_add [add1, add2]] - in CN rec_if [Id 3 1, entry, Z])" +lemma newstat_lemma [simp]: + "rec_eval rec_newstat [n, c] = Newstat n c" +apply(simp add: rec_newstat_def) +apply(case_tac c) +apply(simp_all) +done + +definition + "rec_newstate = (let cond = CN rec_noteq [Id 3 1, Z] in + let if_branch = CN rec_newstat [CN rec_ldec [Id 3 0, CN rec_pred [Id 3 1]], Id 3 2] + in CN rec_if [cond, if_branch, Z])" + +lemma newstate_lemma [simp]: + "rec_eval rec_newstate [m, q, r] = Newstate m q r" +by (simp add: rec_newstate_def) + +definition + "rec_conf = rec_lenc [Id 3 0, Id 3 1, Id 3 2]" + +lemma conf_lemma [simp]: + "rec_eval rec_conf [q, l, r] = Conf (q, l, r)" +by(simp add: rec_conf_def) definition - "rec_trpl = CN rec_penc [CN rec_penc [Id 3 0, Id 3 1], Id 3 2]" + "rec_state = CN rec_ldec [Id 1 0, Z]" definition - "rec_left = rec_pdec1" + "rec_left = CN rec_ldec [Id 1 0, constn 1]" definition - "rec_right = CN rec_pdec2 [rec_pdec1]" + "rec_right = CN rec_ldec [Id 1 0, constn 2]" + +lemma state_lemma [simp]: + "rec_eval rec_state [cf] = State cf" +by (simp add: rec_state_def) -definition - "rec_stat = CN rec_pdec2 [rec_pdec2]" +lemma left_lemma [simp]: + "rec_eval rec_left [cf] = Left cf" +by (simp add: rec_left_def) + +lemma right_lemma [simp]: + "rec_eval rec_right [cf] = Right cf" +by (simp add: rec_right_def) + +(* HERE *) definition "rec_newconf = (let act = CN rec_actn [Id 2 0, CN rec_stat [Id 2 1], CN rec_right [Id 2 1]] in