# HG changeset patch
# User nipkow
# Date 845884278 -7200
# Node ID 73bbf2cc76513370d0d4784c4a7ed2eb85b5054c
# Parent  9709f91885499a855317371996489295691ad936
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.

diff -r 9709f9188549 -r 73bbf2cc7651 src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Mon Oct 21 09:50:50 1996 +0200
+++ b/src/HOL/Lambda/Eta.ML	Mon Oct 21 09:51:18 1996 +0200
@@ -12,7 +12,6 @@
 open Eta;
 
 Addsimps eta.intrs;
-Addsimps [imp_disj];
 
 val eta_cases = map (eta.mk_cases db.simps)
     ["Fun s -e> z","s @ t -e> u","Var i -e> t"];
@@ -23,35 +22,6 @@
 AddIs eta.intrs;
 AddSEs (beta_cases@eta_cases);
 
-section "Arithmetic lemmas";
-
-goal HOL.thy "!!P. P ==> P=True";
-by (fast_tac HOL_cs 1);
-qed "True_eq";
-
-Addsimps [less_not_sym RS True_eq];
-
-goal Arith.thy "i < j --> pred i < j";
-by (nat_ind_tac "j" 1);
-by (ALLGOALS(asm_simp_tac(!simpset addsimps [less_Suc_eq])));
-by (nat_ind_tac "j1" 1);
-by (ALLGOALS Asm_simp_tac);
-qed_spec_mp "less_imp_pred_less";
-
-goal Arith.thy "i<j --> ~ pred j < i";
-by (nat_ind_tac "j" 1);
-by (ALLGOALS(asm_simp_tac(!simpset addsimps [less_Suc_eq])));
-qed_spec_mp "less_imp_not_pred_less";
-Addsimps [less_imp_not_pred_less];
-
-goal Nat.thy "i < j --> j < Suc(Suc i) --> j = Suc i";
-by (nat_ind_tac "j" 1);
-by (ALLGOALS Simp_tac);
-by (simp_tac(!simpset addsimps [less_Suc_eq])1);
-by (fast_tac (HOL_cs addDs [less_not_sym]) 1);
-qed_spec_mp "less_interval1";
-
-
 section "decr and free";
 
 goal Eta.thy "!i k. free (lift t k) i = \
@@ -59,30 +29,23 @@
 by (db.induct_tac "t" 1);
 by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addcongs [conj_cong])));
 by (fast_tac HOL_cs 2);
-by (safe_tac (HOL_cs addSIs [iffI]));
-by (dtac Suc_mono 1);
-by (ALLGOALS(Asm_full_simp_tac));
-by (dtac less_trans_Suc 1 THEN atac 1);
-by (dtac less_trans_Suc 2 THEN atac 2);
-by (ALLGOALS(Asm_full_simp_tac));
+by(simp_tac (!simpset addsimps [pred_def]
+                      setloop (split_tac [expand_nat_case])) 1);
+by (safe_tac HOL_cs);
+by (ALLGOALS trans_tac);
 qed "free_lift";
 Addsimps [free_lift];
 
 goal Eta.thy "!i k t. free (s[t/k]) i = \
 \              (free s k & free t i | free s (if i<k then i else Suc i))";
 by (db.induct_tac "s" 1);
-by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addsimps
-[less_not_refl2,less_not_refl2 RS not_sym])));
-by (fast_tac HOL_cs 2);
-by (safe_tac (HOL_cs addSIs [iffI]));
-by (ALLGOALS(Asm_simp_tac));
-by (fast_tac (HOL_cs addEs [less_imp_not_pred_less RS notE]) 1);
-by (fast_tac (HOL_cs addDs [less_not_sym]) 1);
-by (dtac Suc_mono 1);
-by (dtac less_interval1 1 THEN atac 1);
-by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
-by (dtac less_trans_Suc 1 THEN atac 1);
-by (Asm_full_simp_tac 1);
+by (Asm_simp_tac 2);
+by (Fast_tac 2);
+by (asm_full_simp_tac (addsplit (!simpset)) 2);
+by(simp_tac (!simpset addsimps [pred_def,subst_Var]
+                      setloop (split_tac [expand_if,expand_nat_case])) 1);
+by (safe_tac (HOL_cs addSEs [nat_neqE]));
+by (ALLGOALS trans_tac);
 qed "free_subst";
 Addsimps [free_subst];
 
@@ -248,7 +211,7 @@
     by (fast_tac (HOL_cs addDs [less_not_refl2]) 1);
    by (Simp_tac 1);
   by (Simp_tac 1);
- by (asm_simp_tac (!simpset addsimps [de_Morgan_disj]) 1);
+ by (Asm_simp_tac 1);
  by (etac thin_rl 1);
  by (etac thin_rl 1);
  by (rtac allI 1);
diff -r 9709f9188549 -r 73bbf2cc7651 src/HOL/Lambda/Lambda.ML
--- a/src/HOL/Lambda/Lambda.ML	Mon Oct 21 09:50:50 1996 +0200
+++ b/src/HOL/Lambda/Lambda.ML	Mon Oct 21 09:51:18 1996 +0200
@@ -3,46 +3,9 @@
     Author:     Tobias Nipkow
     Copyright   1995 TU Muenchen
 
-Substitution-lemmas.  Most of the proofs, esp. those about natural numbers,
-are ported from Ole Rasmussen's ZF development.  In ZF, m<=n is syntactic
-sugar for m<Suc(n). In HOL <= is a separate operator. Hence we have to prove
-some compatibility lemmas.
+Substitution-lemmas.
 *)
 
-(*** Nat ***)
-
-goal Nat.thy "!!i. [| i < Suc j; j < k |] ==> i < k";
-by (rtac le_less_trans 1);
-by (assume_tac 2);
-by (asm_full_simp_tac (!simpset addsimps [le_def, less_Suc_eq]) 1);
-by (fast_tac (HOL_cs addEs [less_asym,less_irrefl]) 1);
-qed "lt_trans1";
-
-goal Nat.thy "!!i. [| i < j; j < Suc(k) |] ==> i < k";
-by (etac less_le_trans 1);
-by (asm_full_simp_tac (!simpset addsimps [le_def, less_Suc_eq]) 1);
-by (fast_tac (HOL_cs addEs [less_asym,less_irrefl]) 1);
-qed "lt_trans2";
-
-val major::prems = goal Nat.thy
-  "[| i < Suc j; i < j ==> P; i = j ==> P |] ==> P";
-by (rtac (major RS lessE) 1);
-by (ALLGOALS Asm_full_simp_tac);
-by (resolve_tac prems 1 THEN etac sym 1);
-by (fast_tac (HOL_cs addIs prems) 1);
-qed "leqE";
-
-goal Arith.thy "!!i. Suc i < j ==> i < pred j ";
-by (rtac Suc_less_SucD 1);
-by (Asm_simp_tac 1);
-qed "lt_pred";
-
-goal Arith.thy "!!i. [| i < Suc j; k < i |] ==> pred i < j ";
-by (rtac Suc_less_SucD 1);
-by (Asm_simp_tac 1);
-qed "gt_pred";
-
-
 (*** Lambda ***)
 
 open Lambda;
@@ -102,28 +65,20 @@
 goal Lambda.thy
   "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
 by (db.induct_tac "t" 1);
-by (ALLGOALS Asm_simp_tac);
-by (strip_tac 1);
-by (excluded_middle_tac "nat < i" 1);
-by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2));
-by (ALLGOALS(asm_full_simp_tac (addsplit(!simpset) addsimps [less_SucI])));
+by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])
+                                    addsolver (cut_trans_tac))));
+by (safe_tac HOL_cs);
+by (ALLGOALS trans_tac);
 qed_spec_mp "lift_lift";
 
 goal Lambda.thy "!i j s. j < Suc i --> \
 \         lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
 by (db.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift])));
-by (strip_tac 1);
-by (excluded_middle_tac "nat < j" 1);
-by (Asm_full_simp_tac 1);
-by (eres_inst_tac [("j","nat")] leqE 1);
-by (asm_full_simp_tac (addsplit(!simpset)
-                       addsimps [less_SucI,gt_pred]) 1);
-by (hyp_subst_tac 1);
-by (Asm_simp_tac 1);
-by (forw_inst_tac [("j","j")] lt_trans2 1);
-by (assume_tac 1);
-by (asm_full_simp_tac (addsplit(!simpset) addsimps [less_SucI]) 1);
+by (ALLGOALS(asm_simp_tac (!simpset addsimps [pred_def,subst_Var,lift_lift]
+                                setloop (split_tac [expand_if,expand_nat_case])
+                                addsolver (cut_trans_tac))));
+by (safe_tac HOL_cs);
+by (ALLGOALS trans_tac);
 qed "lift_subst";
 Addsimps [lift_subst];
 
@@ -131,25 +86,16 @@
   "!i j s. i < Suc j -->\
 \         lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
 by (db.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift])));
-by (strip_tac 1);
-by (excluded_middle_tac "nat < j" 1);
-by (Asm_full_simp_tac 1);
-by (eres_inst_tac [("i","j")] leqE 1);
-by (forward_tac  [lt_trans1] 1 THEN assume_tac 1);
-by (ALLGOALS(asm_full_simp_tac
-               (!simpset addsimps [less_SucI,gt_pred])));
-by (hyp_subst_tac 1);
-by (asm_full_simp_tac (!simpset addsimps [less_SucI]) 1);
-by (split_tac [expand_if] 1);
-by (asm_full_simp_tac (!simpset addsimps [less_SucI]) 1);
+by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_Var,lift_lift]
+                                setloop (split_tac [expand_if])
+                                addsolver (cut_trans_tac))));
+by(safe_tac (HOL_cs addSEs [nat_neqE]));
+by(ALLGOALS trans_tac);
 qed "lift_subst_lt";
 
 goal Lambda.thy "!k s. (lift t k)[s/k] = t";
 by (db.induct_tac "t" 1);
-by (ALLGOALS Asm_simp_tac);
-by (split_tac [expand_if] 1);
-by (ALLGOALS Asm_full_simp_tac);
+by (ALLGOALS (asm_full_simp_tac (!simpset setloop (split_tac[expand_if]))));
 qed "subst_lift";
 Addsimps [subst_lift];
 
@@ -157,25 +103,12 @@
 goal Lambda.thy "!i j u v. i < Suc j --> \
 \ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
 by (db.induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac(!simpset addsimps [lift_lift RS sym,lift_subst_lt])));
-by (strip_tac 1);
-by (excluded_middle_tac "nat < Suc(Suc j)" 1);
-by (Asm_full_simp_tac 1);
-by (forward_tac [lessI RS less_trans] 1);
-by (etac leqE 1);
-by (asm_simp_tac (!simpset addsimps [lt_pred]) 2);
-by (forward_tac [Suc_mono RS less_trans] 1 THEN assume_tac 1);
-by (forw_inst_tac [("i","i")] (lessI RS less_trans) 1);
-by (asm_simp_tac (!simpset addsimps [lt_pred]) 1);
-by (eres_inst_tac [("i","nat")] leqE 1);
-by (asm_full_simp_tac (!simpset addsimps [less_SucI]) 2);
-by (excluded_middle_tac "nat < i" 1);
-by (Asm_full_simp_tac 1);
-by (eres_inst_tac [("j","nat")] leqE 1);
-by (asm_simp_tac (!simpset addsimps [gt_pred]) 1);
-by (Asm_simp_tac 1);
-by (forward_tac [lt_trans2] 1 THEN assume_tac 1);
-by (asm_simp_tac (!simpset addsimps [gt_pred]) 1);
+by (ALLGOALS(asm_simp_tac
+      (!simpset addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt]
+                setloop (split_tac [expand_if,expand_nat_case])
+                addsolver (cut_trans_tac))));
+by(safe_tac (HOL_cs addSEs [nat_neqE]));
+by(ALLGOALS trans_tac);
 qed_spec_mp "subst_subst";