added nat_diff_split and a few lemmas in Trancl.
authornipkow
Wed Oct 28 11:25:38 1998 +0100 (1998-10-28)
changeset 57717c2c8cf20221
parent 5770 e2600149f7f4
child 5772 d52d61a66c32
added nat_diff_split and a few lemmas in Trancl.
src/HOL/Arith.ML
src/HOL/Trancl.ML
src/HOL/arith_data.ML
     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.5  Addsimps [diff_is_0_eq RS iffD2];
     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.43 +by (blast_tac (claset() addIs prems addSDs [trancl_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";