Isabelle/HOL Support Wiki

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== FAQ - Ask Questions ======

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 [[http://www.cl.cam.ac.uk/research/hvg/isabelle/faq.html|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

===== Syntax =====

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

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

<code>
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")
</code>

:!: 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:

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

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


==== Strange Things are Happening ====

:?: 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''.
==== Evaluation ====

:?: 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?

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

:!: 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.

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

==== Computing functions ====
:?: How does Isabelle actually "compute" the value of a function application? For example in
<code>
value "1::nat + 1"
</code>
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: <code>
primrec plus_nat
where
  add_0:      "0 + n = (n::nat)"
  | add_Suc:  "Suc m + n = Suc (m + n)"
</code>
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 ;-)
===== Theorem Proving =====

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

:?:  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:
<code>
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
</code>

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:

<code>
rev (replace x y      zs )  =  replace x y (rev      zs ) ==>
rev (replace x y (z # zs))  =  replace x y (rev (z # zs))
</code>

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:

<code>
replace x y (rev (z # zs))  simplifies to  replace x y (rev zs @ [z]))
</code>

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:

<code>
replace x y (xs @ ys)  =  replace x y xs  @  replace x y ys
</code>

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

<code>
replace x y (xs @ [z])  =  replace x y xs  @  replace x y [z]
</code>

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!

==== Schema Variable Matching ====

:?: Assume we have two subgoals:

  - $[| a \land b ; a ; b |] \Longrightarrow ?R$
  - $[| 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 :-P
  * 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)''.
==== Safe Methods ====

:?: Which proof methods are safe and which aren't?

:!: Good question :-) This is a paragraph from the lecture notes:

<file>
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.
</file>

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 **erule**s, 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.

==== Normal vs. _tac Methods ====

:?: 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''.

==== PURE vs. HOL ====

:?: 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:

  - First, the latter is by itself a HOL formula, while the former contains HOL formulas, but is more considered a rule.
  - 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.
  - Maybe the main practical difference: the former is nicely applicable as a rule, where the latter is nearly useless.


==== Equality vs. Meta Equality ====

:?: 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.


==== Bad Simp Sets ====

:?: 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:

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

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.

==== Isabelle Meta Logic====

:?: 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.

==== simp_all vs simp+ ====

:?: 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 and other semantic methods ====

:?: 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?

===== HOL theory =====

This section covers questions about the foundations of HOL.
==== Distinguished Infinite Set ====

:?: 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.


==== Conservative Extensions ====

:?: 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.

==== Non-conservative extensions ====

:?: 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.
==== Empty Types ====

:?: 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//.

==== Axioms of HOL in Isabelle ====
:?: About the axiom of infinity:
  - Does Isabelle/HOL have the axiom of infinity or not? 
  - If it does, this means the deduction system is incomplete (because of standard models), right? 
  - If it does not include the axiom, what are the implications of that? Do we still have a true HOL system?

:!: Answer:
  - 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'': <code>
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"
</code> It is just stated there, that there exists an //injective// but //not surjective// function on this type, which //makes// the type infinite.
  - Yes, it is probably incomplete, yet I dare you to find some theorem which holds but you can't prove it in Isabelle/HOL ;-).
  - 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).
Isabelle/HOL Support Wiki

User Tools

Site Tools

Page Tools
