Email Gateway (Aug 17 2022 at 14:14): Email Gateway (Aug 17 2022 at 14:14):From: chen kun <coolchenice81@gmail.com>
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
Email Gateway (Aug 17 2022 at 14:14):From: Lawrence Paulson <lp15@cam.ac.uk>
Thanks for your question. The problem here is that you aren't using
Isabelle in the way it's designed to be used, specifically with
regard to unification. Your problem would be trivial for first-order
automatic provers. It is perhaps easy enough for Isabelle to prove
with its "meson" method, but not using its basic tools.
To simplify your example considerably, if you have a formula like
ALL x. P x & (EX y. Q(x,y)) --> R x
then its natural Isabelle form is
[| P(x); Q(x,y) |] ==> R(x)
and this can trivially be used to reduce subgoals of the form R(...).
That is, you need to express your big quantified formula as shown
above and give it to the "rule" method.
Larry Paulson
Last updated: May 03 2024 at 04:19 UTC