Re: [Hol-info] Learning HOL Light

[Bill R. <ri...@ma...>]

Thanks, Petros, but I don't see how SUBGOAL_TAC is any better than SUBGOAL_THEN at avoiding the one-step-forward-one-step-back awkwardness of MP_TAC/DISCH_THEN ASSUME_TAC/FIRST_X_ASSUM that John's cases and the modification bcases have.  Below is a tactics script for my proof of the LABEL_TAC exercise in the HOL Light reference manual, which I should have posted yesterday.  BTW how does HOL and Informatics fit together?  Thanks for the feedback on my explanation of John's cases, which as you say assumes tac will prove t, as does bcases.  I thought of this 

   you could use replace MP_TAC with (REPEAT_TCL DISJ_CASES_THEN
   (LABEL_TAC lab)) [but] DISJ_CASES_THEN will create two new subgoals
   (for a total of three).

but as you say that won't work unless I can calculate how my disjuncts I'll get.  There must be a function that calculates that.  In the first bcases below, it's 2, and it's 3 for the second.  I need to know because of the THENL [tac; ALL_TAC], which would be changed to THENL [tac; ALL_TAC; ALL_TAC; ALL_TAC] for 3 disjuncts.  I also don't know how to print a variable number of ALL_TACs.  I thought maybe I could try 
SUBGOAL_THEN t ALL_TAC THENL [SUBGOAL_THEN t ALL_TAC; ALL_TAC]
so the top 3 goals in the goalstack would be (for g the original top goal) 
t, t, and g 
But  that won't fly, because 
MP_TAC is a thm_tactic, and ALL_TAC is just a tactic.  I that the correct usage?  And that's the difference between SUBGOAL_THEN and SUBGOAL_TAC, whether you use a thm_tactic or a tactic?  BTW how do I learn the typed LC or whatever that explains how tactics and thm_tactics actually work?  The HOL Light tutorial I think is actually a pretty good way to learn how to write tactics proofs, if you read the whole tutorial from beginning to end, dipping into the reference manual (and posting here!) when you get stuck, but I don't think it explains the theory of tactics proofs.  Maybe I missed it.  

-- 
Best,
Bill 

let soby labs MesonList = FIRST_ASSUM MP_TAC THEN MAP_EVERY 
   (fun l -> USE_THEN l MP_TAC) labs THEN (MESON_TAC MesonList);;
let consider t lab pf = SUBGOAL_THEN t (CHOOSE_THEN (LABEL_TAC lab)) THENL [pf; ALL_TAC];;
let state t lab pf = SUBGOAL_THEN t (LABEL_TAC lab) THENL [pf; ALL_TAC];;
let bcases t lab pf =
  state t  "" pf THEN FIRST_X_ASSUM 
  (REPEAT_TCL DISJ_CASES_THEN (LABEL_TAC lab));;

let WfAndAntisymImpliesWo = prove
  (`(!x y. x <<= y /\ y <<= x ==> x = y) /\
  (!s. ~(s = {}) ==> ?a:A. a IN s /\ !x. x IN s ==> a <<= x)
  ==> (!x y. x <<= y \/ y <<= x) /\
  !x y z. x <<= y /\ y <<= z ==> x <<= z`, 
  DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "antisym") (LABEL_TAC "swf")) 
  THEN STRIP_TAC THEN REPEAT GEN_TAC THENL [ALL_TAC;
  DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "xLESSy") (LABEL_TAC "yLESSz"))] THENL 
  [consider `?s:A->bool. s = {x:A,y:A}` "" (soby [] []);
  consider `?s:A->bool. s = {x:A,y:A,z:A}` "C" (soby [] [])] THENL
  [state `!p:A. p IN s <=> p = x \/ p = y` "sxy" (soby [] [IN_INSERT; MEMBER_NOT_EMPTY]);
  state `!p:A. p IN s <=> p = x \/ p = y \/ p = z` "sxyz" 
  (soby [] [IN_INSERT; MEMBER_NOT_EMPTY])] THEN
  state `~(s:A->bool = {})` "" (soby [] [MEMBER_NOT_EMPTY]) THEN
  consider `?a:A. a IN (s:A->bool) /\ !p:A. p IN s ==> a <<= p` "aExists" (soby ["swf"] []) THENL
  [bcases `a:A = x:A \/ a = y:A` "" (soby ["sxy"] []);
  bcases `a:A = x:A \/ a = y:A \/ a = z:A` "" (soby ["sxyz"] [])] THENL
  [soby ["aExists"; "sxy"] []; 
  soby ["aExists"; "sxy"] [];
  soby ["aExists"; "sxyz"] [];
  soby ["aExists"; "sxyz"; "xLESSy"; "antisym"; "yLESSz"] [];
  soby ["aExists"; "sxyz"; "yLESSz"; "antisym"; "xLESSy"] []]);;