Email Gateway (Aug 18 2022 at 17:47): Email Gateway (Aug 18 2022 at 17:47):From: attarzadeh@ee.sharif.ir
Hi,
As a beginner, I've written the following theory: (the inductive set is a
a security protocol model and AG, M ,and E stand for Agent, Message and
Event in the message.thy and event.thy theory files. I've just
simplified these datatypes and written the following theory)
datatype AG = A| F nat
datatype M = AG | nat
datatype E = S AG AG M | N AG M
inductive_set I_SET :: "E list set"
where
NIL : "[] \<in> I_SET"
| I_SET1 : "[| e1 \<in> I_SET |] ==> S v1 A m1 #e1 \<in> I_SET "
| I_SET2 : "[| e2 \<in> I_SET; S v2 A m1 \<in> set e2 |] ==> S A v2 m2#e2
\<in> I_SET "
lemma L1 : "[| S A v Y \<in> set e; e \<in> I_SET |] ==>(\<exists> v'. S
v' A Y' \<in> set e ) "
apply (erule rev_mp)
apply(rule I_SET.induct)
apply auto
After applying induction on the set (second line of the
proof script) I got the following subgoals:
e \<in> I_SET ==> e \<in> I_SET
e \<in> I_SET ==> S A v Y \<in> set [] --> (\<exists> v'. S v' A Y'
\<in> set [])
\<forall> e1 v1 m1. [| e \<in> I_SET; e1 \<in> I_SET; S A v Y \<in>
set e1 --> (\<exists> v'. S v' A y' \<in> set e1 )|] ==> S A v Y \<in>
set (S v1 A m1 # e1) --> (\<exists> v'. S v' A y' \<in> set (S v1 A m1
#e1))
4.\<forall> e2 v2 m m2. [| e \<in> I_SET; e2 \<in> I_SET; S A v Y \<in>
set e2 --> (\<exists> v'. S v' A y' \<in> set e2 ); S v2 A m1 \<in> set
e2|] ==> S A v Y \<in> set (S A v2 m2 # e2) --> (\<exists> v'. S v' A y'
\<in> set (S A v2 m2#e2) )
First and second subgoals are trivial and the third and forth subgoals seem
to be provable by a suitable substitution, but when I apply the auto
method, an infinite chain of variable substitutions occurs and it could not
be proved.
What can I do to proceed?
I'm really confused about it,
So Any help or comments would be really appreciated
__
Hoori
Email Gateway (Aug 18 2022 at 17:47):From: Tobias Nipkow <nipkow@in.tum.de>
There are two small problems:
Note, however, that in general auto can indeed fail to terminate, and
then you may need to do the proof in more detail. For such cases I
recommend the structured proof language, not apply.
Tobias
Last updated: Apr 24 2024 at 04:17 UTC