[isabelle] Declaring equal for a type; BNF not working on the left



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


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








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.