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 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"
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)
This archive was generated by a fusion of
Pipermail (Mailman edition) and