Questions about isabelle
Read more about isabelle
python (65.2k questions)
javascript (44.3k questions)
reactjs (22.7k questions)
java (20.8k questions)
c# (17.4k questions)
html (16.3k questions)
r (13.7k questions)
android (13k questions)
Isabelle/jEdit just starts with ~/Scratch.thy (or does not launch) by clicking .thy file or using open command in MacOS
Recently, I restarted playing with Isabelle/HOL.
However, I faced the following problem in MacOS (Monterey):
When I click foo.thy file, Isabelle/jEdit launches but ignores foo.thy and starts with ~/Sc...
snufkin26
Votes: 0
Answers: 0
What's mean "Result contains obtained parameters: b" in Isabelle?
Consider the following code fragment:
lemma ejercicio_10_MSV2:
fixes P Q :: "'b ⇒ bool"
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
proof -
{ assume "P...
María Eugenia irizo cruz
Votes: 0
Answers: 1
Proving correctness and termination of an (imperative) algorithm using Isabelle
I'm an undergraduate student trying to prove correctness and termination of imperative version of Euclidean gcd and Euclidean extended gcd algorithm. I used IMP language to implement the first one and...
Hamed
Votes: 0
Answers: 1
Is there a way to apply the rule to a specific assumption in Isabelle?
Here is my goal
...
∀a b. P1 a b ⟹
∀a b. P2 a b ⟹
...
⟹ some goal
I want to apply the lemma to the second assumption
lemma K: ⟦ ∀a b. P a b⟧ ⟹ ∀b. P a b"
by using
apply (drule_tac a = "...
Huan Sun
Votes: 0
Answers: 1