src/HOL/UNITY/Project.ML

 (*Generalizes project_constrains to the program F Join project h C G;
   useful with guarantees reasoning*)
 Goal "(F Join project h C G : A co B)  =  \
 \       (extend h F Join G : (C Int extend_set h A) co (extend_set h B) &  \
 \        F : A co B)";
-by (simp_tac (simpset() addsimps [Join_constrains, project_constrains]) 1);
+by (simp_tac (simpset() addsimps [project_constrains]) 1);
 by (blast_tac (claset() addIs [extend_constrains RS iffD2 RS constrains_weaken]
                         addDs [constrains_imp_subset]) 1);
 qed "Join_project_constrains";
 
 (*The condition is required to prove the left-to-right direction;

 Goalw [stable_def]
      "extend h F Join G : stable C \
 \     ==> (F Join project h C G : stable A)  =  \
 \         (extend h F Join G : stable (C Int extend_set h A) &  \
 \          F : stable A)";
-by (simp_tac (simpset() addsimps [Join_project_constrains]) 1);
+by (simp_tac (HOL_ss addsimps [Join_project_constrains]) 1);
 by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1);
 qed "Join_project_stable";
 
 (*For using project_guarantees in particular cases*)
 Goal "extend h F Join G : extend_set h A co extend_set h B \
 \     ==> F Join project h C G : A co B";
 by (asm_full_simp_tac
-    (simpset() addsimps [project_constrains, Join_constrains, 
-			 extend_constrains]) 1);
+    (simpset() addsimps [project_constrains, extend_constrains]) 1);
 by (blast_tac (claset() addIs [constrains_weaken]
 			addDs [constrains_imp_subset]) 1);
 qed "project_constrains_I";
 
 Goalw [increasing_def, stable_def]
      "extend h F Join G : increasing (func o f) \
 \     ==> F Join project h C G : increasing func";
-by (asm_full_simp_tac (simpset() addsimps [project_constrains_I, 
-					   extend_set_eq_Collect]) 1);
+by (asm_full_simp_tac (simpset_of SubstAx.thy
+		 addsimps [project_constrains_I, extend_set_eq_Collect]) 1);
 qed "project_increasing_I";
 
 Goal "(F Join project h UNIV G : increasing func)  =  \
 \     (extend h F Join G : increasing (func o f))";
 by (rtac iffI 1);
 by (etac project_increasing_I 2);
-by (asm_full_simp_tac 
-    (simpset() addsimps [increasing_def, Join_project_stable]) 1);
+by (asm_full_simp_tac (simpset_of SubstAx.thy
+		         addsimps [increasing_def, Join_project_stable]) 1);
 by (auto_tac (claset(),
-	      simpset() addsimps [Join_stable, extend_set_eq_Collect,
+	      simpset() addsimps [extend_set_eq_Collect,
 				  extend_stable RS iffD1]));
 qed "Join_project_increasing";
 
 (*The UNIV argument is essential*)
 Goal "F Join project h UNIV G : A co B \
 \     ==> extend h F Join G : extend_set h A co extend_set h B";
 by (asm_full_simp_tac
-    (simpset() addsimps [project_constrains, Join_constrains, 
-			 extend_constrains]) 1);
+    (simpset() addsimps [project_constrains, extend_constrains]) 1);
 qed "project_constrains_D";
 
 
 (*** "projecting" and union/intersection (no converses) ***)
 

 by (rtac extending_constrains 1);
 qed "extending_stable";
 
 Goalw [extending_def]
      "extending v (%G. UNIV) h F (increasing (func o f)) (increasing func)";
-by (simp_tac (simpset() addsimps [Join_project_increasing]) 1);
+by (simp_tac (HOL_ss addsimps [Join_project_increasing]) 1);
 qed "extending_increasing";
 
 
 (** Reachability and project **)
 

 qed "reachable_imp_reachable_project";
 
 Goalw [Constrains_def]
      "F Join project h (reachable (extend h F Join G)) G : A Co B  \
 \     ==> extend h F Join G : (extend_set h A) Co (extend_set h B)";
-by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1);
+by (full_simp_tac (simpset_of SubstAx.thy addsimps [Join_project_constrains]) 1);
 by (Clarify_tac 1);
 by (etac constrains_weaken 1);
 by (auto_tac (claset() addIs [reachable_imp_reachable_project], simpset()));
 qed "project_Constrains_D";
 

 qed "reachable_extend_Join_subset";
 
 Goalw [Constrains_def]
      "extend h F Join G : (extend_set h A) Co (extend_set h B)  \
 \     ==> F Join project h (reachable (extend h F Join G)) G : A Co B";
-by (full_simp_tac (simpset() addsimps [Join_project_constrains, 
+by (full_simp_tac (simpset_of SubstAx.thy addsimps [Join_project_constrains, 
 				       extend_set_Int_distrib]) 1);
 by (rtac conjI 1);
 by (force_tac
     (claset() addEs [constrains_weaken_L]
               addSDs [extend_constrains_project_set,
 		      subset_refl RS reachable_project_imp_reachable], 
-     simpset() addsimps [Join_constrains]) 2);
+     simpset()) 2);
 by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
 qed "project_Constrains_I";
 
 Goalw [Stable_def]
      "extend h F Join G : Stable (extend_set h A)  \

 Goal "[| extend h F : stable C;  G : stable C;  \
 \        extend h F Join G : A ensures B;  A-B = C Int extend_set h D |]  \
 \     ==> F Join project h C G  \
 \           : (project_set h C Int project_set h A) ensures (project_set h B)";
 by (asm_full_simp_tac
-    (simpset() addsimps [ensures_def, Join_constrains, project_constrains, 
+    (simpset() addsimps [ensures_def, project_constrains, 
 			 Join_transient, extend_transient]) 1);
 by (Clarify_tac 1);
 by (REPEAT_FIRST (rtac conjI));
 (*first subgoal*)
 by (blast_tac (claset() addIs [extend_stable_project_set RS stableD RS 

 by (blast_tac (claset() addIs [subset_imp_ensures]) 2);
 by (auto_tac (claset() addDs [extend_transient RS iffD2] 
                        addIs [transient_strengthen, project_set_I,
 			      project_unless RS unlessD, unlessI, 
 			      project_extend_constrains_I], 
-	      simpset() addsimps [ensures_def, Join_constrains,
-				  Join_stable, Join_transient]));
+	      simpset() addsimps [ensures_def, Join_transient]));
 qed_spec_mp "Join_project_ensures";
 
 (** Lemma useful for both STRONG and WEAK progress, but the transient
     condition's very strong **)
 

 Goal "[| C = (reachable (extend h F Join G)); \
 \        ALL D. project h C G : transient D --> D={};  \
 \        F Join project h C G : A LeadsTo B |] \
 \     ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
 by (asm_full_simp_tac 
-    (simpset() addsimps [LeadsTo_def, project_leadsTo_D_lemma, 
+    (simpset_of SubstAx.thy addsimps [LeadsTo_def, project_leadsTo_D_lemma, 
 			 project_set_reachable_extend_eq]) 1);
 qed "Join_project_LeadsTo";
 
 
 (*** Towards project_Ensures_D ***)
-
 
 
 Goalw [project_set_def, extend_set_def, project_act_def]
      "act ^^ (C Int extend_set h A) <= B \
 \     ==> project_act h (Restrict C act) ^^ (project_set h C Int A) \

 \        extend h F Join G : stable C |] \
 \     ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
 (*unless*)
 by (auto_tac (claset() addSIs [rewrite_rule [unless_def] project_unless2] 
                        addIs [project_extend_constrains_I], 
-	      simpset() addsimps [ensures_def, Join_constrains,
-				  Join_stable]));
+	      simpset() addsimps [ensures_def]));
 (*transient*)
 by (auto_tac (claset(), simpset() addsimps [Join_transient]));
 by (blast_tac (claset() addIs [stable_project_transient]) 2);
 by (force_tac (claset() addSEs [extend_transient RS iffD2 RS 
 				transient_strengthen],