src/HOL/Nat.ML

-(*  Title: 	HOL/nat
+(*  Title:      HOL/nat
     ID:         $Id$
-    Author: 	Tobias Nipkow, Cambridge University Computer Laboratory
+    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
 For nat.thy.  Type nat is defined as a set (Nat) over the type ind.
 *)
 

 qed "nat_induct";
 
 (*Perform induction on n. *)
 fun nat_ind_tac a i = 
     EVERY [res_inst_tac [("n",a)] nat_induct i,
-	   rename_last_tac a ["1"] (i+1)];
+           rename_last_tac a ["1"] (i+1)];
 
 (*A special form of induction for reasoning about m<n and m-n*)
 val prems = goal Nat.thy
     "[| !!x. P x 0;  \
 \       !!y. P 0 (Suc y);  \

 by (fast_tac (set_cs addIs [select_equality] addEs [Zero_neq_Suc]) 1);
 qed "nat_case_0";
 
 goalw Nat.thy [nat_case_def] "nat_case a f (Suc k) = f(k)";
 by (fast_tac (set_cs addIs [select_equality] 
-	               addEs [make_elim Suc_inject, Suc_neq_Zero]) 1);
+                       addEs [make_elim Suc_inject, Suc_neq_Zero]) 1);
 qed "nat_case_Suc";
 
 (** Introduction rules for 'pred_nat' **)
 
 goalw Nat.thy [pred_nat_def] "(n, Suc(n)) : pred_nat";

 
 goalw Nat.thy [wf_def] "wf(pred_nat)";
 by (strip_tac 1);
 by (nat_ind_tac "x" 1);
 by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, 
-			     make_elim Suc_inject]) 2);
+                             make_elim Suc_inject]) 2);
 by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, Zero_neq_Suc]) 1);
 qed "wf_pred_nat";
 
 
 (*** nat_rec -- by wf recursion on pred_nat ***)

 val major::prems = goalw Nat.thy [less_def]
     "[| i<k;  k=Suc(i) ==> P;  !!j. [| i<j;  k=Suc(j) |] ==> P \
 \    |] ==> P";
 by (rtac (major RS tranclE) 1);
 by (REPEAT_FIRST (bound_hyp_subst_tac ORELSE'
-		  eresolve_tac (prems@[pred_natE, Pair_inject])));
+                  eresolve_tac (prems@[pred_natE, Pair_inject])));
 by (rtac refl 1);
 qed "lessE";
 
 goal Nat.thy "~ n<0";
 by (rtac notI 1);

 by (fast_tac (HOL_cs addSDs [Suc_inject]) 1);
 qed "less_SucE";
 
 goal Nat.thy "(m < Suc(n)) = (m < n | m = n)";
 by (fast_tac (HOL_cs addSIs [lessI]
-		     addEs  [less_trans, less_SucE]) 1);
+                     addEs  [less_trans, less_SucE]) 1);
 qed "less_Suc_eq";
 
 val prems = goal Nat.thy "m<n ==> n ~= 0";
 by(res_inst_tac [("n","n")] natE 1);
 by(cut_facts_tac prems 1);

 by (rtac (prem RS rev_mp) 1);
 by (nat_ind_tac "n" 1);
 by (rtac impI 1);
 by (etac less_zeroE 1);
 by (fast_tac (HOL_cs addSIs [lessI RS less_SucI]
-	 	     addSDs [Suc_inject]
-		     addEs  [less_trans, lessE]) 1);
+                     addSDs [Suc_inject]
+                     addEs  [less_trans, lessE]) 1);
 qed "Suc_lessD";
 
 val [major,minor] = goal Nat.thy 
     "[| Suc(i)<k;  !!j. [| i<j;  k=Suc(j) |] ==> P \
 \    |] ==> P";

 by (fast_tac (HOL_cs addIs prems) 1);
 by (nat_ind_tac "n" 1);
 by (rtac impI 1);
 by (etac less_zeroE 1);
 by (fast_tac (HOL_cs addSIs [lessI]
-	 	     addSDs [Suc_inject]
-		     addEs  [less_trans, lessE]) 1);
+                     addSDs [Suc_inject]
+                     addEs  [less_trans, lessE]) 1);
 qed "Suc_mono";
 
 goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)";
 by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]);
 qed "Suc_less_eq";