Questions tagged [isabelle]
Isabelle is a generic proof assistant, with Isabelle/HOL as main instance.
1,112
questions
0
votes
0
answers
41
views
How to prove this simple lemma "r^3=8 \Rightarrow r=2" automatically?
I am trying to prove the following lemma.
lemma
fixes r :: real
assumes "r ≥ 0" and "r^4 = 16"
shows "r = 2"
It can be proved by
proof-
have "r = root 4 16&...
0
votes
1
answer
37
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
99
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
30
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
32
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
39
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
35
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 ...
2
votes
1
answer
37
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
35
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
29
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
57
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
17
views
How to represent range regexp in List in Isabelle
I try to implement the transformation from regexp to nfa.
Such as star regexp represents match some character zero or more times, so that it could be formulated below, the concat could match infinite ...
0
votes
0
answers
47
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
28
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
44
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
0
answers
46
views
Locale interpretation and code generation in Isabelle
I'm trying to use the export command to generate code based on a simulation of a state machine defined within a locale, where transitions between states occur based on certain events.
theory ...
0
votes
1
answer
50
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
52
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'...
1
vote
1
answer
36
views
Isabelle: [simp] leading to an infinite loop
I am trying to solve the simple lemma "add m (Suc n) = add n (Suc m)" by induction over m.
I tried solving the last remaining subgoal after applying auto by another lemma, howerver if i use ...
1
vote
0
answers
42
views
How to evaluate Rep of new type in Isabelle?
I'm trying to evaluate terms corresponding to the type t defined as follows.
typedef t = "{(0::nat)..10}" by auto
To evaluate terms of type t, I simply define Abs_t as a constructor.
lemma [...
1
vote
1
answer
38
views
How can I use a size parameter for datatype definitions
I want to use the word type from "HOL-Library.Word" in a datatype where I don't want to fix the size of the word.
datatype 's Foo = Foo1 "'s word" | Foo2 "'s word"
But ...
1
vote
1
answer
37
views
Work backwards from goal in structured (isar) proof
I have a goal invariant (smallStep fac (i, f)) a r And am proving it by case-splitting over i. I am proving the case i = 0 and I would like to simplify the goal in that case (invariant (smallStep fac (...
1
vote
0
answers
29
views
sel4 Verify the script-l4v
When I built c-parser, I didn't find the specific steps to build the environment. Do you have a friend to share
I want to implement automatic conversion of c code
2
votes
1
answer
35
views
sel4 Verify the environment setup
Now I am setting up sel4 verification environment, but I see the blogger said "link isabelle path to verification directory", I would like to ask what it means?
Do you want to download ...
0
votes
0
answers
39
views
Define an auxiliary lemma to help prove such a lemma
In my project of correctness of transition between regexp and nfa. I've defined the semantics of regexp type.
The definition of semantic :
datatype ('v)regexp = ESet | LChr 'v| Concat "'v regexp&...
1
vote
1
answer
46
views
How to prove such a lemma that one hold and other holds, the concat of two still holds
For some purpose, I want to prove such a lemma: if one automaton could be reachable and another automaton could be reachable, such that the concat of these two automata could be reachable. The qa is a ...
0
votes
1
answer
52
views
How to reuse type variables from locales
I want to fix a few functions and constants of arbitrary types in a locale for a bunch of Foo definitions.
I then want to fix some additional functions and constants in another locale for a bunch of ...
0
votes
0
answers
27
views
How to combine all list in a set into a list set which just contains one list
For some purpose, I want to define a function to get a list set just like that "f {[a],[b]} = {[a,b]}.
fun combine_list_set ::"'a list set => 'a list set"
How to define such a ...
0
votes
0
answers
39
views
How to write a lemma form like implication in Isabelle
I've a LTS system below, and try to prove from a same start node to end node, the accept list would be empty. The condition is that the two nodes are both the accept node(final node), thus the idea is ...
1
vote
0
answers
64
views
To prove a lemma of labeled transtion in Isabelle
The labeled transition of Isballe is defined below, which contains the prior node and the successor node, the set represents the condition.
type_synonym ('q,'a) LTS = "('q * 'a set * 'q) set"...
0
votes
0
answers
55
views
How to execute proof by cases which customized by ourself
I'd like to prove a lemma by cases. Assume that I have two variables r1 and r2, r2 is free variable, and r1 r2 belongs to same datatypes. Thus there is an idea that I want to prove the lemma by cases ...
0
votes
0
answers
34
views
Reification for interpretation functions which use different interpretation functions below quantifiers/lambdas
I'm currently trying use Isabelle/HOL's reification tactic. I'm unable to use different interpretation functions below quantifiers/lambdas. The below MWE illustrates this. The important part is the ...
0
votes
0
answers
29
views
Cannot import HOL in Isabelle batch mode from Docker
I'm trying to use HOL in Isabelle in batch mode from Docker, but it can't seem to find HOL.
If I have this My.thy file
theory My
imports HOL
begin
end
and then run this to process the file in batch ...
0
votes
0
answers
27
views
Isabelle locale copy without any new assumptions
In https://www.isa-afp.org/theories/jacobson_basic_algebra/#Group_Theory
there is this interesting locale definition
text ‹p 38, l 4›
locale left_translations_of_monoid = monoid begin
... some stuff .....
1
vote
0
answers
34
views
Isabelle Archive of formal proof dependency graph
I was wondering whether these is some tool that could help me find packages in AFP that depend on some specific package.
For example I see that Jacobson_Basic_Algebra
https://www.isa-afp.org/entries/...
1
vote
1
answer
61
views
How to have full control over substitution in Isabelle
In Isabelle I find myself often using
apply(subst xx)
apply(rule subst)
apply(subst_tac xx)
and similar command but often it is a hit or miss. Is there any resources on how to guide the
term ...
0
votes
1
answer
42
views
Isabelle equivalent definitions treated differently by auto
I'm trying to add some small improvements to Jacobson_Basic_Algebra.
ORIGINAL DEFINITION:
Their definition of monoid isomorphism is as follows.
locale monoid_isomorphism =
bijective_map η M M' + ...
0
votes
1
answer
84
views
Isar: Failed to retrieve literal fact
I have the following code:
assume H: "x ≠ xa ∧ x ∈ elems xs" (is "?H1 ∧ ?H2")
hence "?H1" and "?H2" by auto
from Cons.IH[OF `?H2` ] have 1: "∃...
0
votes
2
answers
74
views
Isabelle multiply both sides of an equation (equational reasoning in Isar)
I want to prove that inverse element is unique in a monoid M
theorem inverse_unique:
assumes "u ⋅ v' = 𝟭"
assumes "v ⋅ u = 𝟭"
assumes "u ∈ M"
assumes "v ∈ ...
0
votes
1
answer
42
views
What is `ind` type in Isabelle
In Isabelle natural numbers are defined as follows
typedecl ind
axiomatization Zero_Rep :: ind and Suc_Rep :: "ind ⇒ ind"
― ‹The axiom of infinity in 2 parts:›
where Suc_Rep_inject: &...
0
votes
1
answer
39
views
Bad number of arguments for type constructor in Isabelle/hol
I am a newbie in Isabelle/hol and I have this record declaration:
record ('v,'w) fca = object_set :: "'v set" attribute_set :: "'w set" inc_set :: "('v×'w) set"
and I ...
0
votes
1
answer
45
views
Case analysis on a premise Isabelle
I have the following proof state:
1. ⋀i is s stk stack.
(⋀stack.
length (exec is s stack) = n' ⟹
length stack = n ⟹ ok n is n') ⟹
length (exec (i # is) s stack) = ...
0
votes
1
answer
44
views
Function definition with one argument as index
This question is somewhat related to function with index
Imagine the definition of the function is
definition myf :: "nat => nat => nat" where
"myf n a = n * a"
and I want ...
1
vote
0
answers
74
views
Problem with multi-sort atoms in Nominal Isabelle
I'm experimenting with Nominal2's support for multi-sort atoms (see this example in the Nominal package and the discussion in Section 5 of this paper). The idea is to define a toy typed λ-calculus in ...
0
votes
0
answers
67
views
Installing from Archive of Formal Proofs
I'm trying to install Grothendieck_Schemes from
https://www.isa-afp.org/entries/Grothendieck_Schemes.html#
I downloaded the tar and uncompressed it. The contents are
$ ls -l
Comm_Ring.thy
Group_Extras....
0
votes
1
answer
21
views
How to type boldface symbols in Isabelle
The definition of semigroup and monoid uses bold * and bold 1
locale semigroup =
fixes f :: "'a ⇒ 'a ⇒ 'a" (infixl "❙*" 70)
assumes assoc [ac_simps]: "a ❙* b ❙* c = a ❙* ...
1
vote
1
answer
43
views
Isabelle Failed to refine any pending goal during instantiation
datatype 'a list = Cons 'a "'a list" | Nil
instantiation list :: (order) order
begin
fun less_eq_list :: "'a list ⇒ 'a list ⇒ bool" where
"less_eq_list Nil Nil = True"...
1
vote
1
answer
51
views
Topological filters in Isabelle
I'm studying topological filters in Filter.thy
theory Filter
imports Set_Interval Lifting_Set
begin
subsection ‹Filters›
text ‹
This definition also allows non-proper filters.
›
locale is_filter ...
1
vote
2
answers
53
views
What is INF in Isabelle
I found this definition in Isabelle
definition (in topological_space) nhds :: "'a ⇒ 'a filter"
where "nhds a = (INF S∈{S. open S ∧ a ∈ S}. principal S)"
What is INF? I can't ...
1
vote
1
answer
31
views
Isabelle `subst` but replace right side with left side
Suppose the goal is P l, then I can use apply(subst X) where X is of the form l=r
and as a result I obtain P r. Now my question is whether there exists some other tactic like subst but which could use ...