From: John Wickerson <jpw48@cam.ac.uk>
Dear Isabelle,
My attempt to make a typedef for finite sets ...
typedef 'a fset = "{A :: 'a set . finite A }"
by (rule exI[of _ "{}"], auto)setup_lifting type_definition_fset
... results in the following warning message.
Generation of a parametrized correspondence relation failed.
Reason: No relator for the type "Set.set" found.
Could somebody kindly tell me how I can address this? Thanks.
john
From: Ondřej Kunčar <kuncar@in.tum.de>
The relator for sets is defined in ~~/src/HOL/Library/Quotient_Set.
Including this file should remove the warning.
The warning is currently not really harmful because parametrized
correspondence relations are not used in Isabelle2013. I didn't include
other improvements of the Lifting package that depends on them to the
coming release. Maybe in the next release this will come into play.
Ondrej
From: John Wickerson <jpw48@cam.ac.uk>
Thanks Ondrej.
Continuing my attempt to make a typedef for finite sets, I've managed to lift definitions like "union" from sets to finite sets. I'm now trying to lift "big union" from sets of sets to finite sets of finite sets, but this turns out to be less trivial. Could somebody kindly advise on how to do this proof?
Below is my complete .thy file.
Thanks very much,
john
------8<--------
theory J_Finite_Set imports
Main
"~~/src/HOL/Library/Quotient_Set"
begin
typedef 'a fset = "{A :: 'a set . finite A }"
by (rule exI[of _ "{}"], auto)
setup_lifting type_definition_fset
lift_definition
union_fset :: "'a fset ⇒ 'a fset ⇒ 'a fset"
is "union :: 'a set ⇒ 'a set ⇒ 'a set"
by simp
lift_definition
Union_fset :: "('a fset) fset ⇒ 'a fset"
is "Union :: 'a set set ⇒ 'a set"
(* not worked out how to prove this yet *)
sorry
end
------8<--------
From: Ondřej Kunčar <kuncar@in.tum.de>
You might want to take a look to ~~/src/HOL/Quotient_Examples/Lift_DList
and ~~/src/HOL/Quotient_Examples/Lift_FSet.
You can find two operations using nested types there
concat :: "'a dlist dlist => 'a dlist (it uses typedef)
fconcat :: "'a fset fset => 'a fset" (it uses quotient)
and also corresponding proofs.
I think the example with 'a dlist is more suitable for what you are
doing in your formalization because 'a dlist is defined as a typedef.
Ondrej
From: John Wickerson <jpw48@cam.ac.uk>
Thanks again, Ondrej.
I have one further question on this topic, which can be summarised as "How can I make the transfer method work properly inside a context?".
In more detail: suppose I'm working inside a context that gives me the assumption "P f" for some fixed f. I write a lemma involving f, and begin the proof by applying the transfer method. The transfer method generalises f, and thus loses the fact that P holds for it.
I find that I can survive, just about, by inserting "P f" before applying the transfer method. But this feels rather unscalable.
All of this is explained in further detail in the following theory file.
Best wishes,
John
---------8<----------
theory Scratch imports
Main
"~~/src/HOL/Library/Quotient_Set"
begin
locale always_true =
fixes f :: "'a ⇒ bool"
assumes always_true: "f x = True"
begin end
typedef 'a fset = "{A :: 'a set . finite A }"
by (rule exI[of _ "{}"], auto)
setup_lifting type_definition_fset
lift_definition
fset_member :: "'a ⇒ 'a fset ⇒ bool" (infix "|∈|" 50)
is "op ∈" by simp
context always_true begin
lemma "a |∈| A ⟹ f a"
apply transfer
oops
lemma "a |∈| A ⟹ f a"
apply (insert always_true)
apply transfer
apply auto
done
end
end
---------8<----------
From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi John,
With the option fixing, you can tell transfer not to generalize certain
variables:
apply(transfer fixing: f)
Hope this helps,
Andreas
From: Ondřej Kunčar <kuncar@in.tum.de>
Just citing from The Isabelle/Isar Reference Manual:
Goals are generalized over all free variables by default; this is
necessary for variables whose types change, but can be overridden for
specific variables with e.g. transfer fixing: x y z.
Ondrej
From: Makarius <makarius@sketis.net>
I've occasionally seen this from a distance, but did not look more closely
(and right now I am also busy with the Isabelle2013 release).
Historically, the treatment of Free variables as arbitrary might stem from
the original HOL4 version of the quotient mechanism by Peter Homeier, when
it was ported to Isabelle/HOL for the first time. But Isabelle has a
clear notion of "fixed variable" within a context, which act as local
constants by default. So the above exception declaration via "fixing"
looks more like a hot fix.
A more standard way in Isabelle is to leave things as fixed as they are
already in the context, unless the users says differenly by augmenting the
"eigen context" of some language element. The "ind_cases" proof method is
an example for that, it uses the "for" syntax for that. (The same "for"
notation helped out in many conceptually difficult situations in locale
expressions some years ago.)
Makarius
Last updated: Mar 29 2024 at 08:18 UTC