[isabelle] Auto Method, Infinite Chain of Substitutiuons



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:

1. e \<in> I_SET ==> e \<in>  I_SET

2. e \<in> I_SET ==> S A v Y \<in> set [] --> (\<exists> v'. S  v' A Y'
\<in> set [])

3. \<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










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