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.


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