*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Auto Method, Infinite Chain of Substitutiuons*From*: attarzadeh at ee.sharif.ir*Date*: Thu, 9 Jun 2011 19:29:39 -0000*Importance*: Normal*User-agent*: SquirrelMail/1.4.19-2.fc10*Z-sharif-server-mailscanner*: Found to be clean

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

**Follow-Ups**:**Re: [isabelle] Auto Method, Infinite Chain of Substitutiuons***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Application order of (safe) introduction rules
- Next by Date: Re: [isabelle] Auto Method, Infinite Chain of Substitutiuons
- Previous by Thread: Re: [isabelle] Application order of (safe) introduction rules
- Next by Thread: Re: [isabelle] Auto Method, Infinite Chain of Substitutiuons
- Cl-isabelle-users June 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list