Isabelle: команды/синтаксические локальные переменные/синтаксические сокращения

Question

Я хочу написать несколько формул, содержащих общую комбинацию переменных, но я ленив, поэтому хочу иметь синтаксическую переменную.

IE "a + b + c" 
"a + b - c" 
"a + b + e - a" 

Вместо того чтобы писать «а + Ь» каждый раз, когда я хотел бы недееспособным написать что-то вроде:

X == a + b 

"X + c" 
"X - c" 
"X - e - a" 

С той же функциональностью, как LaTeX имеет его с \ включает команду. он все равно должен идентифицировать «X - e - a» как «b - e».

Answer 1

Короткий ответ

По умолчанию это является использование abbreviation. Это вводит чисто синтаксическую аббревиатуру, которая будет расширяться во время разбора. Если a и b в вашем случае фиксируются такие термины, как 1+2 и 3+4, вы можете просто сделать это:

abbreviation "X ≡ (1 + 2) + (3 + 4)" 

, а затем написать X + c, X - c, X - e - a. Также обратите внимание, что аббревиатуры складываются перед печатью, то есть (1 + 2) + (3 + 4) + 5 будет напечатано как X + 5. Если вы этого не хотите, вместо этого вы можете использовать abbreviation (input).

отметить также, что 5 + (1 + 2) + (3 + 4) будет не быть напечатан как 5 + X и не синтаксический так же, как 5 + X, потому что аддитивные сопоставляют слева: 5 + (1 + 2) + (3 + 4) является (5 + (1 + 2)) + (3 + 4), в то время как 5 + X является 5 + ((1 + 2) + (3 + 4)).

Вы также можете использовать definition; это вводит новую константу, называемую X. Вы можете развернуть определение, используя теорему X_def. Но из вашего вопроса я понимаю, что вы этого не хотите.

Как насчет переменных?

Это не совсем ясно из вашего вопроса, но я предполагаю, что ваша ситуация чем-то вроде этого:

lemma foo: "P (a + b + c)" 
(* some proof *) 

lemma bar: "P (a + b - c)" 
(* some proof *) 

В этом случае вы не можете использовать аббревиатуру, как указано выше, так как a и b являются переменными и вы не может иметь свободных переменных в правой части аббревиатуры (или определения). Вы можете, однако, локально устранить переменные в анонимной контексте:

context 
    fixes a b :: "'a :: ring_1" (* change this type if necessary *) 
begin 

abbreviation "X ≡ a + b" 

lemma foo: "P (X + 3)" 
(* some proof *) 

lemma bar: "P (X - 3)" 
(* some proof *) 

end 

Лемма foo и bar затем экспортируются с фиксированным свободными переменными a и b обобщается на схематические переменные обычном способе. Однако thm foo будет напечатано как ?P (X (X ?a ?b) 3), что немного странно, и, фактически, любое вхождение + будет напечатано таким образом, поэтому abbreviation (input) - хорошая идея в любом случае.

записку о гигиене

загрязняя глобальное пространство имен с именем, как вообще, так как это, как правило, считается плохим стилем.Альтернатива с использованием локального определения будет следующим образом:

context 
    fixes a b :: "'a :: ring_1" 
    fixes X defines X_def[simp]: "X ≡ a + b" 
begin 

lemma foo: "P (X + 3)" 
sorry 

lemma bar: "P (X - 3)" 
sorry 

end 

Здесь X не просто синтаксическая аббревиатура, а новая константа, определение должны быть развернуты. Однако, объявив определение правилом simp, это разворачивание будет выполнено автоматически. Однако он не будет автоматически складываться автоматически, поэтому вы никогда не увидите X на выходе после использования на нем упростителя.

После выхода из контекста определение будет разворачиваться повсюду и исчезает, предоставляя вам нужные вам лемм.