src/HOLCF/FOCUS/Buffer_adm.ML

 
 (**** adm_BufAC_Asm ***********************************************************)
 
 Goalw [BufAC_Asm_F_def, stream_monoP_def] "stream_monoP BufAC_Asm_F";
 by (res_inst_tac [("x","{x. (? d. x = Md d\\<leadsto>\\<bullet>\\<leadsto><>)}")] exI 1);
-by (res_inst_tac [("x","2")] exI 1);
+by (res_inst_tac [("x","Suc (Suc 0)")] exI 1);
 by (Clarsimp_tac 1);
 qed "BufAC_Asm_F_stream_monoP";
 
 val adm_BufAC_Asm = prove_goalw thy [BufAC_Asm_def] "adm (%x. x:BufAC_Asm)" (K [
 rtac (cont_BufAC_Asm_F RS (BufAC_Asm_F_stream_monoP RS fstream_gfp_admI))1]);

 (**** adm_non_BufAC_Asm *******************************************************)
 
 Goalw [stream_antiP_def, BufAC_Asm_F_def] "stream_antiP BufAC_Asm_F";
 b y strip_tac 1;
 b y res_inst_tac [("x","{x. (? d. x = Md d\\<leadsto>\\<bullet>\\<leadsto><>)}")] exI 1;
-b y res_inst_tac [("x","2")] exI 1;
+b y res_inst_tac [("x","Suc (Suc 0)")] exI 1;
 b y rtac conjI 1;
 b y  strip_tac 2;
 b y  dtac slen_mono 2;
 b y  datac (thm "ile_trans") 1 2;
 b y ALLGOALS Force_tac;

 
 (*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong*)
 Goal "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> Fin (l i) < #x --> \
 		\    (x,f\\<cdot>x):down_iterate BufAC_Cmt_F i --> \
 		\    (s,f\\<cdot>s):down_iterate BufAC_Cmt_F i";
-by (res_inst_tac [("x","%i. #2*i")] exI 1);
+by (res_inst_tac [("x","%i. # 2*i")] exI 1);
 by (rtac allI 1);
 by (nat_ind_tac "i" 1);
 by ( Simp_tac 1);
 by (simp_tac (simpset() addsimps [add_commute]) 1);
 by (strip_tac 1);

 (*
  1. \\<And>i d xa ya t.
        \\<lbrakk>f \\<in> BufEq;
           \\<forall>x s. s \\<in> BufAC_Asm \\<longrightarrow>
                 x \\<sqsubseteq> s \\<longrightarrow>
-                Fin (#2 * i) < #x \\<longrightarrow>
+                Fin (# 2 * i) < #x \\<longrightarrow>
                 (x, f\\<cdot>x) \\<in> down_iterate BufAC_Cmt_F i \\<longrightarrow>
                 (s, f\\<cdot>s) \\<in> down_iterate BufAC_Cmt_F i;
-          Md d\\<leadsto>\\<bullet>\\<leadsto>xa \\<in> BufAC_Asm; Fin (#2 * i) < #ya; f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>t;
+          Md d\\<leadsto>\\<bullet>\\<leadsto>xa \\<in> BufAC_Asm; Fin (# 2 * i) < #ya; f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>t;
           (ya, t) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa\\<rbrakk>
        \\<Longrightarrow> (xa, rt\\<cdot>(f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>xa))) \\<in> down_iterate BufAC_Cmt_F i
 *)
 by (rotate_tac 2 1);
 by (dtac BufAC_Asm_prefix2 1);

 by (		rotate_tac ~1 1);
 by (		Asm_full_simp_tac 1);
 by (hyp_subst_tac 1);
 (*
  1. \\<And>i d xa ya t ff ffa.
-       \\<lbrakk>f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya; Fin (#2 * i) < #ya;
+       \\<lbrakk>f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya; Fin (# 2 * i) < #ya;
           (ya, ffa\\<cdot>ya) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa; f \\<in> BufEq;
           \\<forall>x s. s \\<in> BufAC_Asm \\<longrightarrow>
                 x \\<sqsubseteq> s \\<longrightarrow>
-                Fin (#2 * i) < #x \\<longrightarrow>
+                Fin (# 2 * i) < #x \\<longrightarrow>
                 (x, f\\<cdot>x) \\<in> down_iterate BufAC_Cmt_F i \\<longrightarrow>
                 (s, f\\<cdot>s) \\<in> down_iterate BufAC_Cmt_F i;
           xa \\<in> BufAC_Asm; ff \\<in> BufEq; ffa \\<in> BufEq\\<rbrakk>
        \\<Longrightarrow> (xa, ff\\<cdot>xa) \\<in> down_iterate BufAC_Cmt_F i
 *)