Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] "xa ∈ carrier (free_group gens1) ⟹ xa ∈ carrie...

Email Gateway (Aug 18 2022 at 15:12):

From: Lawrence Paulson <lp15@cam.ac.uk>
I was able to diagnose your problem by enabling the option show_consts:

goal (1 subgoal):

1. xa : carrier (free_group gens1) ==> xa : carrier (free_group gens1)
   constants:
   ...
   free_group ::
   ('b => bool)
   => (| carrier :: (bool * 'b) list => bool,
   mult :: (bool * 'h) list => (bool * 'h) list => (bool * 'h) list, one :: (bool * 'h) list |)
   ...
   free_group ::
   ('b => bool)
   => (| carrier :: (bool * 'b) list => bool,
   mult :: (bool * 'i) list => (bool * 'i) list => (bool * 'i) list, one :: (bool * 'i) list |)

The two occurrences of free_group have different types! You can correct this situation by inserting type constraints.

Larry Paulson

Email Gateway (Aug 18 2022 at 15:13):

From: Joachim Breitner <mail@joachim-breitner.de>
Hi,

thaks, works perfectly. I can turn off quick_and_dirty mode again, feels
much better :-)

Greetings,
Joachim
signature.asc

Email Gateway (Aug 18 2022 at 15:23):

From: Joachim Breitner <mail@joachim-breitner.de>
Hi,

I’m currently working on a submission to the AFP, formalizing the
construction of Free Groups. While proving that bijective sets of
generators produce isomorphic Free Groups, I came across a problem where
I cannot continue, and it seems to be an Isabelle bug.

In line of 337 of
http://darcs.nomeata.de/afp-Free-Groups/Free-Groups.thy
I try to do this
assume "x ∈ image (map (prod_fun id f)) (carrier (free_group gens1))"
then obtain y :: "(bool × 'b) list" where "x = map (prod_fun id f) y"
and "y ∈ carrier (free_group gens1)"
and expected to close this using "by auto", as I did in similar
situations before. This fails. Unwrapping the proof and trying to do it
manually with Isar steps, I end up with this state (as given by i3p):

proof (prove): step 38

goal (1 subgoal):

1. xa ∈ carrier (free_group gens1) ⟹ xa ∈ carrier (free_group gens1)
   variables:
   thesis :: bool
   f :: 'b ⇒ 'c
   x :: (bool × 'c) list
   gens1 :: 'b ⇒ bool
   xa :: (bool × 'b) list
   type variables:
   'b, 'c, 'h, 'i :: type

but "apply assumption" does not work. It is also not a i3p bug, as the
IsaMakefile also fails to build the theory.

I’d be grateful if someone else could try it and see if he can reproduce
the problem, and maybe tell me how I can work around the issue. The
theory Free-Groups also uses
http://darcs.nomeata.de/afp-Free-Groups/Cancelation.thy
and if you have darcs installed, you can just run
darcs get http://darcs.nomeata.de/afp-Free-Groups/

Thanks,
Joachim
signature.asc

Last updated: Apr 25 2024 at 08:20 UTC