*To*: Lars Hupel <hupel at in.tum.de>*Subject*: Re: [isabelle] Ambiguous input*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Thu, 27 Nov 2014 15:59:24 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk, mahmoud abdelazim <m.abdelazim at icloud.com>*In-reply-to*: <54773925.2030601@in.tum.de>*References*: <9F1634CC-C88F-41BE-8A32-813B46921EFA@icloud.com> <54773925.2030601@in.tum.de>

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, René theory Test imports Main begin (* 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'']" end > Am 27.11.2014 um 15:45 schrieb Lars Hupel <hupel at in.tum.de>: > >> 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". > > > >

**References**:**[isabelle] Ambiguous input***From:*mahmoud abdelazim

**Re: [isabelle] Ambiguous input***From:*Lars Hupel

- Previous by Date: Re: [isabelle] Ambiguous input
- Next by Date: [isabelle] Fact completion
- Previous by Thread: Re: [isabelle] Ambiguous input
- Next by Thread: [isabelle] Fact completion
- Cl-isabelle-users November 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list