[ProofPower] Two questions

[Philip Clayton]

Stephen Brackin wrote:

> Here's a dumb question: What's wrong with this?  spec_nth_asm_tac 
> objects that the relevant assumption isn't universally quantified, but 
> it is.
>
> %SZG%[ PT ]%BHH%%BHH%%BHH%%BHH%%BHH%%BHH%%BHH%%BHH%%BHH%%BHH%%BHH%
> %BV% p:PT
> %EZ%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%
>
> set_goal([],%SZT%{p} %neq% %emptyset%%>%);
> a(rewrite_thm_tac (get_thm "z_sets" "z_%neq%_thm"));
> a(rewrite_thm_tac (get_defn "z_sets" "%emptyset%"));
> a(rewrite_thm_tac (get_thm "z_sets" "z_sets_ext_clauses"));
> a(contr_tac);
> a(spec_nth_asm_tac 1 %SZT%p%>%);
>
You need z_spec_nth_asm_tac because it's a Z universal quantification.

Alternatively, the proof could just be:
set_goal([],%SZT%{p} %neq% %emptyset%%>%);
a (PC_T1 "z_sets_ext" prove_tac []);

> Here's a better question: Do you have any suggestions for how I can 
> debug this sort of thing without asking Lemma1?  What should I do when 
> I get an error message that just seems wrong?
>

When things don't work, it's often because the term you're looking at 
isn't what you think it is.  (In my experience with the subgoal package, 
this is usually because types aren't what you think they are.)  I 
usually go about solving the problem by picking apart the terms in my 
current subgoal to see what they really are.  This is done with the term 
destructor functions:

val (asms, conc) = top_goal ();
val asm1 = nth 0 asms; (* get assumption 1 *)

dest_z_term asm1;
dest_term asm1;
(* clearly a Z universal quantification *)

This alone doesn't help if you think spec_nth_asm_tac should work with Z 
quantifiers --- pulling apart the term will just tell you assumption 1 
is really a Z quantification.  Ideally you would find an example of 
spec_nth_asm_tac working (from e.g. the ProofPower distribution) and 
pull apart the terms in that example and compare their structure.  grep 
"spec_nth_asm_tac" imp*.doc gives me an example proof in imp073.   To 
try this I got the theory name from imp073 at the start and just guessed 
at the hol proof context (being a HOL theory) when it didn't work the 
first time:

open_theory "fin_set";
set_pc "hol";
push_goal([], %<%
        %forall%p%spot%    p {} %and% (%forall%a x%spot%a %mem% Finite 
%and% p a %and% %not%x %mem% a %implies% p({x} %union% a))
        %implies%     %forall%a%spot%a %mem% Finite %implies% p a
%>%);
a(REPEAT strip_tac);
a(asm_ante_tac%<%a %mem% Finite%>%);
a(rewrite_tac[get_spec%<%Finite%>%]);
a(REPEAT strip_tac);

(* a(spec_nth_asm_tac 1 %<%{b | b %mem% Finite %and% p b}%>%); *)

val (asms, conc) = top_goal ();
val asm1 = nth 0 asms; (* get assumption 1 *)

dest_z_term asm1; (* fails... not a Z term?? *)
dest_term asm1; (* it's a HOL quantification! *)

That it works on HOL quantification but not Z quantification should give 
some clue as to the problem.

Phil