This page is meant to collect the questions that arise when first using Isabelle/HOL and the Proof General. Just post any questions you have here, even if - and especially if - you don't know the answer yet

Please try to sort the questions into categories, so each category has its own edit button.

It would also help us and the other students a lot, if you could post any questions you had here, even just syntactical problems! Everything which held you up for more than 10 minutes is already worth mentioning here.

Also, check out the official FAQ of Isabelle/HOL.

Dear all proof lovers: I am really new to Isabelle. Recently I hope to learn HOL and try to use automatic therom prover. So I download the Isabelle2013. Now I hope to use Isabelle/jEdit in Windows OS(so I cannot use proof general) for therom proving. However, what make me confused is, what is the difference between Isabelle/HOL and Isabelle/Isar? And what syntax should I learn, Isabelle/Isar syntax or Isabelle/HOL syntax? Please tell me the specific tutorial I should learn. Here, I am learning the simple example, which is in appendix. Am I right? Thanks very much.

Appendix:

header {* Finite sequences *}

theory Seq imports Main begin

datatype 'a seq = Empty | Seq 'a “'a seq”

fun conc :: “'a seq \<Rightarrow> 'a seq \<Rightarrow> 'a seq” where

"conc Empty ys = ys"

| “conc (Seq x xs) ys = Seq x (conc xs ys)”

fun reverse :: “'a seq \<Rightarrow> 'a seq” where

"reverse Empty = Empty"

| “reverse (Seq x xs) = conc (reverse xs) (Seq x Empty)”

lemma conc_empty: “conc xs Empty = xs”

by (induct xs) simp_all

lemma conc_assoc: “conc (conc xs ys) zs = conc xs (conc ys zs)”

by (induct xs) simp_all

lemma reverse_conc: “reverse (conc xs ys) = conc (reverse ys) (reverse xs)”

by (induct xs) (simp_all add: conc_empty conc_assoc)

lemma reverse_reverse: “reverse (reverse xs) = xs”

by (induct xs) (simp_all add: reverse_conc)

end

This section covers questions about why Isabelle/HOL does not accept what you write.

Isabelle does not accept my function definition and gives only strange syntax errors:

3
4 fun test :: "int => int" where
5   "test x = if x = 0 then 42 else x"
6
  
*** Inner syntax error (line 5 of "Scratch.thy") at "if x = 0 then 42 else
***   x"
*** Failed to parse proposition
*** At command "fun" (line 4 of "Scratch.thy")

A good heuristic to avoid such errors is to put parenthesis around the expression on the right side of the defining equality. So the simple solution is:

fun test :: "int => int" where
  "test x = (if x = 0 then 42 else x)"

You almost always have to put them for if-then-else and case-of expressions.

Strange things are happening, there is absolutely nothing wrong with what I typed in, but Isabelle is still not accepting it!

There might of course be various reasons for this, so lets just answer with a growing list of possible reasons

• The most simple explanation is that you did type in something wrong after all, e.g.
  • Implication is a double arrow $\longrightarrow$ in contrast to $\rightarrow$.
  • You have to enclose expressions in quotes, if they do not just consist of a single identifier.

• Check that you at least imported the Main theory and not just Datatype, which is done this way in some examples to redefine lists for educational purposes. Isabelle might not know what you are talking about

• Check that you did not shadow existing symbols. If you name your functions, types or constructors like ones from the Main theory, you might encounter errors which are really hard to track down.

• Isabelle has at least two modes, the theory mode and the proof mode. Make sure you are in the right mode for what you are trying to do! Most of the time you will end proof mode with done, by or oops. You get into proof mode by stating a theorem or making another definition which requires proving, like function.

I am having trouble to evaluate the forall and exists functions. The prompt only shows the sequence of operations in the folding, but does not actually reduce it to the final boolean value. Is there something wrong with the definitions?

value "forall ((op <) 0) (1 # 2 # 3 # 4 # 5 # [])"

The expression you gave is polymorphic, which means the semantics depends on the instance for operators like (op <) for different types. You can annotate a type at one value to enable the type inference to infer a fixed type for the whole expression. Then it will collapse by simplification.

value "forall ((op <) 0) ((1 :: int) # 2 # 3 # 4 # 5 # [])"

How does Isabelle actually “compute” the value of a function application? For example in

value "1::nat + 1"

Is it simply applying simplification (i.e. term rewriting) until the normalized term “2” is reached?

Yes, Isabelle does not have any notion of operational semantics or the like, but just uses simplification, i.e. equalities. The defining equalities of functions can be used for simplification, as soon as termination is shown. In this case the definition of the relevant function is:

primrec plus_nat
where
  add_0:      "0 + n = (n::nat)"
  | add_Suc:  "Suc m + n = Suc (m + n)"

So the term Suc 0 + Suc 0 gets reduced to Suc (0 + Suc 0) by add_Suc, which gets reduced to Suc (Suc 0) by add_0.

I am just claiming this, however, if you want to know that is really going on you can try trace simplification from the Isabelle menu

This section covers questions about finding and doing proofs. This includes technicalities of the proof system.

Hi all. I have more like a general question: I am stuck at Exercise 2a on Sheet 2, so proving/disproving. I got until the last theorem. Problem is that I basically try out stuff and am happy that it works. So can someone give me some help about how we choose the right rule to apply and especially how do we know what kind of lemma to write to include in the simplification for later proving of the theorem ?

I found this on the web:

lemma  replace_append:  "replace  x  y  (xs  @  ys)  =  replace  x  y  xs  @  replace  x  y ys"
apply  (induct  "xs")
apply  auto
done

theorem  "rev(replace  x  y  zs)  =  replace  x  y  (rev  zs)"
apply  (induct  "zs")
apply  (auto  simp  add:  replace_append)
done

So here they make use of the lemma replace_append to prove the theorem. But I wonder how to come up with all these nice little helper lemmas. I took a look at the subgoals but I cannot really get something out of it. Hope some of you can help. Thanks a lot !

Well, you are trying to proof that you can either first replace elements in a list, then reverse it or first reverse it, then replace the elements. You should be able to proof that, as it makes sense

So for now there really aren't many options on going on with the proof and as lists can be arbitrary long, you really need an inductive argument here. In this case an induction over the list should do. What you get now is one case for the empty list, which is really trivial and can be solved just by simplification. As both functions just return an empty list, it all collapses and you get an axiom.

But what about the inductive case. You have to proof the theorem for a constructed list, lets say by putting z into zs, knowing that the theorem holds for zs already! This means you get something in the lines of:

rev (replace x y      zs )  =  replace x y (rev      zs ) ==>
rev (replace x y (z # zs))  =  replace x y (rev (z # zs))

So what you really need to do here is get rid of the z on either side of the equation, so you can use the equality you have as assumption! Lets say you want to get rid of it on the right side. You can pull it out of the rev application just by using the definition, which will probably use the @ operator:

replace x y (rev (z # zs))  simplifies to  replace x y (rev zs @ [z]))

Now you are screwed, because the simplification rules for replace following from its definition can only handle normal list construction using #. This is why you can't solve the rest just by simp, auto or any of the like. What you need now is a theorem stating how list concatenation within the argument of replace can be handled, which is exactly what they do in the helper lemma:

replace x y (xs @ ys)  =  replace x y xs  @  replace x y ys

This is actually more general than what you need, it would be sufficient for our proof to know that:

replace x y (xs @ [z])  =  replace x y xs  @  replace x y [z]

If you try to proof such specialized lemmas of more general notions, however, you might get stuck, because your induction hypothesis, which is the lemma itself, is not strong enough! So its a good idea to keep all lemmas that you want to proof by induction as general as possible.

I didn't actually type any of this in and sometimes there are more technicalities involved than discussed here, but the idea stays the same!

Assume we have two subgoals:

1. $[| a \land b ; a ; b |] \Longrightarrow ?R$
2. $[| a \land b ; ?R |] \Longrightarrow a$

How do we tell assumption to take $?R = a$ in subgoal one?

There are several possible solutions:

• First is to avoid this situation to come up in the first place, by choosing the right method
• Second is to apply (rotate_tac 1), to rotate the assumption $a$ to the front. As anything matches $?R$, we want $a$ to be the first guess.
• Finally, you can use backtracking to make Isabelle find the right substitution. What you want to do is solve subgoal one with assumption and then solve subgoal two with assumption, where the second assumption will only work if $?R$ gets matched correctly. So combining them into one method will do the trick: apply (assumption, assumption).

Which proof methods are safe and which aren't?

Good question This is a paragraph from the lecture notes:

Remark: 
- Safe rules preserve provability
    conjI, impI, notI, iffI, refl, ccontr, classical, conjE, disjE
- Unsafe rules can turn a provable goal into an unprovable one
    disjI1, disjI2, impE, iffD1, iffD2, notE
Apply safe rules before unsafe ones.

But then again it has been pointed out to me that the question was asked for methods, not rules, so here are my thoughts to methods:

• rule is obviously unsafe in general, as you can always apply (rule FalseE), which replaces your current goal with False. Consider the goal $A \Longrightarrow A$, which can be solved by assumption, yet after the rule application it becomes $A \Longrightarrow False$, which cannot be proven (unless $A$ is $False$…).
• frule is always safe, as it only derives new additional assumptions.
• drule on the other hand is in general unsafe, as it eliminates an assumption, which might yet be needed.
• erule is by the same reasoning in general unsafe, as it also drops an assumption.
• All methods which either solve the goal or do nothing are obviously safe. This includes at least assumption, blast, force, arith and metis.
• Meta methods like auto are not safe if they include unsafe rules.
• simp is always safe, as it works only with equalities, which are theorems or whose premises can be proven, so the effect can always be undone (e.g. using [symmetric]).
• safe is always safe, no surprise here
• clarify and clarsimp are safe, I think…
• induct rules are often erules, so can be unsafe, too.
• cases is always safe.
• fold, unfold and subst are always safe like simp, as they also work only with proven equations.
• subgoal_tac is unsafe, if the new assumption is unprovable from the old ones.

In which way are

• cases and case_tac,
• induct and induct_tac

different, respectively?

Good question, please tell us if you find out

On a more serious note, case_tac works in more cases (no pun intended) then cases, I haven't seen a case where you would need cases. As far as induction is concerned, it gets really messy in the more involved examples and I really have no idea why he can sometimes figure it out and sometimes not. This shouldn't be too much of a problem for the lecture though. These special methods just try to make life a bit easier in certain situations, but you can always just apply induction rules by hand, using rule or erule.

Whats the difference between

• $[| A_1, A_2, A_3 |] \Longrightarrow G$ and
• $A_1 \land A_2 \land A_3 \longrightarrow G$ (or to point out the difference: $\Longrightarrow A_1 \land A_2 \land A_3 \longrightarrow G$)?

There are several levels to this question:

1. First, the latter is by itself a HOL formula, while the former contains HOL formulas, but is more considered a rule.
2. The former says that $G$ can be proven syntactically from the given assumptions $A_1, A_2, A_3$. The latter says that you can prove using no assumptions that whenever all $A_1, A_2, A_3$ hold, $G$ holds, too.
3. Maybe the main practical difference: the former is nicely applicable as a rule, where the latter is nearly useless.

What is the difference between $=$ and $\equiv$ if used to formulate identities?

The normal equality $=$ is from HOL, whereas the equivalence $\equiv$ is from PURE logic, i.e. an equality on a higher level. I am not completely sure why you sometimes have to use one over the other. My guess would be, that definition for example is already a concept of PURE, whereas function definitions were introduced in HOL.

Suddenly simp (or auto) is running indecently long (and might or might not be successful). What is wrong?

You most likely have put a theorem into the simp set, that causes the simplifier to try a huge amount of cases (up to a an internal boundary). For example, you might have proven a theorem which states that if a property hold for a constructed list, it also holds for the list without the first element:

theorem sorted_shorter [simp]:
  "sorted (h # t) ==> sorted t"

By introducing this theorem to the simp set, Isabelle/HOL tries to simplify sorted t to True, by trying to simplify the guard sorted (h # t) to True (for any h). To achieve the latter, Isabelle can apply the theorem again, adding another element to the list at the front.

A theorem like this simply doesn't belong in the simp set. Although the “right side” of the (implicit) equality is smaller than the left, the guard of the theorem is not. Such a theorem might, for instance, be put into the dest set.

What is the difference between the operators like ($\equiv$, $\Longrightarrow$ and $!!$) and their logical equivalents like ($=$, $\longrightarrow$ and $\forall$)? And why necessarily Isabelle system requires these separate operators?

The Isabelle system has a common core for the different logics it supports like HOL and ZF. This core logic is called pure and contains the former operators. They are used to formulate theorems on the meta level, e.g. if the formula $P$ is a theorem in HOL, then $Q$ is a theorem, too. The HOL logic, of course, also supports these simple logic connectives and it cannot reuse those of pure for this purpose. It shouldn't be possible, for instance, to freely mix meta (pure) connectives with the ones of HOL. By separating them, this is now guaranteed.

What is the difference between simp_all and simp+?

While simp_all applies the simp method to all subgoals, simp+ only applies simp to the first one, as often as possible. In essence, this means that simp+ will only apply simp more than once, if it completely solves a goal. Therefore, simp+ will start to solve goals from the list and stop as soon as a goal cannot be solved.

If the reason to use it is to get rid of the first n “easy” goals, but the last simplification of the first unsolvable is unwanted, the force+ method might be better. Then again, this method might not terminate on the first unsolvable goal. Unfortunately, there is no way I know of to apply force to all subgoals, comparable to simp_all.

simp_all is a milder version of auto, which is more likely to terminate and often has the desired effect already.

Blast applies the tableaux method, which is purely semantic, right? How do I know when it can be applied?

Are there any other semantic methods for HOL?

This section covers questions about the foundations of HOL.

When defining the Universal set, what does it mean to have a “distinguished” infinite set? What's wrong with the undistinguished?

We want to use this infinite set as domain for functions. Therefore, we need the set “in our hands”; existence is not sufficient. “Distinguished” just means we have a name, i.e. a definition, for such a set so we can talk about it in a constructive way.

What do we essentially forbid when defining conservative extensions?

In the new, extended theory T', we are not allowed to have a proof for a formula from the old theory T that can not be proven in T. Note that this does not mean we necessarly can derive False now (this is an easy to check breach of this contract if T is consistent, though!) i.e. T' is not necessarily inconsistent; if T is not complete, you might find proofs for actual theorems in T' that could not be proven in T. Conservative extensions assert that this can not happen.

Is it possible to perform a non-conservative extension by only defining new types or constants (i.e. without touching the set A of axioms)?

Considering that all proofs are constructed out of axioms, nothing new can be proven, so no it shouldn't be possible. If you don't add axioms though, you are not actually “defining” anything, as you can just extend the signatures without any meaning or knowledge about the new symbols.

Why mustn't types be empty?

If types are allowed to be empty, the theory can become really messy and involves a lot of corner cases you might want to avoid. For example, look at these reasonable looking formulas:

• $\forall x.\; P(x) \longrightarrow \exists x.\; P(x)$
• $\exists x\; y.\; x = y$
• $A \lor \exists x.\; B \;\Longleftrightarrow\; \exists x.\; A \lor B\quad$ if $x$ does not appear freely in $A$.

All these are theorems in first-order logic and really should hold. The last one, for example, allows you to transform formulas into prenex normal form, by dragging quantifiers to the outside, after renaming variables to avoid collisions. None of these formulas is a theorem if types can be empty!

This doesn't say you couldn't define theories with empty types, but you have to be a lot more careful. Just to give you an idea what could go wrong even in first-order logic, if you don't take care with your definitions:

• You define an interpretation to be a mapping of the free variables of a formula to values.
• You define validity to mean that a formula is valid iff it evaluates to true in all possible interpretations.
• Now you can prove that $P(x)\; \lor \neg P(x)$ is valid, as expected.
• But you can also prove that $P(x)\; \land \neg P(x)$ is valid, if your model has an empty domain. In that case there are no interpretations, i.e. it holds that the formula evaluates to true in all of them.

About the axiom of infinity:

1. Does Isabelle/HOL have the axiom of infinity or not?
2. If it does, this means the deduction system is incomplete (because of standard models), right?
3. If it does not include the axiom, what are the implications of that? Do we still have a true HOL system?

Answer:

1. Yes, the Main theory of Isabelle/HOL contains axioms (or axiomatizations), which represent the axioms of HOL. The axiom of infinity is found at the definition of the type ind:

   typedecl ind
   
   axiomatization
     Zero_Rep :: ind and
     Suc_Rep :: "ind => ind"
   where
     -- {* the axiom of infinity in 2 parts *}
     Suc_Rep_inject:       "Suc_Rep x = Suc_Rep y ==> x = y" and
     Suc_Rep_not_Zero_Rep: "Suc_Rep x ≠ Zero_Rep"

   It is just stated there, that there exists an injective but not surjective function on this type, which makes the type infinite.

2. Yes, it is probably incomplete, yet I dare you to find some theorem which holds but you can't prove it in Isabelle/HOL .
3. This case does not apply, but still: if we did not have the axiom of infinity, we would have a weaker HOL system, maybe, but still HOL (cf lecture).