Re: [isabelle] Ambiguous input

Dear Mahmoud,

as Lars already wrote, the problem is that "[a/b]" may be the singleton list with the one element: "a divided by b".
But unlike to Lars I only detect the ambiguity first in the abbreviation, not in the function definition:

After the abbreviation, a term like "p[x/a]" could either be the substb-function with arguments p, x, and a, or, 
it can be a function "p" applied to the list "[x/a]".

Best regards,

theory Test
imports Main 

(* added 
type_synonym vname = string
datatype aexp = V vname | N nat
datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp

fun subst :: "vname ⇒ aexp ⇒ aexp ⇒ aexp" where
"subst x a (V v) = (if x = v then a else (V v))" |
"subst x a (N n) = N n"

fun substb :: "vname => aexp => bexp => bexp" where
"substb x a (Bc v) = Bc v" |
"substb x a (Not b) = Not (substb x a b)" |
"substb x a (And b1 b2) = And (substb x a b1) (substb x a b2)" |
"substb x a (Less a1 a2) = Less (subst x a a1) (subst x a a2)"

abbreviation b_subst :: "bexp => aexp => vname => bexp"
  ("_[_'/_]" [1000,0,0] 999)
where "p[a/x] == substb x a p"

value " (And (Less (V ''x'') (N 1)) (Bc True))[(N 1)/''x'']"

> Am 27.11.2014 um 15:45 schrieb Lars Hupel <hupel at>:
>> in Test.thy file i have made an abbreviation subset_b
>> but in output it gave me in output an Ambiguous input but i don’t know why ? and where is the problem ?
> The problem already occurs earlier, in your function definition:
>> Variable "subst" occurs on right hand side only:
>> ⋀x a a1 a2 subst. substb x a (Less a1 a2) = Less (subst x a a1) (subst x a a2)
> It seems to me that you defined "subst" somewhere else, but didn't
> include it in the theory file you attached.
> After fixing this, the ambiguity error goes away. You might still want
> to define some other syntax, or at least give a fixity annotation,
> because "[a/b]" could also denote the list containing the value "a/b".

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