# HG changeset patch # User berghofe # Date 901280099 -7200 # Node ID 633ec5f6c1554dd6110d962135a54e0b2f255c50 # Parent 55f07169cf5f6284af47508625b888ae0302f7bd 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. diff -r 55f07169cf5f -r 633ec5f6c155 src/HOL/Nat.ML --- a/src/HOL/Nat.ML Fri Jul 24 13:30:28 1998 +0200 +++ b/src/HOL/Nat.ML Fri Jul 24 13:34:59 1998 +0200 @@ -4,6 +4,101 @@ Copyright 1997 TU Muenchen *) +(** conversion rules for nat_rec **) + +val [nat_rec_0, nat_rec_Suc] = nat.recs; + +(*These 2 rules ease the use of primitive recursion. NOTE USE OF == *) +val prems = goal thy + "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c"; +by (simp_tac (simpset() addsimps prems) 1); +qed "def_nat_rec_0"; + +val prems = goal thy + "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)"; +by (simp_tac (simpset() addsimps prems) 1); +qed "def_nat_rec_Suc"; + +val [nat_case_0, nat_case_Suc] = nat.cases; + +Goal "n ~= 0 ==> EX m. n = Suc m"; +by (exhaust_tac "n" 1); +by (REPEAT (Blast_tac 1)); +qed "not0_implies_Suc"; + +val prems = goal thy "m n ~= 0"; +by (exhaust_tac "n" 1); +by (cut_facts_tac prems 1); +by (ALLGOALS Asm_full_simp_tac); +qed "gr_implies_not0"; + +Goal "(n ~= 0) = (0 < n)"; +by (exhaust_tac "n" 1); +by (Blast_tac 1); +by (Blast_tac 1); +qed "neq0_conv"; +AddIffs [neq0_conv]; + +(*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0 0 < n"; +by (dtac gr_implies_not0 1); +by (Asm_full_simp_tac 1); +qed "gr_implies_gr0"; +Addsimps [gr_implies_gr0]; + +qed_goalw "Least_Suc" thy [Least_nat_def] + "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" + (fn _ => [ + rtac select_equality 1, + fold_goals_tac [Least_nat_def], + safe_tac (claset() addSEs [LeastI]), + rename_tac "j" 1, + exhaust_tac "j" 1, + Blast_tac 1, + blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1, + rename_tac "k n" 1, + exhaust_tac "k" 1, + Blast_tac 1, + hyp_subst_tac 1, + rewtac Least_nat_def, + rtac (select_equality RS arg_cong RS sym) 1, + Safe_tac, + dtac Suc_mono 1, + Blast_tac 1, + cut_facts_tac [less_linear] 1, + Safe_tac, + atac 2, + Blast_tac 2, + dtac Suc_mono 1, + Blast_tac 1]); + +qed_goal "nat_induct2" thy +"[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n" (fn prems => [ + cut_facts_tac prems 1, + rtac less_induct 1, + exhaust_tac "n" 1, + hyp_subst_tac 1, + atac 1, + hyp_subst_tac 1, + exhaust_tac "nat" 1, + hyp_subst_tac 1, + atac 1, + hyp_subst_tac 1, + resolve_tac prems 1, + dtac spec 1, + etac mp 1, + rtac (lessI RS less_trans) 1, + rtac (lessI RS Suc_mono) 1]); + Goal "min 0 n = 0"; by (rtac min_leastL 1); by (trans_tac 1); diff -r 55f07169cf5f -r 633ec5f6c155 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Fri Jul 24 13:30:28 1998 +0200 +++ b/src/HOL/Nat.thy Fri Jul 24 13:34:59 1998 +0200 @@ -6,21 +6,15 @@ Nat is a partial order *) -Nat = NatDef + +Nat = NatDef + Inductive + -(*install 'automatic' induction tactic, pretending nat is a datatype - except for induct_tac and exhaust_tac, everything is dummy*) +setup + DatatypePackage.setup -MLtext {| -|> Dtype.add_datatype_info -("nat", {case_const = Bound 0, case_rewrites = [], - constructors = [], induct_tac = nat_ind_tac, - exhaustion = natE, - exhaust_tac = fn v => (res_inst_tac [("n",v)] natE) - THEN_ALL_NEW (rotate_tac ~1), - nchotomy = ProtoPure.flexpair_def, case_cong = ProtoPure.flexpair_def}) -|} - +rep_datatype nat + distinct "[[Suc_not_Zero, Zero_not_Suc]]" + inject "[[Suc_Suc_eq]]" + induct nat_induct instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le) instance nat :: linorder (nat_le_linear)