Re: [isabelle] Isabelle-2016-1, RC-4, simplifier and auto behavior



Btw,
the comment for mk_auto_tac in clasimp.ML reads:

Designed to be idempotent, except if Blast.depth_tac instantiates variables
  in some of the subgoals

Simon

On Wed, Nov 30, 2016 at 1:14 PM Peter Lammich <lammich at in.tum.de> wrote:

>
> > lemma get_unit: "get_unit t = ()" by simp
> > thm get_unit[unfolded get_unit.simps]
> >
> > (* produces the expected result
> >   (case ?t of Fun f ts â undefined (map get_funs ts)) = ()
> >   in Isabelle 2016, but the unfolding loops in Isabelle 2016-1 RC4 *)
>
> Makarius changed the implementation of unfold, in particular, no
> [abs_def] is needed any more. This effect is probably related to that.
>
>
> >
> >
> > text âObservation 2: auto is not idempotent.â
>
> I made the same observation already, but could not yet figure out what
> the exact problem is. I think auto was never intended to be idempotent,
> but it's just a matter of experience: Experience says it should be
> idempotent here, but in 2016-1-RC2 it turns out to be not.
>
> --
>   Peter
>
> >
> > fun funas_term :: "term â (int à nat)set" where
> >   "funas_term (Fun f ts) = {(f, length ts)} â â(set (map funas_term
> > ts))"
> >
> > context
> >   fixes F :: "(int à nat)set"
> >   and comb :: "term list â term"
> >  assumes comb: "funas_term (comb ts) â F â (â (funas_term ` set
> > ts))"
> > begin
> > fun comb_term :: "term â term"
> > where
> >   "comb_term (Fun f ts) =
> >     (if (f,length ts) â F then Fun f (map comb_term ts)
> >     else comb (map comb_term ts))"
> >
> > lemma funas_term_clean_comb_term: "funas_term (comb_term t) â F"
> > proof (induct t)
> >   case (Fun f ts)
> >   show ?case
> >   proof (cases "(f,length ts) â F")
> >     case True
> >     with Fun show ?thesis by auto
> >    (* Here, one "auto" suffices in Isabelle 2016, whereas a single
> > auto is not sufficient in RC4.
> >       In RC4 one needs "by (auto, auto)" *)
> >   next
> >     case False
> >     hence id: "comb_term (Fun f ts) = comb (map comb_term ts)" by
> > simp
> >     show ?thesis unfolding id using comb[of "map comb_term ts"] Fun
> > by auto
> >   qed
> > qed
> > end
> >
> > end
> >
> >
>
>



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