isabelle

0La chaleur

1Répondre

corecursive inattendue Ce (coupé out) de définition de la fonction corecursive Isabelle primcorec tree :: "'form fset ⇒ 'vertex ⇒ 'preform ⇒ (('form fset × 'form), ('rule × 'preform) NatRule) dtree" w

5La chaleur

2Répondre

Isabelle2016 et Proof Général

J'ai essayé d'apprendre à utiliser Isabelle 2016. Alors qu'en principe j'aime l'idée de vérification asynchrone, je n'aime pas Isabelle/jEdit pour plusieurs raisons, dont la plus sévère c'est qu'il ut

0La chaleur

1Répondre

obligation Isabelle classe prouver bleu

Isabelle Je le fichier suivant theory Scratch imports Main begin class named = fixes getName :: "'a ⇒ string" class node = named datatype Node = node string fun getName_Node :: "Node ⇒

0La chaleur

1Répondre

se déroule automatiquement une définition d'enregistrement lorsque accesseur est utilisé

Supposons que j'ai un type d'enregistrement et une définition constante de ce type, comme: record r = r_x :: int r_y :: int r_z :: int definition "a ≡ ⦇r_x=1, r_y=2, r_z=3⦈" Mainten

0La chaleur

1Répondre

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

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

0La chaleur

1Répondre

Discriminant avec Inégalités

Je suis assez nouveau avec Isabelle. J'ai essayé de trouver lemme pour résoudre ce lemma fixes x y z k :: real assumes "x ≠ 0" and "⋀k. (x*(k)⇧2 + y*k + z) ≥0" shows "discrim x y z ≤ 0"

0La chaleur

1Répondre

Prouver la commutativité d'ajouter, Prendre 2

Cette question est un suivi à la question suivante isabelle proving commutativity for add, mon suivi était trop long pour être un commentaire. Le problème comme indiqué était de montrer la commutativi

0La chaleur

1Répondre

Création d'un type de données avec les inégalités Isabelle

Je suis très nouveau à Isabelle et essaie de mettre en œuvre un type de données tels que fruit = pomme datatype | Banane | Cantaloup (choix de mots sont ineptes ici pour ne pas le confondre avec essay

0La chaleur

1Répondre

En attente des hypothèses type

Quelle pourrait être la raison pour laquelle le message d'erreur suivant: Pending sort hypotheses: trelations Ici, trelations est un type de classe l'erreur est généré lorsque la preuve d'un collect

0La chaleur

1Répondre

Isabelle Logic test de déduction naturelle simple

http://pastebin.com/1ZEt9r32 Qu'est-ce qui ne va pas avec la ligne 30? Isabelle dit ceci "Impossible de terminer proof⌂: objectif (2 objectifs secondaires): 1. ¬ P ⟹ Q 2. Q ⟹ ¬ P" C'est une théorie po