Re: [isabelle] nat_code Equation



>> fun foo where
>>  "foo xs 0 = True"
>> | "foo [] (Suc _) = False"
>> | "foo (x # xs) (Suc n) = foo xs n"
>> 
>> export_code foo in Haskell file -
>> 
>> complains about
>> 
>> "Nat.Suc" is not a constructor, on left hand side of equation, in theorem:
>> foo [] (Suc ?uu) ≡ False
> 
> The ML setup in Code_Nat.thy is intended to automatically translate
> away patterns involving Suc, so that you don't have to do it yourself.
> Unfortunately the translation is kind of picky; it only works if for
> each rule with a "Suc n" pattern, there is a matching rule with a "0"
> pattern in its place.

I understand.

> E.g. the following modification works with
> Code_Nat.thy in Isabelle2012:
> 
> fun foo where
>  "foo [] 0 = True"
> | "foo (x # xs) 0 = True"
> | "foo [] (Suc _) = False"
> | "foo (x # xs) (Suc n) = foo xs n"
> 
> But instead of changing your code, please try out the attached version
> of Code_Nat.thy, where I have modified the code preprocessor.

Thanks Brian, for the new version of Code_Nat. Unfortunately, it works for foo, 
but not for other functions. A minimized example that fails is as follows:

fun double :: "nat ⇒ nat" where
  "double 0 = 0"
| "double n = n + n"

export_code double in Haskell file -

Constructor as head in equation:
nat_of_num ?n ≡ plus_nat_inst.plus_nat (pred_numeral ?n) (nat_of_num num.One) 

René




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