src/HOLCF/FOCUS/Buffer_adm.ML

-(*  Title: 	HOLCF/FOCUS/Buffer_adm.ML
+(*  Title:      HOLCF/FOCUS/Buffer_adm.ML
     ID:         $Id$
-    Author: 	David von Oheimb, TU Muenchen
+    Author:     David von Oheimb, TU Muenchen
 *)
 
 infixr 0 y;
 fun _ y t = by t;
 val b=9999;
 
 Addsimps [thm "Fin_0"];
 
 val BufAC_Asm_d2 = prove_forw "a\\<leadsto>s:BufAC_Asm ==> ? d. a=Md d" BufAC_Asm_unfold;
-val BufAC_Asm_d3 = prove_forw 
+val BufAC_Asm_d3 = prove_forw
     "a\\<leadsto>b\\<leadsto>s:BufAC_Asm ==> ? d. a=Md d & b=\\<bullet> & s:BufAC_Asm" BufAC_Asm_unfold;
 
-val BufAC_Asm_F_def3 = prove_goalw thy [BufAC_Asm_F_def] 
+val BufAC_Asm_F_def3 = prove_goalw (the_context ()) [BufAC_Asm_F_def]
  "(s:BufAC_Asm_F A) = (s=<> | \
 \ (? d. ft\\<cdot>s=Def(Md d)) & (rt\\<cdot>s=<> | ft\\<cdot>(rt\\<cdot>s)=Def \\<bullet> & rt\\<cdot>(rt\\<cdot>s):A))" (K [
-	Auto_tac]);
+        Auto_tac]);
 
 Goal "down_cont BufAC_Asm_F";
 by (auto_tac (claset(),simpset() addsimps [down_cont_def,BufAC_Asm_F_def3]));
 qed "cont_BufAC_Asm_F";
 
-val BufAC_Cmt_F_def3 = prove_goalw thy [BufAC_Cmt_F_def] 
+val BufAC_Cmt_F_def3 = prove_goalw (the_context ()) [BufAC_Cmt_F_def]
  "((s,t):BufAC_Cmt_F C) = (!d x.\
 \   (s = <>       --> t = <>                   ) & \
 \   (s = Md d\\<leadsto><>  --> t = <>                   ) & \
 \   (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x,rt\\<cdot>t):C))" (fn _=> [
-	subgoal_tac "!d x. (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> (? y. t = d\\<leadsto>y & (x,y):C)) = \
-		   \ (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x,rt\\<cdot>t):C)"  1,
-	Asm_simp_tac 1,
-	auto_tac (claset() addIs [thm "surjectiv_scons" RS sym], simpset())]);
-
-val cont_BufAC_Cmt_F = prove_goal thy "down_cont BufAC_Cmt_F" (K [
-	auto_tac (claset(),simpset() addsimps [down_cont_def,BufAC_Cmt_F_def3])]);
+        subgoal_tac "!d x. (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> (? y. t = d\\<leadsto>y & (x,y):C)) = \
+                   \ (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x,rt\\<cdot>t):C)"  1,
+        Asm_simp_tac 1,
+        auto_tac (claset() addIs [thm "surjectiv_scons" RS sym], simpset())]);
+
+val cont_BufAC_Cmt_F = prove_goal (the_context ()) "down_cont BufAC_Cmt_F" (K [
+        auto_tac (claset(),simpset() addsimps [down_cont_def,BufAC_Cmt_F_def3])]);
 
 
 (**** 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","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 [
+val adm_BufAC_Asm = prove_goalw (the_context ()) [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 *******************************************************)
 

 (*adm_non_BufAC_Asm*)
 Goal "!f ff. f:BufEq --> ff:BufEq --> s:BufAC_Asm --> f\\<cdot>s = ff\\<cdot>s";
 by (rtac fstream_ind2 1);
 by (simp_tac (simpset() addsimps [adm_non_BufAC_Asm]) 1);
 by   (force_tac (claset() addDs [Buf_f_empty], simpset()) 1);
-by  (force_tac (claset() addSDs [BufAC_Asm_d2] 
-		addDs [Buf_f_d] addEs [ssubst], simpset()) 1);
+by  (force_tac (claset() addSDs [BufAC_Asm_d2]
+                addDs [Buf_f_d] addEs [ssubst], simpset()) 1);
 by (safe_tac (claset() addSDs [BufAC_Asm_d3]));
 by (REPEAT(dtac Buf_f_d_req 1));
 by (fast_tac (claset() addEs [ssubst]) 1);
 qed_spec_mp "BufAC_Asm_cong";
 
 (*adm_non_BufAC_Asm,BufAC_Asm_cong*)
-val BufAC_Cmt_d_req = prove_goal thy 
+val BufAC_Cmt_d_req = prove_goal (the_context ())
 "!!X. [|f:BufEq; s:BufAC_Asm; (s, f\\<cdot>s):BufAC_Cmt|] ==> (a\\<leadsto>b\\<leadsto>s, f\\<cdot>(a\\<leadsto>b\\<leadsto>s)):BufAC_Cmt"
  (K [
-	rtac (BufAC_Cmt_unfold RS iffD2) 1,
-	strip_tac 1,
-	ftac Buf_f_d_req 1,
-	auto_tac (claset() addEs [BufAC_Asm_cong RS subst],simpset())]);
+        rtac (BufAC_Cmt_unfold RS iffD2) 1,
+        strip_tac 1,
+        ftac Buf_f_d_req 1,
+        auto_tac (claset() addEs [BufAC_Asm_cong RS subst],simpset())]);
 
 (*adm_BufAC_Asm*)
 Goal "antitonP BufAC_Asm";
 b y rtac antitonPI 1;
 b y rtac allI 1;

 b y    rtac cont_id 1;
 b y    rtac adm_BufAC_Asm 1;
 b y   safe_tac HOL_cs;
 b y   rtac BufAC_Asm_empty 1;
 b y  force_tac (claset() addSDs [fstream_prefix]
-		addDs [BufAC_Asm_d2] addIs [BufAC_Asm_d],simpset()) 1;
+                addDs [BufAC_Asm_d2] addIs [BufAC_Asm_d],simpset()) 1;
 b y  force_tac (claset() addSDs [fstream_prefix]
-		addDs [] addIs []
-		addDs [BufAC_Asm_d3] addSIs [BufAC_Asm_d_req],simpset()) 1;
+                addDs [] addIs []
+                addDs [BufAC_Asm_d3] addSIs [BufAC_Asm_d_req],simpset()) 1;
 qed "BufAC_Asm_antiton";
 
 (*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";
+                \    (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 (rtac allI 1);
 by (induct_tac "i" 1);
 by ( Simp_tac 1);
 by (simp_tac (simpset() addsimps [add_commute]) 1);

           (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 (EVERY[ftac Buf_f_d_req 1, etac exE 1, etac conjE 1, rotate_tac ~1 1,etac ssubst 1]); 
+by (EVERY[ftac Buf_f_d_req 1, etac exE 1, etac conjE 1, rotate_tac ~1 1,etac ssubst 1]);
 by (EVERY[ftac Buf_f_d_req 1, etac exE 1, etac conjE 1]);
-by (		subgoal_tac "f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya" 1);
+by (            subgoal_tac "f\\<cdot>(Md d\\<leadsto>\\<bullet>\\<leadsto>ya) = d\\<leadsto>ffa\\<cdot>ya" 1);
 by ( atac 2);
-by (		rotate_tac ~1 1);
-by (		Asm_full_simp_tac 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;
           (ya, ffa\\<cdot>ya) \\<in> down_iterate BufAC_Cmt_F i; ya \\<sqsubseteq> xa; f \\<in> BufEq;

 qed "adm_non_BufAC_Asm'";
 
 Goal "f \\<in> BufEq \\<Longrightarrow> adm (\\<lambda>u. u \\<in> BufAC_Asm \\<longrightarrow> (u, f\\<cdot>u) \\<in> BufAC_Cmt)";
 by (rtac triv_admI 1);
 by (Clarify_tac 1);
-by (eatac Buf_Eq_imp_AC_lemma 1 1); 
+by (eatac Buf_Eq_imp_AC_lemma 1 1);
       (* this is what we originally aimed to show, using admissibilty :-( *)
 qed "adm_BufAC'";