src/HOLCF/Dlist.ML

 (* ------------------------------------------------------------------------*)
 
 val temp = prove_goalw Dlist.thy  [dlist_copy_def] "dlist_copy`f`UU=UU"
  (fn prems =>
 	[
-	(asm_simp_tac (HOLCF_ss addsimps 
+	(asm_simp_tac (!simpset addsimps 
 		(dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1)
 	]);
 
 val dlist_copy = [temp];
 
 
 val temp = prove_goalw Dlist.thy  [dlist_copy_def,dnil_def] 
     "dlist_copy`f`dnil=dnil"
  (fn prems =>
 	[
-	(asm_simp_tac (HOLCF_ss addsimps 
+	(asm_simp_tac (!simpset addsimps 
 		(dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1)
 	]);
 
 val dlist_copy = temp :: dlist_copy;
 

 val temp = prove_goalw Dlist.thy  [dlist_copy_def,dcons_def] 
 	"xl~=UU ==> dlist_copy`f`(dcons`x`xl)= dcons`x`(f`xl)"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(asm_simp_tac (HOLCF_ss addsimps 
+	(asm_simp_tac (!simpset addsimps 
 		(dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1),
 	(res_inst_tac [("Q","x=UU")] classical2 1),
-	(asm_simp_tac HOLCF_ss  1),
-	(asm_simp_tac (HOLCF_ss addsimps [defined_spair]) 1)
+	(Asm_simp_tac  1),
+	(asm_simp_tac (!simpset addsimps [defined_spair]) 1)
 	]);
 
 val dlist_copy = temp :: dlist_copy;
 
 val dlist_rews =  dlist_copy @ dlist_rews; 

 
 qed_goalw "Exh_dlist" Dlist.thy [dcons_def,dnil_def]
 	"l = UU | l = dnil | (? x xl. x~=UU &xl~=UU & l = dcons`x`xl)"
  (fn prems =>
 	[
-	(simp_tac HOLCF_ss  1),
+	(Simp_tac 1),
 	(rtac (dlist_rep_iso RS subst) 1),
 	(res_inst_tac [("p","dlist_rep`l")] ssumE 1),
 	(rtac disjI1 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
 	(rtac disjI2 1),
 	(rtac disjI1 1),
 	(res_inst_tac [("p","x")] oneE 1),
 	(contr_tac 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
 	(rtac disjI2 1),
 	(rtac disjI2 1),
 	(res_inst_tac [("p","y")] sprodE 1),
 	(contr_tac 1),
 	(rtac exI 1),
 	(rtac exI 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
 	(fast_tac HOL_cs 1)
 	]);
 
 
 qed_goal "dlistE" Dlist.thy 

 (* ------------------------------------------------------------------------*)
 
 val temp = prove_goalw  Dlist.thy  [dlist_when_def] "dlist_when`f1`f2`UU=UU"
  (fn prems =>
 	[
-	(asm_simp_tac (HOLCF_ss addsimps [dlist_iso_strict]) 1)
+	(asm_simp_tac (!simpset addsimps [dlist_iso_strict]) 1)
 	]);
 
 val dlist_when = [temp];
 
 val temp = prove_goalw  Dlist.thy [dlist_when_def,dnil_def]
  "dlist_when`f1`f2`dnil= f1"
  (fn prems =>
 	[
-	(asm_simp_tac (HOLCF_ss addsimps [dlist_abs_iso]) 1)
+	(asm_simp_tac (!simpset addsimps [dlist_abs_iso]) 1)
 	]);
 
 val dlist_when = temp::dlist_when;
 
 val temp = prove_goalw  Dlist.thy [dlist_when_def,dcons_def]
  "[|x~=UU;xl~=UU|] ==> dlist_when`f1`f2`(dcons`x`xl)= f2`x`xl"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(asm_simp_tac (HOLCF_ss addsimps [dlist_abs_iso,defined_spair]) 1)
+	(asm_simp_tac (!simpset addsimps [dlist_abs_iso,defined_spair]) 1)
 	]);
 
 val dlist_when = temp::dlist_when;
 
 val dlist_rews = dlist_when @ dlist_rews;

 (* ------------------------------------------------------------------------*)
 
 fun prover defs thm = prove_goalw Dlist.thy defs thm
  (fn prems =>
 	[
-	(simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+	(simp_tac (!simpset addsimps dlist_rews) 1)
 	]);
 
 val dlist_discsel = [
 	prover [is_dnil_def] "is_dnil`UU=UU",
 	prover [is_dcons_def] "is_dcons`UU=UU",

 
 fun prover defs thm = prove_goalw Dlist.thy defs thm
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1)
 	]);
 
 val dlist_discsel = [
 prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
   "is_dnil`dnil=TT",

 
 fun prover contr thm = prove_goal Dlist.thy thm
  (fn prems =>
 	[
 	(res_inst_tac [("P1",contr)] classical3 1),
-	(simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(simp_tac (!simpset addsimps dlist_rews) 1),
 	(dtac sym 1),
-	(asm_simp_tac HOLCF_ss  1),
-	(simp_tac (HOLCF_ss addsimps (prems @ dlist_rews)) 1)
+	(Asm_simp_tac  1),
+	(simp_tac (!simpset addsimps (prems @ dlist_rews)) 1)
 	]);
 
 
 val dlist_constrdef = [
 prover "is_dnil`(UU::'a dlist) ~= UU" "dnil~=(UU::'a dlist)",

 
 
 fun prover defs thm = prove_goalw Dlist.thy defs thm
  (fn prems =>
 	[
-	(simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+	(simp_tac (!simpset addsimps dlist_rews) 1)
 	]);
 
 val dlist_constrdef = [
 	prover [dcons_def] "dcons`UU`xl=UU",
 	prover [dcons_def] "dcons`x`UU=UU"

 	[
 	(res_inst_tac [("P1","TT << FF")] classical3 1),
 	(resolve_tac dist_less_tr 1),
 	(dres_inst_tac [("fo5","is_dnil")] monofun_cfun_arg 1),
 	(etac box_less 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
 	(res_inst_tac [("Q","(x::'a)=UU")] classical2 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
 	(res_inst_tac [("Q","(xl ::'a dlist)=UU")] classical2 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1)
 	]);
 
 val dlist_dist_less = [temp];
 
 val temp = prove_goal Dlist.thy  "[|x~=UU;xl~=UU|]==>~ dcons`x`xl << dnil"

 	(cut_facts_tac prems 1),
 	(res_inst_tac [("P1","TT << FF")] classical3 1),
 	(resolve_tac dist_less_tr 1),
 	(dres_inst_tac [("fo5","is_dcons")] monofun_cfun_arg 1),
 	(etac box_less 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1)
 	]);
 
 val dlist_dist_less = temp::dlist_dist_less;
 
 val temp = prove_goal Dlist.thy  "dnil ~= dcons`x`xl"
  (fn prems =>
 	[
 	(res_inst_tac [("Q","x=UU")] classical2 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
 	(res_inst_tac [("Q","xl=UU")] classical2 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
 	(res_inst_tac [("P1","TT = FF")] classical3 1),
 	(resolve_tac dist_eq_tr 1),
 	(dres_inst_tac [("f","is_dnil")] cfun_arg_cong 1),
 	(etac box_equals 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1)
 	]);
 
 val dlist_dist_eq = [temp,temp RS not_sym];
 
 val dlist_rews = dlist_dist_less @ dlist_dist_eq @ dlist_rews;

 	[
 	(cut_facts_tac prems 1),
 	(rtac conjI 1),
 	(dres_inst_tac [("fo5","dlist_when`UU`(LAM x l.x)")] monofun_cfun_arg 1),
 	(etac box_less 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
+	(asm_simp_tac (!simpset addsimps dlist_when) 1),
+	(asm_simp_tac (!simpset addsimps dlist_when) 1),
 	(dres_inst_tac [("fo5","dlist_when`UU`(LAM x l.l)")] monofun_cfun_arg 1),
 	(etac box_less 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1)
+	(asm_simp_tac (!simpset addsimps dlist_when) 1),
+	(asm_simp_tac (!simpset addsimps dlist_when) 1)
 	]);
 
 val dlist_invert =[temp];
 
 (* ------------------------------------------------------------------------*)

 	[
 	(cut_facts_tac prems 1),
 	(rtac conjI 1),
 	(dres_inst_tac [("f","dlist_when`UU`(LAM x l.x)")] cfun_arg_cong 1),
 	(etac box_equals 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
+	(asm_simp_tac (!simpset addsimps dlist_when) 1),
+	(asm_simp_tac (!simpset addsimps dlist_when) 1),
 	(dres_inst_tac [("f","dlist_when`UU`(LAM x l.l)")] cfun_arg_cong 1),
 	(etac box_equals 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_when) 1)
+	(asm_simp_tac (!simpset addsimps dlist_when) 1),
+	(asm_simp_tac (!simpset addsimps dlist_when) 1)
 	]);
 
 val dlist_inject = [temp];
  
 

  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac dlistE 1),
 	(contr_tac 1),
-	(REPEAT (asm_simp_tac (HOLCF_ss addsimps dlist_discsel) 1))
+	(REPEAT (asm_simp_tac (!simpset addsimps dlist_discsel) 1))
 	]);
 
 val dlist_discsel_def = 
 	[
 	prover "l~=UU ==> is_dnil`l~=UU", 

 qed_goal "dhd2" Dlist.thy "xl~=UU ==> dhd`(dcons`x`xl)=x"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(res_inst_tac [("Q","x=UU")] classical2 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1)
 	]);
 
 qed_goal "dtl2" Dlist.thy "x~=UU ==> dtl`(dcons`x`xl)=xl"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(res_inst_tac [("Q","xl=UU")] classical2 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1)
 	]);
 
 val dlist_rews = dhd2 :: dtl2 :: dlist_rews;
 
 (* ------------------------------------------------------------------------*)

 
 val temp = prove_goalw Dlist.thy [dlist_take_def] "dlist_take n`UU=UU"
  (fn prems =>
 	[
 	(res_inst_tac [("n","n")] natE 1),
-	(asm_simp_tac iterate_ss 1),
-	(asm_simp_tac iterate_ss 1),
-	(simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+	(Asm_simp_tac 1),
+	(Asm_simp_tac 1),
+	(simp_tac (!simpset addsimps dlist_rews) 1)
 	]);
 
 val dlist_take = [temp];
 
 val temp = prove_goalw Dlist.thy [dlist_take_def] "dlist_take 0`xs=UU"
  (fn prems =>
 	[
-	(asm_simp_tac iterate_ss 1)
+	(Asm_simp_tac 1)
 	]);
 
 val dlist_take = temp::dlist_take;
 
 val temp = prove_goalw Dlist.thy [dlist_take_def]
 	"dlist_take (Suc n)`dnil=dnil"
  (fn prems =>
 	[
-	(asm_simp_tac iterate_ss 1),
-	(simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+	(Asm_simp_tac 1),
+	(simp_tac (!simpset addsimps dlist_rews) 1)
 	]);
 
 val dlist_take = temp::dlist_take;
 
 val temp = prove_goalw Dlist.thy [dlist_take_def]
   "dlist_take (Suc n)`(dcons`x`xl)= dcons`x`(dlist_take n`xl)"
  (fn prems =>
 	[
 	(res_inst_tac [("Q","x=UU")] classical2 1),
-	(asm_simp_tac iterate_ss 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(Asm_simp_tac 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
 	(res_inst_tac [("Q","xl=UU")] classical2 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
-	(asm_simp_tac iterate_ss 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
+	(Asm_simp_tac 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
 	(res_inst_tac [("n","n")] natE 1),
-	(asm_simp_tac iterate_ss 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
-	(asm_simp_tac iterate_ss 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
-	(asm_simp_tac iterate_ss 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+	(Asm_simp_tac 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
+	(Asm_simp_tac 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
+	(Asm_simp_tac 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1)
 	]);
 
 val dlist_take = temp::dlist_take;
 
 val dlist_rews = dlist_take @ dlist_rews;

 "dlist_bisim R ==> ! p q. R p q --> dlist_take n`p = dlist_take n`q"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(nat_ind_tac "n" 1),
-	(simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(simp_tac (!simpset addsimps dlist_rews) 1),
 	(strip_tac 1),
 	((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
 	(atac 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
 	(etac disjE 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
 	(etac exE 1),
 	(etac exE 1),
 	(etac exE 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
 	(REPEAT (etac conjE 1)),
 	(rtac cfun_arg_cong 1),
 	(fast_tac HOL_cs 1)
 	]);
 

 \  !! x l1.[|x~=UU;l1~=UU;P(l1)|] ==> P(dcons`x`l1)\
 \  |] ==> !l.P(dlist_take n`l)"
  (fn prems =>
 	[
 	(nat_ind_tac "n" 1),
-	(simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(simp_tac (!simpset addsimps dlist_rews) 1),
 	(resolve_tac prems 1),
 	(rtac allI 1),
 	(res_inst_tac [("l","l")] dlistE 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
-	(resolve_tac prems 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
-	(resolve_tac prems 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
+	(resolve_tac prems 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
+	(resolve_tac prems 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
 	(res_inst_tac [("Q","dlist_take n1`xl=UU")] classical2 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
 	(resolve_tac prems 1),
 	(resolve_tac prems 1),
 	(atac 1),
 	(atac 1),
 	(etac spec 1)

 qed_goal "dlist_all_finite_lemma1" Dlist.thy
 "!l.dlist_take n`l=UU |dlist_take n`l=l"
  (fn prems =>
 	[
 	(nat_ind_tac "n" 1),
-	(simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(simp_tac (!simpset addsimps dlist_rews) 1),
 	(rtac allI 1),
 	(res_inst_tac [("l","l")] dlistE 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
 	(eres_inst_tac [("x","xl")] allE 1),
 	(etac disjE 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1)
 	]);
 
 qed_goal "dlist_all_finite_lemma2" Dlist.thy "? n.dlist_take n`l=l"
  (fn prems =>
 	[
 	(res_inst_tac [("Q","l=UU")] classical2 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
 	(subgoal_tac "(!n.dlist_take n`l=UU) |(? n.dlist_take n`l = l)" 1),
 	(etac disjE 1),
 	(eres_inst_tac [("P","l=UU")] notE 1),
 	(rtac dlist_take_lemma 1),
-	(asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+	(asm_simp_tac (!simpset addsimps dlist_rews) 1),
 	(atac 1),
 	(subgoal_tac "!n.!l.dlist_take n`l=UU |dlist_take n`l=l" 1),
 	(fast_tac HOL_cs 1),
 	(rtac allI 1),
 	(rtac dlist_all_finite_lemma1 1)