Email Gateway (Aug 22 2022 at 14:30): Email Gateway (Aug 22 2022 at 14:30):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
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.
Cheers,
René
theory Foo
imports Main
begin
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))"
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
Foo.thy
Email Gateway (Aug 22 2022 at 14:30):From: Peter Lammich <lammich@in.tum.de>
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.
Email Gateway (Aug 22 2022 at 14:30):From: Simon Wimmer <wimmersimon@gmail.com>
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
Last updated: Nov 21 2024 at 12:39 UTC