src/HOLCF/Fix.ML

  (fn prems =>
 	[
 	(resolve_tac (nat_recs iterate_def) 1)
 	]);
 
-val iterate_ss = Cfun_ss addsimps [iterate_0,iterate_Suc];
+Addsimps [iterate_0, iterate_Suc];
 
 qed_goal "iterate_Suc2" Fix.thy "iterate (Suc n) F x = iterate n F (F`x)"
  (fn prems =>
 	[
 	(nat_ind_tac "n" 1),
-	(simp_tac iterate_ss 1),
-	(asm_simp_tac iterate_ss 1)
+	(Simp_tac 1),
+	(Asm_simp_tac 1)
 	]);
 
 (* ------------------------------------------------------------------------ *)
 (* the sequence of function itertaions is a chain                           *)
 (* This property is essential since monotonicity of iterate makes no sense  *)

 	" x << F`x ==> is_chain (%i.iterate i F x)"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(strip_tac 1),
-	(simp_tac iterate_ss 1),
+	(Simp_tac 1),
 	(nat_ind_tac "i" 1),
-	(asm_simp_tac iterate_ss 1),
-	(asm_simp_tac iterate_ss 1),
+	(Asm_simp_tac 1),
+	(Asm_simp_tac 1),
 	(etac monofun_cfun_arg 1)
 	]);
 
 
 qed_goal "is_chain_iterate" Fix.thy  

 	(rtac is_lub_thelub 1),
 	(rtac is_chain_iterate 1),
 	(rtac ub_rangeI 1),
 	(strip_tac 1),
 	(nat_ind_tac "i" 1),
-	(asm_simp_tac iterate_ss 1),
-	(asm_simp_tac iterate_ss 1),
+	(Asm_simp_tac 1),
+	(Asm_simp_tac 1),
 	(res_inst_tac [("t","x")] subst 1),
 	(atac 1),
 	(etac monofun_cfun_arg 1)
 	]);
 

 qed_goalw "monofun_iterate" Fix.thy  [monofun] "monofun(iterate(i))"
  (fn prems =>
 	[
 	(strip_tac 1),
 	(nat_ind_tac "i" 1),
-	(asm_simp_tac iterate_ss 1),
-	(asm_simp_tac iterate_ss 1),
+	(Asm_simp_tac 1),
+	(Asm_simp_tac 1),
 	(rtac (less_fun RS iffD2) 1),
 	(rtac allI 1),
 	(rtac monofun_cfun 1),
 	(atac 1),
 	(rtac (less_fun RS iffD1 RS spec) 1),

 qed_goalw "contlub_iterate" Fix.thy  [contlub] "contlub(iterate(i))"
  (fn prems =>
 	[
 	(strip_tac 1),
 	(nat_ind_tac "i" 1),
-	(asm_simp_tac iterate_ss 1),
+	(Asm_simp_tac 1),
 	(rtac (lub_const RS thelubI RS sym) 1),
-	(asm_simp_tac iterate_ss 1),
+	(Asm_simp_tac 1),
 	(rtac ext 1),
 	(rtac (thelub_fun RS ssubst) 1),
 	(rtac is_chainI 1),
 	(rtac allI 1),
 	(rtac (less_fun RS iffD2) 1),

  (fn prems =>
 	[
 	(rtac monofunI 1),
 	(strip_tac 1),
 	(nat_ind_tac "n" 1),
-	(asm_simp_tac iterate_ss 1),
-	(asm_simp_tac iterate_ss 1),
+	(Asm_simp_tac 1),
+	(Asm_simp_tac 1),
 	(etac monofun_cfun_arg 1)
 	]);
 
 qed_goal "contlub_iterate2" Fix.thy "contlub(iterate n F)"
  (fn prems =>
 	[
 	(rtac contlubI 1),
 	(strip_tac 1),
 	(nat_ind_tac "n" 1),
-	(simp_tac iterate_ss 1),
-	(simp_tac iterate_ss 1),
+	(Simp_tac 1),
+	(Simp_tac 1),
 	(res_inst_tac [("t","iterate n1 F (lub(range(%u. Y u)))"),
 	("s","lub(range(%i. iterate n1 F (Y i)))")] ssubst 1),
 	(atac 1),
 	(rtac contlub_cfun_arg 1),
 	(etac (monofun_iterate2 RS ch2ch_monofun) 1)

 (* ------------------------------------------------------------------------ *)
 
 qed_goalw "fix_eq" Fix.thy  [fix_def] "fix`F = F`(fix`F)"
  (fn prems =>
 	[
-	(asm_simp_tac (Cfun_ss addsimps [cont_Ifix]) 1),
+	(asm_simp_tac (!simpset addsimps [cont_Ifix]) 1),
 	(rtac Ifix_eq 1)
 	]);
 
 qed_goalw "fix_least" Fix.thy [fix_def] "F`x = x ==> fix`F << x"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(asm_simp_tac (Cfun_ss addsimps [cont_Ifix]) 1),
+	(asm_simp_tac (!simpset addsimps [cont_Ifix]) 1),
 	(etac Ifix_least 1)
 	]);
 
 
 qed_goal "fix_eq2" Fix.thy "f == fix`F ==> f = F`f"

 qed_goalw "fix_def2" Fix.thy [fix_def]
  "fix`F = lub(range(%i. iterate i F UU))"
  (fn prems =>
 	[
 	(fold_goals_tac [Ifix_def]),
-	(asm_simp_tac (Cfun_ss addsimps [cont_Ifix]) 1)
+	(asm_simp_tac (!simpset addsimps [cont_Ifix]) 1)
 	]);
 
 
 (* ------------------------------------------------------------------------ *)
 (* Lemmas about admissibility and fixed point induction                     *)

 	(rtac refl_less 1),
 	(res_inst_tac [("P","Y(Suc(x)) = UU")] notE 1),
 	(atac 2),
 	(rtac mp 1),
 	(etac spec 1),
-	(asm_simp_tac nat_ss 1)
+	(Asm_simp_tac 1)
 	]);
 
 
 val adm_flat = flat_imp_chain_finite RS adm_chain_finite;
 (* flat(?x::?'a) ==> adm(?P::?'a => bool) *)

 
 qed_goal "adm_UU_not_less"  Fix.thy "adm(%x.~ UU << t(x))"
  (fn prems =>
 	[
 	(res_inst_tac [("P2","%x.False")] (adm_cong RS iffD1) 1),
-	(asm_simp_tac Cfun_ss 1),
+	(Asm_simp_tac 1),
 	(rtac adm_not_free 1)
 	]);
 
 qed_goalw "adm_not_UU"  Fix.thy [adm_def] 
 	"cont(t)==> adm(%x.~ (t x) = UU)"

 	(rtac notE 1),
 	(rtac (not_less_eq RS iffD2) 1),
 	(atac 1),
 	(atac 1),
 	(res_inst_tac [("s","False"),("t","Suc(ia) < Suc(i)")] ssubst 1),
-	(asm_simp_tac nat_ss  1),
+	(Asm_simp_tac  1),
 	(rtac iffI 1),
 	(etac FalseE 2),
 	(rtac notE 1),
 	(etac less_not_sym 1),	
 	(atac 1),
-	(asm_simp_tac Cfun_ss  1),
+	(Asm_simp_tac 1),
 	(etac (is_chainE RS spec) 1),
 	(hyp_subst_tac 1),
-	(asm_simp_tac nat_ss 1),
-	(rtac refl_less 1),
-	(asm_simp_tac nat_ss 1),
-	(rtac refl_less 1)
+	(Asm_simp_tac 1),
+	(Asm_simp_tac 1)
 	]);
 
 qed_goal "adm_disj_lemma4"  Fix.thy
 "[| ! j. i < j --> Q(Y(j)) |] ==>\
 \	 ! n. Q( if n < Suc i then Y(Suc i) else Y n)"

 	[
 	(cut_facts_tac prems 1),
 	(rtac allI 1),
 	(res_inst_tac [("m","n"),("n","Suc(i)")] nat_less_cases 1),
 	(res_inst_tac[("s","Y(Suc(i))"),("t","if n<Suc(i) then Y(Suc(i)) else Y n")] ssubst 1),
-	(asm_simp_tac nat_ss 1),
+	(Asm_simp_tac 1),
 	(etac allE 1),
 	(rtac mp 1),
 	(atac 1),
-	(asm_simp_tac nat_ss 1),
+	(Asm_simp_tac 1),
 	(res_inst_tac[("s","Y(n)"),("t","if n<Suc(i) then Y(Suc(i)) else Y(n)")] ssubst 1),
-	(asm_simp_tac nat_ss 1),
+	(Asm_simp_tac 1),
 	(hyp_subst_tac 1),
 	(dtac spec 1),
 	(rtac mp 1),
 	(atac 1),
-	(asm_simp_tac nat_ss 1),
+	(Asm_simp_tac 1),
 	(res_inst_tac [("s","Y(n)"),("t","if n < Suc(i) then Y(Suc(i)) else Y(n)")] ssubst 1),
 	(res_inst_tac [("s","False"),("t","n < Suc(i)")] ssubst 1),
 	(rtac iffI 1),
 	(etac FalseE 2),
 	(rtac notE 1),
 	(etac less_not_sym 1),	
 	(atac 1),
-	(asm_simp_tac nat_ss 1),
+	(Asm_simp_tac 1),
 	(dtac spec 1),
 	(rtac mp 1),
 	(atac 1),
 	(etac Suc_lessD 1)
 	]);