# HG changeset patch
# User nipkow
# Date 814610909 -3600
# Node ID 42782316d510809f8a6301249a74626ca54ea52a
# Parent  c7a8f374339b1bd4c12718ae686d26b75836865c
Added various thms and tactics.

diff -r c7a8f374339b -r 42782316d510 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Wed Oct 25 09:46:46 1995 +0100
+++ b/src/HOL/Arith.ML	Wed Oct 25 09:48:29 1995 +0100
@@ -14,6 +14,16 @@
 val [pred_0, pred_Suc] = nat_recs pred_def;
 val [add_0,add_Suc] = nat_recs add_def; 
 val [mult_0,mult_Suc] = nat_recs mult_def; 
+Addsimps [pred_0,pred_Suc,add_0,add_Suc,mult_0,mult_Suc];
+
+(** pred **)
+
+val prems = goal Arith.thy "n ~= 0 ==> Suc(pred n) = n";
+by(res_inst_tac [("n","n")] natE 1);
+by(cut_facts_tac prems 1);
+by(ALLGOALS Asm_full_simp_tac);
+qed "Suc_pred";
+Addsimps [Suc_pred];
 
 (** Difference **)
 
@@ -30,10 +40,7 @@
  (fn _ =>
   [Simp_tac 1, nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]);
 
-(*** Simplification over add, mult, diff ***)
-
-Addsimps [pred_0, pred_Suc, add_0, add_Suc, mult_0, mult_Suc, diff_0,
-          diff_0_eq_0, diff_Suc_Suc];
+Addsimps [diff_0, diff_0_eq_0, diff_Suc_Suc];
 
 
 (**** Inductive properties of the operators ****)
diff -r c7a8f374339b -r 42782316d510 src/HOL/List.ML
--- a/src/HOL/List.ML	Wed Oct 25 09:46:46 1995 +0100
+++ b/src/HOL/List.ML	Wed Oct 25 09:48:29 1995 +0100
@@ -125,17 +125,62 @@
 by (list.induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed"length_append";
+Addsimps [length_append];
+
+goal List.thy "length (map f l) = length l";
+by (list.induct_tac "l" 1);
+by (ALLGOALS Simp_tac);
+qed "length_map";
+Addsimps [length_map];
 
 goal List.thy "length(rev xs) = length(xs)";
 by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [length_append])));
+by (ALLGOALS Asm_simp_tac);
 qed "length_rev";
+Addsimps [length_rev];
 
 (** nth **)
 
 val [nth_0,nth_Suc] = nat_recs nth_def; 
 store_thm("nth_0",nth_0);
 store_thm("nth_Suc",nth_Suc);
+Addsimps [nth_0,nth_Suc];
+
+goal List.thy "!n. n < length xs --> nth n (map f xs) = f (nth n xs)";
+by (list.induct_tac "xs" 1);
+(* case [] *)
+by (Asm_full_simp_tac 1);
+(* case x#xl *)
+by (rtac allI 1);
+by (nat_ind_tac "n" 1);
+by (ALLGOALS Asm_full_simp_tac);
+bind_thm("nth_map", result() RS spec RS mp);
+Addsimps [nth_map];
+
+goal List.thy "!n. n < length xs --> list_all P xs --> P(nth n xs)";
+by (list.induct_tac "xs" 1);
+(* case [] *)
+by (Simp_tac 1);
+(* case x#xl *)
+by (rtac allI 1);
+by (nat_ind_tac "n" 1);
+by (ALLGOALS Asm_full_simp_tac);
+bind_thm("list_all_nth", result() RS spec RS mp RS mp);
+
+goal List.thy "!n. n < length xs --> (nth n xs) mem xs";
+by (list.induct_tac "xs" 1);
+(* case [] *)
+by (Simp_tac 1);
+(* case x#xl *)
+by (rtac allI 1);
+by (nat_ind_tac "n" 1);
+(* case 0 *)
+by (Asm_full_simp_tac 1);
+(* case Suc x *)
+by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+bind_thm ("nth_mem",result() RS spec RS mp);
+Addsimps [nth_mem];
+
 
 (** Additional mapping lemmas **)
 
@@ -171,5 +216,5 @@
    mem_append, mem_filter,
    rev_append, rev_rev_ident,
    map_ident, map_append, map_compose,
-   flat_append, length_append, list_all_True, list_all_conj, nth_0, nth_Suc];
+   flat_append, list_all_True, list_all_conj];
 
diff -r c7a8f374339b -r 42782316d510 src/HOL/Makefile
--- a/src/HOL/Makefile	Wed Oct 25 09:46:46 1995 +0100
+++ b/src/HOL/Makefile	Wed Oct 25 09:48:29 1995 +0100
@@ -119,6 +119,14 @@
 Lambda:  $(BIN)/HOL  $(LAMBDA_FILES)
 	echo 'exit_use"Lambda/ROOT.ML";quit();' | $(LOGIC)
 
+MINIML_NAMES = I Maybe MiniML Type W
+
+LAMBDA_FILES = MiniML/ROOT.ML \
+              $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
+
+MiniML: $(BIN)/HOL  $(MINIML_FILES)
+	echo 'exit_use"MiniML/ROOT.ML";quit();' | $(LOGIC)
+
 ##Miscellaneous examples
 EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String \
 	   BT Perm
@@ -130,7 +138,7 @@
 	echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
 
 #Full test. (IOA has been removed temporarily)
-test:   $(BIN)/HOL IMP Integ Subst Lambda ex
+test:   $(BIN)/HOL IMP Integ Subst Lambda MiniML ex
 	echo 'Test examples ran successfully' > test
 
 .PRECIOUS:  $(BIN)/Pure $(BIN)/HOL 
diff -r c7a8f374339b -r 42782316d510 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Wed Oct 25 09:46:46 1995 +0100
+++ b/src/HOL/Nat.ML	Wed Oct 25 09:48:29 1995 +0100
@@ -97,6 +97,8 @@
 
 bind_thm ("Zero_not_Suc", (Suc_not_Zero RS not_sym));
 
+Addsimps [Suc_not_Zero,Zero_not_Suc];
+
 bind_thm ("Suc_neq_Zero", (Suc_not_Zero RS notE));
 val Zero_neq_Suc = sym RS Suc_neq_Zero;
 
@@ -118,7 +120,7 @@
 
 goal Nat.thy "n ~= Suc(n)";
 by (nat_ind_tac "n" 1);
-by (ALLGOALS(asm_simp_tac (!simpset addsimps [Zero_not_Suc,Suc_Suc_eq])));
+by (ALLGOALS(asm_simp_tac (!simpset addsimps [Suc_Suc_eq])));
 qed "n_not_Suc_n";
 
 val Suc_n_not_n = n_not_Suc_n RS not_sym;
@@ -203,6 +205,7 @@
 goalw Nat.thy [less_def] "n < Suc(n)";
 by (rtac (pred_natI RS r_into_trancl) 1);
 qed "lessI";
+Addsimps [lessI];
 
 (* i(j ==> i(Suc(j) *)
 val less_SucI = lessI RSN (2, less_trans);
@@ -213,6 +216,7 @@
 by (etac less_trans 1);
 by (rtac lessI 1);
 qed "zero_less_Suc";
+Addsimps [zero_less_Suc];
 
 (** Elimination properties **)
 
@@ -251,6 +255,7 @@
 by (etac Zero_neq_Suc 1);
 by (etac Zero_neq_Suc 1);
 qed "not_less0";
+Addsimps [not_less0];
 
 (* n<0 ==> R *)
 bind_thm ("less_zeroE", (not_less0 RS notE));
@@ -269,6 +274,12 @@
 		     addEs  [less_trans, less_SucE]) 1);
 qed "less_Suc_eq";
 
+val prems = goal Nat.thy "m<n ==> n ~= 0";
+by(res_inst_tac [("n","n")] natE 1);
+by(cut_facts_tac prems 1);
+by(ALLGOALS Asm_full_simp_tac);
+qed "gr_implies_not0";
+Addsimps [gr_implies_not0];
 
 (** Inductive (?) properties **)
 
@@ -311,10 +322,18 @@
 goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)";
 by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]);
 qed "Suc_less_eq";
+Addsimps [Suc_less_eq];
 
 goal Nat.thy "~(Suc(n) < n)";
 by(fast_tac (HOL_cs addEs [Suc_lessD RS less_anti_refl]) 1);
 qed "not_Suc_n_less_n";
+Addsimps [not_Suc_n_less_n];
+
+goal Nat.thy "!!i. i<j ==> j<k --> Suc i < k";
+by(nat_ind_tac "k" 1);
+by(ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
+by(fast_tac (HOL_cs addDs [Suc_lessD]) 1);
+bind_thm("less_trans_Suc",result() RS mp);
 
 (*"Less than" is a linear ordering*)
 goal Nat.thy "m<n | m=n | n<(m::nat)";
@@ -328,8 +347,7 @@
 (*Can be used with less_Suc_eq to get n=m | n<m *)
 goal Nat.thy "(~ m < n) = (n < Suc(m))";
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by(ALLGOALS(asm_simp_tac (!simpset addsimps
-                          [not_less0,zero_less_Suc,Suc_less_eq])));
+by(ALLGOALS Asm_simp_tac);
 qed "not_less_eq";
 
 (*Complete induction, aka course-of-values induction*)
@@ -346,9 +364,18 @@
 by (rtac not_less0 1);
 qed "le0";
 
-Addsimps [not_less0, less_not_refl, zero_less_Suc, lessI, 
-          Suc_less_eq, less_Suc_eq, le0, not_Suc_n_less_n,
-          Suc_not_Zero, Zero_not_Suc, Suc_Suc_eq,
+goalw Nat.thy [le_def] "~ Suc n <= n";
+by(Simp_tac 1);
+qed "Suc_n_not_le_n";
+
+goalw Nat.thy [le_def] "(i <= 0) = (i = 0)";
+by(nat_ind_tac "i" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "le_0";
+
+Addsimps [less_not_refl,
+          less_Suc_eq, le0, le_0,
+          Suc_Suc_eq, Suc_n_not_le_n,
           n_not_Suc_n, Suc_n_not_n,
           nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
 
diff -r c7a8f374339b -r 42782316d510 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Wed Oct 25 09:46:46 1995 +0100
+++ b/src/HOL/Prod.ML	Wed Oct 25 09:48:29 1995 +0100
@@ -53,12 +53,40 @@
 by (REPEAT (eresolve_tac [prem,exE] 1));
 qed "PairE";
 
+(* replace parameters of product type by individual component parameters *)
+local
+fun is_pair (_,Type("*",_)) = true
+  | is_pair _ = false;
+
+fun find_pair_param t =
+  let val params = Logic.strip_params t
+  in if exists is_pair params
+     then let val params = rev(rename_wrt_term t params)
+                           (*as they are printed*)
+          in apsome fst (find_first is_pair params) end
+     else None
+  end;
+
+in
+
+val split_all_tac = REPEAT o SUBGOAL (fn (t,_) =>
+  case find_pair_param t of
+    None => no_tac
+  | Some x => EVERY[res_inst_tac[("p",x)] PairE 1,
+                    REPEAT(hyp_subst_tac 1), prune_params_tac]);
+
+end;
+
+goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
+by(fast_tac (HOL_cs addbefore split_all_tac 1) 1);
+qed "split_paired_All";
+
 goalw Prod.thy [split_def] "split c (a,b) = c a b";
 by (sstac [fst_conv, snd_conv] 1);
 by (rtac refl 1);
 qed "split";
 
-Addsimps [fst_conv, snd_conv, split, Pair_eq];
+Addsimps [fst_conv, snd_conv, split_paired_All, split, Pair_eq];
 
 goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
 by (res_inst_tac[("p","s")] PairE 1);
diff -r c7a8f374339b -r 42782316d510 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Wed Oct 25 09:46:46 1995 +0100
+++ b/src/HOL/ROOT.ML	Wed Oct 25 09:48:29 1995 +0100
@@ -11,7 +11,6 @@
 writeln banner;
 
 print_depth 1;
-set eta_contract;
 
 (* Add user sections *)
 use "../Pure/section_utils.ML";
diff -r c7a8f374339b -r 42782316d510 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Wed Oct 25 09:46:46 1995 +0100
+++ b/src/HOL/Trancl.ML	Wed Oct 25 09:48:29 1995 +0100
@@ -31,9 +31,9 @@
 qed "rtrancl_into_rtrancl";
 
 (*rtrancl of r contains r*)
-val [prem] = goal Trancl.thy "[| (a,b) : r |] ==> (a,b) : r^*";
-by (rtac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
-by (rtac prem 1);
+goal Trancl.thy "!!p. p : r ==> p : r^*";
+by(split_all_tac 1);
+by (etac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
 qed "r_into_rtrancl";
 
 (*monotonicity of rtrancl*)
@@ -161,7 +161,24 @@
 by(fast_tac (HOL_cs addEs [rtrancl_trans]) 1);
 be r_into_rtrancl 1;
 qed "rtrancl_idemp";
+Addsimps [rtrancl_idemp];
 
+goal Trancl.thy "!!R. [| R <= S; S <= R^* |] ==> S^* = R^*";
+bd rtrancl_mono 1;
+bd rtrancl_mono 1;
+by(Asm_full_simp_tac 1);
+by(fast_tac eq_cs 1);
+qed "rtrancl_subset";
+
+goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*";
+by(best_tac (set_cs addIs [rtrancl_subset,r_into_rtrancl,
+                           rtrancl_mono RS subsetD]) 1);
+qed "trancl_Un_trancl";
+
+goal Trancl.thy "(R^=)^* = R^*";
+by(fast_tac (rel_cs addIs [rtrancl_refl,rtrancl_subset,r_into_rtrancl]) 1);
+qed "rtrancl_reflcl";
+Addsimps [rtrancl_reflcl];
 
 goal Trancl.thy "!!r. (x,y) : (converse r)^* ==> (x,y) : converse(r^*)";
 br converseI 1;
@@ -198,4 +215,5 @@
 by (fast_tac (rel_cs addSDs [trancl_subset_Sigma_lemma]) 1);
 qed "trancl_subset_Sigma";
 
+(* Don't add r_into_rtrancl: it messes up the proofs in Lambda *)
 val trancl_cs = rel_cs addIs [rtrancl_refl];
diff -r c7a8f374339b -r 42782316d510 src/HOL/Trancl.thy
--- a/src/HOL/Trancl.thy	Wed Oct 25 09:46:46 1995 +0100
+++ b/src/HOL/Trancl.thy	Wed Oct 25 09:48:29 1995 +0100
@@ -5,14 +5,20 @@
 
 Relfexive and Transitive closure of a relation
 
-rtrancl is refl&transitive closure;  trancl is transitive closure
+rtrancl is refl&transitive closure;
+trancl is transitive closure
+reflcl is reflexive closure
 *)
 
 Trancl = Lfp + Relation + 
 consts
     rtrancl :: "('a * 'a)set => ('a * 'a)set"	("(_^*)" [100] 100)
     trancl  :: "('a * 'a)set => ('a * 'a)set"	("(_^+)" [100] 100)  
+syntax
+    reflcl  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [100] 100)
 defs   
-rtrancl_def	"r^* == lfp(%s. id Un (r O s))"
-trancl_def	"r^+ == r O rtrancl(r)"
+  rtrancl_def	"r^*  ==  lfp(%s. id Un (r O s))"
+  trancl_def	"r^+  ==  r O rtrancl(r)"
+translations
+                "r^=" == "r Un id"
 end