# HG changeset patch
# User nipkow
# Date 924192637 -7200
# Node ID 228237ec56e50a49a9d2128206fa695217e96e6c
# Parent  cdde45202c5c35f6f5c24f0a46481d7b7f74fc0d
Added new thms.

diff -r cdde45202c5c -r 228237ec56e5 src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Wed Apr 14 19:07:39 1999 +0200
+++ b/src/HOL/HOL.ML	Thu Apr 15 18:10:37 1999 +0200
@@ -195,6 +195,9 @@
          [cut_facts_tac prems 1, resolve_tac prems 1,
           etac conjunct1 1, etac conjunct2 1]);
 
+qed_goal "context_conjI" HOL.thy  "[| P; P ==> Q |] ==> P & Q"
+ (fn prems => [REPEAT(resolve_tac (conjI::prems) 1)]);
+
 
 (** Disjunction *)
 section "|";
diff -r cdde45202c5c -r 228237ec56e5 src/HOL/List.ML
--- a/src/HOL/List.ML	Wed Apr 14 19:07:39 1999 +0200
+++ b/src/HOL/List.ML	Thu Apr 15 18:10:37 1999 +0200
@@ -436,11 +436,31 @@
 qed "set_map";
 Addsimps [set_map];
 
+Goal "set(filter P xs) = {x. x : set xs & P x}";
+by(induct_tac "xs" 1);
+by(Auto_tac);
+qed "set_filter";
+Addsimps [set_filter];
+(*
 Goal "(x : set (filter P xs)) = (x : set xs & P x)";
 by (induct_tac "xs" 1);
 by Auto_tac;
 qed "in_set_filter";
 Addsimps [in_set_filter];
+*)
+Goal "set[i..j(] = {k. i <= k & k < j}";
+by(induct_tac "j" 1);
+by(Auto_tac);
+by(arith_tac 1);
+qed "set_upt";
+Addsimps [set_upt];
+
+Goal "!i < size xs. set(xs[i := x]) <= insert x (set xs)";
+by(induct_tac "xs" 1);
+ by(Simp_tac 1);
+by(asm_simp_tac (simpset() addsplits [nat.split]) 1);
+by(Blast_tac 1);
+qed_spec_mp "set_list_update_subset";
 
 Goal "(x : set xs) = (? ys zs. xs = ys@x#zs)";
 by (induct_tac "xs" 1);
@@ -643,6 +663,20 @@
 by (auto_tac (claset(), simpset() addsimps [nth_Cons] addsplits [nat.split]));
 qed_spec_mp "nth_list_update";
 
+Goal "!i. i < size xs --> xs[i:=x, i:=y] = xs[i:=y]";
+by(induct_tac "xs" 1);
+ by(Simp_tac 1);
+by(asm_simp_tac (simpset() addsplits [nat.split]) 1);
+qed_spec_mp "list_update_overwrite";
+Addsimps [list_update_overwrite];
+
+Goal "!i < length xs. (xs[i := x] = xs) = (xs!i = x)";
+by(induct_tac "xs" 1);
+ by(Simp_tac 1);
+by(simp_tac (simpset() addsplits [nat.split]) 1);
+by(Blast_tac 1);
+qed_spec_mp "list_update_same_conv";
+
 
 (** last & butlast **)
 
@@ -933,6 +967,43 @@
 qed_spec_mp "nth_upt";
 Addsimps [nth_upt];
 
+Goal "!i. i+m <= n --> take m [i..n(] = [i..i+m(]";
+by(induct_tac "m" 1);
+ by(Simp_tac 1);
+by(Clarify_tac 1);
+by(stac upt_rec 1);
+br sym 1;
+by(stac upt_rec 1);
+by(asm_simp_tac (simpset() delsimps (thms"upt.simps")) 1);
+qed_spec_mp "take_upt";
+Addsimps [take_upt];
+
+Goal "!m i. i < n-m --> (map f [m..n(]) ! i = f(m+i)";
+by(induct_tac "n" 1);
+ by(Simp_tac 1);
+by(Clarify_tac 1);
+by(subgoal_tac "m < Suc n" 1);
+ by(arith_tac 2);
+by(stac upt_rec 1);
+by(asm_simp_tac (simpset() delsplits [split_if]) 1);
+by(split_tac [split_if] 1);
+br conjI 1;
+ by(simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);
+ by(simp_tac (simpset() addsimps [nth_append] addsplits [nat.split]) 1);
+ by(Clarify_tac 1);
+ br conjI 1;
+  by(Clarify_tac 1);
+  by(subgoal_tac "Suc(m+nat) < n" 1);
+   by(arith_tac 2);
+  by(Asm_simp_tac 1);
+ by(Clarify_tac 1);
+ by(subgoal_tac "n = Suc(m+nat)" 1);
+  by(arith_tac 2);
+ by(Asm_simp_tac 1);
+by(simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);
+by(arith_tac 1);
+qed_spec_mp "nth_map_upt";
+
 
 (** nodups & remdups **)
 section "nodups & remdups";
diff -r cdde45202c5c -r 228237ec56e5 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Wed Apr 14 19:07:39 1999 +0200
+++ b/src/HOL/Nat.ML	Thu Apr 15 18:10:37 1999 +0200
@@ -113,3 +113,17 @@
 qed "min_Suc_Suc";
 
 Addsimps [min_0L,min_0R,min_Suc_Suc];
+
+Goalw [max_def] "max 0 n = n";
+by (Simp_tac 1);
+qed "max_0L";
+
+Goalw [max_def] "max n 0 = n";
+by (Simp_tac 1);
+qed "max_0R";
+
+Goalw [max_def] "max (Suc m) (Suc n) = Suc(max m n)";
+by (Simp_tac 1);
+qed "max_Suc_Suc";
+
+Addsimps [max_0L,max_0R,max_Suc_Suc];
diff -r cdde45202c5c -r 228237ec56e5 src/HOL/Ord.ML
--- a/src/HOL/Ord.ML	Wed Apr 14 19:07:39 1999 +0200
+++ b/src/HOL/Ord.ML	Thu Apr 15 18:10:37 1999 +0200
@@ -126,6 +126,16 @@
 
 (** min & max **)
 
+Goalw [min_def] "min (x::'a::order) x = x";
+by(Simp_tac 1);
+qed "min_same";
+Addsimps [min_same];
+
+Goalw [max_def] "max (x::'a::order) x = x";
+by(Simp_tac 1);
+qed "max_same";
+Addsimps [max_same];
+
 Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)";
 by (Simp_tac 1);
 by (cut_facts_tac [linorder_linear] 1);
@@ -145,6 +155,13 @@
 qed "max_le_iff_conj";
 Addsimps [max_le_iff_conj];
 
+Goalw [max_def] "!!z::'a::linorder. (max x y < z) = (x < z & y < z)";
+by (simp_tac (simpset() addsimps [order_le_less]) 1);
+by (cut_facts_tac [linorder_less_linear] 1);
+by (blast_tac (claset() addIs [order_less_trans]) 1);
+qed "max_less_iff_conj";
+Addsimps [max_less_iff_conj];
+
 Goalw [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)";
 by (Simp_tac 1);
 by (cut_facts_tac [linorder_linear] 1);
@@ -153,6 +170,13 @@
 Addsimps [le_min_iff_conj];
 (* AddIffs screws up a blast_tac in MiniML *)
 
+Goalw [min_def] "!!z::'a::linorder. (z < min x y) = (z < x & z < y)";
+by (simp_tac (simpset() addsimps [order_le_less]) 1);
+by (cut_facts_tac [linorder_less_linear] 1);
+by (blast_tac (claset() addIs [order_less_trans]) 1);
+qed "min_less_iff_conj";
+Addsimps [min_less_iff_conj];
+
 Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)";
 by (Simp_tac 1);
 by (cut_facts_tac [linorder_linear] 1);
diff -r cdde45202c5c -r 228237ec56e5 src/HOL/WF.ML
--- a/src/HOL/WF.ML	Wed Apr 14 19:07:39 1999 +0200
+++ b/src/HOL/WF.ML	Thu Apr 15 18:10:37 1999 +0200
@@ -235,6 +235,10 @@
 by (simp_tac (simpset() addsimps [trancl_converse]) 1);
 qed "acyclic_converse";
 
+Goalw [acyclic_def] "[| acyclic s; r <= s |] ==> acyclic r";
+by(blast_tac (claset() addIs [trancl_mono]) 1);
+qed "acyclic_subset";
+
 (** cut **)
 
 (*This rewrite rule works upon formulae; thus it requires explicit use of