Re: [isabelle] Proof state in Isar proof style are difficult to follow



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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.