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

mongodb - How to keep track of users making Stripe Payments -

i'm trying figure out way mean stack application keep track of users have paid grant them access portion of webpage. i've considered several options: stripe customer id, mongodb record, , html attribute can update. my mean stack keeps track of users jwt, , appears stripe assigns them own customer id isn't ideal. can done jwt opposed forced cutomer id? mongodb record. i'm thinking might best option. when new user has been created, i'll give attribute of haspaid = no. update record of customer when payment submitted. guess run script set unpaid each day? html element/attribute. don't know if possible; cool create key carried during html session after payment received. if person closers browser session closed? i'm looking guidance on 3 options determine if they're best solution. also, if has suggestions alternatives, i'm ears! thanks in advance. speaking generally, common approach second one: use attribute in data model indicates
Read more