*To*: <den9562 at rit.edu>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Automating a Repetitive Structured Proof*From*: <Matthew.Brecknell at data61.csiro.au>*Date*: Mon, 16 Oct 2017 02:18:58 +0000*Accept-language*: en-AU, en-US*In-reply-to*: <1968506.uP09iNJjUk@tiger>*References*: <1968506.uP09iNJjUk@tiger>*Thread-index*: AQHTRar5Aomfel+TKESjc+a79sKrPqLlBoIA*Thread-topic*: [isabelle] Automating a Repetitive Structured Proof

On Sat, 2017-10-14 at 13:42 -0400, David E. Narvaez wrote: > Hi, > > I have a structured proof that right now looks roughly like this: > > [...] > ÂÂÂÂcase And_bool_expr > ÂÂÂÂthen show ?thesis > ÂÂÂÂÂÂusing assms > ÂÂÂÂproof (cases "partial_val_bool_expr e2 a", simp_all add: models_def) > ÂÂÂÂÂÂcase (Const_bool_expr b) > ÂÂÂÂÂÂthen show ?thesis using assms And_bool_expr > by (cases b, simp_all add:Âmodels_def) > ÂÂÂÂqed > Â next > ÂÂÂÂcase Or_bool_expr > ÂÂÂÂthen show ?thesis > ÂÂÂÂÂÂusing assms > ÂÂÂÂproof (cases "partial_val_bool_expr e2 a", simp_all add: models_def) > ÂÂÂÂÂÂcase (Const_bool_expr b) > ÂÂÂÂÂÂthen show ?thesis using assms Or_bool_expr > by (cases b, simp_all add:Âmodels_def) > ÂÂÂÂqed > Â next > [...] > > and it goes on for about 6 cases. Instead of repeating these instructions, > IÂwant Isabelle to try the following for every case: > > ÂÂÂcase $casename > ÂÂÂÂthen show ?thesis > ÂÂÂÂÂÂusing assms > ÂÂÂÂproof (cases "partial_val_bool_expr e2 a", simp_all add: models_def) > ÂÂÂÂÂÂcase (Const_bool_expr b) > ÂÂÂÂÂÂthen show ?thesis using assms $casename > by (cases b, simp_all add:Âmodels_def) > ÂÂÂÂqed > > and discharge those that work using this strategy so that I'm left with > thoseÂthat really need work. > > From what I understand, this is the kind of things Eisbach is supposed to > beÂfor, but Eisbach does not seem to be meant for structured proofs, am IÂ > correct? If that is the case, then what tool could help me here? I have > readÂabout automation using ML but I cannot find much documentation about > that, withÂexamples of things that can automated using ML. > > Thanks! Hi David, It ought to be possible to make an Eisbach method to solve the boring cases, while keeping the structure of the overall proof. In that case, the overall proof might look something like this: proof (induct ...) case (Interesting_bool_expr arg1 arg2) show ?case proof ... qed next case (AnotherInteresting_bool_expr arg1 arg2 arg3) show ?case proof ... qed qed solve_boring_case+ Note the "solve_boring_case+" *after* the "qed" to handle any cases not yet proved in the "proof" block. The tricky part of making the Eisbach method will be obtaining bindings for the variables "e2", "a" and "b". For that, you might be able to use the "match" method, also part of Eisbach. Perhaps something like this: method solve_boring_case = (match goal in â... e2 ... a ...â for e2 a â âcases "partial_val_bool_expr e2 a"; simp add: models_def; match goal in â... b ...â for b â âcases b; simp add: models_defââ) You'll need to figure out what term patterns will allow you to correctly identify the right "e2", "a" and "b". You might need "match premises" instead of "match goal", and you might need to bind fact names to matched premises to wire them into proof fragments ("inner methods" in Eisbach-match terminology). Regards, Matthew

**References**:**[isabelle] Automating a Repetitive Structured Proof***From:*David E. Narvaez

- Previous by Date: [isabelle] CFP: ITP 2018
- Next by Date: [isabelle] New in the AFP: More about God
- Previous by Thread: [isabelle] Automating a Repetitive Structured Proof
- Next by Thread: [isabelle] New AFP entry: Homogeneous Linear Diophantine Equations
- Cl-isabelle-users October 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list