Introduced normalize_thm into HOL.ML

Corrected some dependencies among Sum, Prod and mono.

Extended RelPow

--- a/src/HOL/HOL.ML	Mon Feb 19 13:54:15 1996 +0100
+++ b/src/HOL/HOL.ML	Mon Feb 19 18:04:41 1996 +0100
@@ -272,24 +272,34 @@
 
 local
 
-(* work around instantiation bug *)
+(* Use XXX to avoid forall_intr failing because of duplicate variable name *)
 val myspec = read_instantiate [("P","?XXX")] spec;
 val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
 val cvx = cterm_of (#sign(rep_thm myspec)) vx;
 val aspec = forall_intr cvx myspec;
 
-fun specf th a =
-  let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))
-  in th RS forall_elim ca aspec end;
-
-fun spec_mpf th = case concl_of th of
-                    _ $ (Const("All",_) $ Abs(a,_,_)) => spec_mpf (specf th a)
-                  | _ $ (Const("op -->",_)$_$_) => spec_mpf (th RS mp)
-                  | _ => th
-
 in
 
-fun qed_spec_mp name = bind_thm(name, spec_mpf(result()));
+fun RSspec th =
+  (case concl_of th of
+     _ $ (Const("All",_) $ Abs(a,_,_)) =>
+         let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))
+         in th RS forall_elim ca aspec end
+  | _ => raise THM("RSspec",0,[th]));
+
+fun RSmp th =
+  (case concl_of th of
+     _ $ (Const("op -->",_)$_$_) => th RS mp
+  | _ => raise THM("RSmp",0,[th]));
+
+fun normalize_thm funs =
+let fun trans [] th = th
+      | trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
+in trans funs end;
+
+fun qed_spec_mp name =
+  let val thm = normalize_thm [RSspec,RSmp] (result())
+  in bind_thm(name, thm) end;
 
 end;
 

--- a/src/HOL/Prod.ML	Mon Feb 19 13:54:15 1996 +0100
+++ b/src/HOL/Prod.ML	Mon Feb 19 18:04:41 1996 +0100
@@ -224,6 +224,15 @@
     (rtac (major RS SigmaD1) 1),
     (rtac (major RS SigmaD2) 1) ]);
 
+val prems = goal Prod.thy
+    "[| A<=C;  !!x. x:A ==> B<=D |] ==> Sigma A (%x.B) <= Sigma C (%x.D)";
+by (cut_facts_tac prems 1);
+by (fast_tac (set_cs addIs (prems RL [subsetD]) 
+                     addSIs [SigmaI] 
+                     addSEs [SigmaE]) 1);
+qed "Sigma_mono";
+
+
 (*** Domain of a relation ***)
 
 val prems = goalw Prod.thy [image_def] "(a,b) : r ==> a : fst``r";

--- a/src/HOL/ROOT.ML	Mon Feb 19 13:54:15 1996 +0100
+++ b/src/HOL/ROOT.ML	Mon Feb 19 18:04:41 1996 +0100
@@ -29,7 +29,6 @@
 use     "typedef.ML";
 use_thy "Sum";
 use_thy "Gfp";
-use_thy "RelPow";
 
 use "datatype.ML";
 use "ind_syntax.ML";
@@ -38,6 +37,7 @@
 use "indrule.ML";
 use_thy "Inductive";
 
+use_thy "RelPow";
 use_thy "Finite";
 use_thy "Sexp";
 use_thy "List";

--- a/src/HOL/RelPow.ML	Mon Feb 19 13:54:15 1996 +0100
+++ b/src/HOL/RelPow.ML	Mon Feb 19 18:04:41 1996 +0100
@@ -7,50 +7,70 @@
 open RelPow;
 
 val [rel_pow_0, rel_pow_Suc] = nat_recs rel_pow_def;
-Addsimps [rel_pow_0, rel_pow_Suc];
+Addsimps [rel_pow_0];
 
 goal RelPow.thy "(x,x) : R^0";
 by(Simp_tac 1);
 qed "rel_pow_0_I";
 
 goal RelPow.thy "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
-by(Simp_tac 1);
+by(simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
 by(fast_tac comp_cs 1);
 qed "rel_pow_Suc_I";
 
 goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
 by(nat_ind_tac "n" 1);
-by(Simp_tac 1);
+by(simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
 by(fast_tac comp_cs 1);
-by(Asm_full_simp_tac 1);
+by(asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
 by(fast_tac comp_cs 1);
 qed_spec_mp "rel_pow_Suc_I2";
 
+goal RelPow.thy "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P";
+by(Asm_full_simp_tac 1);
+qed "rel_pow_0_E";
+
+val [major,minor] = goal RelPow.thy
+  "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
+by(cut_facts_tac [major] 1);
+by(asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
+by(fast_tac (comp_cs addIs [minor]) 1);
+qed "rel_pow_Suc_E";
+
+val [p1,p2,p3] = goal RelPow.thy
+    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
+\       !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P  \
+\    |] ==> P";
+by(res_inst_tac [("n","n")] natE 1);
+by(cut_facts_tac [p1] 1);
+by(asm_full_simp_tac (!simpset addsimps [p2]) 1);
+by(cut_facts_tac [p1] 1);
+by(Asm_full_simp_tac 1);
+be rel_pow_Suc_E 1;
+by(REPEAT(ares_tac [p3] 1));
+qed "rel_pow_E";
+
 goal RelPow.thy "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
 by(nat_ind_tac "n" 1);
-by(Simp_tac 1);
-by(fast_tac comp_cs 1);
-by(Asm_full_simp_tac 1);
-by(fast_tac comp_cs 1);
-val lemma = result() RS spec RS spec RS mp;
-
-goal RelPow.thy
-  "(x,z) : R^n --> (n=0 --> x=z --> P) --> \
-\     (!y m. n = Suc m --> (x,y):R --> (y,z):R^m --> P) --> P";
-by(res_inst_tac [("n","n")] natE 1);
-by(Asm_simp_tac 1);
-by(hyp_subst_tac 1);
-by(fast_tac (HOL_cs addDs [lemma]) 1);
-val lemma = result() RS mp RS mp RS mp;
+by(fast_tac (HOL_cs addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
+by(fast_tac (HOL_cs addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
+qed_spec_mp "rel_pow_Suc_D2";
 
 val [p1,p2,p3] = goal RelPow.thy
     "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
 \       !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P  \
 \    |] ==> P";
-br (p1 RS lemma) 1;
-by(REPEAT(ares_tac [impI,p2] 1));
-by(REPEAT(ares_tac [allI,impI,p3] 1));
-qed "UN_rel_powE2";
+by(res_inst_tac [("n","n")] natE 1);
+by(cut_facts_tac [p1] 1);
+by(asm_full_simp_tac (!simpset addsimps [p2]) 1);
+by(cut_facts_tac [p1] 1);
+by(Asm_full_simp_tac 1);
+bd rel_pow_Suc_D2 1;
+be exE 1;
+be p3 1;
+be conjunct1 1;
+be conjunct2 1;
+qed "rel_pow_E2";
 
 goal RelPow.thy "!!p. p:R^* ==> p : (UN n. R^n)";
 by(split_all_tac 1);
@@ -60,17 +80,15 @@
 
 goal RelPow.thy "!y. (x,y):R^n --> (x,y):R^*";
 by(nat_ind_tac "n" 1);
-by(Simp_tac 1);
-by(fast_tac (HOL_cs addIs [rtrancl_refl]) 1);
-by(Simp_tac 1);
-by(fast_tac (trancl_cs addEs [rtrancl_into_rtrancl]) 1);
+by(fast_tac (HOL_cs addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
+by(fast_tac (trancl_cs addEs [rel_pow_Suc_E,rtrancl_into_rtrancl]) 1);
 val lemma = result() RS spec RS mp;
 
 goal RelPow.thy "!!p. p:R^n ==> p:R^*";
 by(split_all_tac 1);
 be lemma 1;
-qed "UN_rel_pow_imp_rtrancl";
+qed "rel_pow_imp_rtrancl";
 
 goal RelPow.thy "R^* = (UN n. R^n)";
-by(fast_tac (eq_cs addIs [rtrancl_imp_UN_rel_pow,UN_rel_pow_imp_rtrancl]) 1);
+by(fast_tac (eq_cs addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);
 qed "rtrancl_is_UN_rel_pow";

--- a/src/HOL/Sum.ML	Mon Feb 19 13:54:15 1996 +0100
+++ b/src/HOL/Sum.ML	Mon Feb 19 18:04:41 1996 +0100
@@ -193,6 +193,8 @@
 by (fast_tac (set_cs addSIs [PartI] addSEs [PartE]) 1);
 qed "Part_mono";
 
+val basic_monos = basic_monos @ [Part_mono];
+
 goalw Sum.thy [Part_def] "!!a. a : Part A h ==> a : A";
 by (etac IntD1 1);
 qed "PartD1";

--- a/src/HOL/Sum.thy	Mon Feb 19 13:54:15 1996 +0100
+++ b/src/HOL/Sum.thy	Mon Feb 19 18:04:41 1996 +0100
@@ -6,7 +6,7 @@
 The disjoint sum of two types.
 *)
 
-Sum = Prod +
+Sum = mono + Prod +
 
 (* type definition *)
 

--- a/src/HOL/mono.ML	Mon Feb 19 13:54:15 1996 +0100
+++ b/src/HOL/mono.ML	Mon Feb 19 18:04:41 1996 +0100
@@ -61,15 +61,6 @@
 by (fast_tac set_cs 1);
 qed "Compl_anti_mono";
 
-val prems = goal Prod.thy
-    "[| A<=C;  !!x. x:A ==> B<=D |] ==> Sigma A (%x.B) <= Sigma C (%x.D)";
-by (cut_facts_tac prems 1);
-by (fast_tac (set_cs addIs (prems RL [subsetD]) 
-                     addSIs [SigmaI] 
-                     addSEs [SigmaE]) 1);
-qed "Sigma_mono";
-
-
 (** Monotonicity of implications.  For inductive definitions **)
 
 goal Set.thy "!!A B x. A<=B ==> x:A --> x:B";
@@ -119,5 +110,5 @@
 
 (*Used in intr_elim.ML and in individual datatype definitions*)
 val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 
-                   ex_mono, Collect_mono, Part_mono, in_mono];
+                   ex_mono, Collect_mono, in_mono];