isabelle

0La chaleur

1Répondre

Comment définir une instance de classe de type_synonym?

type est une instance de classe semilattice_sup: datatype type = BType | IType | AType instantiation type :: semilattice_sup begin end Je suis en train de déclarer type × bool le type comme une

2La chaleur

1Répondre

Comment définir un prédicat constructif pour une carte?

Voici deux prédicats simples: definition map_is_empty :: "(string ⇒ nat option) ⇒ bool" where "map_is_empty env ≡ ∀x. env x = None" value "map_is_empty Map.empty" value "map_is_empty [''x''↦1]

1La chaleur

1Répondre

Noms de cas de règles d'induction (Isabelle)

Certaines règles d'induction ont des noms de cas: la valeur par défaut est case 0 et case (Suc n) par exemple. Étant donné une règle, par ex. int_induct, comment puis-je trouver ses noms de cas (si, e

0La chaleur

1Répondre

Comment définir Sup pour un type de données inductif?

Voici un système de types simple avec les types suivants: any, void, integer, real, set. datatype ty = AType | VType | IType | RType | SType ty Types forment un demi-treillis avec supremum:

2La chaleur

1Répondre

Comment utiliser des motifs complexes dans les fonctions?

Voici une fonction exemple: fun divide :: "enat option ⇒ enat option ⇒ real option" where "divide (Some ∞) _ = None" | "divide _ (Some ∞) = None" | "divide _ (Some 0) = None" | "divide (Some a

0La chaleur

2Répondre

Comment mapper les deux clés et les valeurs d'un mappage?

J'ai besoin de définir une fonction qui clés et des valeurs d'une carte finie en un ensemble de paires clé-valeur: theory Test imports Main "~~/src/HOL/Library/Finite_Map" begin definition den

0La chaleur

1Répondre

Comment définir un prédicat inductif dans les paramètres régionaux?

Voici un exemple d'un lieu simple: locale test = fixes test_less_eq :: "'a ⇒ 'a ⇒ bool" begin inductive test_eq where "test_less_eq x y ⟹ test_less_eq y x ⟹ test_eq x y" end Il défini

0La chaleur

1Répondre

Comment fusionner un ensemble de cartes finies?

je peux fusionner deux cartes finies comme suit: value "fmadd (fmap_of_list [(1::nat,2::nat)]) (fmap_of_list [(2::nat,3::nat)])" Mais lorsque je tente de fusionner un ensemble de cartes: v

0La chaleur

1Répondre

Comment définir un supremum sur un ensemble?

J'essaie de décrire un système de type d'un langage de programmation. Il a un sous-type commun pour tous types (VoidType) et un super-type commun pour tous types (AnyType): datatype type = VoidTy

0La chaleur

1Répondre

objectifs Réorganiser (Isabelle)

Je voudrais savoir comment réorganiser les objectifs dans la situation suivante: lemma "P=Q" proof (rule iffI, (*here I would like to swap goal order*), rule ccontr) oops Je voudrais une solut