Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] confusion with obtain

Email Gateway (Feb 13 2025 at 10:40):

From: Phil Rieckmann <phirie@uni-bremen.de>
Dear Isabelle users,

i had a problem with a proof that can be shown with this example:

datatype( 'a, 'e) state_result =
    Value " 'a "
    | Ex " ( 'e )"

definition u :: "(int, 'e)state_result set" where
  "u ≡ undefined"

lemma existence:
  "∃v. u  =  {Value(v)}"
  sorry

lemma something: "A"
proof -
  obtain v where v_def: "u  =  {Value(v)}"
    using existence by blast
  hence "u  =  {Value(v)}"
    try

The last formula does not seem provable (with try).
I don't understand how v is influenced by 'e, v is always of type int.
If i change 'e to int, auto can proof it. I'm still using Isabelle2022.

Can someone explain me, whats happening here?

Phil

Email Gateway (Feb 13 2025 at 10:49):

From: Jan van Brügge <jan@vanbruegge.de>
Hi,

if you ctrl-hover over both u in your proof, you see that one has type
(int, 'a) state_result set while the other is (int, 'b) state_result set.

Adding a type annotation makes this work:

lemma something: "A"
proof -
  obtain v where v_def: "(u::(int, 'a) state_result set)  = {Value(v)}"
    using existence by blast
  hence "(u::(int, 'a) state_result set)  =  {Value(v)}"
    by simp

Cheers,
Jan

Am 13.02.25 um 10:12 schrieb Phil Rieckmann:

Dear Isabelle users,

i had a problem with a proof that can be shown with this example:

datatype( 'a, 'e) state_result =
    Value " 'a "
    | Ex " ( 'e )"

definition u :: "(int, 'e)state_result set" where
  "u ≡ undefined"

lemma existence:
  "∃v. u  =  {Value(v)}"
  sorry

lemma something: "A"
proof -
  obtain v where v_def: "u  =  {Value(v)}"
    using existence by blast
  hence "u  =  {Value(v)}"
    try

The last formula does not seem provable (with try).
I don't understand how v is influenced by 'e, v is always of type int.
If i change 'e to int, auto can proof it. I'm still using Isabelle2022.

Can someone explain me, whats happening here?

Phil

Email Gateway (Feb 13 2025 at 10:55):

From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>

Am 13.02.2025 um 11:12 schrieb Phil Rieckmann <phirie@uni-bremen.de>:

Dear Isabelle users,

i had a problem with a proof that can be shown with this example:

datatype( 'a, 'e) state_result =
Value " 'a "
| Ex " ( 'e )"

definition u :: "(int, 'e)state_result set" where
"u ≡ undefined"

lemma existence:
"∃v. u = {Value(v)}"
sorry

lemma something: "A"
proof -
obtain v where v_def: "u = {Value(v)}"
using existence by blast
hence "u = {Value(v)}"
try

The last formula does not seem provable (with try).
I don't understand how v is influenced by 'e, v is always of type int.
If i change 'e to int, auto can proof it. I'm still using Isabelle2022.

Can someone explain me, whats happening here?

v can be influence by ‘e. Have a look at the following modified version
of the definition of u. If one replaces your try by sorry, then one can prove
anything.

definition u :: "(int, 'e)state_result set" where
"u ≡ {Value (int (card(UNIV :: 'e set)))}"

lemma existence:
"∃v. u = {Value(v)}"
unfolding u_def by auto

lemma something: "A"
proof -
let ?u1 = "u :: (int, bool) state_result set"
let ?u2 = "u :: (int, unit) state_result set"
obtain v where v_def: "?u1 = {Value(v)}"
using existence by blast
hence "?u2 = {Value(v)}" sorry
hence "v = 1" unfolding u_def by auto
moreover from v_def have "v = 2" unfolding u_def by auto
ultimately show A by auto
qed

Best,
René

Last updated: Mar 09 2025 at 12:28 UTC