[isabelle] How to unify the premises with my rule?
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: [isabelle] How to unify the premises with my rule?
- From: "chen kun" <coolchenice81 at gmail.com>
- Date: Fri, 17 Mar 2006 11:20:27 +0800
- Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:to:subject:mime-version:content-type; b=LrfhYW0qnV35l3FFqb+rl1S/bWGU6p52FJAftDWTUumsYgaZ6na18abEenMFG1mAFlEt1GDAPF6MPzQxsIoMUQp1G0j61mRpN3ilnX1kZYrzdHcg5WHcRHtDhlH4P96NJu4iiQNUCliLZRwOs5sl1u0P639RusHjq40tY9/9bk8=
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
Foundation Software Engineer Center
Institute of Software
Chinese Academy of Science
This archive was generated by a fusion of
Pipermail (Mailman edition) and