src/HOLCF/FOCUS/Buffer_adm.ML
changeset 11704 3c50a2cd6f00
parent 11701 3d51fbf81c17
child 12484 7ad150f5fc10
     1.1 --- a/src/HOLCF/FOCUS/Buffer_adm.ML	Fri Oct 05 23:58:52 2001 +0200
     1.2 +++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Sat Oct 06 00:02:46 2001 +0200
     1.3 @@ -110,7 +110,7 @@
     1.4  Goal "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> Fin (l i) < #x --> \
     1.5  		\    (x,f\\<cdot>x):down_iterate BufAC_Cmt_F i --> \
     1.6  		\    (s,f\\<cdot>s):down_iterate BufAC_Cmt_F i";
     1.7 -by (res_inst_tac [("x","%i. # 2*i")] exI 1);
     1.8 +by (res_inst_tac [("x","%i. 2*i")] exI 1);
     1.9  by (rtac allI 1);
    1.10  by (nat_ind_tac "i" 1);
    1.11  by ( Simp_tac 1);
    1.12 @@ -129,10 +129,10 @@
    1.13         \\<lbrakk>f \\<in> BufEq;
    1.14            \\<forall>x s. s \\<in> BufAC_Asm \\<longrightarrow>
    1.15                  x \\<sqsubseteq> s \\<longrightarrow>
    1.16 -                Fin (# 2 * i) < #x \\<longrightarrow>
    1.17 +                Fin (2 * i) < #x \\<longrightarrow>
    1.18                  (x, f\\<cdot>x) \\<in> down_iterate BufAC_Cmt_F i \\<longrightarrow>
    1.19                  (s, f\\<cdot>s) \\<in> down_iterate BufAC_Cmt_F i;
    1.20 -          Md d\\<leadsto>\\<bullet>\\<leadsto>xa \\<in> BufAC_Asm; Fin (# 2 * i) < #ya; f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>t;
    1.21 +          Md d\\<leadsto>\\<bullet>\\<leadsto>xa \\<in> BufAC_Asm; Fin (2 * i) < #ya; f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>t;
    1.22            (ya, t) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa\\<rbrakk>
    1.23         \\<Longrightarrow> (xa, rt\\<cdot>(f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>xa))) \\<in> down_iterate BufAC_Cmt_F i
    1.24  *)
    1.25 @@ -147,11 +147,11 @@
    1.26  by (hyp_subst_tac 1);
    1.27  (*
    1.28   1. \\<And>i d xa ya t ff ffa.
    1.29 -       \\<lbrakk>f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya; Fin (# 2 * i) < #ya;
    1.30 +       \\<lbrakk>f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya; Fin (2 * i) < #ya;
    1.31            (ya, ffa\\<cdot>ya) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa; f \\<in> BufEq;
    1.32            \\<forall>x s. s \\<in> BufAC_Asm \\<longrightarrow>
    1.33                  x \\<sqsubseteq> s \\<longrightarrow>
    1.34 -                Fin (# 2 * i) < #x \\<longrightarrow>
    1.35 +                Fin (2 * i) < #x \\<longrightarrow>
    1.36                  (x, f\\<cdot>x) \\<in> down_iterate BufAC_Cmt_F i \\<longrightarrow>
    1.37                  (s, f\\<cdot>s) \\<in> down_iterate BufAC_Cmt_F i;
    1.38            xa \\<in> BufAC_Asm; ff \\<in> BufEq; ffa \\<in> BufEq\\<rbrakk>