# HG changeset patch
# User nipkow
# Date 909570338 -3600
# Node ID 7c2c8cf20221a4c7e83152c8d86a816a9bfe0ee1
# Parent  e2600149f7f4021e2ac566563e5efacbdc9dd212
added nat_diff_split and a few lemmas in Trancl.

diff -r e2600149f7f4 -r 7c2c8cf20221 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Mon Oct 26 13:05:08 1998 +0100
+++ b/src/HOL/Arith.ML	Wed Oct 28 11:25:38 1998 +0100
@@ -435,11 +435,6 @@
 qed "diff_is_0_eq";
 Addsimps [diff_is_0_eq RS iffD2];
 
-Goal "m-n = 0  -->  n-m = 0  -->  m=n";
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (REPEAT(Simp_tac 1 THEN TRY(atac 1)));
-qed_spec_mp "diffs0_imp_equal";
-
 Goal "(0<n-m) = (m<n)";
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (ALLGOALS Asm_simp_tac);
diff -r e2600149f7f4 -r 7c2c8cf20221 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Mon Oct 26 13:05:08 1998 +0100
+++ b/src/HOL/Trancl.ML	Wed Oct 28 11:25:38 1998 +0100
@@ -6,9 +6,9 @@
 Theorems about the transitive closure of a relation
 *)
 
-open Trancl;
+(** The relation rtrancl **)
 
-(** The relation rtrancl **)
+section "^*";
 
 Goal "mono(%s. Id Un (r O s))";
 by (rtac monoI 1);
@@ -195,6 +195,8 @@
 
 (**** The relation trancl ****)
 
+section "^+";
+
 Goalw [trancl_def] "[| p:r^+; r <= s |] ==> p:s^+";
 by (blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1);
 qed "trancl_mono";
@@ -296,6 +298,24 @@
 				  r_comp_rtrancl_eq]) 1);
 qed "trancl_converse";
 
+Goal "(x,y) : (r^+)^-1 ==> (x,y) : (r^-1)^+";
+by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1);
+qed "trancl_converseI";
+
+Goal "(x,y) : (r^-1)^+ ==> (x,y) : (r^+)^-1";
+by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1);
+qed "trancl_converseD";
+
+val major::prems = Goal
+    "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y); \
+\       !!y z.[| (y,z) : r;  (z,b) : r^+;  P(z) |] ==> P(y) |]  \
+\     ==> P(a)";
+by (rtac ((major RS converseI RS trancl_converseI) RS trancl_induct) 1);
+ by (resolve_tac prems 1);
+ be converseD 1;
+by (blast_tac (claset() addIs prems addSDs [trancl_converseD])1);
+qed "converse_trancl_induct";
+
 (*Unused*)
 qed_goal "irrefl_tranclI" Trancl.thy 
    "!!r. r^-1 Int r^+ = {} ==> (x, x) ~: r^+" 
diff -r e2600149f7f4 -r 7c2c8cf20221 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Mon Oct 26 13:05:08 1998 +0100
+++ b/src/HOL/arith_data.ML	Wed Oct 28 11:25:38 1998 +0100
@@ -232,3 +232,21 @@
 by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
 				      Suc_diff_le, less_imp_le]) 1);
 qed_spec_mp "diff_less_mono2";
+
+(** Elimination of - on nat due to John Harrison **)
+(*This proof requires natle_cancel_sums*)
+
+Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";
+by(case_tac "a <= b" 1);
+by(Auto_tac);
+by(eres_inst_tac [("x","b-a")] allE 1);
+by(Auto_tac);
+qed "nat_diff_split";
+
+(*
+This is an example of the power of nat_diff_split. Many of the `-' thms in
+Arith.ML could take advantage of this, but would need to be moved.
+*)
+Goal "m-n = 0  -->  n-m = 0  -->  m=n";
+by(simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed_spec_mp "diffs0_imp_equal";