1,135
questions
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 ...
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)"
...
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"
...
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 ...
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/...
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:
...
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 ...
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"
...
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 ...
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 :: ‹...
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 ...
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 ...
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&...
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 ...
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 ...
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 =...
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"
...
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 ...
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 ...
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 ...
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 ...
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
...
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 ...
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 ...
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
...
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 ...
-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, ...
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&...
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 ∈ ...
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 ...
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 ...
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\...
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, ...
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 ...
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 =...
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.
...
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
...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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. ...
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 (...
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 ...
-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 ...
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 (...
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'...