Questions tagged [isabelle]

Isabelle is a generic proof assistant, with Isabelle/HOL as main instance.

Filter by
Sorted by
Tagged with
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&...
Ze-Nan Li's user avatar
  • 123
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. ...
david-wang-0's user avatar
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 ...
Ze-Nan Li's user avatar
  • 123
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 ...
gfs's user avatar
  • 1
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 ...
H.Zhao Zhang's user avatar
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 ...
Jim's user avatar
  • 229
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 ...
Ann Dorian's user avatar
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 ...
Ann Dorian's user avatar
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 ...
Kookie's user avatar
  • 328
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 ...
Hongjian Jiang's user avatar
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. ...
saltine's user avatar
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 ...
Hongjian Jiang's user avatar
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 (...
bobismijnnaam's user avatar
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 ...
bearhug15's user avatar
-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 ...
Kowmei's user avatar
  • 1
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 ...
gfs's user avatar
  • 1
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 (...
bobismijnnaam's user avatar
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'...
bobismijnnaam's user avatar
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 ...
helppls's user avatar
  • 13
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 [...
Username's user avatar
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 ...
Proof-By-Sledgehammer's user avatar
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 (...
cxandru's user avatar
  • 158
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
Xinyue Wang's user avatar
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 ...
Xinyue Wang's user avatar
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&...
Hongjian Jiang's user avatar
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 ...
Hongjian Jiang's user avatar
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 ...
Proof-By-Sledgehammer's user avatar
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 ...
Hongjian Jiang's user avatar
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 ...
Hongjian Jiang's user avatar
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"...
Hongjian Jiang's user avatar
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 ...
Hongjian Jiang's user avatar
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 ...
MercedesJones's user avatar
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 ...
Michal Charemza's user avatar
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 .....
alagris's user avatar
  • 1,828
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/...
alagris's user avatar
  • 1,828
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 ...
alagris's user avatar
  • 1,828
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' + ...
alagris's user avatar
  • 1,828
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: "∃...
cxandru's user avatar
  • 158
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 ∈ ...
alagris's user avatar
  • 1,828
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: &...
alagris's user avatar
  • 1,828
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 ...
Jceric's user avatar
  • 3
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) = ...
cxandru's user avatar
  • 158
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 ...
Alicia M.'s user avatar
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 ...
Javier Díaz's user avatar
  • 1,071
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....
alagris's user avatar
  • 1,828
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 ❙* ...
alagris's user avatar
  • 1,828
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"...
alagris's user avatar
  • 1,828
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 ...
alagris's user avatar
  • 1,828
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 ...
alagris's user avatar
  • 1,828
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 ...
alagris's user avatar
  • 1,828

1
2 3 4 5
23