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.

Best!
----------------------------------------------xxxxxxxx--------------------------------------------------

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
begin

   datatype Nat = Z | suc Nat

   primrec add::"Nat=>Nat=>Nat"
   where
      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"
    where
        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"
end


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.

Alex
--------------------------------------------xxxxxxxxxxxxxxxx------------------------------------------
On Fri, Aug 5, 2011 at 3:41 AM, Alexander Krauss <krauss at in.tum.de> 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.