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



ÂÂ
> 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.