--- 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 \<circ> (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 \<Rightarrow> 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 \<le> lenc xs"
@@ -766,21 +767,45 @@
"enclen 0 = 0"
by (simp add: enclen_def)
+fun
+ rec_lenc :: "recf list \<Rightarrow> 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 (\<lambda>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
--- 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 \<Rightarrow> nat \<Rightarrow> nat" where
- "actn n 0 = pdec1 (pdec1 n)"
-| "actn n _ = pdec1 (pdec2 n)"
+fun Actn :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+ "Actn n 0 = pdec1 (pdec1 n)"
+| "Actn n _ = pdec1 (pdec2 n)"
-fun Actn :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+fun Action :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
where
- "Actn m q r = (if q \<noteq> 0 \<and> within m (q - 1) then (actn (ldec m (q - 1)) r) else 4)"
+ "Action m q c = (if q \<noteq> 0 \<and> within m (q - 1) then Actn (ldec m (q - 1)) c else 4)"
-fun newstate :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
- "newstate n 0 = pdec2 (pdec1 n)"
-| "newstate n _ = pdec2 (pdec2 n)"
+fun Newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+ "Newstat n 0 = pdec2 (pdec1 n)"
+| "Newstat n _ = pdec2 (pdec2 n)"
fun Newstate :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
where
- "Newstate m q r = (if q \<noteq> 0 then (newstate (ldec m (q - 1)) r) else 0)"
+ "Newstate m q r = (if q \<noteq> 0 then Newstat (ldec m (q - 1)) r else 0)"
fun Conf :: "nat \<times> (nat \<times> nat) \<Rightarrow> nat"
where
@@ -149,8 +149,8 @@
fun Step :: "nat \<Rightarrow> nat \<Rightarrow> 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 \<Longrightarrow> Actn (Code_tprog tp) st (cell_num c) = action_num (fst (fetch tp st c))"
+ "tm_wf tp \<Longrightarrow> 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 = \<lambda>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