Hello Bill, On 01/01/2013 08:08, Bill Richter wrote: > Is there any easy HOL 1-line way to state a result t, prove it, then use for > some purpose?
Apart from SUBGOAL_THEN you can also: 1) Use SUBGOAL_TAC. 2) Use a 'prove' command inline, then use the resulting theorem for any purpose. These two alternatives allow you to prove your subgoal immediately and then use it whichever way you want. (Very) trivial example: g `a:num = a`;; e (SUBGOAL_THEN `!x:num. x = x` MATCH_ACCEPT_TAC);; e (GEN_TAC THEN REFL_TAC);; You can also: g `a:num = a`;; e (SUBGOAL_TAC "label" `!x:num. x = x` [GEN_TAC THEN REFL_TAC]);; e (USE_THEN "label" MATCH_ACCEPT_TAC);; Or: g `a:num = a`;; e (MATCH_ACCEPT_TAC (prove (`!x:num. x = x`, GEN_TAC THEN REFL_TAC)));; > let cases (lab,t) tac = > SUBGOAL_THEN t MP_TAC THENL [tac; ALL_TAC] THEN > DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN (LABEL_TAC lab));; > > Tell me if this is right: SUBGOAL_THEN is normally used with ASSUME_TAC, but > not always, and here if the first goal is g, then > SUBGOAL_THEN t MP_TAC > makes the first and second goals > t and t ==> g > THENL applies tac to prove t, and does nothing to t ==> g. > Then DISCH_THEN pulls off the antecedent t, and DISJ_CASES_THEN breaks the > disjunction t, and then LABEL_TAC gives each disjunct the same label lab, > which is fine, because the different disjuncts have different goals and so > there's no conflict between the the different copies of the label lab. You have got this right. > > That's nice code, but I wondered if we could avoid the MP_TAC/DISCH_THEN > routine, as Ramana, Petros and Michael taught me was sometimes possible. In theory, you could use replace MP_TAC with (REPEAT_TCL DISJ_CASES_THEN (LABEL_TAC lab)) - or whichever tactic you wish to apply to your new assumpion. The problem if you do this is that DISJ_CASES_THEN will create two new subgoals (for a total of three). eg.: g `P:bool`;; Warning: Free variables in goal: P val it : goalstack = 1 subgoal (1 total) `P` # e (SUBGOAL_THEN `p:bool = T \/ p:bool = F` (DISJ_CASES_THEN (LABEL_TAC "case")));; val it : goalstack = 3 subgoals (3 total) 0 [`p <=> F`] (case) `P` 0 [`p <=> T`] (case) `P` `(p <=> T) \/ (p <=> F)` Since t can have multiple disjuncts, the number of generated subgoals is arbitrary. This makes things complicated for THENL because the list of tactics in its argument must be the same size as the number of subgoals (so as to provide one tactic for each subgoal). Using MP_TAC/DISCH_THEN solves this problem and makes the "cases" work for any t. As far as I can think right now, the best alternatives if you want to avoid the MP_TAC/DISCH_THEN combination are the ones I gave in the beginning. (Note that, as far as I can tell, "cases" assumes tac will prove t.) Regards, Petros -- Petros Papapanagiotou CISA, School of Informatics The University of Edinburgh Email: [email protected] --- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ------------------------------------------------------------------------------ Master SQL Server Development, Administration, T-SQL, SSAS, SSIS, SSRS and more. Get SQL Server skills now (including 2012) with LearnDevNow - 200+ hours of step-by-step video tutorials by Microsoft MVPs and experts. SALE $99.99 this month only - learn more at: http://p.sf.net/sfu/learnmore_122512 _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
