converted to Isar therory, adding attributes complete_split and split_format
authoroheimb
Thu Feb 01 20:51:48 2001 +0100 (2001-02-01)
changeset 11025a70b796d9af8
parent 11024 23bf8d787b04
child 11026 a50365d21144
converted to Isar therory, adding attributes complete_split and split_format
src/HOL/Induct/LList.ML
src/HOL/Modelcheck/MuckeSyn.ML
src/HOL/Product_Type.thy
src/HOL/Product_Type_lemmas.ML
src/HOL/Tools/split_rule.ML
src/HOL/ex/cla.ML
src/HOLCF/Cprod1.ML
     1.1 --- a/src/HOL/Induct/LList.ML	Thu Feb 01 20:51:13 2001 +0100
     1.2 +++ b/src/HOL/Induct/LList.ML	Thu Feb 01 20:51:48 2001 +0100
     1.3 @@ -782,7 +782,7 @@
     1.4  by (ALLGOALS Asm_simp_tac);
     1.5  qed "fun_power_Suc";
     1.6  
     1.7 -val Pair_cong = read_instantiate_sg (sign_of Product_Type.thy)
     1.8 +val Pair_cong = read_instantiate_sg (sign_of (theory "Product_Type"))
     1.9   [("f","Pair")] (standard(refl RS cong RS cong));
    1.10  
    1.11  (*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}
     2.1 --- a/src/HOL/Modelcheck/MuckeSyn.ML	Thu Feb 01 20:51:13 2001 +0100
     2.2 +++ b/src/HOL/Modelcheck/MuckeSyn.ML	Thu Feb 01 20:51:48 2001 +0100
     2.3 @@ -147,7 +147,7 @@
     2.4  
     2.5  (* first simplification, then model checking *)
     2.6  
     2.7 -goalw Product_Type.thy [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
     2.8 +goalw (theory "Product_Type") [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
     2.9    by (rtac ext 1);
    2.10    by (stac (surjective_pairing RS sym) 1);
    2.11    by (rtac refl 1);
     3.1 --- a/src/HOL/Product_Type.thy	Thu Feb 01 20:51:13 2001 +0100
     3.2 +++ b/src/HOL/Product_Type.thy	Thu Feb 01 20:51:48 2001 +0100
     3.3 @@ -7,7 +7,11 @@
     3.4  The unit type.
     3.5  *)
     3.6  
     3.7 -Product_Type = Fun +
     3.8 +theory Product_Type = Fun
     3.9 +files 
    3.10 +  ("Tools/split_rule.ML")
    3.11 +  ("Product_Type_lemmas.ML")
    3.12 +:
    3.13  
    3.14  
    3.15  (** products **)
    3.16 @@ -15,31 +19,34 @@
    3.17  (* type definition *)
    3.18  
    3.19  constdefs
    3.20 -  Pair_Rep      :: ['a, 'b] => ['a, 'b] => bool
    3.21 -  "Pair_Rep == (%a b. %x y. x=a & y=b)"
    3.22 +  Pair_Rep :: "['a, 'b] => ['a, 'b] => bool"
    3.23 + "Pair_Rep == (%a b. %x y. x=a & y=b)"
    3.24  
    3.25  global
    3.26  
    3.27  typedef (Prod)
    3.28    ('a, 'b) "*"          (infixr 20)
    3.29      = "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}"
    3.30 +proof
    3.31 +  fix a b show "Pair_Rep a b : ?Prod"
    3.32 +    by blast
    3.33 +qed
    3.34  
    3.35  syntax (symbols)
    3.36 -  "*"           :: [type, type] => type         ("(_ \\<times>/ _)" [21, 20] 20)
    3.37 -
    3.38 +  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
    3.39  syntax (HTML output)
    3.40 -  "*"           :: [type, type] => type         ("(_ \\<times>/ _)" [21, 20] 20)
    3.41 +  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
    3.42  
    3.43  
    3.44  (* abstract constants and syntax *)
    3.45  
    3.46  consts
    3.47 -  fst           :: "'a * 'b => 'a"
    3.48 -  snd           :: "'a * 'b => 'b"
    3.49 -  split         :: "[['a, 'b] => 'c, 'a * 'b] => 'c"
    3.50 -  prod_fun      :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd"
    3.51 -  Pair          :: "['a, 'b] => 'a * 'b"
    3.52 -  Sigma         :: "['a set, 'a => 'b set] => ('a * 'b) set"
    3.53 +  fst      :: "'a * 'b => 'a"
    3.54 +  snd      :: "'a * 'b => 'b"
    3.55 +  split    :: "[['a, 'b] => 'c, 'a * 'b] => 'c"
    3.56 +  prod_fun :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd"
    3.57 +  Pair     :: "['a, 'b] => 'a * 'b"
    3.58 +  Sigma    :: "['a set, 'a => 'b set] => ('a * 'b) set"
    3.59  
    3.60  
    3.61  (* patterns -- extends pre-defined type "pttrn" used in abstractions *)
    3.62 @@ -51,11 +58,11 @@
    3.63    "_tuple"      :: "'a => tuple_args => 'a * 'b"        ("(1'(_,/ _'))")
    3.64    "_tuple_arg"  :: "'a => tuple_args"                   ("_")
    3.65    "_tuple_args" :: "'a => tuple_args => tuple_args"     ("_,/ _")
    3.66 -  "_pattern"    :: [pttrn, patterns] => pttrn           ("'(_,/ _')")
    3.67 -  ""            :: pttrn => patterns                    ("_")
    3.68 -  "_patterns"   :: [pttrn, patterns] => patterns        ("_,/ _")
    3.69 -  "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3SIGMA _:_./ _)" 10)
    3.70 -  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    (infixr "<*>" 80)
    3.71 +  "_pattern"    :: "[pttrn, patterns] => pttrn"         ("'(_,/ _')")
    3.72 +  ""            :: "pttrn => patterns"                  ("_")
    3.73 +  "_patterns"   :: "[pttrn, patterns] => patterns"      ("_,/ _")
    3.74 +  "@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10)
    3.75 +  "@Times" ::"['a set,  'a => 'b set] => ('a * 'b) set" (infixr "<*>" 80)
    3.76  
    3.77  translations
    3.78    "(x, y)"       == "Pair x y"
    3.79 @@ -70,8 +77,10 @@
    3.80    "A <*> B"      => "Sigma A (_K B)"
    3.81  
    3.82  syntax (symbols)
    3.83 -  "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3\\<Sigma> _\\<in>_./ _)" 10)
    3.84 -  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ \\<times> _" [81, 80] 80)
    3.85 +  "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
    3.86 +  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
    3.87 +
    3.88 +print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))]; *}
    3.89  
    3.90  
    3.91  (* definitions *)
    3.92 @@ -79,12 +88,12 @@
    3.93  local
    3.94  
    3.95  defs
    3.96 -  Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
    3.97 -  fst_def       "fst p == @a. ? b. p = (a, b)"
    3.98 -  snd_def       "snd p == @b. ? a. p = (a, b)"
    3.99 -  split_def     "split == (%c p. c (fst p) (snd p))"
   3.100 -  prod_fun_def  "prod_fun f g == split(%x y.(f(x), g(y)))"
   3.101 -  Sigma_def     "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
   3.102 +  Pair_def:     "Pair a b == Abs_Prod(Pair_Rep a b)"
   3.103 +  fst_def:      "fst p == @a. ? b. p = (a, b)"
   3.104 +  snd_def:      "snd p == @b. ? a. p = (a, b)"
   3.105 +  split_def:    "split == (%c p. c (fst p) (snd p))"
   3.106 +  prod_fun_def: "prod_fun f g == split(%x y.(f(x), g(y)))"
   3.107 +  Sigma_def:    "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
   3.108  
   3.109  
   3.110  
   3.111 @@ -92,7 +101,11 @@
   3.112  
   3.113  global
   3.114  
   3.115 -typedef  unit = "{True}"
   3.116 +typedef  unit = "{True}" 
   3.117 +proof
   3.118 +  show "True : ?unit"
   3.119 +    by blast
   3.120 +qed
   3.121  
   3.122  consts
   3.123    "()"          :: unit                           ("'(')")
   3.124 @@ -100,10 +113,11 @@
   3.125  local
   3.126  
   3.127  defs
   3.128 -  Unity_def     "() == Abs_unit True"
   3.129 +  Unity_def:    "() == Abs_unit True"
   3.130 +
   3.131 +use "Product_Type_lemmas.ML"
   3.132 +
   3.133 +use "Tools/split_rule.ML"
   3.134 +setup split_attributes
   3.135  
   3.136  end
   3.137 -
   3.138 -ML
   3.139 -
   3.140 -val print_translation = [("Sigma", dependent_tr' ("@Sigma", "@Times"))];
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Product_Type_lemmas.ML	Thu Feb 01 20:51:48 2001 +0100
     4.3 @@ -0,0 +1,584 @@
     4.4 +(*  Title:      HOL/Product_Type_lemmas.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Copyright   1991  University of Cambridge
     4.8 +
     4.9 +Ordered Pairs, the Cartesian product type, the unit type
    4.10 +*)
    4.11 +
    4.12 +(* ML bindings *)
    4.13 +val Pair_def  = thm "Pair_def";
    4.14 +val fst_def   = thm "fst_def";
    4.15 +val snd_def   = thm "snd_def";
    4.16 +val split_def = thm "split_def";
    4.17 +val prod_fun_def = thm "prod_fun_def";
    4.18 +val Sigma_def = thm "Sigma_def";
    4.19 +val Unity_def = thm "Unity_def";
    4.20 +
    4.21 +
    4.22 +(** unit **)
    4.23 +
    4.24 +Goalw [Unity_def] "u = ()";
    4.25 +by (stac (rewrite_rule [thm"unit_def"] (thm"Rep_unit") RS singletonD RS sym) 1);
    4.26 +by (rtac (thm "Rep_unit_inverse" RS sym) 1);
    4.27 +qed "unit_eq";
    4.28 +
    4.29 +(*simplification procedure for unit_eq.
    4.30 +  Cannot use this rule directly -- it loops!*)
    4.31 +local
    4.32 +  val unit_pat = Thm.cterm_of (Theory.sign_of (the_context ())) (Free ("x", HOLogic.unitT));
    4.33 +  val unit_meta_eq = standard (mk_meta_eq unit_eq);
    4.34 +  fun proc _ _ t =
    4.35 +    if HOLogic.is_unit t then None
    4.36 +    else Some unit_meta_eq;
    4.37 +in
    4.38 +  val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc;
    4.39 +end;
    4.40 +
    4.41 +Addsimprocs [unit_eq_proc];
    4.42 +
    4.43 +Goal "(!!x::unit. PROP P x) == PROP P ()";
    4.44 +by (Simp_tac 1);
    4.45 +qed "unit_all_eq1";
    4.46 +
    4.47 +Goal "(!!x::unit. PROP P) == PROP P";
    4.48 +by (rtac triv_forall_equality 1);
    4.49 +qed "unit_all_eq2";
    4.50 +
    4.51 +Goal "P () ==> P x";
    4.52 +by (Simp_tac 1);
    4.53 +qed "unit_induct";
    4.54 +
    4.55 +(*This rewrite counters the effect of unit_eq_proc on (%u::unit. f u),
    4.56 +  replacing it by f rather than by %u.f(). *)
    4.57 +Goal "(%u::unit. f()) = f";
    4.58 +by (rtac ext 1);
    4.59 +by (Simp_tac 1);
    4.60 +qed "unit_abs_eta_conv";
    4.61 +Addsimps [unit_abs_eta_conv];
    4.62 +
    4.63 +
    4.64 +(** prod **)
    4.65 +
    4.66 +Goalw [thm "Prod_def"] "Pair_Rep a b : Prod";
    4.67 +by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]);
    4.68 +qed "ProdI";
    4.69 +
    4.70 +Goalw [thm "Pair_Rep_def"] "Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'";
    4.71 +by (dtac (fun_cong RS fun_cong) 1);
    4.72 +by (Blast_tac 1);
    4.73 +qed "Pair_Rep_inject";
    4.74 +
    4.75 +Goal "inj_on Abs_Prod Prod";
    4.76 +by (rtac inj_on_inverseI 1);
    4.77 +by (etac (thm "Abs_Prod_inverse") 1);
    4.78 +qed "inj_on_Abs_Prod";
    4.79 +
    4.80 +val prems = Goalw [Pair_def]
    4.81 +    "[| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R";
    4.82 +by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1);
    4.83 +by (REPEAT (ares_tac (prems@[ProdI]) 1));
    4.84 +qed "Pair_inject";
    4.85 +
    4.86 +Goal "((a,b) = (a',b')) = (a=a' & b=b')";
    4.87 +by (blast_tac (claset() addSEs [Pair_inject]) 1);
    4.88 +qed "Pair_eq";
    4.89 +AddIffs [Pair_eq];
    4.90 +
    4.91 +Goalw [fst_def] "fst (a,b) = a";
    4.92 +by (Blast_tac 1);
    4.93 +qed "fst_conv";
    4.94 +Goalw [snd_def] "snd (a,b) = b";
    4.95 +by (Blast_tac 1);
    4.96 +qed "snd_conv";
    4.97 +Addsimps [fst_conv, snd_conv];
    4.98 +
    4.99 +Goal "fst (x, y) = a ==> x = a";
   4.100 +by (Asm_full_simp_tac 1);
   4.101 +qed "fst_eqD";
   4.102 +Goal "snd (x, y) = a ==> y = a";
   4.103 +by (Asm_full_simp_tac 1);
   4.104 +qed "snd_eqD";
   4.105 +
   4.106 +Goalw [Pair_def] "? x y. p = (x,y)";
   4.107 +by (rtac (rewrite_rule [thm "Prod_def"] (thm "Rep_Prod") RS CollectE) 1);
   4.108 +by (EVERY1[etac exE, etac exE, rtac exI, rtac exI,
   4.109 +           rtac (thm "Rep_Prod_inverse" RS sym RS trans),  etac arg_cong]);
   4.110 +qed "PairE_lemma";
   4.111 +
   4.112 +val [prem] = Goal "[| !!x y. p = (x,y) ==> Q |] ==> Q";
   4.113 +by (rtac (PairE_lemma RS exE) 1);
   4.114 +by (REPEAT (eresolve_tac [prem,exE] 1));
   4.115 +qed "PairE";
   4.116 +
   4.117 +fun pair_tac s = EVERY' [res_inst_tac [("p",s)] PairE, hyp_subst_tac,
   4.118 +                         K prune_params_tac];
   4.119 +
   4.120 +(* Do not add as rewrite rule: invalidates some proofs in IMP *)
   4.121 +Goal "p = (fst(p),snd(p))";
   4.122 +by (pair_tac "p" 1);
   4.123 +by (Asm_simp_tac 1);
   4.124 +qed "surjective_pairing";
   4.125 +Addsimps [surjective_pairing RS sym];
   4.126 +
   4.127 +Goal "? x y. z = (x, y)";
   4.128 +by (rtac exI 1);
   4.129 +by (rtac exI 1);
   4.130 +by (rtac surjective_pairing 1);
   4.131 +qed "surj_pair";
   4.132 +Addsimps [surj_pair];
   4.133 +
   4.134 +
   4.135 +bind_thm ("split_paired_all",
   4.136 +  SplitPairedAll.rule (standard (surjective_pairing RS eq_reflection)));
   4.137 +bind_thms ("split_tupled_all", [split_paired_all, unit_all_eq2]);
   4.138 +
   4.139 +(*
   4.140 +Addsimps [split_paired_all] does not work with simplifier
   4.141 +because it also affects premises in congrence rules,
   4.142 +where is can lead to premises of the form !!a b. ... = ?P(a,b)
   4.143 +which cannot be solved by reflexivity.
   4.144 +*)
   4.145 +
   4.146 +(* replace parameters of product type by individual component parameters *)
   4.147 +local
   4.148 +  fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) =
   4.149 +        can HOLogic.dest_prodT T orelse exists_paired_all t
   4.150 +    | exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u
   4.151 +    | exists_paired_all (Abs (_, _, t)) = exists_paired_all t
   4.152 +    | exists_paired_all _ = false;
   4.153 +  val ss = HOL_basic_ss
   4.154 +    addsimps [split_paired_all, unit_all_eq2, unit_abs_eta_conv]
   4.155 +    addsimprocs [unit_eq_proc];
   4.156 +in
   4.157 +  val split_all_tac = SUBGOAL (fn (t, i) =>
   4.158 +    if exists_paired_all t then full_simp_tac ss i else no_tac);
   4.159 +  fun split_all th =
   4.160 +    if exists_paired_all (#prop (Thm.rep_thm th)) then full_simplify ss th else th;
   4.161 +end;
   4.162 +
   4.163 +claset_ref() := claset()
   4.164 +  addSWrapper ("split_all_tac", fn tac2 => split_all_tac ORELSE' tac2);
   4.165 +
   4.166 +Goal "(!x. P x) = (!a b. P(a,b))";
   4.167 +by (Fast_tac 1);
   4.168 +qed "split_paired_All";
   4.169 +Addsimps [split_paired_All];
   4.170 +(* AddIffs is not a good idea because it makes Blast_tac loop *)
   4.171 +
   4.172 +bind_thm ("prod_induct",
   4.173 +  allI RS (allI RS (split_paired_All RS iffD2)) RS spec);
   4.174 +
   4.175 +Goal "(? x. P x) = (? a b. P(a,b))";
   4.176 +by (Fast_tac 1);
   4.177 +qed "split_paired_Ex";
   4.178 +Addsimps [split_paired_Ex];
   4.179 +
   4.180 +Goalw [split_def] "split c (a,b) = c a b";
   4.181 +by (Simp_tac 1);
   4.182 +qed "split_conv";
   4.183 +Addsimps [split_conv];
   4.184 +(*bind_thm ("split", split_conv);                  (*for compatibility*)*)
   4.185 +
   4.186 +(*Subsumes the old split_Pair when f is the identity function*)
   4.187 +Goal "split (%x y. f(x,y)) = f";
   4.188 +by (rtac ext 1);
   4.189 +by (pair_tac "x" 1);
   4.190 +by (Simp_tac 1);
   4.191 +qed "split_Pair_apply";
   4.192 +
   4.193 +(*Can't be added to simpset: loops!*)
   4.194 +Goal "(SOME x. P x) = (SOME (a,b). P(a,b))";
   4.195 +by (simp_tac (simpset() addsimps [split_Pair_apply]) 1);
   4.196 +qed "split_paired_Eps";
   4.197 +
   4.198 +Goalw [split_def] "Eps (split P) = (SOME xy. P (fst xy) (snd xy))";
   4.199 +by (rtac refl 1);
   4.200 +qed "Eps_split";
   4.201 +
   4.202 +Goal "!!s t. (s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
   4.203 +by (split_all_tac 1);
   4.204 +by (Asm_simp_tac 1);
   4.205 +qed "Pair_fst_snd_eq";
   4.206 +
   4.207 +Goal "fst p = fst q ==> snd p = snd q ==> p = q";
   4.208 +by (asm_simp_tac (simpset() addsimps [Pair_fst_snd_eq]) 1);
   4.209 +qed "prod_eqI";
   4.210 +AddXIs [prod_eqI];
   4.211 +
   4.212 +(*Prevents simplification of c: much faster*)
   4.213 +Goal "p=q ==> split c p = split c q";
   4.214 +by (etac arg_cong 1);
   4.215 +qed "split_weak_cong";
   4.216 +
   4.217 +Goal "(%(x,y). f(x,y)) = f";
   4.218 +by (rtac ext 1);
   4.219 +by (split_all_tac 1);
   4.220 +by (rtac split_conv 1);
   4.221 +qed "split_eta";
   4.222 +
   4.223 +val prems = Goal "(!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g";
   4.224 +by (asm_simp_tac (simpset() addsimps prems@[split_eta]) 1);
   4.225 +qed "cond_split_eta";
   4.226 +
   4.227 +(*simplification procedure for cond_split_eta.
   4.228 +  using split_eta a rewrite rule is not general enough, and using
   4.229 +  cond_split_eta directly would render some existing proofs very inefficient.
   4.230 +  similarly for split_beta. *)
   4.231 +local
   4.232 +  fun  Pair_pat k 0 (Bound m) = (m = k)
   4.233 +  |    Pair_pat k i (Const ("Pair",  _) $ Bound m $ t) = i > 0 andalso
   4.234 +                        m = k+i andalso Pair_pat k (i-1) t
   4.235 +  |    Pair_pat _ _ _ = false;
   4.236 +  fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t
   4.237 +  |   no_args k i (t $ u) = no_args k i t andalso no_args k i u
   4.238 +  |   no_args k i (Bound m) = m < k orelse m > k+i
   4.239 +  |   no_args _ _ _ = true;
   4.240 +  fun split_pat tp i (Abs  (_,_,t)) = if tp 0 i t then Some (i,t) else None
   4.241 +  |   split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
   4.242 +  |   split_pat tp i _ = None;
   4.243 +  fun metaeq sg lhs rhs = mk_meta_eq (prove_goalw_cterm []
   4.244 +        (cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))))
   4.245 +        (K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1]));
   4.246 +  val sign = sign_of (the_context ());
   4.247 +  fun simproc name patstr = Simplifier.mk_simproc name
   4.248 +                [Thm.read_cterm sign (patstr, HOLogic.termT)];
   4.249 +
   4.250 +  val beta_patstr = "split f z";
   4.251 +  val  eta_patstr = "split f";
   4.252 +  fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
   4.253 +  |   beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
   4.254 +                        (beta_term_pat k i t andalso beta_term_pat k i u)
   4.255 +  |   beta_term_pat k i t = no_args k i t;
   4.256 +  fun  eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg
   4.257 +  |    eta_term_pat _ _ _ = false;
   4.258 +  fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t)
   4.259 +  |   subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg
   4.260 +                              else (subst arg k i t $ subst arg k i u)
   4.261 +  |   subst arg k i t = t;
   4.262 +  fun beta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t) $ arg) =
   4.263 +        (case split_pat beta_term_pat 1 t of
   4.264 +        Some (i,f) => Some (metaeq sg s (subst arg 0 i f))
   4.265 +        | None => None)
   4.266 +  |   beta_proc _ _ _ = None;
   4.267 +  fun eta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t)) =
   4.268 +        (case split_pat eta_term_pat 1 t of
   4.269 +          Some (_,ft) => Some (metaeq sg s (let val (f $ arg) = ft in f end))
   4.270 +        | None => None)
   4.271 +  |   eta_proc _ _ _ = None;
   4.272 +in
   4.273 +  val split_beta_proc = simproc "split_beta" beta_patstr beta_proc;
   4.274 +  val split_eta_proc  = simproc "split_eta"   eta_patstr  eta_proc;
   4.275 +end;
   4.276 +
   4.277 +Addsimprocs [split_beta_proc,split_eta_proc];
   4.278 +
   4.279 +Goal "(%(x,y). P x y) z = P (fst z) (snd z)";
   4.280 +by (stac surjective_pairing 1 THEN rtac split_conv 1);
   4.281 +qed "split_beta";
   4.282 +
   4.283 +(*For use with split_tac and the simplifier*)
   4.284 +Goal "R (split c p) = (! x y. p = (x,y) --> R (c x y))";
   4.285 +by (stac surjective_pairing 1);
   4.286 +by (stac split_conv 1);
   4.287 +by (Blast_tac 1);
   4.288 +qed "split_split";
   4.289 +
   4.290 +(* could be done after split_tac has been speeded up significantly:
   4.291 +simpset_ref() := simpset() addsplits [split_split];
   4.292 +   precompute the constants involved and don't do anything unless
   4.293 +   the current goal contains one of those constants
   4.294 +*)
   4.295 +
   4.296 +Goal "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))";
   4.297 +by (stac split_split 1);
   4.298 +by (Simp_tac 1);
   4.299 +qed "split_split_asm";
   4.300 +
   4.301 +(** split used as a logical connective or set former **)
   4.302 +
   4.303 +(*These rules are for use with blast_tac.
   4.304 +  Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
   4.305 +
   4.306 +Goal "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
   4.307 +by (split_all_tac 1);
   4.308 +by (Asm_simp_tac 1);
   4.309 +qed "splitI2";
   4.310 +
   4.311 +Goal "!!p. [| !!a b. (a,b)=p ==> c a b x |] ==> split c p x";
   4.312 +by (split_all_tac 1);
   4.313 +by (Asm_simp_tac 1);
   4.314 +qed "splitI2'";
   4.315 +
   4.316 +Goal "c a b ==> split c (a,b)";
   4.317 +by (Asm_simp_tac 1);
   4.318 +qed "splitI";
   4.319 +
   4.320 +val prems = Goalw [split_def]
   4.321 +    "[| split c p;  !!x y. [| p = (x,y);  c x y |] ==> Q |] ==> Q";
   4.322 +by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   4.323 +qed "splitE";
   4.324 +
   4.325 +val prems = Goalw [split_def]
   4.326 +    "[| split c p z;  !!x y. [| p = (x,y);  c x y z |] ==> Q |] ==> Q";
   4.327 +by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   4.328 +qed "splitE'";
   4.329 +
   4.330 +val major::prems = Goal
   4.331 +    "[| Q (split P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R  \
   4.332 +\    |] ==> R";
   4.333 +by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   4.334 +by (rtac (split_beta RS subst) 1 THEN rtac major 1);
   4.335 +qed "splitE2";
   4.336 +
   4.337 +Goal "split R (a,b) ==> R a b";
   4.338 +by (etac (split_conv RS iffD1) 1);
   4.339 +qed "splitD";
   4.340 +
   4.341 +Goal "z: c a b ==> z: split c (a,b)";
   4.342 +by (Asm_simp_tac 1);
   4.343 +qed "mem_splitI";
   4.344 +
   4.345 +Goal "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p";
   4.346 +by (split_all_tac 1);
   4.347 +by (Asm_simp_tac 1);
   4.348 +qed "mem_splitI2";
   4.349 +
   4.350 +val prems = Goalw [split_def]
   4.351 +    "[| z: split c p;  !!x y. [| p = (x,y);  z: c x y |] ==> Q |] ==> Q";
   4.352 +by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   4.353 +qed "mem_splitE";
   4.354 +
   4.355 +AddSIs [splitI, splitI2, splitI2', mem_splitI, mem_splitI2];
   4.356 +AddSEs [splitE, splitE', mem_splitE];
   4.357 +
   4.358 +Goal "(%u. ? x y. u = (x, y) & P (x, y)) = P";
   4.359 +by (rtac ext 1);
   4.360 +by (Fast_tac 1);
   4.361 +qed "split_eta_SetCompr";
   4.362 +Addsimps [split_eta_SetCompr];
   4.363 +
   4.364 +Goal "(%u. ? x y. u = (x, y) & P x y) = split P";
   4.365 +br ext 1;
   4.366 +by (Fast_tac 1);
   4.367 +qed "split_eta_SetCompr2";
   4.368 +Addsimps [split_eta_SetCompr2];
   4.369 +
   4.370 +(* allows simplifications of nested splits in case of independent predicates *)
   4.371 +Goal "(%(a,b). P & Q a b) = (%ab. P & split Q ab)";
   4.372 +by (rtac ext 1);
   4.373 +by (Blast_tac 1);
   4.374 +qed "split_part";
   4.375 +Addsimps [split_part];
   4.376 +
   4.377 +Goal "(@(x',y'). x = x' & y = y') = (x,y)";
   4.378 +by (Blast_tac 1);
   4.379 +qed "Eps_split_eq";
   4.380 +Addsimps [Eps_split_eq];
   4.381 +(*
   4.382 +the following  would be slightly more general,
   4.383 +but cannot be used as rewrite rule:
   4.384 +### Cannot add premise as rewrite rule because it contains (type) unknowns:
   4.385 +### ?y = .x
   4.386 +Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)";
   4.387 +by (rtac some_equality 1);
   4.388 +by ( Simp_tac 1);
   4.389 +by (split_all_tac 1);
   4.390 +by (Asm_full_simp_tac 1);
   4.391 +qed "Eps_split_eq";
   4.392 +*)
   4.393 +
   4.394 +(*** prod_fun -- action of the product functor upon functions ***)
   4.395 +
   4.396 +Goalw [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
   4.397 +by (rtac split_conv 1);
   4.398 +qed "prod_fun";
   4.399 +Addsimps [prod_fun];
   4.400 +
   4.401 +Goal "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
   4.402 +by (rtac ext 1);
   4.403 +by (pair_tac "x" 1);
   4.404 +by (Asm_simp_tac 1);
   4.405 +qed "prod_fun_compose";
   4.406 +
   4.407 +Goal "prod_fun (%x. x) (%y. y) = (%z. z)";
   4.408 +by (rtac ext 1);
   4.409 +by (pair_tac "z" 1);
   4.410 +by (Asm_simp_tac 1);
   4.411 +qed "prod_fun_ident";
   4.412 +Addsimps [prod_fun_ident];
   4.413 +
   4.414 +Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)`r";
   4.415 +by (rtac image_eqI 1);
   4.416 +by (rtac (prod_fun RS sym) 1);
   4.417 +by (assume_tac 1);
   4.418 +qed "prod_fun_imageI";
   4.419 +
   4.420 +val major::prems = Goal
   4.421 +    "[| c: (prod_fun f g)`r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P  \
   4.422 +\    |] ==> P";
   4.423 +by (rtac (major RS imageE) 1);
   4.424 +by (res_inst_tac [("p","x")] PairE 1);
   4.425 +by (resolve_tac prems 1);
   4.426 +by (Blast_tac 2);
   4.427 +by (blast_tac (claset() addIs [prod_fun]) 1);
   4.428 +qed "prod_fun_imageE";
   4.429 +
   4.430 +AddIs  [prod_fun_imageI];
   4.431 +AddSEs [prod_fun_imageE];
   4.432 +
   4.433 +
   4.434 +(*** Disjoint union of a family of sets - Sigma ***)
   4.435 +
   4.436 +Goalw [Sigma_def] "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B";
   4.437 +by (REPEAT (ares_tac [singletonI,UN_I] 1));
   4.438 +qed "SigmaI";
   4.439 +
   4.440 +AddSIs [SigmaI];
   4.441 +
   4.442 +(*The general elimination rule*)
   4.443 +val major::prems = Goalw [Sigma_def]
   4.444 +    "[| c: Sigma A B;  \
   4.445 +\       !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P \
   4.446 +\    |] ==> P";
   4.447 +by (cut_facts_tac [major] 1);
   4.448 +by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ;
   4.449 +qed "SigmaE";
   4.450 +
   4.451 +(** Elimination of (a,b):A*B -- introduces no eigenvariables **)
   4.452 +
   4.453 +Goal "(a,b) : Sigma A B ==> a : A";
   4.454 +by (etac SigmaE 1);
   4.455 +by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ;
   4.456 +qed "SigmaD1";
   4.457 +
   4.458 +Goal "(a,b) : Sigma A B ==> b : B(a)";
   4.459 +by (etac SigmaE 1);
   4.460 +by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ;
   4.461 +qed "SigmaD2";
   4.462 +
   4.463 +val [major,minor]= Goal
   4.464 +    "[| (a,b) : Sigma A B;    \
   4.465 +\       [| a:A;  b:B(a) |] ==> P   \
   4.466 +\    |] ==> P";
   4.467 +by (rtac minor 1);
   4.468 +by (rtac (major RS SigmaD1) 1);
   4.469 +by (rtac (major RS SigmaD2) 1) ;
   4.470 +qed "SigmaE2";
   4.471 +
   4.472 +AddSEs [SigmaE2, SigmaE];
   4.473 +
   4.474 +val prems = Goal
   4.475 +    "[| A<=C;  !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
   4.476 +by (cut_facts_tac prems 1);
   4.477 +by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
   4.478 +qed "Sigma_mono";
   4.479 +
   4.480 +Goal "Sigma {} B = {}";
   4.481 +by (Blast_tac 1) ;
   4.482 +qed "Sigma_empty1";
   4.483 +
   4.484 +Goal "A <*> {} = {}";
   4.485 +by (Blast_tac 1) ;
   4.486 +qed "Sigma_empty2";
   4.487 +
   4.488 +Addsimps [Sigma_empty1,Sigma_empty2];
   4.489 +
   4.490 +Goal "UNIV <*> UNIV = UNIV";
   4.491 +by Auto_tac;
   4.492 +qed "UNIV_Times_UNIV";
   4.493 +Addsimps [UNIV_Times_UNIV];
   4.494 +
   4.495 +Goal "- (UNIV <*> A) = UNIV <*> (-A)";
   4.496 +by Auto_tac;
   4.497 +qed "Compl_Times_UNIV1";
   4.498 +
   4.499 +Goal "- (A <*> UNIV) = (-A) <*> UNIV";
   4.500 +by Auto_tac;
   4.501 +qed "Compl_Times_UNIV2";
   4.502 +
   4.503 +Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2];
   4.504 +
   4.505 +Goal "((a,b): Sigma A B) = (a:A & b:B(a))";
   4.506 +by (Blast_tac 1);
   4.507 +qed "mem_Sigma_iff";
   4.508 +AddIffs [mem_Sigma_iff];
   4.509 +
   4.510 +Goal "x:C ==> (A <*> C <= B <*> C) = (A <= B)";
   4.511 +by (Blast_tac 1);
   4.512 +qed "Times_subset_cancel2";
   4.513 +
   4.514 +Goal "x:C ==> (A <*> C = B <*> C) = (A = B)";
   4.515 +by (blast_tac (claset() addEs [equalityE]) 1);
   4.516 +qed "Times_eq_cancel2";
   4.517 +
   4.518 +Goal "Collect (split (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))";
   4.519 +by (Fast_tac 1);
   4.520 +qed "SetCompr_Sigma_eq";
   4.521 +
   4.522 +(*** Complex rules for Sigma ***)
   4.523 +
   4.524 +Goal "{(a,b). P a & Q b} = Collect P <*> Collect Q";
   4.525 +by (Blast_tac 1);
   4.526 +qed "Collect_split";
   4.527 +
   4.528 +Addsimps [Collect_split];
   4.529 +
   4.530 +(*Suggested by Pierre Chartier*)
   4.531 +Goal "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)";
   4.532 +by (Blast_tac 1);
   4.533 +qed "UN_Times_distrib";
   4.534 +
   4.535 +Goal "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))";
   4.536 +by (Fast_tac 1);
   4.537 +qed "split_paired_Ball_Sigma";
   4.538 +Addsimps [split_paired_Ball_Sigma];
   4.539 +
   4.540 +Goal "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))";
   4.541 +by (Fast_tac 1);
   4.542 +qed "split_paired_Bex_Sigma";
   4.543 +Addsimps [split_paired_Bex_Sigma];
   4.544 +
   4.545 +Goal "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))";
   4.546 +by (Blast_tac 1);
   4.547 +qed "Sigma_Un_distrib1";
   4.548 +
   4.549 +Goal "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))";
   4.550 +by (Blast_tac 1);
   4.551 +qed "Sigma_Un_distrib2";
   4.552 +
   4.553 +Goal "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))";
   4.554 +by (Blast_tac 1);
   4.555 +qed "Sigma_Int_distrib1";
   4.556 +
   4.557 +Goal "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))";
   4.558 +by (Blast_tac 1);
   4.559 +qed "Sigma_Int_distrib2";
   4.560 +
   4.561 +Goal "(SIGMA i:I - J. C(i)) = (SIGMA i:I. C(i)) - (SIGMA j:J. C(j))";
   4.562 +by (Blast_tac 1);
   4.563 +qed "Sigma_Diff_distrib1";
   4.564 +
   4.565 +Goal "(SIGMA i:I. A(i) - B(i)) = (SIGMA i:I. A(i)) - (SIGMA i:I. B(i))";
   4.566 +by (Blast_tac 1);
   4.567 +qed "Sigma_Diff_distrib2";
   4.568 +
   4.569 +Goal "Sigma (Union X) B = (UN A:X. Sigma A B)";
   4.570 +by (Blast_tac 1);
   4.571 +qed "Sigma_Union";
   4.572 +
   4.573 +(*Non-dependent versions are needed to avoid the need for higher-order
   4.574 +  matching, especially when the rules are re-oriented*)
   4.575 +Goal "(A Un B) <*> C = (A <*> C) Un (B <*> C)";
   4.576 +by (Blast_tac 1);
   4.577 +qed "Times_Un_distrib1";
   4.578 +
   4.579 +Goal "(A Int B) <*> C = (A <*> C) Int (B <*> C)";
   4.580 +by (Blast_tac 1);
   4.581 +qed "Times_Int_distrib1";
   4.582 +
   4.583 +Goal "(A - B) <*> C = (A <*> C) - (B <*> C)";
   4.584 +by (Blast_tac 1);
   4.585 +qed "Times_Diff_distrib1";
   4.586 +
   4.587 +
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/split_rule.ML	Thu Feb 01 20:51:48 2001 +0100
     5.3 @@ -0,0 +1,95 @@
     5.4 +(*Attempts to remove occurrences of split, and pair-valued parameters*)
     5.5 +val remove_split = rewrite_rule [split_conv RS eq_reflection] o split_all;
     5.6 +
     5.7 +local
     5.8 +
     5.9 +(*In ap_split S T u, term u expects separate arguments for the factors of S,
    5.10 +  with result type T.  The call creates a new term expecting one argument
    5.11 +  of type S.*)
    5.12 +fun ap_split (Type ("*", [T1, T2])) T3 u =
    5.13 +      HOLogic.split_const (T1, T2, T3) $
    5.14 +      Abs("v", T1,
    5.15 +          ap_split T2 T3
    5.16 +             ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $
    5.17 +              Bound 0))
    5.18 +  | ap_split T T3 u = u;
    5.19 +
    5.20 +(*Curries any Var of function type in the rule*)
    5.21 +fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) =
    5.22 +      let val T' = HOLogic.prodT_factors T1 ---> T2
    5.23 +          val newt = ap_split T1 T2 (Var (v, T'))
    5.24 +          val cterm = Thm.cterm_of (#sign (rep_thm rl))
    5.25 +      in
    5.26 +          instantiate ([], [(cterm t, cterm newt)]) rl
    5.27 +      end
    5.28 +  | split_rule_var' (t, rl) = rl;
    5.29 +
    5.30 +(*** Complete splitting of partially splitted rules ***)
    5.31 +
    5.32 +fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
    5.33 +      (ap_split T (flat (map HOLogic.prodT_factors Ts) ---> U)
    5.34 +        (incr_boundvars 1 u) $ Bound 0))
    5.35 +  | ap_split' _ _ u = u;
    5.36 +
    5.37 +fun complete_split_rule_var ((t as Var (v, T), ts), (rl, vs)) =
    5.38 +      let
    5.39 +        val cterm = Thm.cterm_of (#sign (rep_thm rl))
    5.40 +        val (Us', U') = strip_type T;
    5.41 +        val Us = take (length ts, Us');
    5.42 +        val U = drop (length ts, Us') ---> U';
    5.43 +        val T' = flat (map HOLogic.prodT_factors Us) ---> U;
    5.44 +        fun mk_tuple ((xs, insts), v as Var ((a, _), T)) =
    5.45 +              let
    5.46 +                val Ts = HOLogic.prodT_factors T;
    5.47 +                val ys = variantlist (replicate (length Ts) a, xs);
    5.48 +              in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
    5.49 +                (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
    5.50 +              end
    5.51 +          | mk_tuple (x, _) = x;
    5.52 +        val newt = ap_split' Us U (Var (v, T'));
    5.53 +        val cterm = Thm.cterm_of (#sign (rep_thm rl));
    5.54 +        val (vs', insts) = foldl mk_tuple ((vs, []), ts);
    5.55 +      in
    5.56 +        (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
    5.57 +      end
    5.58 +  | complete_split_rule_var (_, x) = x;
    5.59 +
    5.60 +fun collect_vars (vs, Abs (_, _, t)) = collect_vars (vs, t)
    5.61 +  | collect_vars (vs, t) = (case strip_comb t of
    5.62 +        (v as Var _, ts) => (v, ts)::vs
    5.63 +      | (t, ts) => foldl collect_vars (vs, ts));
    5.64 +
    5.65 +in
    5.66 +
    5.67 +val split_rule_var = standard o remove_split o split_rule_var';
    5.68 +
    5.69 +(*Curries ALL function variables occurring in a rule's conclusion*)
    5.70 +fun split_rule rl = standard (remove_split (foldr split_rule_var' (term_vars (concl_of rl), rl)));
    5.71 +
    5.72 +fun complete_split_rule rl =
    5.73 +  standard (remove_split (fst (foldr complete_split_rule_var
    5.74 +    (collect_vars ([], concl_of rl),
    5.75 +     (rl, map (fst o fst o dest_Var) (term_vars (#prop (rep_thm rl))))))))
    5.76 +	|> RuleCases.save rl;
    5.77 +
    5.78 +end;
    5.79 +fun complete_split x = 
    5.80 +	Attrib.no_args (Drule.rule_attribute (K complete_split_rule)) x;
    5.81 +
    5.82 +fun split_rule_goal xss rl = let 
    5.83 +	val ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv]; 
    5.84 +	fun one_split i (th,s) = rule_by_tactic (pair_tac s i) th;
    5.85 +	fun one_goal (xs,i) th = foldl (one_split i) (th,xs);
    5.86 +        in standard (Simplifier.full_simplify ss (foldln one_goal xss rl))
    5.87 +	   |> RuleCases.save rl
    5.88 +        end;
    5.89 +fun split_format x = 
    5.90 +	Attrib.syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name)) 
    5.91 +	>> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x;
    5.92 +
    5.93 +val split_attributes = [Attrib.add_attributes 
    5.94 +	[("complete_split", (complete_split, complete_split), 
    5.95 +          "recursively split all pair-typed function arguments"),
    5.96 +	 ("split_format", (split_format, split_format), 
    5.97 +          "split given pair-typed subterms in premises")]];
    5.98 +
     6.1 --- a/src/HOL/ex/cla.ML	Thu Feb 01 20:51:13 2001 +0100
     6.2 +++ b/src/HOL/ex/cla.ML	Thu Feb 01 20:51:48 2001 +0100
     6.3 @@ -462,7 +462,8 @@
     6.4  
     6.5  (*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
     6.6    Fast_tac indeed copes!*)
     6.7 -goal Product_Type.thy "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \
     6.8 +goal (theory "Product_Type") 
     6.9 +             "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \
    6.10  \             (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y))) &   \
    6.11  \             (ALL x. K(x) --> ~G(x))  -->  (EX x. K(x) & J(x))";
    6.12  by (Fast_tac 1);
    6.13 @@ -470,7 +471,7 @@
    6.14  
    6.15  (*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.  
    6.16    It does seem obvious!*)
    6.17 -goal Product_Type.thy
    6.18 +goal (theory "Product_Type")
    6.19      "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) &        \
    6.20  \    (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y)))  &        \
    6.21  \    (ALL x. K(x) --> ~G(x))   -->   (EX x. K(x) --> ~G(x))";
    6.22 @@ -488,7 +489,7 @@
    6.23  by (Blast_tac 1);
    6.24  result();
    6.25  
    6.26 -goal Product_Type.thy
    6.27 +goal (theory "Product_Type")
    6.28      "(ALL x y. R(x,y) | R(y,x)) &                \
    6.29  \    (ALL x y. S(x,y) & S(y,x) --> x=y) &        \
    6.30  \    (ALL x y. R(x,y) --> S(x,y))    -->   (ALL x y. S(x,y) --> R(x,y))";
     7.1 --- a/src/HOLCF/Cprod1.ML	Thu Feb 01 20:51:13 2001 +0100
     7.2 +++ b/src/HOLCF/Cprod1.ML	Thu Feb 01 20:51:48 2001 +0100
     7.3 @@ -11,11 +11,12 @@
     7.4  (* less_cprod is a partial order on 'a * 'b                                 *)
     7.5  (* ------------------------------------------------------------------------ *)
     7.6  
     7.7 +(*###TO Product_Type_lemmas.ML *)
     7.8  Goal "[|fst x = fst y; snd x = snd y|] ==> x = y";
     7.9  by (subgoal_tac "(fst x,snd x)=(fst y,snd y)" 1);
    7.10  by (rotate_tac ~1 1);
    7.11  by (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing RS sym])1);
    7.12 -by (asm_simp_tac (simpset_of Product_Type.thy) 1);
    7.13 +by (asm_simp_tac (simpset_of (theory "Product_Type")) 1);
    7.14  qed "Sel_injective_cprod";
    7.15  
    7.16  Goalw [less_cprod_def] "(p::'a*'b) << p";