src/HOL/UNITY/WFair.thy

 apply (unfold transient_def, clarify)
 apply (blast intro!: rev_bexI)
 done
 
 lemma transientI: 
-    "[| act: Acts F;  act``A \<subseteq> -A |] ==> F \<in> transient A"
+    "[| act \<in> Acts F;  act``A \<subseteq> -A |] ==> F \<in> transient A"
 by (unfold transient_def, blast)
 
 lemma transientE: 
     "[| F \<in> transient A;   
-        !!act. [| act: Acts F;  act``A \<subseteq> -A |] ==> P |]  
+        \<And>act. [| act \<in> Acts F;  act``A \<subseteq> -A |] ==> P |]  
      ==> P"
 by (unfold transient_def, blast)
 
 lemma transient_empty [simp]: "transient {} = UNIV"
 by (unfold transient_def, auto)

                  Un_Image, safe)
 apply (blast intro!: rev_bexI)+
 done
 
 lemma totalize_transientI: 
-    "[| act: Acts F;  A \<subseteq> Domain act;  act``A \<subseteq> -A |] 
+    "[| act \<in> Acts F;  A \<subseteq> Domain act;  act``A \<subseteq> -A |] 
      ==> totalize F \<in> transient A"
 by (simp add: totalize_transient_iff, blast)
 
 subsection\<open>ensures\<close>
 

 (** The most general rule: r is any wf relation; f is any variant function **)
 
 lemma leadsTo_wf_induct_lemma:
      "[| wf r;      
          \<forall>m. F \<in> (A \<inter> f-`{m}) leadsTo                      
-                    ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]  
+                    ((A \<inter> f-`(r\<inverse> `` {m})) \<union> B) |]  
       ==> F \<in> (A \<inter> f-`{m}) leadsTo B"
 apply (erule_tac a = m in wf_induct)
-apply (subgoal_tac "F \<in> (A \<inter> (f -` (r^-1 `` {x}))) leadsTo B")
+apply (subgoal_tac "F \<in> (A \<inter> (f -` (r\<inverse> `` {x}))) leadsTo B")
  apply (blast intro: leadsTo_cancel1 leadsTo_Un_duplicate)
 apply (subst vimage_eq_UN)
 apply (simp only: UN_simps [symmetric])
 apply (blast intro: leadsTo_UN)
 done

 
 (** Meta or object quantifier ? **)
 lemma leadsTo_wf_induct:
      "[| wf r;      
          \<forall>m. F \<in> (A \<inter> f-`{m}) leadsTo                      
-                    ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]  
+                    ((A \<inter> f-`(r\<inverse> `` {m})) \<union> B) |]  
       ==> F \<in> A leadsTo B"
 apply (rule_tac t = A in subst)
  defer 1
  apply (rule leadsTo_UN)
  apply (erule leadsTo_wf_induct_lemma)

 
 
 lemma bounded_induct:
      "[| wf r;      
          \<forall>m \<in> I. F \<in> (A \<inter> f-`{m}) leadsTo                    
-                      ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]  
+                      ((A \<inter> f-`(r\<inverse> `` {m})) \<union> B) |]  
       ==> F \<in> A leadsTo ((A - (f-`I)) \<union> B)"
 apply (erule leadsTo_wf_induct, safe)
 apply (case_tac "m \<in> I")
 apply (blast intro: leadsTo_weaken)
 apply (blast intro: subset_imp_leadsTo)