src/FOL/ex/Nat2.ML
changeset 22822 c1a6a2159e69
parent 22821 15b2e7ec1f3b
child 22823 fa9ff469247f
     1.1 --- a/src/FOL/ex/Nat2.ML	Fri Apr 27 14:21:23 2007 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,159 +0,0 @@
     1.4 -(*  Title:      FOL/ex/nat2.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Tobias Nipkow
     1.7 -    Copyright   1991  University of Cambridge
     1.8 -*)
     1.9 -
    1.10 -Addsimps [pred_0, pred_succ, plus_0, plus_succ,
    1.11 -          nat_distinct1, nat_distinct2, succ_inject,
    1.12 -          leq_0, leq_succ_succ, leq_succ_0,
    1.13 -          lt_0_succ, lt_succ_succ, lt_0];
    1.14 -
    1.15 -
    1.16 -val prems = goal (the_context ())
    1.17 -    "[| P(0);  !!x. P(succ(x)) |] ==> All(P)";
    1.18 -by (rtac nat_ind 1);
    1.19 -by (REPEAT (resolve_tac (prems@[allI,impI]) 1));
    1.20 -qed "nat_exh";
    1.21 -
    1.22 -Goal "~ n=succ(n)";
    1.23 -by (IND_TAC nat_ind Simp_tac "n" 1);
    1.24 -result();
    1.25 -
    1.26 -Goal "~ succ(n)=n";
    1.27 -by (IND_TAC nat_ind Simp_tac "n" 1);
    1.28 -result();
    1.29 -
    1.30 -Goal "~ succ(succ(n))=n";
    1.31 -by (IND_TAC nat_ind Simp_tac "n" 1);
    1.32 -result();
    1.33 -
    1.34 -Goal "~ n=succ(succ(n))";
    1.35 -by (IND_TAC nat_ind Simp_tac "n" 1);
    1.36 -result();
    1.37 -
    1.38 -Goal "m+0 = m";
    1.39 -by (IND_TAC nat_ind Simp_tac "m" 1);
    1.40 -qed "plus_0_right";
    1.41 -
    1.42 -Goal "m+succ(n) = succ(m+n)";
    1.43 -by (IND_TAC nat_ind Simp_tac "m" 1);
    1.44 -qed "plus_succ_right";
    1.45 -
    1.46 -Addsimps [plus_0_right, plus_succ_right];
    1.47 -
    1.48 -Goal "~n=0 --> m+pred(n) = pred(m+n)";
    1.49 -by (IND_TAC nat_ind Simp_tac "n" 1);
    1.50 -result();
    1.51 -
    1.52 -Goal "~n=0 --> succ(pred(n))=n";
    1.53 -by (IND_TAC nat_ind Simp_tac "n" 1);
    1.54 -result();
    1.55 -
    1.56 -Goal "m+n=0 <-> m=0 & n=0";
    1.57 -by (IND_TAC nat_ind Simp_tac "m" 1);
    1.58 -result();
    1.59 -
    1.60 -Goal "m <= n --> m <= succ(n)";
    1.61 -by (IND_TAC nat_ind Simp_tac "m" 1);
    1.62 -by (rtac (impI RS allI) 1);
    1.63 -by (ALL_IND_TAC nat_ind Simp_tac 1);
    1.64 -by (Fast_tac 1);
    1.65 -bind_thm("le_imp_le_succ", result() RS mp);
    1.66 -
    1.67 -Goal "n<succ(n)";
    1.68 -by (IND_TAC nat_ind Simp_tac "n" 1);
    1.69 -result();
    1.70 -
    1.71 -Goal "~ n<n";
    1.72 -by (IND_TAC nat_ind Simp_tac "n" 1);
    1.73 -result();
    1.74 -
    1.75 -Goal "m < n --> m < succ(n)";
    1.76 -by (IND_TAC nat_ind Simp_tac "m" 1);
    1.77 -by (rtac (impI RS allI) 1);
    1.78 -by (ALL_IND_TAC nat_ind Simp_tac 1);
    1.79 -by (Fast_tac 1);
    1.80 -result();
    1.81 -
    1.82 -Goal "m <= n --> m <= n+k";
    1.83 -by (IND_TAC nat_ind (simp_tac (simpset() addsimps [le_imp_le_succ]))
    1.84 -     "k" 1);
    1.85 -qed "le_plus";
    1.86 -
    1.87 -Goal "succ(m) <= n --> m <= n";
    1.88 -by (res_inst_tac [("x","n")]spec 1);
    1.89 -by (ALL_IND_TAC nat_exh (simp_tac (simpset() addsimps [le_imp_le_succ])) 1);
    1.90 -qed "succ_le";
    1.91 -
    1.92 -Goal "~m<n <-> n<=m";
    1.93 -by (IND_TAC nat_ind Simp_tac "n" 1);
    1.94 -by (rtac (impI RS allI) 1);
    1.95 -by (ALL_IND_TAC nat_ind Asm_simp_tac 1);
    1.96 -qed "not_less";
    1.97 -
    1.98 -Goal "n<=m --> ~m<n";
    1.99 -by (simp_tac (simpset() addsimps [not_less]) 1);
   1.100 -qed "le_imp_not_less";
   1.101 -
   1.102 -Goal "m<n --> ~n<=m";
   1.103 -by (cut_facts_tac [not_less] 1 THEN Fast_tac 1);
   1.104 -qed "not_le";
   1.105 -
   1.106 -Goal "m+k<=n --> m<=n";
   1.107 -by (IND_TAC nat_ind (K all_tac) "k" 1);
   1.108 -by (Simp_tac 1);
   1.109 -by (rtac (impI RS allI) 1);
   1.110 -by (Simp_tac 1);
   1.111 -by (REPEAT (resolve_tac [allI,impI] 1));
   1.112 -by (cut_facts_tac [succ_le] 1);
   1.113 -by (Fast_tac 1);
   1.114 -qed "plus_le";
   1.115 -
   1.116 -val prems = goal (the_context ()) "[| ~m=0;  m <= n |] ==> ~n=0";
   1.117 -by (cut_facts_tac prems 1);
   1.118 -by (REPEAT (etac rev_mp 1));
   1.119 -by (IND_TAC nat_exh Simp_tac "m" 1);
   1.120 -by (ALL_IND_TAC nat_exh Simp_tac 1);
   1.121 -qed "not0";
   1.122 -
   1.123 -Goal "a<=a' & b<=b' --> a+b<=a'+b'";
   1.124 -by (IND_TAC nat_ind (simp_tac (simpset() addsimps [le_plus])) "b" 1);
   1.125 -by (resolve_tac [impI RS allI] 1);
   1.126 -by (resolve_tac [allI RS allI] 1);
   1.127 -by (ALL_IND_TAC nat_exh Asm_simp_tac 1);
   1.128 -qed "plus_le_plus";
   1.129 -
   1.130 -Goal "i<=j --> j<=k --> i<=k";
   1.131 -by (IND_TAC nat_ind (K all_tac) "i" 1);
   1.132 -by (Simp_tac 1);
   1.133 -by (resolve_tac [impI RS allI] 1);
   1.134 -by (ALL_IND_TAC nat_exh Simp_tac 1);
   1.135 -by (rtac impI 1);
   1.136 -by (ALL_IND_TAC nat_exh Simp_tac 1);
   1.137 -by (Fast_tac 1);
   1.138 -qed "le_trans";
   1.139 -
   1.140 -Goal "i < j --> j <=k --> i < k";
   1.141 -by (IND_TAC nat_ind (K all_tac) "j" 1);
   1.142 -by (Simp_tac 1);
   1.143 -by (resolve_tac [impI RS allI] 1);
   1.144 -by (ALL_IND_TAC nat_exh Simp_tac 1);
   1.145 -by (ALL_IND_TAC nat_exh Simp_tac 1);
   1.146 -by (ALL_IND_TAC nat_exh Simp_tac 1);
   1.147 -by (Fast_tac 1);
   1.148 -qed "less_le_trans";
   1.149 -
   1.150 -Goal "succ(i) <= j <-> i < j";
   1.151 -by (IND_TAC nat_ind Simp_tac "j" 1);
   1.152 -by (resolve_tac [impI RS allI] 1);
   1.153 -by (ALL_IND_TAC nat_exh Asm_simp_tac 1);
   1.154 -qed "succ_le2";
   1.155 -
   1.156 -Goal "i<succ(j) <-> i=j | i<j";
   1.157 -by (IND_TAC nat_ind Simp_tac "j" 1);
   1.158 -by (ALL_IND_TAC nat_exh Simp_tac 1);
   1.159 -by (resolve_tac [impI RS allI] 1);
   1.160 -by (ALL_IND_TAC nat_exh Simp_tac 1);
   1.161 -by (Asm_simp_tac 1);
   1.162 -qed "less_succ";