author nipkow Wed Oct 28 11:25:38 1998 +0100 (1998-10-28) changeset 5771 7c2c8cf20221 parent 5770 e2600149f7f4 child 5772 d52d61a66c32
added nat_diff_split and a few lemmas in Trancl.
 src/HOL/Arith.ML file | annotate | diff | revisions src/HOL/Trancl.ML file | annotate | diff | revisions src/HOL/arith_data.ML file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Arith.ML	Mon Oct 26 13:05:08 1998 +0100
1.2 +++ b/src/HOL/Arith.ML	Wed Oct 28 11:25:38 1998 +0100
1.3 @@ -435,11 +435,6 @@
1.4  qed "diff_is_0_eq";
1.6
1.7 -Goal "m-n = 0  -->  n-m = 0  -->  m=n";
1.8 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
1.9 -by (REPEAT(Simp_tac 1 THEN TRY(atac 1)));
1.10 -qed_spec_mp "diffs0_imp_equal";
1.11 -
1.12  Goal "(0<n-m) = (m<n)";
1.13  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
1.14  by (ALLGOALS Asm_simp_tac);
```
```     2.1 --- a/src/HOL/Trancl.ML	Mon Oct 26 13:05:08 1998 +0100
2.2 +++ b/src/HOL/Trancl.ML	Wed Oct 28 11:25:38 1998 +0100
2.3 @@ -6,9 +6,9 @@
2.4  Theorems about the transitive closure of a relation
2.5  *)
2.6
2.7 -open Trancl;
2.8 +(** The relation rtrancl **)
2.9
2.10 -(** The relation rtrancl **)
2.11 +section "^*";
2.12
2.13  Goal "mono(%s. Id Un (r O s))";
2.14  by (rtac monoI 1);
2.15 @@ -195,6 +195,8 @@
2.16
2.17  (**** The relation trancl ****)
2.18
2.19 +section "^+";
2.20 +
2.21  Goalw [trancl_def] "[| p:r^+; r <= s |] ==> p:s^+";
2.22  by (blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1);
2.23  qed "trancl_mono";
2.24 @@ -296,6 +298,24 @@
2.25  				  r_comp_rtrancl_eq]) 1);
2.26  qed "trancl_converse";
2.27
2.28 +Goal "(x,y) : (r^+)^-1 ==> (x,y) : (r^-1)^+";
2.29 +by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1);
2.30 +qed "trancl_converseI";
2.31 +
2.32 +Goal "(x,y) : (r^-1)^+ ==> (x,y) : (r^+)^-1";
2.33 +by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1);
2.34 +qed "trancl_converseD";
2.35 +
2.36 +val major::prems = Goal
2.37 +    "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y); \
2.38 +\       !!y z.[| (y,z) : r;  (z,b) : r^+;  P(z) |] ==> P(y) |]  \
2.39 +\     ==> P(a)";
2.40 +by (rtac ((major RS converseI RS trancl_converseI) RS trancl_induct) 1);
2.41 + by (resolve_tac prems 1);
2.42 + be converseD 1;
2.44 +qed "converse_trancl_induct";
2.45 +
2.46  (*Unused*)
2.47  qed_goal "irrefl_tranclI" Trancl.thy
2.48     "!!r. r^-1 Int r^+ = {} ==> (x, x) ~: r^+"
```
```     3.1 --- a/src/HOL/arith_data.ML	Mon Oct 26 13:05:08 1998 +0100
3.2 +++ b/src/HOL/arith_data.ML	Wed Oct 28 11:25:38 1998 +0100
3.3 @@ -232,3 +232,21 @@
3.4  by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
3.5  				      Suc_diff_le, less_imp_le]) 1);
3.6  qed_spec_mp "diff_less_mono2";
3.7 +
3.8 +(** Elimination of - on nat due to John Harrison **)
3.9 +(*This proof requires natle_cancel_sums*)
3.10 +
3.11 +Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";
3.12 +by(case_tac "a <= b" 1);
3.13 +by(Auto_tac);
3.14 +by(eres_inst_tac [("x","b-a")] allE 1);
3.15 +by(Auto_tac);
3.16 +qed "nat_diff_split";
3.17 +
3.18 +(*
3.19 +This is an example of the power of nat_diff_split. Many of the `-' thms in
3.20 +Arith.ML could take advantage of this, but would need to be moved.
3.21 +*)
3.22 +Goal "m-n = 0  -->  n-m = 0  -->  m=n";
3.23 +by(simp_tac (simpset() addsplits [nat_diff_split]) 1);
3.24 +qed_spec_mp "diffs0_imp_equal";
```