Re: [isabelle] Auto Method, Infinite Chain of Substitutiuons



There are two small problems:

- Induction needs to be applied with erule, not rule.
- You also need the quantify Y', not only v'.

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

Am 09/06/2011 21:29, schrieb attarzadeh at ee.sharif.ir:
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)





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