Skip to main content

New answers tagged

1 vote

How to choose an axiom system in Isabelle/HOL?

If one wants to be really sure that one is not using any of Isabelle/HOL's facts, an alternative to my main answer would be to really start with a blank slate, only building on Isabelle/Pure (i.e. the ...
Benjamin Bisping's user avatar
1 vote

How to choose an axiom system in Isabelle/HOL?

Usually, Isabelle/HOL's proof methods will get most of propositional and predicate logic out of the way immediately. (Otherwise, by blast will solve them reliably.) ...
Benjamin Bisping's user avatar
2 votes

Properties of determinants in Isabelle

You don't have to do this from scratch. The facts in HOL-Analysis.Determinants and related theories suffice. Your first fact, $\det AB=\det A \det B$, is ...
Benjamin Bisping's user avatar
1 vote
Accepted

Automatic proofs after simp

The ¬ indeed seems to be wrong. So it's no wonder that Isabelle struggles to find a proof. (Actually, in my case, it even reports on its own that ...
Benjamin Bisping's user avatar
0 votes

Using Isabelle's Archive of Formal Proofs

I followed the advice “If the AFP is in C:\afp, run the following command in a Cygwin terminal: isabelle components -u /cygdrive/c/afp/thys“ It worked. I was told by one of the experts on Isabelle not ...
Craig Feinstein's user avatar
2 votes

What is an assumption in Isar?

Slawomir already answers the main question of how to refer to assumptions in Isar proofs. (Usually, one does not use the proof method assumption for this.) I'll try ...
Benjamin Bisping's user avatar
2 votes
Accepted

Automatic proofs concerning inequalities

What's going on? Oftentimes, sledgehammer comes up with proof ideas that cannot be replayed in Isabelle/HOL. This is the case here, as indicated by One-line proof reconstruction failed It's ...
Benjamin Bisping's user avatar
0 votes

Extract explicit value from Isabelle proof

The value of ?solution in a schematic_goal-theorem depends on the proof. ...
Benjamin Bisping's user avatar

Top 50 recent answers are included