types - Isabelle: generic datatypes and equivalence -

-

i'm starting making type generic in isabelle funny error messages once start using parenthesis.

theory scratch imports main begin no_notation plus (infixl "+" 65)  datatype typea = aa datatype typeb = bb datatype ('a, 'b) generictype = cc |                                  plus 'a 'b (infixr "+" 35)  lemma test1 : "x + y ≡ x + y" auto lemma test2 : "x + y + z ≡ x + y + z" auto lemma test3 : "x + (y + z) ≡ x + y + z" auto lemma test4 : "(x + y) + z ≡ x + y + z" lemma test5 : "(aa + aa) + aa ≡ aa + aa + aa" lemma test6 : "(cc + cc) + cc ≡ cc + cc + cc" lemma test7 : "(cc + aa) + cc ≡ cc + aa + cc" lemma test8 : "(aa + cc) + cc ≡ cc + aa + cc"

everything fine test1-3, test 4 , 5 result in error: 

type unification failed: occurs check!  type error in application: incompatible operand type  operator:  op ≡ ((x + y) + z) :: ((??'a, ??'b) generictype, ??'c) generictype ⇒ prop operand:   x + y + z :: (??'a, (??'b, ??'c) generictype) generictype

and respectivly:

type unification failed: clash of types "typea" , "(_, _) generictype"  type error in application: incompatible operand type  operator:  op ≡ ((aa + aa) + aa) :: ((typea, typea) generictype, typea) generictype ⇒ prop operand:   aa + aa + aa :: (typea, (typea, typea) generictype) generictype

test6 , weirdly test7/8 fine again. more replacement of "cc" "aa" leads same problem though.

ps: can somehow specifiy types 'a , 'b?

two types in isabelle equal when syntactically equal. equation left-hand side , right-hand side have different types not well-typed , lead error message.

you defined + right-associative, x + y + z abbreviation x + (y + z). lemmas test1 test3 therefore trivially true, since 2 sides of equation syntactically equal terms.

in test4 , test5, left-hand sides have type ((_,_) generictype, _) generictype. right-hand sides, on other hand, have type (_, (_,_) generictype) generictype.

to illustrate bit better, write + generictype in infix: left-hand sides have type (_ + _) + _; right-hand sides have _ + (_ + _). these 2 types not syntactically equal , therefore different types. isomorphic, still different.

the fact test6 test8 type-correct has polymorphism: cc polymorphic schematic type variables 'a , 'b can instantiated anything, and, importantly, if cc occurs in term several times, type variables can instantiated different types in every occurrence. not possible variables x, y, , z earlier examples.

note, however, while test6 test8 can type-checked, quite false, quickcheck tell you.

as specifying type variables: can annotate terms types, e.g. x + y :: (typea, typeb) generictype or (x :: typea) + (y :: typeb).


Comments

Post a Comment

Popular posts from this blog

ruby - Trying to change last to "x"s to 23 -

-
i have been playing around irb , have string looks this: irb(main):072:0> puts ["[\"4354 5432 5432 xxxxx\", \"6547 6547 8543 xxxxx\", \"2344 6543 6674 xxxxx\", \"2346 6236 7543 xxxxx\", \"1273 5585 5587 xxxxx\"]"] => nil irb(main):073:0> what want gsub last 2 "x" s of each 17 digit combination, 23 . what i've tried far (i've been using rubular): a.gsub(/\d[x]/,"23") <= grabs "x" s i'm close a.gsub(/\w[x{2}]/,"23") <= grabs "x" s grabs two digits each combination. is there easier way i'm not understanding? a.gsub(/\d{4} \d{4} \d{4} xxx\kxx/, '23') \d{4} = 4 digits what \k drop matched far. can use don't replace entire number, still able validate have in desired format.
Read more

jquery - Clone last and append item to closest class -

-
this bare-bones code on page: <div class="list-container"> <div class="single-list-item"> <button>remove</button> </div> <div class="single-list-item"> <button>remove</button> </div> <div class="single-list-item"> <button>remove</button> </div> </div> <p><button class="add-list-item">add</button></p> <div class="list-container"> <div class="single-list-item"> <button>remove</button> </div> <div class="single-list-item"> <button>remove</button> </div> <div class="single-list-item"> <button>remove</button> </div> </div> <p><button class="add-list-item">add</button></p> <di...
Read more

css - Can I use the :after pseudo-element on an input field? -

-
i trying use :after css pseudo-element on input field, not work. if use span , works ok. <style type="text/css"> .mystyle:after {content:url(smiley.gif);} .mystyle {color:red;} </style> this works (puts smiley after "buu!" , before "some more") <span class="mystyle">buuu!</span>a more this not work - colors somevalue in red, there no smiley. <input class="mystyle" type="text" value="somevalue"> what doing wrong? should use pseudo-selector? note: cannot add span around input , because being generated third-party control. :after , :before not supported in internet explorer 7 , under, on elements. it's not meant used on replaced elements such form elements (inputs) , image elements . in other words it's impossible pure css. however if using jquery can use $(".mystyle").after("add smiley here"); api docs on .after to ...
Read more