# HG changeset patch
# User oheimb
# Date 829756798 -7200
# Node ID 8cb42cd9757922f59c0ac1aadc88d19c1ba5e18b
# Parent  41e37e5211f2dda8c05a87ff78a7f2cdfb1eeef1
*** empty log message ***

diff -r 41e37e5211f2 -r 8cb42cd97579 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Wed Apr 17 11:46:10 1996 +0200
+++ b/src/HOL/Arith.ML	Wed Apr 17 17:59:58 1996 +0200
@@ -157,7 +157,7 @@
 val [prem] = goal Arith.thy "[| ~ m<n |] ==> n+(m-n) = (m::nat)";
 by (rtac (prem RS rev_mp) 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (Asm_simp_tac));
 qed "add_diff_inverse";
 
 
@@ -166,7 +166,7 @@
 goal Arith.thy "m - n < Suc(m)";
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (etac less_SucE 3);
-by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
 qed "diff_less_Suc";
 
 goal Arith.thy "!!m::nat. m - n <= m";
@@ -236,7 +236,7 @@
 by (res_inst_tac [("n","m")] less_induct 1);
 by (rename_tac "k" 1);    (*Variable name used in line below*)
 by (case_tac "k<n" 1);
-by (ALLGOALS (asm_simp_tac(!simpset addsimps (add_ac @
+by (ALLGOALS (asm_simp_tac(!simpset addsimps ([add_assoc] @
                        [mod_less, mod_geq, div_less, div_geq,
                         add_diff_inverse, diff_less]))));
 qed "mod_div_equality";
@@ -247,7 +247,8 @@
 val [prem] = goal Arith.thy "m < Suc(n) ==> m-n = 0";
 by (rtac (prem RS rev_mp) 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
+by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
+by (ALLGOALS (Asm_simp_tac));
 qed "less_imp_diff_is_0";
 
 val prems = goal Arith.thy "m-n = 0  -->  n-m = 0  -->  m=n";
@@ -258,13 +259,13 @@
 val [prem] = goal Arith.thy "m<n ==> 0<n-m";
 by (rtac (prem RS rev_mp) 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (Asm_simp_tac));
 qed "less_imp_diff_positive";
 
 val [prem] = goal Arith.thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
 by (rtac (prem RS rev_mp) 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (Asm_simp_tac));
 qed "Suc_diff_n";
 
 goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
@@ -346,7 +347,8 @@
 
 goal Arith.thy "!!m. m<n --> (? k. n=Suc(m+k))";
 by (nat_ind_tac "n" 1);
-by (ALLGOALS(Simp_tac));
+by (Simp_tac 1);
+by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
 by (REPEAT_FIRST (ares_tac [conjI, impI]));
 by (res_inst_tac [("x","0")] exI 2);
 by (Simp_tac 2);
diff -r 41e37e5211f2 -r 8cb42cd97579 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Wed Apr 17 11:46:10 1996 +0200
+++ b/src/HOL/Finite.ML	Wed Apr 17 17:59:58 1996 +0200
@@ -73,7 +73,8 @@
 by (rtac (major RS Fin_induct) 1);
 by (Simp_tac 1);
 by (asm_simp_tac
-    (!simpset addsimps [image_eqI RS Fin.insertI, image_insert]) 1);
+    (!simpset addsimps [image_eqI RS Fin.insertI, image_insert]
+	      delsimps [insert_Fin]) 1);
 qed "Fin_imageI";
 
 val major::prems = goal Finite.thy 
@@ -181,7 +182,7 @@
 by (hyp_subst_tac 1);
 by (res_inst_tac [("x","Suc n")] exI 1);
 by (res_inst_tac [("x","%i. if i<n then f i else x")] exI 1);
-by (asm_simp_tac (!simpset addsimps [Collect_conv_insert]
+by (asm_simp_tac (!simpset addsimps [Collect_conv_insert, less_Suc_eq]
                           addcongs [rev_conj_cong]) 1);
 qed "finite_has_card";
 
@@ -198,14 +199,14 @@
  by (Simp_tac 2);
  by (fast_tac eq_cs 2);
 by (etac exE 1);
-by (Simp_tac 1);
+by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
 by (rtac exI 1);
 by (rtac conjI 1);
  br disjI2 1;
  br refl 1;
 by (etac equalityE 1);
 by (asm_full_simp_tac
-     (!simpset addsimps [subset_insert,Collect_conv_insert]) 1);
+     (!simpset addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1);
 by (SELECT_GOAL(safe_tac eq_cs)1);
   by (Asm_full_simp_tac 1);
   by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
@@ -259,7 +260,8 @@
  by (res_inst_tac
    [("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1);
  by (simp_tac
-    (!simpset addsimps [Collect_conv_insert] addcongs [rev_conj_cong]) 1);
+    (!simpset addsimps [Collect_conv_insert, less_Suc_eq] 
+	      addcongs [rev_conj_cong]) 1);
  be subst 1;
  br refl 1;
 by (rtac notI 1);
@@ -270,7 +272,7 @@
 by (etac conjE 1);
 by (dres_inst_tac [("P","%x. ? g. A = {g i |i. i < x}")] Least_le 1);
 by (dtac le_less_trans 1 THEN atac 1);
-by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
 by (etac disjE 1);
 by (etac less_asym 1 THEN atac 1);
 by (hyp_subst_tac 1);
diff -r 41e37e5211f2 -r 8cb42cd97579 src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Wed Apr 17 11:46:10 1996 +0200
+++ b/src/HOL/HOL.ML	Wed Apr 17 17:59:58 1996 +0200
@@ -11,6 +11,7 @@
 
 
 (** Equality **)
+section "=";
 
 qed_goal "sym" HOL.thy "s=t ==> t=s"
  (fn prems => [cut_facts_tac prems 1, etac subst 1, rtac refl 1]);
@@ -34,7 +35,9 @@
     (rtac sym 1),
     (REPEAT (resolve_tac prems 1)) ]);
 
+
 (** Congruence rules for meta-application **)
+section "Congruence";
 
 (*similar to AP_THM in Gordon's HOL*)
 qed_goal "fun_cong" HOL.thy "(f::'a=>'b) = g ==> f(x)=g(x)"
@@ -49,7 +52,9 @@
  (fn [prem1,prem2] =>
    [rtac (prem1 RS subst) 1, rtac (prem2 RS subst) 1, rtac refl 1]);
 
+
 (** Equality of booleans -- iff **)
+section "iff";
 
 qed_goal "iffI" HOL.thy
    "[| P ==> Q;  Q ==> P |] ==> P=Q"
@@ -65,7 +70,9 @@
     "[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R"
  (fn [p1,p2] => [REPEAT(ares_tac([p1 RS iffD2, p1 RS iffD1, p2, impI])1)]);
 
+
 (** True **)
+section "True";
 
 qed_goalw "TrueI" HOL.thy [True_def] "True"
   (fn _ => [rtac refl 1]);
@@ -76,7 +83,9 @@
 qed_goal "eqTrueE" HOL.thy "P=True ==> P" 
  (fn prems => [REPEAT(resolve_tac (prems@[TrueI,iffD2]) 1)]);
 
+
 (** Universal quantifier **)
+section "!";
 
 qed_goalw "allI" HOL.thy [All_def] "(!!x::'a. P(x)) ==> !x. P(x)"
  (fn prems => [resolve_tac (prems RL [eqTrueI RS ext]) 1]);
@@ -96,6 +105,7 @@
 
 (** False ** Depends upon spec; it is impossible to do propositional logic
              before quantifiers! **)
+section "False";
 
 qed_goalw "FalseE" HOL.thy [False_def] "False ==> P"
  (fn [major] => [rtac (major RS spec) 1]);
@@ -105,6 +115,7 @@
 
 
 (** Negation **)
+section "~";
 
 qed_goalw "notI" HOL.thy [not_def] "(P ==> False) ==> ~P"
  (fn prems=> [rtac impI 1, eresolve_tac prems 1]);
@@ -112,7 +123,9 @@
 qed_goalw "notE" HOL.thy [not_def] "[| ~P;  P |] ==> R"
  (fn prems => [rtac (prems MRS mp RS FalseE) 1]);
 
+
 (** Implication **)
+section "-->";
 
 qed_goal "impE" HOL.thy "[| P-->Q;  P;  Q ==> R |] ==> R"
  (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
@@ -135,6 +148,7 @@
 
 
 (** Existential quantifier **)
+section "?";
 
 qed_goalw "exI" HOL.thy [Ex_def] "P(x) ==> ? x::'a.P(x)"
  (fn prems => [rtac selectI 1, resolve_tac prems 1]);
@@ -145,6 +159,7 @@
 
 
 (** Conjunction **)
+section "&";
 
 qed_goalw "conjI" HOL.thy [and_def] "[| P; Q |] ==> P&Q"
  (fn prems =>
@@ -163,7 +178,9 @@
          [cut_facts_tac prems 1, resolve_tac prems 1,
           etac conjunct1 1, etac conjunct2 1]);
 
+
 (** Disjunction *)
+section "|";
 
 qed_goalw "disjI1" HOL.thy [or_def] "P ==> P|Q"
  (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
@@ -176,7 +193,9 @@
         [rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,
          rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 1]);
 
+
 (** CCONTR -- classical logic **)
+section "classical logic";
 
 qed_goalw "classical" HOL.thy [not_def]  "(~P ==> P) ==> P"
  (fn [prem] =>
@@ -191,11 +210,23 @@
  (fn [major]=>
   [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
 
+qed_goal "contrapos2" HOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
+	rtac classical 1,
+	dtac p2 1,
+	etac notE 1,
+	rtac p1 1]);
+
+qed_goal "swap2" HOL.thy "[| P;  Q ==> ~ P |] ==> ~ Q" (fn [p1,p2] => [
+	rtac notI 1,
+	dtac p2 1,
+	etac notE 1,
+	rtac p1 1]);
 
 (** Unique existence **)
+section "?!";
 
 qed_goalw "ex1I" HOL.thy [Ex1_def]
-    "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
+	    "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
  (fn prems =>
   [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
 
@@ -206,6 +237,7 @@
 
 
 (** Select: Hilbert's Epsilon-operator **)
+section "@";
 
 (*Easier to apply than selectI: conclusion has only one occurrence of P*)
 qed_goal "selectI2" HOL.thy
@@ -219,8 +251,15 @@
  (fn prems => [ rtac selectI2 1, 
                 REPEAT (ares_tac prems 1) ]);
 
+qed_goal "select_eq_Ex" HOL.thy "P (@ x. P x) =  (? x. P x)" (fn prems => [
+        rtac iffI 1,
+        etac exI 1,
+        etac exE 1,
+        etac selectI 1]);
+
 
 (** Classical intro rules for disjunction and existential quantifiers *)
+section "classical intro rules";
 
 qed_goal "disjCI" HOL.thy "(~Q ==> P) ==> P|Q"
  (fn prems=>
@@ -263,6 +302,7 @@
 
 fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
 
+
 (** Standard abbreviations **)
 
 fun stac th = rtac(th RS ssubst);
@@ -303,9 +343,13 @@
 
 end;
 
+
+
 (*** Load simpdata.ML to be able to initialize HOL's simpset ***)
 
+
 (** Applying HypsubstFun to generate hyp_subst_tac **)
+section "Classical Reasoner";
 
 structure Hypsubst_Data =
   struct
@@ -343,6 +387,9 @@
 val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
                      addSEs [exE,ex1E] addEs [allE];
 
+
+section "Simplifier";
+
 use     "simpdata.ML";
 simpset := HOL_ss;
 
diff -r 41e37e5211f2 -r 8cb42cd97579 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Wed Apr 17 11:46:10 1996 +0200
+++ b/src/HOL/Nat.ML	Wed Apr 17 17:59:58 1996 +0200
@@ -291,6 +291,14 @@
 qed "gr_implies_not0";
 Addsimps [gr_implies_not0];
 
+qed_goal "zero_less_eq" Nat.thy "0 < n = (n ~= 0)" (fn _ => [
+	rtac iffI 1,
+	etac gr_implies_not0 1,
+	rtac natE 1,
+	contr_tac 1,
+	etac ssubst 1,
+	rtac zero_less_Suc 1]);
+
 (** Inductive (?) properties **)
 
 val [prem] = goal Nat.thy "Suc(m) < n ==> m<n";
@@ -341,7 +349,8 @@
 
 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 (ALLGOALS (asm_simp_tac (!simpset)));
+by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
 by (fast_tac (HOL_cs addDs [Suc_lessD]) 1);
 qed_spec_mp "less_trans_Suc";
 
@@ -354,6 +363,17 @@
 by (fast_tac (HOL_cs addIs [lessI, Suc_mono, less_SucI] addEs [lessE]) 1);
 qed "less_linear";
 
+qed_goal "nat_less_cases" Nat.thy 
+   "[| (m::nat)<n ==> P n m; m=n ==> P n m; n<m ==> P n m |] ==> P n m"
+( fn prems =>
+        [
+        (res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1),
+        (etac disjE 2),
+        (etac (hd (tl (tl prems))) 1),
+        (etac (sym RS hd (tl prems)) 1),
+        (etac (hd prems) 1)
+        ]);
+
 (*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);
@@ -384,7 +404,7 @@
 qed "le_0";
 
 Addsimps [less_not_refl,
-          less_Suc_eq, le0, le_0,
+          (*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];
@@ -417,12 +437,12 @@
 qed "not_leE";
 
 goalw Nat.thy [le_def] "!!m. m < n ==> Suc(m) <= n";
-by (Simp_tac 1);
+by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
 by (fast_tac (HOL_cs addEs [less_irrefl,less_asym]) 1);
 qed "lessD";
 
 goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
-by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
 by (fast_tac HOL_cs 1);
 qed "Suc_leD";
 
@@ -519,3 +539,28 @@
 by (etac (rewrite_rule [le_def] Least_le RS notE) 1);
 by (rtac prem 1);
 qed "not_less_Least";
+
+qed_goalw "Least_Suc" Nat.thy [Least_def]
+ "[| ? n. P (Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P (Suc m))"
+ (fn prems => [
+	cut_facts_tac prems 1,
+	rtac select_equality 1,
+	fold_goals_tac [Least_def],
+	safe_tac (HOL_cs addSEs [LeastI]),
+	res_inst_tac [("n","j")] natE 1,
+	fast_tac HOL_cs 1,
+	fast_tac (HOL_cs addDs [Suc_less_SucD] addDs [not_less_Least]) 1,	
+	res_inst_tac [("n","k")] natE 1,
+	fast_tac HOL_cs 1,
+	hyp_subst_tac 1,
+	rewtac Least_def,
+	rtac (select_equality RS arg_cong RS sym) 1,
+	safe_tac HOL_cs,
+	dtac Suc_mono 1,
+	fast_tac HOL_cs 1,
+	cut_facts_tac [less_linear] 1,
+	safe_tac HOL_cs,
+	atac 2,
+	fast_tac HOL_cs 2,
+	dtac Suc_mono 1,
+	fast_tac HOL_cs 1]);
diff -r 41e37e5211f2 -r 8cb42cd97579 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Apr 17 11:46:10 1996 +0200
+++ b/src/HOL/Nat.thy	Wed Apr 17 17:59:58 1996 +0200
@@ -76,4 +76,7 @@
   (*least number operator*)
   Least_def     "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
 
+(* start 8bit 1 *)
+(* end 8bit 1 *)
+
 end
diff -r 41e37e5211f2 -r 8cb42cd97579 src/HOL/Prod.thy
--- a/src/HOL/Prod.thy	Wed Apr 17 11:46:10 1996 +0200
+++ b/src/HOL/Prod.thy	Wed Apr 17 17:59:58 1996 +0200
@@ -53,10 +53,16 @@
 
   "%(x,y,zs).b"   == "split(%x (y,zs).b)"
   "%(x,y).b"      == "split(%x y.b)"
+(*<<<<<<< Prod.thy*)
+(* The <= direction fails if split has more than one argument because
+   ast-matching fails. Otherwise it would work fine *)
+
+(*=======*)
 
   "SIGMA x:A. B"  =>  "Sigma A (%x.B)"
   "A Times B"     =>  "Sigma A (_K B)"
 
+(*>>>>>>> 1.13*)
 defs
   Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
   fst_def       "fst(p) == @a. ? b. p = (a, b)"
@@ -80,8 +86,39 @@
 (* end 8bit 1 *)
 
 end
+(*<<<<<<< Prod.thy*)
+(*
+ML
+
+local open Syntax
+
+fun pttrn(_ $ s $ t) = const"@pttrn" $ s $ t;
+fun pttrns s t = const"@pttrns" $ s $ t;
+
+fun split2(Abs(x,T,t)) =
+      let val (pats,u) = split1 t
+      in (pttrns (Free(x,T)) pats, subst_bounds([free x],u)) end
+  | split2(Const("split",_) $ r) =
+      let val (pats,s) = split2(r)
+          val (pats2,t) = split1(s)
+      in (pttrns (pttrn pats) pats2, t) end
+and split1(Abs(x,T,t)) =  (Free(x,T), subst_bounds([free x],t))
+  | split1(Const("split",_)$t) = split2(t);
+
+fun split_tr'(t::args) =
+  let val (pats,ft) = split2(t)
+  in list_comb(const"_lambda" $ pttrn pats $ ft, args) end;
+
+in
+
+val print_translation = [("split", split_tr')];
+
+end;
+*)
+(*=======*)
 
 ML
 
 val print_translation = [("Sigma", dependent_tr' ("@Sigma", "@Times"))];
 
+(*>>>>>>> 1.13*)
diff -r 41e37e5211f2 -r 8cb42cd97579 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Wed Apr 17 11:46:10 1996 +0200
+++ b/src/HOL/equalities.ML	Wed Apr 17 17:59:58 1996 +0200
@@ -69,7 +69,7 @@
 by (fast_tac eq_cs 1);
 qed "mk_disjoint_insert";
 
-section "''";
+section "``";
 
 goal Set.thy "f``{} = {}";
 by (fast_tac eq_cs 1);
@@ -81,6 +81,19 @@
 qed "image_insert";
 Addsimps[image_insert];
 
+qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
+ (fn _ => [fast_tac set_cs 1]);
+
+section "range";
+
+qed_goal "ball_range" Set.thy "(!y:range f. P y) = (!x. P (f x))"
+ (fn _ => [fast_tac set_cs 1]);
+
+qed_goalw "image_range" Set.thy [image_def, range_def]
+ "f``range g = range (%x. f (g x))" (fn _ => [
+	rtac Collect_cong 1,
+	fast_tac set_cs 1]);
+
 section "Int";
 
 goal Set.thy "A Int A = A";
diff -r 41e37e5211f2 -r 8cb42cd97579 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Apr 17 11:46:10 1996 +0200
+++ b/src/HOL/simpdata.ML	Wed Apr 17 17:59:58 1996 +0200
@@ -181,6 +181,9 @@
 prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)";
 prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
 
+prove "not_all" "(~ (! x.P(x))) = (? x.~P(x))";
+prove "not_ex"  "(~ (? x.P(x))) = (! x.~P(x))";
+
 prove "ex_disj_distrib" "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))";
 prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";