*To*: "ehmety at univ-nkc.mr" <ehmety at univ-nkc.mr>*Subject*: Re: [isabelle] Proof state in Isar proof style are difficult to follow*From*: "chen kun" <coolchenice81 at gmail.com>*Date*: Fri, 24 Mar 2006 14:13:43 +0800*Cc*: cl-isabelle-users at lists.cam.ac.uk*Domainkey-signature*: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=d4a//lxdOr9eiI8MzmRae/l8W6n263Qs3h/IB/hs+Z4hwbP9+ITa9cXHgDGuNv+xqXQhO1LzvOu/ApZWexLx/7osv6UD7chOqvH5YpGqOg6L2QZF6TRx8IzfSKsAsHO76xDuxOR8r29ceKpx16m2dOpUJLiKf/Jfp/mOWUFlEa8=*In-reply-to*: <48790.82.151.64.3.1143023312.squirrel@www.univ-nkc.mr>*References*: <17439.41051.289539.743971@raceme.rsise.anu.edu.au> <ea4eb58d1baa7a9b07c3f237bf25d5b2@in.tum.de> <48790.82.151.64.3.1143023312.squirrel@www.univ-nkc.mr>

Here is an avaiable proof script: lemma assumes ex: "EX x. ALL y. P x y" shows "ALL y. EX x. P x y" proof fix y - - Here must fix "y" ,which is exacatly the variable name in your goal from ex obtain x where "ALL y. P x y" by blast thus "EX x. P x y" by blast qed 2006/3/22, ehmety at univ-nkc.mr <ehmety at univ-nkc.mr>: > Hi > > I was used to ML proof style and now I am trying to learn the isar mode. > But I found it very hard to follow. I am not sure whether this is normal > or I am missing something: > > Let me explain this with this example taken from the 'Structured Proofs in > Isar/HOL' document: > > lemma assumes ex: "EX x. ALL y. P x y" shows "ALL y. EX x. P x y" > proof > fix a > from ex obtain x where "ALL y. P x y" .. > hence "P x a" .. > thus "EX x. P x a" .. > qed > > Proof starts with a nice display of the proof state (with every thing I > need): > > proof (state): step 1 > fixed variables: P > prems: > EX x. ALL y. P x y > goal (lemma, 1 subgoal): > 1. !!y. EX x. P x y > > But things go differently > 1. When I do 'fix a' for the variable 'y' in the goal, > I get the equality a = a in the 'fixed variables' section. > > proof (state): step 2 > > fixed variables: P, a = a > prems: > EX x. ALL y. P x y > > goal (lemma, 1 subgoal): > 1. !!y. EX x. P x y > > However I was expecting 'y = a' instead. > > 2. At the second step (from ex obtain …) the display becomes difficult to > follow: > a) execution of 'from ex' gives: > > proof (chain): step 3 > > picking this: > EX x. ALL y. P x y > > (nothing shown about the rest of the state) You can use "print_context ", " print_theorems" , "print_facts" etc. to inspect proof contexts . See <<Isar-ref.pdf>> 3.3.2 for details . Or you can simply use command "term ?thesis" to see what the term ?thesis stands for. See <<Isar-ref.pdf>> 3.3.1 for details. > > b) execution of all the 'from' step returns > have (!!x. ALL y. P x y ==> ?thesis) ==> ?thesis > Every thing is hided. > > The same thing happens with proof steps starting 'have'. > > How one can see what goals remain to be proved? > > This kind of displays confuses me. > > Best regards > > > > -- Chen Kun Foundation Software Engineering Center Institute of Software Chinese Academy of Science

**References**:**[isabelle] programming with locales***From:*Michael Norrish

**Re: [isabelle] programming with locales***From:*Clemens Ballarin

**[isabelle] Proof state in Isar proof style are difficult to follow***From:*ehmety

- Previous by Date: [isabelle] CFP: AFM 2006 Workshop on Automated Formal Methods @ IJCAR/FLoC 2006
- Next by Date: [isabelle] FOL.thy
- Previous by Thread: [isabelle] Proof state in Isar proof style are difficult to follow
- Next by Thread: [isabelle] CFP: AFM 2006 Workshop on Automated Formal Methods @ IJCAR/FLoC 2006
- Cl-isabelle-users March 2006 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