equal
deleted
inserted
replaced
18 |
18 |
19 |
19 |
20 (** Prove the termination condition and remove it from the recursion equations |
20 (** Prove the termination condition and remove it from the recursion equations |
21 and induction rule **) |
21 and induction rule **) |
22 |
22 |
23 Tfl.tgoalw thy [] gcd.rules; |
23 Tfl.tgoalw thy [] gcd.simps; |
24 by (simp_tac (simpset() addsimps [mod_less_divisor]) 1); |
24 by (simp_tac (simpset() addsimps [mod_less_divisor]) 1); |
25 val tc = result(); |
25 val tc = result(); |
26 |
26 |
27 val gcd_eq = tc RS hd gcd.rules; |
27 val gcd_eq = tc RS hd gcd.simps; |
28 |
28 |
29 val prems = goal thy |
29 val prems = goal thy |
30 "[| !!m. P m 0; \ |
30 "[| !!m. P m 0; \ |
31 \ !!m n. [| 0<n; P n (m mod n) |] ==> P m n \ |
31 \ !!m n. [| 0<n; P n (m mod n) |] ==> P m n \ |
32 \ |] ==> P m n"; |
32 \ |] ==> P m n"; |