equal
deleted
inserted
replaced
982 |
982 |
983 lemma [intro]: "tm_wf (tcopy_end, 0)" |
983 lemma [intro]: "tm_wf (tcopy_end, 0)" |
984 by(auto simp: tm_wf.simps tcopy_end_def) |
984 by(auto simp: tm_wf.simps tcopy_end_def) |
985 |
985 |
986 lemma [intro]: "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)" |
986 lemma [intro]: "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)" |
987 apply(auto simp: tm_wf.simps shift.simps adjust.simps length_comp |
987 apply(auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length |
988 tm_comp.simps) |
988 tm_comp.simps) |
989 done |
989 done |
990 |
990 |
991 lemma tcopy_correct1: |
991 lemma tcopy_correct1: |
992 "\<lbrakk>x > 0\<rbrakk> \<Longrightarrow> {inv_init1 x} tcopy {inv_end0 x}" |
992 "\<lbrakk>x > 0\<rbrakk> \<Longrightarrow> {inv_init1 x} tcopy {inv_end0 x}" |