proof,isabelle,theorem-proving,isar , Skip a subgoal while proving in Isabelle

Skip a subgoal while proving in Isabelle


Tag: proof,isabelle,theorem-proving,isar

I am trying to prove a theorem but got stuck at a subgoal (that I prefer to skip and prove later). How can I skip this and prove the others ?

First, I tried oops and sorry but they both abort the entire proof (instead of the only subgoal). I also tried to put the subgoal into a dummy lemma (assuming proven with sorry) then using it (apply (rule [my dummy lemma])) but it applies the dummy lemma to every other subgoals (not only the first one).


It mostly depends on whether you are using the archaic (sorry for that ;)) apply-style or proper structured Isar for proving. I will give a small example to cover both styles. Assume you wanted to prove

lemma "A & B"

Where A and B just serve as placeholders for potentially huge formulas.

As structured proof you would do something like:

  show "A" sorry
  show "B" sorry

I.e., in this style you can use sorry to omit proofs for subgoals.

In apply-style you could do

apply (rule conjI)
defer -- "moves the first subgoal to the last position"
apply (*proof for subgoal "B"*)
apply (*proof for subgoal "A"*)

There is also the apply-style command prefer n which moves subgoal n to the front.


What is the difference between primrec and fun in Isabelle/HOL?

I'm reading the Isabelle tutorial and been trying to clear my concept on use of primrec and fun. With what I've searched so far, including the answer here; I understand that constructor inside primrec can have only one equation and primrec has [simp] by default whereas fun can have multiple...

How can I prove that elem z (xs ++ ys) == elem z xs || elem z ys?

I have the following: elem :: Eq a => a -> [a] -> Bool elem _ [] = False elem x (y:ys) = x == y || elem x ys How can I prove that for all x's y's and z's... elem z (xs ++ ys) == elem z xs...

Isabelle: understanding the use of quantifiers

I have found that I can prove the following lemma, which seems false to me. lemma assumes "∀a b. f a > f b ∧ a ≠ b" shows "∀a b. f b > f a" using assms by auto How can the lemma above be true? Is Isabelle substituting...

Create a quotient-lifted type with polymorphism over working set and equivalence relation in Isabelle/HOL

I would like to create a quotient type with quotient_type in Isabelle/HOL in which I would left "non-constructed" the non-empty set S and the equivalence relation ≡. The goal is for me to derive generic properties w.r.t. S and ≡ over the quotient-lifted set S/≡. In this way, it would...

Proving a simple arithmetic statement with rewriting in Isabelle

I am trying to prove a big case distinction in Isabelle for some (conceptually) simple arithmetic statement. During the proof, I stumbled upon the following subgoal. ⋀d l k. 0 < d ⟹ ¬ 2 * k + 1 ≤ 2 * l ⟹ 2 * l ≠ 1 ⟹...

Using type classes to overload notation for constructors (now a namespace issue)

This is a derivative question of Existing constants (e.g. constructors) in type class instantiations. The short question is this: How can I prevent the error that occurs due to free_constructors, so that I can combine the two theories that I include below. I've been sitting on this for months. The...

Converting a set to a list in Isabelle

How can I convert a set to a list in Isabelle? I am interested in a function definition, with the signature: "'a set => 'a list" How can I define this?...

Is there an include-like command for 'struct', similar to 'include' for 'sig'?

This question is related to how sectioning and Sidekick can be used with Isabelle/ML in Isabelle/jEdit. Consider two Isar commands, section and ML. These commands act as sectioning commands in the tree of the jEdit Sidekick plugin. One consequence is that I can use multiple ML{*...*} statements in a THY...

Why do we need to use the negation part in Turing's Halting Proof?

For instance, let's say I have this Turing machine, H, which tells us whether or not a program and input will halt. Let's say we call H on itself. It has to give an answer, so if it prints out "does not halt" then didn't it technically halt to print...

Isabelle: Unsupported recursive occurrence of a datatype via type constructor “Set.set”

The problem I am wondering if is there a natural way of encoding in Isabelle a grammar like this: type_synonym Var = string datatype Value = VInt int | ... datatype Cmd = Skip | NonDeterministicChoice "Cmd set" | ... The motivation would be to give definition a few specification...

What's the difference between “arith” and “presburger” in Isabelle?

Every goal that I have encountered in Isabelle so far that could be solved using arith could also be solved by presburger and vice versa, for example lemma "odd (n::nat) ⟹ Suc (2 * (n div 2)) = n" by presburger (* or arith *) What's the difference between the...

Handling let in hypothesis

As an exercise in Coq, I'm trying to prove that the following function returns a pair of lists of equal length. Require Import List. Fixpoint split (A B:Set)(x:list (A*B)) : (list A)*(list B) := match x with |nil => (nil, nil) |cons (a,b) x1 => let (ta, tb) := split...

Apply lemmas to bound variables

I can prove the following lemma: lemma lem1: assumes "(a::real) ≤ b / c" and "c > 0" shows "a * c ≤ b" using assms using pos_le_divide_eq[of "c" "a" "b"] by auto however, if I use bound variables, the proof does not work. lemma lem2: assumes "∀a b c....

Trying to define custom 'declare' & 'using' commands

I figure out how to modify some Isar and ML, but here I don't know how to get what I want. I use declare and using to turn info on and off, like with these (and other longer combinations): declare[[simp_trace_new mode=full]] declare[[show_sorts=false]] using[[simp_trace_new mode=full]] using[[show_sorts=false]] I've created jEdit macros to...

Needs a proof in a part of prime factorisation

According to topcoder Link, We need to compute till square root of number to list its all prime factors... Now I am able to prove in the following code that we are doing right till we are in the for loop.. But I am unable to figure out why the...

Substitution in Isabelle

In many paper proofs you see authors substitute variables in equations. For example, if there is an inequality "f(x-y) >= g(x-y)*z, the author simply writes let h=(x-y), therefore "f(h) >= g(h)*z" and continues with the proof. To do the same in Isabelle, would I have to assume that h=(x-y), is...

Converting free variables to bound variables

I want to prove the following lemma lemma assumes "f (w+n) - f w / n ≤ g (w+n)" shows "∀n. (f (w+n) - f w) / n ≤ g (w+n)" I assumed this would be very simple however it is proving trickier than I first thought. From my thoughts,...

Variable arity function in Isabelle

Is it possible to define using the Isabelle proof assistant a theory involving functions of variable arity ? For example, I would like to define the theory of all predicates of arity n, which are invariant by cyclic permutation. Given a type T and an integer n, I would like...

Concatenation of undef and list is undef - proof Haskell

How could one prove that the following is true for every list xs: undefined ++ xs = undefined ...

De Bruijn indices in Isabelle and Coq

I would like to be able use something like de Bruijn indices in Isabelle or in Coq, in order to refer to variables that have been introduced by quantifiers. For example, instead of writing: forall x. forall y. (p x y) I would like to write something like: forall x....

Inductive predicate with type parameters in Isabelle

I started learning Isabelle and wanted to try defining a monoid in Isabelle but don't know how. In Coq, I would do something like this: Inductive monoid (τ : Type) (op: τ -> τ -> τ) (i: τ): Prop := | axioms: (forall (e: τ), op e i = e)...

Substituting for the lambda expression in Isabelle

Given the function f: definition f :: "real => real" where "f x = x" I can show that as n tends to 0, f(x+n) tends to f(x) by the following lemma lemma "(λn. f(x+n)) -- 0 --> f x" unfolding f_def apply (auto intro!: tendsto_eq_intros) done As a further...

Skip a subgoal while proving in Isabelle

I am trying to prove a theorem but got stuck at a subgoal (that I prefer to skip and prove later). How can I skip this and prove the others ? First, I tried oops and sorry but they both abort the entire proof (instead of the only subgoal). I...

Compute the highest value with a given list and operators in OCaml

With a given positive integer list and the addition and the multiplication as operators, I want to compute the highest value. So if my list is [2,3,4], it will be : 2 * 3 * 4 = 24. If there is at least one 1 in the list, it is...

Isabelle solvers: “auto” or “fastforce”? (comparison of solver strength)

In Isabelle, I often find that I can prove a goal successfully using different solvers. Generally I would prefer to use the weakest solver that can just about prove the goal. Based on my experience with Isabelle so far, my current understanding is that in order of increasing strength and...

Formal proof for what algorithm return

I need to formal proof that below algorithm return 1 for n = 1 and 0 in other cases. function K( n: word): word; begin if (n < 2) then K := n else K := K(n − 1) * K(n − 2); end; Anyone could help? Thank you...

Proving integration within a set

I am attempting to use the fundamental theorem of calculus to prove the lemma lm1: lemma lm1: fixes f :: "real ⇒ real" assumes "∀x∈{a..b}. (f has_vector_derivative f' x) (at x within {a .. b})" "∀x∈{a..b}. a ≤ x" "∀x∈{a..b}. x ≤ b" shows "∀x∈{a..b}. (f' has_integral (f x -...

How to prove x + y - z = x + (y - z) in Coq

I want to prove this : 1 subgoals x : nat y : nat z : nat ______________________________________(1/1) x + y - z = x + (y - z) It looks trivial, but it confuse me a lot, and I need it for another proof. Thanks....

Solving (BEq a a0 = BTrue \/ BEq a a0 = BFalse) in Coq

(BEq a a0 = BTrue \/ BEq a a0 = BFalse) is either true or false since a==a0 or a!=a0. However, I'm not sure how I can get Coq to see this. Here is my complete proof window: 4 subgoal a : aexp a0 : aexp st : state ______________________________________(1/4)...

Isabelle: locale interpration about record fails in proof

Using the Algebra library, I encountered the following problem. In a proof I wanted to interpret the additive structure of a ring as a group. Here is a sample code: theory aaa imports "~~/src/HOL/Algebra/Ring" begin lemma assumes "ring R" shows "True" proof- interpret ring R by fact interpret additive: comm_group...

Agda: Simulate Coq's rewrite tactic

I have some experience using Coq and am now in the process of learning Agda. I'm working on a correctness proof of insertion sort and have reached a point where I would like to perform something similar to Coq's rewrite tactic. Currently, I have: open import Data.Nat open import Relation.Binary.PropositionalEquality...

Rewriting with non-equality equivalence-relations using Isabelle simplifier

I would like to use the simplifier to replace subterms that are not equalities. Instead of a generic definition of my problem, I will illustrate this by an example: Say I have a simple programming language and a Hoare logic on top of it. Say we have if, while, and...

Why won't simp handle this term inside of a lambda expression?

I have proven this simp rule: lemma AAA: the_sector (log_update ?f ?s) ?p = the_sector ?s ?p The rule is not used to simplify the following: lemma BBB: "(λA. if A then (the_sector (log_update f s) p) else B) = (λA. if A then (the_sector s p) else B)" I...

Proving topology statement in Isabelle

I have been working with limits and topology in and I want to prove the following lemma: lemma fixes f g :: "real ⇒ real" assumes "open S" "∀a b. a < b <--> f a < f b" "∀a. (f a)>0" "continuous_on UNIV (f)" "∀w∈S. ∀h. (w+h)∈S --> h...

If f(n) = O(h(n)) then c*f(n) = O(h(n)) for all c > 0 - proof challenged?

I have been asked to prove or disprove the following conjecture: For any given constant c>0 | If f(n) = O(h(n)) then c*f(n) = O(h(n)) I have came up with the following counter example: Let f(n) = n and c = n+1. Then c*f(n) = (n+1)n = n^2+n = O(n^2),...

Proof assistant for mathematics only

Most proof assistants are functional programming languages with dependent types. They can proof programs/algorithms. I'm interested, instead, in proof assistant suitable best for mathematics and only (calculus for instance). Can you recommend one? I heard about Mizar but I don’t like that the source code is closed, but if it...

Proving st X + st Y = st Y + (st X - 1) + 1 using Coq

Just like the title says, I'm looking for a way to prove st X + st Y = st Y + (st X - 1) + 1 in Coq. I've been trying applying various combinations of plus_comm, plus_assoc and plus_permute but I haven't been able to make it go through....

Merging two small sequencies - algorithm

Prove that it is enough to make at most 5 comparisons in order to merge two sorted sequences of lengths 2 and 5.

How to understand the time complexity of Kademlia node operation

I'm now learning Kademlia network by reading the classical paper Kademlia: A Peer-to-peer Information System Based on the XOR Metric. I want to understand the complexity of its operation but still cannot figure it out. In the 3 Sketch of proof section, the paper gives two definitions: Depth of a...

Existing constants (e.g. constructors) in type class instantiations

Consider this Isabelle code theory Scratch imports Main begin datatype Expr = Const nat | Plus Expr Expr it is quite reasonable to instantiate the plus type class to get nice syntax for the Plus constructor: instantiation Expr :: plus begin definition "plus_Exp = Plus" instance.. end But now, +...

how to make an example to test the rev_app immediately after lemma proved. an starting example for custom lemma

expect to use the subgoal to run the list which defined by let? aa = [1,2] and run rev_app on this aa and show the value as [2,1] theory Scratch2 imports Datatype begin datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65) (* This is...

Asymptotic notation and Growth of Combinations of Functions: Difference

I need to prove or disprove the following conjecture: if f(n) = O(h(n)) AND g(n) = O(k(n)) then (f − g)(n) = O(h(n) − k(n)) I am aware of the sum and product theorems for growth combination, but I could not find a way to apply them here, even though...

Asymptotic notation: How to prove that n^2 = Ω(nlogn)?

I was asked to prove or disprove the following conjecture: n^2 = Ω(nlogn) This one feels like it should be very easy, and intuitively it seems to me that because Ω is a lower bound function, and n^2 is by definition of higher magnitude than nlogn, then it is also...

Fixed Point and Proof theory

For any given logic program, proof theory of it uses SLD (Selective Linear Definite) resolution to find the satisfiablity of the query. For the same logic program, we can apply fixed point theorem to find the models. My question is, should we consider finding fixed point of logic programs as...

An example of pratical application of Isabelle/HOL

I have looked into the Isabelle tutorial which presents an example of it's use in verifying security protocol. However, it is a bit out of my understanding as I only know the basics. I'm looking for some examples which are not just simple theorems but practical applications using Isabelle/HOL. For...

Apply simplifier to arbitrary term

I have a term in mind, say "foo 1 2 a b", and I'd like to know if Isabelle can simplify it for me. I'd like to write something like simplify "foo 1 2 a b" and have the simplified term printed in the output buffer. Is this possible? My...