Skip to main content
Filter by
Sorted by
Tagged with
2 votes
0 answers
34 views

Bad session in Isabelle

I am trying to run Incompleteness from afp-2019-08-19 on Isabelle2023. When I open the ROOT file chapter AFP session Incompleteness (AFP) = HereditarilyFinite + description "The Incompleteness ...
God bless's user avatar
  • 121
0 votes
0 answers
22 views

Access functions from an imported theory in Isabelle/ML

I have an Isabelle theory here: theory Even imports Main begin notation Suc ("S") fun even:: "nat ⇒ bool" where "even 0 = True" | "even (S n) = (¬even n)" ...
Michael's user avatar
  • 216
1 vote
1 answer
49 views

Define evaluable inductive predicate for a record and set

I'm trying to define an inductive predicate for some graph calculations: type_synonym node = nat type_synonym edge = nat record graph = nodes :: "node set" edges :: "edge set" ...
Denis's user avatar
  • 1,219
3 votes
1 answer
40 views

Overloading operators and theorems over isomorphic datatypes in Isabelle

I want to represent durations in Isabelle and exploit type safety. Naturally, I do: datatype seconds = Seconds (secs: nat) datatype minutes = Minutes (mins: nat) That way, the type system will warn ...
math2001's user avatar
  • 4,414
0 votes
0 answers
42 views

How do I fold a function over the bindings in a map in Isabelle?

What I want to be able to do is fold a function over the bindings in a map, and look up keys. Coq has the FMap modules, is there a similar Isabelle theory module? https://coq.inria.fr/doc/v8.19/stdlib/...
Glyn Webster's user avatar
0 votes
1 answer
46 views

Function that constructs a Set of all elements that statisfy a given condition in Isabelle

I am trying to learn set construction in Isabelle but I am failing. Consider you want a function that gives you all natural numbers that are smaller than a given number. I thought this should work: ...
Jonas's user avatar
  • 75
2 votes
1 answer
58 views

Recursive function on finite sets - how to prove termination

I am (still) struggling with a recursive function on finite sets. I would like to define a special Cartesian product on a finite set of (finite) sets. A simplified example of what I am trying to ...
Alicia M.'s user avatar
1 vote
1 answer
42 views

Some problems using maps in Isabelle/HOL

Two questions about mappings: [1] This lemma is trivial lemma [simp] : "(m(x ↦ v))|` {x} = [x ↦ v]" but how can I prove these two lemmas? lemma : "(m(x ↦ v))|`(dom(m) - {x}) = m" ...
Montserrat Hermo's user avatar
0 votes
0 answers
33 views

Simplifying expressions of classical propositional logic in isabelle

I'm new to isabelle and I wanted to use something like automatically simplifying a propositional expression for educational purposes by showing the steps and rules applied. I'm guessing it's a ...
Rodolpho Pueyrredón's user avatar
1 vote
1 answer
43 views

Cannot access definition in HOL.Bit_Operations

How can I properly import the definition of bit_nat from HOL.Bit_Operations? Working code, with copying the definition into current theory: theory Scratch imports Main begin definition bit_nat :: ‹...
TFuto's user avatar
  • 1,442
0 votes
1 answer
36 views

Filtering on sets of sets

I am working with sets of sets, where the internal sets are representation of objects, i.e. the elements of internal sets are pairs of the form (attribute, value). In a simplified, toy example, I have ...
Alicia M.'s user avatar
0 votes
0 answers
18 views

Proving state sequence properties through sets

I have recursive datatype state and several operations on it: datatype state = emptyState | toEnv state | setVarBool state variable bool | setVarInt state variable int | setVarNat state ...
bearhug15's user avatar
0 votes
0 answers
60 views

Proof on inductive sets

I am trying to wrap my brain around proofs on inductive sets and I am failing miserably. This is what I have so far: theory MyTheory imports Main begin inductive_set S where emptyI: "{} ∈ S&...
Alicia M.'s user avatar
0 votes
0 answers
72 views

Isabelle/HOL: How to handle `let` and `if`?

I'm completely new to Isabelle/HOL and trying to read the Concrete Semantics book. I'm stuck with one of the very first exercises: Exercise 2.3. Define a function count :: ′a ⇒ ′a list ⇒ nat that ...
kjam's user avatar
  • 829
0 votes
1 answer
67 views

Exists irrational number: sqrt fails to refine pending goal

In Isabelle, why does this theory Example imports "HOL-Examples.Sqrt" begin theorem exists_irrational_number: "∃x. x ∉ ℚ" proof (rule exI) show "sqrt 2 ∉ ℚ" using ...
Matthias's user avatar
  • 737
0 votes
1 answer
64 views

Proof by reductio ad absurdum in Isabelle

I understand how ccontr works, however I am unsure how (or even if it is possible) to use it on a lemma declared with assumption(s). Take this simple example, all is good: lemma l1: "A⊆B ⟶ A ∩ B =...
Alicia M.'s user avatar
1 vote
0 answers
38 views

I have a problem in Isabelle related to 'Clash of types' that I am unable to solve. Could someone help me?

I would want to formalise a calculus in Isabelle. I started with this definitions: type_synonym Signature = "string ⇀ nat" type_synonym 'a Interpretation = "string ⇀ 'a list set" ...
Montserrat Hermo's user avatar
0 votes
1 answer
79 views

Customized datatype

I am trying to create a datatype with rules, so to speak, and I am unsure where to start (assuming it is possible!). For example, I have a datatype, a pair (kind, value) defined as a record. I would ...
Alicia M.'s user avatar
0 votes
0 answers
59 views

How to improve a LH=RH chain proof

I am tying to get a better understanding how Isabelle manages the chain proofs, specifically when associativity/commutativity is involved. Imagine I have a binary non-homogeneous operator op that is ...
Alicia M.'s user avatar
0 votes
1 answer
89 views

Locale inheritance after interpretation

I am trying to understand how "inheritance" work at locale/interpretation level. I have an abstract locale (locA), with a method (g) defined within it. I have a concrete locale (locB), which ...
Alicia M.'s user avatar
1 vote
1 answer
125 views

How to verify C functions with array parameters using Isabelle

I am using Isabelle to verify a C program. During the verification process, I used the c-parser install-C-file to load the code, but the following issue occurred: attempt to cause decay to pointer on ...
riiiiyueeeejiiiiiiuzhao's user avatar
0 votes
1 answer
80 views

Is it possible to define a context for syntax rules?

I'm trying to define a syntax for a C-like language. Let's for the sake of simplicity it has only arithmetic expressions, variable declarations and blocks of statements: type_synonym vname = nat ...
Denis's user avatar
  • 1,219
0 votes
1 answer
68 views

stuck on a proof (modeling IMP language)

I've been trying 'port' some of the imperative language (IMP2) formalized in Isabelle here: https://www.isa-afp.org/sessions/imp2/#Semantics.html to Agda. First, here are some initial translations I ...
adev's user avatar
  • 13
0 votes
0 answers
71 views

Isabelle Server HOL-Library Build Failed

I'm trying to build a session through isabelle server on Isabelle 2023. The sessions itself are pretty long, but I have narrowed the problem down into HOL-Library. It outputs the following log on ...
Achmad Afriza's user avatar
0 votes
0 answers
69 views

Isabelle/HOL: Induction fails because the assumption about the inductive predicate is not the first assumption

I have the following definitions: inductive star :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" for r where refl: "star r x x" |step: "r x y ⟹ star r y z ⟹ star r x z" and ...
Trayan Gospodinov's user avatar
0 votes
1 answer
61 views

Complex set comprehension

I am running into an issue and I don't know if it's Isabelle way of managing set comprehension or I am having a really slow moment. This lemma goes on just fine lemma "{x | x. P x} ∩ {x | x y. (Q ...
Alicia M.'s user avatar
-1 votes
2 answers
67 views

Sledgehammer output with vampire

I tried to use sledgehammer in proof and got such output Sledgehammering... vampire found a proof... Derived "False" from these facts alone: SymbolicE, const_bool_simp, ptype_bool_not, ...
bearhug15's user avatar
0 votes
0 answers
78 views

Exporting code in Isabelle: code equations for instances of a type declared using typedecl

I'm trying to export code for functions with quantifiers based on a type declared using typedecl, i.e., something like this: typedecl x consts set_x1 :: "x set" consts set_x2 :: "x set&...
gfs's user avatar
  • 1
0 votes
1 answer
92 views

Can I define an "inductive" function on finite sets?

I am working with a finite set of elements and I need to define a recursive operation on them. Think something of the form "fx {} = []" | "fx (insert x X) = (if finite X then (if x ∈ ...
Alicia M.'s user avatar
0 votes
0 answers
43 views

How to have Isabelle output cartouches instead of quotes?

Over the years, Isabelle has been transitioning from using quotes "..." to cartouches ‹...› to wrap types, object logic terms, and notation. As of now (Isabelle 2023), it's still quite ...
Ben Keks's user avatar
  • 936
0 votes
0 answers
89 views

How to use Isabelle's command line commands in macOS

I have installed the Isabelle 2023 on my MacBook and I want to use command line commands to compile the proof. However, when I enter the command like isabelle jedit -d . -l the terminal just tell me ...
Huan Sun's user avatar
  • 167
0 votes
2 answers
74 views

Illegal character ":" in path element "C:\Isabelle\Isabelle2023\tmp\MLTEMPb14572"

When I entered the isabelle build -bv CParserTest command in cygwin, the following error occurred [isabelle] *** Illegal character ":" in path element "C:\Isabelle\Isabelle2023\tmp\...
leo's user avatar
  • 1
1 vote
1 answer
65 views

Transforming arithmetic expressions into lists of polynomial coefficients in Isabelle. Can't prove algorithm for expressions with multiplication

Introduction The datatype for an arithmetic expression is defined as datatype exp = Var | Const int | Add exp exp | Mult exp exp I am attempting to implement a function, coeffs :: exp ⟹ int list, ...
curiousCprogrammer1231's user avatar
0 votes
1 answer
70 views

Schematic variables as functions in isabelle?

I am working on proving a lemma in predicate logic using Isabelle, and I've encountered a schematic variable in the proof state that I'm finding somewhat confusing. I would greatly appreciate your ...
curiousCprogrammer1231's user avatar
0 votes
0 answers
137 views

Have proof A==>B how to proof not A ==> not B

I have proof for let's say A ==>B but how to do not A ==> not B with basic proof in Isabelle. I also want to know that i know A is the equivalent as B in propositional logic, and I have proof A =...
user22346194's user avatar
0 votes
1 answer
54 views

Concrete Semantics Chapter 7 Question 1 structured Isar Proof

I am trying to produce a structured Isar proof for Chapter 7 Question 1 in Concrete Semantics, but I am having trouble defining the proper assumptions and induction hypotheses for the inductive cases. ...
david-wang-0's user avatar
2 votes
1 answer
148 views

Why this trivally incorrect lemma can be proved using sos?

I'm new to Isabelle and have encountered a problem that I'm struggling with. I have the following lemma: imports Main HOL.HOL HOL.Real "HOL-Library.Sum_of_Squares" lemma fixes r :: real ...
Ze-Nan Li's user avatar
  • 123
0 votes
0 answers
79 views

Exporting code for definitions with the universal quantifier in Isabelle

I’m trying to export code from the Isabelle theorem prover using its code extraction tools. The code I’m trying to extract is based on an integrity constraint that returns a boolean value from a ...
gfs's user avatar
  • 1
0 votes
0 answers
51 views

Isabelle update: can I update one single lemma in an already built Isabelle session?

I am not quite familiar with formal proof nor Isabelle, but unfortunately I am asked by my leader to work on an Isabelle project. There is a project with multiple sessions. I can successfully build ...
H.Zhao Zhang's user avatar
0 votes
1 answer
58 views

Isabelle Nitpick cardinality limit of 65536 exceeded; what to do?

I'm getting this Limit reached: too high cardinality (65536) error from Isabelle's Nitpick tool: Nitpicking formula... [...] The type 'a passed the monotonicity test; Nitpick might be able to skip ...
Jim's user avatar
  • 239
1 vote
1 answer
46 views

Is it possible to have an AFP entry with documentation that uses BibLatex as opposed to Bibtex?

I have submitted an entry to the Archive of Formal Proofs (AFP). In the documents folder, I have a root.tex and a root.bib that work with BibLatex. The automated system seems to be trying to use ...
Ann Dorian's user avatar
3 votes
1 answer
45 views

What do I do about "I/O error: /opt/afp/tools/lib/classes/afp_tools.jar" in an AFP submission?

I am submitting to the AFP (Archive of Formal Proofs) for the first time, and I am getting a build error. The Isabelle log is: Extract archive Checking for hidden files Found no hidden files or ...
Ann Dorian's user avatar
0 votes
1 answer
48 views

Custom syntax for datatype constructor

So I'm trying to define syntax for the abbreviation provided in section 10.2 near the end of page 189 of https://isabelle.in.tum.de/doc/tutorial.pdf, but I'm not sure how. I tried looking at the list ...
Kookie's user avatar
  • 348
0 votes
0 answers
34 views

How to define the range lemma like star

Based on the repositoy in AFP, I plan to extend the library of regexp in Isabelle. Here I try to prove the range regexp in below which is similay to star. The index of star could start from zero(empty ...
Hongjian Jiang's user avatar
0 votes
1 answer
81 views

Trouble with extremely basic Isabelle/ISAR proofs

I am just starting to learn Isabelle/ISAR, and I wanted to try some basic logic proofs. My core issue is that even when I copy proofs straight out of an instruction manual, I am still getting errors. ...
saltine's user avatar
0 votes
0 answers
87 views

Option that is some, let and case of cause rewriter not to simplify

In Isabelle, I have to following proof state: proof (prove) using this: find (λc. length c = 1) f = Some [l] goal (1 subgoal): 1. fst (units_propagate f) = fst (units_propagate (update_formula f (...
bobismijnnaam's user avatar
1 vote
1 answer
35 views

exception MATCH rised in line 359

I have co-inductive exec and eval. For eval code_pred worked automaticaly, but for exec couldn't. I added [code_pred_intro] lemmas according with example with tranclp (I ommit it becouse it takes ...
bearhug15's user avatar
-2 votes
1 answer
82 views

Solving a system of linear equations on Isabelle

I am having problem in representing a system of linear equations on Isabelle/HOL. I suppose I should simply write some equations jointed by "\and" but I have problem with type declaration ...
Kowmei's user avatar
  • 1
0 votes
1 answer
58 views

Instantiate typeclass over type_synonym

In my theory developent I have one concept "bar" of function for a bunch of types (say, bar_atom, bar_clause, etc.), so I figured I'd abstract that out using a typeclass for readability (...
bobismijnnaam's user avatar
0 votes
2 answers
82 views

Recursive function leads to simplifier loop in Isabelle

I have the following two Isabelle definitions: fun remove_left :: "cmd ⇒ cmd × cmd option" where "remove_left (Comp c d) = (case remove_left c of (head, Some c') ⇒ (head, Some (Comp c'...
bobismijnnaam's user avatar

1
2 3 4 5
23