*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Declaring equal for a type; BNF not working on the left*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Wed, 06 Nov 2013 22:48:49 -0600*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

Hi,

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"

---CONCERNING BNF ERRORS As to BNF, again I have this datatype: datatype_new 'a mS = mSp "'a * int" |mSS "'a mS fset"

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 = [].

mTp(x,y)#L.

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

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)])"

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

apply simp oops

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))))"

apply simp

oops

apply simp

oops theorem "mTeq

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 (******************************************************************************)

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 (******************************************************************************)

**Follow-Ups**:**Re: [isabelle] Declaring equal for a type; BNF not working on the left***From:*Andreas Lochbihler

**Re: [isabelle] Declaring equal for a type; BNF not working on the left***From:*Gottfried Barrow

- Previous by Date: Re: [isabelle] PDFs for HOL-BNF? Tutorials for transfer, lifting, and quotients?
- Next by Date: [isabelle] Additional type variable(s) in specification
- Previous by Thread: Re: [isabelle] Isabelle2013-1-RC1 available for testing
- Next by Thread: Re: [isabelle] Declaring equal for a type; BNF not working on the left
- Cl-isabelle-users November 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list