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

Dear all,

during porting our theories from Isabelle 2016 to 2016-1-RC4, I made two strange observations where I donât know whether these have been intended.


theory Foo
  imports Main

datatype "term" = Fun int "term list" 

text âObservation 1: change of simplifier behaviour which more often leads to nontermination.â

fun get_unit :: "term â unit" where
  "get_unit t = (case t of Fun f ts â undefined (map get_unit ts))" 
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 *)

text âObservation 2: auto is not idempotent.â
fun funas_term :: "term â (int à nat)set" where
  "funas_term (Fun f ts) = {(f, length ts)} â â(set (map funas_term ts))"

  fixes F :: "(int à nat)set" 
  and comb :: "term list â term" 
 assumes comb: "funas_term (comb ts) â F â (â (funas_term ` set ts))" 
fun comb_term :: "term â term"
  "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)" *)
    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


Attachment: Foo.thy
Description: Foo.thy

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