Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nitpick_Examples/Record_Nits.thy
author wenzelm
Fri, 05 Apr 2019 17:05:32 +0200
changeset 70067 9b34dbeb1103
parent 63167 0909deb8059b
child 74641 6f801e1073fa
permissions -rw-r--r--
auxiliary operation for common uses of 'compile_generated_files';
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset 
     1
 
(*  Title:      HOL/Nitpick_Examples/Record_Nits.thy
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset 
     2
 
    Author:     Jasmin Blanchette, TU Muenchen
45035
60d2c03d5c70 reintroduced Minipick as Nitpick example
blanchet
parents: 42959
diff changeset 
     3
 
    Copyright   2009-2011
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents:
diff changeset 
     4
 












de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




     5


Examples featuring Nitpick applied to records.













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




     6


*)













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




     7









63167






0909deb8059b
isabelle update_cartouches -c -t;



wenzelm


parents: 
58889

diff
changeset




     8


section \<open>Examples Featuring Nitpick Applied to Records\<close>








33197






de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




     9














de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    10


theory Record_Nits













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    11


imports Main













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    12


begin













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    13









55893






aed17a173d16
fixed handling of 'case_prod' and other 'case' functions for interpreted types



blanchet


parents: 
54680

diff
changeset




    14


nitpick_params [verbose, card = 1-6, max_potential = 0,








54680






93f6d33a754e
reverted 86e0b402994c, which was accidentally qfinish'ed and pushed



blanchet


parents: 
54633

diff
changeset




    15


                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]








34083






652719832159
make Nitpick tests more robust by specifying SAT solver, singlethreading (in Kodkod, not in Isabelle), and higher time limits



blanchet


parents: 
33197

diff
changeset




    16









33197






de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    17


record point2d =













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    18


  xc :: int













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    19


  yc :: int













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    20














de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    21


lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x, yc := y\<rparr>"













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    22


nitpick [expect = none]













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    23


sorry













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    24














de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    25


lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x\<rparr>"













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    26


nitpick [expect = genuine]













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    27


oops













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    28














de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    29


lemma "p\<lparr>xc := x, yc := y\<rparr> \<noteq> p"













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    30


nitpick [expect = genuine]













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    31


oops













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    32














de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    33


lemma "p\<lparr>xc := x, yc := y\<rparr> = p"













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    34


nitpick [expect = genuine]













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    35


oops













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    36














de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    37


record point3d = point2d +













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    38


  zc :: int













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    39














de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    40


lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x, yc := y, zc := z\<rparr>"













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    41


nitpick [expect = none]













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    42


sorry













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    43














de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    44


lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x\<rparr>"













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    45


nitpick [expect = genuine]













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    46


oops













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    47














de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    48


lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>zc := z\<rparr>"













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    49


nitpick [expect = genuine]













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    50


oops













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    51














de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    52


lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> \<noteq> p"













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    53


nitpick [expect = genuine]













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    54


oops













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    55














de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    56


lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> = p"













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    57


nitpick [expect = genuine]













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    58


oops













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    59














de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    60


record point4d = point3d +













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    61


  wc :: int













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    62














de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    63


lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr>"













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    64


nitpick [expect = none]













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    65


sorry













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    66














de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    67


lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x\<rparr>"













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    68


nitpick [expect = genuine]













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    69


oops













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    70














de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    71


lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>zc := z\<rparr>"













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    72


nitpick [expect = genuine]













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    73


oops













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    74














de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    75


lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>wc := w\<rparr>"













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    76


nitpick [expect = genuine]













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    77


oops













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    78














de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    79


lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> \<noteq> p"













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    80


nitpick [expect = genuine]













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    81


oops













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    82














de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    83


lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> = p"













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    84


nitpick [expect = genuine]













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    85


oops













de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    86














de6285ebcc05
continuation of Nitpick's integration into Isabelle;



blanchet


parents: 

diff
changeset




    87


end















isabelle