Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Strange behaviour of Spec_Rules

view this post on Zulip Email Gateway (Aug 22 2022 at 10:39):

From: Manuel Eberl <eberlm@in.tum.de>
Hallo,

I just tried to use Spec_Rules to get function equations and noticed the
following strange behaviour (Isabelle 2015):

theory Scratch
imports Main GCD
begin

ML_val {*
Spec_Rules.retrieve @{context} @{term "map"}
|> map snd |> map snd |> flat
*}

val it =
["Lcm (?f ?A) = Lcm (?f ?A)",
"Gcd (?f ?A) = Gcd (?f ?A)",
"map ?f [] = []",
"map ?f (?x21.0 # ?x22.0) =
?f ?x21.0 # map ?f ?x22.0"]:
thm list

Where on earth do these strange reflexive Lcm/Gcd rules come from? My
guess is ‘gcd_lcm_complete_lattice_nat.SUP_def’, but why does it show up
in the result here?

Cheers,

Manuel

view this post on Zulip Email Gateway (Aug 22 2022 at 11:03):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Manuel,

the issue is straight-forward indeed.

In GCD.thy
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC