Email Gateway (Aug 19 2022 at 16:32): Email Gateway (Aug 19 2022 at 16:32):From: mahmoud abdelazim <m.abdelazim@icloud.com>
Hi
Test.thy
Email Gateway (Aug 19 2022 at 16:32):From: Lars Hupel <hupel@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".
Email Gateway (Aug 19 2022 at 16:32):From: René Thiemann <rene.thiemann@uibk.ac.at>
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
Last updated: Apr 26 2024 at 01:06 UTC