FAQ Database Discussion Community


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

isabelle
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...

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

isabelle
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...

Isabelle: understanding the use of quantifiers

isabelle
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...

Proving topology statement in Isabelle

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

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

typeclass,isabelle
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, +...

Apply lemmas to bound variables

isabelle
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....

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

set,higher-order-functions,isabelle,theorem-proving,isar
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...

Variable arity function in Isabelle

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

Inductive predicate with type parameters in Isabelle

coq,isabelle,type-parameter
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)...

Substitution in Isabelle

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

Isabelle: locale interpration about record fails in proof

locale,record,isabelle,interpretation
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...

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

isabelle
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...

Skip a subgoal while proving in Isabelle

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

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

sml,ml,isabelle
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...

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

isabelle
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...

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

solver,isabelle,theorem-proving
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...

Proving a simple arithmetic statement with rewriting in Isabelle

isabelle,isar
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 ⟹...

Converting free variables to bound variables

isabelle
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,...

An example of pratical application of Isabelle/HOL

isabelle
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...

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

recursion,isabelle,theorem-proving
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 is the difference between primrec and fun in Isabelle/HOL?

isabelle
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...

Apply simplifier to arbitrary term

isabelle
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...

Proving integration within a set

isabelle
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 -...

De Bruijn indices in Isabelle and Coq

coq,isabelle
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....

Substituting for the lambda expression in Isabelle

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

Rewriting with non-equality equivalence-relations using Isabelle simplifier

isabelle
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...

Converting a set to a list in Isabelle

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

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

solver,isabelle,theorem-proving
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...