Hi Felix, > 7) When using the compact way of writing proofs, e.g. > > let rewrite_x_lemma = prove > (`~(x:num=0) ==> ?n:num. x = n + 1`, > DISCH_TAC THEN (EXISTS_TAC `x - 1`) THEN ASM_SIMP_TAC[ARITH_RULE > `~(x=0) ==> x >= 1`;ARITH_RULE `x >= 1 ==> x - 1 + 1 = x`]);; > > is there a way to generate a "long form" of this with all intermediate > subgoals? Or would I have to rewrite the whole thing manually using g() and > e()?
I've been working on a mechanism to flatten HOL Light proofs into "g"s and "e"s and to package them up into a "prove" proof. I'm just tidying it up a little now. So I'll announce to the HOL list when it's ready to use (any week now). Mark. ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
