Stack Overflow
Stack Overflow

Questions tagged [hol]

The HOL interactive theorem prover is a proof assistant for higher-order logic: a programming environment in which theorems can be proved and proof tools implemented.

The HOL interactive theorem prover is a proof assistant for higher-order logic: a programming environment in which theorems can be proved and proof tools implemented.

36 questions
6
votes
1 answer

Automatic translation from Isabelle/HOL to HOL

I have some definitions and theorems in Isabelle/HOL and need to use those same definitions and theorems with HOL. Translating the code manually is certainly possible, but cumbersome. Are there any programs that (semi-)automatically perform such a…
Lorenz Leutgeb
  • 474
  • 6
  • 12
4
votes
1 answer

Isabelle/Pure Isabelle/HOL Isabell/Isar conceptual questions

I need to do a presentation on a paper which at some point makes use of Isabelle/Isar and Isabelle/HOL. I tried researching online about Isabelle/HOL and Isabelle/Isar to be able to eplain the relations in one or two slides. Here are the relations…
Jonathan
  • 552
  • 1
  • 4
  • 10
3
votes
1 answer

Isabelle structure proof

There is a set of some structures. I'm trying to prove that the cardinality of the set equals some number. Full theory is too long to post here. So here is a simplified one just to show the idea. Let the objects (which I need to count) are sets…
Eva
  • 35
  • 2
2
votes
1 answer

What does it mean for a fact used in Isabelle to have a number after the name?

Most of the proofs suggested by Sledgehammer use this notation of number inside of parentheses: by (smt (z3) ApplyAllResult.distinct(1) ApplyResult.case(1) ApplyResult.case(2) ApplyResult.exhaust …
julianferres
  • 23
  • 4
2
votes
3 answers

Certified calculations in a proof assistant

Symbolic calculations performed manually or by a computer algebra system may be faulty or hold only subject to certain assumptions. A classical example is sqrt(x^2) == x which is not true in general but it does hold if x is real and…
calcert
  • 33
  • 4
2
votes
1 answer

How to get ML values from HOL?

I have an embedded ML code like this: ML ‹ val boo = true; val num = 1234; val rea = 3.14; val str = "hi"; › Can anyone give me an example of code that gets those values from HOL?
notooth
  • 31
  • 1
2
votes
1 answer

Why can't I make my cases explicit in Isabelle when the proof is already complete but gives a "fails to refine any pending goal" error?

I'm going through chapter 5 of concrete semantics. I got some error while working through this toy example proof: lemma shows "¬ ev (Suc 0)" I know this is more than needed (since by cases) magically solves everything & gives a finished proof,…
Charlie Parker
  • 5,884
  • 57
  • 198
  • 323
2
votes
1 answer

How can we force Isabelle to reveal to us what rule it's applying in the background in Isar when a proof starts?

I was trying to prove: lemma shows "¬ ev (Suc 0)" I did: lemma shows "¬ ev (Suc 0)" proof (rule notI) assume "ev (Suc 0)" then show False proof and it gave me really pretty goals: proof (state) goal (2 subgoals): 1. Suc 0 = 0 ⟹ False …
Charlie Parker
  • 5,884
  • 57
  • 198
  • 323
2
votes
0 answers

View Proof Steps From Tactic Application

I have spent some time constructing "forward proofs" using the theorem library in HOL. I am now hoping to move to applying tactics to make "backward proofs". I am wondering if there is a way to, after a tactic has been applied, to view the list of…
Simon Diemert
  • 330
  • 3
  • 9
2
votes
1 answer

Prove a goal with an assumption in HOL

I state the following goal in HOL4: set_goal([``A:bool``,``B:bool``], ``B:bool``); resulting in the proof state val it = Proof manager status: 1 proof. 1. Incomplete goalstack: Initial goal: B …
Gergely
  • 6,879
  • 6
  • 25
  • 35
2
votes
1 answer

Exception on ACCEPT_TAC after THEN in HOL

I am trying to create a theorem named "absorptionRule" by packaging the tactics that are used to prove the goal !(p:bool) (q:bool). (p==>q) ==> p ==> p /\ q. However, I am getting an exception on ACCEPT_TAC. When I execute each tactic one-by-one,…
Tuffie
  • 71
  • 2
2
votes
1 answer

Theorem proving from first principles using SML with HOL inference rules

I am trying to prove the theorem [] |- p /\ q <=> q /\ p :thm using SML with HOL Inference Rules. Here's the SML code: val thm1 = ASSUME ``p:bool /\ q:bool``; val thm2 = ASSUME ``p:bool``; val thm3 = ASSUME ``q:bool``; val thm4 = CONJ thm2 thm3; val…
Tuffie
  • 71
  • 2
1
vote
1 answer

What is the difference between universal quantifiers and meta-universal quantifiers?

The universal quantifier in first-order logic (the symbol is ∀) and meta-universal quantifier in meta-logic (the symbol is ⋀) what is the main difference? For the following two lemmas, the first example proves successful using universal…
hahahahaha-sh
  • 11
  • 1
1
vote
1 answer

setting up Emacs for HOL4

I am a newbie of both HOL4 and Emacs. Apologize for the probably silly question. I wish to set up Emacs for HOL4 following the instruction from https://hol-theorem-prover.org/HOL-interaction.pdf. I tried to start HOL process on Emacs with Alt-h h…
Pingchuan Ma
  • 17
  • 2
1
vote
1 answer

Termination proof in Isabelle

I'm trying to provide an automatic termination proof for this function: function aux :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list" where "aux p xs = (if ¬isEmpty xs ∧ p (hd xs) then hd xs#aux p (drop 1 xs) else [])" by pat_completeness auto with…
Darsen
  • 119
  • 6
1
2 3