Declaration of type 'nat' as a datatype (this allows usage of
authorberghofe
Fri Jul 24 13:34:59 1998 +0200 (1998-07-24)
changeset 5188633ec5f6c155
parent 5187 55f07169cf5f
child 5189 362e4d6213c5
Declaration of type 'nat' as a datatype (this allows usage of
exhaust_tac and induct_tac on type 'nat'). Moved some proofs
using natE from NatDef.ML to Nat.ML.
src/HOL/Nat.ML
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Nat.ML	Fri Jul 24 13:30:28 1998 +0200
     1.2 +++ b/src/HOL/Nat.ML	Fri Jul 24 13:34:59 1998 +0200
     1.3 @@ -4,6 +4,101 @@
     1.4      Copyright   1997 TU Muenchen
     1.5  *)
     1.6  
     1.7 +(** conversion rules for nat_rec **)
     1.8 +
     1.9 +val [nat_rec_0, nat_rec_Suc] = nat.recs;
    1.10 +
    1.11 +(*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
    1.12 +val prems = goal thy
    1.13 +    "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c";
    1.14 +by (simp_tac (simpset() addsimps prems) 1);
    1.15 +qed "def_nat_rec_0";
    1.16 +
    1.17 +val prems = goal thy
    1.18 +    "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)";
    1.19 +by (simp_tac (simpset() addsimps prems) 1);
    1.20 +qed "def_nat_rec_Suc";
    1.21 +
    1.22 +val [nat_case_0, nat_case_Suc] = nat.cases;
    1.23 +
    1.24 +Goal "n ~= 0 ==> EX m. n = Suc m";
    1.25 +by (exhaust_tac "n" 1);
    1.26 +by (REPEAT (Blast_tac 1));
    1.27 +qed "not0_implies_Suc";
    1.28 +
    1.29 +val prems = goal thy "m<n ==> n ~= 0";
    1.30 +by (exhaust_tac "n" 1);
    1.31 +by (cut_facts_tac prems 1);
    1.32 +by (ALLGOALS Asm_full_simp_tac);
    1.33 +qed "gr_implies_not0";
    1.34 +
    1.35 +Goal "(n ~= 0) = (0 < n)";
    1.36 +by (exhaust_tac "n" 1);
    1.37 +by (Blast_tac 1);
    1.38 +by (Blast_tac 1);
    1.39 +qed "neq0_conv";
    1.40 +AddIffs [neq0_conv];
    1.41 +
    1.42 +(*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
    1.43 +bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
    1.44 +
    1.45 +Goal "(~(0 < n)) = (n=0)";
    1.46 +by (rtac iffI 1);
    1.47 + by (etac swap 1);
    1.48 + by (ALLGOALS Asm_full_simp_tac);
    1.49 +qed "not_gr0";
    1.50 +Addsimps [not_gr0];
    1.51 +
    1.52 +Goal "m<n ==> 0 < n";
    1.53 +by (dtac gr_implies_not0 1);
    1.54 +by (Asm_full_simp_tac 1);
    1.55 +qed "gr_implies_gr0";
    1.56 +Addsimps [gr_implies_gr0];
    1.57 +
    1.58 +qed_goalw "Least_Suc" thy [Least_nat_def]
    1.59 + "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
    1.60 + (fn _ => [
    1.61 +        rtac select_equality 1,
    1.62 +        fold_goals_tac [Least_nat_def],
    1.63 +        safe_tac (claset() addSEs [LeastI]),
    1.64 +        rename_tac "j" 1,
    1.65 +        exhaust_tac "j" 1,
    1.66 +        Blast_tac 1,
    1.67 +        blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1,
    1.68 +        rename_tac "k n" 1,
    1.69 +        exhaust_tac "k" 1,
    1.70 +        Blast_tac 1,
    1.71 +        hyp_subst_tac 1,
    1.72 +        rewtac Least_nat_def,
    1.73 +        rtac (select_equality RS arg_cong RS sym) 1,
    1.74 +        Safe_tac,
    1.75 +        dtac Suc_mono 1,
    1.76 +        Blast_tac 1,
    1.77 +        cut_facts_tac [less_linear] 1,
    1.78 +        Safe_tac,
    1.79 +        atac 2,
    1.80 +        Blast_tac 2,
    1.81 +        dtac Suc_mono 1,
    1.82 +        Blast_tac 1]);
    1.83 +
    1.84 +qed_goal "nat_induct2" thy 
    1.85 +"[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n" (fn prems => [
    1.86 +        cut_facts_tac prems 1,
    1.87 +        rtac less_induct 1,
    1.88 +        exhaust_tac "n" 1,
    1.89 +         hyp_subst_tac 1,
    1.90 +         atac 1,
    1.91 +        hyp_subst_tac 1,
    1.92 +        exhaust_tac "nat" 1,
    1.93 +         hyp_subst_tac 1,
    1.94 +         atac 1,
    1.95 +        hyp_subst_tac 1,
    1.96 +        resolve_tac prems 1,
    1.97 +        dtac spec 1,
    1.98 +        etac mp 1,
    1.99 +        rtac (lessI RS less_trans) 1,
   1.100 +        rtac (lessI RS Suc_mono) 1]);
   1.101 +
   1.102  Goal "min 0 n = 0";
   1.103  by (rtac min_leastL 1);
   1.104  by (trans_tac 1);
     2.1 --- a/src/HOL/Nat.thy	Fri Jul 24 13:30:28 1998 +0200
     2.2 +++ b/src/HOL/Nat.thy	Fri Jul 24 13:34:59 1998 +0200
     2.3 @@ -6,21 +6,15 @@
     2.4  Nat is a partial order
     2.5  *)
     2.6  
     2.7 -Nat = NatDef +
     2.8 +Nat = NatDef + Inductive +
     2.9  
    2.10 -(*install 'automatic' induction tactic, pretending nat is a datatype
    2.11 -  except for induct_tac and exhaust_tac, everything is dummy*)
    2.12 +setup
    2.13 +  DatatypePackage.setup
    2.14  
    2.15 -MLtext {|
    2.16 -|> Dtype.add_datatype_info
    2.17 -("nat", {case_const = Bound 0, case_rewrites = [],
    2.18 -  constructors = [], induct_tac = nat_ind_tac,
    2.19 -  exhaustion = natE,
    2.20 -  exhaust_tac = fn v => (res_inst_tac [("n",v)] natE)
    2.21 -                        THEN_ALL_NEW (rotate_tac ~1),
    2.22 -  nchotomy = ProtoPure.flexpair_def, case_cong = ProtoPure.flexpair_def})
    2.23 -|}
    2.24 -
    2.25 +rep_datatype nat
    2.26 +  distinct "[[Suc_not_Zero, Zero_not_Suc]]"
    2.27 +  inject   "[[Suc_Suc_eq]]"
    2.28 +  induct   nat_induct
    2.29  
    2.30  instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
    2.31  instance nat :: linorder (nat_le_linear)