Isabelle: commandes/variables locales syntaxiques/abréviations syntaxiques

Question

Je veux écrire plusieurs formules qui incluent une combinaison de variable commune, mais je suis fainéant donc je veux avoir une variable syntaxique.

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

Au lieu d'écrire « a + b » à chaque fois que je voudrais être abled écrire quelque chose comme:

X == a + b 

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

Avec les mêmes fonctionnalités que LaTeX il a la commande \ include. il devrait encore identifier "X - e - a" comme "b - e".

Answer 1

La réponse courte

Le chemin par défaut est d'utiliser abbreviation. Cela introduit une abréviation purement syntaxique qui sera étendue lors de l'analyse. Si le a et b dans votre cas sont des termes fixes comme 1+2 et 3+4, vous pouvez simplement faire ceci:

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

puis écrire X + c, X - c, X - e - a. Notez également que les abréviations sont repliées avant l'impression, c'est-à-dire que (1 + 2) + (3 + 4) + 5 sera imprimé en tant que X + 5. Si vous ne le souhaitez pas, vous pouvez utiliser abbreviation (input) à la place.

Notez également que 5 + (1 + 2) + (3 + 4) sera pas imprimer comme 5 + X et est pas syntaxiquement les mêmes que 5 + X parce que les associés d'addition à gauche: 5 + (1 + 2) + (3 + 4) est-(5 + (1 + 2)) + (3 + 4), alors que 5 + X est 5 + ((1 + 2) + (3 + 4)).

Vous pouvez également utiliser definition; ceci introduit une nouvelle constante appelée X. Vous pouvez déplier la définition en utilisant le théorème X_def. Mais d'après votre question, je suppose que vous ne le voulez pas.

Qu'en est-il des variables?

Il est pas tout à fait claire de votre question, mais je pense que votre situation est quelque chose comme ceci:

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

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

Dans ce cas, vous ne pouvez pas utiliser une abréviation comme ci-dessus, puisque a et b sont des variables et vous ne peut pas avoir de variables libres sur le côté droit d'une abréviation (ou d'une définition). Vous pouvez toutefois fixer localement les variables dans un contexte anonyme:

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 

Le lemmes foo et bar sont ensuite exportés avec les variables libres fixes a et b généralisées à des variables schématiques de la manière habituelle. Cependant, thm foo sera imprimé comme ?P (X (X ?a ?b) 3), ce qui est un peu étrange, et, en fait, toute occurrence de + sera imprimée de cette façon, donc faire abbreviation (input) est une bonne idée dans tous les cas.

Une note sur l'hygiène

l'espace de noms global Polluer avec un nom aussi général que cela est généralement considéré comme mauvais style.Une alternative à l'aide d'une définition locale serait ceci:

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 

Ici, X est non seulement une abréviation syntaxique, mais une nouvelle constante dont la définition doit être déplié. Cependant, en déclarant la règle simp, ce déploiement se fera automatiquement. Il ne sera cependant pas replié automatiquement, donc vous ne verrez jamais X dans la sortie après avoir utilisé le simplificateur. À la sortie du contexte, la définition sera dépliée partout et disparaîtra, vous donnant les lemmes que vous voulez.