1,144 questions
-4
votes
0
answers
34
views
What are the necessary imports to use Isabelle LLVM code generator? [closed]
I want to make some tests on Isabelle to compare the efficiency of Sepref and LLVM. To do so I am using the Sepref examples given in the Archive of Formal Proof in the Refine_Imperative_HOL section.
...
- 1
0
votes
1
answer
51
views
How to convert proof_body to string?
Consider the following theory:
theory Scratch2
imports Main
begin
lemma ex: "A ∧ B ⟶ B ∧ A"
proof
assume "A ∧ B"
then obtain B and A ..
then show "B ∧ A" ..
qed
...
- 133
1
vote
1
answer
169
views
How to prove time complexity of an algorithm?
I'm trying to prove time complexity of merge sort algorithm in Isabelle HOL:
theory Merge_Sort_Time
imports Complex_Main "HOL-ex.BigO"
begin
fun merge :: "'a::linorder list ⇒ 'a list ...
- 1,325
1
vote
1
answer
35
views
Representing the Gradient in Isabelle
I would like to state a simple equation in Isabelle:
\nabla f (x) = 0
where 0 is n dimensional and f : R^n --> R. What I have so far is:
`fixes f :: "ℝ vec['n] ⇒ real"
and x :: "ℝ ...
- 155
1
vote
0
answers
33
views
How can I make an inductive argument that quantifies over a type parameter?
If I'm proving some property "P (n :: nat)", and apply some intermediate rule that changes it into "P (LENGTH(?'a))" with an additional proof obligation to show that "n = ...
1
vote
1
answer
31
views
Using continuous_on_diff with subst (Isabelle)
ORIGINAL POST:
I'm trying to show the following:
have "continuous_on {x. 0 < x} (λx. 12 * x⇧2 - 1)"
And I would like to use the following lemma:
thm continuous_on_diff
-------------------...
- 155
0
votes
0
answers
21
views
Retrieving Symbol Definition in Isabelle
I'm interested in simulating the effect of going to the definition of a constant (ctrl + click) in Isabelle. So given a symbol, for example AExp.plus in ~~/src/HOL/IMP/AExp, I want to recover the ...
2
votes
1
answer
61
views
The distinction of "proof" and "proof-" in isabelle
I have been using isabelle for some time, and although I can use isabelle to prove something, I am still not clear about the distinction between proof and proof-. The differences between the two I ...
- 21
2
votes
0
answers
57
views
How to use Isabelle scalac wrapper in build.sbt
I have a Scala development environment with Metals and a build.sbt. The theorem-prover Isabelle provides its own wrappers for Scala tools such as scalac, scala, etc. I have Isabelle added to my path ...
- 542
0
votes
1
answer
106
views
A few questions about derivatives of functions in Isabelle
Just curious if there is a way to express the nth derivative of f or f^{(n)}(x) in Isabelle. Would this involve using something like "(f has_derivative f') (at x)" or would it involve DERIV ...
- 155
0
votes
1
answer
56
views
How to prove sequential commands C1; C2 can always execute to C2 if we know C1 always terminates?
I am using a theorem prover to demonstrate the progress of programs.
The semantics of a program are defined using a small-step relation, denoted as
ctran, between program configurations. A program ...
- 167
1
vote
1
answer
53
views
Why does isabelle's preorder requires to provide less _and_ less_eq
Isabelle's preorder class requires providing both less_eq and less:
class ord =
fixes less_eq :: "'a ⇒ 'a ⇒ bool"
and less :: "'a ⇒ 'a ⇒ bool"
class preorder = ord +
...
- 4,540
0
votes
1
answer
42
views
Applying auto _only_ to the created proof goals in tactic mode
I want to apply auto to all the proof goals the previous apply created, but not the other ones. I only know how to do it by putting everything in a subgoal. Is there a nicer way?
lemma bar:
assumes ...
- 4,540
1
vote
1
answer
78
views
Isabelle record update reordering
record r =
a :: nat
b :: nat
c :: nat
lemma "P (r ⦇ a := 2, b := 3 ⦈) ⟹ P (r ⦇b := 3, a := 2⦈)"
apply auto ― ‹doesn't work›
by (metis r.simps(5) r.simps(6) r.surjective)
Why ...
- 4,540
0
votes
1
answer
47
views
What does the `using` keyword do with `blast`?
Sometimes, using XXX apply blast discharges a proof goal, but apply (blast mod: XXX) doesn't work for mod any of intro, elim or del, with or without !.
What does using actually do to blast?
- 4,540