equal
deleted
inserted
replaced
7 |
7 |
8 (* ------------------------------------------------------------------------- *) |
8 (* ------------------------------------------------------------------------- *) |
9 (* Arithmetic extensions *) |
9 (* Arithmetic extensions *) |
10 (* ------------------------------------------------------------------------- *) |
10 (* ------------------------------------------------------------------------- *) |
11 |
11 |
12 goal Arith.thy |
12 Goal "[| p < n; n:nat|] ==> n~=p"; |
13 "!!m.[| p < n; n:nat|] ==> n~=p"; |
|
14 by (Fast_tac 1); |
13 by (Fast_tac 1); |
15 qed "gt_not_eq"; |
14 qed "gt_not_eq"; |
16 |
15 |
17 val succ_pred = prove_goal Arith.thy |
16 Goal "[|j:nat; i:nat|] ==> i < j --> succ(j #- 1) = j"; |
18 "!!i.[|j:nat; i:nat|] ==> i < j --> succ(j #- 1) = j" |
17 by (induct_tac "j" 1); |
19 (fn prems =>[(induct_tac "j" 1), |
18 by (Fast_tac 1); |
20 (Fast_tac 1), |
19 by (Asm_simp_tac 1); |
21 (Asm_simp_tac 1)]); |
20 qed "succ_pred"; |
22 |
21 |
23 goal Arith.thy |
22 Goal "[|succ(x)<n; n:nat; x:nat|] ==> x < n #- 1 "; |
24 "!!i.[|succ(x)<n; n:nat; x:nat|] ==> x < n #- 1 "; |
|
25 by (rtac succ_leE 1); |
23 by (rtac succ_leE 1); |
26 by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1); |
24 by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1); |
27 by (asm_simp_tac (simpset() addsimps [succ_pred]) 1); |
25 by (asm_simp_tac (simpset() addsimps [succ_pred]) 1); |
28 qed "lt_pred"; |
26 qed "lt_pred"; |
29 |
27 |
30 goal Arith.thy |
28 Goal "[|n < succ(x); p<n; p:nat; n:nat; x:nat|] ==> n #- 1 < x "; |
31 "!!i.[|n < succ(x); p<n; p:nat; n:nat; x:nat|] ==> n #- 1 < x "; |
|
32 by (rtac succ_leE 1); |
29 by (rtac succ_leE 1); |
33 by (asm_simp_tac (simpset() addsimps [succ_pred]) 1); |
30 by (asm_simp_tac (simpset() addsimps [succ_pred]) 1); |
34 qed "gt_pred"; |
31 qed "gt_pred"; |
35 |
32 |
36 |
33 |