Email Gateway (Aug 19 2022 at 12:43): Email Gateway (Aug 19 2022 at 12:43):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
I think I understand that BNF is a work in progress, but I report some
errors I get when trying to use it. I'll do that second, since the first
part sets the context. The good news is that it works well enough to use it.
For the first part, I have a datatype, "'a mT", and an equality function
for that type, mTeq. I want to declare mTeq as equality for "'a mT", but
I don't understand all the complexities of overloading in Isabelle.
I want to make the simple statement, "foo x y ==> (x::'a mT) = y", but I
can't. I would have to introduce new notation for "=", and then use that.
For anyone who has time, I give a brief summary of my application, I
include the source at the bottom, and I attach the file.
I have a main datatype:
datatype 'a mT =
mTp "'a * int"
|mTL "'a mT list"
And then a secondary datatype:
datatype_new 'a mS =
mSp "'a * int"
|mSS "'a mS fset"
The type "'a mT" is list of ordered pairs, and nested lists of ordered
pairs. For a pair "mTp (x,y)", y is the multiplicity, where the
multiplicities of pairs with the same first component name, at the save
level of nesting, can be added together. The type int allows for
negative quantities, where int could be replaced with a type class, such
as linordered_ab_group_add.
For an equality function, I first define a function mTcomb, which
combines any pairs with the same name, at the same level of nesting,
into one pair, by adding their multiplicities.
I then define a function mTset. This converts lists to fsets, the lists
and fsets used in the constructors mTL "'a mT list" and mSS "'a mS
fset".
My equality function is then mTeq, with 3 simple cases, and the fourth
case using mTcomb and mTset:
"mTeq (mTL x) (mTL y) = (mTset (mTL(mTcomb [] (mTL x))) = mTset
(mTL(mTcomb [] (mTL y))))"
That takes you to the bottom of my file, where I try to instantiate type
mT as type class equal. It doesn't work, which makes me wonder why I
think I need to do that.
---CONCERNING BNF ERRORS
As to BNF, again I have this datatype:
datatype_new 'a mS =
mSp "'a * int"
|mSS "'a mS fset"
What I think I've found is that I can use it on the right side of
recursive functions, but I can't use it on the left side.
I try using datatype_new_compat, and also primrec instead of fun. I
tried to define a function to use "'a mS fset option", but it doesn't
work, where a function like that for mT does work.
Thanks,
GB
theory i131031a__v5a__generalized_datatype_to_model_a_nested_set
imports Complex_Main BNF ("../../../iHelp/i")
begin
(__1__) MULTILIST: datatype and utility functions.)
datatype 'a mT =
mTp "'a * int"
|mTL "'a mT list"
fun mTp_1st :: "'a mT => 'a option" where
"mTp_1st (mTp(x,y)) = Some x"
|"mTp_1st (mTL x) = None"
fun mTp_2nd :: "'a mT => int option" where
"mTp_2nd (mTp(x,y)) = Some y"
|"mTp_2nd (mTL x) = None"
fun mTLsome :: "'a mT => 'a mT list option" where
"mTLsome (mTp x) = None"
|"mTLsome (mTL x) = Some x"
(__2__) MSET: datatype and utility functions.)
datatype_new 'a mS =
mSp "'a * int"
|mSS "'a mS fset"
datatype_new_compat "mS"
primrec mSSsome :: "'a mS => 'a mS fset option" where
"mSSsome (mSp x) = None"
|"mSSsome (mSS x) = Some x"
fun mSSsome2 :: "'a mS => 'a mS fset option" where
"mSSsome2 (mSp x) = None"
|"mSSsome2 (mSS x) = Some x"
(*__3__) COMBINE BY ADDING MULTIPLICITIES: Start with L = [].
CASE mTp(x,y): If there exists mTp(x,z) in List.set L, then remove
mTp(x,z)
from L and return mTp(x,y+z)#L. If there exists no mTp(x,z), then
return
mTp(x,y)#L.
CASE mTL(x#xs): If x is just a pair, then "mTcomb (mTcomb L (mTL xs))
x". The
"mTcomb L (mTL xs)" will recursively work on the list which x will
be given.
CASE mTL(x#xs): If x is a mTL, then mTL(mTcomb [] x)) # (mTcomb L
(mTL xs)).
The "mTL(mTcomb [] x))" will work on adding, to a new empty list, the
multiplicities in the list of "mTL x"*)
fun mTcomb :: "'a mT list => 'a mT => 'a mT list" where
"mTcomb L (mTp(x,y)) = (
if List.find (%z. mTp_1st z = Some x) L
= Some(mTp(x,the(mTp_2nd(the(List.find(%z. mTp_1st z = Some x)
L)))))
then mTp(x,y + the(mTp_2nd(the(List.find(%z. mTp_1st z = Some x) L))))
# (remove1(the(List.find(%z. mTp_1st z = Some x) L)) L)
else (mTp(x,y))#L)"
|"mTcomb L (mTL []) = L"
|"mTcomb L (mTL(x#xs)) = (if mTLsome x = None
then (mTcomb (mTcomb L (mTL xs)) x)
else (mTL(mTcomb [] x)) # (mTcomb L (mTL xs)))"
value "mTcomb [] (mTL[mTp(x,1),mTL[mTp(x,y)],mTp(x,2)])"
value "mTcomb []
(mTL[mTp(x,9),mTL[mTp(x,1),mTL[mTp(x,2),mTp(y,2)]],mTp(x,3),mTp(x,4),mTL[mTp(x,5)]])"
value "mTcomb []
(mTL[mTp(1::int,9),mTL[mTp(1,1),mTL[mTp(1,2),mTp(y,2)]],mTp(1,3),mTp(1,4),mTL[mTp(1,5)]])"
(*__4__) FSET: Equality of a set is easy to state because it doesn't
have to be
ordered.*)
fun mTset :: "'a mT => 'a mS fset" where
"mTset (mTp x) = {|mSp x|}"
|"mTset (mTL []) = fempty"
|"mTset (mTL(x#xs)) = (if mTLsome x = None
then funion (mTset x) (mTset (mTL xs))
else finsert (mSS(mTset x)) (mTset (mTL xs)))"
theorem "mTset (mTL[mTp(x,1),mTL[mTp(x,y)],mTp(x,2)]) = z"
apply simp oops
theorem "mTset
(mTL[mTp(x,9),mTL[mTp(x,1),mTL[mTp(x,2),mTp(y,2)]],mTp(x,3),mTp(x,4),mTL[mTp(x,5)]])
= z"
apply simp oops
theorem "mTset
(mTL[mTp(1::int,9),mTL[mTp(1,1),mTL[mTp(1,2),mTp(y,2)]],mTp(1,3),mTp(1,4),mTL[mTp(1,5)]])
= z"
apply simp oops
(__5__) EQUALITY: The 4th case is what takes all the work.)
fun mTeq :: "'a mT => 'a mT => bool" where
"mTeq (mTp x) (mTp y) = (x = y)"
|"mTeq (mTp x) (mTL y) = ([mTp x] = y)"
|"mTeq (mTL x) (mTp y) = (x = [mTp y])"
|"mTeq (mTL x) (mTL y) = (mTset (mTL(mTcomb [] (mTL x))) =
mTset (mTL(mTcomb [] (mTL y))))"
theorem "mTset
(mTL[mTp(x,9),mTL[mTp(x,1),mTL[mTp(x,2),mTp(y,2)]],mTp(x,3),mTp(x,4),mTL[mTp(x,5)]])
= z"
apply simp
(*{|mSS{|mSS{|mSp(y,2),mSp(x,2)|},mSp(x,1)|},mSS{|mSp(x,5)|},mSp(x,4),mSp(x,3),mSp(x,9)|}
= z*)
oops
theorem "mTset
(mTL[mTp(x,3),mTp(x,9),mTp(x,4),mTL[mTp(x,5)],mTL[mTp(x,1),mTL[mTp(x,2),mTp(y,2)]]])
= z"
apply simp
(*{|mSS{|mSp(x,5)|},mSS{|mSS{|mSp(y,2),mSp(x,2)|},mSp(x,1)|},mSp(x,4),mSp(x,9),mSp(x,3)|}
= z*)
oops
theorem "mTeq
(mTL[mTp(x,9),mTL[mTp(x,1),mTL[mTp(x,2),mTp(y,2)]],mTp(x,3),mTp(x,4),mTL[mTp(x,5)]])
(mTL[mTp(x,3),mTp(x,9),mTp(x,4),mTL[mTp(x,5)],mTL[mTp(x,1),mTL[mTp(x,2),mTp(y,2)]]])"
by(auto)
(*Trying to define equal for type "'a mT". I don't know if I even need to to
this.*)
instantiation mT :: equal
begin
definition
"HOL.equal x y = (mTeq x y)"
instance
proof
qed
end
(******************)
end
(******************)
i131031a__v5a__generalized_datatype_to_model_a_nested_set.thy
Email Gateway (Aug 19 2022 at 12:45):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Gottfried,
You cannot define equality in Isabelle/HOL for any type as you wish, as the HOL axioms
already define it for all types. The datatype package (and the BNF package) introduce an
algebraic type whose constructors are free, i.e., injective and their ranges pairwise
distinct. If you want to have a coarser notion of equality, you can define your own
function such as mTeq with fancy notation such as (infix "==="), but you cannot use HOL
equality = for it, and the proof tools (esp. the simplifier) will not treat it as equality
either.
If you really want a type with your custom equality relation, you have to quotient your
datatype through your custom equality relation [1] or directly construct a type with
non-free type constructors [2]. You find more information on that in the references, but I
have not examined your use case to see which route seems easier or feasible.
Andreas
[1] http://www21.in.tum.de/~kuncar/documents/huffman-kuncar-cpp2013.pdf
[2]
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-August/004413.html
Email Gateway (Aug 19 2022 at 12:47):From: Gottfried Barrow <gottfried.barrow@gmx.com>
The BNF crew can officially consider that this error report has been
resolved to my satisfaction, primarily because I should have been using
primrec_new instead of primrec, though up to this point, I've stayed
away from using primrec, because the magic of fun can kick in where the
magic of primrec ends. Consequently, there being no fun_new caused me to
forget about primrec_new, until things led me back to datatype.pdf
Here, Andrea's answer to my question about equality led me to a
reference he gave me, which led me back to datatype.pdf.
I don't care that I can't make fun work with datatype_new, as long as
primrec_new is working for me.
However, if one of the BNF crew cares, below is what I get, which could
be due to me doing things wrong, or not knowing how to register
something to make it work. I give an example of "value" returning an
error, where I know that "value" and the code generator can be a whole
different matter.
Regards,
GB
datatype_new 'a mS =
mSp "'a * int"
|mSS "'a mS fset"
primrec_new mSSsome :: "'a mS => 'a mS fset option" where
"mSSsome (mSp x) = None"
|"mSSsome (mSS x) = Some x"
theorem "mSSsome (mSS{|mSp x|}) = Some {|mSp x|}"
by(simp)
theorem "mSSsome (mSp x) = None"
by(simp)
value "mSSsome (mSp x)"
(*ERROR:
"c.mS.mSp" is not a constructor, on left hand side of equation, in theorem:
mSSsome (mSp ?x) ≡ None*)
datatype_new_compat "mS"
(*ERROR:
Unsupported recursion via type constructor "FSet.fset" not associated with
new-style datatype (cf. "datatype_new")*)
fun mSSsome2 :: "'a mS => 'a mS fset option" where
"mSSsome2 (mSp x) = None"
|"mSSsome2 (mSS x) = Some x"
(*Malformed definition:
Non-constructor pattern not allowed in sequential mode.
⋀x. mSSsome2 (mSp x) = None*)
Email Gateway (Aug 19 2022 at 12:49):From: Dmitriy Traytel <traytel@in.tum.de>
Am 07.11.2013 16:29, schrieb Gottfried Barrow:
However, if one of the BNF crew cares, below is what I get, which
could be due to me doing things wrong, or not knowing how to register
something to make it work. I give an example of "value" returning an
error, where I know that "value" and the code generator can be a whole
different matter.
In this case it is simply the case that the new datatypes are not yet
registered in the code generator. A simple
code_datatype mSp mSS
will make the "value" command work for now. There is some more useful
default code generator setup (see e.g.
$AFP/thys/Coinductive/Coinductive_List) that is as well on our agenda
(to make it happen automatically) as the interaction with fun (as Jasmin
mentioned).
Dmitriy
datatype_new 'a mS =
mSp "'a * int"
|mSS "'a mS fset"primrec_new mSSsome :: "'a mS => 'a mS fset option" where
"mSSsome (mSp x) = None"
|"mSSsome (mSS x) = Some x"theorem "mSSsome (mSS{|mSp x|}) = Some {|mSp x|}"
by(simp)theorem "mSSsome (mSp x) = None"
by(simp)value "mSSsome (mSp x)"
(*ERROR:
"c.mS.mSp" is not a constructor, on left hand side of equation, in
theorem:
mSSsome (mSp ?x) ≡ None*)
Email Gateway (Aug 19 2022 at 12:49):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Andreas,
Thanks for the help again. I looked at [2] a little, but without knowing
the advantages of either, I'd pick [2] over [1]. That's because I
constantly see emails about lifting and transfer, where quotients are a
part of that, so I need to learn all that anyway. The doc [2] also gives
some instruction about specific Isar commands related to that, and
explains things like Reb and Abs.
From [1], they write, "Building a theory library that implements a new
abstract type can take a lot of work." If I knew my datatype was going
to be a winner, then I'd want to research it all and set things up
right, because you only want to do things once. However, the datatype
could be a loser, so I first need to prove enough theorems about it to
think it's worth setting up in a more sophisticated way.
Also, I need the experience working with more basic things anyway,
because I'm still working on learning how to use datatype, fun, primrec,
and function.
Thinking about equality can be a brainbuster, because it's so basic, and
you generally just use "=".
Other than the methods you mentioned, there's an easy way to associate a
function with HOL.eq, and that's with an axiom.
That's what I did with another type, where the type has to have axioms.
I can easily say `theorem bar [intro?]: "foo a b ==> a = b", because the
axiom says "(foo a b) <-> (a = b)". So "=" is still the function HOL.eq,
but the intro rule makes it easy to set up proving equality, which came
from a tip by Lars.
I thought using my new type in a local might be the thing to do, but I
don't understand locales that well. From what you told me, I sort of
left off here:
1) Variable 'a is special.
2) Instantiation sometimes works in the background to help you out, but
sometimes it doesn't, at which times you must know what you're doing.
I put me an assumes axiom in a local like this:
locale mTloc =
assumes mTeq_ax: "mTeq == HOL.eq"
begin
theorem mTeq_imp_HOL_eq [simp]:
"(mTeq x y) ==> (x = y)"
by (metis (full_types) mT.distinct(1) mTeq.simps(3) mTeq_ax)
end
Doing that confused the issue for me even more about how type variables
are used in locales. First, the locale complains with this warning:
"Additional type variable(s) in locale specification "mTloc": 'a∷type "
It then uses 'b variables in the theorem. My goal was to determine
whether what's proved in the locale is only true in the locale, where I
already know that some things proved in a local are not completely
localized:
locale P_by_sorry
begin
theorem P_is_true: "P" sorry
end
theorem "True & False"
by(rule, simp, rule P_by_sorry.P_is_true)
So I tried to prove this outside the locale:
theorem "(mTeq x y) ==> (x = y)"
(*variables:
x, y :: 'a mT
type variables:
'a :: type *)
oops
It can't use the locale theorem to prove the global theorem because the
locale theorem is using 'b variables, and the global theorem is using 'a
variables. I am left pondering the subject of type variables, though I
must move on.
Regards,
GB
Email Gateway (Aug 19 2022 at 12:49):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 11/7/2013 11:01 AM, Jasmin Blanchette wrote:
Once the next release is out, one of our first priorities will be to make sure "fun", the code generator, Quickcheck, Nitpick, etc., work with "datatype_new" just like they do with "datatype". We're currently waiting to avoid too much divergence between the release branch (from which the release candidates are generated) and the development branch (which will lead to the next-to-next Isabelle release).
Jasmin,
Alright, sounds good. Sledgehammer is my friend.
On 11/7/2013 3:14 PM, Dmitriy Traytel wrote:
In this case it is simply the case that the new datatypes are not yet
registered in the code generator. A simplecode_datatype mSp mSS
will make the "value" command work for now. There is some more useful
default code generator setup (see e.g.
$AFP/thys/Coinductive/Coinductive_List) that is as well on our agenda
(to make it happen automatically) as the interaction with fun (as
Jasmin mentioned).
Dmitriy,
Thanks. One error leads to another. That got me to the usual type of errors:
Wellsortedness error:
Type 'a∷type mS not of sort equal
No type arity mS :: equal
I might figure out how to fix that someday. On the other hand, my type
mT, which is based on lists rather than fsets, doesn't give me that
error, so it's just easier to go with the magic.
On 11/7/2013 3:32 PM, Gottfried Barrow wrote:
...I looked at [2] a little, but without knowing the advantages of
either, I'd pick [2] over [1].
That should have been [1] over [2].
I put me an assumes axiom in a local like this:
assumes mTeq_ax: "mTeq == HOL.eq"
I guess it should be obvious that I wouldn't want the axiom "mTeq x y
<-> x = y" anywhere, since I'll commonly have "mTeq x y = True" when I
have "HOL.eq x y = False". I suppose that's the difference between
starting with a new type where you make all the rules, and a type you
use which already has lots of rules with it.
Regards,
GB
Last updated: Apr 26 2024 at 04:17 UTC