From 927f0446a0f5b551265f763180a21af9a0ea57b3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Thu, 3 Feb 2022 11:04:39 +0100 Subject: [PATCH] Update invariants section --- examples/scholarly_paper/2021-ITP-PMTI/ROOT | 2 + .../term-context-failed-checking-example.png | Bin 0 -> 8606 bytes ...term-context-failed-evaluation-example.png | Bin 0 -> 9292 bytes .../document/lstisadof-manual.sty | 298 ++++++++++++++++++ .../scholarly_paper/2021-ITP-PMTI/paper.thy | 188 ++++++----- 5 files changed, 415 insertions(+), 73 deletions(-) create mode 100644 examples/scholarly_paper/2021-ITP-PMTI/document/figures/term-context-failed-checking-example.png create mode 100644 examples/scholarly_paper/2021-ITP-PMTI/document/figures/term-context-failed-evaluation-example.png create mode 100755 examples/scholarly_paper/2021-ITP-PMTI/document/lstisadof-manual.sty diff --git a/examples/scholarly_paper/2021-ITP-PMTI/ROOT b/examples/scholarly_paper/2021-ITP-PMTI/ROOT index e577066b..3155be07 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/ROOT +++ b/examples/scholarly_paper/2021-ITP-PMTI/ROOT @@ -18,6 +18,8 @@ session "2021-ITP-PMTI" = "Isabelle_DOF" + "figures/invariant-checking-violated-example.png" "figures/inherited-invariant-checking-violated-example.png" "figures/term-context-checking-example.png" + "figures/term-context-failed-checking-example.png" "figures/term-context-evaluation-example.png" + "figures/term-context-failed-evaluation-example.png" "figures/term-context-equality-evaluation-example.png" "lstisadof.sty" diff --git a/examples/scholarly_paper/2021-ITP-PMTI/document/figures/term-context-failed-checking-example.png b/examples/scholarly_paper/2021-ITP-PMTI/document/figures/term-context-failed-checking-example.png new file mode 100644 index 0000000000000000000000000000000000000000..76a25bc72b47a3750229a34d3bdb4d759a93f9ef GIT binary patch literal 8606 zcmV;PAz|K$P)`%oSlEW_nqwvDTVa9-Km^_o0jyGWLE*LY$G=)V&&GEoX2krx#Y%;5?;Z^PcCJ&9 zKY6Ub^%sk0Mm)&kH4>;VeLp2Xc5PA3pMPE-5O&V?hbIr(RF|0FPxpvYM!8M-Ys-xB zyH!fmzuMN)oW8C2XZ|$S)`8x4+`JRX9L=SF0+h<`%1YREB=Sb7ZZCUUQ`;&^O3Czb z8<%gqx@Ysg0IQ_aYX@$zO*Sfq@Ykg;x+bmRV_+c+hj2^a38BAlG$MB9)YZ}3G}8vHKFn)Gz%lf~ z)7albD0hB1bd%qefKi^i>ia}q8gHzJ&p*G!_KiZs#6)#8Ji0fjY-0FGo}?$9q_xZ~b?#gzzR-Yns#R-o*zScE)oV7;~0q5kil0CU~Z+VCrjWWBp z#b#TgL`89R@bCFCi2lwIgsac1AG5?XQ?qk+HKP(Rp*=)@y%7xdFmcN(`<03RVu<}g z8`8{f0oB9SP`tj%5BEx$E%t8qnMsyr32QDyChmB_U{Q>x2M^sum*$FUuU&hx z^I2&Q2WxF-zdX3_RCBrfq^mK0`ED2cR&TzUlgva+9DAReM|Y8OQlG>E9tJP9SDM7- zSBftmV7$!`V2pGef-EL)q)H#Vh%l=va(D5I*CL9iQSebqy2Ka2AhwY5XZK0NBm}I8 ztj#}DmOn7JlKf&{9h{N>wR7L}qMI>nCW3cd4>J7-}@o+?<@~Ba{UMK#gwOJyOkjG)9J^ka` zs7&L*0h0`sj8|VOC)K4a>~6f$o+Z%AsFIe6ewaJ=O>Hre>}N&NsbTJj z&D&I=I4Z3Ti)ZBOkbNw42pj=R!j5&J5MzPiUwK{}g(2wkIEPbeDiN#^8E;0yibZ1J zYC;^&goHO#dM=4d?rfN|=c!De{1@quoqH{@!}BZiHvV$4&kr#(U-BL5m^lKuzFdJ2 z!78~cvsU2T&->Kkz(*@buQV=Ob>hVn)w@Ok76bQ~oip<`4H$}07A={X2d;OHnIZF4 z@T^Emi?i{HTpRODZpy5Tu_(Ja6C z|M+a~MNxj@D#&fT6!FtG#8=Y5P zv*}h|cHsa^ja?1=OOF*kH#eJgo&KM{ta{l>JWEUd{73V%W6Sh|qTE(pvGEp_hcB$G zspno3k$2`Cx4tbD&BNmf2$#oI%mUZN5la@HQ(RS1Deu%jHE3%k`;wPUT5`AwWD&ag ztbOpkuca2H^`v_G8@=_x-1X;N4xdWh>TM|R(QB)=XA2Oj@y$RBZ!E&fFR;7I*q6fG zJd9f3Gh#-1J707o0zc<)1UcDt2!an8;5arTHQ+6I&1mbIJLzlc`1wLs_~S}}ljU8D za?dQvEpOZ(FN@X@9S-%8DZooVyJXgntOXIWzEhZxUD2?I7^Zu-Kb@Z+YU#`%tf5yqgn>jn{XWYA-`qd(LY9pvtpH0x6IeA7=_{kN0CHy|A zq^-NUtloQkc3t(`*SB{>>!i-LRX$!!K8Qc^=Qd80YbVVa+H8&SQoaDcC zXE;lI6(kY~FLiPZ8HZ3L9)JaZ`M|A(Vh)b-KYvG1#>glKe=W@n_xni30MgzV$v8Rl z^Kh%}(MKlO%53Kr*Wheu1f=HejZ&MHOYD1Nk=_$}UVf4Zh_hm^kGfVaq*!bVbup4w zmn9*i=+KQ<7qe>$S$w`&%teSEst(kj%{n)L*LQEh*$anE5u|%6ice1BC$wr#Ka{nXK11G;U;rGj@>Q6S_1! z!Vm$mExN1u06k@WwBwIYVKW7FQC_d2okk!W71n!S9+8Qz^h<)nXy1rms{s|>*-IZ+T;s#Lc z@6msZ0mFXRzTN&q_w{VRLw#uruz`6nxHk}8@)R?LsRx;;FzLkVwx}-{|JKW)x!Q|d zRfSURx*69cr{*&!*fxyg@se@5P|U~SNV2Ci4o{NyWVQo`-*GNK6&b(d*1O4H*w@eN zYmP?TJ4xxeV|qV26_4lTF4>nV6RI@BQqV+I35DM{oKkNKrpX|IKd7@cc|8(AHqBJS zwxI}X)D6!|=2S5a43+0C2-}b6mro_ad@I* z+Q^At%qc0unmXf^*B^wB4{wUWPd*s4pq~p^_h?M);*5+kij%Xk>UxEW-ktBK)^pbe z6V2S+?U9P)tcFR3lJV+GC8RhE3H%j_8y2APG!h-;U`PuG+ngOP`S-^lvu|DXlv?7w z5jG#QJtlnY!$pCsZ6q#93K#-}W;%%UF8px~8%*@>r`?jiA0Uu)U2N@^^)sz` zSN^s^G_U+&K53GVho1w@(MZptt`2krvP2~l>Ui~U78oq04Jde=4k8u`8@M!ofz@}Q ziBbydfvshv*5VzEl?Q^&*H$SZ(6>9!8e98EV1BC1UP(F0!W}7iRIBkj5GkuQ zV9-*a`p%$UNpI1 zH#@_|PL%y(-;|kWY_`W7pH@FkXrf=I&1k*57Qar-K}c36=)*Ggr4qQP#BSjETUtKj zVezV`#b>~Lm`3}~8i%l|K8t?qdoOSNjkgZxGiJ5Jq5-wzpytW07Lg@GbP2agCujiX(nz7v&wCn4u`6)Q74^SjGA^~*F!cUu!t zX72S`F(RlvAD5%#t^_>?D*Hi7X&GN6kgPSUNk%gVnxsE?a_CKUURmkM=vNO7T)vQi z)yjmkU*;6L6kFc#R6z*+Rv6);3(g#=Da_@Uzhd6sQjxEYImy;joO!9HR)h%hs^b1e zTlZ0_t|kBeW@84iZ_O`y{)AhV&&|72c{Q}8;pteLA?_aT95j~D1OTwMk5F_eDvDQR z)cJ--ZyRgg`deEa6d$)tWpG)O^yqm82dR8p4PL4wKaRa%fKcqb{G7l%D)GC}Q`Lh< zjdroIBysan@9jDB7;&DxOtLBglKN6K8+8qL^TQ9eMcM|vJTCR8Obzyz?8V;gQMi>mf ze3mR32VfAfSYe6ObmbSG1<}uf_V9I$E#{2xIrzkD880)hzMC`eui1Tmoq^%R;g0>1 zauw7wT{wxJdO2=j9G5Lpc#(rzDX2*xT{<+%hPw3)hoDLVZpkc$z=#VMGPvV8Kw zpCk)3jmdu6(VRuy!2)^I&p#i0lA2On#o*yh%x(J*o3trpTyK5ZLr;Ava(qM@;3zwh z(*d{m7be9AMl*fK_g&y&YO90P)$wt<#K!Se#$$RoW9fHe7Mr#>b^ZiyiB4hyzvSG! z;j0O|vwoSVzEwV@E&eL*+Fnhi=&qNXoq?DM5fR|;<=L}8*tOadIg(9?JFdUElFQ=Z zFd~9o`1+x~4gI>X^3d_Sd$Ku*0sXK4ddpWJ+Y2hlw`Byfjs%R_{!FCbbJ2;v*A7CT zjx}(B?%Fb-Dilq7*AMBaGFhXNl3LVT$mdnCMYw9yD3_2ea+2y`_B z)X&n}1r5xQA??DqC8qV899p7-5T zyXKpqp&s2_U4z35lsM;I*}5nsVAQ}qJ$rf$88>akk-P6uH_8e#4^4D;b)~Po^*)Nh zx)1?~fGPsYgJEX;@f{J_E*|dA#wD**Ng0JjIvznwXE|FL;wxVLeds{w=PCQI9h#uH z_Z`&9KNEH$k3>Wy`+s4A2tWkd5CLU(r3M^Mm_noCi%(4-_DZ$u^q6;ee}m)!Lu|`m zOb$PHvueV0#jWGzF`NHaGJVnb^Sdv!p_Ur5!l>I9uOSae1`+5G2#C=(sw%rHPLHPP z5kZWeK6pJX1Shu@67%-XU9U%PJ>c>0`Hy6>SS$}y@sZ?1u@HeaKmdc01o3E^w0@Bz z5(@e3%B=gxw?w4TMo;xMY2?XCII#7W+saj=Rd-!C6$^790uTZ15zzKU&eJVJXPlO7 zDkeGx?D}h0aO1vlVd{~vbA}6ICV{Lh?G=GFAOaA9mJrakckMp!WK`tYU-z#bPrSP! zH0*YL;8Jn+$*^D9)7Q^+X>!h~B^6*fL;xb783Nk&uDVwAUf@NohxhP7hLt1MZv5qQ zpLJdcQt|h;gP9{Y|Ku*Hs{^MYIg%5RLT+6hn?NEHw0$IKra7d72y{6Fv~|};fQ&sn ztdO`j=?uh+h7@LI)-elK4Zpdnk>JXT-dC*WM#X;L>ytor&z|2OC!JDKBr|pB zv7dA!cNF7P+_gF__F)bOVWfgsEd2Di>(`ACvg4o;ZXlG`lbw?fGDrCjaR9=FVR;3ssm0egFLPCdh;yt1*g@u$2g?+^N|Y)-V07{>^1{*isNm(t7Us z*zZ9cT5GTVMiDoT-8oTF!zCD6Irg5h`^N=A^md8O(n@30RAaGt`T2~>%32U63HYi| zBxcodi;5YgBhHGPe~HWgW`s?{irUeml6TDa?I1*6~G+;^Z~ zb$9Cq+UR9+O6r>o4u{KOa|#NZ{i-inSBId}=#W?}7J~&R2{0ftuZFwhO7`xl5^gX- z1U>))UBX=@YfD0~yd+7I&(cW~$f%S0Du^zP#WlMZ3xmVr2udh{Whx=~M2A@HYC&21 z8G4`m0a^}<=z<7z33t`i)v2xH0#~)Mvg+>c_A>dkKq&O`^kB0&3C|O`Jf5A6V$5u% z+u-s-`6qzV(Qg0~Me`NJZh?5+Yv#p#!&@i~=G zO1Nxum)O~M3NKUHSMFy1@vinQgIkLsSeej*1~|=iCf5hg7Dh$Jtx?+APo6(((5epc z!Er-F-QtpJb92)k-6g)7l9n#*SGj`+^{ZmkB)&{`bZA-6n3!15G+-&1%jS)t8?N-R z1uMfJwy~hJu8x4RyE1cfcRa6ivCwy>aGOMv;1@En9^D;g8IugLyjQPt4n#do2^e@t z@y)A+{cmGT>tA7F&0GBR=m$dI+>BaQR-Koh4<@b|Z*$me@DX3`<7Y3bY9zku>SWae ze4R_W7P{^CmWaNM(QnxxDac zcw%W4-MTTFgbul<6;;y%?rmm6i;Td&B_}5{E??%W9G;|S1v6HDQqn8nt3w9&)YH@A z`)-RzgD+;n1QGZM2q?QNj!4kh+3@;cUjbNe{Rm38LZl&$(xYhgI4N0j-ys#9(0*e1GD3a(YB5VYI)QLNo~kDa!inr#BS> zoQ0Xuq`@vroJmbSUC~y0w}KDYx75Sk2K;M9U04Mo&=C;O)?M>6hMvurM3cbj2Ke>e zrSKV4V@u0#T}?cV2%_4W8&7f$MLjQ^)PI+=wgNf=D5yH9Z0<*;fte72c11v2Z!)tx zIm@D!&3=)Zd-&$dFp}4H7ujB0+=#*MBjl>mhC5LN;YraC3YR%6t}VB#C6GBp;FCu{ z+dacX65WF8?PxyF-*dek=lspw=co`7jmFwz#U)JnXNpm2U?xNWBA^`t+PZ5acOuv* zfUsEU&4mA!>>Yw}f3<52NDUECk3j3)m6uq=K?p>%#*d6ENa9!C%M)QO^yNE()aw9C zAp#HqjSx_oyK-t{bL%*WAQkkPqT0AOrA7$O(cajNgdp!SCqEF3ax-){B$5T(q_o^) z*$91*?J$|cm*jl)FK>t&&DDT_)Yaa3nsb3g4)M3L)JO?P1QCD;Xo7%>yH*yhzxb{` znnZEf#bN{@%?%m+JqUhCHRw;yzwxB}1WUlh5v&ZUGyHoj=%FV+tfH&yC@wqmZ*c`j z$j1@vElk%=bNbS@BfZDb1Puk6f8Zzcv_uS&YlA?Yx3@Ora#~DAMn)^DXs?S~ zzIeX26}6%VbLBSs=mvCGt)Pd*S|Xs{T`3d_>Nj#)KX=tqy)Huj;0vFH2kK*`H)FFf zIc7tTKtDa-8EYC>&I@-hn!G%*nHrjAYa(4!Uf_r!nx2|h?@*MP-_Mx*T}s=k)E+!r z&`{g=t}U>G#VsQsdc5;U>Fkr2*H|ge6|7btiEO# zr`R z!>Ol3^?ZGGM)@yz)}Rc!AT*u`s`O^8dh^}XsY@?KO_>v<@9Xcd?H&jxjm8sQPc%v( zM?;?I79j}h`NcgWW=*2`1-LBP7bTrXG$RN>N-hV_n)U4?Q8U&xWTWr|WtA^f8V&)>LFd*kdb>4`-5FOJpT zII+P=Q3|+jA_$cyx^xv*ia!~@U&;#Ec9wDFTy(Gl5tS#po~RbdIBUWa)gq)KcF)*| z>e*qxm0kYp)|YMs$(JCS7bK|8&dV!c$;0d^G(oD4-n!rIJ`iKPu`WSi$VfM4eZmir`M2i(^ee0`%dKp>+H7|cP$JW z(YI&!Uf#nd%=zDgW_CPju3iVEB>D#icGJNcdJP(eyi2b{ki3VN%LgqEwAaN`hffa} zEK|Ag&WYDv{|)VLO~C3qPFmV8E$R_dOJkY{Lgk4nU7aNUh|d=VS(9;iYM<_o6jYw5 z)zwjI$g_z>2q)%hEPd*-xi0zy9NDqo_yBNRN{t}vki@vS3uDy3A4KCRv8btZR6Avv z$`+yOiON%r@@k}MT%^3z#Ed__BO=?y!`<1qq)9XhMq!bTN6^w)&Q^x_idTOhIuQDK z%KmGICK$mH zCVTGD49#U1rKRr#59b8>ek}(_)XfHTulm}6(L_)s8c$T|>ckki+9-UoKyy9SQEI{y z=+wj_r1V`W*3r^TNndq>)EQP^hQ?D;)>OJ0Zps#+>WRt|wT-lEcQsle%I-=HIGiwr zM#UGOnm+86O4o^a%saflfz^N^w&gD-ho8GyHDS6mnndmOeS038E{Oc?KRsnfbOw)6 zC%5C55lK2ihV1aYm{p@@oM32ZUY%bG=2O5?8C4~+iItg|t-jxnm%ba-hK8c@%te!~ zPACqq*g2u{M6IrlQWKt;Xk5)~&4jm#!Gu*Iw4FLZXgpN&(0HoS$bPG7Vr7dEjd{MW z^5}{-2k0!y3yL!9MYsPH3uWH7lLsOZ#+OQK+ih%c( z|8wWId`60M70RfxQS8qMCGYQ zc~p8WGqql70ug)p?8>bB$G1eJ(MC`8l}D4vN=xIJ(oJ6P|7M(bcY1ekpIIBC-l*x4 zv{dsWkdr3Oo@;n{dG94Fm*m)tR1*^i>+;{Quc?=oTLpZzp6Kl_-<4^;c+)1|+@r&% zOwgY=JMdIOL9@$0BF3Xu z-3X!l8aCU+FR0&v`_lcd%?r|OsR@lIs!19*F@mZmD$nMXM87QqE5|51MgWvdBqv4A^pP*Ca>z-T7#P_pEDV3!>?mWy?OZQ)UsV5`6rG*>oy^3IP`76uKT=`QNguUc`q*ie0W1>81>9{AL+CM#N0-z zE9`!V+%#RXa4>LyY4NkEzn!?cdf+6j)>l69MuO%+1l|V$ZQWJZirxzx&++gcKFF|g z#M+I&eD1T(3n-wk54_T1;K2GtKAcDIo>*aeb{>K>Mmv2UMPXft07O9RxoZPt#vUG4 zNZFfohBU{{PBr+h7`)7e;UwT41`%jO1hnm48%38TCKVuLPcuDfmchV*bmY*ZN2N<0 zr5&sggxnV4dpK(m9luSiVluS|@U2E7u2sho)i8ub5CKI5gu-Um9@PM);;z+cu@7@N z2qP72CgrEcUB7OGkR1n&a5F%VCp#w}WRCJ5_j02^k~nx#wfQ_e79_ zo4a;L#3yAIRMc<@hE|TfeZE+>Ac$_z_^}vPTI8M`zg&NjSB=n|2Lvqs?@B+gDOH+2 z*vfECO>=KSw1Ne};neSR(~cXYh6t!2puTsdQmLrN)6rk#v^luYUE3T|$goo*&^mW* z{Zdn>1`8?=5$KEvKzHqotp;`Oq6k2D?V=42&F+i{KzHqotp;`Oq6k2D?V=42&F+i{ zD8F|F(Iig)c{M)%{*#mvb`O;;{vevf&OaWfzRfSI#TZz*_74jE&)m_r@^5Z5Z2eaP zVbJEs5i{k-*E=IRP-lohheANvU0WYb!u^}@^Ai;gg%(AvUUp7@)QAu5tKfxIhr$;s z0}*IL1eD#i_0c3K);&BG4%_8E*pQ9u9~Pi`{;mx*M`4BfW*LRF>ob}F00Bx#L_t&z zW>G-!hS?0V;f25Jov=x7LNz0}l9Gzmq!L{Be7=aNPS z`O!L>wNM|3K&M7P+Y>oYw+wBFCb8?UUBL<=vFdRUJdC_lr028V2X620)VBsyzT+XF zZSN|HCJ}k|*Zr%<6Yqj(61SUvy@`GI!nG;`zu-~Qs4p-<1Rw%!hJd!cYje>g8Wdt) zkG#z?ofJGo9>l55G=+>H0$m;fZF|>7z?7p&)aRF9iHze|2L^k?^JiWD-hu$MIRdSB zS6MU(b9pogxncz|kxzt^-CL~NkoS&jYg3AXcE?5{f#1S9J_O(KAOag-9Lh85(-mPaq@-ebWESM k6CK)9W5^pK&}9+$KVAH71L_k0<^TWy07*qoM6N<$f~qC18UO$Q literal 0 HcmV?d00001 diff --git a/examples/scholarly_paper/2021-ITP-PMTI/document/figures/term-context-failed-evaluation-example.png b/examples/scholarly_paper/2021-ITP-PMTI/document/figures/term-context-failed-evaluation-example.png new file mode 100644 index 0000000000000000000000000000000000000000..3f59fbb3b36151073ea343d5ad55cc57578129d6 GIT binary patch literal 9292 zcmV-SB(vLzP)w3IB^f^0C6j*wOTj&)|YBsEpF=g z9Mxj0D3n+0mV)3O;8v=FD4-yF&p;r1d?yKk8@LHK7;xS5%MX$>{?Bv%=RWt0d(U$; zva+(EP7Ze*?*IvlMT+ApXvv8sF>3=q1wnxcmf zyI7)fagDutDbIkVVhnTv13Ef7=%o-GN=ne@?pRLoj1~(R0~iBpVgNQg=9gSOfAqVx zi!6MHYYbbww@gmL`#Xmw|7W3Hz<8}Ot&Niw+BVqm7v)B5Ep0V8e z?2#JaS|DQoce2MN`Kv*#_^N`@|7Vtd>AtF^(C1ede)hpJmNqVZ$1XaN#zrq4O-`86 zHYV>1zj(cZ;%-fATe7;mLd#|BFF*WpWzUv1 zzkdDqTod#{Mddk}YmZ;)zwLaVz1NrBDX$X2%I0Kle!(9XI6gU~k2iYARykSOGuFoJ z_z3KDSmRH(pzV?i|0ez~Nc;BI!#C8_g*8N zDSG+9KbA3iv`6?vDw$Cc8JGAiZe09usuX}#$E?#b8tY6oMT>{!>s$u#WIYobZ@;0o zd+(OjK#&SI=l1l1^|Ux`V6pAxm!@k_DHI42@P*Q!1?hQ0TF;(hixmf)XWu^hg4Ek7 z{I+P^!eYJXH>BHih9pf`Qepsp-m0yIpn{@`!0XvoXEQWUW|+j}F34ml9St*Ao&&?? z+{5AyU2yn1_@22^I*8-5BcJBGofG3&#uscX*v;c{I*k(D@VG!c+ULe zjrfLAetXZNfMI=HY_09xhs^ltYzDIl92Aj`gXMp#3{@Y12@O|yAznce3g8B;=ul3z@#wG0L=1f_vu;FULonc$gSZ_Et z=#Qu8%3GQ{^-8SS(ae9JKlKYcYqR03*Rjm(_Ub217xCqK3sF@{IpbIa zM^Z*5e85rTgCE}i>iT-4Tjrsqm3h@IbrNs^{fL1`Btk+#lc6-{;BmRFqYz6YN2>P7 zM<^6<+4RhR|NhUVY{Nl*Q<}OC9xw|c9(KVHi6n@hU0l&tCdo{9EFR*QHzY}veqPo{ zhaewIU4ZnisODU)(1b=AZ>FiqWJWzJ+>8Lw7P3{0Am(xY!nX}&B&~5~WX*a;SYp9u zvAN+4vd1yT*MtA;?4NNkN<52XRI%)5ZH|h6@Z`?_LadY5%-QiwdKr6f zdfy5Q6q4nijd5eP(x z!I(XR``BfnmE)5i9wxFf0niBjw=o2BL)9Ce&*7nC5ypCUYjf+K%cdDR?#=P65;LfV$XCYR@&Dkp3i((_uDD%~Ow-om6 zG7e;{i2$M`s-bpgE+3*A-taf|!aN2szhhd}J4gGb7yj>8 zr5i{#hxbxnoM1J->Ted=gZ7Szubuq7P`lOU*d+bOAse3BqJ zx7xdh1r4e{eDZO!&44IBoxCScR&mMWCD*Hn$B56UCKy@Sz=}C|^_A(P9pLK}{WLSF z9O@@)v$mq~I2@!QzL+(D@yp-Lc^1x_`x_fVkj+p#m#2lP_0RxX&B@1APCov@&SHMP zo7^*D`}4ovdiHje4fk2Jg+U(UBsVIHZlI|0z~v+d=iF#CTF}ft#7o{^!=G#u6ifxo z0Tzu~l0+8s&H8(TD}^+48u{rpW<8{hunr?Hk>%1YD1<7}N3WZBQluh&a^=k@I^)xf zUBvYz4%}(<(xc{Ofx$2<3F0?2QeaL*sr9$3DY84ARJ^ghy>8as_>AwCyHZ<7HTz~F zC2;EO(ul~_eZ_dH1(l4}VeQ_d^O$w--`om|-s`_#CvmNh#7fQPPVBwy!0F}xxcoNC zil3dZ=vWUsI8cM>*wspI71jeZ+%3sUG=Rp4)TWBvW3#p49&x@}fu;Is&{oiX7P zEoFpMr)N~~pRe_FkX`s-;HK+Z0D&tGx4Z1C-K^dt5pJR(;Z73 z3?#XwK|n7(eEoG?Zhc83k0%mwAd*K%ZyHoX-6pf6kZ2IM4h)c~jC?xI#Z-31>Cjwt z_-WN3K{lQ+G479gXu)|D`2K;J`SNf**x-jKJ$|2>zF28M0^O}y#RtFMvJr1n-Pn@5|kItvRSo(0$VmEjak2E z;-rgsS6_)$KRcsmf!*>(*|6ZtvybNV%sXOR#!-LYs0zKwK5#(yA z>i{4a)w2^TlSL4XO8Lf=fNx;N)$j#iC@TrlySIW_14wU~P=I;1c*;f5nr=*Lxo2pR znkTO`M{A*@6t(3q)ym0`nU+z+m}m)KEHa*TBre#kB^yr12+FwHy0ApP2zq~H;k-zL zRbjtvburN)G{yywIx0jnY(s!Uj3SW1r63UT@OZMcVt4{s!i(jAp||a;qAorNyIDAO zjyOG*G!)AHAPzeNXe(=5wsXB5iUtq3)C`~>RkC(guO6dm8A?cVE1Tqo1 z`H`~Y44equG;zN+JK~S7A ze5j&n)Plq-W0zOrjO+>W>m-7wzi*BuOg$94)Z4)tUJq7TR#v69oxNe}b(PkYZTlOs zGi;l!b&RpAt2I=emLnU~#SJT^q<`)Xvz5F^`w~ue}Mz^^#!d>S|Q=t_W`l z3+DP_RgnYp`QulHQ$j+EuW2n6Evk?!8{5!}TR;D3ql{|!I<92hDs~N?sBhWwp~$WW-pleo18ej_ zEoQ>{3bDxY)RZ!Z$;+pDJ6Y+sbf~PC`=$q;ve+4Wbf#>~&_+MS5gjzzvNsud5ZSDo z+<=2bHSJ+%ZBF4PUQ9?c7(PSc(-h()OEM&Eh|1wZT4DnRK|_z+6WsOqy!T8Yy^bFC zUY>IUEpMP{WySCtg|qJ!tuFvmev-RBh~gZ3R`&D5(un4PD2?``IUZ`P{U+wU@7;n4 z*WcTm&zg&3%1`aP>deKJq@3n!yWi5)15@`d-g5C-c2QB*i`yr+FFB~>6-Sw;yJ?G~9@H+;DMjHmL_}=%}qpfcU}|>nG{jQCYW>^WM}pX6I)A7@sH82XeFQ zCd|&i)*yoT4d;{cUstSkGaO z6LQC;1f@9%Z@tQH$x2*R%e{{1z1jdDQ+z7Cz9gSl^_uZ;TXm5#B(i01QTFBf1|h^R zs7?9@X;nzBxQh7wj7JS*-CSJy;u)v5h*NO8=E{=t=6hsAmdGu_K41*74FTfk5!w{V z{0|nYvzWdSF+0YXbjbeT!{hqYCoi(tP|bU=vd&L?ns`AE(zfy(X9wmjDL*cWsv9(7 zq=Q9wGN&Np?w(UmA^Ul&#A^YPPe0p*v8DKsEep5I6W${gQv)8R}8|x@kfMu>MDjc5nc5@he73S$!4+^`aStSrMl7 zF^y+bTrQ`_S{lwVVud%o>OovE%$D%7e1AUkUJ-{xBG?$|&Fqfq-3*f5jO|NWn6;dL z^qgR8*uI5-6)_0<=FWXbE)IeqSYHoo1n|`>M3?Z=5JaxXim5!LwRIi z-)%3N@~-F^559S9cyuk;MiNE#UB7>NaOkXoVGN$n-pq4>3YH}-J)OO8r|iw|zRA}8 z!X~$RHl(Ws(dj&rtY&yHR27L}V_l<=IlYTxo(JsVQ4CGzPv|-5#2cv+#-4q*WIz0A z_xTNa`jdv*dZ*?$DJTACv}}q?MtstMBo0exx_8UyK*fEh-4LH6jHkQKT;0Rb=x$-P zXMS%l#VrmKq42AQ(F`;A;Ed#BzT`+*{DI;lyZDek$;z*L4~1nx0?~7`S$1&o?w-YZ zJ!wOyQc~lT5o4SJ4$5AVcR9dG%6oo~qi2+{unMFg_5_jhuo20x| zRN62AH(E6*+6D%0w3qGeLHfk#Xz(|F-n@_g{j=KTBYurB?AqIe{6;QbLrAoW*yQ8e zJcba|96owyPc9qMb2+!st7(<8OFK#sJ2ElmX?_WA(G7F?g{0 zK|cUd1%Ck_AO$OmF`z~U2-#+4YJ^h&C0;$o0>%KwfLa)U^|X9?^~qNi5AtfBm2+4o z4vF)u%#lP0s&l7A<)({F!+&%e(~?1$laamUQTfX{p*D>+X|U6OowbnO8bw0H;xGm< z22@}GHm7Ce<%hkfE+y&Mw|;*Ej>kH6v#_AmCJ?ZxJooLq_)@y1{o!dnSDCR-#=YE; zkLG1K6*R@NVhmsmNEm?iv{X0uWDg=0$BFv;;cEpifmNly`>nxzxl76JG&q6m^N-8Q zjclXGn%RM9OU<&9XMa8}3$`{_@b)oAKE?pXK!+KC^|W{ruvn!)oT^_F86!v7c(i&x z$gR0wBC>NZ5?d??8aksL$bzDp$Ee@+Rw@-s#2COBfHR=N>aj5S!MmGA_P6ZuIl1yA z)-rQNkh4B`O;yC=3N=Z18+{5SV&>ApyR4l=w}!G^VVxusgT)x=6b8gQJ5>p&jaE>R z7n(|3`fYb$hB>Vyu=({6PDc}0`8s9v)q0-^0}qS$ukz~K-EpRhrfu?yL`}|t+N59+ z7z3XT0~#78s_LqIJlulDjJ#RE>gBXhsoxMhk*Gr==#iwoV4Gb^s_KU2#~8pEKwtn} zPh0&a>rl1f7JnT+R{)l%B-=qn9Ik+c$7$g;ATmK0Y>(v#4SMu==qwh}kOr2H2~-um zXdtMEMPUqJ476qdoza$5H!?ZwHGd?nX(?a6`e3=aw|C-jT}Yo|rvc^G0zWTJ4~z0@ znUIFAZM%MZT5E&-#u&gDXqN$WMr+^O{j^=nbJz6eueN1TLuT0w)|KoyA{h)ZgLb~J z%=OW>75{FymCeRmSPw+C^}Jmbu?!dk7z1zy;6}@CNX%!lA$|tvGKCFEZz~KSysfpN zGZ~^#b-iFN6$F`JzDlyUpt(0ek*5vpe*8lI>YJMXbs?3czdv40o;k|2vsR8fy#@E| z`3q6T;K98I4N~Yt2eAkii7}vd2H-|pQ@SaxP_`ml78(a!bCVYa4O)ldU_-@xdBLGz9e@JtS*% ztBg21SEs*RozN8T{5(9KpsKpDwuafz$QBBP+S-~lJuPEnD)8!vUig|d-@-G4?swKK z-?L|LfJn@4(bI_KR67G`ANi@S5($#ye)m5UQDOU z&euUF{#a5G{IU0uBj;;s>K;B!L01~fg)z`6418%u3;NiiB06wKYS_&X^s&I-xj^!v z(ez5o=x^T@v)JuA#BCuuF0E$o^*p{nY`LK0ZPoX7N`qja7z6Dw@TD1TRaIkEHN(KL zo0FrXX?IhhP{il+EiKIZd3ls}x!&XGjq)EfU2c&9hk)9N?LgU`ExY(X0 zMQma5UCn?BbG)urtwZu^Ya79voaGf2I6U6b-kuLm;}nTpU7TLMev_S($6<4F^UB>^ zED*6r?oNh#s3no=v~{(>i5RadI3eeE*uXPB7!T*? z7lJ<4)mgkW_9`ts<82n3&0(|H#UH;VbQq`971fa(mudRnUA@5wJ7C7j$bN%0YLRk2%sE1$J|LTi8NXv(UtTn9?% z>r;dRk%_TU4>z&Jrf0rONlSn9IC;gm+hijnHWwO-J#o=-|PoKZ6t*=jcmF8$?)&rc;i8@Sj*Iz!;3fp6dnlLP5S1_Q$BOiA1f$cY) zL)MH`=J%~DbXFzgXsw2d)k93d~~L zaDqjAbOunb9t$$UL(k|hjh%wvx#FYOLQVmFns%RF)_PQ}y!^7lVm5(*>uzFXYh%*G z)kYSIQt(ZH$2~W&oYh+6NvwJ)*_8VtVA_ZMS=coLn)uyZDG` zEMN>^40Is_aHFluOnjWjhUgi!!2jvHq-)m|h^30@&bgVDIJC z(#a|=+l7_EL}3hk4Gh4IHuu7&m4C@RSHy&_jDaBYh36C3^+rL&hm=JDk7dCaz!;D* zppli8)!A&^al8XWEEX+Rqabj?0OqV*jeKHIABzFtti01s82DIq>H@jW~NJlB(x~F7VZv9sZbiXS%O% z^YA$1N4+Tx2$&#$&C6B| zhuFl(HA2)A2~)B1N;UrQM3~V^yieRO)p530cAlloa|K*9=gFyK|Kj@0Ub{Eq*uK@@ zP#*4@J9Sec~E;!qL3 zdBb_b?;l=_&)(tlYVXd7DiCS6<;3-dlS{mbBhO#I-f;c&t{&p7u556G;RUQ&xIsUV5VH{i=;1L`+2K%IM(@o3=c_TnkU2 z_Hnb-M#Mxct}G`?%r-TG*s)g@0ln62pN=Zt(FiQE^GDw)> z8nu;?7$zM&pW8BIqAOGs2v0XiH5b?Erf zFmw#4(w>O(K^CdIoxJg&xgVdZVN1n@GP@R21?b&-eFTAk|YObg}?7*HuO9HiBx9 zFcGCI6Jy|L0rLxlUQcB?(O?3d+SCZDD6GKQb~l#OSD7GX6_ceQVT#k*N>_p=Un4|4 z5it?lNVRrXqLs2F6;_X%JXhQrshx9Q86?C^NzH<^N4i-l&GiW-lE|6@x^xmQYOI%c zStqBazP?FaQ3aT10du9-mP;pG#>SSqqcScT#JZaqUjB|&g z-ZS_@Zdv;MyWlN%C4x{bL?K}!)(Aq~#E5z#Vk%J{F~9mEQ5tQN=Za13dakItwQ+T1 zh3A?BD_oUNN7Pq^4@V+TnYU0s{)b+{A;EbT!cn;e^) ztk}HSH~+}c=@WG)&GU~+E>^g5{(NZwSV>;6EvNDLI`GBUFQIvFkD1T_00a0*L_t&q zx>YTZFp;IBuRanca_P><2^o%9b3I7=c<8)t;{v=7Je2HAQ7j1ELKG4vVwF%gF@&fm zBBo;H5woi=5@EwYS=6i{J2*cj#(dwr8?QR%`;pr;wzISXqpLkHmml zJXf%u?_IDuhBa)%vfiwWl%`kVafbFDmMT5?_(&9BVlf6jF9y`&xuW9fy-aXa^PQdZ z#k<{`g4XoouXYaYL^c=<72J+1(F3pU?T$)hVM$*h0|J4z0s3gsgob?J}cU<_akd?*8$(S9g{Sb26NfSIp$uR~`=JbCb&eRz_qqoYg6&6W%W3EP(k`HdLRr)N*k!DDBx4!={_a)^im94s1R0Arv- z48We#N<3HOI(WF+8>$;>?ZO ziL>-SX5BE^7z1A<18VVH(TW)j9bMosLBLn@dmyd(2T!G2M`6D)2EGCY&}|ry5YevZ z3L$v)gIibl;=;D*OxnoZzTG;JKUH5M=|oj9XpDibWdOC&HhHdy6??A8LDcczZ9cP4 ziX9P>Z2fkf+cmj87Z->iSR}>(#y~p^pnT+m#&d<+qR2}ZPaogEb^__n&r3pYwR2)d zJBne+7y}ps$PA$CX{-O)aVUHEmV>T*CKEXAW{Vwn3ph+B3+}msV&>v*20cp^*1Vlf6V20F|DI-^D7xdNtwp@)YVl=Su;9rA>Eo$0WSSV4>di~$$} z=!~{q&lU2VR;HvDLt4F!bug+i1~3NH&H&tK>oOA`=dmGr1~~SG_b%z$H3LY?cHl5) zJ&0oN?$zw&4UCKvzz$RcdoM3{sXotsoqC8dV*Ef?Ya=aANoqpGpZ6e_74wFmyCbN* zP8cA@z!%K`+^%vjY+Cu3#Iq#`F`+ACAjo{-`NVa-+hf4ov!6lq^*?W)sIKP__04R1 u&EEZgO9Nb*JdCzi8cW9*z!*@4f&T~L_RwG!;b+ +%% Hack: re-defining tag types for supporting highlighting of antiquotations +\gdef\lst@tagtypes{s} +\gdef\lst@TagKey#1#2{% + \lst@Delim\lst@tagstyle #2\relax + {Tag}\lst@tagtypes #1% + {\lst@BeginTag\lst@EndTag}% + \@@end\@empty{}} +\lst@Key{tag}\relax{\lst@TagKey\@empty{#1}} +\lst@Key{tagstyle}{}{\def\lst@tagstyle{#1}} +\lst@AddToHook{EmptyStyle}{\let\lst@tagstyle\@empty} +\gdef\lst@BeginTag{% + \lst@DelimOpen + \lst@ifextags\else + {\let\lst@ifkeywords\iftrue + \lst@ifmarkfirstintag \lst@firstintagtrue \fi}} +\lst@AddToHookExe{ExcludeDelims}{\let\lst@ifextags\iffalse} +\gdef\lst@EndTag{\lst@DelimClose\lst@ifextags\else} +\lst@Key{usekeywordsintag}t[t]{\lstKV@SetIf{#1}\lst@ifusekeysintag} +\lst@Key{markfirstintag}f[t]{\lstKV@SetIf{#1}\lst@ifmarkfirstintag} +\gdef\lst@firstintagtrue{\global\let\lst@iffirstintag\iftrue} +\global\let\lst@iffirstintag\iffalse + \lst@AddToHook{PostOutput}{\lst@tagresetfirst} + \lst@AddToHook{Output} + {\gdef\lst@tagresetfirst{\global\let\lst@iffirstintag\iffalse}} + \lst@AddToHook{OutputOther}{\gdef\lst@tagresetfirst{}} +\lst@AddToHook{Output} + {\ifnum\lst@mode=\lst@tagmode + \lst@iffirstintag \let\lst@thestyle\lst@gkeywords@sty \fi + \lst@ifusekeysintag\else \let\lst@thestyle\lst@gkeywords@sty\fi + \fi} +\lst@NewMode\lst@tagmode +\gdef\lst@Tag@s#1#2\@empty#3#4#5{% + \lst@CArg #1\relax\lst@DefDelimB {}{}% + {\ifnum\lst@mode=\lst@tagmode \expandafter\@gobblethree \fi}% + #3\lst@tagmode{#5}% + \lst@CArg #2\relax\lst@DefDelimE {}{}{}#4\lst@tagmode}% +\gdef\lst@BeginCDATA#1\@empty{% + \lst@TrackNewLines \lst@PrintToken + \lst@EnterMode\lst@GPmode{}\let\lst@ifmode\iffalse + \lst@mode\lst@tagmode #1\lst@mode\lst@GPmode\relax\lst@modetrue} +% +\def\beginlstdelim#1#2#3% +{% + \def\endlstdelim{\texttt{\textbf{\color{black!60}#2}}\egroup}% + \ttfamily\textbf{\color{black!60}#1}\bgroup\rmfamily\color{#3}\aftergroup\endlstdelim% +} +%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% +\providecolor{isar}{named}{blue} +\renewcommand{\isacommand}[1]{\textcolor{OliveGreen!60}{\ttfamily\bfseries #1}} +\newcommand{\inlineisarbox}[1]{#1} +\NewTColorBox[]{isarbox}{}{ + ,boxrule=0pt + ,boxsep=0pt + ,colback=white!90!isar + ,enhanced jigsaw + ,borderline west={2pt}{0pt}{isar!60!black} + ,sharp corners + ,before skip balanced=0.5\baselineskip plus 2pt + % ,before skip=10pt + % ,after skip=10pt + ,enlarge top by=0mm + ,enhanced + ,overlay={\node[draw,fill=isar!60!black,xshift=0pt,anchor=north + east,font=\bfseries\footnotesize\color{white}] + at (frame.north east) {Isar};} +} +%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% +\providecolor{out}{named}{green} +\newtcblisting{out}[1][]{% + listing only% + ,boxrule=0pt + ,boxsep=0pt + ,colback=white!90!out + ,enhanced jigsaw + ,borderline west={2pt}{0pt}{out!60!black} + ,sharp corners + % ,before skip=10pt + % ,after skip=10pt + ,enlarge top by=0mm + ,enhanced + ,overlay={\node[draw,fill=out!60!black,xshift=0pt,anchor=north + east,font=\bfseries\footnotesize\color{white}] + at (frame.north east) {Document};} + ,listing options={ + breakatwhitespace=true + ,columns=flexible% + ,basicstyle=\small\rmfamily + ,mathescape + ,#1 + } + }% +%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% +\lstloadlanguages{ML} +\providecolor{sml}{named}{red} +\lstdefinestyle{sml}{ + basicstyle=\ttfamily,% + commentstyle=\itshape,% + keywordstyle=\bfseries\color{CornflowerBlue},% + ndkeywordstyle=\color{green},% + language=ML +% ,literate={% +% {<@>}{@}1% +% } + ,keywordstyle=[6]{\itshape}% + ,morekeywords=[6]{args_type}% + ,tag=**[s]{@\{}{\}}% + ,tagstyle=\color{CornflowerBlue}% + ,markfirstintag=true% +}% +\def\inlinesml{\lstinline[style=sml,breaklines=true,mathescape,breakatwhitespace=true]} +\newtcblisting{sml}[1][]{% + listing only% + ,boxrule=0pt + ,boxsep=0pt + ,colback=white!90!sml + ,enhanced jigsaw + ,borderline west={2pt}{0pt}{sml!60!black} + ,sharp corners + % ,before skip=10pt + % ,after skip=10pt + ,enlarge top by=0mm + ,enhanced + ,overlay={\node[draw,fill=sml!60!black,xshift=0pt,anchor=north + east,font=\bfseries\footnotesize\color{white}] + at (frame.north east) {SML};} + ,listing options={ + style=sml + ,columns=flexible% + ,basicstyle=\small\ttfamily + ,mathescape + ,#1 + } + }% +%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% +\lstloadlanguages{TeX} +\providecolor{ltx}{named}{yellow} +\lstdefinestyle{lltx}{language=[AlLaTeX]TeX, + ,basicstyle=\ttfamily% + ,showspaces=false% + ,escapechar=ë + ,showlines=false% + ,morekeywords={newisadof} + % ,keywordstyle=\bfseries% + % Defining 2-keywords + ,keywordstyle=[1]{\color{BrickRed!60}\bfseries}% + % Defining 3-keywords + ,keywordstyle=[2]{\color{OliveGreen!60}\bfseries}% + % Defining 4-keywords + ,keywordstyle=[3]{\color{black!60}\bfseries}% + % Defining 5-keywords + ,keywordstyle=[4]{\color{Blue!70}\bfseries}% + % Defining 6-keywords + ,keywordstyle=[5]{\itshape}% + % +} +\lstdefinestyle{ltx}{style=lltx, + basicstyle=\ttfamily\small}% +\def\inlineltx{\lstinline[style=ltx, breaklines=true,columns=fullflexible]} +% see +% https://tex.stackexchange.com/questions/247643/problem-with-tcblisting-first-listed-latex-command-is-missing +\NewTCBListing{ltx}{ !O{} }{% + listing only% + ,boxrule=0pt + ,boxsep=0pt + ,colback=white!90!ltx + ,enhanced jigsaw + ,borderline west={2pt}{0pt}{ltx!60!black} + ,sharp corners + % ,before skip=10pt + % ,after skip=10pt + ,enlarge top by=0mm + ,enhanced + ,overlay={\node[draw,fill=ltx!60!black,xshift=0pt,anchor=north + east,font=\bfseries\footnotesize\color{white}] + at (frame.north east) {\LaTeX};} + ,listing options={ + style=lltx, + ,columns=flexible% + ,basicstyle=\small\ttfamily + ,#1 + } + }% +%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% +\providecolor{bash}{named}{black} +\lstloadlanguages{bash} +\lstdefinestyle{bash}{% + language=bash + ,escapechar=ë + ,basicstyle=\ttfamily% + ,showspaces=false% + ,showlines=false% + ,columns=flexible% + % ,keywordstyle=\bfseries% + % Defining 2-keywords + ,keywordstyle=[1]{\color{BrickRed!60}\bfseries}% + % Defining 3-keywords + ,keywordstyle=[2]{\color{OliveGreen!60}\bfseries}% + % Defining 4-keywords + ,keywordstyle=[3]{\color{black!60}\bfseries}% + % Defining 5-keywords + ,keywordstyle=[4]{\color{Blue!80}\bfseries}% + ,alsoletter={*,-,:,~,/} + ,morekeywords=[4]{}% + % Defining 6-keywords + ,keywordstyle=[5]{\itshape}% + % +} +\def\inlinebash{\lstinline[style=bash, breaklines=true,columns=fullflexible]} +\newcommand\@isabsolutepath[3]{% + \StrLeft{#1}{1}[\firstchar]% + \IfStrEq{\firstchar}{/}{#2}{#3}% +} + +\newcommand{\@homeprefix}[1]{% + \ifthenelse{\equal{#1}{}}{\textasciitilde}{\textasciitilde/}% +} + +\newcommand{\prompt}[1]{% + \color{Blue!80}\textbf{\texttt{% + achim@logicalhacking:{\@isabsolutepath{#1}{#1}{\@homeprefix{#1}#1}}\$}}% +} +\newtcblisting{bash}[1][]{% + listing only% + ,boxrule=0pt + ,boxsep=0pt + ,colback=white!90!bash + ,enhanced jigsaw + ,borderline west={2pt}{0pt}{bash!60!black} + ,sharp corners + % ,before skip=10pt + % ,after skip=10pt + ,enlarge top by=0mm + ,enhanced + ,overlay={\node[draw,fill=bash!60!black,xshift=0pt,anchor=north + east,font=\bfseries\footnotesize\color{white}] + at (frame.north east) {Bash};} + ,listing options={ + style=bash + ,columns=flexible% + ,breaklines=true% + ,prebreak=\mbox{\space\textbackslash}% + ,basicstyle=\small\ttfamily% + ,#1 + } + }% +%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index e0b1e66e..b6b10f56 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -431,13 +431,14 @@ text\ and can now be specified in common HOL syntax. One can now specify the constraints using the keyword \<^theory_text>\invariant\ in the class definition. If we take back the ontology example for mathematical papers - of~@{cite "brucker.ea:isabelledof:2019"} (ADD LISTING REFERENCE!!!), + of~@{cite "brucker.ea:isabelledof:2019"} (see ADD LISTING REFERENCE!!!), it was proposed to specify some constraints like that any instance of a \<^emph>\result\ class finally has a non-empty property list, if its \<^theory_text>\kind\ is \<^theory_text>\"proof"\ (see the \<^theory_text>\invariant has_property\), or that the \<^theory_text>\establish\ relation between \<^theory_text>\claim\ and \<^theory_text>\result\ must be defined when an instance - of the class \<^theory_text>\conclusion\ is defined (see the \<^theory_text>\invariant establish_defined\). -@{boxed_theory_text [display,indent=10, margin=70] \ + of the class \<^theory_text>\conclusion\ is defined (see the \<^theory_text>\invariant establish_defined\). +\begin{figure} +@{boxed_theory_text [display] \ doc_class author = email :: "string" <= "''''" doc_class text_section = @@ -464,7 +465,9 @@ doc_class conclusion = text_section + invariant establisg_defined :: "\ x. x \ Domain (establish \) \ (\ y \ Range (establish \). (x, y) \ establish \)" \} - +\caption{Excerpt of an ontology example for mathematical papers.} +\label{fig-ontology-example} +\end{figure} In our example, the invariant \<^theory_text>\author_finite \ of the class \<^theory_text>\introduction\ enforces that the user sets the \<^theory_text>\authored_by\ set. @@ -477,15 +480,21 @@ doc_class conclusion = text_section + of the future instance of the class \<^theory_text>\conclusion\. Now we can define some instances: +\begin{figure} @{boxed_theory_text [display] \ text*[church::author, email="\church@lambda.org\"]\\ text*[resultProof::result, evidence = "proof", property="[@{thm \HOL.refl\}]"]\\ +text*[resultProof2::result, evidence = "proof", property="[@{thm \HOL.sym\}]"]\\ + text*[introduction1::introduction, authored_by = "{@{author \church\}}", level = "Some 0"]\\ text*[claimNotion::claim, authored_by = "{@{author \church\}}", based_on= "[\Notion1\, \Notion2\]", level = "Some 0"]\\ \} +\caption{Some instances of the classes of the ontology in the \autoref{fig-ontology-example}.} +\label{fig-instances-example} +\end{figure} \ (*<*) @@ -507,7 +516,7 @@ text\ constraint specified in the \<^theory_text>\force_level\ invariant, when we specify the \<^theory_text>\level\ attribute of \<^theory_text>\introduction\ to \<^theory_text>\Some 0\. The \<^theory_text>\force_level\ invariant forces the value of the argument - of the attribute \<^theory_text>\level\ option type to be greater than 1. + of the attribute \<^theory_text>\level\ to be greater than 1. \ figure*[ @@ -522,7 +531,7 @@ declare_reference*["inherited-invariant-checking-figure"::figure] (*>*) text\ - Classes inherit the invariants from their superclasses. + Classes inherit the invariants from their superclass. As the class \<^theory_text>\claim\ is a subsclass of the class \<^theory_text>\introduction\, it inherits the \<^theory_text>\introduction\ invariants. Hence the \<^theory_text>\force_level\ invariant is checked @@ -538,35 +547,6 @@ figure*[ from the class \<^theory_text>\introduction\ and is violated by the instance \<^theory_text>\claimNotion\. \ -(* -text\For example, with the following two classes: -\<^theory_text>\ -doc_class class_inv1 = - int1 :: "int" - invariant inv1 :: "int1 \ \ 3" - -doc_class class_inv2 = class_inv1 + - int2 :: "int" - invariant inv2 :: "int2 \ < 2" -\ - - as the class \<^theory_text>\class_inv2\ is a subsclass - of the class \<^theory_text>\class_inv1\, it inherits \<^theory_text>\class_inv1\ invariants. - Hence the \<^theory_text>\inv1\ invariant is checked - when the instance \<^theory_text>\testinv2\ is defined, like we can see in . - - Now let's define two instances, one of each class:\ - - - -text\ -\<^theory_text>\ -text*[testinv1::class_inv1, int1=4]\lorem ipsum...\ -text*[testinv2::class_inv2, int1=3, int2=1]\lorem ipsum...\ -\ -\ -*) - text\ The value of each attribute defined for the instances is checked against their classes invariants. As the class \<^theory_text>\class_inv2\ is a subsclass of the class \<^theory_text>\class_inv1\, @@ -574,37 +554,97 @@ text\ Hence the \<^theory_text>\int1\ invariant is checked when the instance \<^theory_text>\testinv2\ is defined.\ text\ - Isabelle/HOl provides commands which type-check and print terms (the command \<^theory_text>\term\) - and evaluates and print a term (the command \<^theory_text>\value\). - We provide the equivalent commands, respectively \<^theory_text>\term*\ and \<^theory_text>\value*\. - These commands add up type-checking and expanding of isabelle/DOF antiquotations - in a own validation phase. + To offer a smooth integration into the theory development process, + Isabelle/HOL should be able to dynamically interpret the source document. + But the specific antiquotations introduced by Isabelle/DOF are not directly recognized + by Isabelle/HOL, and the process of term checking and evaluation must be enriched. + Previous works added a validation step fo the SML and semi-formal text contexts. + But to support Isabelle/DOF antiquotations in the term contexts, the validation step must + be enriched and a new step, which we call \<^emph>\elaboration\ must be added to allow + these antiquotations in \\\-terms. + The resulting process encompasses the following steps: + \<^item> Parse the term which represents the object; + \<^item> Infer the type of the term; + \<^item> Certify the term; + \<^item> Pass on the information to PIDE; + \<^item> Validate the term: the Isabelle/DOF antiquotations terms are parsed and type-checked; + Validate the term: a step to understand the reference + which refers to the object. + + This step is mandatory because the ontology framework adds + up objects not directly recognized by Isabelle/HOL; + + \<^item> Elaborate: the Isabelle/DOF antiquotations terms are expanded. + The antiquotations are replaced by the objects in HOL they reference + i.e. a \(\lambda\)-calculus term; + \<^item> Code generation: + \<^item> Evaluation of HOL expressions with ontological annotations, + \<^item> Implementation of the ontological invariants processed simultaneously + with the generation of the document (a theory in HOL). + + Isabelle/HOL provides commands to type-check and print terms (the command \<^theory_text>\term\) + and evaluate and print a term (the command \<^theory_text>\value\). + We provide the equivalent commands, respectively \<^theory_text>\term*\ and \<^theory_text>\value*\, which support + the validation and elaboration phase. + This allow a smooth integration into the \<^emph>\formal\ theory development process. +\ + +(*<*) +declare_reference*["type-checking-example"::side_by_side_figure] +(*>*) + +text\ For example one can now reference a class instance in a \<^theory_text>\term*\ command: @{theory_text [display,indent=10, margin=70] \ term*\@{author \church\}\ \} The term \<^theory_text>\@{author \church\}\ is type-checked, \<^ie>, the command \<^theory_text>\term*\ checks that -\<^theory_text>\church\ references a term of type \<^theory_text>\author\. - - and the and we would like -Isabelle to check that this instance is indeed an instance of this class. -Here, we want to reference the instance \<^theory_text>\@{docitem \xcv4\}\ previously defined. -We can use the term* command which extends the classic term command -and does the appropriate checking. -@{theory_text [display,indent=10, margin=70] \ -term*\@{F \xcv4\}\ -\} -We can also reference an attribute of the instance. -Here we reference the attribute r of the class F which has the type @{typ \thm list\}. - -@{theory_text [display,indent=10, margin=70] \ -term*\r @{F \xcv4\}\ - -term \@{A \xcv2\}\ -\} +\<^theory_text>\church\ references a term of type \<^theory_text>\author\ +(see \<^side_by_side_figure>\type-checking-example\). \ +side_by_side_figure*[ + "type-checking-example"::side_by_side_figure + , anchor="''fig-term-type-checking-ex''" + , caption="''church is an existing instance.''" + , relative_width="48" + , src="''figures/term-context-checking-example''" + , anchor2="''fig-term-type-checking-failed-ex''" + , caption2="''The churche instance is not defined.''" + , relative_width2="48" + , src2="''figures/term-context-failed-checking-example''" +]\Type-checking of antiquotations in term context.\ + +(*<*) +declare_reference*["evaluation-example"::side_by_side_figure] +(*>*) + +text\ + This \<^theory_text>\value*\ command: +@{theory_text [display,indent=10, margin=70] \ +value*\email @{author \church\}\ +\} + +type-checks the antiquotation \<^theory_text>\@{author \church\}\, +and then returns the value of the \<^theory_text>\email\ attribute for the \<^theory_text>\church\ instance, +\<^ie> the HOL string \<^term>\''church@lambda.org''\ +(see \<^side_by_side_figure>\evaluation-example\). +\ + +side_by_side_figure*[ + "evaluation-example"::side_by_side_figure + , anchor="''fig-term-evaluation-ex''" + , caption="''A Text-Element as Requirement.''" + , relative_width="48" + , src="''figures/term-context-evaluation-example''" + , anchor2="''fig-term-failed-evaluation-ex''" + , caption2="''Referencing a Requirement.''" + , relative_width2="48" + , src2="''figures/term-context-failed-evaluation-example''" +]\Evaluation of antiquotations in term context.\ + +(* figure*[ "term-context-checking-example-figure"::figure , relative_width="99" @@ -620,27 +660,27 @@ figure*[ ]\The invariant \<^theory_text>\force_level\ of the class claim is inherited from the class \<^theory_text>\introduction\ and is violated by the instance \<^theory_text>\claimNotion\. \ +*) -figure*[ - "term-context-equality-evaluation-figure"::figure - , relative_width="99" - , src="''figures/term-context-equality-evaluation-example''" -]\The invariant \<^theory_text>\force_level\ of the class claim is inherited - from the class \<^theory_text>\introduction\ and is violated by the instance \<^theory_text>\claimNotion\. +(*<*) +declare_reference*["term-context-equality-evaluation"::figure] +(*>*) + +text\ +We can even compare classes. \<^figure>\term-context-equality-evaluation\ +shows that the two classes \<^theory_text>\resultProof\ and \<^theory_text>\resultProof2\ are not equivalent +because their attribute \<^theory_text>\property\ differ. \ +figure*[ + "term-context-equality-evaluation"::figure + , relative_width="80" + , src="''figures/term-context-equality-evaluation-example''" +]\Evaluation of the equivalence of two class instances. +\ -text\We declare a new text element. Note that the class name contains an underscore "\_".\ -text*[te::text_element]\Lorem ipsum...\ - -text\Unfortunately due to different lexical conventions for constant symbols and mixfix symbols - this term antiquotation has to be denoted like this: @{term\@{text-element \ee\}\}. - We need to substitute an hyphen "-" for the underscore "\_".\ -term*\@{text-element \te\}\ subsection\Example and Queries\ -section*["morphisms"::technical,main_author="Some(@{docitem ''idir''}::author)"] \Proving Morphisms on Ontologies\ - text\ A new mechanism to make query on instances is available and uses the HOL implementation of lists. So complex queries can be defined using functions over the instances list. @@ -668,6 +708,8 @@ value*\filter (\\. Z.z \ > 2) @{Z-instances}\ EXPLAIN VALUE* ??? \ +section*["morphisms"::technical,main_author="Some(@{docitem ''idir''}::author)"] \Proving Morphisms on Ontologies\ + section*[ontoexample::text_section,main_author="Some(@{docitem ''idir''}::author)"] \Applications\ subsection\Engineering Example : An Extract from PLib\