Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/FOL/ex/nat2.ML
changeset 0 a5a9c433f639 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/nat2.ML	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,163 @@
+(*  Title: 	FOL/ex/nat2.ML
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1991  University of Cambridge
+
+For ex/nat.thy.  
+Examples of simplification and induction on the natural numbers
+*)
+
+open Nat2;
+
+val nat_rews = [pred_0, pred_succ, plus_0, plus_succ, 
+		    nat_distinct1, nat_distinct2, succ_inject,
+		    leq_0,leq_succ_succ,leq_succ_0, 
+		    lt_0_succ,lt_succ_succ,lt_0];
+
+val nat_ss = FOL_ss addsimps nat_rews;
+
+val prems = goal Nat2.thy 
+    "[| P(0);  !!x. P(succ(x)) |] ==> All(P)";
+by (rtac nat_ind 1);
+by (REPEAT (resolve_tac (prems@[allI,impI]) 1));
+val nat_exh = result();
+
+goal Nat2.thy "~ n=succ(n)";
+by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
+result();
+
+goal Nat2.thy "~ succ(n)=n";
+by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
+result();
+
+goal Nat2.thy "~ succ(succ(n))=n";
+by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
+result();
+
+goal Nat2.thy "~ n=succ(succ(n))";
+by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
+result();
+
+goal Nat2.thy "m+0 = m";
+by (IND_TAC nat_ind (simp_tac nat_ss) "m" 1);
+val plus_0_right = result();
+
+goal Nat2.thy "m+succ(n) = succ(m+n)";
+by (IND_TAC nat_ind (simp_tac nat_ss) "m" 1);
+val plus_succ_right = result();
+
+goal Nat2.thy "~n=0 --> m+pred(n) = pred(m+n)";
+by (IND_TAC nat_ind (simp_tac (nat_ss addsimps [plus_succ_right])) "n" 1);
+result();
+
+goal Nat2.thy "~n=0 --> succ(pred(n))=n";
+by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
+result();
+
+goal Nat2.thy "m+n=0 <-> m=0 & n=0";
+by (IND_TAC nat_ind (simp_tac nat_ss) "m" 1);
+result();
+
+goal Nat2.thy "m <= n --> m <= succ(n)";
+by (IND_TAC nat_ind (simp_tac nat_ss) "m" 1);
+by (rtac (impI RS allI) 1);
+by (ALL_IND_TAC nat_ind (simp_tac nat_ss) 1);
+by (fast_tac FOL_cs 1);
+val le_imp_le_succ = result() RS mp;
+
+goal Nat2.thy "n<succ(n)";
+by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
+result();
+
+goal Nat2.thy "~ n<n";
+by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
+result();
+
+goal Nat2.thy "m < n --> m < succ(n)";
+by (IND_TAC nat_ind (simp_tac nat_ss) "m" 1);
+by (rtac (impI RS allI) 1);
+by (ALL_IND_TAC nat_ind (simp_tac nat_ss) 1);
+by (fast_tac FOL_cs 1);
+result();
+
+goal Nat2.thy "m <= n --> m <= n+k";
+by (IND_TAC nat_ind 
+    (simp_tac (nat_ss addsimps [plus_0_right, plus_succ_right, le_imp_le_succ]))
+     "k" 1);
+val le_plus = result();
+
+goal Nat2.thy "succ(m) <= n --> m <= n";
+by (res_inst_tac [("x","n")]spec 1);
+by (ALL_IND_TAC nat_exh (simp_tac (nat_ss addsimps [le_imp_le_succ])) 1);
+val succ_le = result();
+
+goal Nat2.thy "~m<n <-> n<=m";
+by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
+by (rtac (impI RS allI) 1);
+by (ALL_IND_TAC nat_ind (asm_simp_tac nat_ss) 1);
+val not_less = result();
+
+goal Nat2.thy "n<=m --> ~m<n";
+by (simp_tac (nat_ss addsimps [not_less]) 1);
+val le_imp_not_less = result();
+
+goal Nat2.thy "m<n --> ~n<=m";
+by (cut_facts_tac [not_less] 1 THEN fast_tac FOL_cs 1);
+val not_le = result();
+
+goal Nat2.thy "m+k<=n --> m<=n";
+by (IND_TAC nat_ind (K all_tac) "k" 1);
+by (simp_tac (nat_ss addsimps [plus_0_right]) 1);
+by (rtac (impI RS allI) 1);
+by (simp_tac (nat_ss addsimps [plus_succ_right]) 1);
+by (REPEAT (resolve_tac [allI,impI] 1));
+by (cut_facts_tac [succ_le] 1);
+by (fast_tac FOL_cs 1);
+val plus_le = result();
+
+val prems = goal Nat2.thy "[| ~m=0;  m <= n |] ==> ~n=0";
+by (cut_facts_tac prems 1);
+by (REPEAT (etac rev_mp 1));
+by (IND_TAC nat_exh (simp_tac nat_ss) "m" 1);
+by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
+val not0 = result();
+
+goal Nat2.thy "a<=a' & b<=b' --> a+b<=a'+b'";
+by (IND_TAC nat_ind (simp_tac (nat_ss addsimps [plus_0_right,le_plus])) "b" 1);
+by (resolve_tac [impI RS allI] 1);
+by (resolve_tac [allI RS allI] 1);
+by (ALL_IND_TAC nat_exh (asm_simp_tac (nat_ss addsimps [plus_succ_right])) 1);
+val plus_le_plus = result();
+
+goal Nat2.thy "i<=j --> j<=k --> i<=k";
+by (IND_TAC nat_ind (K all_tac) "i" 1);
+by (simp_tac nat_ss 1);
+by (resolve_tac [impI RS allI] 1);
+by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
+by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
+by (fast_tac FOL_cs 1);
+val le_trans = result();
+
+goal Nat2.thy "i < j --> j <=k --> i < k";
+by (IND_TAC nat_ind (K all_tac) "j" 1);
+by (simp_tac nat_ss 1);
+by (resolve_tac [impI RS allI] 1);
+by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
+by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
+by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
+by (fast_tac FOL_cs 1);
+val less_le_trans = result();
+
+goal Nat2.thy "succ(i) <= j <-> i < j";
+by (IND_TAC nat_ind (simp_tac nat_ss) "j" 1);
+by (resolve_tac [impI RS allI] 1);
+by (ALL_IND_TAC nat_exh (asm_simp_tac nat_ss) 1);
+val succ_le = result();
+
+goal Nat2.thy "i<succ(j) <-> i=j | i<j";
+by (IND_TAC nat_ind (simp_tac nat_ss) "j" 1);
+by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
+by (resolve_tac [impI RS allI] 1);
+by (ALL_IND_TAC nat_exh (asm_simp_tac nat_ss) 1);
+val less_succ = result();
+
isabelle