system "date"; (* --------------------------------------------------------------------- *) (* Define the seventh example program: Bicycling multiplication. *) (* --------------------------------------------------------------------- *) g `^(||` program procedure pedal (;val n,m); global a,b,c; pre n*m + c = a*b; post c = a*b; calls pedal with n < 'n /\ m = 'm; calls coast with n < 'n /\ m < 'm; recurses with n < 'n; if n = 0 \/ m = 0 then skip else c := c + m; if n < m then coast(;n - 1,m - 1) else pedal(;n - 1,m) fi fi end procedure; procedure coast (;val n,m); global a,b,c; pre n*(m + 1) + c = a*b; post c = a*b; calls pedal with n = 'n /\ m = 'm; calls coast with n = 'n /\ m < 'm; recurses with m < 'm; c := c + n; if n < m then coast(;n,m - 1) else pedal(;n,m) fi end procedure; a := 7; b := 12; c := 0; pedal(;a,b) end program [ c = a*b ] `||)`; et(VCG_TAC); (* val print_vcg = ref true ; (* when true, causes tracing of the VCG's work. *) val print_subst = ref false; (* when true, causes tracing of substitutions. *) val debug_vcg = ref false; (* when true, causes deep tracing of the VCG.. *) val caching = ref true ; (* when true, causes caching of some theorems. *) val debug_cache = ref false; (* when true, causes deep tracing of the cache. *) val timing = ref false; (* when true, causes timing of the VCG's work. *) val new_graph = ref true ; (* when true, prints diagram of graph analysis. *) *) (* Timing for Sunrise version 6.2: CPU: usr: 26.609783 s sys: 0.287688 s gc: 1.245379 s tot: 28.142850 s *) (* Trace: - et(VCG_TAC); OK.. For procedure "pedal", By the skip rule, we have {c = a * b} skip {c = a * b} /r By the CALL rule, we have {((n - 1) * ((m - 1) + 1) + c = a * b /\ (n - 1 < 'n /\ m - 1 < 'm)) /\ (!n m a b c. c = a * b ==> c = a * b)} coast(;n - 1,m - 1) {c = a * b} /r By the CALL rule, we have {((n - 1) * m + c = a * b /\ (n - 1 < 'n /\ m = 'm)) /\ (!n m a b c. c = a * b ==> c = a * b)} pedal(;n - 1,m) {c = a * b} /r By the IF rule, we have {(n < m => ((n - 1) * ((m - 1) + 1) + c = a * b /\ (n - 1 < 'n /\ m - 1 < 'm)) /\ (!n m a b c. c = a * b ==> c = a * b) | ((n - 1) * m + c = a * b /\ (n - 1 < 'n /\ m = 'm)) /\ (!n m a b c. c = a * b ==> c = a * b))} if n < m then coast(;n - 1,m - 1) else pedal(;n - 1,m) fi {c = a * b} /r By the ASSIGN rule, we have {(n < m => ((n - 1) * ((m - 1) + 1) + (c + m) = a * b /\ (n - 1 < 'n /\ m - 1 < 'm)) /\ (!n m a b c. c = a * b ==> c = a * b) | ((n - 1) * m + (c + m) = a * b /\ (n - 1 < 'n /\ m = 'm)) /\ (!n m a b c. c = a * b ==> c = a * b))} c := c + m {(n < m => ((n - 1) * ((m - 1) + 1) + c = a * b /\ (n - 1 < 'n /\ m - 1 < 'm)) /\ (!n m a b c. c = a * b ==> c = a * b) | ((n - 1) * m + c = a * b /\ (n - 1 < 'n /\ m = 'm)) /\ (!n m a b c. c = a * b ==> c = a * b))} /r By the SEQ rule, we have {(n < m => ((n - 1) * ((m - 1) + 1) + (c + m) = a * b /\ (n - 1 < 'n /\ m - 1 < 'm)) /\ (!n m a b c. c = a * b ==> c = a * b) | ((n - 1) * m + (c + m) = a * b /\ (n - 1 < 'n /\ m = 'm)) /\ (!n m a b c. c = a * b ==> c = a * b))} c := c + m; if n < m then coast(;n - 1,m - 1) else pedal(;n - 1,m) fi {c = a * b} /r By the IF rule, we have {(n = 0 \/ m = 0 => c = a * b | (n < m => ((n - 1) * ((m - 1) + 1) + (c + m) = a * b /\ (n - 1 < 'n /\ m - 1 < 'm)) /\ (!n m a b c. c = a * b ==> c = a * b) | ((n - 1) * m + (c + m) = a * b /\ (n - 1 < 'n /\ m = 'm)) /\ (!n m a b c. c = a * b ==> c = a * b)))} if n = 0 \/ m = 0 then skip else c := c + m; if n < m then coast(;n - 1,m - 1) else pedal(;n - 1,m) fi fi {c = a * b} /r By precondition strengthening, we have {('n = n /\ ('m = m /\ ('a = a /\ ('b = b /\ ('c = c /\ true))))) /\ n * m + c = a * b} if n = 0 \/ m = 0 then skip else c := c + m; if n < m then coast(;n - 1,m - 1) else pedal(;n - 1,m) fi fi {c = a * b} /r with additional verification condition ('n = n /\ ('m = m /\ ('a = a /\ ('b = b /\ ('c = c /\ true))))) /\ n * m + c = a * b ==> (n = 0 \/ m = 0 => c = a * b | (n < m => ((n - 1) * ((m - 1) + 1) + (c + m) = a * b /\ (n - 1 < 'n /\ m - 1 < 'm)) /\ (!n m a b c. c = a * b ==> c = a * b) | ((n - 1) * m + (c + m) = a * b /\ (n - 1 < 'n /\ m = 'm)) /\ (!n m a b c. c = a * b ==> c = a * b))) For procedure "coast", By the CALL rule, we have {(n * ((m - 1) + 1) + c = a * b /\ (n = 'n /\ m - 1 < 'm)) /\ (!n m a b c. c = a * b ==> c = a * b)} coast(;n,m - 1) {c = a * b} /r By the CALL rule, we have {(n * m + c = a * b /\ (n = 'n /\ m = 'm)) /\ (!n m a b c. c = a * b ==> c = a * b)} pedal(;n,m) {c = a * b} /r By the IF rule, we have {(n < m => (n * ((m - 1) + 1) + c = a * b /\ (n = 'n /\ m - 1 < 'm)) /\ (!n m a b c. c = a * b ==> c = a * b) | (n * m + c = a * b /\ (n = 'n /\ m = 'm)) /\ (!n m a b c. c = a * b ==> c = a * b))} if n < m then coast(;n,m - 1) else pedal(;n,m) fi {c = a * b} /r By the ASSIGN rule, we have {(n < m => (n * ((m - 1) + 1) + (c + n) = a * b /\ (n = 'n /\ m - 1 < 'm)) /\ (!n m a b c. c = a * b ==> c = a * b) | (n * m + (c + n) = a * b /\ (n = 'n /\ m = 'm)) /\ (!n m a b c. c = a * b ==> c = a * b))} c := c + n {(n < m => (n * ((m - 1) + 1) + c = a * b /\ (n = 'n /\ m - 1 < 'm)) /\ (!n m a b c. c = a * b ==> c = a * b) | (n * m + c = a * b /\ (n = 'n /\ m = 'm)) /\ (!n m a b c. c = a * b ==> c = a * b))} /r By the SEQ rule, we have {(n < m => (n * ((m - 1) + 1) + (c + n) = a * b /\ (n = 'n /\ m - 1 < 'm)) /\ (!n m a b c. c = a * b ==> c = a * b) | (n * m + (c + n) = a * b /\ (n = 'n /\ m = 'm)) /\ (!n m a b c. c = a * b ==> c = a * b))} c := c + n; if n < m then coast(;n,m - 1) else pedal(;n,m) fi {c = a * b} /r By precondition strengthening, we have {('n = n /\ ('m = m /\ ('a = a /\ ('b = b /\ ('c = c /\ true))))) /\ n * (m + 1) + c = a * b} c := c + n; if n < m then coast(;n,m - 1) else pedal(;n,m) fi {c = a * b} /r with additional verification condition ('n = n /\ ('m = m /\ ('a = a /\ ('b = b /\ ('c = c /\ true))))) /\ n * (m + 1) + c = a * b ==> (n < m => (n * ((m - 1) + 1) + (c + n) = a * b /\ (n = 'n /\ m - 1 < 'm)) /\ (!n m a b c. c = a * b ==> c = a * b) | (n * m + (c + n) = a * b /\ (n = 'n /\ m = 'm)) /\ (!n m a b c. c = a * b ==> c = a * b)) Exploring the structure of the procedure call graph: Traversing the call graph back from the procedure pedal: pedal n < 'n | <-- pedal !n1 m1 a b c. n1 < n /\ m1 = m ==> n1 < 'n | Undiverted recursion verification condition for the path pedal->pedal: n * m + c = a * b /\ n = 'n ==> (!n1 m1 a b c. n1 < n /\ m1 = m ==> n1 < 'n) | <-- coast !n1 m1 a b c. n1 = n /\ m1 = m ==> n1 < 'n | <-- pedal !n1 m1 a b c. n1 < n /\ m1 < m ==> (!n2 m2 a b c. n2 = n1 /\ m2 = m1 ==> n2 < 'n) | Undiverted recursion verification condition for the path pedal->coast->pedal: n * m + c = a * b /\ n = 'n ==> (!n1 m1 a b c. n1 < n /\ m1 < m ==> (!n2 m2 a b c. n2 = n1 /\ m2 = m1 ==> n2 < 'n)) | <-- coast !n1 m1 a b c. n1 = n /\ m1 < m ==> (!n2 m2 a b c. n2 = n1 /\ m2 = m1 ==> n2 < 'n) | Diversion verification condition for the path coast->coast->pedal: (!n1 m1 a b c. n1 = n /\ m1 = m ==> n1 < 'n) ==> (!n1 m1 a b c. n1 = n /\ m1 < m ==> (!n2 m2 a b c. n2 = n1 /\ m2 = m1 ==> n2 < 'n)) Traversing the call graph back from the procedure coast: coast m < 'm | <-- pedal !n1 m1 a b c. n1 < n /\ m1 < m ==> m1 < 'm | <-- pedal !n1 m1 a b c. n1 < n /\ m1 = m ==> (!n2 m2 a b c. n2 < n1 /\ m2 < m1 ==> m2 < 'm) | Diversion verification condition for the path pedal->pedal->coast: (!n1 m1 a b c. n1 < n /\ m1 < m ==> m1 < 'm) ==> (!n1 m1 a b c. n1 < n /\ m1 = m ==> (!n2 m2 a b c. n2 < n1 /\ m2 < m1 ==> m2 < 'm)) | <-- coast !n1 m1 a b c. n1 = n /\ m1 = m ==> (!n2 m2 a b c. n2 < n1 /\ m2 < m1 ==> m2 < 'm) | Undiverted recursion verification condition for the path coast->pedal->coast: n * (m + 1) + c = a * b /\ m = 'm ==> (!n1 m1 a b c. n1 = n /\ m1 = m ==> (!n2 m2 a b c. n2 < n1 /\ m2 < m1 ==> m2 < 'm)) | <-- coast !n1 m1 a b c. n1 = n /\ m1 < m ==> m1 < 'm | Undiverted recursion verification condition for the path coast->coast: n * (m + 1) + c = a * b /\ m = 'm ==> (!n1 m1 a b c. n1 = n /\ m1 < m ==> m1 < 'm) For the main body, By the CALL rule, we have {(a * b + c = a * b /\ true) /\ (!n m a b c. c = a * b ==> c = a * b)} pedal(;a,b) {c = a * b} /r By the ASSIGN rule, we have {(a * b + 0 = a * b /\ true) /\ (!n m a b c. c = a * b ==> c = a * b)} c := 0 {(a * b + c = a * b /\ true) /\ (!n m a b c. c = a * b ==> c = a * b)} /r By the SEQ rule, we have {(a * b + 0 = a * b /\ true) /\ (!n m a b c. c = a * b ==> c = a * b)} c := 0; pedal(;a,b) {c = a * b} /r By the ASSIGN rule, we have {(a * 12 + 0 = a * 12 /\ true) /\ (!n m a b c. c = a * b ==> c = a * b)} b := 12 {(a * b + 0 = a * b /\ true) /\ (!n m a b c. c = a * b ==> c = a * b)} /r By the SEQ rule, we have {(a * 12 + 0 = a * 12 /\ true) /\ (!n m a b c. c = a * b ==> c = a * b)} b := 12; c := 0; pedal(;a,b) {c = a * b} /r By the ASSIGN rule, we have {(7 * 12 + 0 = 7 * 12 /\ true) /\ (!n m a b c. c = a * b ==> c = a * b)} a := 7 {(a * 12 + 0 = a * 12 /\ true) /\ (!n m a b c. c = a * b ==> c = a * b)} /r By the SEQ rule, we have {(7 * 12 + 0 = 7 * 12 /\ true) /\ (!n m a b c. c = a * b ==> c = a * b)} a := 7; b := 12; c := 0; pedal(;a,b) {c = a * b} /r By precondition strengthening, we have {true} a := 7; b := 12; c := 0; pedal(;a,b) {c = a * b} /r with additional verification condition true ==> (7 * 12 + 0 = 7 * 12 /\ true) /\ (!n m a b c. c = a * b ==> c = a * b) 9 subgoals: CPU: usr: 26.096071 s sys: 0.171775 s gc: 0.384534 s tot: 26.652380 s val it = (--`7 * 12 + 0 = 7 * 12`--) (--`!n m c a b 'm. (n * (m + 1) + c = a * b) /\ (m = 'm) ==> (!n1 m1. (n1 = n) /\ m1 < m ==> m1 < 'm)`--) (--`!n m c a b 'm. (n * (m + 1) + c = a * b) /\ (m = 'm) ==> (!n1 m1. (n1 = n) /\ (m1 = m) ==> (!n2 m2. n2 < n1 /\ m2 < m1 ==> m2 < 'm))`--) (--`!n m 'm. (!n1 m1. n1 < n /\ m1 < m ==> m1 < 'm) ==> (!n1 m1. n1 < n /\ (m1 = m) ==> (!n2 m2. n2 < n1 /\ m2 < m1 ==> m2 < 'm))`--) (--`!n m 'n. (!n1 m1. (n1 = n) /\ (m1 = m) ==> n1 < 'n) ==> (!n1 m1. (n1 = n) /\ m1 < m ==> (!n2 m2. (n2 = n1) /\ (m2 = m1) ==> n2 < 'n))`--) (--`!n m c a b 'n. (n * m + c = a * b) /\ (n = 'n) ==> (!n1 m1. n1 < n /\ m1 < m ==> (!n2 m2. (n2 = n1) /\ (m2 = m1) ==> n2 < 'n))`--) (--`!n m c a b 'n. (n * m + c = a * b) /\ (n = 'n) ==> (!n1 m1. n1 < n /\ (m1 = m) ==> n1 < 'n)`--) (--`!'n n 'm m 'a a 'b b 'c c. (('n = n) /\ ('m = m) /\ ('a = a) /\ ('b = b) /\ ('c = c)) /\ (n * (m + 1) + c = a * b) ==> ((n < m) => ((n * ((m - 1) + 1) + c + n = a * b) /\ (n = 'n) /\ m - 1 < 'm) | ((n * m + c + n = a * b) /\ (n = 'n) /\ (m = 'm)))`--) (--`!'n n 'm m 'a a 'b b 'c c. (('n = n) /\ ('m = m) /\ ('a = a) /\ ('b = b) /\ ('c = c)) /\ (n * m + c = a * b) ==> (((n = 0) \/ (m = 0)) => (c = a * b) | ((n < m) => (((n - 1) * ((m - 1) + 1) + c + m = a * b) /\ n - 1 < 'n /\ m - 1 < 'm) | (((n - 1) * m + c + m = a * b) /\ n - 1 < 'n /\ (m = 'm))))`--) : goalstack - *) (* 9 subgoals, of which 4 do not succumb immediately to decision procedures. *) (* These verification conditions are solved by the following tactics: *) (* 1st subgoal (body of pedal): *) et(REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN COND_CASES_TAC THENL [ POP_ASSUM DISJ_CASES_TAC THEN ASM_REWRITE_TAC[MULT_CLAUSES,ADD_CLAUSES], POP_ASSUM (STRIP_ASSUME_TAC o REWRITE_RULE[DE_MORGAN_THM]) THEN DISCH_THEN (REWRITE_THM o SYM) THEN COND_REWRITE_TAC[SUB_ADD] THEN SUBST1_TAC (EQT_ELIM (ARITH_CONV (--`c + m = m + c`--))) THEN REWRITE_TAC[ADD_ASSOC,ONCE_REWRITE_RULE[MULT_SYM] (ONCE_REWRITE_RULE[EQ_SYM_EQ] (ONCE_REWRITE_RULE[ADD_SYM] MULT_SUC))] THEN IMP_RES_THEN REWRITE_THM (EQT_ELIM (ARITH_CONV (--`~(n = 0) ==> (SUC (n - 1) = n)`--))) THEN UNDISCH_LAST_TAC THEN UNDISCH_LAST_TAC THEN ARITH_TAC ] ); (* Interactive version: e(REPEAT STRIP_TAC); e(POP_ASSUM (REWRITE_THM o SYM)); e(ASM_REWRITE_TAC[]); (* e(ARITH_TAC) handle e => (print_HOL_ERR e; raise e); *) e(COND_CASES_TAC); e(POP_ASSUM DISJ_CASES_TAC); e(ASM_REWRITE_TAC[MULT_CLAUSES,ADD_CLAUSES]); e(ASM_REWRITE_TAC[MULT_CLAUSES,ADD_CLAUSES]); e(POP_ASSUM (STRIP_ASSUME_TAC o REWRITE_RULE[DE_MORGAN_THM])); e(COND_REWRITE_TAC[SUB_ADD]); e(SUBST1_TAC (EQT_ELIM (ARITH_CONV (--`c + m = m + c`--)))); e(REWRITE_TAC[ADD_ASSOC,ONCE_REWRITE_RULE[MULT_SYM] (ONCE_REWRITE_RULE[EQ_SYM_EQ] (ONCE_REWRITE_RULE[ADD_SYM] MULT_SUC))]); e(IMP_RES_THEN REWRITE_THM (EQT_ELIM (ARITH_CONV (--`~(n = 0) ==> (SUC (n - 1) = n)`--)))); e(UNDISCH_LAST_TAC); e(UNDISCH_LAST_TAC); e(ARITH_TAC) handle e => (print_HOL_ERR e; raise e); *) (* 2nd subgoal (body of coast): *) et(REPEAT STRIP_TAC THEN POP_ASSUM (REWRITE_THM o SYM) THEN ASM_REWRITE_TAC[] THEN COND_CASES_TAC THEN COND_REWRITE_TAC[SUB_ADD] THEN REWRITE_TAC[GSYM ADD1,MULT_CLAUSES] THEN UNDISCH_LAST_TAC THEN ARITH_TAC ); (* Interactive version: e(REPEAT STRIP_TAC); e(POP_ASSUM (REWRITE_THM o SYM)); e(ASM_REWRITE_TAC[]); (* e(ARITH_TAC) handle e => (print_HOL_ERR e; raise e); *) e(COND_CASES_TAC); e(COND_REWRITE_TAC[SUB_ADD]); e(REWRITE_TAC[GSYM ADD1,MULT_CLAUSES]); e(UNDISCH_LAST_TAC); e(ARITH_TAC) handle e => (print_HOL_ERR e; raise e); e(REWRITE_TAC[GSYM ADD1,MULT_CLAUSES]); e(UNDISCH_LAST_TAC); e(ARITH_TAC) handle e => (print_HOL_ERR e; raise e); *) (* 3rd subgoal (undiverted recursion vc for coast -> coast): *) e(ARITH_TAC); (* 4th subgoal (undiverted recursion vc for coast -> pedal -> coast: *) e(ARITH_TAC); (* 5th subgoal (diversion vc for pedal -> pedal -> coast): *) et(REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN EXISTS_TAC (--`m:num`--) THEN ASM_REWRITE_TAC[]); (* Interactive version: e(REPEAT STRIP_TAC); e(FIRST_ASSUM MATCH_MP_TAC); e(EXISTS_TAC (--`m:num`--)); e(ASM_REWRITE_TAC[]); *) (* 6th subgoal (diversion vc for coast -> coast -> pedal): *) et(ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN EXISTS_TAC (--`n1:num`--) THEN ASM_REWRITE_TAC[]); (* Interactive version: e(ONCE_REWRITE_TAC[EQ_SYM_EQ]); e(REPEAT STRIP_TAC); e(FIRST_ASSUM MATCH_MP_TAC); e(EXISTS_TAC (--`n1:num`--)); e(ASM_REWRITE_TAC[]); *) (* 7th subgoal (undiverted recursion vc for pedal -> coast -> pedal): *) e(ARITH_TAC); (* 8th subgoal (undiverted recursion vc for pedal -> pedal): *) e(ARITH_TAC); (* 9th subgoal (main body): *) e(ARITH_TAC); val bicycling = top_thm(); (* theorem: val bicycling = |- program procedure pedal(var ;val n,m); global a,b,c; pre n * m + c = a * b; post c = a * b; calls pedal with n < 'n /\ m = 'm; calls coast with n < 'n /\ m < 'm; recurses with n < 'n; if n = 0 \/ m = 0 then skip else c := c + m; if n < m then coast(;n - 1,m - 1) else pedal(;n - 1,m) fi fi end procedure; procedure coast(var ;val n,m); global a,b,c; pre n * (m + 1) + c = a * b; post c = a * b; calls pedal with n = 'n /\ m = 'm; calls coast with n = 'n /\ m < 'm; recurses with m < 'm; c := c + n; if n < m then coast(;n,m - 1) else pedal(;n,m) fi end procedure; a := 7; b := 12; c := 0; pedal(;a,b) end program [c = a * b] : thm *)