code_pred dans les paramètres régionaux

Question

Je souhaite créer un fichier exécutable inductive dans un locale. Sans le tout locale fonctionne très bien:

definition "P a b = True" 

inductive test :: "'a ⇒ 'a ⇒ bool" where 
    "test a a" | 
    "test a b ⟹ P b c ⟹ test a c" 

code_pred test . 

Cependant, lorsque je tente la même chose dans un locale, il ne fonctionne pas:

locale localTest 
begin 
definition "P' a b = True" 

inductive test' :: "'a ⇒ 'a ⇒ bool" where 
    "test' a a" | 
    "test' a b ⟹ P' b c ⟹ test' a c" 

code_pred test' 
end 

La ligne code_pred dans les paramètres régionaux renvoie l'erreur suivante:

Not a constant: test' 

Answer 1

Vous pouvez donner des règles d'introduction alternatives (voir isabelle doc codegen section 4.2 : Règles d'introduction alternatives) et éviter ainsi une interprétation. Cela fonctionne également pour les locales avec des paramètres (et même pour les constantes qui ne sont pas définies par induction). Une variante de votre exemple ayant un paramètre:

locale l = 
    fixes A :: "'a set" 
begin 
definition "P a b = True" 

inductive test :: "'a ⇒ 'a ⇒ bool" where 
    "a ∈ A ⟹ test a a" | 
    "test a b ⟹ P b c ⟹ test a c" 
end 

Nous introduisons une nouvelle constante

definition "foo A = l.test A" 

Et prouver ses règles d'introduction (donc la nouvelle constante est son w.r.t. l'ancien). Enfin, nous devons montrer que la nouvelle constante est également complète w.r.t. l'ancien:

code_pred foo by (unfold foo_def) (metis l.test.simps) 

Answer 2

Terminez deviner ici, mais je me demande si renommer test à test' a tout chambardé pour vous. (Pensez à changer code_pred test' à code_pred "test'".)

Answer 3

Exprimé sloppily, locales sont un mécanisme d'abstraction qui permet d'introduire de nouvelles constantes par rapport à certaines constantes hypothétiques satisfaisant des propriétés hypothétiques, alors que la génération de code est plus concret (vous avez besoin de toutes les informations qui sont nécessaires implémenter une fonction, pas seulement sa spécification abstraite). Pour cette raison, vous devez d'abord interpréter les paramètres régionaux avant de pouvoir générer du code. Bien sûr, dans votre exemple, il n'y a pas de constantes hypothétiques et propriétés, donc une interprétation est trivial

interpretation test: localTest . 

Après cela, vous pouvez utiliser

code_pred test.test' .