1040 

  1041 text {*

  1042   The following lemma shows the meaning of @{text "tinres"} with respect to 

  1043   one step execution.

  1044   *}

  1045 lemma tinres_step: 

  1046   "\<lbrakk>tinres l l'; step (ss, l, r) (t, 0) = (sa, la, ra); 

  1047                  step (ss, l', r) (t, 0) = (sb, lb, rb)\<rbrakk>

  1048     \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"

  1049 apply(case_tac ss, case_tac [!]r, case_tac [!] "a::cell")

  1050 apply(auto simp: step.simps fetch.simps

  1051         split: if_splits )

  1052 apply(case_tac [!] "t ! (2 * nat)", 

  1053      auto simp: tinres_def split: if_splits)

  1054 apply(case_tac [1-8] a, auto split: if_splits)

  1055 apply(case_tac [!] "t ! (2 * nat)", 

  1056      auto simp: tinres_def split: if_splits)

  1057 apply(case_tac [1-4] a, auto split: if_splits)

  1058 apply(case_tac [!] "t ! Suc (2 * nat)", 

  1059      auto simp: if_splits)

  1060 apply(case_tac [!] aa, auto split: if_splits)

  1061 done

  1062 

  1063 text {*

  1064   The following lemma shows the meaning of @{text "tinres"} with respect to 

  1065   many step execution.

  1066   *}

  1067 

  1068 lemma tinres_steps: 

  1069   "\<lbrakk>tinres l l'; steps (ss, l, r) (t, 0) stp = (sa, la, ra); 

  1070                  steps (ss, l', r) (t, 0) stp = (sb, lb, rb)\<rbrakk>

  1071     \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"

  1072 apply(induct stp arbitrary: sa la ra sb lb rb, simp add: steps.simps)

  1073 apply(simp add: step_red)

  1074 apply(case_tac "(steps (ss, l, r) (t, 0) stp)")

  1075 apply(case_tac "(steps (ss, l', r) (t, 0) stp)")

  1076 proof -

  1077   fix stp sa la ra sb lb rb a b c aa ba ca

  1078   assume ind: "\<And>sa la ra sb lb rb. \<lbrakk>steps (ss, l, r) (t, 0) stp = (sa, (la::cell list), ra); 

  1079           steps (ss, l', r) (t, 0) stp = (sb, lb, rb)\<rbrakk> \<Longrightarrow> tinres la lb \<and> ra = rb \<and> sa = sb"

  1080   and h: " tinres l l'" "step (steps (ss, l, r) (t, 0) stp) (t, 0) = (sa, la, ra)"

  1081          "step (steps (ss, l', r) (t, 0) stp) (t, 0) = (sb, lb, rb)" "steps (ss, l, r) (t, 0) stp = (a, b, c)" 

  1082          "steps (ss, l', r) (t, 0) stp = (aa, ba, ca)"

  1083   have "tinres b ba \<and> c = ca \<and> a = aa"

  1084     apply(rule_tac ind, simp_all add: h)

  1085     done

  1086   thus "tinres la lb \<and> ra = rb \<and> sa = sb"

  1087     apply(rule_tac l = b and l' = ba and r = c  and ss = a   

  1088             and t = t in tinres_step)

  1089     using h

  1090     apply(simp, simp, simp)

  1091     done

  1092 qed

  1093 

  1094 lemma tinres_ex1: "tinres (Bk \<up> nb) b \<Longrightarrow> \<exists>nb. b = Bk \<up> nb"

  1095   apply(auto simp: tinres_def replicate_add[THEN sym])

  1096   apply(case_tac "nb > n")

  1097   apply(subgoal_tac "\<exists> d. nb = d + n", auto simp: replicate_add)

  1098   apply arith

  1099   by (metis Nil_is_append_conv add_diff_inverse append_assoc nat_add_commute replicate_0 replicate_add 

  1100     self_append_conv2)

  1101