How to describe inaccuracy points inside (| |) in Isabelle?

Question 1

To concisely say that records x and y are equal except for field i, you can simply update field i in both records to the same dummy value and compare the results:

x⦇i := undefined⦈ = y⦇i := undefined⦈

Alternatively, you could quantify over the dummy value like this:

∀u. x⦇i := u⦈ = y⦇i := u⦈

The two forms are logically equivalent, although I suspect that the second form might be slightly more useful as a simp rule.

A third formulation is very similar to your attempt:

y = x⦇i := i y⦈

Beware that this form is not useful for simplification: since y appears also on the right-hand side, the rule would loop.

Question 2

I think your "for all item" approach seems quite reasonable here. Maybe it's a bit longer than absolutely necessary, but at least it's clear what you mean. In Isabelle syntax, you could write:

"∀i ∈ -{2,3,5}. f i = g i"

to state that f and g differ only on inputs 2,3, and 5. (The - indicates the complement of a set.)

Question 3

If you're asking about records specifically, then this may not be the right answer. I've only looked at "8.2 Records" [1] just enough to try and figure out what you're talking about.

If you are asking, "How do I keep from repeatedly having to enter the same, long, obnoxious syntax that clutters up my theorems?", then I might have an answer for your question.

Short answer: Use the Isar commands abbreviation, notation, and syntax to set up notation for functions and constants, when you want practical syntax that contains frequently used, long formulas. At first, you will struggle with the syntax for these commands, but the pain will pay off.

Another short answer: If you've figured out what your formula is, such as your for all item != i. y = x, and it's a predicate or some other formula that's in many of your formulas, then what I say below applies, and also, if you can define an abbreviation to eliminate much of your clutter, though maybe not all of it.

If you look at the Records.thy example, you'll see that they're defining a little bit of notation to make things more convenient.

An important thing to remember is to use abbreviation instead of definition, when you want the expansion of your abbreviation to automatically be part of your lemma.

My brief look at records

After briefly looking at records in 8.2, which is good info to know about, and which I wouldn't know about otherwise, I don't completely understand your first sentence. I didn't see anything that shows me I can use a variable for a field name, like this:

term "x(|  (i::int point_scheme => int) := 1  |)".

So, I take the point example from [1], and specify the following conditions, to try to come up with an example that's close to your first sentence:

x = p1, y = p2, i = Xcoord

(Ycoord p1) = (Ycoord p2) & p2 = p1(|Xcoord := 1|), or
p2 = p1(|Xcoord := 1, Ycoord := 1|)

My abbreviation below will be used like this, in relation to that first one:

xCONDyEQ(p1, p2, P) ==> p2 = p1(|Xcoord := 1|).

If, for example, P = (%i. 0 < i & i < 2), then the statement is true. My examples are not meant as solutions to your particular problem. I've found that it's work to try and find specialized notation that ends up being a good solution.

My example source is below. The examples I show are definitely not what my end choices would be if it was my syntax I was trying to optimize. I would select more graphical notation, but that's not good for SO and examples.

Also, it bugs me that in lemmas xp1 and xp2 that I'm passing a function, and that I'm having to use p1 and p2 twice in the formula. However, if I spent 8 hours trying to come up with a cleaner solution, I would have spent 8 hours to define your notation, and as it is with personal preferences, you might hate it, and I'm not clear on what you're asking.

I actually did spend another n minutes to use syntax to overload notation, to get the following equivalencies, where both notations are abbreviations for the same function:

xpCOND(p,P) = xCONDyEQ(p,p,P)
ypCOND(p,P) = yCONDxEQ(p,p,P)

It is the syntax command that will cause you hours and days of grief. Having done it gets me one step closer to not having to think real hard to get it done.

My answer here about notation and syntax shows that these kind of solutions to problems are application specific, and it's the user, not the developers, who needs to brainstorm to come up with a decent solution to keep from having to use massive amounts of syntax to state a theorem.

You don't necessarily want to try and get too fancy. You can define syntax to get shorter syntax, but it can be too specific, to where you're defining too much specialized syntax. My example xp4 below is to try to make that point.

Recently, I decided something like isP_andIsEq(D,C,x,y) would be worse than something like isP(D,C) ==> x = y. The idea is to utilize the standard syntax of Isabelle/HOL as much as possible.

(******************************************************************************)
(* POINT RECORD: **************************************************************)

record point = 
  Xcoord :: int 
  Ycoord :: int (*page 154 of tutorial.pdf*)

(******************************************************************************)
(* ABBREVIATIONS: *************************************************************)
(* xCONDyEQ(p1, p2, x coord property fun), p1 and p2 y coordinates are equal.**)
(* yCONDxEQ(p1, p2, y coord property fun), p1 and p2 x coordinates are equal.**)
(******************************************************************************)

abbreviation (input) point_0_0 :: "point" where
  "point_0_0 == (|Xcoord = 0, Ycoord = 0|)"
notation
  point_0_0 ("'(||')")

abbreviation (input) p2_x_cond_y_eq 
  :: "point => point => (int => bool) => bool" where 
  "p2_x_cond_y_eq p1 p2 P == P(Xcoord p2) ∧ (Ycoord p1 = Ycoord p2)"
notation (input)
  p2_x_cond_y_eq ("xCONDyEQ'(_, _, _')")
syntax 
  "_xcond" :: "point => (int => bool) => bool" ("xpCOND'(_, _')")
translations
  "xpCOND(p,P)" => "xCONDyEQ(p,p,P)"

abbreviation p2_y_cond_x_eq :: "point => point => (int => bool) => bool" 
  where "p2_y_cond_x_eq p1 p2 P == P(Ycoord p2) ∧ (Xcoord p1 = Xcoord p2)"
notation (input)
  p2_y_cond_x_eq ("yCONDxEQ'(_, _, _')")
syntax 
  "_ycond" :: "point => (int => bool) => bool" ("ypCOND'(_, _')")
translations
  "ypCOND(p,P)" => "yCONDxEQ(p,p,P)"

lemma xp1: 
  "xCONDyEQ(p1, p2, (%i. i > 0 & i < 2)) ==> p2 = p1(|Xcoord := 1|)"
  by(auto)

lemma xp2: 
  "xpCOND(p2, (%i. i = 0)) & 
   ypCOND(p2, (%i. i = 0)) ==> p2 = (||)"
by(auto)

lemma xp3: 
  "xCONDyEQ(p1, p2, (%i. i > 0 & i < 2)) & 
   yCONDxEQ(p1, p2, (%i. i > 0 & i < 2))
     ==> p2 = p1(|Xcoord := 1, Ycoord := 1|)"
  by(auto)

(******************************************************************************)
(* ALL-IN-ONE OPERATOR ********************************************************)
(******************************************************************************)

(*It's tempting to want to put bool operators in your abbreviated function, but  
  it may be better to figure out a predicate to be used with ==>, so that you 
  have `P p2 ==> f p1 p2*)

abbreviation O_p2_x_cond_y_eq :: "point => point => (int => bool) => bool" 
  where "O_p2_x_cond_y_eq p1 p2 P == 
     P(Xcoord p2) ∧ (Ycoord p1 = Ycoord p2) --> p1 = p2"
notation (input)
  O_p2_x_cond_y_eq ("xCONDyEQ'_yEQ'(_, _, _')")

lemma xp4: 
  "xCONDyEQ_yEQ( p1(|Xcoord := 1|), p2, (%i. i > 0 & i < 2) )"
by(simp)