[isabelle] Strange behaviour of Spec_Rules



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




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