Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <26108-0@swan.cl.cam.ac.uk>; Wed, 29 Apr 1992 06:31:37 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA15053; Tue, 28 Apr 92 21:56:12 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from panther.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) id AA14699; Tue, 28 Apr 92 21:56:01 -0700 Received: from localhost by panther.cs.uidaho.edu with SMTP id AA04693 (5.65c/IDA-1.4.4 for info-hol@ted); Tue, 28 Apr 1992 22:00:27 -0700 Message-Id: <199204290500.AA04693@panther.cs.uidaho.edu> To: info-hol@edu.uidaho.cs.ted Subject: the joyce lemma: comparing PVS and HOL (with proposals ;-) Date: Tue, 28 Apr 92 22:00:26 -0700 From: Phil Windley X-Mts: smtp Recently, Jeff Joyce posted Shankar's proof (in PVS) of the "joyce lemma" to info-hol. Having compared EHDM to HOL a little when I was at NASA, I thought it would be fun to try to follow Shankar's proof in HOL and compare the level of proof effort. The results were quite interesting (at least from the HOL user's perspective). The first snag that I ran into was that HOL has no built in mechanism for conditional rewrites. This wasn't a problem, because I was able to cobble together a tactic in a few minutes that did what I wanted and simulated what was happening in PVS quite nicely. The second major difference was that case splitting in HOL splits into two subgoals with the case on the assumption list of one and the negation of the case on the assumption list of the other. The PVS approach is actually easier to use in many cases (where you don't want to rewrite using the negation, or resolve it with something else on the assumption list). Again, it was easy to put together a HOL tactic that did this. PVS essnetially does SUBGOAL_THEN "case term" ASSUME_TAC. These two issues were more proof style and I was happy I took the time to go through the proof since it gave me two new tools. I found that some of the difficulties of doing rewrites with conditional equalities were made easier by the inclusion of even this simple tactic. Certainly, a well heeled HOL user would have no problem writing this tactic, but having a built in tactic affects the proof style of novice users. ***** Here's a proposal ******** In this light I propose that conditional rewriting and positive case analysis be added as built-in's in HOL, not just libraries. This is important if we are to make these tools available to beginners. The third problem was more significant (in terms of time it took to solve). In most cases, when Shankar used (assert), I was able to come up with a one or two line HOL proof that did the same thing. In one case (joyce.1.1.1.1.1.2), however, my proof is about 25 lines long and uses 2 lemmas I'm fairly certain that PVS didn't have available to it (dealing with MOD). In discussing this with Shankar, it became clear that the reason PVS didn't need the complicated mathematics that I produced was that PVS is using integers (particularly in its subtraction lemmas). This meant that PVS did not have to establish two non-trivial conditions in order to use use the following lemma: |- !m n p. ((m - p) + (p - n) = m - n) The same lemma in HOL is |- !m n p. p <= m /\ n <= p ==> ((m - p) + (p - n) = m - n) and the two conditions added considerable proof effort. In one sense, Shankar really didn't prove the lemma that Jeff proposed since Jeff (by posing the problem in HOL) assumed that +, -, *, div, and mod were the operators defined on natural numbers, but PVS used the same symbols for different operations (defined on integers). The fact that PVS's "+:int # int -> int" operates on ":num: as well is due to PVS's use of subtypes and simplified the proof considerably. Timewise, following Shankar's proof was straightforward and after I had the conditional rewriting and case splitting figured out, probably took about an hour not counting the time I spent proving manually what (assert) did automatically. Here, I'd suppose that I spent several hours (hard to tell with all the interruptions ;-). I guess this is no surprise, it basically underscores what we've known for a long time: proving nasty little lemmas about multiplication, addition, and subtraction in HOL is no fun. The other side of the coin is that modulo the things (assert) can prove automatically, PVS and HOL required about the same amount of user intervention. This did surprise me a little. I'm going to include the proof script from HOL below. I've put the corresponding PVS scripts in comments, so that you can follow what I did in HOL and see how it compares to PVS. I assumed the same axioms that Shankar did in PVS plus two that I needed for the problem mentioned above. I wanted to compare the theorem provers, not prove the lemmas; so the axioms are there--apologies to all! Cheers, --phil-- system `/bin/rm joyce.th`;; new_theory `joyce`;; loadf `normalize`;; loadf `num_thms`;; load_parent `exp`;; load_library `reduce`;; let GEN_COND_REWRITE_TAC thms thm thl (asl,g) = let equality = (snd o strip_imp o snd o strip_forall o concl) thm in let lhs = is_eq equality => (fst o dest_eq o snd o strip_forall) equality | equality in let inst = find_match lhs g in let inst_thm = INST_TY_TERM inst (SPEC_ALL thm) in let new_sub_goal = (list_mk_conj o fst o strip_imp o concl) inst_thm in (SUBGOAL_THEN new_sub_goal (\x.REWRITE_TAC (thms@thl@[(REWRITE_RULE [x] inst_thm)]) THEN ASSUME_TAC x) THEN REWRITE_TAC (thms@thl) THEN REDUCE_TAC) (asl,g);; let COND_REWRITE_TAC = GEN_COND_REWRITE_TAC [GREATER;LESS_0;NOT_SUC;SUC_NOT;EXP_POS];; let POS_CASES_TAC = (C SUBGOAL_THEN) ASSUME_TAC;; %---------------------------------------------------------------- W A R N I N G ! new_axiom in use. ----------------------------------------------------------------% %---------------------------------------------------------------- DIV(a,(b:posnat)): RECURSIVE nat = (IF a>=b THEN 1+DIV(a-b, b) ELSE 0 ENDIF) BY (LAMBDA a,(b:posnat): a) MOD(a,(b:posnat)): RECURSIVE nat = (IF a>=b THEN MOD(a-b, b) ELSE a ENDIF) BY (LAMBDA a,(b:posnat): a) pow2(i): RECURSIVE posnat = (IF i>0 THEN 2*pow2(i-1) ELSE 1 ENDIF) BY (LAMBDA i: i) ----------------------------------------------------------------% let pow2 = new_axiom (`pow2`, "x > 0 ==> ((2 EXP x) = (2 * (2 EXP (x-1))))" );; %---------------------------------------------------------------- pow2_plus: LEMMA pow2(a+b) = pow2(a)*pow2(b) ----------------------------------------------------------------% let pow2_plus = new_axiom (`pow2_plus`, "2 EXP (a+b) = ((2 EXP a) * (2 EXP b))" );; %---------------------------------------------------------------- mod_bnd: LEMMA b>0 IMPLIES mod(a,b) 0 ==> ((a MOD b) < b)" );; %---------------------------------------------------------------- div_mod: LEMMA b > 0 IMPLIES mod(a, b) = a - div(a, b) * b ----------------------------------------------------------------% let div_mod = new_axiom (`div_mod`, "b > 0 ==> (a MOD b = (a - ((a DIV b) * b)))" );; %---------------------------------------------------------------- strong_ind: LEMMA pp(0) AND (FORALL j: (FORALL (i|i<=j) : pp(i)) IMPLIES pp(j+1)) IMPLIES pp(n) ----------------------------------------------------------------% let strong_ind = new_axiom (`strong_ind`, "! pp. (pp 0) /\ (!j .(!i. (i <= j) ==> (pp i)) ==> (pp (SUC j))) ==> !n.(pp n)" );; %---------------------------------------------------------------- div_div: LEMMA b>0 AND c>0 IMPLIES div(div(a, b),c) = div(a, b*c) ----------------------------------------------------------------% let div_div = new_axiom (`div_div`, "(b > 0) /\ (c > 0) ==> (((a DIV b) DIV c) = (a DIV (b * c)))" );; %---------------------------------------------------------------- both_sides: LEMMA x/=0 AND x*y = x*z IMPLIES y=z ----------------------------------------------------------------% let both_sides = new_axiom (`both_sides`, "~(x = 0) /\ ((x * y) = (x * z)) ==> (y = z)" );; %---------------------------------------------------------------- postimes: LEMMA x>0 AND y>0 IMPLIES x*y>0 ----------------------------------------------------------------% let postimes = new_axiom (`postimes`, "(x > 0) /\ (y > 0) ==> (x * y) > 0" );; %---------------------------------------------------------------- mod_prod: LEMMA b > 0 AND mod(a, b) = 0 IMPLIES mod(a * c, b) = 0 ----------------------------------------------------------------% let mod_prod = new_axiom (`mod_prod`, "(b > 0) /\ (a MOD b = 0) ==> ((a * c) MOD b = 0)" );; %---------------------------------------------------------------- plus_div: LEMMA c > 0 AND (mod(a, c) = 0 OR mod(b, c) = 0) IMPLIES div(a + b, c) = (div(a, c) + div(b, c)) ----------------------------------------------------------------% let plus_div = new_axiom (`plus_div`, "(c > 0) /\ ((a MOD c = 0) \/ (b MOD c = 0)) ==> ((a + b) DIV c = ((a DIV c) + (b DIV c)))" );; %---------------------------------------------------------------- times_div: LEMMA b > 0 AND mod(a, b) = 0 IMPLIES div(a * c, b) = div(a, b) * c ----------------------------------------------------------------% let times_div = new_axiom (`times_div`, "(b > 0) /\ (a MOD b = 0) ==> ((a * c) DIV b = (a DIV b) * c)" );; %---------------------------------------------------------------- minus_div: LEMMA c>0 AND a>=b AND (mod(a,c)=0 OR mod(b,c)=0) IMPLIES div(a-b,c) = (div(a,c) - div(b,c)) ----------------------------------------------------------------% let minus_div = new_axiom (`minus_div`, "(c > 0) /\ (a >= b) /\ ((a MOD c = 0) \/ (b MOD c = 0)) ==> ((a - b) DIV c = ((a DIV c) - (b DIV c)))" );; %---------------------------------------------------------------- div_pow2: LEMMA a>0 IMPLIES mod(pow2(a), 2) = 0 ----------------------------------------------------------------% let div_pow2 = new_axiom (`div_pow2`, "a > 0 ==> ((2 EXP a) MOD 2 = 0)" );; %---------------------------------------------------------------- These lemmas were necessary in HOL, but apparently not PVS ----------------------------------------------------------------% let mod_less_eq_id = new_axiom (`mod_less_eq_id`, "! k n . n > 0 ==> (k MOD n) <= k" );; let mod_mod_less_eq = new_axiom (`mod_mod_less_eq`, "! a b c . (0 < c) ==> ((a MOD b) <= (a MOD (b * c)))" );; %---------------------------------------------------------------- A few lemmas... ----------------------------------------------------------------% let division_lemma1 = let x1 = ASSUME "0 < n" in let x2 = MP (SPEC_ALL DIVISION) x1 in let x3 = CONJUNCT1 (SPEC_ALL x2) in let y1 = ASSUME "(k MOD n) <= k /\ (k MOD n) <= ((k DIV n) * n) + (k MOD n)" in let y2 = SPECL ["k MOD n";"k:num"; "((k DIV n) * n) + (k MOD n)"] CANCEL_SUB in let y3 = REWRITE_RULE [y1] (SYM_RULE y2) in DISCH_ALL (SYM_RULE (REWRITE_RULE [ADD_SUB] (EQ_MP y3 x3)));; let mult_lemma = SYM_RULE(SPEC "2" (CONJUNCT1 MULT));; let LESS_EQ_ADD_SYM = (ONCE_REWRITE_RULE [ADD_SYM] LESS_EQ_ADD);; let MONO_LESS_MULT_SYM = (ONCE_REWRITE_RULE [MULT_SYM] MONO_LESS_MULT);; %---------------------------------------------------------------- joyce: LEMMA i (((((2 EXP (n - i)) * (A * (B MOD (2 EXP i)))) + (C DIV (2 EXP i))) DIV 2) + (((B DIV (2 EXP i)) MOD 2) * (A * (2 EXP (n - 1)))) = ((2 EXP (n - (i + 1))) * (A * (B MOD (2 EXP (i + 1))))) + (C DIV (2 EXP (i + 1))))");; e( REPEAT GEN_TAC );; %---------------------------------------------------------------- Rule? (dsimp) Apply disjunctive simplification, this simplifies to: joyce : {-1} i!5 < n!4 |------- {1} div((pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5))), 2) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) ----------------------------------------------------------------% e( STRIP_TAC );; %---------------------------------------------------------------- Rule? (rewrite "plus_div") Rewriting using plus_div, this yields 2 subgoals: joyce.1 : [-1] i!5 < n!4 |------- {1} (div(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) + div(div(c!1, pow2(i!5)), 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) ----------------------------------------------------------------% e( COND_REWRITE_TAC plus_div [] );; rotate(1);; % HOL generates subgoals in reverse order of PVS % %---------------------------------------------------------------- Rule? (rewrite "div_div") Rewriting using div_div, this simplifies to: joyce.1 : [-1] i!5 < n!4 |------- {1} (div(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) ----------------------------------------------------------------% e( COND_REWRITE_TAC div_div [] );; %---------------------------------------------------------------- Rule? (assert (-1)) Invoking decision procedures, this simplifies to: joyce.1 : [-1] i!5 < n!4 |------- [1] (div(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) I can't see a change.... ----------------------------------------------------------------% %---------------------------------------------------------------- Rule? (rewrite "pow2") Rewriting using pow2, this simplifies to: joyce.1 : [-1] i!5 < n!4 |------- {1} (div(2 * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)), 2) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) ----------------------------------------------------------------% e( COND_REWRITE_TAC pow2 [] );; %---------------------------------------------------------------- prove the conditional obligation now ----------------------------------------------------------------% e( IMP_RES_TAC SUB_LESS_0 );; %---------------------------------------------------------------- Rule? (rewrite "times_div") Rewriting using times_div, this yields 2 subgoals: joyce.1.1 : [-1] i!5 < n!4 |------- {1} (div(2 * pow2((n!4 - i!5) - 1) * a!3, 2) * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) ----------------------------------------------------------------% e( COND_REWRITE_TAC times_div [] );; rotate(1);; %---------------------------------------------------------------- Rule? (rewrite "times_div") Rewriting using times_div, this yields 2 subgoals: joyce.1.1.1 : [-1] i!5 < n!4 |------- {1} (div(2 * pow2((n!4 - i!5) - 1), 2) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (rewrite "times_div") Rewriting using times_div, this yields 2 subgoals: joyce.1.1.1.1 : [-1] i!5 < n!4 |------- {1} (div(2, 2) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) ----------------------------------------------------------------% e( COND_REWRITE_TAC times_div [MULT_CLAUSES] );; %---------------------------------------------------------------- Rule? (rewrite "div") Rewriting using div, this simplifies to: joyce.1.1.1.1 : [-1] i!5 < n!4 |------- {1} ((1 + div(2 - 2, 2)) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (rewrite "div") Rewriting using div, this simplifies to: joyce.1.1.1.1 : [-1] i!5 < n!4 |------- {1} ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (case "pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1))*pow2(i!5)") Case splitting on pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1))*pow2(i!5) this yields 4 subgoals: joyce.1.1.1.1.1 : {-1} pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) [-2] i!5 < n!4 |------- [1] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) ----------------------------------------------------------------% e( POS_CASES_TAC "2 EXP (n-1) = ((2 EXP (n-(i+1))) * (2 EXP i))" );; %---------------------------------------------------------------- Rule? (replace -1) Replacing using formula -1, this simplifies to: joyce.1.1.1.1.1 : [-1] pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) [-2] i!5 < n!4 |------- {1} ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - (i!5 + 1)) * pow2(i!5) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (delete (-1)) this simplifies to: joyce.1.1.1.1.1 : [-1] i!5 < n!4 |------- [1] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - (i!5 + 1)) * pow2(i!5) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) ----------------------------------------------------------------% rotate(1);; e( ASM_REWRITE_TAC [] );; %---------------------------------------------------------------- Rule? (case "mod(b!2, pow2(i!5 + 1)) = mod(b!2, pow2(i!5)) + pow2(i!5) * mod(div(b!2, pow2(i!5)), 2)") Case splitting on mod(b!2, pow2(i!5 + 1)) = mod(b!2, pow2(i!5)) + pow2(i!5) * mod(div(b!2, pow2(i!5)), 2) this yields 3 subgoals: joyce.1.1.1.1.1.1 : {-1} mod(b!2, pow2(i!5 + 1)) = mod(b!2, pow2(i!5)) + pow2(i!5) * mod(div(b!2, pow2(i!5)), 2) [-2] i!5 < n!4 |------- [1] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - (i!5 + 1)) * pow2(i!5) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) ----------------------------------------------------------------% e( POS_CASES_TAC "B MOD (2 EXP (i+1)) = ((B MOD (2 EXP i)) + ((2 EXP i) * ((B DIV (2 EXP i)) MOD 2)))" );; %---------------------------------------------------------------- Rule? (replace -1) Replacing using formula -1, this simplifies to: joyce.1.1.1.1.1.1 : [-1] mod(b!2, pow2(i!5 + 1)) = mod(b!2, pow2(i!5)) + pow2(i!5) * mod(div(b!2, pow2(i!5)), 2) [-2] i!5 < n!4 |------- {1} ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - (i!5 + 1)) * pow2(i!5) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * (mod(b!2, pow2(i!5)) + pow2(i!5) * mod(div(b!2, pow2(i!5)), 2)) + div(c!1, pow2(i!5 + 1)) Rule? (delete (-1)) this simplifies to: joyce.1.1.1.1.1.1 : [-1] i!5 < n!4 |------- [1] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - (i!5 + 1)) * pow2(i!5) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * (mod(b!2, pow2(i!5)) + pow2(i!5) * mod(div(b!2, pow2(i!5)), 2)) + div(c!1, pow2(i!5 + 1)) ----------------------------------------------------------------% rotate(1);; e( ASM_REWRITE_TAC [] );; %---------------------------------------------------------------- Rule? (rewrite "pow2" + ("i" "i!5+1")) Rewriting using pow2, this simplifies to: joyce.1.1.1.1.1.1 : [-1] i!5 < n!4 |------- {1} ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - (i!5 + 1)) * pow2(i!5) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * (mod(b!2, pow2(i!5)) + pow2(i!5) * mod(div(b!2, pow2(i!5)), 2)) + div(c!1, 2 * pow2((i!5 + 1) - 1)) ----------------------------------------------------------------% e( COND_REWRITE_TAC (SPEC "i+1" pow2) [] );; %---------------------------------------------------------------- this proves the conditional obligation ----------------------------------------------------------------% e( REWRITE_TAC [(SYM_RULE ADD1);GREATER;LESS_0] );; %---------------------------------------------------------------- Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.1.1.1.1.1. ----------------------------------------------------------------% e( REWRITE_TAC [ADD_SUB;MULT_CLAUSES;ADD_CLAUSES;SUB_PLUS; LEFT_ADD_DISTRIB;RIGHT_ADD_DISTRIB] THEN NORMALIZE_TAC THEN NORMALIZE_TAC );; %---------------------------------------------------------------- joyce.1.1.1.1.1.2 : [-1] i!5 < n!4 |------- {1} mod(b!2, pow2(i!5 + 1)) = mod(b!2, pow2(i!5)) + pow2(i!5) * mod(div(b!2, pow2(i!5)), 2) [2] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - (i!5 + 1)) * pow2(i!5) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (delete (2)) this simplifies to: joyce.1.1.1.1.1.2 : [-1] i!5 < n!4 |------- [1] mod(b!2, pow2(i!5 + 1)) = mod(b!2, pow2(i!5)) + pow2(i!5) * mod(div(b!2, pow2(i!5)), 2) Rule? (rewrite "div_mod") Rewriting using div_mod, this simplifies to: joyce.1.1.1.1.1.2 : [-1] i!5 < n!4 |------- {1} b!2 - div(b!2, pow2(i!5 + 1)) * pow2(i!5 + 1) = mod(b!2, pow2(i!5)) + pow2(i!5) * mod(div(b!2, pow2(i!5)), 2) ----------------------------------------------------------------% e( COND_REWRITE_TAC div_mod [] );; %---------------------------------------------------------------- Rule? (rewrite "div_mod") Rewriting using div_mod, this simplifies to: joyce.1.1.1.1.1.2 : [-1] i!5 < n!4 |------- {1} b!2 - div(b!2, pow2(i!5 + 1)) * pow2(i!5 + 1) = b!2 - div(b!2, pow2(i!5)) * pow2(i!5) + pow2(i!5) * mod(div(b!2, pow2(i!5)), 2) ----------------------------------------------------------------% e( COND_REWRITE_TAC div_mod [] );; %---------------------------------------------------------------- Rule? (rewrite "div_mod") Rewriting using div_mod, this simplifies to: joyce.1.1.1.1.1.2 : [-1] i!5 < n!4 |------- {1} b!2 - div(b!2, pow2(i!5 + 1)) * pow2(i!5 + 1) = b!2 - div(b!2, pow2(i!5)) * pow2(i!5) + pow2(i!5) * (div(b!2, pow2(i!5)) - div(div(b!2, pow2(i!5)), 2) * 2) ----------------------------------------------------------------% e( COND_REWRITE_TAC div_mod [] );; %---------------------------------------------------------------- Rule? (rewrite "div_div") Rewriting using div_div, this simplifies to: joyce.1.1.1.1.1.2 : [-1] i!5 < n!4 |------- {1} b!2 - div(b!2, pow2(i!5 + 1)) * pow2(i!5 + 1) = b!2 - div(b!2, pow2(i!5)) * pow2(i!5) + pow2(i!5) * (div(b!2, pow2(i!5)) - div(b!2, pow2(i!5) * 2) * 2) ----------------------------------------------------------------% e( COND_REWRITE_TAC div_div [] );; %---------------------------------------------------------------- Rule? (rewrite "pow2") Rewriting using pow2, this simplifies to: joyce.1.1.1.1.1.2 : [-1] i!5 < n!4 |------- {1} b!2 - div(b!2, 2 * pow2((i!5 + 1) - 1)) * (2 * pow2((i!5 + 1) - 1)) = b!2 - div(b!2, pow2(i!5)) * pow2(i!5) + pow2(i!5) * (div(b!2, pow2(i!5)) - div(b!2, pow2(i!5) * 2) * 2) ----------------------------------------------------------------% e( COND_REWRITE_TAC pow2 [] );; %---------------------------------------------------------------- this proves the conditional obligation ----------------------------------------------------------------% e( REWRITE_TAC [(SYM_RULE ADD1);GREATER;LESS_0] );; %---------------------------------------------------------------- Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.1.1.1.1.2. ----------------------------------------------------------------% e( REWRITE_TAC [RIGHT_SUB_DISTRIB;LEFT_SUB_DISTRIB; SPEC "2 EXP i" MULT_SYM;ADD_SUB] THEN COND_REWRITE_TAC INV_SUB_ADD [] THEN NORMALIZE_TAC THEN CONJ_TAC THENL [ % first conj % COND_REWRITE_TAC division_lemma1 [SUB_LESS_EQ] THEN COND_REWRITE_TAC division_lemma1 [] THEN REWRITE_TAC [EXP_POS;LESS_EQ_ADD_SYM] THEN COND_REWRITE_TAC mod_less_eq_id [EXP_POS] ; % second conj % ONCE_REWRITE_TAC [SYM_RULE MULT_ASSOC] THEN ONCE_REWRITE_TAC [SPEC "2" MULT_SYM] THEN COND_REWRITE_TAC division_lemma1 [] THENL [ % conditional obligation % ONCE_REWRITE_TAC [mult_lemma] THEN REWRITE_TAC [EXP_POS;LESS_EQ_ADD_SYM] THEN COND_REWRITE_TAC MONO_LESS_MULT_SYM [] THEN IMP_RES_TAC GREATER THEN COND_REWRITE_TAC mod_less_eq_id [EXP_POS] THEN ONCE_REWRITE_TAC [mult_lemma] THEN COND_REWRITE_TAC MONO_LESS_MULT_SYM [] THEN IMP_RES_TAC GREATER ; % main lemma % ONCE_REWRITE_TAC [SYM_RULE MULT_ASSOC] THEN ONCE_REWRITE_TAC [SPEC "2" MULT_SYM] THEN COND_REWRITE_TAC division_lemma1 [EXP_POS;LESS_EQ_ADD_SYM] THENL [ % do the condition % COND_REWRITE_TAC mod_less_eq_id [EXP_POS] ; % back to the main show % COND_REWRITE_TAC LESS_EQ_SUB [] THEN ASM_REWRITE_TAC [] THEN COND_REWRITE_TAC mod_mod_less_eq [] ] ] ] );; %---------------------------------------------------------------- This was taken care of earlier... [-1] i!5 < n!4 |------- {1} 2 > 0 [2] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - (i!5 + 1)) * pow2(i!5) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (assert (1)) Invoking decision procedures, That completes the proof of joyce.1.1.1.1.1.3. That completes the proof of joyce.1.1.1.1.1. joyce.1.1.1.1.2 : [-1] i!5 < n!4 |------- {1} pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) [2] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) ----------------------------------------------------------------% %---------------------------------------------------------------- Rule? (lemma "pow2_plus" ("a" "n!4 - (i!5 + 1)" "b" "i!5")) Applying pow2_plus where a gets n!4 - (i!5 + 1) b gets i!5 this yields 2 subgoals: joyce.1.1.1.1.2.1 : {-1} pow2((n!4 - (i!5 + 1)) + i!5) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) [-2] i!5 < n!4 |------- [1] pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) [2] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (delete (2)) this simplifies to: joyce.1.1.1.1.2.1 : [-1] pow2((n!4 - (i!5 + 1)) + i!5) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) [-2] i!5 < n!4 |------- [1] pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) Rule? (replace -1) Replacing using formula -1, this simplifies to: joyce.1.1.1.1.2.1 : [-1] pow2((n!4 - (i!5 + 1)) + i!5) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) [-2] i!5 < n!4 |------- [1] pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) ----------------------------------------------------------------% e( REWRITE_TAC [(SYM_RULE (SPECL ["n-(i+1)"; "i:num"] pow2_plus)); SUB_PLUS] THEN COND_REWRITE_TAC SUB_ADD_SUB [] THENL [ % conditional obligation % IMP_RES_TAC GREATER THEN IMP_RES_TAC LESS_EQ THEN ASM_REWRITE_TAC [num_CONV "1"] ; % main lemma % COND_REWRITE_TAC SUB_ADD [] THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ ] );; %---------------------------------------------------------------- Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.1.1.1.2.1. joyce.1.1.1.1.2.2 : [-1] i!5 < n!4 |------- {1} (n!4 - (i!5 + 1)) >= 0 [2] pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) [3] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (delete (3)) this simplifies to: joyce.1.1.1.1.2.2 : [-1] i!5 < n!4 |------- [1] (n!4 - (i!5 + 1)) >= 0 [2] pow2(n!4 - 1) = pow2(n!4 - (i!5 + 1)) * pow2(i!5) Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.1.1.1.2.2. That completes the proof of joyce.1.1.1.1.2. joyce.1.1.1.1.3 : [-1] i!5 < n!4 |------- {1} (n!4 - (i!5 + 1)) >= 0 [2] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (delete (2)) this simplifies to: joyce.1.1.1.1.3 : [-1] i!5 < n!4 |------- [1] (n!4 - (i!5 + 1)) >= 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.1.1.1.3. joyce.1.1.1.1.4 : [-1] i!5 < n!4 |------- {1} (n!4 - 1) >= 0 [2] ((1 + 0) * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (delete (2)) this simplifies to: joyce.1.1.1.1.4 : [-1] i!5 < n!4 |------- [1] (n!4 - 1) >= 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.1.1.1.4. That completes the proof of joyce.1.1.1.1. joyce.1.1.1.2 : [-1] i!5 < n!4 |------- {1} mod(2, 2) = 0 [2] (div(2 * pow2((n!4 - i!5) - 1), 2) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (delete (2)) this simplifies to: joyce.1.1.1.2 : [-1] i!5 < n!4 |------- [1] mod(2, 2) = 0 Rule? (rewrite "mod") Rewriting using mod, this simplifies to: joyce.1.1.1.2 : [-1] i!5 < n!4 |------- {1} mod(2 - 2, 2) = 0 Rule? (rewrite "mod") Rewriting using mod, this simplifies to: joyce.1.1.1.2 : [-1] i!5 < n!4 |------- {1} 2 - 2 = 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.1.1.2. That completes the proof of joyce.1.1.1. joyce.1.1.2 : [-1] i!5 < n!4 |------- {1} mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 [2] (div(2 * pow2((n!4 - i!5) - 1) * a!3, 2) * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (delete (2)) this simplifies to: joyce.1.1.2 : [-1] i!5 < n!4 |------- [1] mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 ----------------------------------------------------------------% %---------------------------------------------------------------- Rule? (rewrite "mod_prod") Rewriting using mod_prod, this yields 2 subgoals: joyce.1.1.2.1 : [-1] i!5 < n!4 |------- {1} 0 = 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.1.2.1. joyce.1.1.2.2 : [-1] i!5 < n!4 |------- {1} mod(2, 2) = 0 [2] mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 Rule? (rewrite "mod") Rewriting using mod, this simplifies to: joyce.1.1.2.2 : [-1] i!5 < n!4 |------- {1} mod(2 - 2, 2) = 0 [2] mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 Rule? (rewrite "mod") Rewriting using mod, this simplifies to: joyce.1.1.2.2 : [-1] i!5 < n!4 |------- {1} 2 - 2 = 0 [2] mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.1.2.2. That completes the proof of joyce.1.1.2. That completes the proof of joyce.1.1. ----------------------------------------------------------------% e( COND_REWRITE_TAC mod_prod [] );; %---------------------------------------------------------------- This proof doesn't show up in the HOL proof... joyce.1.2 : [-1] i!5 < n!4 |------- {1} mod(2 * pow2((n!4 - i!5) - 1) * a!3, 2) = 0 [2] (div(2 * pow2((n!4 - i!5) - 1) * a!3 * mod(b!2, pow2(i!5)), 2) + div(c!1, pow2(i!5) * 2)) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (delete (2)) this simplifies to: joyce.1.2 : [-1] i!5 < n!4 |------- [1] mod(2 * pow2((n!4 - i!5) - 1) * a!3, 2) = 0 Rule? (rewrite "mod_prod") Rewriting using mod_prod, this yields 2 subgoals: joyce.1.2.1 : [-1] i!5 < n!4 |------- {1} 0 = 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.2.1. joyce.1.2.2 : [-1] i!5 < n!4 |------- {1} mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 [2] mod(2 * pow2((n!4 - i!5) - 1) * a!3, 2) = 0 Rule? (rewrite "mod_prod") Rewriting using mod_prod, this yields 2 subgoals: joyce.1.2.2.1 : [-1] i!5 < n!4 |------- {1} 0 = 0 [2] mod(2 * pow2((n!4 - i!5) - 1) * a!3, 2) = 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.2.2.1. joyce.1.2.2.2 : [-1] i!5 < n!4 |------- {1} mod(2, 2) = 0 [2] mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 [3] mod(2 * pow2((n!4 - i!5) - 1) * a!3, 2) = 0 Rule? (rewrite "mod") Rewriting using mod, this simplifies to: joyce.1.2.2.2 : [-1] i!5 < n!4 |------- {1} mod(2 - 2, 2) = 0 [2] mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 [3] mod(2 * pow2((n!4 - i!5) - 1) * a!3, 2) = 0 Rule? (rewrite "mod") Rewriting using mod, this simplifies to: joyce.1.2.2.2 : [-1] i!5 < n!4 |------- {1} 2 - 2 = 0 [2] mod(2 * pow2((n!4 - i!5) - 1), 2) = 0 [3] mod(2 * pow2((n!4 - i!5) - 1) * a!3, 2) = 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.1.2.2.2. That completes the proof of joyce.1.2.2. That completes the proof of joyce.1.2. That completes the proof of joyce.1. ----------------------------------------------------------------% %---------------------------------------------------------------- joyce.2 : [-1] i!5 < n!4 |------- {1} (mod(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) = 0 OR mod(div(c!1, pow2(i!5)), 2) = 0) [2] div((pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)) + div(c!1, pow2(i!5))), 2) + pow2(n!4 - 1) * a!3 * mod(div(b!2, pow2(i!5)), 2) = pow2(n!4 - (i!5 + 1)) * a!3 * mod(b!2, pow2(i!5 + 1)) + div(c!1, pow2(i!5 + 1)) Rule? (delete (2)) this simplifies to: joyce.2 : [-1] i!5 < n!4 |------- [1] (mod(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) = 0 OR mod(div(c!1, pow2(i!5)), 2) = 0) Rule? (dsimp) Apply disjunctive simplification, this simplifies to: joyce.2 : [-1] i!5 < n!4 |------- {1} mod(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) = 0 {2} mod(div(c!1, pow2(i!5)), 2) = 0 ----------------------------------------------------------------% %---------------------------------------------------------------- Rule? (rewrite "mod_prod") Rewriting using mod_prod, this yields 2 subgoals: joyce.2.1 : [-1] i!5 < n!4 |------- {1} 0 = 0 [2] mod(div(c!1, pow2(i!5)), 2) = 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.2.1. joyce.2.2 : [-1] i!5 < n!4 |------- {1} mod(pow2(n!4 - i!5) * a!3, 2) = 0 [2] mod(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) = 0 [3] mod(div(c!1, pow2(i!5)), 2) = 0 Rule? (rewrite "div_pow2") No matching instance for div_pow2 found. No change. joyce.2.2 : [-1] i!5 < n!4 |------- {1} mod(pow2(n!4 - i!5) * a!3, 2) = 0 [2] mod(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) = 0 [3] mod(div(c!1, pow2(i!5)), 2) = 0 Rule? (rewrite "mod_prod") Rewriting using mod_prod, this yields 2 subgoals: joyce.2.2.1 : [-1] i!5 < n!4 |------- {1} 0 = 0 [2] mod(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) = 0 [3] mod(div(c!1, pow2(i!5)), 2) = 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.2.2.1. joyce.2.2.2 : [-1] i!5 < n!4 |------- {1} mod(pow2(n!4 - i!5), 2) = 0 [2] mod(pow2(n!4 - i!5) * a!3, 2) = 0 [3] mod(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) = 0 [4] mod(div(c!1, pow2(i!5)), 2) = 0 ----------------------------------------------------------------% e( COND_REWRITE_TAC mod_prod [] );; %---------------------------------------------------------------- Rule? (rewrite "div_pow2") Rewriting using div_pow2, this simplifies to: joyce.2.2.2 : [-1] i!5 < n!4 |------- {1} 0 = 0 [2] mod(pow2(n!4 - i!5) * a!3, 2) = 0 [3] mod(pow2(n!4 - i!5) * a!3 * mod(b!2, pow2(i!5)), 2) = 0 [4] mod(div(c!1, pow2(i!5)), 2) = 0 Rule? (assert) Invoking decision procedures, That completes the proof of joyce.2.2.2. That completes the proof of joyce.2.2. That completes the proof of joyce.2. ----------------------------------------------------------------% e( COND_REWRITE_TAC div_pow2 [] THEN IMP_RES_TAC SUB_LESS_0 );; %---------------------------------------------------------------- Now for the script ----------------------------------------------------------------% TAC_PROOF(([], "!A B C n i. i < n ==> (((((2 EXP (n - i)) * (A * (B MOD (2 EXP i)))) + (C DIV (2 EXP i))) DIV 2) + (((B DIV (2 EXP i)) MOD 2) * (A * (2 EXP (n - 1)))) = ((2 EXP (n - (i + 1))) * (A * (B MOD (2 EXP (i + 1))))) + (C DIV (2 EXP (i + 1))))"), REPEAT GEN_TAC THEN STRIP_TAC THEN COND_REWRITE_TAC plus_div [] THENL [ COND_REWRITE_TAC mod_prod [] THEN COND_REWRITE_TAC div_pow2 [] THEN IMP_RES_TAC SUB_LESS_0 ; COND_REWRITE_TAC div_div [] THEN COND_REWRITE_TAC pow2 [] THENL [ % conditional obligation % IMP_RES_TAC SUB_LESS_0 ; COND_REWRITE_TAC times_div [] THENL [ COND_REWRITE_TAC mod_prod [] THEN COND_REWRITE_TAC mod_prod [] THEN COND_REWRITE_TAC div_pow2 [] THEN IMP_RES_TAC SUB_LESS_0 ; COND_REWRITE_TAC times_div [MULT_CLAUSES] THEN POS_CASES_TAC "2 EXP (n-1) = ((2 EXP (n-(i+1))) * (2 EXP i))" THENL [ REWRITE_TAC [(SYM_RULE (SPECL ["n-(i+1)"; "i:num"] pow2_plus)); SUB_PLUS] THEN COND_REWRITE_TAC SUB_ADD_SUB [] THENL [ % conditional obligation % IMP_RES_TAC GREATER THEN IMP_RES_TAC LESS_EQ THEN ASM_REWRITE_TAC [num_CONV "1"] ; % main lemma % COND_REWRITE_TAC SUB_ADD [] THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ ] ; ASM_REWRITE_TAC [] THEN POS_CASES_TAC "B MOD (2 EXP (i+1)) = ((B MOD (2 EXP i)) + ((2 EXP i) * ((B DIV (2 EXP i)) MOD 2)))" THENL [ COND_REWRITE_TAC div_mod [] THEN COND_REWRITE_TAC div_mod [] THEN COND_REWRITE_TAC div_mod [] THEN COND_REWRITE_TAC div_div [] THEN COND_REWRITE_TAC pow2 [] THENL [ % conditional obligation % REWRITE_TAC [(SYM_RULE ADD1);GREATER;LESS_0] ; REWRITE_TAC [RIGHT_SUB_DISTRIB;LEFT_SUB_DISTRIB; SPEC "2 EXP i" MULT_SYM;ADD_SUB] THEN COND_REWRITE_TAC INV_SUB_ADD [] THEN NORMALIZE_TAC THEN CONJ_TAC THENL [ % first conj % COND_REWRITE_TAC division_lemma1 [SUB_LESS_EQ] THEN COND_REWRITE_TAC division_lemma1 [] THEN REWRITE_TAC [LESS_EQ_ADD_SYM] THEN COND_REWRITE_TAC mod_less_eq_id [] ; % second conj % ONCE_REWRITE_TAC [SYM_RULE MULT_ASSOC] THEN ONCE_REWRITE_TAC [SPEC "2" MULT_SYM] THEN COND_REWRITE_TAC division_lemma1 [] THENL [ % conditional obligation % ONCE_REWRITE_TAC [mult_lemma] THEN REWRITE_TAC [LESS_EQ_ADD_SYM] THEN COND_REWRITE_TAC MONO_LESS_MULT_SYM [] THEN IMP_RES_TAC GREATER THEN COND_REWRITE_TAC mod_less_eq_id [] THEN ONCE_REWRITE_TAC [mult_lemma] THEN COND_REWRITE_TAC MONO_LESS_MULT_SYM [] THEN IMP_RES_TAC GREATER ; % main lemma % ONCE_REWRITE_TAC [SYM_RULE MULT_ASSOC] THEN ONCE_REWRITE_TAC [SPEC "2" MULT_SYM] THEN COND_REWRITE_TAC division_lemma1 [ONCE_REWRITE_RULE [ADD_SYM] LESS_EQ_ADD] THENL [ % do the condition % COND_REWRITE_TAC mod_less_eq_id [] ; % back to the main show % COND_REWRITE_TAC LESS_EQ_SUB [] THEN ASM_REWRITE_TAC [] THEN COND_REWRITE_TAC mod_mod_less_eq [] ] ] ] ] ; ASM_REWRITE_TAC [] THEN COND_REWRITE_TAC (SPEC "i+1" pow2) [] THENL [ % conditionial obligation % REWRITE_TAC [(SYM_RULE ADD1);GREATER;LESS_0] ; REWRITE_TAC [ADD_SUB;MULT_CLAUSES;ADD_CLAUSES;SUB_PLUS; LEFT_ADD_DISTRIB;RIGHT_ADD_DISTRIB] THEN NORMALIZE_TAC THEN NORMALIZE_TAC ] ] ] ] ] ] );;