Re: [isabelle] Accessing (individual) simplification rules of function definitions

Dear Isabelle  Users,

In order to keep it in the same thread, I am pasting an answer Alexander
gave me about a remaining doubt I had concerning the main topic of all
these messages.


Hi Alfio,

I have small problem. Using 'primrec" I can access the individual rules
> both using subscripts and tags, as you suggested.
> But If i define using 'fun" it works only with subscripts. In the
> following small script, Isabelle (2009-2) can not process
> the last thm command. It sends an error message: unknown fact. Thanks
> for any help!

theory playing_tags

imports Main

   datatype Nat = Z | suc Nat

   primrec add::"Nat=>Nat=>Nat"
      add01:  "(add x Z) = x" |
      add02:  "(add x (suc y)) = suc(add x y)"

   thm "add.simps"
   thm "add.simps"(2)
   thm "add.simps"(1)
   thm "add.add01"
   thm "add.add02"

  fun sum::"Nat * Nat => Nat"
        sum01:  "sum(x,Z)=x" |
        sum02:  "sum(x,suc(y)) = suc(sum(x,y))"

  thm "sum.simps"
  thm "sum.simps"(1)
  thm "sum.simps"(2)
  thm "sum.sum01"

The function packages produces names without the function name as (optional)
qualifier. So plain "sum01" instead of "sum.sum01" works.
This should probably be made more uniform.

btw: you can inspect the theorems produced by a command by using
"print_theorems" afterwards.

On Fri, Aug 5, 2011 at 3:41 AM, Alexander Krauss <krauss at> wrote:

> On 08/05/2011 12:13 AM, Alfio Martini wrote:
>> Great!! Thanks for the quick reply!
>>  f.simps(2)
> You can also name the rules at definition time:
> fun/primrec f :: "..."
> where
>  name1: "..."
> | name2: "..."
> Alex

Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Porto Alegre - RS - Brasil

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