isabelle - Simplify meta-universally quantified assumptions with equality -


sorry not being able come shorter example.

i have proof state of

 1. ⋀e1 t1 l e2 t2 g1.        typing (g1 @ (x, u) # g2) e1 t1 ⟹        typing (g1 @ g2) e1 t1 ⟹        (⋀xa. xa |∉| l ⟹               typing ((xa, t1) # g1 @ (x, u) # g2) (open e2 (exp_fvar xa))                t2) ⟹        (⋀xa g1a.            xa |∉| l ⟹            (xa, t1) # g1 = g1a ⟹            x |∉| fv (open e2 (exp_fvar xa)) ⟹            typing (g1a @ g2) (open e2 (exp_fvar xa)) t2) ⟹        x |∉| fv e1 ⟹ x |∉| fv e2 ⟹ typing (g1 @ g2) (exp_let e1 e2) t2

note fourth premise (the large one): universally meta-quantifies on g1a, g1a determined equation there. substitute (and simplify conclusion of premise) , auto able solve goal.

can make simplifier solve this?

i guess small example is

lemma foo:   "(⋀ g.  x#xs = g ⟹ p x ⟹ f g) ⟹ f (x#xs)" apply simp

there related question equalities under existentials.

this problem can solved reliably using simproc. induct proof method in ~~/src/tools/induct.ml has implementation this, might able adapt code. idea move equations front using induct.rearrange_eqs_simproc , use appropriate 1 point rules eliminate equality.


-

Comments

Post a Comment

Popular posts from this blog

javascript - Thinglink image not visible until browser resize -

Image
i trying repurpose pre-existing theme, includes drop down menu displays image. trying embed thinglink drop down menu's content section, not visible until resize browser window. here menu looks like: then when clicked, can see empty space image should show: then when browser resized, image appears: this code content of menu: <div class="ajax_accordion_content" style="display: none;"> <div class="report-detail"> <table border="0" cellpadding="0" cellspacing="0" width="100%" class="table_basic"> <tbody> <!-- thinglink image embedded --> <img style="max-width: 100%;" src="http://cdn.thinglink.me/api/image/832705713204625409/1024/10/scaletowidth#tl-832705713204625409;1043138249'" class="alwaysthinglink"/> <script async charset="utf-8" src="http://cdn.thinglink.me/jse/embed.j...
Read more

firebird - Error "invalid transaction handle (expecting explicit transaction start)" executing script from Delphi -

i'm developing update app delphi 10. i'm running windows 7 64x, firebird 2.5.1.26351 32x. execution order: checks current version(select statement firebird database) downloads update(via ftp) apply it(.exe files, , execute .sql) error code -901 pops out when try execute .sql files. know there incompatibility issue w7 64x , fdb 32x, but, can everything: backup , restore(gbak), db commands(all). tried fdb 64x instead, , not working. code: //components fdwaitcursor: tfdguixwaitcursor; fddriverlink: tfdphysfbdriverlink; fdconnection:tfdconnection; fdscript: tfdscript; function tthr_script.createcomponents:boolean; begin try fddriverlink := tfdphysfbdriverlink.create(fddriverlink); fdwaitcursor := tfdguixwaitcursor.create(fdwaitcursor); fdconnection := tfdconnection.create(fdconnection); fdconnection begin drivername := 'fb'; params.username := thrbanco.bduser; params.password := thrbanco.bdpass; params.database := ...
Read more

Sound is not coming out while implementing Text-to-speech in Android activity -

i using texttospeak in 1 of app. while adding speech string texttospeech object instance, doesn't produce sound. though not getting error in log still sound not coming out. want device speak value of textview gets set resultmsg.settext() method. public class resultactivity extends activity { @override protected void oncreate(bundle savedinstancestate){ ............ resultmsg.settext(resultmsg_str); texttospeech = new texttospeech(getapplicationcontext(),newtexttospeech.oninitlistener(){ @override public void oninit(int status) { system.out.println("txt speech status = "+status); system.out.println("txt speech error status = "+texttospeech.error); system.out.println("txt speech success status = "+texttospeech.success); if(status == texttospeech.success){ texttospeech.setlanguage(locale.english); ...
Read more