[isabelle] How to unify the premises with my rule?



Hello
  I am a newbie in isabelle ,and now I am stucked with a proof which looks somewhat trivial. I am using Isabelle2005/HOL with ProofGeneral, the proof is :
  !! v s1 s2 .
  [| Subject_user v s1 \<in> Users v ; Subject_user v s2 \<in> Users v ; Subject_user v s1 = Subject_user v s2
    Subject_role v s1 \<in> tRoles v \/ Subject_role v s1 \<in> nRoles v ;
    Subject_role v s2 \<in> tRoles v \/ Subject_role v s2 \<in> nRoles v ;
    s1 \<in> tSubjects v \/ s1 \<in> nSubjects v;
    s2 \<in> tSubjects v \/ s2 \<in> nSubjects v;
    s1 \<noteq> s2;
    (Subject_user v s1 , Subject_role v s1) \<in> URs v;
    (Subject_user v s2 , Subject_role v s2) \<in> URs v;
   
   \<forall> u r1 r2 .
     u \<in> Users v /\
     (r1 \<in> tRoles v \/ r1 \<in> nRoles v) /\
     (r2 \<in> tRoles v \/ r2 \<in> nRoles v) /\
     (EX s1. (s1 \<in> tSubjects v \/ s1 \<in> nSubjects v) /\
             (EX s2. (s2 \<in> tSubjects v \/ s2 \<in> nSubjects v) /\
                     s1 \<noteq> s2 /\
                     u = Subject_user v s1 /\ u = Subject_user v s2 /\
                     r1 = Subject_role v s1 /\ r2 = Subject_role v s2 /\
                     (u, r1) \<in> URs v /\ (u, r2) \<in> URs v)) -->
      (r1, r2) \<notin> DMRs v /\ (r2, r1) \<notin> DMRs v;       
 |]
 ==> (Subject_role v s1, Subject_role v s2) \<notin> DMRs v /\ (Subject_role v s2, Subject_role v s1) \<notin> DMRs v

Sorry for the extreme long proof .Here is some explanation on the notations :
1 . v is a record
2 . (Subject_role v) is a fuction which takes a subject and return its role
3 . (Subject_user v) is a function which takes a subject and return its user
4 . (Users v) ,(tRoles v) , (nRoles v) , (tSubjects v) , (nSubjects v) , (URs v) , (DMRs v) are all sets of the record v

You can see the last one of the premises is a derivation rule, and the others could satisfy the assumption of the rule.
So it is supposed to prove the conclusion ,but I failed to unify the premises with the rule in the premises.
Could anyone give me some help on this ? IF POSSIBLE , could you show the proof step by step?

Thanks in advance

                                                            Kun  Chen
                                                            Foundation Software Engineer Center
                                                            Institute of  Software
                                                            Chinese  Academy of  Science


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.