--- a/thys2/UF_Rec.thy Sat May 25 01:33:31 2013 +0100
+++ b/thys2/UF_Rec.thy Sat May 25 11:46:25 2013 +0100
@@ -162,6 +162,11 @@
"Steps cf p 0 = cf"
| "Steps cf p (Suc n) = Steps (Step cf p) p n"
+lemma Step_Steps_comm:
+ "Step (Steps cf p n) p = Steps (Step cf p) p n"
+by (induct n arbitrary: cf) (simp_all only: Steps.simps)
+
+
text {*
Decoding tapes into binary or stroke numbers.
*}
@@ -310,6 +315,8 @@
where
"Halt m cf = (LEAST k. Stop m cf k)"
+thm Steps.simps
+
fun UF :: "nat \<Rightarrow> nat \<Rightarrow> nat"
where
"UF m cf = Stknum (Right (Steps cf m (Halt m cf))) - 1"
@@ -567,139 +574,101 @@
"rec_eval rec_right [cf] = Right cf"
by (simp add: rec_right_def)
-(* HERE *)
+definition
+ "rec_step = (let left = CN rec_left [Id 2 0] in
+ let right = CN rec_right [Id 2 0] in
+ let state = CN rec_state [Id 2 0] in
+ let read = CN rec_read [right] in
+ let action = CN rec_action [Id 2 1, state, read] in
+ let newstate = CN rec_newstate [Id 2 1, state, read] in
+ let newleft = CN rec_newleft [left, right, action] in
+ let newright = CN rec_newright [left, right, action]
+ in CN rec_conf [newstate, newleft, newright])"
-definition
- "rec_newconf = (let act = CN rec_actn [Id 2 0, CN rec_stat [Id 2 1], CN rec_right [Id 2 1]] in
- let left = CN rec_left [Id 2 1] in
- let right = CN rec_right [Id 2 1] in
- let stat = CN rec_stat [Id 2 1] in
- let one = CN rec_newleft [left, right, act] in
- let two = CN rec_newstat [Id 2 0, stat, right] in
- let three = CN rec_newright [left, right, act]
- in CN rec_trpl [one, two, three])"
-
-definition
- "rec_conf = PR (CN rec_trpl [constn 0, constn 1, Id 2 1])
- (CN rec_newconf [Id 4 2 , Id 4 1])"
+lemma step_lemma [simp]:
+ "rec_eval rec_step [cf, m] = Step cf m"
+by (simp add: Let_def rec_step_def)
definition
- "rec_nstd = (let disj1 = CN rec_noteq [rec_stat, constn 0] in
- let disj2 = CN rec_noteq [rec_left, constn 0] in
- let rhs = CN rec_pred [CN rec_power [constn 2, CN rec_lg [CN S [rec_right], constn 2]]] in
- let disj3 = CN rec_noteq [rec_right, rhs] in
- let disj4 = CN rec_eq [rec_right, constn 0] in
- CN rec_disj [CN rec_disj [CN rec_disj [disj1, disj2], disj3], disj4])"
-
-definition
- "rec_nostop = CN rec_nstd [rec_conf]"
+ "rec_steps = PR (Id 3 0)
+ (CN rec_step [Id 4 1, Id 4 3])"
-definition
- "rec_value = CN rec_pred [CN rec_lg [S, constn 2]]"
-
-definition
- "rec_halt = MN rec_nostop"
-
-definition
- "rec_uf = CN rec_value [CN rec_right [CN rec_conf [rec_halt, Id 2 0, Id 2 1]]]"
-
+lemma steps_lemma [simp]:
+ "rec_eval rec_steps [n, cf, p] = Steps cf p n"
+by (induct n) (simp_all add: rec_steps_def Step_Steps_comm del: Step.simps)
-section {* Correctness Proofs for Recursive Functions *}
-
-lemma entry_lemma [simp]:
- "rec_eval rec_entry [sr, i] = Entry sr i"
-by(simp add: rec_entry_def)
+definition
+ "rec_stknum = CN rec_minus
+ [CN (rec_sigma1 (CN rec_ldec [Id 2 1, Id 2 0])) [CN rec_enclen [Id 1 0], Id 1 0],
+ CN rec_ldec [Id 1 0, CN rec_enclen [Id 1 0]]]"
-lemma listsum2_lemma [simp]:
- "length xs = vl \<Longrightarrow> rec_eval (rec_listsum2 vl n) xs = Listsum2 xs n"
-by (induct n) (simp_all)
-
-lemma strt'_lemma [simp]:
- "length xs = vl \<Longrightarrow> rec_eval (rec_strt' vl n) xs = Strt' xs n"
-by (induct n) (simp_all add: Let_def)
+lemma stknum_lemma [simp]:
+ "rec_eval rec_stknum [z] = Stknum z"
+by (simp add: rec_stknum_def Stknum_def lessThan_Suc_atMost[symmetric])
-lemma map_suc:
- "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs"
-proof -
- have "Suc \<circ> (\<lambda>x. xs ! x) = (\<lambda>x. Suc (xs ! x))" by (simp add: comp_def)
- then have "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map (Suc \<circ> (\<lambda>x. xs ! x)) [0..<length xs]" by simp
- also have "... = map Suc (map (\<lambda>x. xs ! x) [0..<length xs])" by simp
- also have "... = map Suc xs" by (simp add: map_nth)
- finally show "map (\<lambda>x. Suc (xs ! x)) [0..<length xs] = map Suc xs" .
-qed
+definition
+ "rec_right_std = (let bound = CN rec_enclen [Id 1 0] in
+ let cond1 = CN rec_le [constn 1, Id 2 0] in
+ let cond2 = rec_all1_less (CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], constn 1]) in
+ let bound2 = CN rec_minus [CN rec_enclen [Id 2 1], Id 2 0] in
+ let cond3 = CN (rec_all2_less
+ (CN rec_eq [CN rec_ldec [Id 3 2, CN rec_add [Id 3 1, Id 3 0]], Z]))
+ [bound2, Id 2 0, Id 2 1] in
+ CN (rec_ex1 (CN rec_conj [CN rec_conj [cond1, cond2], cond3])) [bound, Id 1 0])"
-lemma strt_lemma [simp]:
- "length xs = vl \<Longrightarrow> rec_eval (rec_strt vl) xs = Strt xs"
-by (simp add: comp_def map_suc[symmetric])
-
-lemma scan_lemma [simp]:
- "rec_eval rec_scan [r] = r mod 2"
-by(simp add: rec_scan_def)
+definition
+ "rec_left_std = (let cond = CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], Z]
+ in CN (rec_all1_less cond) [CN rec_enclen [Id 1 0], Id 1 0])"
-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)
+lemma left_std_lemma [simp]:
+ "rec_eval rec_left_std [z] = (if left_std z then 1 else 0)"
+by (simp add: Let_def rec_left_std_def left_std_def)
-lemma actn_lemma [simp]:
- "rec_eval rec_actn [m, q, r] = Actn m q r"
-by (simp add: rec_actn_def)
-
-lemma newstat_lemma [simp]:
- "rec_eval rec_newstat [m, q, r] = Newstat m q r"
-by (simp add: rec_newstat_def)
+lemma right_std_lemma [simp]:
+ "rec_eval rec_right_std [z] = (if right_std z then 1 else 0)"
+by (simp add: Let_def rec_right_std_def right_std_def)
-lemma trpl_lemma [simp]:
- "rec_eval rec_trpl [p, q, r] = Trpl p q r"
-apply(simp)
-apply (simp add: rec_trpl_def)
+definition
+ "rec_std = CN rec_conj [CN rec_left_std [CN rec_left [Id 1 0]],
+ CN rec_right_std [CN rec_right [Id 1 0]]]"
-lemma left_lemma [simp]:
- "rec_eval rec_left [c] = Left c"
-by(simp add: rec_left_def)
+definition
+ "rec_final = CN rec_eq [CN rec_state [Id 1 0], Z]"
-lemma right_lemma [simp]:
- "rec_eval rec_right [c] = Right c"
-by(simp add: rec_right_def)
+definition
+ "rec_stop = (let steps = CN rec_steps [Id 3 2, Id 3 1, Id 3 0] in
+ CN rec_conj [CN rec_final [steps], CN rec_std [steps]])"
-lemma stat_lemma [simp]:
- "rec_eval rec_stat [c] = Stat c"
-by(simp add: rec_stat_def)
-
-lemma newconf_lemma [simp]:
- "rec_eval rec_newconf [m, c] = Newconf m c"
-by (simp add: rec_newconf_def Let_def)
-
-lemma conf_lemma [simp]:
- "rec_eval rec_conf [k, m, r] = Conf k m r"
-by(induct k) (simp_all add: rec_conf_def)
+lemma std_lemma [simp]:
+ "rec_eval rec_std [cf] = (if Std cf then 1 else 0)"
+by (simp add: rec_std_def)
-lemma nstd_lemma [simp]:
- "rec_eval rec_nstd [c] = (if Nstd c then 1 else 0)"
-by(simp add: rec_nstd_def)
+lemma final_lemma [simp]:
+ "rec_eval rec_final [cf] = (if Final cf then 1 else 0)"
+by (simp add: rec_final_def)
-lemma nostop_lemma [simp]:
- "rec_eval rec_nostop [t, m, r] = (if Nostop t m r then 1 else 0)"
-by (simp add: rec_nostop_def)
+lemma stop_lemma [simp]:
+ "rec_eval rec_stop [m, cf, k] = (if Stop m cf k then 1 else 0)"
+by (simp add: Let_def rec_stop_def)
-lemma value_lemma [simp]:
- "rec_eval rec_value [x] = Value x"
-by (simp add: rec_value_def)
+definition
+ "rec_halt = MN (CN rec_not [CN rec_stop [Id 3 1, Id 3 2, Id 3 0]])"
lemma halt_lemma [simp]:
- "rec_eval rec_halt [m, r] = Halt m r"
-by (simp add: rec_halt_def)
+ "rec_eval rec_halt [m, cf] = Halt m cf"
+by (simp add: rec_halt_def del: Stop.simps)
+
+definition
+ "rec_uf = CN rec_pred
+ [CN rec_stknum
+ [CN rec_right
+ [CN rec_steps [CN rec_halt [Id 2 0, Id 2 1], Id 2 1, Id 2 0]]]]"
lemma uf_lemma [simp]:
- "rec_eval rec_uf [m, r] = UF m r"
+ "rec_eval rec_uf [m, cf] = UF m cf"
by (simp add: rec_uf_def)
-
-
end